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: PA ⊳ φ iff PA + φ consistent. Interpretability = relative consistency.

Σ₁-completeness: Interpretability = Π₁-conservativity. 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	Interprets	Relative strength
□	U+25A1	Provable	Standard
IL	—	Interpretability	Logic family

Metatheory. Decidable. Complete for appropriate semantics. Arithmetic completeness for ILM.

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

Limitations. Specialized. Less intuitive than GL. Technical semantics. Limited applications.