Logic of Proofs

Origin. Artemov introduced Logic of Proofs LP (1995, 2001). Explicit justification logic. t:A means "t is a proof of A." Realizes modal logic S4: □A becomes t:A for some proof term t. Provides computational semantics for modality.

Models. Explicit proof terms. Modal □A: "A is necessary/provable." LP t:A: "t is a proof/justification of A." Proof terms have structure: combine, apply, check. Realization: every S4 theorem has LP version with explicit terms.

Formalism.

Proof terms: t ::= x | c | (t · s) | (t + s) | !t | ?t

x: proof variable
c: proof constant (axiom proof)
t · s: application (modus ponens)
t + s: sum (disjunction of proofs)
!t: proof checker (proof of t:A is proof of !t:(t:A))

Formulas: φ ::= p | ¬φ | φ → ψ | t:φ

Axioms:

Classical propositional axioms
t:(A → B) → (s:A → (t·s):B) (application)
t:A → (t+s):A, s:A → (t+s):A (sum)
t:A → !t:(t:A) (proof checker)
t:A → A (reflexivity)

Realization theorem: For every S4 theorem φ, there exists LP formula φʳ with proof terms such that LP ⊢ φʳ. Replaces □ with explicit t:.

Justification logic: Generalization: various justification logics. J: basic justification logic. JT, J4, LP: adding reflection and positive introspection.

Symbols.

Symbol	Unicode	Name	Meaning
t:A	—	Justification assertion	t is a proof of A
·	U+00B7	Middle dot	Application: modus ponens on proofs
+	—	Plus sign	Sum: either proof suffices
!	—	Proof checker	Proof that t proves A
?	—	Negative verifier	Proof that t does not prove A
x	—	Proof variable	Unspecified proof
c	—	Proof constant	Proof of an axiom, fixed by a constant specification
□	U+25A1	White square / Box	Implicit necessity; the forgetful projection of t:
¬	U+00AC	Not sign	Negation
→	U+2192	Rightwards arrow	Material implication
⊢	U+22A2	Derivability	Provable in the calculus
⌜ ⌝	U+231C, U+231D	Corner quotes	Gödel numeral of a formula
φ, ψ	U+03C6, U+03C8	Phi, psi	Schematic formulas
::=	—	BNF definition	Grammar of terms and formulas
LP, J, JT, J4	—	System names	Justification logics projecting onto S4, K, T and K4

Metatheory. Artemov (1995, 2001) proved LP arithmetically complete for proof predicates in Peano Arithmetic: a formula is a theorem of LP exactly when every arithmetical interpretation of it — terms sent to proofs, t:A to the standard proof predicate applied to ⌜A⌝ — is provable in PA. The realization theorem supplies the other half: every theorem of S4 becomes a theorem of LP when each □ is replaced by an appropriate term, and the forgetful projection sending every t: back to □ maps LP onto exactly S4, so the two are the explicit and implicit presentations of one logic. Composing this with the Gödel–McKinsey–Tarski translation gives intuitionistic propositional logic the provability semantics Gödel sought in 1933 and that □ itself cannot carry, since by Löb's theorem PA proves Prov(⌜A⌝) → A only for those A it already proves. The projections of the weaker systems are equally exact: J onto K, JT onto T, J4 onto K4. Mkrtychev (1997) proved completeness for single-world models, which yields decidability outright, and derivability in LP is Π₂ᵖ-complete for axiomatically appropriate, schematic constant specifications (Kuznets's upper bound, Milnikel's hardness, generalized by Buss and Kuznets).

Applies to. Foundations of modal logic. Epistemic logic (explicit evidence). Verification (proof certificates). Type theory (Curry-Howard). Cryptographic protocols. Certified computation.

Limitations. Realization is not unique: many terms realize the same S4 theorem and the logic offers no criterion for choosing among them, so the theorem produces an explicit counterpart without identifying the explicit counterpart. Self-referential constant specifications of the form c:A(c) cannot be eliminated if S4 is to be realized, so circular base evidence is forced rather than adopted for convenience. The terms are untyped codes rather than lambda terms, which makes the Curry–Howard reading an analogy: t·s is well formed whatever t and s prove, and only the application axiom limits what it justifies. Arithmetical completeness is a propositional result about proof predicates for Peano Arithmetic and does not carry to the quantified language. Justification is monotone — the calculus combines and checks evidence but has no operation for defeating or withdrawing it, so a reason once held is never lost.