Several justification logics have been created, starting with the logic LP, [1]. These can be thought of as explicit versions of modal logics, or of logics of knowledge or belief, in which the unanalyzed necessity (knowledge, belief) operator has been replaced with a family of explicit justification terms. We begin by sketching the basics of justification logics and their relations with modal logics. Then we move to new material. Modal logics come in various strengths. For their corresponding justification logics, differing (...) strength is reflected in different vocabularies. What we show here is that for justification logics corresponding to modal logics extending T, various familiar extensions are actually conservative with respect to each other. Our method of proof is very simple, and general enough to handle several justification logics not directly corresponding to distinct modal logics. Our methods do not, however, allow us to prove comparable results for justification logics corresponding to modal logics that do not extend T. That is, we are able to handle explicit logics of knowledge, but not explicit logics of belief. This remains open. (shrink)

A new semantics is presented for the logic of proofs (LP), [1, 2], based on the intuition that it is a logic of explicit knowledge. This semantics is used to give new proofs of several basic results concerning LP. In particular, the realization of S4 into LP is established in a way that carefully examines and explicates the role of the + operator. Finally connections are made with the conventional approach, via soundness and completeness results.

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)

LP can be seen as a logic of knowledge with justifications. See [S. Artemov, The logic of justification, The Review of Symbolic Logic 1 477–513] for a recent comprehensive survey of justification logics generally. Artemov’s Realization Theorem says justifications can be extracted from validities in the more conventional Hintikka-style logic of knowledge S4, in which they are not explicitly present. Justifications, however, are far from unique. There are many ways of realizing each theorem of S4 in the logic LP. If (...) the machinery of justifications is to be applied to artificial intelligence, or better yet, to everyday reasoning, we will need to work with whatever justifications we may have at hand—one version may not be interchangeable with another, even though they realize the same S4 formula. In this paper we begin the process of providing tools for reasoning about justifications directly. The tools are somewhat complex, but in retrospect this should not be surprising. Among other things, we provide machinery for combining two realizations of the same formula, and for replacing subformulas by equivalent subformulas. The results are algorithmic in nature—semantics for LP plays no role. We apply our results to provide a new algorithmic proof of Artemov’s Realization Theorem itself. This paper is a much extended version of [M.C. Fitting, Realizations and LP, in: S. Artemov, A. Nerode , Logical Foundations of Computer Science—New York ’07, in: Lecture Notes in Computer Science, vol. 4514, Springer-Verlag, 2007, pp. 212–223]. (shrink)

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)

Justification logics are logics of knowledge in which explicit reasons are formally represented. Standard logics of knowledge have justification logic analogs. Connecting justification logics and logics of knowledge are Realization Theorems. In this paper we give a new, constructive proof of the Realization Theorem connecting S5 and its justification analog, JS5. This proof is, I believe, the simplest in the literature.