Justification Logic

Origin. Sergei Artemov introduced the Logic of Proofs (LP) in 1995, solving a long-standing problem about the intended provability semantics of intuitionistic logic. Extended to justification logic more broadly (2000s). Replaces the box □φ with explicit justifications t:φ ("t is a justification for φ"). Makes evidence explicit where modal logic leaves it implicit.

Models. Explicit reasons for knowledge/belief. Epistemic logic says Kφ ("the agent knows φ") but not why. Justification logic says t:φ ("t justifies φ") — the evidence is named. Solves puzzles about logical omniscience: you might know all axioms without knowing complex theorems built from them.

Formalism.

Justification terms:

Constants: a, b, c, ... (atomic justifications, axiom evidence)
Variables: x, y, z, ... (unknown justifications)
Application: t · s (combining justifications)
Sum: t + s (alternative justifications)
Check: !t (justification that t is a justification)

Formulas:

Propositional atoms: p, q, ...
Connectives: ¬, ∧, ∨, →
Justification assertion: t:φ ("t is a justification for φ")

Basic axioms (LP - Logic of Proofs):

t:(φ → ψ) → (s:φ → (t·s):ψ) — Application
t:φ → (t+s):φ and s:φ → (t+s):φ — Sum
t:φ → φ — Factivity (for knowledge)
t:φ → !t:(t:φ) — Positive introspection (proof checker)

Constant specification: CS: assignment of constants to axioms. c:A means constant c justifies axiom A.

Connection to modal logic: Forgetful projection: replace t:φ with □φ. LP projects onto S4: if LP ⊢ t:φ then S4 ⊢ □φ.

Realization theorem (Artemov): Every S4 theorem has an LP realization. □φ can be replaced by t:φ for appropriate t.

Justified knowledge vs belief:

LP: factivity (t:φ → φ) — knowledge
J: no factivity — belief
JT, J4, J45, etc. — various systems

Symbols.

Symbol	Unicode	Name	Meaning
t:φ	—	Justification assertion	t justifies φ
·	U+00B7	Application	Combine justifications
+	—	Sum	Alternative justification
!	—	Check/Proof checker	Justify the justification
?	—	Negative checker	Justifies that t does not justify φ
c	—	Constant	Atomic evidence
□	U+25A1	Box	Implicit modality
⊢	U+22A2	Derives	Provability
t, s	—	Justification terms	Built from constants, variables, ·, +, !
x, y	—	Justification variables	Unspecified evidence
CS	—	Constant specification	Which constants justify which axioms
→	U+2192	Material conditional	Used in the application axiom
¬	U+00AC	Negation	Propositional connective
∧	U+2227	Conjunction	Propositional connective
∨	U+2228	Disjunction	Propositional connective
⌜	U+231C	Left corner quote	Gödel numeral, opening
⌝	U+231D	Right corner quote	Gödel numeral, closing

Metatheory. The realization theorem is the central result: every theorem of S4 becomes a theorem of LP when each occurrence of □ is replaced by a suitable term, and the replacement is computed constructively from a cut-free Gentzen derivation; conversely the forgetful projection, sending every t: to □, maps LP theorems to S4 theorems, so LP is exactly the explicit counterpart of S4. Artemov (1995, 2001) proved LP arithmetically complete for the provability reading, which settles the problem Gödel raised in 1933: S4 is the modal logic of intuitionistic provability, but its axiom □A → A is not arithmetically sound when □ is read as provability in Peano Arithmetic, since by Löb's theorem PA proves Prov(⌜A⌝) → A only when it proves A — whereas the explicit t:A → A is sound, a concrete proof of A witnessing A. Mkrtychev (1997) showed LP complete for single-world models, so no accessibility relation is needed; Fitting (2005) restored Kripke structure. Derivability in LP is Π₂ᵖ-complete for axiomatically appropriate, schematic constant specifications — Kuznets gave the Π₂ᵖ upper bound, Milnikel the matching hardness, which Buss and Kuznets generalized — and Π₂ᵖ is contained in PSPACE, though the inclusion is not known to be strict.

Applies to. Formal epistemology (explicit evidence). Proof theory (provability semantics). Security (explicit credentials). Verification (evidence-carrying code). Philosophy (justified true belief analysis). Avoiding logical omniscience in AI agents.

Limitations. Realization is a fact about theorems, not a decision procedure for agents: it yields a term for each S4 theorem, but many terms realize the same formula and the logic supplies no criterion for preferring one, so "the" justification of a belief is not determined. Self-referential constant specifications of the form c:A(c) cannot be eliminated — Kuznets showed S4 is not realizable in LP without them — so the framework is committed to a form of circularity in its base evidence. Explicit terms defeat omniscience only over which formulas are justified; the underlying propositional logic remains classical and closed. Justification is monotone: terms record how a conclusion was reached but carry no notion of strength, defeat or retraction, so evidence once possessed is never undermined, and the logic has no operation corresponding to losing a reason.