2 What Is Not in This Book?
There are several historical works and pivotal developments in justification logic that will not be covered in the book due to natural limitations, and in this section we will mention them briefly.
We are confident that other books and surveys will do justice to these works in more detail.Apart from Godel’s lecture, Godel (1938), which remained unpublished until 1995 and thus could not influence development in this area, the first results and publications on the logic of proofs are dated 1992: a technical report, Artemov and StraBen (1992), based on work done in January of 1992 in Bern, and a conference presentation of this work at CSL’92 published in Springer Lecture Notes in Computer Science as Artemov and StraBen (1993a). In this work, the basic logic of proofs was presented: it had proof variables, and the format t is a proof of F, but without operations on proofs. However, it already had the first installment of the fixed-point arithmetical completeness construction together with an observation that, unlike provability logic, the logic of proofs cannot be limited to one standard proof predicate “from the textbook” or to any single-conclusion proof predicate.
This line was further developed in Artemov and StraBen (1993b), where the logic of single-conclusion proof predicates (without operations on proofs) was studied. This work introduced the unification axiom, which captures single- conclusioness by propositional tools. After the full-scale logic of proofs with operations had been discovered (Artemov, 1995), the logic of single-conclusion proofs with operations was axiomatized in V. Krupski (1997, 2001). A similar technique was used recently to characterize so-called sharp single-conclusion justification models in Krupski (2018).
Another research direction pursued after the papers on the basic logic of proofs was to combine provability and explicit proofs.
Such a combination, with new provability principles, was given in Artemov (1994). Despite its title, this paper did not introduce what is known now as The Logic of Proofs, but rather a fusion of the provability logic GL and the basic logic of proofs without operations, but with new arithmetical principles combining proofs and provability and an arithmetical completeness theorem. After the logic of proofs paper (Artemov, 1995), the full-scale logic of provability and proofs (with operations), LPP, was axiomatized and proved arithmetically complete in Sidon (1997) and Yavorskaya (Sidon) (2001). A leaner logic combining provability and explicit proofs, GLA, was introduced and proved arithmetically complete in Nogina (2006,2014b). Unlike LPP, the logic GLA did not use additional operations on proofs other than those inherited from LP. Later, GLA was used to find a complete classification of reflection principles in arithmetic that involve provability and explicit proofs (Nogina, 2014a).The first publication of the full-scale logic of proofs with operations, LP, which became the first justification logic in the modern sense, was Artemov (1995). This paper contains all the results needed to complete Godel’s program of characterizing intuitionistic propositional logic IPC and its BHK semantics via proofs in classical arithmetic: internalization, the realization theorem for S4 in LP, arithmetical semantics for LP, and the arithmetical completeness theorem. It took six years for the Correspondingjournal paper to appear: Artemov (2001). In Goris (2008), the completeness of LP for the semantics of proofs in Peano arithmetiC was extended to the semantiCs of proofs in Buss's bounded arithmetic
In view of applications in epistemology, this result shows that explicit knowledge in the propositional framework can be made computationally feasible. Kuznets and Studer (2016) extend the arithmetical interpretation of LP from the original finite constant specifications to a wide class of constant specifications, including some infinite ones.
Decidability of LP (with the total constant specification) was also established in Mkrtychev (1997), and this opened the door to decidability and complexity studies in justification logics using model-theoretic and other means. Among the milestones are complexity estimates in Kuznets (2000), Brezhnev and Kuznets (2006), Krupski (2006a), Milnikel (2007), Buss and Kuznets (2012), and Achilleos (2014a).
The arithmetical provability semantics for the Logic of Proofs, LP, naturally generalizes to a first-order version with conventional quantifiers and to a version with quantifiers over proofs. In both cases, axiomatizability questions were answered negatively in Artemov and Yavorskaya (2001) and Yavorsky (2001). A natural and manageable first-order version of the logic of proofs, FOLP, has been studied in Artemov and Yavorskaya (Sidon) (2011), Fitting (2014a), and Fitting and Salvatore (2018) and will be covered in Chapter 10.
Originally, the logic of proofs was formulated as a Hilbert-style axiomatic system, but this has gradually broadened. Early attempts were tableau based (which could equivalently be presented using sequent calculus machinery). Tableaus generally are analytic, meaning that everything entering into a proof is a subformula of what is being proved. This was problematic for attempts at LP tableaus because of the presence of the ■ operation, which represented an application of modus ponens, a rule that is decidedly not analytic. Successful tableau systems, though not analytic, for LP and closely related logics can be found in Fitting (2003, 2005) and Renne (2004, 2006). The analyticity problem was overcome in Ghari (2014, 2016a). Broader proof systems have been investigated: hypersequents in Kurokawa (2009, 2012), prefixed tableaus in Kurokawa (2013), and labeled deductive systems in Ghari (2017).
Indeed some of this has led to new realization results (Artemov, 1995, 2001, 2002, 2006; Artemov and Bonelli, 2007; Ghari, 2012; Kurokawa, 2012).Finding a computational reading of justification logics has been a natural research goal. There were several attempts to use the ideas of LP for building a lambda-calculus with internalization, cf. Alt and Artemov (2001), Artemov
(2002), Artemov and Bonelli (2007), Pouliasis and Primiero (2014), and others. Corresponding combinatory logic systems with internalization were studied in Artemov (2004), Krupski (2006b), and Shamkanov (2011). These and other studies can serve as a ground for further applications in typed programming languages. A version of the logic of proofs with a built-in verification predicate was considered in Protopopescu (2016a, b).
The aforementioned intuition that justification logic naturally avoids the logical omniscience problem has been formalized and studied in Artemov and Kuznets (2006, 2009, 2014). The key idea there was to view logical omniscience as a proof complexity problem: The logical omniscience defect occurs if an epistemic system assumes knowledge of propositions, which have no feasible proofs. Through this prism, standard modal logics are logically omniscient (modulo some common complexity assumptions), and justification logics are not logically omniscient. The ability of justification logic to track proof complexity via time bounds led to another formal definition of logical omniscience in Wang (2011a) with the same conclusion: Justification logic keeps logical omniscience under control.
Shortly after the first paper on the logic of proofs, it became clear that the logical tools developed are capable of evidence tracking in a general setting and as such can be useful in epistemic logic. Perhaps, the first formal work in this direction was Artemov et al. (1999), in which modal logic S5 was equivalently modified and supplied with an LP-style explicit counterpart. Applications to epistemology have benefited greatly from Fitting semantics, which connected justification logics to mainstream epistemology via possible worlds models.
In addition to applications discussed in this book, we would like to mention some other influential work. Game semantics of justification logic was studied in Renne (2008) and dynamic epistemic logic with justifications in Renne (2008) and Baltag et al. (2014). In Sedlar (2013), Fitting semantics for justification models was elaborated to a special case of the models of general awareness. Multiagentjustification logic and common knowledge has been studied in Artemov (2006), Antonakos (2007), Yavorskaya (Sidon) (2008), Bucheli et al. (2010, 2011), Bucheli (2012), Antonakos (2013), and Achilleos (2014b, 2015a, b). In Dean and Kurokawa (2010), justification logic was used for the analysis of Knower and Knowability paradoxes. A fast-growing and promising area is probabilistic justification logic, cf. Milnikel (2014), Artemov (2016b), Kokkinis et al. (2016), Ghari (2016b), and Lurie (2018).We are deeply indebted to all contributors to the exciting justification logic project, without whom there would not be this book.
Very special thanks to our devoted readers for their sharp eyes and their useful comments: Vladimir Krupski, Vincent Alexis Peluce, and Tatiana Yavorskaya (Sidon).
I think there is no sense in forming an opinion when there is no evidence to form it on. If you build a person without any bones in him he may look fair enough to the eye, but he will be limber and cannot stand up; and I consider that evidence is the bones of an opinion.[2]