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.

ILM axioms: GL + L1: □(A → B) → A ⊳ B L2: (A ⊳ B ∧ B ⊳ C) → A ⊳ C L3: (A ⊳ B ∧ A ⊳ C) → A ⊳ (B ∧ C) M: (A ⊳ B ∧ ◇A) → ◇B

Orey-Hájek: PA ⊳ φ iff PA + φ consistent. Interpretability = relative consistency.

Σ₁-completeness: Interpretability = Π₁-conservativity. Connection to proof theory.

IL systems: ILP: basic interpretability. ILM: with M axiom (PA). ILW: with W axiom (weaker).

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.