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	—	Justifies	t is proof of A
·	—	Application	Combine proofs
+	—	Sum	Either proof
!	—	Checker	Proof of proof
?	—	Verifier	Check proof
x	—	Variable	Proof variable
c	—	Constant	Axiom proof

Metatheory. LP decidable (PSPACE). Realization theorem: S4 ⊆ LP (via forgetful projection). Arithmetic completeness: LP captures provability in PA (Artemov). Fitting models: possible worlds + evidence. Internalization: proofs about proofs.

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

Limitations. Proof terms can be complex. Realization not unique. Less intuitive than modal. Tool support limited. Research community specialized. Extensions multiply.