Abstract The consistency of a theory means that each of its formal derivations $D_{0}, D_{1}, D_{2}, \ldots $ is free of contradictions. For Peano Arithmetic PA, after the standard coding of derivations by numerals, PA-consistency is directly represented by the consistency scheme $\textsf{Con}^{S}_{\textsf{PA}}$, which is a series of arithmetical statements ‘$n$ is not a code of a derivation of $\ (0=1)$’ for numerals $n=0,1,2,\ldots $. We note that the consistency formula $\textsf{Con}_{\textsf{PA}}$, $\forall x$ ‘$x$ is not a code of a derivation of $(0=1)$,’ is strictly stronger in PA than PA-consistency and corresponds to some other property, which we call uniform consistency. When studying the provability of consistency in PA we ought to work not with the consistency formula $\textsf{Con}_{\textsf{PA}}$ but rather with the consistency scheme $\textsf{Con}^{S}_{\textsf{PA}}$, which adequately represents PA-consistency. This paper introduces the Hilbert-inspired notion of proof of an infinite series of formulas in a theory and proves PA-consistency in the form $\textsf{Con}^{S}_{\textsf{PA}}$ in PA. These findings show that PA proves its consistency whereas, by Gödel’s second incompleteness theorem, PA cannot prove its uniform consistency.

Traditionally, Epistemic Logic represents epistemic scenarios using a single model. This, however, covers only complete descriptions that specify truth values of all assertions. Indeed, many—and perhaps most—epistemic descriptions are not complete. Syntactic Epistemic Logic, SEL, suggests viewing an epistemic situation as a set of syntactic conditions rather than as a model. This allows us to naturally capture incomplete descriptions; we discuss a case study in which our proposal is successful. In Epistemic Game Theory, this closes the conceptual and technical gap, identified by R. Aumann, between the syntactic character of game-descriptions and semantic representations of games.

This volume stems from the International Symposium on Logical Foundations of Computer Science (LFCS’22), held online, 10–13 January 2022. Subsequent to that meeting, some of the speakers were invited to contribute to this volume. The LFCS’22 Steering Committee consisted of Anil Nerode (Ithaca, NY, USA; General Chair), Samuel Buss (San Diego, CA, USA), Stephen Cook (Toronto), Dirk van Dalen (Utrecht), Yuri Matiyasevich (St. Petersburg), Andre Scedrov (Philadelphia, PA) and Dana Scott (Pittsburgh, PA/Berkeley, CA, USA). LFCS’22 topics of interest included, but were not limited to, constructive mathematics and type theory; homotopy-type theory; logic, automata and automatic structures; computability and randomness; logical foundations of programming; logical aspects of computational complexity; parameterized complexity; logic programming and constraints; automated deduction and interactive theorem proving; logical methods in protocol and program verification; logical methods in program specification and extraction; domain theory logics; logical foundations of database theory; equational logic and term rewriting; lambda and combinatory calculi; categorical logic and topological semantics; linear logic; epistemic and temporal logics; intelligent and multiple-agent system logics; logics of proof and justification; non-monotonic reasoning; logic in game theory and social software; logic of hybrid systems; distributed system logics; mathematical fuzzy logic; system design logics; and other logics in computer science.

Abstract Imagine a database—a set of propositions $\varGamma =\{F_1,\ldots ,F_n\}$ with some kind of probability estimates and let a proposition $X$ logically follow from $\varGamma $. What is the best justified lower bound of the probability of $X$? The traditional approach, e.g. within Adams’ probability logic, computes the numeric lower bound for $X$ corresponding to the worst-case scenario. We suggest a more flexible parameterized approach by assuming probability events $u_1,u_2,\ldots ,u_n$ that support $\varGamma $ and calculating aggregated evidence$e(u_1,u_2,\ldots ,u_n)$ for $X$. The probability of $e$ provides a tight lower bound for any, not only a worst-case, situation. The problem is formalized in a version of justification logic and the conclusions are supported by corresponding completeness theorems. This approach can handle conflicting and inconsistent data and allows the gathering both positive and negative evidence for the same proposition.

Abstract We offer a new semantic approach to formal epistemology that incorporates two principal ideas: (i) justifications are prime objects of the model: knowledge and belief are defined evidence-based concepts; (ii) awareness restrictions are applied to justifications rather than to propositions, which allows for the maintaining of desirable closure properties. The resulting structures, Justification Awareness Models, JAMs, naturally include major justification models, Kripke models and, in addition, represent situations with multiple possibly fallible justifications which, in full generality, were previously off the scope of rigorous epistemic modeling.

The origins of this volume are with The International Symposium on Logical Foundations of Computer Science (LFCS’16), held in Deerfield Beach, Florida, January 4 – 7, 2016. Afterwards, some speakers were invited to contribute to a volume, and the invitation was extended more generally as well. LFCS’16 Steering Committee comprised Anil Nerode, (Ithaca, NY, General Chair); Stephen Cook (Toronto); Dirk van Dalen (Utrecht); Yuri Matiyasevich (St. Petersburg); Alan Robinson (Syracuse, NY); Gerald Sacks (Cambridge, MA); Dana Scott, (Pittsburgh, PA – Berkeley, CA). LFCS’16 topics of interest included, but were not limited to: constructive mathematics and type theory; homotopy type theory; logic, automata, and automatic structures; computability and randomness; logical foundations of programming; logical aspects of computational complexity; parameterized complexity; logic programming and constraints; automated deduction and interactive theorem proving; logical methods in protocol and program verification; logical methods in program specification and extraction; domain theory logics; logical foundations of database theory; equational logic and term rewriting; lambda and combinatory calculi; categorical logic and topological semantics; linear logic; epistemic and temporal logics; intelligent and multiple-agent system logics; logics of proof and justification; non-monotonic reasoning; logic in game theory and social software; logic of hybrid systems; distributed system logics; mathematical fuzzy logic; system design logics; other logics in computer science.

The standard first-order reading of modality does not bind individual variables, i.e. if x is free in F ( x ), then x remains free in □ F ( x ). Accordingly, if □ stands for ‘provable in arithmetic,’ ∀ x □ F ( x ) states that F ( n ) is provable for any given value of n = 0,1,2,...; this corresponds to a de re reading of modality. The other, de dicto meaning of □ F ( x ), suggesting that F ( x ) is derivable as a formula with a free variable x , is not directly represented by a modality, though, semantically, it could be approximated by compound constructions, e.g. □∀ xF ( x ). We introduce the first-order logic FOS4* in which modalities can bind individual variables and, in particular, can directly represent both de re and de dicto modalities. FOS4* extends first-order S4 and is the natural forgetful projection of the first-order logic of proofs FOLP. The same method of introducing binding modalities obviously works for other modal logics as well.

The logical omniscience feature assumes that an epistemic agent knows all logical consequences of her assumptions. This paper offers a general theoretical framework that views logical omniscience as a computational complexity problem. We suggest the following approach: we assume that the knowledge of an agent is represented by an epistemic logical system E; we call such an agent not logically omniscient if for any valid knowledge assertion A of type F is known, a proof of F in E can be found in polynomial time in the size of A. We show that agents represented by major modal logics of knowledge and belief are logically omniscient, whereas agents represented by justification logic systems are not logically omniscient with respect to t is a justification for F.

Abstract The language of the basic logic of proofs extends the usual propositional language by forming sentences of the sort x is a proof of F for any sentence F. In this paper a complete axiomatization for the basic logic of proofs in Heyting Arithmetic HA was found.

Plato's tripartite definition of knowledge as justified true belief (JTB) is generally regarded as a set of necessary conditions for the possession of knowledge. The true belief components the JTB definition are represented in formal epistemology by modal logic and its possible worlds semantics. At the same time, the justification component of Plato's definition did not have a formal representation. This paper introduces the notion of justification into formal epistemology. Epistemic logic with justification, along with the usual knowledge operator □F (F is known), contains assertions t:F (t is a justification for F). We study two basic systems, S4LP and S4LPN, of epistemic logic with justification and show completeness with respect to natural epistemic semantics, which augments Kripke models with a natural Fitting-style treatment of justification assertions t:F. Some new specific properties of epistemic logic with justification are established.

Abstract In this paper the modal operator “x is provable in Peano Arithmetic” is incorporated into first-order theories. A provability extension of a theory is defined. Presburger Arithmetic of addition, Skolem Arithmetic of multiplication, and some first order theories of partial consistency statements are shown to remain decidable after natural provability extensions. It is also shown that natural provability extensions of a decidable theory may be undecidable.

Abstract The paper proves a predicate version of Solovay's well-known theorem on provability interpretations of modal logic: If a closed modal predicate-logical formula R is not valid in some finite Kripke model, then there exists an arithmetical interpretation f such that PA ⊬ fR. This result implies the arithmetical completeness of arithmetically correct modal predicate logics with the finite model property (including the one-variable fragments of QGL and QS). The proof was obtained by adding “the predicate part” as a specific addition to the standard Solovay construction.