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 φ
·	—	Application	Combine justifications
+	—	Sum	Alternative justification
!	—	Check/Proof checker	Justify the justification
?	—	Evidence variable	Unknown justification
c	—	Constant	Atomic evidence
□	U+25A1	Box	Implicit modality
⊢	U+22A2	Derives	Provability

Metatheory. LP is decidable (same complexity as S4). Realization theorem: S4 embeds into LP. Internalization: proofs can be converted to terms. No logical omniscience problem: t:φ and s:(φ→ψ) gives (t·s):ψ only via explicit step. Arithmetical completeness: LP terms correspond to Gödel numbers of proofs in Peano Arithmetic.

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. More complex than modal logic. Term structure adds overhead. Which constants justify which axioms (constant specification) is a design choice. Applications less developed than modal logic. Realization from modal to justification can be non-constructive. Evidence arithmetic becomes complex in rich systems.