You may say, “I know that Abraham Lincoln was a tall man.” In turn you may be asked how you know. You would almostcertainly not reply semantically, Hintikka-style, that Abraham Lincolnwas tall in all situations compatible with your knowledge. Instead youwould more likely say, “I read about Abraham Lincoln’sheight in several books, and I have seen photographs of him next toother people. ” One certifies knowledge by providing a reason, ajustification. Hintikka semantics captures knowledge as true belief.Justification logics supply the missing third component ofPlato’s characterization of knowledge asjustified truebelief.

• 1. Why Justification Logic?
  • 1.1 Epistemic Tradition
  • 1.2 Mathematical Logic Tradition
  • 1.3 Hyperintensionality
• 2. The Basic Components of Justification Logic
  • 2.1 The Language of Justification Logic
  • 2.2 Basic Justification Logic \(\mathsf{J}_{0}\)
  • 2.3 Logical Awareness and Constant Specifications
  • 2.4 Extending Basic Justification Logic
  • 2.5 Factivity
  • 2.6 Positive Introspection
  • 2.7 Negative Introspection
  • 2.8 Geach Logics and More
• 3. Semantics
  • 3.1 Single-Agent Possible World Justification Models for \(\mathsf{J}\)
  • 3.2 Weak and Strong Completeness
  • 3.3 The Single-Agent Family
  • 3.4 Single World Justification Models
  • 3.5 Ontologically Transparent Semantics
  • 3.6 Connections with Awareness Models
• 4. Realization Theorems
• 5. Generalizations
  • 5.1 Mixing Explicit and Implicit Knowledge
  • 5.2 Multi-Agent Possible World Justification Models
• 6. Russell’s Example: Induced Factivity
• 7. Self-referentiality of justifications
• 8. Quantifiers in Justification Logic
• 9. Historical Notes
• Bibliography
• Academic Tools
• Other Internet Resources
• Related Entries

1. Why Justification Logic?

Justification logics are epistemic logics which allow knowledge andbelief modalities to be ‘unfolded’ intojustificationterms: instead of \(\Box X\) one writes \(t : X\), and reads itas “\(X\) is justified by reason \(t\)”. One may think oftraditional modal operators asimplicit modalities, andjustification terms as theirexplicit elaborations whichsupplement modal logics with finer-grained epistemic machinery. Thefamily of justification terms has structure and operations. Choice ofoperations gives rise to different justification logics. For allcommon epistemic logics their modalities can be completely unfoldedinto explicit justification form. In this respect Justification Logicreveals and uses the explicit, but hidden, content of traditionalEpistemic Modal Logic.

Justification logic originated as part of a successful project toprovide a constructive semantics for intuitionisticlogic—justification terms abstracted away all but the most basicfeatures of mathematical proofs. Proofs are justifications in perhapstheir purest form. Subsequently justification logics were introducedinto formal epistemology. This article presents the general range ofjustification logics as currently understood. It discusses theirrelationships with conventional modal logics. In addition to technicalmachinery, the article examines in what way the use of explicitjustification terms sheds light on a number of traditionalphilosophical problems. The subject as a whole is still under activedevelopment.

The roots of justification logic can be traced back to many differentsources, two of which are discussed in detail: epistemology andmathematical logic.

1.1 Epistemic Tradition

The properties of knowledge and belief have been a subject for formallogic at least since von Wright and Hintikka, (Hintikka 1962, vonWright 1951). Knowledge and belief are both treated as modalities in away that is now very familiar—Epistemic Logic. But ofPlato’s three criteria for knowledge,justified, true,belief, (Gettier 1963, Hendricks 2005), epistemic logic reallyworks with only two of them. Possible worlds and indistinguishabilitymodel belief—one believes what is so under all circumstancesthought possible. Factivity brings a trueness component intoplay—if something is not so in the actual world it cannot beknown, only believed. But there is no representation for thejustification condition. Nonetheless, the modal approach has beenremarkably successful in permitting the development of a richmathematical theory and applications, (Fagin, Halpern, Moses, andVardi 1995, van Ditmarsch, van der Hoek, and Kooi 2007). Still, it isnot the whole picture.

The modal approach to the logic of knowledge is, in a sense, builtaround the universal quantifier: \(X\) is known in a situation if\(X\) is true inall situations indistinguishable from thatone. Justifications, on the other hand, bring an existentialquantifier into the picture: \(X\) is known in a situation ifthere exists a justification for \(X\) in that situation.This universal/existential dichotomy is a familiar one tologicians—in formal logics there exists a proof for a formula\(X\) if and only if \(X\) is true in all models for the logic. Onethinks of models as inherently non-constructive, and proofs asconstructive things. One will not go far wrong in thinking ofjustifications in general as much like mathematical proofs. Indeed,the first justification logic was explicitly designed to capturemathematical proofs in arithmetic, something which will be discussedfurther in Section 1.2.

In Justification Logic, in addition to the category of formulas, thereis a second category ofjustifications. Justifications areformal terms, built up from constants and variables using variousoperation symbols. Constants represent justifications for commonlyaccepted truths—typically axioms. Variables denote unspecifiedjustifications. Different justification logics differ on whichoperations are allowed (and also in other ways too). If \(t\) is ajustification term and \(X\) is a formula, \(t : X\) is a formula, andis intended to be read:

\(t\) is a justification for X.

One operation, common to all justification logics, isapplication, written like multiplication. The idea is, if\(s\) is a justification for \(A \rightarrow B\) and \(t\) is ajustification for \(A\), then [\(s\cdot t\)] is a justification for \(B\)^[1]. That is, the validity of the following is generally assumed:

This is the explicit version of the usual distributivity of knowledgeoperators, and modal operators generally, across implication:

In fact, formula (2) is behind many of the problems oflogicalomniscience. It asserts that an agent knows everything that isimplied by the agent’s knowledge—knowledge is closed underconsequence. While knowable-in-principle, knowability, is closed underconsequence, the same cannot be said for any plausible version ofactual knowledge. The distinction between (1) and (2) can be exploitedin a discussion of the paradigmatic Red Barn Example of Goldman andKripke; here is a simplified version of the story taken from (Dretske2005).

Suppose I am driving through a neighborhood in which, unbeknownst tome, papier-mâché barns are scattered, and I see that theobject in front of me is a barn. Because I have barn-before-mepercepts, I believe that the object in front of me is a barn. Ourintuitions suggest that I fail to know barn. But now suppose that theneighborhood has no fake red barns, and I also notice that the objectin front of me is red, so I know a red barn is there. Thisjuxtaposition, being a red barn, which I know, entails there being abarn, which I do not, “is an embarrassment”.

In the first formalization of the Red Barn Example, logical derivationwill be performed in a basic modal logic in which \(\Box\) isinterpreted as the ‘belief’ modality. Then some of theoccurrences of \(\Box\) will be externally interpreted as‘knowledge’ according to the problem’s description.Let \(B\) be the sentence ‘the object in front of me is abarn’, and let \(R\) be the sentence ‘the object in frontof me is red’.

1. \(\Box B\), ‘I believe that the object in front of me is abarn’;
2. \(\Box ( B \wedge R)\), ‘I believe that the object in frontof me is a red barn’.

At the metalevel, 2 is actually knowledge, whereas by the problemdescription, 1 is not knowledge.

3. \(\Box ( B \wedge R \rightarrow B)\), a knowledge assertion of alogical axiom.

Within this formalization, it appears that epistemic closure in itsmodal form (2) is violated: line 2, \(\Box ( B \wedge R )\), and line3, \(\Box ( B \wedge R \rightarrow B)\) are cases of knowledge whereas\(\Box B\) (line 1) is not knowledge. The modal language here does notseem to help resolving this issue.

Next consider the Red Barn Example in Justification Logic where \(t :F\) is interpreted as ‘Ibelieve \(F\) forreason \(t\)’. Let \(u\) be a specific individual justificationfor belief that \(B\), and \(v\), for belief that \(B \wedge R\). Inaddition, let \(a\) be a justification for the logical truth \(B\wedge R \rightarrow B\). Then the list of assumptions is:

1. \(u : B\), ‘\(u\) is a reason to believe that the object infront of me is a barn’;
2. \(v :( B \wedge R)\), ‘\(v\) is a reason to believe thatthe object in front of me is a red barn’;
3. \(a :( B \wedge R \rightarrow B)\).

On the metalevel, the problem description states that 2 and 3 arecases of knowledge, and not merely belief, whereas 1 is belief whichis not knowledge. Here is how the formal reasoning goes:

4. \(a :( B \wedge R \rightarrow B ) \rightarrow ( v :( B \wedge R )\rightarrow [ a\cdot v ]: B)\), by principle (1);
5. \(v :( B \wedge R ) \rightarrow [ a \cdot v ]: B\), from 3 and 4,by propositional logic;
6. [\(a\cdot v ]: B\), from 2 and 5, by propositional logic.

Notice that conclusion 6 is [\(a\cdot v ]: B\), and not \(u : B\) ;epistemic closure holds. By reasoning in justification logic it wasconcluded that [\(a\cdot v ]: B\) is a case of knowledge, i.e.,‘I know \(B\) for reason \(a\cdot v\)’. The fact that \(u: B\) is not a case of knowledge does not spoil the closure principle,since the latter claims knowledge specifically for [\(a\cdot v ]: B\).Hence after observing a red façade, I indeed know \(B\), butthis knowledge has nothing to do with 1, which remains a case ofbelief rather than of knowledge. The justification logic formalizationrepresents the situation fairly.

Tracking justifications represents the structure of the Red BarnExample in a way that is not captured by traditional epistemic modaltools. The Justification Logic formalization models what seems to behappening in such a case; closure of knowledge under logicalentailment is maintained even though ‘barn’ is notperceptually known.^[2]

1.2 Mathematical Logic Tradition

According to Brouwer, truth in constructive (intuitionistic)mathematics means the existence of a proof, cf. (Troelstra and vanDalen 1988). In 1931–34, Heyting and Kolmogorov gave an informaldescription of the intended proof-based semantics for intuitionisticlogic (Kolmogorov 1932, Heyting 1934), which is now referred to as theBrouwer-Heyting-Kolmogorov (BHK) semantics. According to theBHK conditions, a formula is ‘true’ if it has a proof.Furthermore, a proof of a compound statement is connected to proofs ofits components in the following way:

• a proof of \(A \wedge B\) consists of a proof of proposition\(A\) and a proof of proposition \(B\);
• a proof of \(A \vee B\) is given by presenting either a proof of\(A\) or a proof of \(B\);
• a proof of \(A \rightarrow B\) is a construction transformingproofs of \(A\) into proofs of \(B\);
• falsehood \(\bot\) is a proposition which has no proof, \(\negA\) is shorthand for \(A \rightarrow \bot\) .

Kolmogorov explicitly suggested that the proof-like objects in hisinterpretation (“problem solutions”) came from classicalmathematics (Kolmogorov 1932). Indeed, from a foundational point ofview it does not make much sense to understand the‘proofs’ above as proofs in an intuitionistic system whichthese conditions are supposed to be specifying.

The fundamental value of the BHK semantics is that informally butunambiguously it suggests treating justifications, here mathematicalproofs, as objects with operations.

In (Gödel 1933), Gödel took the first step towardsdeveloping a rigorous proof-based semantics for intuitionism.Gödel considered the classical modal logic \(\mathsf{S4}\) to bea calculus describing properties of provability:

• Axioms and rules of classical propositional logic;
• \(\Box ( F \rightarrow G ) \rightarrow ( \Box F \rightarrow \BoxG)\);
• \(\Box F \rightarrow F\);
• \(\Box F \rightarrow \Box \Box F\);
• Rule of necessitation: if \(\vdash F\), then \(\vdash \Box F\).

Based on Brouwer’s understanding of logical truth asprovability, Gödel defined a translation tr\((F)\) of thepropositional formula \(F\) in the intuitionistic language into thelanguage of classical modal logic: tr\((F)\) is obtained by prefixingevery subformula of \(F\) with the provability modality \(\Box\).Informally speaking, when the usual procedure of determining classicaltruth of a formula is applied to tr\((F)\), it will test theprovability (not the truth) of each of \(F\)’s subformulas, inagreement with Brouwer’s ideas. From Gödel’s resultsand the McKinsey-Tarski work on topological semantics for modal logic,it follows that the translation tr\((F)\) provides a proper embeddingof the Intuitionistic Propositional Calculus, \(\mathsf{IPC}\), into\(\mathsf{S4}\), i.e., an embedding of intuitionistic logic intoclassical logic extended by the provability operator.

Still, Gödel’s original goal of defining intuitionisticlogic in terms of classical provability was not reached, since theconnection of \(\mathsf{S4}\) to the usual mathematical notion ofprovability was not established. Moreover, Gödel noted that thestraightforward idea of interpreting modality \(\Box F\) asF isprovable in a given formal system T contradictedGödel’s second incompleteness theorem. Indeed, \(\Box (\Box F \rightarrow F)\) can be derived in \(\mathsf{S4}\) by the ruleof necessitation from the axiom \(\Box F \rightarrow F\). On the otherhand, interpreting modality \(\Box\) as the predicate of formalprovability in theory \(T\) and \(F\) as contradiction, converts thisformula into a false statement that the consistency of \(T\) isinternally provable in \(T\).

The situation after (Gödel 1933) can be described by thefollowing figure where ‘\(X \hookrightarrow Y\)’ should beread as ‘\(X\) is interpreted in \(Y\)’

In a public lecture in Vienna in 1938, Gödel observed that usingthe format of explicit proofs:

can help in interpreting his provability calculus \(\mathsf{S4}\)(Gödel 1938). Unfortunately, Gödel’s work (Gödel1938) remained unpublished until 1995, by which time the Gödelianlogic of explicit proofs had already been rediscovered, andaxiomatized as the Logic of Proofs \(\mathsf{LP}\) and supplied withcompleteness theorems connecting it to both \(\mathsf{S4}\) andclassical proofs (Artemov 1995).

The Logic of Proofs \(\mathsf{LP}\) became the first in theJustification Logic family. Proof terms in \(\mathsf{LP}\) are nothingbut BHK terms understood as classical proofs. With \(\mathsf{LP}\),propositional intuitionistic logic received the desired rigorous BHKsemantics:

For further discussion of the mathematical logic tradition, see theSection 1 of the supplementary documentSome More Technical Matters.

1.3 Hyperintensionality

Thehyperintensional paradox was formulated by Cresswell in1975.

It is well known that it seems possible to have a situation in whichthere are two propositions \(p\) and \(q\) which are logicallyequivalent and yet are such that a person may believe the one but notthe other. If we regard a proposition as a set of possible worlds thentwo logically equivalent propositions will be identical, and so if‘\(x\) believes that’ is a genuine sentential functor, thesituation described in the opening sentence could not arise. I callthis the paradox of hyperintensional contexts. Hyperintensionalcontexts are simply contexts which do not respect logicalequivalence.

Starting with Cresswell himself, several ways of dealing with thishave been proposed. Generally these involve adding more layers tofamiliar possible world approaches so that some way of distinguishingbetween logically equivalent sentences is available. Cresswellsuggested that the syntactic form of sentences be taken into account.Justification Logic, in effect, takes sentence form into accountthrough its mechanism for handling justifications for sentences. ThusJustification Logic addresses some of the central issues ofhyperintensionality and, as a bonus, we automatically have anappropriate proof theory, model theory, complexity estimates and abroad variety of applications.

A good example of a hyperintensional context is the informal languageused by mathematicians conversing with each other. Typically when amathematician says he or she knows something, the understanding isthat a proof is at hand. But as the following illustrates, this kindof knowledge is essentially hyperintensional.

Fermat’s Last Theorem, FLT, is logically equivalent to \(0=0\)since both are provable, and hence denote the same proposition.However, the context of proofs distinguishes them immediately: a proof\(t\) of \(0=0\) is not necessarily a proof of FLT, and viceversa.

To formalize mathematical speech the justification logic\({\textsf{LP}}\) is a natural choice since \(t{:}X\) was designed tohave characteristics of “\(t\)is a proof of\(X\).”

The fact that propositions \(X\) and \(Y\) are equivalent in\({\textsf{LP}}\), \(X\leftrightarrow Y\), does not warrant theequivalence of the corresponding justification assertions andtypically \(t{:}X\) and \(t{:}Y\) are not equivalent,\(t{:}X\not\leftrightarrow t{:}Y\).

Going further \({\textsf{LP}}\), and Justification Logic in general,is not only sufficiently refined to distinguish justificationassertions for logically equivalent sentences, it provides a flexiblemachinery to connect justifications of equivalent sentences and henceto maintain constructive closure properties necessary for a qualitylogic system. For example, let \(X\) and \(Y\) be provably equivalent,i.e., there is a proof \(u\) of \(X\leftrightarrow Y\), and so\(u{:}(X\leftrightarrow Y)\) is provable in \({\textsf{LP}}\). Supposealso that \(v\) is a proof of \(X\), and so \(v{:}X\). It has alreadybeen mentioned that this does not mean \(v\) is a proof of\(Y\)—this is a hyperintensional context. However within theframework of Justification Logic, building on the proofs of \(X\) andof \(X\leftrightarrow Y\), we canconstruct a proof term\(f(u,v)\) which represents the proof of \(Y\) and so \(f(u,v){:}Y\)is provable. In this respect, Justification Logic goes beyondCresswell’s expectations: logically equivalent sentences displaydifferent but constructively controlled epistemic behavior.

2. The Basic Components of Justification Logic

In this section the syntax and axiomatics of the most common systemsof justification logic are presented.

2.1 The Language of Justification Logic

In order to build a formal account of justification logics one mustmake a basic structural assumption:justifications are abstractobjects which have structure and operations on them. A goodexample of justifications is provided by formal proofs, which havelong been objects of study in mathematical logic and computer science(cf. Section 1.2).

Justification Logic is a formal logical framework which incorporatesepistemic assertions \(t : F\), standing for ‘\(t\) is ajustification for \(F\)’. Justification Logic does not directlyanalyze what it means for \(t\) to justify \(F\) beyond the format \(t: F\), but rather attempts to characterize this relationaxiomatically. This is similar to the way Boolean logic treats itsconnectives, say, disjunction: it does not analyze the formula \(p\vee q\) but rather assumes certain logical axioms and truth tablesabout this formula.

There are several design decisions made. Justification Logic startswith the simplest base:classical Boolean logic, and for goodreasons. Justifications provide a sufficiently serious challenge oneven the simplest level. The paradigmatic examples by Russell,Goldman-Kripke, Gettier and others, can be handled with BooleanJustification Logic. The core of Epistemic Logic consists of modalsystems with a classical Boolean base (K, T,K4, S4, K45, KD45, S5, etc.), and each of them has beenprovided with a corresponding Justification Logic companion based onBoolean logic. Finally, factivity of justifications is not alwaysassumed. This makes it possible to capture the essence of discussionsin epistemology involving matters of belief and not knowledge.

The basic operation on justifications isapplication. Theapplication operation takes justifications \(s\) and \(t\)and produces a justification \(s\cdot t\) such that if \(s :( F\rightarrow G)\) and \(t : F\), then [\(s\cdot t ]: G\).Symbolically,

This is a basic property of justifications assumed in combinatorylogic and\(\lambda\)-calculi (Troelstra and Schwichtenberg1996), Brouwer-Heyting-Kolmogorov semantics (Troelstra and van Dalen1988), Kleene realizability (Kleene 1945), the Logic of Proofs\(\mathsf{LP}\), etc.

Another common operation on justifications is sum: it has beenintroduced to make explicit the modal logic reasoning (Artemov 1995).However, some meaningful justification logics like\({\mathsf{J}}^{-}\) (Artemov and Fitting 2019) or\({\mathsf{JNoC}}^{-}\) (Faroldi, Ghari, Lehmann, and Studer 2024) donot use the operation sum. With sum, any two justifications can safelybe combined into something with broader scope. If \(s : F\), thenwhatever evidence \(t\) may be, the combined evidence \(s\) + \(t\)remains a justification for \(F\). More properly, the operation‘+’ takes justifications \(s\) and \(t\) and produces\(s\) + \(t\), which is a justification for everything justified by\(s\) or by \(t\).

As motivation, one might think of \(s\) and \(t\) as two volumes of anencyclopedia, and \(s\) + \(t\) as the set of those two volumes.Imagine that one of the volumes, say \(s\), contains a sufficientjustification for a proposition \(F\), i.e., \(s : F\) is the case.Then the larger set \(s\) + \(t\) also contains a sufficientjustification for \(F\), [\(s\) + \(t ]: F\). In the Logic of Proofs\(\mathsf{LP}\), Section 1.2, ‘\(s + t\)’ can beinterpreted as a concatenation of proofs \(s\) and \(t\).

2.2 Basic Justification Logic \(\mathsf{J}_{0}\)

Justification terms are built from justification variables \(x , y ,z\), … and justification constants \(a , b , c\), …(with indices \(i\) = 1, 2, 3, … which are omitted whenever itis safe) by means of the operations ‘\(\cdot\) ’ and‘+’. More elaborate logics considered below also allowadditional operations on justifications. Constants denote atomicjustifications which the system does not analyze; variables denoteunspecified justifications. The Basic Logic of Justifications,\(\mathsf{J}_{0}\) is axiomatized by the following.

Classical Logic

Classical propositional axioms and the rule ModusPonens

Application Axiom

\(s :( F \rightarrow G ) \rightarrow ( t : F \rightarrow [ s\cdott ]: G)\),

Sum Axioms

\(s : F \rightarrow [ s\) + \(t ]: F ,   s : F \rightarrow [t\) + \(s ]: F\).

\(\mathsf{J}_{0}\) is the logic of general (not necessarily factive)justifications for an absolutely skeptical agent for whom no formulais provably justified, i.e., \(\mathsf{J}_{0}\) does not derive \(t :F\) for any \(t\) and \(F\). Such an agent is, however, capable ofdrawingrelative justification conclusions of the form

With this capacity \(\mathsf{J}_{0}\) is able to adequately emulatemany other Justification Logic systems in its language.

2.3 Logical Awareness and Constant Specifications

TheLogical Awareness principle states that logical axiomsare justifiedex officio: an agent accepts logical axioms asjustified (including the ones concerning justifications). As juststated, Logical Awareness may be too strong in some epistemicsituations. However Justification Logic offers the flexible mechanismof Constant Specifications to represent varying shades of LogicalAwareness.

Of course one distinguishes between an assumption and a justifiedassumption. In Justification Logic constants are used to representjustifications of assumptions in situations where they are notanalyzed any further. Suppose it is desired to postulate that an axiom\(A\) is justified for the knower. One simply postulates \(e_{1} : A\)for some evidence constant \(e_{1}\) (with index 1). If, furthermore,it is desired to postulate that this new principle \(e_{1} : A\) isalso justified, one can postulate \(e_{2} :( e_{1} : A)\) for aconstant \(e_{2}\) (with index 2). And so on. Keeping track of indicesis not necessary, but it is easy and helps in decision procedures(Kuznets 2008). The set of all assumptions of this kind for a givenlogic is called aConstant Specification. Here is the formaldefinition:

There are a number of special conditions that have been placed onconstant specifications in the literature. The following are the mostcommon.

Empty

\(CS = \varnothing\) . This corresponds to an absolutely skepticalagent. It amounts to working with the logic \(\mathsf{J}_{0}\).

Finite

\(CS\) is a finite set of formulas. This is a fully representativecase, since any specific derivation in Justification Logic willinvolve only a finite set of constants.

Axiomatically Appropriate

Each axiom, including those newly acquired through the constantspecification itself, have justifications. In the formal setting, foreach axiom \(A\) there is a constant \(e_{1}\) such that \(e_{1} : A\)is in \(CS\), and if \(e_{n} : e_{n- 1} : \ldots : e_{1} : A \in CS\),then \(e_{n+1} : e_{n} : e_{n- 1} : \ldots : e_{1} : A \in CS\), foreach \(n \ge 1\). Axiomatically appropriate constant specificationsare necessary for ensuring the Internalization property, discussed atthe end of this section.

Total

For each axiom \(A\) and any constants \(e_{1} , e_{2}, \ldots,e_{n}\), \[e_{n} : e_{n- 1} : \ldots : e_1 : A \in CS.\] The nameTCS is reserved for the totalconstant specification (for a given logic). Naturally, the totalconstant specification is axiomatically appropriate.

We may now specify:

The latter embodies the idea of unrestricted Logical Awareness for\(\mathsf{J}\). A similar rule appeared in the Logic of Proofs\(\mathsf{LP}\), and has also been anticipated in Goldman’s(Goldman 1967). Logical Awareness, as expressed by axiomaticallyappropriate Constant Specifications, is an explicit incarnation of theNecessitation Rule in Modal Logic: \(\vdash F \Rightarrow\, \vdash\Box F\), but restricted to axioms. Note that \(\mathsf{J}\) coincideswith \(\mathsf{J}_{TCS}\).

The key feature of Justification Logic systems is their ability tointernalize their own derivations as provable justification assertionswithin their languages. This property was anticipated in (Gödel1938).

See Section 2 of the supplementary documentSome More Technical Matters for examples of concrete syntactic derivations in justificationlogic.

2.4 Extending Basic Justification Logic

The basic justification logic \({\textsf{J}}_0\), and its extensionwith a constant specification \({\textsf{J}}_{CS}\), is an explicitcounterpart of the smallest normal modal logic \({\textsf{K}}\). Aproper definition of counterpart will be given in Section 4 becausethe notion ofrealization is central, but some hints arealready apparent at this stage of our presentation. For instance, itwas noted in Section 1.1 that (1), \(s{:}(A\rightarrowB)\rightarrow(t{:}A\rightarrow [s\cdot t]{:}B)\), is an explicitversion of the familiar modal principle (2), \({\square}(A\rightarrowB) \rightarrow ({\square}A\rightarrow {\square}B)\). In a similar waythe first justification logic \(\textsf{LP}\) is an explicitcounterpart of modal \({\textsf{S4}}\). It turns out that many modallogics have justification logic counterparts—indeed, generallymore than one. In what follows we begin by discussing some veryfamiliar logics, leading up to \({\textsf{S4}}\) and \(\textsf{LP}\).Up to this point much of our original motivation applies—we havejustification logics that are interpretable in arithmetic. Then wemove on to a broader family of modal logics, and the arithmeticmotivation is no longer applicable. The phenomenon of having a modallogic with a justification logic counterpart has turned out to beunexpectedly broad.

In almost all cases, one must add operations to the \(+\) and\(\cdot\) of \({\textsf{J}}_0\), along with axioms capturing theirintended behavior. The exception is factivity, discussed next, forwhich no additional operations are required, though additional axiomsare. It is always understood that constant specifications cover axiomsfrom the enlarged set. We continue using the terminology of Section2.3; for instance a constant specification is axiomaticallyappropriate if it meets the condition as stated there,for allaxioms including any that have been added to the original set.Theorem 1 from Section 2.3 continues to apply to our new justificationlogics, and with the same proof: if we have a justification logic\(\textsf{JL}_{CS}\) with an axiomatically appropriate constantspecification, Internalization holds.

2.5 Factivity

Factivity states that justifications are sufficient for an agent toconclude truth. This is embodied in the following.

Factivity Axiom \(t : F \rightarrow F\).

The Factivity Axiom has a similar motivation to the Truth Axiom ofEpistemic Logic, \(\Box F \rightarrow F\), which is widely accepted asa basic property of knowledge.

Factivity of justifications is not required in basic JustificationLogic systems, which makes them capable of representing both partialand factive justifications. The Factivity Axiom appeared in the Logicof Proofs \(\mathsf{LP}\), Section 1.2, as a principal feature ofmathematical proofs. Indeed, in this setting Factivity is clearlyvalid: if there is a mathematical proof \(t\) of \(F\), then \(F\)must be true.

The Factivity Axiom is adopted for justifications that lead toknowledge. However, factivity alone does not warrant knowledge, as hasbeen demonstrated by the Gettier examples (Gettier 1963).

Systems \(\mathsf{JT}_{CS}\) corresponding to Constant Specifications\(CS\) are defined as in Section 2.3.

2.6 Positive Introspection

One of the common principles of knowledge is identifyingknowing andknowing that one knows. In a modalsetting, this corresponds to \(\Box F \rightarrow \Box \Box F\). Thisprinciple has an adequate explicit counterpart: the fact that an agentaccepts \(t\) as sufficient evidence for \(F\) serves as sufficientevidence for \(t : F\). Often such ‘meta-evidence’ has aphysical form: a referee report certifying that a proof in a paper iscorrect; a computer verification output given a formal proof \(t\) of\(F\) as an input; a formal proof that \(t\) is a proof of \(F\), etc.APositive Introspection operation ‘!’ may beadded to the language for this purpose; one then assumes that given\(t\), the agent produces a justification !\(t\) of \(t : F\) suchthat \(t : F \rightarrow ! t :( t : F)\). Positive Introspection inthis operational form first appeared in the Logic of Proofs\(\mathsf{LP}\).

Positive Introspection Axiom: \(t : F \rightarrow ! t:( t : F)\).

We then define:

• \(\mathsf{J4} := \mathsf{J}\) + Positive Introspection;
• \(\mathsf{LP} := \mathsf{JT}\) + Positive Introspection.^[3]

Logics \(\mathsf{J4}_{0} , \mathsf{J4}_{CS} , \mathsf{LP}_{0}\), and\(\mathsf{LP}_{CS}\) are defined in the natural way (cf. Section2.3).

In the presence of the Positive Introspection Axiom, one can limit thescope of the Axiom Internalization Rule to internalizing axioms whichare not of the form \(e : A\). This is how it was done in\(\mathsf{LP}\): Axiom Internalization can then be emulated by using!!\(e :(! e :( e : A))\) instead of \(e_{3} :( e_{2} :( e_{1} : A))\),etc. The notion of Constant Specification can also be simplifiedaccordingly. Such modifications are minor and they do not affect themain theorems and applications of Justification Logic.

2.7 Negative Introspection

(Pacuit 2006, Rubtsova 2006) considered theNegativeIntrospection operation ‘?’ which verifies that agiven justification assertion is false. A possible motivation forconsidering such an operation is that the positive introspectionoperation ‘!’ may well be regarded as capable of providingconclusive verification judgments about the validity ofjustification assertions \(t : F\), so when \(t\) is not ajustification for \(F\), such a ‘!’ should conclude that\(\neg t : F\). This is normally the case for computer proofverifiers, proof checkers in formal theories, etc. This motivation is,however, nuanced: the examples of proof verifiers and proof checkerswork with both \(t\) and \(F\) as inputs, whereas the Pacuit-Rubtsovaformat ?\(t\) suggests that the only input for ‘?’ is ajustification \(t\), and the result ?\(t\) is supposed to justifypropositions \(\neg t : F\) uniformly for all \(F\)s for which \(t :F\) does not hold. Such an operation ‘?’ does not existfor formal mathematical proofs since ?\(t\) should then be a singleproof of infinitely many propositions \(\neg t : F\), which isimpossible. The operation ‘?’ was, historically, the firstexample that did not fit into the original framework in whichjustifications were abstract versions of formal proofs.

Negative Introspection Axiom \(\neg t : F \rightarrow? t :( \neg t : F)\)

We define the systems:

• \(\mathsf{J45} = \mathsf{J4}\) + Negative Introspection;
• \(\mathsf{JD45} = \mathsf{J45}\) + \(\neg t : \bot\) ;
• \(\mathsf{JT45} = \mathsf{J45}\) + Factivity

and naturally extend these definitions to \(\mathsf{J}45_{CS} ,\mathsf{JD}45_{CS}\), and \(\mathsf{JT}45_{CS}\).

2.8 Geach Logics and More

Justification logics involving \(?\) were the first examples that wentbeyond sublogics of \({\textsf{LP}}\). More recently it has beendiscovered that there is aninfinite family of modal logicsthat have justification counterparts, but for which the connectionwith arithmetic proofs is weak or missing. We discuss a single case insome detail, and sketch others.

Peter Geach proposed the axiom scheme\({\lozenge}{\square}X{\rightarrow}{\square}{\lozenge}X\). When addedto axiomatic \({\textsf{S4}}\) it yields an interesting logic known as\(\textsf{S4.2}\). Semantically, Geach’s scheme imposesconfluence on frames. That is, if two possible worlds,\(w_1\) and \(w_2\) are accessible from the same world \(w_0\), thereis a common world \(w_4\) accessible from both \(w_1\) and \(w_2\).Geach’s scheme was generalized inLemmonand Scott (1977) and a corresponding notation was introduced:\({\textsf{G}}^{k,l,m,n}\) is the scheme \({\lozenge}^k{\square}^l X{\rightarrow}{\square}^m{\lozenge}^n X\), where \(k, l, m, n\geq 0\).Semantically these schemes correspond to generalized versions ofconfluence. Some people have begun referring to the schemes asGeach schemes, and we will follow this practice. Moregenerally, we will call a modal logic aGeach logic if it canbe axiomatized by adding a finite set of Geach schemes to\({\textsf{K}}\). The original Geach scheme is\({\textsf{G}}^{1,1,1,1}\), but also note that\({\square}X{\rightarrow}X\) is \({\textsf{G}}^{0,1,0,0}\),\({\square}X{\rightarrow}{\square}{\square}X\) is\({\textsf{G}}^{0,1,2,0}\),\({\lozenge}X{\rightarrow}{\square}{\lozenge}X\) is\({\textsf{G}}^{1,0,1,1}\), and \(X{\rightarrow}{\square}{\lozenge}X\)is \({\textsf{G}}^{0,0,1,1}\), so Geach logics include the most commonof the modal logics. Geach logics constitute an infinite family.

Every Geach logic has a justification counterpart. Consider theoriginal Geach logic, with axiom scheme \(\textsf{G}^{1,1,1,1}\),\({\lozenge}{\square}X{\rightarrow}{\square}{\lozenge}X\) added to asystem for \(\textsf{S4}\)—the system \(\textsf{S4.2}\)mentioned above. We build a justification counterpart for\(\textsf{S4.2}\) axiomatically by starting with \({\textsf{LP}}\).Then we add two function symbols, \(f\) and \(g\), each two-place, andadopt the following axiom scheme, calling the resulting justificationlogic \(\textsf{J4.2}\).

There is some informal motivation for this scheme. In\({\textsf{LP}}\), because of the axiom scheme\(t{:}X{\rightarrow}X\), we have provability of \((t{:}X\landu{:}\lnot X){\rightarrow}\bot\) for any \(t\) and \(u\), and thusprovability of \(\lnot t{:}X \lor\lnot u{:}\lnot X\). In any contextone of the disjuncts must hold. The scheme above is equivalent to\(f(t,u){:}\lnot t{:}X \lor g(t,u){:}\lnot u{:}\lnot X\), whichinformally says that in any context we have means for computing ajustification for the disjunct that holds. It is a strong assumption,but not implausible at least in some circumstances.

A realization theorem connects \(\textsf{S4.2}\) and\(\textsf{J4.2}\), though it is not known if this has a constructiveproof.

As another example, consider \({\textsf{G}}^{1,2,2,1}\),\({\lozenge}{\square}{\square}X{\rightarrow}{\square}{\square}{\lozenge}X\),or equivalently \({\square}\lnot{\square}{\square}X \lor{\square}{\square}\lnot{\square}X\). It has as a correspondingjustification axiom scheme the following, where \(f\), \(g\), and\(h\) are three-place function symbols.

An intuitive interpretation for \(f\), \(g\), and \(h\) is not asclear as it is for \(\textsf{G}^{1,1,1,1}\), but formally thingsbehave quite well.

Even though the Geach family is infinite, these logics do not coverthe full range of logics with justification counterparts. Forinstance, the normal modal logic using the axiom scheme\({\square}({\square}X{\rightarrow}X)\), sometimes calledshiftreflexivity, is not a Geach logic, but it does have ajustification counterpart. Add a one-place function symbol \(k\) tothe machinery building up justification terms, and adopt thejustification axiom scheme \(k(t){:}(t{:}X{\rightarrow}X)\). ARealization Theorem holds; this is shown inFitting(2014b). We speculate that all logicsaxiomatized with Sahlquist formulas will have justificationcounterparts, but this remains a conjecture at this point.

3. Semantics

The now-standard semantics for justification logic originates in(Fitting 2005)—the models used are generally calledFittingmodels in the literature, but will be calledpossible worldjustification models here. Possible world justification modelsare an amalgam of the familiar possible world semantics for logics ofknowledge and belief, due to Hintikka and Kripke, with machineryspecific to justification terms, introduced by Mkrtychev in (Mkrtychev1997), (cf. Section 3.4).

3.1 Single-Agent Possible World Justification Models for \(\mathsf{J}\)

To be precise, a semantics for \(\mathsf{J}_{CS}\), where \(CS\) isany constant specification, is to be defined. Formally, apossibleworld justification logic model for \(\mathsf{J}_{CS}\) is astructure \(\mathcal{M} = \langle \mathcal{G} , \mathcal{R} ,\mathcal{E} , \mathcal{V}\rangle\) . Of this, \(\langle \mathcal{G} ,\mathcal{R}\rangle\) is a standard \(\mathsf{K}\) frame, where\(\mathcal{G}\) is a set of possible worlds and \(\mathcal{R}\) is abinary relation on it. \(\mathcal{V}\) is a mapping from propositionalvariables to subsets of \(\mathcal{G}\), specifying atomic truth atpossible worlds.

The new item is \(\mathcal{E}\), anevidence function, whichoriginated in (Mkrtychev 1997). This maps justification terms andformulas to sets of worlds. The intuitive idea is, if the possibleworld \(\Gamma\) is in \(\mathcal{E} ( t , X)\), then \(t\) isrelevant oradmissible evidence for \(X\) at world\(\Gamma\) . One should not think of relevant evidence as conclusive.Rather, think of it as more like evidence that can be admitted in acourt of law: this testimony, this document is something a jury shouldexamine, something that is pertinent, but something whosetruth-determining status is yet to be considered. Evidence functionsmust meet certain conditions, but these are discussed a bit later.

Given a \(\mathsf{J}_{CS}\) possible world justification model\(\mathcal{M} = \langle \mathcal{G} , \mathcal{R} , \mathcal{E} ,\mathcal{V}\rangle\) , truth of formula \(X\) at possible world\(\Gamma\) is denoted by \(\mathcal{M} , \Gamma \Vdash X\), and isrequired to meet the following standard conditions:

These just say that atomic truth is specified arbitrarily, andpropositional connectives behave truth-functionally at each world. Thekey item is the next one.

1. \(\mathcal{M} , \Gamma \Vdash ( t : X)\) if and only if \(\Gamma\in \mathcal{E} ( t , X)\) and, for every \(\Delta \in \mathcal{G}\)with \(\Gamma \mathcal{R} \Delta\) , we have that \(\mathcal{M} ,\Delta \Vdash X\).

This condition breaks into two parts. The clause requiring that\(\mathcal{M} , \Delta \Vdash X\) for every \(\Delta \in \mathcal{G}\)such that \(\Gamma \mathcal{R} \Delta\) is the familiarHintikka/Kripke condition for \(X\) to be believed, or be believable,at \(\Gamma\) . The clause requiring that \(\Gamma \in \mathcal{E} ( t, X)\) adds that \(t\) should be relevant evidence for \(X\) at\(\Gamma\) . Then, informally, \(t : X\) is true at a possible worldif \(X\) is believable at that world in the usual sense of epistemiclogic, and \(t\) is relevant evidence for \(X\) at that world.

It is important to realize that, in this semantics, one might notbelieve something for a particular reason at a world either because itis simply not believable, or because it is but the reason is notappropriate.

Some conditions must still be placed on evidence functions, and theconstant specification must also be brought into the picture. Supposeone is given \(s\) and \(t\) as justifications. One can combine thesein two different ways: simultaneously use the information from both;or use the information from just one of them, but first choose whichone. Each gives rise to a basic operation on justification terms,\(\cdot\) and +, introduced axiomatically in Section 2.2.

Suppose \(s\) is relevant evidence for an implication and \(t\) isrelevant evidence for the antecedent. Then \(s\) and \(t\) togetherprovides relevant evidence for the consequent. The following conditionon evidence functions is assumed:

With this condition added, the validity of

is secured.

If \(s\) and \(t\) are items of evidence, one might say that somethingis justified by one of \(s\) or \(t\), without bothering to specifywhich, and this will still be evidence. The following requirement isimposed on evidence functions.

Not surprisingly, both

and

now hold.

Finally, the Constant Specification \(CS\) should be taken intoaccount. Recall that constants are intended to represent reasons forbasic assumptions that are accepted outright. A model \(\mathcal{M} =\langle \mathcal{G} , \mathcal{R} , \mathcal{E} , \mathcal{V}\rangle\)meets Constant Specification \(CS\) provided: if \(c : X \inCS\) then \(\mathcal{E}\)(c,X) = \(\mathcal{G}\).

Possible World Justification Model A possible worldjustification model for \(\mathsf{J}_{CS}\) is a structure\(\mathcal{M} = \langle \mathcal{G} , \mathcal{R} , \mathcal{E} ,\mathcal{V}\rangle\) satisfying all the conditions listed above, andmeeting Constant Specification \(CS\).

Despite their similarities, possible world justification models allowa fine-grained analysis that is not possible with Kripke models. SeeSection 3 of the supplementary documentSome More Technical Matters for more details.

3.2 Weak and Strong Completeness

A formula \(X\) isvalid in a particular model for\(\mathsf{J}_{CS}\) if it is true at all possible worlds of the model.Axiomatics for \(\mathsf{J}_{CS}\) was given in Sections 2.2 and 2.3.A completeness theorem now takes the expected form.

Theorem 2: A formula \(X\) is provable in\(\mathsf{J}_{CS}\) if and only if \(X\) is valid in all\(\mathsf{J}_{CS}\) models.

The completeness theorem as just stated is sometimes referred to asweak completeness. It maybe a bit surprising that it issignificantly easier to prove than completeness for the modal logic\(\mathsf{K}\). Comments on this point follow. On the other hand it isvery general, working for all Constant Specifications.

In (Fitting 2005) a stronger version of the semantics was alsointroduced. A model \(\mathcal{M} = \langle \mathcal{G} , \mathcal{R}, \mathcal{E} , \mathcal{V}\rangle\) is calledfullyexplanatory if it meets the following condition. For each\(\Gamma \in \mathcal{G}\), if \(\mathcal{M} , \Delta \Vdash X\) forall \(\Delta \in \mathcal{G}\) such that \(\Gamma \mathcal{R} \Delta\), then \(\mathcal{M} , \Gamma \Vdash t : X\) for some justificationterm \(t\). Note that the condition, \(\mathcal{M} , \Delta \Vdash X\)for all \(\Delta \in \mathcal{G}\) such that \(\Gamma \mathcal{R}\Delta\) , is the usual condition for \(X\) being believable at\(\Gamma\) in the Hintikka/Kripke sense. So, fully explanatory reallysays that if a formula is believable at a possible world, there is ajustification for it.

Not all weak models meet the fully explanatory condition. Models thatdo are calledstrong models. If constant specification \(CS\)is rich enough so that an Internalization theorem holds, then one hascompleteness with respect to strong models meeting \(CS\). Indeed, inan appropriate sense completeness with respect to strong models isequivalent to being able to prove Internalization.

The proof of completeness with respect to strong models bears a closesimilarity to the proof of completeness using canonical models for themodal logic \(\mathsf{K}\). In turn, strong models can be used to givea semantic proof of the Realization Theorem (cf. Section 4).

3.3 The Single-Agent Family

So far a possible world semantics for one justification logic has beendiscussed, for \(\mathsf{J}\), the counterpart of \(\mathsf{K}\). Nowthings are broadened to encompass justification analogs of otherfamiliar modal logics.

Simply by adding reflexivity of the accessibility relation\(\mathcal{R}\) to the conditions for a model in Section 3.1, onegains the validity of \(t{:}X \rightarrow X\) for every \(t\) and\(X\), and obtains a semantics for \(\mathsf{JT}\), the justificationlogic analog of the modal logic \({\textsf{T}}\), the weakest logic ofknowledge. Indeed, if \({\mathcal{M},\Gamma{\Vdash}t{:}X}\) then, inparticular, \(X\) is true at every state accessible from \(\Gamma\).Since the accessibility relation is required to be reflexive,\({\mathcal{M},\Gamma{\Vdash}X}\). Weak and strong completenesstheorems are provable using the same machinery that applied in thecase of \(\textsf{J}\), and a semantic proof of a Realization Theoremconnecting \(\mathsf{JT}\) and \({\textsf{T}}\) is also available. Thesame applies to the logics discussed below.

For a justification analog of \({\textsf{K4}}\) an additional unaryoperator ‘!’ is added to the term language, see Section2.5. Recall this operator maps justifications to justifications, wherethe idea is that if \(t\) is a justification for \(X\), then \(!t\)should be a justification for \(t{:}X\). Semantically this addsconditions to a model \(\mathcal{M} = \langle\mathcal{G},\mathcal{R},\mathcal{E},\mathcal{V}\rangle\), asfollows.

First, of course, \(\mathcal{R}\) should be transitive, but notnecessarily reflexive. Second, a monotonicity condition on evidencefunctions is required:

\[\mbox{If } \Gamma \mathcal{R} \Delta \mbox{ and } \Gamma\in\mathcal{E}(t,X) \mbox{ then } \Delta \in \mathcal{E}(t,X)\] And finally, one more evidence function condition isneeded.

\[\mathcal{E}(t,X) \subseteq \mathcal{E}(!t,t{:}X)\] These conditions together entail the validity of \(t{:}X\rightarrow !t{:}t{:}X\) and produce a semantics for \(\mathsf{J4}\),a justification analog of \(\mathsf{K4}\), with a Realization Theoremconnecting them. Adding reflexivity leads to a logic that is called\({\textsf{LP}}\) for historical reasons.

We have discussed justification logics that are sublogics of\({\textsf{LP}}\), corresponding to sublogics of the modal logic\(\textsf{S4}\). The first examples that went beyond \({\textsf{LP}}\)were those discussed in Section 2.7, involving a negativeintrospection operator, ‘?’. Models for justificationlogics that include this operator add three conditions. First R issymmetric. Second, one adds a condition that has come to be known asstrong evidence: \({\mathcal{M},\Gamma{\Vdash}t{:}X}\) forall \(\Gamma\in \mathcal{E}(t, X)\). Finally, there is a condition onthe evidence function:

If this machinery is added to that for \(\mathsf{J4}\) we get thelogic \(\mathsf{J45}\), a justification counterpart of\(\mathsf{K45}\). Axiomatic soundness and completeness can be proved.In a similar way, related logics \(\mathsf{JD45}\) and\(\mathsf{JT45}\) can be formulated semantically. A RealizationTheorem taking the operator \(?\) into account was shown in (Rubtsova2006).

Moving to Geach logics as introduced in Section 2.8, a semantic modelfor \(\textsf{J4.2}\) can also be specified. Suppose \(G = \langle\mathcal{G}, \mathcal{R}, \mathcal{E}, \mathcal{V}\rangle\) is an\({\textsf{LP}}\) model. We add the following requirements. First, theframe must be convergent, as with \(\textsf{S4.2}\). Second, as with\(?\), \(\mathcal{E}\) must be astrong evidence function.And third, \(\mathcal{E}(f(t,u), \lnot t{:}X)\cup \mathcal{E}(g(t,u),\lnot u{:}\lnot X) = \mathcal{G}\). Completeness and soundness resultsfollow in the usual way.

In a similar way every modal logic axiomatized by Geach schemes inthis family has a justification counterpart, with a Fitting semanticsand a realization theorem connecting the justification counterpartwith the corresponding modal logic. In particular, this tells us thatthe justification logic family is infinite, and certainly much broaderthan it was originally thought to be. It is also the case that somemodal logics not previously considered, and not in this family, havejustification counterparts as well. Investigating the consequences ofall this is still work in progress.

3.4 Single World Justification Models

Single world justification models were developed considerably beforethe more general possible world justification models we have beendiscussing, (Mkrtychev 1997). Today they can most simply be thought ofas possible world justification models that happen to have a singleworld. The completeness proof for \(\mathsf{J}\) and the otherjustification logics mentioned above can easily be modified toestablish completeness with respect to single world justificationmodels, though of course this was not the original argument. Whatcompleteness with respect to single world justification models tellsus is that information about the possible world structure ofjustification models can be completely encoded by the admissibleevidence function, at least for the logics discussed so far. Mkrtychevused single world justification models to establish decidability of\(\mathsf{LP}\), and others have made fundamental use of them insetting complexity bounds for justification logics, as well as forshowing conservativity results for justification logics of belief(Kuznets 2000, Kuznets 2008, Milnikel 2007, Milnikel 2009). Complexityresults have further been used to address the problem of logicalomniscience (Artemov and Kuznets 2014).

3.5 Ontologically Transparent Semantics

The formal semantics for Justification Logic described above in3.1–3.4 defines truth value at a given world \(\Gamma\) the sameway it is done in Awareness Models: \(t{:}F\) holds at \(\Gamma\)iff

1. \(F\) holds at all worlds accessible from \(\Gamma\) and

2. \(t\) is admissible evidence for \(F\) according to the given evidencefunction.

In addition, there is a different kind of semantics, so-called modularsemantics, which focuses on making more transparent the ontologicalstatus of justifications. Within modular semantics propositionsreceive the usual classical truth values and justifications areinterpreted syntactically as sets of formulas. We retain a classicalinterpretation \(\ast\) of the propositional formulas \(Fm\), which,in the case of a single world, reduces to \[\ast: Fm \mapsto\ \ \{0,1\}\] i.e., eachformula gets a truth value 0 (false) or 1 (true), with the usualBoolean conditions: \({\Vdash}A\rightarrow B\) iff \(\not\Vdash A\) or\({\Vdash}B\), etc. The principal issue is how to interpretjustification terms. Forsets of formulas \(X\) and \(Y\), wedefine \[X\cdot Y = \{ F \mid G{\rightarrow}F \in X\ \mbox{and} \ G \in Y\\mbox{for some}\ G\}.\] Informally, \(X\cdot Y\) is the result of applyingModus Ponens once between all members of \(X\) and of \(Y\)(in that order). Justification termsTm are interpreted assubsets of the set of formulas: \[\ast: Tm \mapsto\ \2^{Fm}\] such that \[(s\cdot t)^\ast\supseteq s^\ast\cdot t^\ast \ \\mbox{and}\ \ \ (s+t)^\ast\supseteq s^\ast\cup t^\ast .\]These conditions correspond to the basic justification logic\(\textsf{J}\); other systems require additional closure properties of\(\ast\). Note that whereas propositions in modular models areinterpreted semantically, as truth values, justifications areinterpreted syntactically, as sets of formulas. This is a principalhyperintensional feature: a modular model may treat distinct formulas\(F\) and \(G\) as equal in the sense that \(F^\ast = G^\ast\), butstill be able to distinguish justification assertions \(t{:}F\) and\(t{:}G\), for example when \(F \in t^\ast\) but \(G\not\in t^\ast\)yielding \({\Vdash}t{:}F\) but \(\not\Vdash t{:}G\). In the generalpossible world setting, formulas are interpreted classically assubsets of the set \(W\) of possible worlds, \[\ast: Fm \mapsto\ \ 2^W ,\] andjustification terms are interpreted syntactically as sets of formulasat each world \[\ast:W\times Tm \mapsto\ \ 2^{Fm}.\] Soundness and completeness of JustificationLogic systems with respect to modular models have been demonstrated in(Artemov 2012; Kuznets and Studer2012).

3.6 Connections with Awareness Models

The logical omniscence problem is that in epistemic logics alltautologies are known and knowledge is closed under consequence, whichis unreasonable. InFagin and Halpern(1988) a simple mechanism for avoiding the problems wasintroduced. One adds to the usual Kripke model structure an awarenessfunction \(\cal A\) indicating for each world which formulas the agentis aware of at this world. Then a formula is taken to be known at apossible world \(\Gamma\) if 1) the formula is true at all worldsaccessible from \(\Gamma\) (the Kripkean condition for knowledge) and2) the agent is aware of the formula at \(\Gamma\). Awarenessfunctions can serve as a practical tool for blocking knowledge of anarbitrary set of formulas. However as logical structures, awarenessmodels can exhibit unusual behavior due to the lack of natural closureproperties. For example, the agent can know \(A\wedge B\) but be awareof neither \(A\) nor \(B\) and hence not know either.

Possible world justification logic models use a forcing definitionreminiscent of the one from the awareness models: for any givenjustification \(t\) the justification assertion \(t{:}F\) holds atworld \(\Gamma\) iff 1) \(F\) holds at all worlds \(\Delta\)accessible from \(\Gamma\) and 2) \(t\) is admissible evidence for\(F\) at \(\Gamma\), \(\Gamma\in{\cal E}(t,F)\). The principaldifference is in the operations on justifications and correspondingclosure conditions on admissible evidence function \(\cal E\) inJustification Logic models, which may hence be regarded as a dynamicversion of awareness models which necessary closure propertiesspecified. This idea has been explored inSedlár(2013) which worked with thelanguage of \(\textsf{LP}\), thinking of it as a multi-agent modallogic, and taking justification terms as agents (more properly,actions of agents). This shows that Justification Logic models absorbthe usual epistemic themes of awareness, group agency and dynamics ina natural way.

4. Realization Theorems

The natural modal epistemic counterpart of the evidence assertion \(t: F\) is \(\Box F\), readfor some x, x:\(F\). Thisobservation leads to the notion offorgetful projection whichreplaces each occurrence of \(t : F\) by \(\Box F\) and hence convertsa Justification Logic sentence \(S\) to a corresponding Modal Logicsentence \(S^{o}\). The forgetful projection extends in the naturalway from sentences to logics.

Obviously, different Justification Logic sentences may have the sameforgetful projection, hence \(S^{o}\) loses certain information thatwas contained in \(S\). However, it is easily observed that theforgetful projection always maps valid formulas of Justification Logic(e.g., axioms of \(\mathsf{J})\) to valid formulas of a correspondingEpistemic Logic \((\mathsf{K}\) in this case). The converse alsoholds: any valid formula of Epistemic Logic is the forgetfulprojection of some valid formula of Justification Logic. This followsfrom the Correspondence Theorem 3.

Theorem 3: \(\mathsf{J}^{o} = \mathsf{K}\).

This correspondence holds for other pairs of Justification andEpistemic systems, for instance \(\mathsf{J4}\) and \(\mathsf{K4}\),or \(\mathsf{LP}\) and \(\mathsf{S4}\), and many others. In suchextended form, the Correspondence Theorem shows that major modallogics such as \(\mathsf{K} , \mathsf{T} , \mathsf{K4} , \mathsf{S4} ,\mathsf{K45} , \mathsf{S5}\) and some others have exact JustificationLogic counterparts.

At the core of the Correspondence Theorem is the following RealizationTheorem.

Theorem 4: There is an algorithm which, for eachmodal formula \(F\) derivable in \(\mathsf{K}\), assigns evidenceterms to each occurrence of modality in \(F\) in such a way that theresulting formula \(F^{r}\) is derivable in \(\mathsf{J}\). Moreover,the realization assigns evidence variables to the negative occurrencesof modal operators in \(F\), thus respecting the existential readingof epistemic modality.

Known realization algorithms which recover evidence terms in modaltheorems use cut-free derivations in the corresponding modal logics.Alternatively, the Realization Theorem can be established semanticallyby Fitting’s method or its proper modifications. In principle,these semantic arguments also produce realization procedures which arebased on exhaustive search.

It would be a mistake to draw the conclusion thatanymodal logic has a reasonable Justification Logic counterpart. Forexample the logic of formal provability, \(\mathsf{GL}\), (Boolos1993) contains theLöb Principle:

which does not seem to have an epistemically acceptable explicitversion. Consider, for example, the case where \(F\) is thepropositional constant \(\bot\) forfalse. If an analogue ofTheorem 4 would cover the Löb Principle there would bejustification terms \(s\) and \(t\) such that \(x :( s : \bot\rightarrow \bot ) \rightarrow t : \bot\) . But this is intuitivelyfalse for factive justification. Indeed, \(s : \bot \rightarrow \bot\)is an instance of the Factivity Axiom. Apply Axiom Internalization toobtain \(c :( s : \bot \rightarrow \bot )\) for some constant \(c\).This choice of \(c\) makes the antecedent of \(c :( s : \bot\rightarrow \bot ) \rightarrow t : \bot\) intuitively true and theconclusion false^[4]. In particular, the Löb Principle (5) is not valid for the proofinterpretation (cf. (Goris 2007) for a full account of whichprinciples of \(\mathsf{GL}\) are realizable).

The Correspondence Theorem gives fresh insight into epistemic modallogics. Most notably, it provides a new semantics for the major modallogics. In addition to the traditional Kripke-style‘universal’ reading of \(\Box F\) asF holds in allpossible situations, there is now a rigorous‘existential’ semantics for \(\Box F\) that can be read asthere is a witness (proof, justification) for F.

Justification semantics plays a similar role in Modal Logic to thatplayed by Kleene realizability in Intuitionistic Logic. In both cases,the intended semantics isexistential: theBrouwer-Heyting-Kolmogorov interpretation of Intuitionistic Logic(Heyting 1934, Troelstra and van Dalen 1988, van Dalen 1986) andGödel’s provability reading of \(\mathsf{S4}\) (Gödel1933, Gödel 1938). In both cases there is a possible-worldsemantics ofuniversal character which is a highlypotent and dominant technical tool. It does not, however, address theexistential character of the intended semantics. It took Kleenerealizability (Kleene 1945, Troelstra 1998) to reveal thecomputational semantics of Intuitionistic Logic and the Logic ofProofs to provide exact BHK semantics of proofs for Intuitionistic andModal Logic.

In the epistemic context, Justification Logic and the CorrespondenceTheorem add a new ‘justification’ component to modallogics of knowledge and belief. Again, this new component was, infact, an old and central notion which has been widely discussed bymainstream epistemologists but which remained out of the scope ofclassical epistemic logic. The Correspondence Theorem tells us thatjustifications are compatible with Hintikka-style systems and hencecan be safely incorporated into the foundation for Epistemic ModalLogic.

See Section 4 of the supplementary documentSome More Technical Matters for more on Realization Theorems.

5. Generalizations

So far in this article only single-agent justification logics,analogous to single-agent logics of knowledge, have been considered.Justification Logic can be thought of as logic ofexplicitknowledge, related to more conventional logics ofimplicitknowledge. A number of systems beyond those discussed above have beeninvestigated in the literature, involving multiple agents, or havingboth implicit and explicit operators, or some combination ofthese.

5.1 Mixing Explicit and Implicit Knowledge

Since justification logics provide explicit justifications, whileconventional logics of knowledge provide an implicit knowledgeoperator, it is natural to consider combining the two in a singlesystem. The most common joint logic of explicit and implicit knowledgeis \(\mathsf{S4LP}\) (Artemov and Nogina 2005). The language of\(\mathsf{S4LP}\) is like that of \(\mathsf{LP}\), but with animplicit knowledge operator added, written either \(\mathbf{K}\) or\(\Box\) . The axiomatics is like that of \(\mathsf{LP}\), combinedwith that of \(\mathsf{S4}\) for the implicit operator, together witha connecting axiom, \(t : X \rightarrow \Box X\), anything that has anexplicit justification is knowable.

Semantically, possible world justification models for \(\mathsf{LP}\)need no modification, since they already have all the machinery ofHintikka/Kripke models. One models the \(\Box\) operator in the usualway, making use of just the accessibility relation, and one models thejustification terms as described in Section 3.1 using bothaccessibility and the evidence function. Since the usual condition for\(\Box X\) being true at a world is one of the two clauses of thecondition for \(t : X\) being true, this immediately yields thevalidity of \(t : X \rightarrow \Box X\), and soundness followseasily. Axiomatic completeness is also rather straightforward.

In \(\mathsf{S4LP}\) both implicit and explicit knowledge isrepresented, but in possible world justification model semantics asingle accessibility relation serves for both. This is not the onlyway of doing it. More generally, an explicit knowledge accessibilityrelation could be a proper extension of that for implicit knowledge.This represents the vision of explicit knowledge as having stricterstandards for what counts as known than that of implicit knowledge.Using different accessibility relations for explicit and implicitknowledge becomes necessary when these epistemic notions obeydifferent logical laws, e.g., \(\mathsf{S5}\) for implicit knowledgeand \(\mathsf{LP}\) for explicit. The case of multiple accessibilityrelations is commonly known in the literature as Artemov-Fittingmodels, but will be called multi-agent possible world models here.(cf. Section 5.2).

Curiously, while the logic \(\mathsf{S4LP}\) seems quite natural, aRealization Theorem has been problematic for it: no such theorem canbe proved if one insists on what are callednormalrealizations (Kuznets 2010). Realization of implicit knowledgemodalities in \(\mathsf{S4LP}\) by explicit justifications which wouldrespect the epistemic structure remains a major challenge in thisarea.

Interactions between implicit and explicit knowledge can sometimes berather delicate. As an example, consider the following mixed principleof negative introspection (again \(\Box\) should be read as animplicit epistemic operator),

From the provability perspective, it is the right form of negativeintrospection. Indeed, let \(\Box F\) be interpreted asF isprovable and \(t : F\) ast is a proof of F in a givenformal theory \(T\), e.g., in Peano Arithmetic \(\mathsf{PA}\). Then(6) states a provable principle. Indeed, if \(t\) is not a proof of\(F\) then, since this statement is decidable, it can be establishedinside \(T\), hence in \(T\) this sentence is provable. On the otherhand, the proof \(p\) of ‘\(t\) is not a proof of \(F\)’depends on both \(t\) and \(F , p = p ( t , F)\) and cannot becomputed given \(t\) only. In this respect, \(\Box\) cannot bereplaced by any specific proof term depending on \(t\) only and (6)cannot be presented in an entirely explicit justification-styleformat.

The first examples of explicit/implicit knowledge systems appeared inthe area of provability logic. In (Sidon 1997, Yavorskaya (Sidon)2001), a logic \(\mathsf{LPP}\) was introduced which combined thelogic of provability \(\mathsf{GL}\) with the logic of proofs\(\mathsf{LP}\), but to ensure that the resulting system had desirablelogical properties someadditional operations from outsidethe original languages of \(\mathsf{GL}\) and \(\mathsf{LP}\) wereadded. In (Nogina 2006, Nogina 2007) a complete logical system,\(\mathsf{GLA}\), for proofs and provability was offered, in the sumof theoriginal languages of \(\mathsf{GL}\) and\(\mathsf{LP}\). Both \(\mathsf{LPP}\) and \(\mathsf{GLA}\) enjoycompleteness relative to the class of arithmetical models, and alsorelative to the class of possible world justification models.

Another example of a provability principle that cannot be madecompletely explicit is the Löb Principle (5). For each of\(\mathsf{LPP}\) and \(\mathsf{GLA}\), it is easy to find a proof term\(l ( x)\) such that

holds. However, there is no realization which makes allthree\(\Box\) s in (5) explicit. In fact, the set of realizable provabilityprinciples is the intersection of \(\mathsf{GL}\) and \(\mathsf{S4}\)(Goris 2007).

5.2 Multi-Agent Possible World Justification Models

Inmulti-agent possible world justification models multipleaccessibility relations are employed, with connections between them,(Artemov 2006). The idea is, there are multiple agents, each with animplicit knowledge operator, and there are justification terms, whicheach agent understands. Loosely, everybody understands explicitreasons; these amount toevidence-based common knowledge.

An \(n\)-agent possible world justification model is a structure\(\langle \mathcal{G} , \mathcal{R}_{1}\), …,\(\mathcal{R}_{n}, \mathcal{R} , \mathcal{E} , \mathcal{V}\rangle\) meeting thefollowing conditions. \(\mathcal{G}\) is a set of possible worlds.Each of \(\mathcal{R}_{1}\),…,\(\mathcal{R}_{n}\) is anaccessibility relation, one for each agent. These may be assumed to bereflexive, transitive, or symmetric, as desired. They are used tomodel implicit agent knowledge for the family of agents. Theaccessibility relation \(\mathcal{R}\) meets the \(\mathsf{LP}\)conditions, reflexivity and transitivity. It is used in the modelingof explicit knowledge. \(\mathcal{E}\) is an evidence function,meeting the same conditions as those for \(\mathsf{LP}\) in Section3.3. \(\mathcal{V}\) maps propositional letters to sets of worlds, asusual. There is a special condition imposed: for each \(i\) = 1,…,\(n , \mathcal{R}_{i} \subseteq \mathcal{R}\).

If \(\mathcal{M} = \langle \mathcal{G} , \mathcal{R}_{1}\),…,\(\mathcal{R}_{n} , \mathcal{R} , \mathcal{E} ,\mathcal{V}\rangle\) is a multi-agent possible world justificationmodel a truth-at-a-world relation, \(\mathcal{M} , \Gamma \Vdash X\),is defined with most of the usual clauses. The ones of particularinterest are these:

• \(\mathcal{M} , \Gamma \Vdash K_{i}X\) if and only if, for every\(\Delta \in \mathcal{G}\) with \(\Gamma \mathcal{R}_{i} \Delta\), wehave that \(\mathcal{M} , \Delta \Vdash X\).
• \(\mathcal{M} , \Gamma \Vdash t : X\) if and only if \(\Gamma \in\mathcal{E} ( t , X)\) and, for every \(\Delta \in \mathcal{G}\) with\(\Gamma \mathcal{R} \Delta\), we have that \(\mathcal{M} , \Delta\Vdash X\).

The condition \(\mathcal{R}_{i} \subseteq \mathcal{R}\) entails thevalidity of \(t : X \rightarrow K_{i}X\), for each agent \(i\). Ifthere is only a single agent, and the accessibility relation for thatagent is reflexive and transitive, this provides another semantics for\(\mathsf{S4LP}\). Whatever the number of agents, each agent acceptsexplicit reasons as establishing knowledge.

A version of \(\mathsf{LP}\) with two agents was introduced andstudied in (Yavorskaya (Sidon) 2008), though it can be generalized toany finite number of agents. In this, each agent has its own set ofjustification operators, variables, and constants, rather than havinga single set for everybody, as above. In addition some limitedcommunication between agents may be permitted, using a new operatorthat allows one agent to verify the correctness of the otheragent’s justifications. Versions of both single world and moregeneral possible world justification semantics were created for thetwo-agent logics. This involves a straightforward extension of thenotion of an evidence function, and for possible world justificationmodels, using two accessibility relations. Realization theorems havebeen proved syntactically, though presumably a semantic proof wouldalso work.

Multi-agent models (where each agent has its own set of justificationoperators) with explicit and implicit knowledge can be used toepistemically analyze zero-knowledge proofs (Lehnherr, Ognjanovic, andStuder 2022). Zero-knowledge proofs are protocols by which one agent(the prover) can prove to another agent (the verifier) that the proverhas certain knowledge (e.g., knows a password) without conveying anyinformation beyond the mere fact of the possession of knowledge (e.g.,without revealing the password). The following formulas can be used todescribe the situation after the execution of the protocol, where theterm \(s\) justifies the verifier’s knowledge that results fromthe protocol: \[s:_V K_P F,\] meaning the protocol yields a justification\(s\) to the verifier \(V\) that the prover \(P\) knows \(F\); and\[\lnot s:_V t:_P F \text{ for any term t,}\] i.e., for no term \(t\) the protocol justifies that theverifier could know that \(t\) justifies the prover’s knowledgeof \(F\). That is, the protocol justifies that the prover knows \(F\)but it does not justify any possible evidence for that knowledge.

There has been some exploration of the role of public announcements inmulti-agent justification logics (Renne 2008, Renne 2009).

There is more on the notion of evidence-based common knowledge inSection 5 of the supplementary documentSome More Technical Matters.

Besides multi-agent epistemic logics, there are other justificationlogics that feature two types of terms. Kuznets, Marin, andStrassburger (2021) introduce an explicit version of constructivemodal logic. There, the \(\Box\)-modality is realized by proof termslike in \(\mathsf{LP}\). To realize the \(\Diamond\)-modality, asecond kind of terms is introduced, which are called witness terms. Inconstructive modal logic, the formula \(\Diamond F\) means\(F\)is consistent. In its realization \(s:F\), the witness term \(s\)represents an abstract witnessing model for the formula \(F\).

Another example is dyadic deontic logic (DDL), which can beaxiomatized by two modalities \(\Box\) and \(\bigcirc\). The formula\(\Box F\) means\(F\) is settled true, and the conditional\(\bigcirc(F/G)\) means\(F\) is obligatory given G. Faroldi,Rohani, and Studer (2023) consider an explicit version of DDL. Again,\(\Box F\) is realized by a proof term as in \(\mathsf{LP}\), whereas\(\bigcirc(F/G)\) is realized by making use of a new type of termsthat represent deontic reasons.

6. Russell’s Example: Induced Factivity

There is a technique for using Justification Logic to analyzedifferent justifications for the same fact, in particular when some ofthe justifications are factive and some are not. To demonstrate thetechnique consider a well-known example:

If a man believes that the late Prime Minister’s last name beganwith a ‘B,’ he believes what is true, since the late PrimeMinister was Sir Henry Campbell Bannerman^[5]. But if he believes that Mr. Balfour was the late Prime Minister^[6], he will still believe that the late Prime Minister’s last namebegan with a ‘B,’ yet this belief, though true, would notbe thought to constitute knowledge. (Russell 1912)

As in the Red Barn Example, discussed in Section 1.1, here one has todeal with two justifications for a true statement, one of which iscorrect and one of which is not. Let \(B\) be a sentence(propositional atom), \(w\) be a designated justification variable forthe wrong reason for \(B\) and \(r\) a designated justificationvariable for the right (hence factive) reason for \(B\). Then,Russell’s example prompts the following set of assumptions^[7]:

Somewhat counter to intuition, one can logically deduce factivity of\(w\) from \(\mathcal{R}\):

1. \(r : B\) (assumption)
2. \(r : B \rightarrow B\) (assumption)
3. \(B\) (from 1 and 2 by Modus Ponens)
4. \(B \rightarrow ( w : B \rightarrow B)\) (propositional axiom)
5. \(w : B \rightarrow B\) (from 3 and 4 by Modus Ponens)

However, this derivation utilizes the fact that \(r\) is a factivejustification for \(B\) to conclude \(w : B \rightarrow B\), whichconstitutes a case of ‘induced factivity’ for \(w : B\).The question is, how can one distinguish the ‘real’factivity of \(r : B\) from the ‘induced factivity’ of \(w: B\) ? Some sort of evidence-tracking is needed here, andJustification Logic is an appropriate tool. The natural approach is toconsider the set of assumptionswithout \(r : B\),i.e.,

and establish that factivity of \(w\), i.e., \(w : B \rightarrow B\)is not derivable from \(\mathcal{S}\). Here is a possible worldjustification model \(\mathcal{M}\) = \((\mathcal{G} , \mathcal{R} ,\mathcal{E} , \mathcal{V})\) in which \(\mathcal{S}\) holds but \(w :B \rightarrow B\) does not:

• \(\mathcal{G} = \{\mathbf{1}\}\),
• \(\mathcal{R} = \varnothing\) ,
• \(\mathcal{V} ( B)\) = \(\varnothing\) (and so not-\(\mathbf{1}\Vdash B)\),
• \(\mathcal{E} ( t , F)\) = \(\{\mathbf{1}\}\) for all pairs \((t ,F)\) except \((r , B)\),and
• \(\mathcal{E} ( r , B)\) = \(\varnothing\) .

It is easy to see that the closure conditionsApplication andSum on \(\mathcal{E}\) are fulfilled. At \(\mathbf{1} , w :B\) holds, i.e.,

since \(w\) is admissible evidence for \(B\) at \(\mathbf{1}\) andthere are no possible worlds accessible from \(\mathbf{1}\).Furthermore,

since, according to \(\mathcal{E} , r\) is not admissible evidence for\(B\) at \(\mathbf{1}\). Hence:

On the other hand,

since \(B\) does not hold at \(\mathbf{1}\).

7. Self-referentiality of justifications

The Realization algorithms sometimes produce Constant Specificationscontaining self-referential justification assertions \(c : A ( c)\),that is, assertions in which the justification (here \(c)\) occurs inthe asserted proposition (here \(A ( c))\).

Self-referentiality of justifications is a new phenomenon which is notpresent in the conventional modal language. In addition to beingintriguing epistemic objects, such self-referential assertions providea special challenge from the semantical viewpoint because of thebuilt-in vicious circle. Indeed, to evaluate \(c\) one would expectfirst to evaluate \(A\) and then assign a justification object for\(A\) to \(c\). However, this cannot be done since \(A\) contains\(c\) which is yet to be evaluated. The question of whether or notmodal logics can be realized without using self-referentialjustifications was a major open question in this area.

The principal result by Kuznets in (Brezhnev and Kuznets 2006) statesthat self-referentiality of justifications is unavoidable inrealization of \(\mathsf{S4}\) in \(\mathsf{LP}\). The current stateof things is given by the following theorem due to Kuznets:

Theorem 5: Self-referentiality can be avoided inrealizations of modal logics \(\mathsf{K}\) and \(\mathsf{D}\).Self-referentiality cannot be avoided in realizations of modal logics\(\mathsf{T} , \mathsf{K4} , \mathsf{D4}\) and \(\mathsf{S4}\).

This theorem establishes that a system of justification terms for\(\mathsf{S4}\) will necessarily be self-referential. This creates aserious, though not directly visible, constraint on provabilitysemantics. In the Gödelian context of arithmetical proofs, theproblem was coped with by a general method of assigning arithmeticalsemantics to self-referential assertions \(c : A ( c)\) stating that\(c\) is a proof of \(A ( c)\). In the Logic of Proofs \(\mathsf{LP}\)it was dealt with by a non-trivial fixed-point construction.

Self-referentiality gives an interesting perspective on Moore’sParadox. See Section 6 of the supplementary documentSome More Technical Matters for details.

The question of the self-referentiality of BHK-semantics forintuitionistic logic \(\mathsf{IPC}\) has been answered by Junhua Yu(Yu 2014). Extending Kuznets’ method, he established

Theorem 6: Each \(\mathsf{LP}\) realization of theintuitionistic law of double negation \(\neg\neg(\neg\neg p\rightarrow p)\) requires self referential constantspecifications.

8. Quantifiers in Justification Logic

While the investigation of propositional Justification Logic is farfrom complete, there has also been some work on first-order versions.Quantified versions of Modal Logic already offer complexities beyondstandard first-order logic. Quantification has an even broader fieldto play when Justification Logics are involved. Classically onequantifies over ‘objects,’ and models are equipped with adomain over which quantifiers range. Modally one might have a singledomain common to all possible worlds, or one might have separatedomains for each world. The role of the Barcan formula is well-knownhere. Both constant and varying domain options are available forJustification Logic as well. In addition there is a possibility thathas no analog for Modal Logic: one might quantify over justificationsthemselves.

Initial results concerning the possibility of Quantified JustificationLogic were notably unfavorable. The arithmetical provability semanticsfor the Logic of Proofs \(\mathsf{LP}\), naturally generalizes to afirst-order version with conventional quantifiers, and to a versionwith quantifiers over proofs. In both cases, axiomatizabilityquestions were answered negatively.

Theorem 7: The first-order logic of proofs is notrecursively enumerable (Artemov and Yavorskaya (Sidon) 2001). Thelogic of proofs with quantifiers over proofs is not recursivelyenumerable (Yavorsky 2001).

Although an arithmetic semantics is not possible, in (Fitting 2008) apossible world semantics, and an axiomatic proof theory, was given fora version of \(\mathsf{LP}\) with quantifiers ranging overjustifications. Soundness and completeness were proved. At this pointpossible world semantics separates from arithmetic semantics, whichmay or may not be a cause for alarm. It was also shown that\(\mathsf{S4}\) embeds into the quantified logic by translating \(\BoxZ\) as “there exists a justification \(x\) such that \(x :Z^{*}\),” where \(Z^{*}\) is the translation of \(Z\). Whilethis logic is somewhat complicated, it has found applications, e.g.,in (Dean and Kurokawa 2009b) it is used to analyze the Knower Paradox,though objections have been raised to this analysis in (Arlo-Costa andKishida 2009).

A First-Order Logic of Proofs, \(\textsf{FOLP}\), with quantifiersover individual variables, has been presented inArtemovand Yavorskaya (Sidon) (2011). In\(\textsf{FOLP}\) proof assertions are represented by formulas of theform \(t{:}_X A\) where \(X\) is a finite set of individual variablesthat are considered global parameters open for substitution. Alloccurrences of variables from \(X\) that are free in \(A\) are alsofree in \(t{:}_X A\). All other free variables of \(A\) are consideredlocal and hence bound in \(t{:}_X A\). For example, if \(A(x,y)\) isan atomic formula, then in \(p{:}_{\{x\}} A(x,y)\) variable \(x\) isfree and variable \(y\) is bound. Likewise, in \(p{:}_{\{x,y\}}A(x,y)\) both variables are free, and in \(p{:}_{\emptyset} A(x,y)\)neither \(x\) nor \(y\) is free.

Proofs (justifications) are represented by proof terms which do notcontain individual variables. In addition to \(\textsf{LP}\)operations there is one more series of operations on proof terms,\({\sf gen}_x(t)\), corresponding to generalization over individualvariable \(x\). The new axiom that governs this operation is \(t{:}_XA {\rightarrow}{\sf gen{:}_x(t)}_X\forall x A\), with \(x\not\in X\).The complete list of \(\textsf{FOLP}\) principles along withrealization of First-Order \(\textsf{S4}\) can be found inArtemovand Yavorskaya (Sidon) (2011). Asemantics for \(\textsf{FOLP}\) has been developed inFitting(2014a).

9. Historical Notes

The initial Justification Logic system, the Logic of Proofs\(\mathsf{LP}\), was introduced in 1995 in (Artemov 1995) (cf. also(Artemov 2001)) where such basic properties as Internalization,Realization, arithmetical completeness, were first established.\(\mathsf{LP}\) offered an intended provability semantics forGödel’s provability logic \(\mathsf{S4}\), thus providing aformalization of Brouwer-Heyting-Kolmogorov semantics forintuitionistic propositional logic. Epistemic semantics andcompleteness (Fitting 2005) were first established for\(\mathsf{LP}\). Symbolic models and decidability for \(\mathsf{LP}\)are due to Mkrtychev (Mkrtychev 1997). Complexity estimates firstappeared in (Brezhnev and Kuznets 2006, Kuznets 2000, Milnikel 2007).A comprehensive overview of all decidability and complexity resultscan be found in (Kuznets 2008). Systems \(\mathsf{J} , \mathsf{J4}\),and \(\mathsf{JT}\) were first considered in (Brezhnev 2001) underdifferent names and in a slightly different setting. \(\mathsf{JT45}\)appeared independently in (Pacuit 2006) and (Rubtsova 2006), and\(\mathsf{JD45}\) in (Pacuit 2006). The logic of uni-conclusion proofshas been found in (Krupski 1997). A more general approach to commonknowledge based on justified knowledge was offered in (Artemov 2006).Game semantics of Justification Logic and Dynamic Epistemic Logic withjustifications were studied in (Renne 2008, Renne 2009). Connectionsbetween Justification Logic and the problem of logical omnisciencewere examined in (Artemov and Kuznets 2009, Artemov and Kuznets 2014,Wang 2009). The nameJustification Logic was introduced in(Artemov 2008), in which Kripke, Russell, and Gettier examples wereformalized; this formalization has been used for the resolution ofparadoxes, verification, hidden assumption analysis, and eliminatingredundancies. In (Dean and Kurokawa 2009a), Justification Logic wasused for the analysis of Knower and Knowability paradoxes.

The first two monographs on Justification Logic were published in 2019(Artemov and Fitting 2019, Kuznets and Studer 2019).

Bibliography

• Antonakos, E., 2007. “Justified and Common Knowledge:Limited Conservativity”, in S. Artemov and A. Nerode (eds.),Logical Foundations of Computer Science, International Symposium,LFCS 2007, New York, NY, USA, June 4–7, 2007, Proceedings(Lecture Notes in Computer Science: Volume 4514), Berlin: Springer,pp. 1–11.
• Arlo-Costa, H. and K. Kishida, 2009. “Three proofs and theKnower in the Quantified Logic of Proofs”, inFormalEpistemology Workshop / FEW 2009. Proceedings, Carnegie MellonUniversity, Pittsburgh, PA, USA.
• Artemov, S., 1995. “Operational modal logic”,Technical Report MSI 95–29, Cornell University.
• –––, 2001. “Explicit provability andconstructive semantics”,The Bulletin of SymbolicLogic, 7(1): 1–36.
• –––, 2006. “Justified commonknowledge”,Theoretical Computer Science, 357(1–3): 4–22.
• –––, 2008. “The logic ofjustification”,The Review of Symbolic Logic, 1(4):477–513.
• –––, 2012. “The Ontology of Justificationsin the Logical Setting.”Studia Logica, 100(1–2):17–30.
• Artemov, S. and M. Fitting, 2019.Justification Logic:Reasoning with Reasons, New York: Cambridge UniversityPress.
• Artemov, S. and R. Kuznets, 2009. “Logical omniscience as acomputational complexity problem”, in A. Heifetz (ed.),Theoretical Aspects of Rationality and Knowledge, Proceedings ofthe Twelfth Conference (TARK 2009), ACM Publishers, pp.14–23.
• –––, 2014. “Logical omniscience asinfeasibility”,Annals of Pure and Applied Logic,165(1): 6–25.
• Artemov, S. and E. Nogina, 2005. “Introducing justificationinto epistemic logic”,Journal of Logic andComputation, 15(6): 1059–1073.
• Artemov, S. and T. Yavorskaya (Sidon), 2001. “On first-orderlogic of proofs”,Moscow Mathematical Journal, 1(4):475–490.
• –––, 2011. “First-Order Logic ofProofs.” TR–2011005, City University of New York, Ph.D.Program in Computer Science.
• Boolos, G., 1993.The Logic of Provability, Cambridge:Cambridge University Press.
• Brezhnev, V., 2001. “On the logic of proofs”, in K.Striegnitz (ed.),Proceedings of the Sixth ESSLLI Student Session,13th European Summer School in Logic, Language and Information(ESSLLI’01), pp. 35–46.
• Brezhnev, V. and R. Kuznets, 2006. “Making knowledgeexplicit: How hard it is”,Theoretical ComputerScience, 357(1–3): 23–34.
• Cubitt, R. P. and R. Sugden, 2003. “Common knowledge,salience and convention: A reconstruction of David Lewis’ gametheory”,Economics and Philosophy, 19:175–210.
• Dean, W. and H. Kurokawa, 2009a. “From the KnowabilityParadox to the existence of proofs”,Synthese, 176(2):177–225.
• –––, 2009b. “Knowledge, proof and theKnower”, in A. Heifetz (ed.),Theoretical Aspects ofRationality and Knowledge, Proceedings of the Twelfth Conference(TARK 2009), ACM Publications, pp. 81–90.
• Dretske, F., 2005. “Is Knowledge Closed Under KnownEntailment? The Case against Closure”, in M. Steup and E. Sosa(eds.),Contemporary Debates in Epistemology, Oxford:Blackwell, pp. 13–26.
• Fagin, R., and J. Y. Halpern, 1988. “Belief, Awareness, andLimited Reasoning.”Artificial Intelligence, 34:39–76.
• Fagin, R., J. Halpern, Y. Moses, and M. Vardi, 1995.ReasoningAbout Knowledge, Cambridge, MA: MIT Press.
• Faroldi, F. L. G., M. Ghari, E. Lehmann, and T. Studer, 2024.“Consistency and permission in deontic justificationlogic”,Journal of Logic and Computation, 34(4):640–664.
• Faroldi, F. L. G., A. Rohani, and T. Studer, 2023.“Conditional Obligations in Justification Logic”, in H.H.Hansen, A. Scedrov, R. de Queiroz (eds),Logic, Language,Information, and Computation, WoLLIC 2023 (Lecture Notes inComputer Science: Volume 13923), Cham: Springer, pp.178–193.
• Fitting, M., 2005. “The logic of proofs,semantically”,Annals of Pure and Applied Logic,132(1): 1–25.
• –––, 2006. “A replacement theorem for\(\mathbf{LP}\)”, Technical Report TR-2006002, Department ofComputer Science, City University of New York.
• –––, 2008. “A quantified logic ofevidence”,Annals of Pure and Applied Logic,152(1–3): 67–83.
• –––, 2009. “Realizations and\(\mathbf{LP}\)”,Annals of Pure and Applied Logic,161(3): 368–387.
• –––, 2014a. “Possible World Semantics forFirst Order Logic of Proofs.”Annals of Pure and AppliedLogic 165: 225–40.
• –––, 2014b. “Justification Logics andRealization.” TR-2014004, City University of New York, Ph.D.Program in Computer Science.
• Gettier, E., 1963. “Is Justified True BeliefKnowledge?”Analysis, 23: 121–123.
• Girard, J.-Y., P. Taylor, and Y. Lafont, 1989.Proofs andTypes (Cambridge Tracts in Computer Science: Volume 7),Cambridge: Cambridge University Press.
• Gödel, K., 1933. “Eine Interpretation desintuitionistischen Aussagenkalkuls”,Ergebnisse Math.Kolloq., 4: 39–40. English translation in: S. Fefermanet al. (eds.),Kurt Gödel Collected Works(Volume 1), Oxford and New York: Oxford University Press and ClarendonPress, 1986, pp. 301–303.
• –––, 1938. “Vortrag bei Zilsel/Lecture atZilsel’s” (*1938a), in S. Feferman, J. J. Dawson, W.Goldfarb, C. Parsons, and R. Solovay (eds.),Unpublished Essaysand Lectures (Kurt Gödel Collected Works: Volume III),Oxford: Oxford University Press, 1995, pp. 86–113.
• Goldman, A., 1967. “A causal theory of meaning”,The Journal of Philosophy, 64: 335–372.
• Goodman, N., 1970. “A theory of constructions is equivalentto arithmetic”, in J. Myhill, A. Kino, and R. Vesley (eds.),Intuitionism and Proof Theory, Amsterdam: North-Holland, pp.101–120.
• Goris, E., 2007. “Explicit proofs in formal provabilitylogic”, in S. Artemov and A. Nerode (eds.),LogicalFoundations of Computer Science, International Symposium, LFCS 2007,New York, NY, USA, June 4–7, 2007, Proceedings (LectureNotes in Computer Science: Volume 4514), Berlin: Springer, pp.241–253.
• Lehnherr, D., Z. Ognjanovic, and T. Studer, 2022. “A logicof interactive proofs”,Journal of Logic andComputation, 32(8): 1645–1658.
• Hendricks, V., 2005.Mainstream and Formal Epistemology,New York: Cambridge University Press.
• Heyting, A., 1934.Mathematische Grundlagenforschung.Intuitionismus. Beweistheorie, Berlin: Springer.
• Hintikka, J., 1962.Knowledge and Belief, Ithaca: CornellUniversity Press.
• Kleene, S., 1945. “On the interpretation of intuitionisticnumber theory”,The Journal of Symbolic Logic, 10(4):109–124.
• Kolmogorov, A., 1932. “Zur Deutung der IntuitionistischenLogik”,Mathematische Zeitschrift, 35: 58–65.English translation in V.M. Tikhomirov (ed.),Selected works ofA.N. Kolmogorov. Volume I: Mathematics and Mechanics, Dordrecht:Kluwer, 1991, pp. 151–158.
• Kreisel, G., 1962. “Foundations of intuitionisticlogic”, in E. Nagel, P. Suppes, and A. Tarski (eds.),Logic,Methodology and Philosophy of Science. Proceedings of the 1960International Congress, Stanford: Stanford University Press, pp.198–210.
• –––, 1965. “Mathematical logic”, inT. Saaty (ed.),Lectures in Modern Mathematics III, New York:Wiley and Sons, pp. 95–195.
• Krupski, V., 1997. “Operational logic of proofs withfunctionality condition on proof predicate”, in S. Adian and A.Nerode (eds.),Logical Foundations of Computer Science, 4thInternational Symposium, LFCS’97, Yaroslavl, Russia, July6–12, 1997, Proceedings (Lecture Notes in Computer Science:Volume 1234), Berlin: Springer, pp. 167–177.
• Kurokawa, H., 2009. “Tableaux and Hypersequents forJustification Logic”, in S. Artemov and A. Nerode (eds.),Logical Foundations of Computer Science, International Symposium,LFCS 2009, Deerfield Beach, FL, USA, January 3–6, 2009,Proceedings (Lecture Notes in Computer Science: Volume 5407),Berlin: Springer, pp. 295–308.
• Kuznets, R., 2000. “On the Complexity of Explicit ModalLogics”, in P. Clote and H. Schwichtenberg (eds.),ComputerScience Logic, 14th International Workshop, CSL 2000, AnnualConference of the EACSL, Fischbachau, Germany, August 21–26,2000, Proceedings (Lecture Notes in Computer Science: Volume1862), Berlin: Springer, pp. 371–383.
• –––, 2008.Complexity Issues inJustification Logic, Ph. D. dissertation, Computer ScienceDepartment, City University of New York Graduate Center.
• –––, 2010. “A note on the abnormality ofrealizations ofS4LP”, in K. Brünnler and T. Studer(eds.),Proof, Computation, Complexity PCC 2010, InternationalWorkshop, Proceedings, IAM Technical Reports IAM-10-001,Institute of Computer Science and Applied Mathematics, University ofBern.
• Kuznets, R., S. Marin, and L. Strassburger, 2021.“Justification logic for constructive modal logic”,Journal of Applied Logics, 8(8): 2313– 2332.
• Kuznets, R. and T. Studer, 2012. “Justifications, Ontology,and Conservativity”, inAdvances in Modal Logic (Volume9), Thomas Bolander, Torben Braüner, Silvio Ghilardi, andLawrence Moss (eds.), London: College Publications, 437–58.
• –––, 2019.Logics of Proofs andJustifications, London: College Publications.
• Lemmon, E. J., and Dana S. Scott, 1977.The “LemmonNotes”: An Introduction to Modal Logic (AmericanPhilosophical Quarterly Monograph 11), Oxford: Blackwell.
• McCarthy, J., M. Sato, T. Hayashi, and S. Igarishi, 1978.“On the model theory of knowledge”, Technical ReportSTAN-CS-78-667, Department of Computer Science, StanfordUniversity.
• Milnikel, R., 2007. “Derivability in certain subsystems ofthe Logic of Proofs is \(\Pi _{2}^{p}\)-complete”,Annals ofPure and Applied Logic, 145(3): 223–239.
• –––, 2009. “Conservativity for Logics ofJustified Belief”, in S. Artemov and A. Nerode (eds.),Logical Foundations of Computer Science, International Symposium,LFCS 2009, Deerfield Beach, FL, USA, January 3–6, 2009,Proceedings (Lecture Notes in Computer Science: Volume 5407),Berlin: Springer, pp. 354–364.
• Mkrtychev, A., 1997. “Models for the Logic of Proofs”,in S. Adian and A. Nerode (eds.),Logical Foundations of ComputerScience, 4th International Symposium, LFCS’97, Yaroslavl,Russia, July 6–12, 1997, Proceedings (Lecture Notes inComputer Science: Volume 1234), Berlin: Springer, pp.266–275.
• Nogina, E., 2006. “On logic of proofs andprovability”, in2005 Summer Meeting of the Association forSymbolic Logic, Logic Colloquium’05, Athens, Greece (July28–August 3, 2005),The Bulletin of Symbolic Logic,12(2): 356.
• –––, 2007. “Epistemic completeness ofGLA”, in2007 Annual Meeting of the Association forSymbolic Logic, University of Florida, Gainesville, Florida(March 10–13, 2007),The Bulletin of Symbolic Logic,13(3): 407.
• Pacuit, E., 2006. “A Note on Some Explicit ModalLogics”, Technical Report PP–2006–29, Institute forLogic, Language and Computation, University of Amsterdam.
• Plaza, J., 2007. “Logics of public communications”,Synthese, 158(2): 165–179.
• Renne, B., 2008.Dynamic Epistemic Logic withJustification, Ph. D. thesis, Computer Science Department, CUNYGraduate Center, New York, NY, USA.
• –––, 2009. “Evidence Elimination inMulti-Agent Justification Logic”, in A. Heifetz (ed.),Theoretical Aspects of Rationality and Knowledge, Proceedings ofthe Twelfth Conference (TARK 2009), ACM Publications, pp.227–236.
• Rose, G., 1953. “Propositional calculus andrealizability”,Transactions of the American MathematicalSociety, 75: 1–19.
• Rubtsova, N., 2006. “On Realization of\(\mathbf{S5}\)-modality by Evidence Terms”,Journal ofLogic and Computation, 16(5): 671–684.
• Russell, B., 1912.The Problems of Philosophy, Oxford:Oxford University Press.
• Sedlár, Igor. 2013. “Justifications, Awareness andEpistemic Dynamics”, in S. Artemov and A. Nerode (eds.),Logical Foundations of Computer Science (Lecture Notes inComputer Science: 7734), Berlin/Heidelberg: Springer,307–18.
• Sidon, T., 1997. “Provability logic with operations onproofs”, in S. Adian and A. Nerode (eds.),LogicalFoundations of Computer Science, 4th International Symposium,LFCS’97, Yaroslavl, Russia, July 6–12, 1997,Proceedings (Lecture Notes in Computer Science: Volume 1234),Berlin: Springer, pp. 342–353.
• Troelstra, A., 1998. “Realizability”, in S. Buss(ed.),Handbook of Proof Theory, Amsterdam: Elsevier, pp.407–474.
• Troelstra, A. and H. Schwichtenberg, 1996.Basic ProofTheory, Amsterdam: Cambridge University Press.
• Troelstra, A. and D. van Dalen, 1988.Constructivism inMathematics (Volumes 1, 2), Amsterdam: North–Holland.
• van Dalen, D., 1986. “Intuitionistic logic”, in D.Gabbay and F. Guenther (eds.),Handbook of PhilosophicalLogic (Volume 3), Bordrecht: Reidel, pp. 225–340.
• van Ditmarsch, H., W. van der Hoek, and B. Kooi (eds.), 2007.Dynamic Epistemic Logic (Synthese Library: Volume 337),Berlin: Springer..
• von Wright, G., 1951.An Essay in Modal Logic, Amsterdam:North-Holland.
• Wang, R.-J., 2009. “Knowledge, Time, and LogicalOmniscience”, in H. Ono, M. Kanazawa, and R. de Queiroz (eds.),Logic, Language, Information and Computation, 16th InternationalWorkshop, WoLLIC 2009, Tokyo, Japan, June 21–24, 2009,Proceedings (Lecture Notes in Artificial Intelligence: Volume5514), Berlin: Springer, pp. 394–407.
• Yavorskaya (Sidon), T., 2001. “Logic of proofs andprovability”,Annals of Pure and Applied Logic, 113(1–3): 345–372.
• –––, 2008. “Interacting Explicit EvidenceSystems”,Theory of Computing Systems, 43(2):272–293.
• Yavorsky, R., 2001. “Provability logics with quantifiers onproofs”,Annals of Pure and Applied Logic, 113(1–3): 373–387.
• Yu, J., 2014. “Self-Referentiality ofBrouwer-Heyting-Kolmogorov semantics”,Annals of Pure andApplied Logic, 165: 371–388.

Academic Tools

	How to cite this entry.
	Preview the PDF version of this entry at theFriends of the SEP Society.
	Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
	Enhanced bibliography for this entryatPhilPapers, with links to its database.

Other Internet Resources

• Justification Logic Bibliography, a complete bibliography of material on justification logic up toFebruary 2014. Maintained by Roman Kuznets.

Related Entries

belief, formal representations of |logic: modal |logic: provability

Acknowledgments

Beginning with the 2024 update, Thomas Studer has taken responsibilityfor updating and maintaining this entry.