Interpretability Logic

Origin. Visser (1990s). One theory interprets another. □ for provability, ⊳ for interpretability. IL systems. Foundation for relative consistency.

Models. Frame with interpretability relation. A ⊳ B: A interprets B. Stronger than provable implication. Orey-Hájek characterization.

Formalism.

Interpretation: T₁ interprets T₂ (T₁ ⊳ T₂) iff: translation τ: L₂ → L₁ with T₁ ⊢ τ(φ) for all T₂ ⊢ φ.

Interpretability operator: A ⊳ B: "A interprets B." Modal formula over sentences.

IL axioms (the base system): GL + J1: □(A → B) → A ⊳ B J2: (A ⊳ B ∧ B ⊳ C) → A ⊳ C J3: (A ⊳ C ∧ B ⊳ C) → (A ∨ B) ⊳ C J4: A ⊳ B → (◇A → ◇B) J5: ◇A ⊳ A

Montagna's axiom (ILM = IL + M): M: A ⊳ B → (A ∧ □C) ⊳ (B ∧ □C)

Orey–Hájek characterization: For essentially reflexive T (e.g. PA): T + A interprets T + B iff T + A ⊢ Con_n(T + B) for every n, where Con_n is consistency for proofs of complexity ≤ n. Not the same as "T + B is consistent": PA + Con(PA) is consistent but PA does not interpret it, since that would give PA ⊢ Con(PA), contra Gödel II.

Conservativity: Over essentially reflexive T, T + A ⊳ T + B iff T + B is Π₁-conservative over T + A. Connection to proof theory.

IL systems: IL: the base system. ILM: with M axiom — arithmetically complete for PA and other essentially reflexive theories. ILP: with P axiom (A ⊳ B → □(A ⊳ B)) — finitely axiomatized theories. ILW: with W axiom (A ⊳ B → A ⊳ (B ∧ □¬A)).

Semantics: Veltman frames. Accessibility + interpretability order. Specific conditions per system.

Fixed points: Exist for interpretability formulas. More complex than GL.

Symbols.

Symbol	Unicode	Name	Meaning
⊳	U+22B3	Interpretability operator	A interprets B
□	U+25A1	Box / Provability	Provable in the base theory
◇	U+25C7	Diamond / Consistency	¬□¬; consistent with the base theory
⊢	U+22A2	Derivability	Provable in the calculus or the theory
τ	U+03C4	Tau	Translation between languages
Σ₁	—	Sigma-one	Existential arithmetical complexity class
Π₁	—	Pi-one	Universal arithmetical complexity class
IL	—	Base interpretability logic	GL + J1–J5
ILM	—	IL plus Montagna's axiom	Interpretability logic of PA
ILP	—	IL plus persistence	Interpretability logic of finitely axiomatized theories
ILW	—	IL plus W	A ⊳ B → A ⊳ (B ∧ □¬A)
J1–J5	—	Interpretability axioms	Base laws for ⊳
Con_n	—	Partial consistency statement	Consistency for proofs of complexity ≤ n

Metatheory. De Jongh and Veltman (1990) proved IL sound and complete for Veltman semantics — frames ⟨W, R, {S_w}⟩ where R is the GL accessibility relation and each S_w is a preorder on the R-successors of w — and established the same for ILM and ILP; all three have the finite model property and are decidable. Arithmetical completeness splits by the character of the base theory: Shavrukov (1988) and Berarducci (1990) independently proved that ILM is exactly the interpretability logic of PA and of every essentially reflexive Σ₁-sound theory, while Visser (1990) proved that ILP is the interpretability logic of finitely axiomatized sequential theories such as GB and ACA₀. The Orey–Hájek characterization reduces ⊳ over essentially reflexive theories to provability of all partial consistency statements, and thence to Π₁-conservativity. IL extends GL conservatively in the modal fragment, and the de Jongh–Sambin fixed point property carries over.

Applies to. Foundations. Relative consistency. Theory comparison. Proof theory.

Limitations. There is no single interpretability logic: ILM and ILP are incomparable extensions of IL, each arithmetically complete for a class of theories the other excludes, and no theory falls under both, since essential reflexivity rules out finite axiomatizability. The operator ⊳ therefore has no theory-independent reading — which principles it obeys depends on how the base theory is presented. The interpretability logic of all reasonable arithmetical theories, IL(All) — the intersection over every sensible base theory — remains unidentified; the known lower bound ILW and its strengthenings have not been matched by a completeness proof. Arithmetical completeness requires Σ₁-soundness of the base theory and breaks for theories that are consistent but not Σ₁-sound. The language is propositional, and since quantified provability logic is already Π⁰₂-complete by Vardanyan's theorem, no recursive axiomatization of a quantified interpretability logic is available. Veltman semantics is not canonical in the usual sense: the frame conditions for M and P are not first-order Sahlqvist conditions on a single accessibility relation.