1 What Is This Book About?
How did justification logics originate? It is an interesting story, with revealing changes of direction along the way. Going back to the days when Godel was a young logician, there was a dream of finding a provability interpretation for intuitionistic logic.
As part of his work on that project, in Godel (1933), Godel showed that one could abstract some of the key features of provability and make a propositional modal logic using them. Then, remarkably but naturally, one could embed propositional intuitionistic logic into the resulting system. C. I. Lewis had pioneered the modern formal study of modal logics (Lewis, 1918; Lewis and Langford, 1932), and Godel observed that his system was equivalent to the Lewis system S4. All modern axiomatizations of modal logics follow the lines pioneered in Godel’s note, while Lewis’s original formulation is rarely seen today. Godel showed that propositional intuitionistic logic embedded into S4 using a mapping that inserted
in front of every subformula. In effect, intuitionistic logic could be understood using classical logic plus an abstract notion of provability: a propositional formula X is an intuitionistic theorem if and only if the result of applying Godel’s mapping is a theorem of S4. (This story is somewhat simplified. There are several versions of the Godel translation—we have used the simplest one to describe. And Godel did not use the symbol
but rather an operator Bew, short for beweisbar, or provability in the German language. None of this affects our main points.) Unfortunately, the story breaks off at this point because Gddel also noted that S4 does not behave like formal provability (e.g., in arithmetic), by using the methods he had pioneered in his work on incompleteness. Specifically, S4 validates 
S4 into formal arithmetic under which ? corresponded to Godel’s arithmetic formula representing provability, we would be able to prove in arithmetic that falsehood was not provable. That is, we would be able to show provability of consistency, violating Godel’s second incompleteness theorem. So, work on an arithmetic semantics for propositional intuitionistic logic paused for a while.
Although it did not solve the problem of a provability semantics for in- tuitionistic logic, an important modal/arithmetic connection was eventually worked out. One can define a modal logic by requiring that its validities are
By now the project for finding an arithmetic interpretation of intuitionistic logic had reached an impasse. Intuitionistic logic embedded into S4, but S4 did not embed into formal arithmetic. GL embedded into formal arithmetic, but the Godel translation does not embed intuitionistic logic into GL.
In his work on incompleteness for Peano arithmetic, Godel gave a formula
Bew(x, y)
that represents the relation: x is the GOdel number of a proof of a formula with Godel number y. Then, a formal version of provability is
3 xBew(x, y)
which expresses that there is a proof of (the formula whose Godel number is) 
outside the formal language. We provide an explicit proof term, rather than just asserting that one exists. Godel believed that this approach should lead to a provability embedding of S4 into Peano arithmetic.
GodeTs proposal was not published until 1995 when Volume 3 of his collected works appeared. By this time the idea of using a modal-like language with explicit representatives for proofs had been rediscovered independently by Sergei Artemov, see Artemov (1995, 2001).
The logic that Artemov created was called LP, which stood for logic of proofs. It was the first example of a justification logic. What are now called justification terms were called proof terms in LP.Crucially, Artemov showed LP filled the gap between modal S4 and Peano arithmetic. The connection with S4 is primarily embodied in a Realization Theorem, which has since been shown to hold for a wide range of justification logic, modal logic pairs. It will be extensively examined in this book. The connection between LP and formal arithmetic is Artemov’s Arithmetic Completeness Theorem, which also will be examined in this book. Its range is primarily limited to the original justification logic, LP, and a few close relatives. This should not be surprising, though. Godel’s motivation for his formulation of S4 was that ? should embody properties of a formal arithmetic proof predicate. This connection with arithmetic provability is not present for almost all modal
logics and is consequently also missing for corresponding justification logics, when they exist. Nonetheless, the venerable goal of finding a provability interpretation for propositional intuitionistic logic had been attained. The Godel translation embeds propositional intuitionistic logic into the modal logic S4. The Realization Theorem establishes an embedding of S4 into the justification logic LP. And the Arithmetic Completeness Theorem shows that LP embeds into formal arithmetic.
It was recognized from the very beginning that the connection between S4 and LP could be weakened to sublogics of S4 and LP. Thus, there were justification logic counterparts for the standard modal logics, K, K4, T, and a few others. Thesejustification logics had arithmetic connections because they were sublogics of LP. The use of proof term was replaced with justification term. Although the connection with arithmetic was weaker than it had been with LP, justification terms still had the role of supplying explicit justifications for epis- temically necessary statements.
One can consult Artemov (2008) and Artemov and Fitting (2012) for survey treatments, though the present book includes the material found there.Almost all of the early work on justification logics was proof-theoretically based. Realization theorems were shown constructively, making use of a sequent calculus. The existence of an algorithm to compute what are called re- alizers is important, but this proof-theoretic approach limits the field to those logics known to have sequent calculus proof systems. For a time it was hoped that various extensions of sequent and tableau calculi would be useful and, to some extent, this has been the case. The most optimistic version of this hope was expressed in Artemov (2001) quite directly, “Gabbay’s Labelled Deductive Systems, Gabbay (1994), may serve as a natural framework for LP.” Unfortunately this seems to have been too optimistic. While the formats had similarities, the goals were different, and the machinery did not interact well.
A semantics for LP and its near relatives, not based on arithmetic provability, was introduced in Mkrtychev (1997) and is discussed in Chapter 3. (A constructive version of the canonical model for LP with a completeness theorem can be found already in Artemov (1995).) Mkrtychev’s semantics did not use possible worlds and had a strong syntactic flavor. Possible worlds were added to the mix in Fitting (2005), producing something that potentially applied much more broadly than the earlier semantics. This is the subject of Chapter 4. Using this possible world semantics, a nonconstructive, semantic-based, proof of realization was given. It was now possible to avoid the use of a sequent calculus, though the algorithmic nature of realization was lost. More recently, a semantics with a very simple structure was created, Artemov’s basic semantics (Artemov, 2012). It is presented in Chapter 3. Its machinery is almost minimal for the purpose. In this book, we will use possible world semantics to establish very general realization results, but basic models will often be used when we simply want to show some formula fails to be a theorem.
Though its significance was not properly realized at the time, in 2005 the subject broadened when a justification logic counterpart of S5 was introduced in Pacuit (2005) and Rubtsova (2006a, b), with a connecting realization theorem. There was no arithmetical interpretation for this justification logic. Also there is no sequent calculus for S5 of the standard kind, so the proof given for realization was nonconstructive, using a version of the semantics from Fitting (2005). The semantics needed some modification to what is called its evidence function, and this turned out to have a greater impact than was first realized. Eventually constructive proofs connecting S5 and its justification counterpart were found. These made use of cut-free proof systems that were not exactly standard sequent calculi. Still, the door to a larger room was beginning to open.
Out of the early studies of the logics of proofs and its variants a general logical framework for reasoning about epistemic justification at large naturally emerged, and the name, Justification Logic, was introduced (cf. Arte- mov, 2008). Justification Logic is based on justification assertions, t:F, that are read t is a justification for F, with a broader understanding of the word justification going beyond just mathematical proofs. The notion of justification, which has been an essential component of epistemic studies since Plato, had been conspicuously absent in the mathematical models of knowledge within the epistemic logic framework. The Justification Logic framework fills in this void.
In Fitting (2016a) the subject expanded abruptly. Using nonconstructive semantic methods it was shown that the family of modal logics having justification counterparts is infinite. The justification phenomenon is not the relatively narrow one it first seemed to be. While that work was nonconstructive, there are now cut-free proof systems of various kinds for a broader range of modal logics than was once the case, and these have been used successfully to create realization algorithms, in Kuznets and Goetschi (2012), for instance.
It may be that the very general proof methodologies of Fitting (2015) and especially Negri (2005) and Negri and von Plato (2001) will extend the constructive range still further, perhaps even to the infinite family that nonconstructive methods are known to work for. This is active current work.Work on quantified justification logics exists, but the subject is considerably behind its propositional counterpart. An important feature of justification logics is that they can, in a very precise sense, internalize their own proofs. Doing this for axioms is generally simple. Rules of inference are more of a problem. Earlier we discussed a justification formula as a simple, representative example:
This, in effect, internalizes the axiomatic
modus ponens rule. The central problem in developing quantified justification logics was how to internalize the rule of universal generalization. It turned out that the key was the clear separation between two roles played by individual variables. On the one hand, they are formal symbols, and one can simply infer 8xφ(x) from a proof of φ(x). On the other hand, they can be thought of as open for substitution, that is, throughout a proof one can replace free occurrences of x with a term t to produce a new proof (subject to appropriate freeness of substitution conditions, of course). These two roles for variables are actually incompatible. It was the introduction of specific machinery to keep track of which role a variable occurrence had that made possible the internalization of proofs, and thus a quantified justification logic.
An axiomatic version of first-order LP was introduced in Artemov and Yavorskaya (Sidon) (2011) and a possible world semantics for it in Fitting (2011a, 2014b). A connection with formal arithmetic was established. There is a constructive proof of a Realization Theorem, connecting first-order LP with first- order S4. Unlike propositionally, no nonconstructive proof is currently known The possible world semantics includes the familiar monotonicity condition on world domains. It is likely that all this can be extended to a much broader range of quantified modal logics than just first-order S4, provided monotonicity is appropriate. A move to constant domain models, to quantified S5 in particular, has been made, and a semantics, but not yet a Realization Theorem, can be found in Fitting and Salvatore (2018). Much involving quantification is still uncharted territory.
This book will cover the whole range of topics just described. It will not do so in the historical order that was followed in this Introduction, but will make use of the clearer understanding that has emerged from study of the subject thus far. We will finish with the current state of affairs, standing on the edge of unknown lands. We hope to prepare some of you for the journey, should you choose to explore further on your own.