This is a file in the archives of the Stanford Encyclopedia of Philosophy.

Author & Citation Info | Friends PDF Preview | InPho Search | PhilPapers Bibliography

Justification Logic

You may say, “I know that Abraham Lincoln was a tall man. ” In turn you may be asked how you know. You would almost certainly not reply semantically, Hintikka-style, that Abraham Lincoln was tall in all situations compatible with your knowledge. Instead you would more likely say, “I read about Abraham Lincoln's height in several books, and I have seen photographs of him next to other people. ” One certifies knowledge by providing a reason, a justification. Hintikka semantics captures knowledge as true belief. Justification logics supply the missing third component of Plato's characterization of knowledge as justified true belief.

• 1. Why Justification Logic?
  • 1.1 Epistemic Tradition
  • 1.2 Mathematical Logic Tradition
• 2. The Basic Components of Justification Logic
  • 2.1 The Language of Justification Logic
  • 2.2 Basic Justification Logic J₀
  • 2.3 Logical Awareness and Constant Specifications
  • 2.4 Factivity
  • 2.5 Positive Introspection
  • 2.6 Negative Introspection
• 3. Semantics
  • 3.1 Single-Agent Possible World Justification Models for J
  • 3.2 Weak and Strong Completeness
  • 3.3 The Single-Agent Family
  • 3.4 Single World Justification 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
• Related Entries
• Other Internet Resources

---

1. Why Justification Logic?

Justification logics are epistemic logics which allow knowledge and belief modalities to be ‘unfolded’ into justification terms: instead of □X one writes t:X, and reads it as “X is justified by reason t”. One may think of traditional modal operators as implicit modalities, and justification terms as their explicit elaborations which supplement modal logics with finer-grained epistemic machinery. The family of justification terms has structure and operations. Choice of operations gives rise to different justification logics. For all common epistemic logics their modalities can be completely unfolded into explicit justification form. In this respect Justification Logic reveals and uses the explicit, but hidden, content of traditional Epistemic Modal Logic.

Justification logic originated as part of a successful project to provide a constructive semantics for intuitionistic logic—justification terms abstracted away all but the most basic features of mathematical proofs. Proofs are justifications in perhaps their purest form. Subsequently justification logics were introduced into formal epistemology. This article presents the general range of justification logics as currently understood. It discusses their relationships with conventional modal logics. In addition to technical machinery, the article examines in what way the use of explicit justification terms sheds light on a number of traditional philosophical problems. The subject as a whole is still under active development. What is presented here is a snapshot of it at the time of writing.

The roots of justification logic can be traced back to many different sources, two of which are discussed in detail: epistemology and mathematical logic.

1.1 Epistemic Tradition

The properties of knowledge and belief have been a subject for formal logic at least since von Wright and Hintikka, (Hintikka 1962, von Wright 1951). Knowledge and belief are both treated as modalities in a way that is now very familiar—Epistemic Logic. But of Plato's three criteria for knowledge, justified, true, belief, (Gettier 1963, Hendricks 2005), epistemic logic really works with only two of them. Possible worlds and indistinguishability model belief—one believes what is so under all circumstances thought possible. Factivity brings a trueness component into play—if something is not so in the actual world it cannot be known, only believed. But there is no representation for the justification condition. Nonetheless, the modal approach has been remarkably successful in permitting the development of a rich mathematical theory and applications, (Fagin, Halpern, Moses, and Vardi 1995, van Ditmarsch, van der Hoek, and Kooi 2007). Still, it is not the whole picture.

The modal approach to the logic of knowledge is, in a sense, built around the universal quantifier: X is known in a situation if X is true in all situations indistinguishable from that one. Justifications, on the other hand, bring an existential quantifier into the picture: X is known in a situation if there exists a justification for X in that situation. This universal/existential dichotomy is a familiar one to logicians—in formal logics there exists a proof for a formula X if and only if X is true in all models for the logic. One thinks of models as inherently non-constructive, and proofs as constructive things. One will not go far wrong in thinking of justifications in general as much like mathematical proofs. Indeed, the first justification logic was explicitly designed to capture mathematical proofs in arithmetic, something which will be discussed further in Section 1.2.

In Justification Logic, in addition to the category of formulas, there is a second category of justifications. Justifications are formal terms, built up from constants and variables using various operation symbols. Constants represent justifications for commonly accepted truths—typically axioms. Variables denote unspecified justifications. Different justification logics differ on which operations are allowed (and also in other ways too). If t is a justification term and X is a formula, t:X is a formula, and is intended to be read:

t is a justification for X.

One operation, common to all justification logics, is application, written like multiplication. The idea is, if s is a justification for A → B and t is a justification for A, then [s⋅t] is a justification for B^[1]. That is, the validity of the following is generally assumed:

(1)	s:(A → B) → (t:A → [s⋅t]:B).

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

(2)	□(A → B) → (□A → □B).

In fact, formula (2) is behind many of the problems of logical omniscience. It asserts that an agent knows everything that is implied by the agent's knowledge—knowledge is closed under consequence. While knowable-in-principle, knowability, is closed under consequence, the same cannot be said for any plausible version of actual knowledge. The distinction between (1) and (2) can be exploited in a discussion of the paradigmatic Red Barn Example of Goldman and Kripke; here is a simplified version of the story taken from (Dretske 2005).

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

In the first formalization of the Red Barn Example, logical derivation will be performed in a basic modal logic in which □ is interpreted as the ‘belief’ modality. Then some of the occurrences of □ will be externally interpreted as ‘knowledge’ according to the problem's description. Let B be the sentence ‘the object in front of me is a barn’, and let R be the sentence ‘the object in front of me is red’.

1. □B, ‘I believe that the object in front of me is a barn’;
2. □(B ∧ R), ‘I believe that the object in front of me is a red barn’.

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

3. □(B ∧ R → B), a knowledge assertion of a logical axiom.

Within this formalization, it appears that epistemic closure in its modal form (2) is violated:line 2, □(B ∧ R ), and line 3, □(B ∧ R → B) are cases of knowledge whereas □B (line 1) is not knowledge. The modal language here does not seem to help resolving this issue.

Next consider the Red Barn Example in Justification Logic where t:F is interpreted as ‘I believe F for reason t’. Let u be a specific individual justification for belief that B, and v, for belief that B ∧ R. In addition, let a be a justification for the logical truth B ∧ R → B. Then the list of assumptions is:

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

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

4. a:(B ∧ R → B) → (v:(B ∧ R) → [a⋅v]:B), by principle (1);
5. v:(B ∧ R) → [a ⋅v]:B, from 3 and 4, by propositional logic;
6. [a⋅v]:B, from 2 and 5, by propositional logic.

Notice that conclusion 6 is [a⋅v]:B, and not u:B ; epistemic closure holds. By reasoning in justification logic it was concluded that [a⋅v]:B is a case of knowledge, i.e., ‘I know B for reason a⋅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⋅v]:B. Hence after observing a red façade, I indeed know B, but this knowledge has nothing to do with 1, which remains a case of belief rather than of knowledge. The justification logic formalization represents the situation fairly.

Tracking justifications represents the structure of the Red Barn Example in a way that is not captured by traditional epistemic modal tools. The Justification Logic formalization models what seems to be happening in such a case; closure of knowledge under logical entailment is maintained even though ‘barn’ is not perceptually known.^[2]

1.2 Mathematical Logic Tradition

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

• a proof of A ∧ B consists of a proof of proposition A and a proof of proposition B;
• a proof of A ∨ B is given by presenting either a proof of A or a proof of B;
• a proof of A → B is a construction transforming proofs of A into proofs of B;
• falsehood ⊥ is a proposition which has no proof, ¬A is shorthand for A → ⊥.

Kolmogorov explicitly suggested that the proof-like objects in his interpretation (“problem solutions”) came from classical mathematics (Kolmogorov 1932). Indeed, from a foundational point of view it does not make much sense to understand the ‘proofs’ above as proofs in an intuitionistic system which these conditions are supposed to be specifying.

The fundamental value of the BHK semantics is that informally but unambiguously it suggests treating justifications, here mathematical proofs, as objects with operations.

In (Gödel 1933), Gödel took the first step towards developing a rigorous proof-based semantics for intuitionism. Gödel considered the classical modal logic S4 to be a calculus describing properties of provability:

• Axioms and rules of classical propositional logic;
• □(F → G) → (□F → □G);
• □F → F;
• □F → □□F;
• Rule of necessitation: if ⊢F, then ⊢□F.

Based on Brouwer's understanding of logical truth as provability, Gödel defined a translation tr(F) of the propositional formula F in the intuitionistic language into the language of classical modal logic: tr(F) is obtained by prefixing every subformula of F with the provability modality □. Informally speaking, when the usual procedure of determining classical truth of a formula is applied to tr(F), it will test the provability (not the truth) of each of F's subformulas, in agreement with Brouwer's ideas. From Gödel's results and the McKinsey-Tarski work on topological semantics for modal logic, it follows that the translation tr(F) provides a proper embedding of the Intuitionistic Propositional Calculus, IPC, into S4, i.e., an embedding of intuitionistic logic into classical logic extended by the provability operator.

(3)	If IPC proves F, then S4 proves tr(F).

Still, Gödel's original goal of defining intuitionistic logic in terms of classical provability was not reached, since the connection of S4 to the usual mathematical notion of provability was not established. Moreover, Gödel noted that the straightforward idea of interpreting modality □F as F is provable in a given formal system T contradicted Gödel's second incompleteness theorem. Indeed, □(□F → F) can be derived in S4 by the rule of necessitation from the axiom □F → F. On the other hand, interpreting modality □ as the predicate of formal provability in theory T and F as contradiction, converts this formula into a false statement that the consistency of T is internally provable in T.

The situation after (Gödel 1933) can be described by the following figure where ‘X ↪Y’ should be read as ‘X is interpreted in Y’

IPC ↪ S4 ↪ ? ↪ CLASSICAL PROOFS

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

(4)	t is a proof of F

can help in interpreting his provability calculus S4 (Gödel 1938). Unfortunately, Gödel's work (Gödel 1938) remained unpublished until 1995, by which time the Gödelian logic of explicit proofs had already been rediscovered, and axiomatized as the Logic of Proofs LP and supplied with completeness theorems connecting it to both S4 and classical proofs (Artemov 1995).

The Logic of Proofs LP became the first in the Justification Logic family. Proof terms in LP are nothing but BHK terms understood as classical proofs. With LP, propositional intuitionistic logic received the desired rigorous BHK semantics:

IPC ↪ S4 ↪ LP ↪ CLASSICAL PROOFS

For further discussion of the mathematical logic tradition, see the Section 1 of the supplementary document Some More Technical Matters.

2. The Basic Components of Justification Logic

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

2.1 The Language of Justification Logic

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

Justification Logic is a formal logical framework which incorporates epistemic assertions t:F, standing for ‘t is a justification for F’. Justification Logic does not directly analyze what it means for t to justify F beyond the format t:F, but rather attempts to characterize this relation axiomatically. This is similar to the way Boolean logic treats its connectives, say, disjunction: it does not analyze the formula p ∨ q but rather assumes certain logical axioms and truth tables about this formula.

There are several design decisions made. Justification Logic starts with the simplest base: classical Boolean logic, and for good reasons. Justifications provide a sufficiently serious challenge on even the simplest level. The paradigmatic examples by Russell, Goldman-Kripke, Gettier and others, can be handled with Boolean Justification Logic. The core of Epistemic Logic consists of modal systems with a classical Boolean base (K, T, K4, S4, K45, KD45, S5, etc.), and each of them has been provided with a corresponding Justification Logic companion based on Boolean logic. Finally, factivity of justifications is not always assumed. This makes it possible to capture the essence of discussions in epistemology involving matters of belief and not knowledge.

The basic operation on justifications are application and sum. The application operation takes justifications s and t and produces a justification s⋅t such that if s:(F → G) and t:F, then [s⋅t]:G. Symbolically,

s:(F → G) → (t:F → [s⋅t]:G)

This is a basic property of justifications assumed in combinatory logic and λ -calculi (Troelstra and Schwichtenberg 1996), Brouwer-Heyting-Kolmogorov semantics (Troelstra and van Dalen 1988), Kleene realizability (Kleene 1945), the Logic of Proofs LP, etc.

Any two justifications can safely be combined into something with broader scope. This is done using the operation sum ‘+’. If s:F, then whatever 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.

s:F → [s + t]:F and t:F → [s + t]:F

As motivation, one might think of s and t as two volumes of an encyclopedia, and s + t as the set of those two volumes. Imagine that one of the volumes, say s, contains a sufficient justification for a proposition F, i.e., s:F is the case. Then the larger set s + t also contains a sufficient justification for F, [s + t]:F. In the Logic of Proofs LP, Section 1.2, ‘s + t’ can be interpreted as a concatenation of proofs s and t.

2.2 Basic Justification Logic J₀

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 it is safe) by means of the operations ‘⋅’ and ‘+’. More elaborate logics considered below also allow additional operations on justifications. Constants denote atomic justifications which the system does not analyze; variables denote unspecified justifications. The Basic Logic of Justifications, J₀ is axiomatized by the following.

Classical Logic

Classical propositional axioms and the rule Modus Ponens

Application Axiom

s:(F → G) → (t:F → [s⋅t]:G),

Sum Axioms

s:F → [s + t]:F, s:F → [t + s]:F.

J₀ is the logic of general (not necessarily factive) justifications for an absolutely skeptical agent for whom no formula is provably justified, i.e., J₀ does not derive t:F for any t and F. Such an agent is, however, capable of drawing relative justification conclusions of the form

If x:A, y:B, …, z:C hold, then t:F.

With this capacity J₀ is able to adequately emulate other Justification Logic systems in its language.

2.3 Logical Awareness and Constant Specifications

The Logical Awareness principle states that logical axioms are justified ex officio: an agent accepts logical axioms as justified (including the ones concerning justifications). As just stated, Logical Awareness may be too strong in some epistemic situations. However Justification Logic offers the flexible mechanism of Constant Specifications to represent varying shades of Logical Awareness.

Of course one distinguishes between an assumption and a justified assumption. In Justification Logic constants are used to represent justifications of assumptions in situations where they are not analyzed any further. Suppose it is desired to postulate that an axiom A is justified for the knower. One simply postulates e₁:A for some evidence constant e₁ (with index 1). If, furthermore, it is desired to postulate that this new principle e₁:A is also justified, one can postulate e₂:(e₁:A) for a constant e₂ (with index 2). And so on. Keeping track of indices is not necessary, but it is easy and helps in decision procedures (Kuznets 2008). The set of all assumptions of this kind for a given logic is called a Constant Specification. Here is the formal definition:

A Constant Specification CS for a given justification logic L is a set of formulas of the form

e_n:e_n−1:…:e₁:A (n ≥ 1),

where A is an axiom of L, and e₁, e₂, …, e_n are similar constants with indices 1, 2, …, n. It is assumed that CS contains all intermediate specifications, i.e., whenever e_n:e_n−1:…:e₁:A is in CS, then e_n−1:…:e₁:A is in CS too.

There are a number of special conditions that have been placed on constant specifications in the literature. The following are the most common.

Empty

CS = ∅. This corresponds to an absolutely skeptical agent. It amounts to working with the logic J₀.

Finite

CS is a finite set of formulas. This is a fully representative case, since any specific derivation in Justification Logic will involve only a finite set of constants.

Axiomatically Appropriate

Each axiom, including those newly acquired through the constant specification itself, have justifications. In the formal setting, for each axiom A there is a constant e₁ such that e₁:A is in CS, and if e_n:e_n−1: …: e₁: A ∈ CS, then e_{n +1}: e_n: e_n−1: …: e₁: A ∈ CS, for each n ≥ 1. Axiomatically appropriate constant specifications are necessary for ensuring the Internalization property, discussed at the end of this section.

Total

For each axiom A and any constants e₁, e₂, … e_n,

e_n:e_n−1:…:e₁:A ∈ CS.

The name TCS is reserved for the total constant specification (for a given logic). Naturally, the total constant specification is axiomatically appropriate.

We may now specify:

Logic of Justifications with given Constant Specification:
Let CS be a constant specification. J_CS is the logic J₀ + CS ; the axioms are those of J₀ together with the members of CS, and the only rule of inference is Modus Ponens. Note that J₀ is J_∅.

Logic of Justifications:
J is the logic J₀ + Axiom Internalization Rule. The new rule states:

For each axiom A and any constants e₁, e₂, …, e_n infer e_n:e_n−1:…:e₁: A.

The latter embodies the idea of unrestricted Logical Awareness for J. A similar rule appeared in the Logic of Proofs LP, and has also been anticipated in Goldman's (Goldman 1967). Logical Awareness, as expressed by axiomatically appropriate Constant Specifications, is an explicit incarnation of the Necessitation Rule in Modal Logic: ⊢ F ⇒ ⊢□F, but restricted to axioms. Note that J coincides with J_TCS.

The key feature of Justification Logic systems is their ability to internalize their own derivations as provable justification assertions within their languages. This property was anticipated in (Gödel 1938).

Theorem 1: For each axiomatically appropriate constant specification CS, J_CS enjoys Internalization:

If ⊢ F, then ⊢ p:F for some justification term p.

Proof. Induction on derivation length. Suppose ⊢ F. If F is a member of J₀, or a member of CS, there is a constant e_n (where n might be 1) such that e_n:F is in CS, since CS is axiomatically appropriate. Then e_n:F is derivable. If F is obtained by Modus Ponens from X → F and X, then, by the Induction Hypothesis, ⊢ s:(X → F) and ⊢ t:X for some s, t. Using the Application Axiom, ⊢ [s⋅t]:F.

See Section 2 of the supplementary document Some More Technical Matters for examples of concrete syntactic derivations in justification logic.

2.4 Factivity

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

Factivity Axiom t:F → F.

The Factivity Axiom has a similar motivation to the Truth Axiom of Epistemic Logic, □F → F, which is widely accepted as a basic property of knowledge.

Unlike the principles of Application and Sum, factivity of justifications is not required in basic Justification Logic systems, which makes them capable of representing both partial and factive justifications. The Factivity Axiom appeared in the Logic of Proofs LP, Section 1.2, as a principal feature of mathematical proofs. Indeed, in this setting Factivity is clearly valid: if there is a mathematical proof t of F, then F must be true.

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

Logic of Factive Justifications:

• JT₀ = J₀ + Factivity;
• JT = J + Factivity.

Systems JT_CS corresponding to Constant Specifications CS are defined as in Section 2.3.

2.5 Positive Introspection

One of the common principles of knowledge is identifying knowing and knowing that one knows. In a modal setting, this corresponds to □F → □□F. This principle has an adequate explicit counterpart: the fact that an agent accepts t as sufficient evidence for F serves as sufficient evidence for t:F. Often such ‘meta-evidence’ has a physical form: a referee report certifying that a proof in a paper is correct; 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. A Positive Introspection operation ‘!’ may be added to the language for this purpose; one then assumes that given t, the agent produces a justification !t of t:F such that t:F → !t:(t:F). Positive Introspection in this operational form first appeared in the Logic of Proofs LP.

Positive Introspection Axiom: t:F → !t:(t:F).

We then define:

• J4 := J + Positive Introspection;
• LP := JT + Positive Introspection.^[3]

Logics J4₀, J4_CS, LP₀, and LP_CS are defined in the natural way (cf. Section 2.3). The direct analogue of Theorem 1 holds for J4_CS and LP_CS as well.

In the presence of the Positive Introspection Axiom, one can limit the scope of the Axiom Internalization Rule to internalizing axioms which are not of the form e:A. This is how it was done in LP: Axiom Internalization can then be emulated by using !!e:(!e:(e:A)) instead of e₃:(e₂:(e₁:A)), etc. The notion of Constant Specification can also be simplified accordingly. Such modifications are minor and they do not affect the main theorems and applications of Justification Logic.

2.6 Negative Introspection

(Pacuit 2006, Rubtsova 2006) considered the Negative Introspection operation ‘?’ which verifies that a given justification assertion is false. A possible motivation for considering such an operation is that the positive introspection operation ‘!’ may well be regarded as capable of providing conclusive verification judgments about the validity of justification assertions t:F, so when t is not a justification for F, such a ‘!’ should conclude that ¬t:F. This is normally the case for computer proof verifiers, proof checkers in formal theories, etc. This motivation is, however, nuanced: the examples of proof verifiers and proof checkers work with both t and F as inputs, whereas the Pacuit-Rubtsova format ?t suggests that the only input for ‘?’ is a justification t, and the result ?t is supposed to justify propositions ¬t:F uniformly for all Fs for which t:F does not hold. Such an operation ‘?’ does not exist for formal mathematical proofs since ?t should then be a single proof of infinitely many propositions ¬t:F, which is impossible.

Negative Introspection Axiom ¬t:F → ?t:(¬t:F)

We define the systems:

• J45 = J4 + Negative Introspection;
• JD45 = J45 + ¬t:⊥;
• JT45 = J45 + Factivity

and naturally extend these definitions to J45_CS, JD45_CS, and JT45_CS. The direct analogue of Theorem 1 holds for J45_CS, JD45_CS, and JT45_CS.

3. Semantics

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

3.1 Single-Agent Possible World Justification Models for J

To be precise, a semantics for J_CS, where CS is any constant specification, is to be defined. Formally, a possible world justification logic model for J_CS is a structure M = ⟨G,R,E,V⟩. Of this, ⟨G,R⟩ is a standard K frame, where G is a set of possible worlds and R is a binary relation on it. V is a mapping from propositional variables to subsets of G, specifying atomic truth at possible worlds.

The new item is E, an evidence function, which originated in (Mkrtychev 1997). This maps justification terms and formulas to sets of worlds. The intuitive idea is, if the possible world Γ is in E(t,X), then t is relevant or admissible evidence for X at world Γ. One should not think of relevant evidence as conclusive. Rather, think of it as more like evidence that can be admitted in a court of law: this testimony, this document is something a jury should examine, something that is pertinent, but something whose truth-determining status is yet to be considered. Evidence functions must meet certain conditions, but these are discussed a bit later.

Given a J_CS possible world justification model M = ⟨G,R,E,V⟩, truth of formula X at possible world Γ is denoted by M, Γ ⊩ X, and is required to meet the following standard conditions:

For each Γ ∈ G:

1. M, Γ ⊩ P iff Γ ∈ V(P) for P a propositional letter;
2. it is not the case that M, Γ ⊩ ⊥;
3. M, Γ ⊩ X → Y iff it is not the case that M, Γ ⊩ X or M, Γ ⊩ Y.

These just say that atomic truth is specified arbitrarily, and propositional connectives behave truth-functionally at each world. The key item is the next one.

1. M, Γ ⊩ (t:X) if and only if Γ ∈ E(t,X) and, for every Δ ∈ G with Γ R Δ, we have that M, Δ ⊩ X.

This condition breaks into two parts. The clause requiring that M, Δ ⊩ X for every Δ ∈ G such that Γ R Δ is the familiar Hintikka/Kripke condition for X to be believed, or be believable, at Γ. The clause requiring that Γ ∈ E(t,X) adds that t should be relevant evidence for X at Γ. Then, informally, t:X is true at a possible world if X is believable at that world in the usual sense of epistemic logic, and t is relevant evidence for X at that world.

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

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

Suppose s is relevant evidence for an implication and t is relevant evidence for the antecedent. Then s and t together provides relevant evidence for the consequent. The following condition on evidence functions is assumed:

E(s,X → Y) ∩E(t,X) ⊆ E(s⋅t,Y)

With this condition added, the validity of

s:(X → Y) → (t:X → [s⋅t]:Y)

is secured.

If s and t are items of evidence, one might say that something is justified by one of s or t, without bothering to specify which, and this will still be evidence. The following requirement is imposed on evidence functions.

E(s,X) ∪ E(t,X) ⊆ E(s + t,X)

Not surprisingly, both

s:X → [s + t]:X

and

t:X → [s + t]:X

now hold.

Finally, the Constant Specification CS should be taken into account. Recall that constants are intended to represent reasons for basic assumptions that are accepted outright. A model M = ⟨G,R,E,V⟩ meets Constant Specification CS provided: if c:X ∈ CS then E(c,X) = G.

Possible World Justification Model A possible world justification model for J_CS is a structure M = ⟨G,R,E,V⟩ satisfying all the conditions listed above, and meeting Constant Specification CS.

Despite their similarities, possible world justification models allow a fine-grained analysis that is not possible with Kripke models. See Section 3 of the supplementary document Some More Technical Matters for more details.

3.2 Weak and Strong Completeness

A formula X is valid in a particular model for J_CS if it is true at all possible worlds of the model. Axiomatics for 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 J_CS if and only if X is valid in all J_CS models.

The completeness theorem as just stated is sometimes referred to as weak completeness. It maybe a bit surprising that it is significantly easier to prove than completeness for the modal logic K. Comments on this point follow. On the other hand it is very general, working for all Constant Specifications.

In (Fitting 2005) a stronger version of the semantics was also introduced. A model M = ⟨G,R,E,V⟩ is called fully explanatory if it meets the following condition. For each Γ ∈ G, if M, Δ ⊩ X for all Δ ∈ G such that Γ R Δ, then M, Γ ⊩ t:X for some justification term t. Note that the condition, M, Δ ⊩ X for all Δ ∈ G such that Γ R Δ, is the usual condition for X being believable at Γ in the Hintikka/Kripke sense. So, fully explanatory really says that if a formula is believable at a possible world, there is a justification for it.

Not all weak models meet the fully explanatory condition. Models that do are called strong models. If constant specification CS is rich enough so that an Internalization theorem holds, then one has completeness with respect to strong models meeting CS. Indeed, in an appropriate sense completeness with respect to strong models is equivalent to being able to prove Internalization.

The proof of completeness with respect to strong models bears a close similarity to the proof of completeness using canonical models for the modal logic K. In turn, strong models can be used to give a 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 been discussed, for J, the counterpart of K. Now things are broadened to encompass justification analogs of other familiar modal logics.

Simply by adding reflexivity of the accessibility relation R to the conditions for a model in Section 3.1, one gains the validity of t:X → X for every t and X, and obtains a semantics for JT, the justification logic analog of the modal logic T, the weakest logic of knowledge. Indeed, if M, Γ ⊩ t:X then, in particular, X is true at every state accessible from Γ. Since the accessibility relation is required to be reflexive, M, Γ ⊩ X. Weak and strong completeness theorems are provable using the same machinery that applied in the case of J, and a semantic proof of a Realization Theorem connecting JT and T is also available. The same applies to the logics discussed below.

For a justification analog of K4 an additional unary operator ‘!’ is added to the term language, see Section 2.5. Recall this operator maps justifications to justifications, where the idea is that if t is a justification for X, then !t should be a justification for t:X. Semantically this adds conditions to a model M = ⟨G,R,E,V⟩, as follows.

First, of course, R should be transitive, but not necessarily reflexive. Second, a monotonicity condition on evidence functions is required:

If Γ R Δ and Γ ∈ E(t,X) then Δ ∈ E(t,X)

And finally, one more evidence function condition is needed.

E(t,X) ⊆ E(!t,t:X)

These conditions together entail the validity of t:X → !t:t:X and produce a semantics for J4, a justification analog of K4, with a Realization Theorem connecting them. Adding reflexivity leads to a logic that is called LP for historical reasons.

One can also add a negative introspection operator, ‘?,’ see Section 2.6. Models for justification logics that include this operator add three conditions. First R is symmetric. Second, one adds a condition that has come to be known as strong evidence: M, Γ ⊩ t:X for all Γ ∈ E(t,X). Finally, there is a condition on the evidence function:

E(t,X) ⊆ E(?t, ¬t:X)

If this machinery is added to that for J4 we get the logic J45, a justification counterpart of K45. Axiomatic soundness and completeness can be proved. In a similar way, related logics JD45 and JT45 can be formulated.

A Realization Theorem taking this operator into account was shown in (Rubtsova 2006).

3.4 Single World Justification Models

Single world justification models were developed considerably before the more general possible world justification models we have been discussing, (Mkrtychev 1997). Today they can most simply be thought of as possible world justification models that happen to have a single world. The completeness proof for J and the other justification logics mentioned above can easily be modified to establish completeness with respect to single world justification models, though of course this was not the original argument. What completeness with respect to single world justification models tells us is that information about the possible world structure of justification models can be completely encoded by the admissible evidence function, at least for the logics discussed so far. Mkrtychev used single world justification models to establish decidability of LP, and others have made fundamental use of them in setting complexity bounds for justification logics, as well as for showing conservativity results for justification logics of belief, (Kuznets 2000, Kuznets 2008, Milnikel 2007, Milnikel 2009). Complexity results have further been used to address the problem of logical omniscience.

4. Realization Theorems

The natural modal epistemic counterpart of the evidence assertion t:F is □F, read for some x, x:F. This observation leads to the notion of forgetful projection which replaces each occurrence of t:F by □F and hence converts a Justification Logic sentence S to a corresponding Modal Logic sentence S^o. The forgetful projection extends in the natural way from sentences to logics.

Obviously, different Justification Logic sentences may have the same forgetful projection, hence S^o loses certain information that was contained in S. However, it is easily observed that the forgetful projection always maps valid formulas of Justification Logic (e.g., axioms of J) to valid formulas of a corresponding Epistemic Logic (K in this case). The converse also holds: any valid formula of Epistemic Logic is the forgetful projection of some valid formula of Justification Logic. This follows from the Correspondence Theorem 3.

Theorem 3: J^o = K.

This correspondence holds for other pairs of Justification and Epistemic systems, for instance J4 and K4, or LP and S4, and many others. In such extended form, the Correspondence Theorem shows that major modal logics such as K, T, K4, S4, K45, S5 and some others have exact Justification Logic counterparts.

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

Theorem 4: There is an algorithm which, for each modal formula F derivable in K, assigns evidence terms to each occurrence of modality in F in such a way that the resulting formula F^r is derivable in J. Moreover, the realization assigns evidence variables to the negative occurrences of modal operators in F, thus respecting the existential reading of epistemic modality.

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

It would be a mistake to draw the conclusion that any modal logic has a reasonable Justification Logic counterpart. For example the logic of formal provability, GL, (Boolos 1993) contains the Löb Principle:

(5)	□(□F → F)→ □F,

which does not seem to have an epistemically acceptable explicit version. Consider, for example, the case where F is the propositional constant ⊥ for false. If an analogue of Theorem 4 would cover the Löb Principle there would be justification terms s and t such that x:(s:⊥→ ⊥)→ t:⊥. But this is intuitively false for factive justification. Indeed, s:⊥→ ⊥ is an instance of the Factivity Axiom. Apply Axiom Internalization to obtain c:(s:⊥→ ⊥) for some constant c. This choice of c makes the antecedent of c:(s:⊥→ ⊥)→ t:⊥ intuitively true and the conclusion false^[4]. In particular, the Löb Principle (5) is not valid for the proof interpretation (cf. (Goris 2007) for a full account of which principles of GL are realizable).

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

Justification semantics plays a similar role in Modal Logic to that played by Kleene realizability in Intuitionistic Logic. In both cases, the intended semantics is existential: the Brouwer-Heyting-Kolmogorov interpretation of Intuitionistic Logic (Heyting 1934, Troelstra and van Dalen 1988, van Dalen 1986) and Gödel's provability reading of S4 (Gödel 1933, Gödel 1938). In both cases there is a possible-world semantics of universal character which is a highly potent and dominant technical tool. It does not, however, address the existential character of the intended semantics. It took Kleene realizability (Kleene 1945, Troelstra 1998) to reveal the computational semantics of Intuitionistic Logic and the Logic of Proofs to provide exact BHK semantics of proofs for Intuitionistic and Modal Logic.

In the epistemic context, Justification Logic and the Correspondence Theorem add a new ‘justification’ component to modal logics of knowledge and belief. Again, this new component was, in fact, an old and central notion which has been widely discussed by mainstream epistemologists but which remained out of the scope of classical epistemic logic. The Correspondence Theorem tells us that justifications are compatible with Hintikka-style systems and hence can be safely incorporated into the foundation for Epistemic Modal Logic.

See Section 4 of the supplementary document Some 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 of explicit knowledge, related to more conventional logics of implicit knowledge. A number of systems beyond those discussed above have been investigated in the literature, involving multiple agents, or having both implicit and explicit operators, or some combination of these.

5.1 Mixing Explicit and Implicit Knowledge

Since justification logics provide explicit justifications, while conventional logics of knowledge provide an implicit knowledge operator, it is natural to consider combining the two in a single system. The most common joint logic of explicit and implicit knowledge is S4LP (Artemov and Nogina 2005). The language of S4LP is like that of LP, but with an implicit knowledge operator added, written either K or □. The axiomatics is like that of LP, combined with that of S4 for the implicit operator, together with a connecting axiom, t:X → □X, anything that has an explicit justification is knowable.

Semantically, possible world justification models for LP need no modification, since they already have all the machinery of Hintikka/Kripke models. One models the □ operator in the usual way, making use of just the accessibility relation, and one models the justification terms as described in Section 3.1 using both accessibility and the evidence function. Since the usual condition for □X being true at a world is one of the two clauses of the condition for t:X being true, this immediately yields the validity of t:X → □X, and soundness follows easily. Axiomatic completeness is also rather straightforward.

In S4LP both implicit and explicit knowledge is represented, but in possible world justification model semantics a single accessibility relation serves for both. This is not the only way of doing it. More generally, an explicit knowledge accessibility relation could be a proper extension of that for implicit knowledge. This represents the vision of explicit knowledge as having stricter standards for what counts as known than that of implicit knowledge. Using different accessibility relations for explicit and implicit knowledge becomes necessary when these epistemic notions obey different logical laws, e.g., S5 for implicit knowledge and LP for explicit. The case of multiple accessibility relations is commonly known in the literature as Artemov-Fitting models, but will be called multi-agent possible world models here. (cf. Section 5.2).

Curiously, while the logic S4LP seems quite natural, a Realization Theorem has been problematic for it: no such theorem can be proved if one insists on what are called normal realizations (Kuznets 2010). Realization of implicit knowledge modalities in S4LP by explicit justifications which would respect the epistemic structure remains a major challenge in this area.

Interactions between implicit and explicit knowledge can sometimes be rather delicate. As an example, consider the following mixed principle of negative introspection (again □ should be read as an implicit epistemic operator),

(6)	¬t:X → □¬t:X.

From the provability perspective, it is the right form of negative introspection. Indeed, let □F be interpreted as F is provable and t:F as t is a proof of F in a given formal theory T, e.g., in Peano Arithmetic 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 established inside T, hence in T this sentence is provable. On the other hand, the proof p of ‘t is not a proof of F’ depends on both t and F, p = p(t,F) and cannot be computed given t only. In this respect, □ cannot be replaced by any specific proof term depending on t only and (6) cannot be presented in an entirely explicit justification-style format.

The first examples of explicit/implicit knowledge systems appeared in the area of provability logic. In (Sidon 1997, Yavorskaya (Sidon) 2001), a logic LPP was introduced which combined the logic of provability GL with the logic of proofs LP, but to ensure that the resulting system had desirable logical properties some additional operations from outside the original languages of GL and LP were added. In (Nogina 2006, Nogina 2007) a complete logical system, GLA, for proofs and provability was offered, in the sum of the original languages of GL and LP. Both LPP and GLA enjoy completeness relative to the class of arithmetical models, and also relative to the class of possible world justification models.

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

(7)	x:(□F → F)→ l(x):F

holds. However, there is no realization which makes all three □s in (5) explicit. In fact, the set of realizable provability principles is the intersection of GL and S4 (Goris 2007).

5.2 Multi-Agent Possible World Justification Models

In Multi-Agent possible world justification models multiple accessibility relations are employed, with connections between them, (Artemov 2006). The idea is, there are multiple agents, each with an implicit knowledge operator, and there are justification terms, which each agent understands. Loosely, everybody understands explicit reasons; these amount to evidence-based common knowledge.

An n -agent possible world justification model is a structure ⟨G,R₁, …,R_n,R,E,V⟩ meeting the following conditions. G is a set of possible worlds. Each of R₁,…,R_n is an accessibility relation, one for each agent. These may be assumed to be reflexive, transitive, or symmetric, as desired. They are used to model implicit agent knowledge for the family of agents. The accessibility relation R meets the LP conditions, reflexivity and transitivity. It is used in the modeling of explicit knowledge. E is an evidence function, meeting the same conditions as those for LP in Section 3.3. V maps propositional letters to sets of worlds, as usual. There is a special condition imposed: for each i = 1, …,n, R_i ⊆ R.

If M = ⟨G,R₁, …,R_n,R,E,V⟩ is a multi-agent possible world justification model a truth-at-a-world relation,M, Γ ⊩ X, is defined with most of the usual clauses. The ones of particular interest are these:

• M, Γ ⊩ K_iX if and only if, for every Δ ∈ G with Γ R_i Δ, we have that M, Δ ⊩ X.
• M, Γ ⊩ t:X if and only if Γ ∈ E(t,X) and, for every Δ ∈ G with Γ R Δ, we have that M, Δ ⊩ X.

The condition R_i ⊆ R entails the validity of t:X → K_iX, for each agent i. If there is only a single agent, and the accessibility relation for that agent is reflexive and transitive, this provides another semantics for S4LP. Whatever the number of agents, each agent accepts explicit reasons as establishing knowledge.

A version of LP with two agents was introduced and studied in (Yavorskaya (Sidon) 2008), though it can be generalized to any finite number of agents. In this, each agent has its own set of justification operators, variables, and constants, rather than having a single set for everybody, as above. In addition some limited communication between agents may be permitted, using a new operator that allows one agent to verify the correctness of the other agent's justifications. Versions of both single world and more general possible world justification semantics were created for the two-agent logics. This involves a straightforward extension of the notion of an evidence function, and for possible world justification models, using two accessibility relations. Realization theorems have been proved syntactically, though presumably a semantic proof would also work.

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

There is more on the notion of evidence-based common knowledge in Section 5 of the supplementary document Some More Technical Matters.

6. Russell's Example: Induced Factivity

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

If a man believes that the late Prime Minister's last name began with a ‘B,’ he believes what is true, since the late Prime Minister 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 name began with a ‘B,’ yet this belief, though true, would not be thought to constitute knowledge. (Russell 1912)

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

R = {w:B, r:B, r:B → B}

Somewhat counter to intuition, one can logically deduce factivity of w from R:

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

However, this derivation utilizes the fact that r is a factive justification for B to conclude w:B → B, which constitutes 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 truth-tracking is needed here, and Justification Logic is an appropriate tool. The natural approach is to consider the set of assumptions without r:B, i.e.,

S = {w:B, r:B → B}

and establish that factivity of w, i.e., w:B → B is not derivable from S. Here is a possible world justification model M = (G,R,E,V) in which S holds but w:B → B does not:

• G = {1},
• R = ∅,
• V(B) = ∅ (and so not-1 ⊩ B),
• E(t,F) = {1} for all pairs (t,F) except (r,B),and
• E(r,B) = ∅.

It is easy to see that the closure conditions Application and Sum on E are fulfilled. At 1, w:B holds, i.e.,

1 ⊩ w:B

since w is admissible evidence for B at 1 and there are no possible worlds accessible from 1. Furthermore,

not-1 ⊩ r:B

since, according to E, r is not admissible evidence for B at 1. Hence:

1 ⊩ r:B → B

On the other hand,

not-1 ⊩ w:B → B

since B does not hold at 1.

7. Self-referentiality of justifications

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

Self-referentiality of justifications is a new phenomenon which is not present in the conventional modal language. In addition to being intriguing epistemic objects, such self-referential assertions provide a special challenge from the semantical viewpoint because of the built-in vicious circle. Indeed, to evaluate c one would expect first 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 not modal logics can be realized without using self-referential justifications was a major open question in this area.

The principal result by Kuznets in (Brezhnev and Kuznets 2006) states that self-referentiality of justifications is unavoidable in realization of S4 in LP. The current state of things is given by the following theorem due to Kuznets:

Theorem 5: Self-referentiality can be avoided in realizations of modal logics K and D. Self-referentiality cannot be avoided in realizations of modal logics T, K4, D4 and S4.

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

Self-referentiality gives an interesting perspective on Moore's Paradox. See Section 6 of the supplementary document Some More Technical Matters for details.

8. Quantifiers in Justification Logic

While the investigation of propositional Justification Logic is far from complete, there has also been sporadic work on first-order versions. Quantified versions of Modal Logic already offer complexities beyond standard first-order logic. Quantification has an even broader field to play when Justification Logics are involved. Classically one quantifies over ‘objects,’ and models are equipped with a domain over which quantifiers range. Modally one might have a single domain common to all possible worlds, or one might have separate domains for each world. The role of the Barcan formula is well-known here. Both constant and varying domain options are available for Justification Logic as well. In addition there is a possibility that has no analog for Modal Logic: one might quantify over justifications themselves.

Initial results concerning the possibility of Quantified Justification Logic were notably unfavorable. The arithmetical provability semantics for the Logic of Proofs LP, naturally generalizes to a first-order version with conventional quantifiers, and to a version with quantifiers over proofs. In both cases, axiomatizability questions were answered negatively.

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

Although an arithmetic semantics is not possible, in (Fitting 2008) a possible world semantics, and an axiomatic proof theory, was given for a version of LP with quantifiers ranging over justifications. Soundness and completeness were proved. At this point possible world semantics separates from arithmetic semantics, which may or may not be a cause for alarm. It was also shown that S4 embeds into the quantified logic by translating □Z as “there exists a justification x such that x:Z^*,” where Z^* is the translation of Z. While this 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 and Kishida 2009).

Work has also been done on versions of Justification Logic with quantifiers over objects, both with and without an analog of the Barcan formula. None of this has been published, and it should be considered still work in progress.

9. Historical Notes

The initial Justification Logic system, the Logic of Proofs LP, was introduced in 1995 in (Artemov 1995) (cf. also (Artemov 2001)) where such basic properties as Internalization, Realization, arithmetical completeness, were first established. LP offered an intended provability semantics for Gödel's provability logic S4, thus providing a formalization of Brouwer-Heyting-Kolmogorov semantics for intuitionistic propositional logic. Epistemic semantics and completeness (Fitting 2005) were first established for LP. Symbolic models and decidability for LP are due to Mkrtychev (Mkrtychev 1997). Complexity estimates first appeared in (Brezhnev and Kuznets 2006, Kuznets 2000, Milnikel 2007). A comprehensive overview of all decidability and complexity results can be found in (Kuznets 2008). Systems J, J4, and JT were first considered in (Brezhnev 2001) under different names and in a slightly different setting. JT45 appeared independently in (Pacuit 2006) and (Rubtsova 2006), and JD45 in (Pacuit 2006). The logic of uni-conclusion proofs has been found in (Krupski 1997). A more general approach to common knowledge based on justified knowledge was offered in (Artemov 2006). Game semantics of Justification Logic and Dynamic Epistemic Logic with justifications were studied in (Renne 2008, Renne 2009). Connections between Justification Logic and the problem of logical omniscience were examined in (Artemov and Kuznets 2009, Wang 2009). The name Justification Logic was introduced in (Artemov 2008), in which Kripke, Russell, and Gettier examples were formalized; this formalization has been used for the resolution of paradoxes, verification, hidden assumption analysis, and eliminating redundancies. In (Dean and Kurokawa 2009a), Justification Logic was used for the analysis of Knower and Knowability paradoxes.

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 the Knower in the Quantified Logic of Proofs”, in Formal Epistemology Workshop / FEW 2009. Proceedings, Carnegie Mellon University, Pittsburgh, PA, USA.
• Artemov, S. (1995). “Operational modal logic”, Technical Report MSI 95–29, Cornell University.
• –––. (2001). “Explicit provability and constructive semantics”, The Bulletin of Symbolic Logic, 7(1): 1–36.
• –––. (2006). “Justified common knowledge”, Theoretical Computer Science, 357 (1–3): 4–22.
• –––. (2008). “The logic of justification”, The Review of Symbolic Logic, 1(4): 477–513.
• Artemov, S. and R. Kuznets (2009). “Logical omniscience as a computational complexity problem”, in A. Heifetz (ed.), Theoretical Aspects of Rationality and Knowledge, Proceedings of the Twelfth Conference (TARK 2009), ACM Publishers, pp. 14–23.
• Artemov, S. and E. Nogina (2005). “Introducing justification into epistemic logic”, Journal of Logic and Computation, 15(6): 1059–1073.
• Artemov, S. and T. Yavorskaya (Sidon) (2001). “On first-order logic of proofs”, Moscow Mathematical Journal, 1(4): 475–490.
• 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 knowledge explicit: How hard it is”, Theoretical Computer Science, 357 (1–3): 23–34.
• Cubitt, R. P. and R. Sugden (2003). “Common knowledge, salience and convention: A reconstruction of David Lewis' game theory”, Economics and Philosophy, 19: 175–210.
• Dean, W. and H. Kurokawa (2009a). “From the Knowability Paradox to the existence of proofs”, Synthese,, 176(2): 177–225.
• –––. (2009b). “Knowledge, proof and the Knower”, in A. Heifetz (ed.), Theoretical Aspects of Rationality and Knowledge, Proceedings of the Twelfth Conference (TARK 2009), ACM Publications, pp. 81–90.
• Dretske, F. (2005). “Is Knowledge Closed Under Known Entailment? The Case against Closure”, in M. Steup and E. Sosa (eds.), Contemporary Debates in Epistemology, Oxford: Blackwell, pp. 13–26.
• Fagin, R., J. Halpern, Y. Moses, and M. Vardi (1995). Reasoning About Knowledge, Cambridge, MA: MIT Press.
• Fitting, M. (2005). “The logic of proofs, semantically”, Annals of Pure and Applied Logic, 132(1): 1–25.
• –––. (2006). “A replacement theorem for LP”, Technical Report TR-2006002, Department of Computer Science, City University of New York.
• –––. (2008). “A quantified logic of evidence”, Annals of Pure and Applied Logic, 152(1–3): 67–83.
• –––. (2009). “Realizations and LP”, Annals of Pure and Applied Logic, 161(3): 368–387.
• Gettier, E. (1963). “Is Justified True Belief Knowledge?” Analysis, 23: 121–123.
• Girard, J.-Y., P. Taylor, and Y. Lafont (1989). Proofs and Types (Cambridge Tracts in Computer Science: Volume 7), Cambridge: Cambridge University Press.
• Gödel, K. (1933). “Eine Interpretation des intuitionistischen Aussagenkalkuls”, Ergebnisse Math. Kolloq., 4: 39–40. English translation in: S. Feferman et al. (eds.), Kurt Gödel Collected Works (Volume 1), Oxford and New York: Oxford University Press and Clarendon Press, 1986, pp. 301–303.
• –––. (1938). “Vortrag bei Zilsel/Lecture at Zilsel's” (*1938a), in S. Feferman, J. J. Dawson, W. Goldfarb, C. Parsons, and R. Solovay (eds.), Unpublished Essays and 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 equivalent to 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 provability logic”, 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 (ecture Notes in Computer Science: Volume 4514), Berlin: Springer, pp. 241–253.
• 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: Cornell University Press.
• Kleene, S. (1945). “On the interpretation of intuitionistic number theory”, The Journal of Symbolic Logic, 10(4): 109–124.
• Kolmogorov, A. (1932). “Zur Deutung der Intuitionistischen Logik”, Mathematische Zeitschrift, 35: 58–65. English translation in V.M. Tikhomirov (ed.), Selected works of A.N. Kolmogorov. Volume I: Mathematics and Mechanics, Dordrecht: Kluwer, 1991, pp. 151–158.
• Kreisel, G. (1962). “Foundations of intuitionistic logic”, in E. Nagel, P. Suppes, and A. Tarski (eds.), Logic, Methodology and Philosophy of Science. Proceedings of the 1960 International Congress, Stanford: Stanford University Press, pp. 198–210.
• –––. (1965). “Mathematical logic”, in T. Saaty (ed.), Lectures in Modern Mathematics III, New York: Wiley and Sons, pp. 95–195.
• Krupski, V. (1997). “Operational logic of proofs with functionality condition on proof predicate”, in S. Adian and A. Nerode (eds.), Logical Foundations 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. 167–177.
• Kurokawa, H. (2009). “Tableaux and Hypersequents for Justification 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 Modal Logics”, in P. Clote and H. Schwichtenberg (eds.), Computer Science Logic, 14th International Workshop, CSL 2000, Annual Conference of the EACSL, Fischbachau, Germany, August 21–26, 2000, Proceedings (Lecture Notes in Computer Science: Volume 1862), Berlin: Springer, pp. 371–383.
• –––. (2008). Complexity Issues in Justification Logic, Ph. D. dissertation, Computer Science Department, City University of New York Graduate Center.
• –––. (2010). “A note on the abnormality of realizations of S4LP”, in K. Brünnler and T. Studer (eds.), Proof, Computation, Complexity PCC 2010, International Workshop, Proceedings, IAM Technical Reports IAM-10-001, Institute of Computer Science and Applied Mathematics, University of Bern.
• McCarthy, J., M. Sato, T. Hayashi, and S. Igarishi (1978). “On the model theory of knowledge”, Technical Report STAN-CS-78-667, Department of Computer Science, Stanford University.
• Milnikel, R. (2007). “Derivability in certain subsystems of the Logic of Proofs is Π₂^p-complete”, Annals of Pure and Applied Logic, 145(3): 223–239.
• –––. (2009). “Conservativity for Logics of Justified 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 Computer Science, 4th International Symposium, LFCS'97, Yaroslavl, Russia, July 6–12, 1997, Proceedings (Lecture Notes in Computer Science: Volume 1234), Berlin: Springer, pp. 266–275.
• Nogina, E. (2006). “On logic of proofs and provability”, in 2005 Summer Meeting of the Association for Symbolic Logic, Logic Colloquium'05, Athens, Greece (July 28–August 3, 2005), The Bulletin of Symbolic Logic, 12(2): 356.
• –––. (2007). “Epistemic completeness of GLA”, in 2007 Annual Meeting of the Association for Symbolic 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 Modal Logics”, Technical Report PP–2006–29, Institute for Logic, Language and Computation, University of Amsterdam.
• Plaza, J. (2007). “Logics of public communications”, Synthese, 158(2): 165–179.
• Renne, B. (2008). Dynamic Epistemic Logic with Justification, Ph. D. thesis, Computer Science Department, CUNY Graduate Center, New York, NY, USA.
• –––. (2009). “Evidence Elimination in Multi-Agent Justification Logic”, in A. Heifetz (ed.), Theoretical Aspects of Rationality and Knowledge, Proceedings of the Twelfth Conference (TARK 2009), ACM Publications, pp. 227–236.
• Rose, G. (1953). “Propositional calculus and realizability”, Transactions of the American Mathematical Society, 75: 1–19.
• Rubtsova, N. (2006). “On Realization of S5-modality by Evidence Terms”, Journal of Logic and Computation, 16(5): 671–684.
• Russell, B. (1912). The Problems of Philosophy, Oxford: Oxford University Press.
• Sidon, T. (1997). “Provability logic with operations on proofs”, in S. Adian and A. Nerode (eds.), Logical Foundations 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 Proof Theory, Amsterdam: Cambridge University Press.
• Troelstra, A. and D. van Dalen (1988). Constructivism in Mathematics (Volumes 1, 2), Amsterdam: North–Holland.
• van Dalen, D. (1986). “Intuitionistic logic”, in D. Gabbay and F. Guenther (eds.), Handbook of Philosophical Logic (Volume 3), Bordrecht: Reidel, pp. 225–340.
• van Ditmarsch, H., W. van der Hoek, and B. Kooi (ed.), (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 Logical Omniscience”, in H. Ono, M. Kanazawa, and R. de Queiroz (eds.), Logic, Language, Information and Computation, 16th International Workshop, WoLLIC 2009, Tokyo, Japan, June 21-24, 2009, Proceedings (Lecture Notes in Artificial Intelligence: Volume 5514), Berlin: Springer, pp. 394–407.
• Yavorskaya (Sidon), T. (2001). “Logic of proofs and provability”, Annals of Pure and Applied Logic, 113 (1–3): 345–372.
• –––. (2008). “Interacting Explicit Evidence Systems”, Theory of Computing Systems, 43(2): 272–293.
• Yavorsky, R. (2001). “Provability logics with quantifiers on proofs”, Annals of Pure and Applied Logic, 113 (1–3): 373–387.

Academic Tools

	How to cite this entry.
	Preview the PDF version of this entry at the Friends of the SEP Society.
	Look up this entry topic at the Indiana Philosophy Ontology Project (InPhO).
	Enhanced bibliography for this entry at PhilPapers, with links to its database.

Other Internet Resources

• Justification Logic Bibliography, A complete bibliography of material on justification logic. Maintained by Roman Kuznets, researcher at the Research Group for Theoretical Computer Science and Logic (TIL) in the Institute of Computer Science and Applied Mathematics (IAM) of the University of Bern.

Related Entries

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

Copyright © 2011 by
Sergei Artemov <sartemov@gc.cuny.edu>
Melvin Fitting <melvin.fitting@lehman.cuny.edu>