#### Supplement to Justification Logic

## Some More Technical Matters

- 1. Mathematical Logic Tradition
- 2. Logical Awareness and Constant Specifications
- 3. Single-Agent Possible World Models for \(\mathsf{J}\)
- 4. Realization Theorems
- 5. Multi-Agent Justification Models
- 6. Self-referentiality of Justifications

### 1. Mathematical Logic Tradition

Several well-known mathematical notions which appeared prior to
Justification Logic have sometimes been perceived as related to the
BHK idea: Kleene realizability (Troelstra 1998), Curry-Howard
isomorphism (Girard, Taylor, and Lafont 1989, Troelstra and
Schwichtenberg 1996), Kreisel-Goodman theory of constructions
(Goodman 1970, Kreisel 1962, Kreisel 1965), just to name a few. These
interpretations have been very instrumental for understanding
intuitionistic logic, though none of them qualifies as the
*BHK* semantics.

Kleene realizability revealed a fundamental *computational
content* of formal intuitionistic derivations, however it is
still quite different from the intended *BHK* semantics.
Kleene realizers are computational programs rather then proofs. The
predicate ‘*r realizes F* ’ is not decidable,
which leads to some serious deviations from intuitionistic logic.
Kleene realizability is not adequate for the intuitionistic
propositional calculus \(\mathsf{IPC}\).
There are realizable propositional formulas
not derivable in \(\mathsf{IPC}\)
(Rose
1953).^{[1]}

The Curry-Howard isomorphism transliterates natural derivations in \(\mathsf{IPC}\) to typed \(\lambda\)-terms thus providing a generic functional reading for logical derivations. However the foundational value of this interpretation is limited since, as proof objects, Curry-Howard \(\lambda\)-terms denote nothing but derivations in \(\mathsf{IPC}\) itself and thus yield a circular provability semantics for the latter.

An attempt to formalize the *BHK* semantics directly was made
by Kreisel in his theory of constructions (Kreisel 1962, Kreisel
1965). The original variant of the theory was
inconsistent; difficulties already occurred at the propositional
level. In (Goodman 1970) this was fixed by introducing a
stratification of constructions into levels, which ruined the
*BHK* character of this semantics. In particular, a proof of
\(A \rightarrow B\) was no longer a construction that could
be applied to any proof of \(A\)

### 2. Logical Awareness and Constant Specifications

Two examples in \(\mathsf{J}\) are presented, showing modal theorems of \(\mathsf{K}\), and realizations for them. In the examples indices on constants have been omitted.

**Example 1.** This shows how to build
a justification of a conjunction from justifications of the
conjuncts. In traditional modal language, this principle is
formalized as \(\Box A \wedge \Box B \rightarrow \Box ( A \wedge B)\). In
\(\mathsf{J}\) this idea is expressed in the more
precise justification language.

- \(A \rightarrow ( B \rightarrow ( A \wedge B))\) (propositional axiom)
- \(c :( A \rightarrow ( B \rightarrow ( A \wedge B))\)) (from 1 by Axiom Internalization)
- \(x : A \rightarrow [ c \cdot x ]:( B \rightarrow ( A \wedge B))\) (from 2 by Application and Modus Ponens)
- \(x : A \rightarrow ( y : B \rightarrow [[ c \cdot x ] \cdot y ]:( A \wedge B))\) (from 3 by Application and propositional reasoning)
- \(x : A \wedge y : B \rightarrow [[ c \cdot x ] \cdot y ]:( A \wedge B)\) (from 5 by propositional reasoning)

The derived formula 5 contains the constant \(c\), which was introduced in line 2, and the complete reading of the result of this derivation is:

\(x : A \wedge y : B \rightarrow [[ c \cdot x ] \cdot y ]:( A \wedge B)\), given \(c :( A \rightarrow ( B \rightarrow ( A \wedge B))\)).

**Example 2.** This example shows how to build a
justification of a disjunction from justifications of either of the
disjuncts. In the usual modal language this is represented by \(\Box A
\vee \Box B \rightarrow \Box ( A \vee B)\).Here is the corresponding
result in \(\mathsf{J}\).

- \(A \rightarrow ( A \vee B)\) (classical logic)
- \(a :( A \rightarrow ( A \vee B))\) (from 1 by Axiom Internalization)
- \(x : A \rightarrow [ a \cdot x ]:( A \vee B)\) (from 2 by Application and Modus Ponens)
- \(B \rightarrow ( A \vee B)\) (by classical logic)
- \(b :( B \rightarrow ( A \vee B))\) (from 4 by Axiom Internalization)
- \(y : B \rightarrow [ b \cdot y ]:( A \vee B)\) (from 5 by Application and Modus Ponens)
- [\(a \cdot x ]:( A \vee B ) \rightarrow [ a \cdot x\) + \(b \cdot y ]:( A \vee B)\) (by Sum)
- [\(b \cdot y ]:( A \vee B ) \rightarrow [ a \cdot x\) + \(b \cdot y ]:( A \vee B)\) (by Sum)
- \((x : A \vee y : B ) \rightarrow [ a \cdot x\) + \(b \cdot y ]:( A \vee B)\) (from 3, 6, 7, and 8 by propositional reasoning)

The complete reading of the result of this derivation is:

\((x : A \vee y : B ) \rightarrow [ a \cdot x\) + \(b \cdot y ]:( A \vee B)\), given \(a :( A \rightarrow ( A \vee B))\) and \(b :( B \rightarrow ( A \vee B))\)

### 3. Single-Agent Possible World Models for \(\mathsf{J}\)

Here are two models in each of which \(x : P \rightarrow x :( P \wedge Q)\) is not valid. \((P\) and \(Q\) are atomic and \(x\) is a justification variable.) It was pointed out that a formula \(t : X\) might fail at a possible world either because \(X\) is not believable there (it is false at some accessible world), or because \(t\) is not an appropriate reason for \(X\). The two models illustrate both versions.

First, consider the model \(\mathcal{M}\) having a single state, \(\Gamma\), accessible to itself, and with an evidence function such that \(\mathcal{E} ( x , Z)\) is \(\Gamma\), for every formula \(Z\). In this model, \(x\) serves as‘universal’ evidence. Use a valuation such that \(\mathcal{V} ( P)\) = \(\Gamma\) and \(\mathcal{V} ( Q)\) = \(\varnothing\). Then one has \(\mathcal{M} , \Gamma\) ⊩ \(x : P\) but not-\(\mathcal{M} , \Gamma\) ⊩ \(x :( P \wedge Q)\) because, even though \(x\) serves as universal evidence, \(P \wedge Q\) is not believable at \(\Gamma\) in the Hintikka/Kripke sense because \(Q\) is not true.

Next consider the model \(\mathcal{N}\) , again having a single state \(\Gamma\) accessible to itself. This time take \(\mathcal{V}\) to be the mapping assigning \(\Gamma\) to every propositional letter. But also, set \(\mathcal{E} ( x , P)\) = \(\Gamma , \mathcal{E} ( x , Z)\) = \(\varnothing\) for \(Z \ne P\), and otherwise \(\mathcal{E}\) doesn’t matter for this example. Then of course both \(P\) and \(P \wedge Q\) are believable at \(\Gamma\), but \(\mathcal{N} , \Gamma\) ⊩ \(x : P\) and not-\(\mathcal{N} , \Gamma\) ⊩ \(x :( P \wedge Q)\), the latter because \(x\) does not serve as evidence for \(P \wedge Q\) at \(\Gamma\).

In Hintikka/Kripke models, believability and knowability are
essentially semantic notions, but the present treatment of evidence is
more of a syntactic nature. For example, the model \(\mathcal{N}\)
above also invalidates \(x : P \rightarrow x :( P \wedge P)\). At
first glance this is surprising, since in any standard logic of
knowledge or belief \(\Box P \rightarrow \Box ( P \wedge P)\) is
valid. But, just because \(x\) serves as evidence for \(P\), it need
not follow that it also serves as evidence for \(P \wedge P\). The
formulas are syntactically different, and effort is needed to
recognize that the later formula is a redundant version of the
former.To take this to an extreme, consider the formula \(x : P
\rightarrow x :( P \wedge P \wedge\) … \(\wedge P )\), where
the consequent has as many conjuncts as there are elementary particles
in the universe! In brief, Hintikka/Kripke style knowledge is
knowledge of *propositions*, but justification terms
justify *sentences*.

### 4. Realization Theorems

Here is an example of an \(\mathsf{S4}\)-derivation realized as an \(\mathsf{LP}\)-derivation in the style of the Realization theorem. There are two columns in the table below. The first is a Hilbert-style \(\mathsf{S4}\)-derivation of a modal formula \(\Box A \vee \Box B \rightarrow \Box ( \Box A \vee B)\). The second column displays corresponding steps of an \(\mathsf{LP}\)-derivation of a formula:

\(x : A \vee y : B \rightarrow ( a \cdot ! x\) + \(b \cdot y ):( x : A \vee B)\)

with constant specification

\(\{a :( x : A \rightarrow x : A \vee B ), b :( B \rightarrow x : A \vee B ) \}\).

Derivation in \(\mathsf{S4}\) | Derivation in \(\mathsf{LP}\) | |

1. | \(\Box A \rightarrow \Box A \vee B\) | \(x : A \rightarrow x : A \vee B\) |

2. | \(\Box ( \Box A \rightarrow \Box A \vee B)\) | \(a :( x : A \rightarrow x : A \vee B)\) |

3. | \(\Box \Box A \rightarrow \Box ( \Box A \vee B)\) | !\(x : x : A \rightarrow ( a \cdot ! x ):( x : A \vee B)\) |

4. | \(\Box A \rightarrow \Box \Box A\) | \(x : A \rightarrow ! x : x : A\) |

5. | \(\Box A \rightarrow \Box ( \Box A \vee B)\) | \(x : A \rightarrow ( a \cdot ! x ):( x : A \vee B)\) |

\(5'\). | \((a \cdot ! x ):( x : A \vee B ) \rightarrow ( a \cdot ! x\) + \(b \cdot y ):( x : A \vee B)\) | |

\(5''\). | \(x : A \rightarrow ( a \cdot ! x\) + \(b \cdot y ):( x : A \vee B)\) | |

6. | \(B \rightarrow \Box A \vee B\) | \(B \rightarrow x : A \vee B\) |

7. | \(\Box ( B \rightarrow \Box A \vee B)\) | \(b :( B \rightarrow x : A \vee B)\) |

8. | \(\Box B \rightarrow \Box ( \Box A \vee B)\) | \(y : B \rightarrow ( b \cdot y ):( x : A \vee B)\) |

\(8'\). | \((b \cdot y ):( x : A \vee B ) \rightarrow ( a \cdot ! x\) + \(b \cdot y ):( x : A \vee B)\) | |

\(8''\). | \(y : B \rightarrow ( a \cdot ! x\) + \(b \cdot y ):( x : A \vee B)\) | |

9. | \(\Box A \vee \Box B \rightarrow \Box ( \Box A \vee B)\) | \(x : A \vee y : B \rightarrow ( a \cdot ! x\) + \(b \cdot y ):( x : A \vee B)\) |

Extra steps \(5' , 5'' , 8'\), and \(8''\) are needed in the \(\mathsf{LP}\) case to reconcile different internalized proofs of the same formula: \((a \cdot ! x ):( x : A \vee B)\) and \((b \cdot y ):( x : A \vee B)\). The resulting realization respects Skolem’s idea that negative occurrences of existential quantifiers (here over proofs hidden in the modality of provability) are realized by free variables whereas positive occurrences are realized by functions of those variables.

Proof theory plays an important role in the study of Justification Logics. Axiom systems we represented in this article, and a sequent calculus was introduced in (Artemov 1995, Artemov 2001).It has the curious disadvantage that it is cut free, but does not have the subformula property—no version with the subformula property is known. More recently, other kinds of proof procedures for Justification Logics have been created. Kurokawa uses hypersequents to provide a comprehensive proof-theoretical treatment of major systems of Justification Logic, (Kurokawa 2009), including those which combine implicit and explicit knowledge. These systems are notoriously hard to analyze and Kurokawa’s results constitute a remarkable fundamental contribution to this area.

Currently realizations are being investigated for their own sake,
(Fitting 2009). The basic results all are algorithmic in nature. For
example, in Modal Logic a Replacement Theorem holds just as it does
classically: if \(X \equiv X'\) is provable in a normal modal logic
then so is \(F \equiv F '\) where \(F\) is a formula and \(F'\) is
like \(F\) except that some subformula occurrence \(X\) has been
replaced with \(X'\). Indeed this can be strengthened to establish
that if \(X \rightarrow X'\) is provable, and \(X\) has
a *positive* designated subformula occurrence in \(F\), while
\(F'\) replaces that occurrence with \(X'\), then \(F \rightarrow F
'\) is provable. This does not carry over in a simple way to
Justification Logic. Roughly speaking, an occurrence of \(X\) in a
formula \(F\) of Justification Logic may be within the scope of
various justification terms, and in \(F'\) these will need to be
‘adjusted’ to take into account a justification for \(X
\rightarrow X'\). It turns out this is not simple, but an algorithm
for doing so has been developed, (Fitting 2006, Fitting 2009).

Here is another result having a similar proof. In a modal sequent calculus argument a typical step is the following.

\[\notag \frac{S_{1} \rightarrow S_{2} , X \quad\quad S_{1} \rightarrow S_{2} , Y}{S_{1} \rightarrow S_{2} , X \wedge Y} \]The notion of a realization easily extends from formulas to sequents. Suppose both of the premise sequents above have realizations, and one would like a realization for the consequent sequent. The problem is, the two premise realizations may be quite different. Algorithmic machinery for merging them has been developed that does exactly this. This algorithm, in turn, serves as part of a new algorithm for the Realization Theorem itself.

### 5. Multi-Agent Justification Models

To simplify the language, one can use the forgetful projection which
replaces explicit knowledge assertions \(t : X\) by
\(\mathbf{J}X\) where \(\mathbf{J}\) stands for so-called
*justified common knowledge*
modality. Modality \(\mathbf{J}\) is a stronger version of common
knowledge: \(\mathbf{J}X\) states all agents share
sufficient evidence for \(X\). In a formal setting, in Kripke
models, \(\mathbf{J}X \rightarrow \mathbf{C}X\), but not necessarily
\(\mathbf{C}X \rightarrow \mathbf{J}X\) (Artemov 2006).

Informally, the traditional common knowledge modality (Fagin, Halpern, Moses, and Vardi 1995) is represented by the condition

\(\mathbf{C}X \Leftrightarrow X \wedge EX \wedge E^{2}X \wedge\) … \(\wedge E^{n}X \wedge\) …

whereas for the justified common knowledge operator \(\mathbf{J}\) one has

\(\mathbf{J}X \Rightarrow X \wedge EX \wedge E^{2}X \wedge\) … \(\wedge E^{n}X \wedge\) …

Justified common knowledge has the same modal principles as McCarthy’s common knowledge (McCarthy, Sato, Hayashi, and Igarishi 1978). In (Cubitt and Sugden 2003) a case is made that David Lewis’ version of common knowledge (more properly, belief) is not identified with unlimited iteration of knowledge operators, but is much closer to justified common knowledge. (See the encyclopedia article on Common Knowledge). A good example of such a Lewis-McCarthy-Artemov justified common knowledge assertion, \(\mathbf{J}X\), which is stronger than the usual common knowledge, \(\mathbf{C}X\), is provided by situations following a public announcement of \(X\) (Plaza 2007) after which \(X\) holds at all states, not only at reachable states. Note that public announcements are the usual means for attaining common knowledge, and they lead to justified common knowledge \(\mathbf{J}\) rather than the usual common knowledge \(\mathbf{C}\).

The axiomatic description of justified common knowledge \(\mathbf{J}\) is significantly simpler than that of \(\mathbf{C}\) . According to (Antonakos 2007), in the standard epistemic scenarios, justified common knowledge \(\mathbf{J}\) is conservative with respect to the usual common knowledge \(\mathbf{C}\) and hence provides a lighter alternative to the latter.

### 6. Self-referentiality of Justifications

Let us consider an example which was suggested by the well-known
*Moore’s paradox*:

It will rain but I don’t believe that it will.

If \(R\) stands for *it will rain*, then a modal
formalization is:

\(M = R \wedge \neg \Box R\).

The Moore sentence \(M\) is easily satisfiable, hence consistent, e.g., whenever the weather forecast wrongly shows “no rain”. However, it is impossible to know Moore’s sentence because

\(\neg \Box M = \neg \Box ( R \wedge \neg \Box R)\)

holds in any modal logic containing \(\mathsf{T}\) . Here is a derivation.

- \((R \wedge \neg \Box R ) \rightarrow R\) (logical axiom)
- \(\Box (( R \wedge \neg \Box R ) \rightarrow R)\) (Necessitation)
- \(\Box ( R \wedge \neg \Box R ) \rightarrow \Box R\), (from 2 by Distribution)
- \(\Box ( R \wedge \neg \Box R ) \rightarrow ( R \wedge \neg \Box R)\) (Factivity in \(\mathsf{T})\)
- \(\Box ( R \wedge \neg \Box R ) \rightarrow \neg \Box R\) (from 4 in Boolean logic)
- \(\neg \Box ( R \wedge \neg \Box R)\) (from 3 and 5 in Boolean logic)

Furthermore, here is how this derivation is realized in \(\mathsf{LP}\).

- \((R \wedge \neg [ c \cdot x ]: R ) \rightarrow R\) (logical axiom)
- \(c :(( R \wedge \neg [ c \cdot x ]: R ) \rightarrow R)\) (Constant Specification)
- \(x :( R \wedge \neg [ c \cdot x ]: R ) \rightarrow [ c \cdot x ]: R\) (from 2 by Application)
- \(x :( R \wedge \neg [ c \cdot x ]: R ) \rightarrow ( R \wedge \neg [ c \cdot x ]: R)\) (Factivity)
- \(x :( R \wedge \neg [ c \cdot x ]: R ) \rightarrow \neg [ c \cdot x ]: R\) (from 4 by Boolean logic)
- \(\neg x :( R \wedge \neg [ c \cdot x ]: R)\) (from 3 and 5 in Boolean logic)

Note that Constant Specification in line 2 is self-referential.