Justification Logic provides an axiomatic description of justifications and delegates the question of their nature to semantics. In this note, we address the conceptual issue of the logical type of justifications: we argue that justifications in the logical setting are naturally interpreted as sets of formulas which leads to a class of epistemic models that we call modular models . We show that Fitting models for Justification Logic naturally encode modular models and can be regarded as convenient pre-models of the (...) former. (shrink)
We describe a general logical framework, Justification Logic, for reasoning about epistemic justification. Justification Logic is based on classical propositional logic augmented by justification assertions t: F that read t is a justification for F. Justification Logic absorbs basic principles originating from both mainstream epistemology and the mathematical theory of proofs. It contributes to the studies of the well-known Justified True Belief vs. Knowledge problem. We state a general Correspondence Theorem showing that behind each epistemic modal logic, there is a (...) robust system of justifications. This renders a new, evidence-based foundation for epistemic logic. As a case study, we offer a resolution of the GoldmanRed Barns in Justification Logic. Furthermore, we formalize the well-known Gettier example and reveal hidden assumptions and redundancies in Gettier’s reasoning. (shrink)
Justification Logic is a family of epistemic logical systems obtained from modal logics of knowledge by adding a new type of formula t:F, which is read t is a justification for F. The principal epistemic modal logic S4 includes Tarski’s well-known topological interpretation, according to which the modality 2X is read the Interior of X in a topological space (the topological equivalent of the ‘knowable part of X’). In this paper, we extend Tarski’s topological interpretation from S4 to Justification Logic (...) systems with both modality and justification assertions. The topological semantics interprets t:X as a reachable subset of X (the topological equivalent of ‘test t confirms X’). We establish a number of soundness and completeness results with respect to Kripke topology and the real topology for S4-based systems of Justification Logic. (shrink)
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.
In 1933 Godel introduced a calculus of provability (also known as modal logic S4) and left open the question of its exact intended semantics. In this paper we give a solution to this problem. We find the logic LP of propositions and proofs and show that Godel's provability calculus is nothing but the forgetful projection of LP. This also achieves Godel's objective of defining intuitionistic propositional logic Int via classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics for Int which (...) resisted formalization since the early 1930s. LP may be regarded as a unified underlying structure for intuitionistic, modal logics, typed combinatory logic and λ-calculus. (shrink)
ABSTRACT In 1933 Gödel introduced an axiomatic system, currently known as S4, for a logic of an absolute provability, i.e. not depending on the formalism chosen ([God 33]). The problem of finding a fair provability model for S4 was left open. The famous formal provability predicate which first appeared in the Gödel Incompleteness Theorem does not do this job: the logic of formal provability is not compatible with S4. As was discovered in [Art 95], this defect of the formal provability (...) predicate can be bypassed by replacing hidden quantifiers over proofs by proof polynomials in a certain finite basis. The resulting Logic of Proofs enjoys a natural arithmetical semantics and provides an intended provability model for S4, thus answering a question left open by Gödel in 1933. Proof polynomials give an intended semantics for some other constructions based on the concept of provability, including intuitionistic logic with its Brouwer- Heyting- Kolmogorov interpretation, ?-calculus and modal ?-calculus. In the current paper we demonstrate how the intuitionistic propositional logic Int can be directly realized by proof polynomials. It is shown, that Int is complete with respect to this proof realizability. (shrink)
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.
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 \nvdash 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. (shrink)