Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Uniform interpolation for interpretability logic

Sebastijan Horvat, Borja Sierra Miranda, Thomas Studer

TL;DR

The paper develops a comprehensive proof-theoretic framework for interpretability logic $\mathsf{IL}$ by introducing three calculi: a wellfounded sequent calculus $\mathcal{G}\mathsf{IL}$, a non-wellfounded local-progress calculus $\mathcal{G}^\infty\mathsf{IL}$, and its cyclic regularization $\mathcal{G}^\circ\mathsf{IL}$. It proves equivalence among these systems and with the Hilbert calculus, and leverages non-wellfounded proofs to establish uniform interpolation for $\mathsf{IL}$ and $\mathsf{ILP}$ via a sophisticated interpolation template construction and a fixpoint-based modal-equational analysis. Central to the approach are translations between calculi, cut-elimination foundations, and a regularization process that yields cyclic proofs suitable for interpolation. The results provide a robust syntactic method for interpolation in interpretability logics and open avenues for extending these methods to broader bimodal provability frameworks. The work thus advances both the theory of non-wellfounded proof systems and the practical understanding of interpolation in modal logics with interpretability modalities.

Abstract

We present a proof-theoretical study of the interpretability logic IL, providing a wellfounded and a non-wellfounded sequent calculus for IL. The non-wellfounded calculus is used to establish a cut elimination argument for both calculi. In addition, we show that the non-wellfounded proof theory of IL is well-behaved, i.e., that cyclic proofs suffice. This makes it possible to prove uniform interpolation for IL. As a corollary we also provide a proof of uniform interpolation for the interpretability logic ILP.

Uniform interpolation for interpretability logic

TL;DR

The paper develops a comprehensive proof-theoretic framework for interpretability logic by introducing three calculi: a wellfounded sequent calculus , a non-wellfounded local-progress calculus , and its cyclic regularization . It proves equivalence among these systems and with the Hilbert calculus, and leverages non-wellfounded proofs to establish uniform interpolation for and via a sophisticated interpolation template construction and a fixpoint-based modal-equational analysis. Central to the approach are translations between calculi, cut-elimination foundations, and a regularization process that yields cyclic proofs suitable for interpolation. The results provide a robust syntactic method for interpolation in interpretability logics and open avenues for extending these methods to broader bimodal provability frameworks. The work thus advances both the theory of non-wellfounded proof systems and the practical understanding of interpolation in modal logics with interpretability modalities.

Abstract

We present a proof-theoretical study of the interpretability logic IL, providing a wellfounded and a non-wellfounded sequent calculus for IL. The non-wellfounded calculus is used to establish a cut elimination argument for both calculi. In addition, we show that the non-wellfounded proof theory of IL is well-behaved, i.e., that cyclic proofs suffice. This makes it possible to prove uniform interpolation for IL. As a corollary we also provide a proof of uniform interpolation for the interpretability logic ILP.

Paper Structure

This paper contains 19 sections, 36 theorems, 154 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Interpretability Logic
  4. Non-wellfounded Proof Theory
  5. Basics of Local Progress Calculi.
  6. The Method of Translations.
  7. Transformations between calculi
  8. Equivalence of Hilbert calculus and $\mathcal{G}\mathsf{IL} + \mathrm{Cut}$
  9. From $\mathcal{G}\mathsf{IL} + \mathrm{Cut}$ to $\mathcal{G}^\infty \mathsf{IL} + \mathrm{Cut}$
  10. From $\mathcal{G}^\infty \mathsf{IL}$ to $\mathcal{G}\mathsf{IL}$
  11. Cut elimination
  12. Regularizing proofs
  13. Uniform interpolation
  14. Modal equational systems
  15. Construction of the interpolant
  16. ...and 4 more sections

Key Result

Lemma 2.3

Let $\phi,\psi$ be formulas and $\Sigma$ be a non-empty finite multiset of formulas. Then

Figures (5)

  • Figure 1: The plan. Arrows without labels are omitted in this paper.
  • Figure 2: Structure of proofs in local progress calculi
  • Figure 3: Corecursive step function (top) and its extension from proofs to proofs (bottom). Tall gray (white) triangles represent proofs in $G$ ($G'$) and short gray (white) triangles represent local fragments in $G$ ($G'$).
  • Figure 4: Sequent rules
  • Figure 5: $\mathbin{\rhd}^*_{\mathrm{IK4}}$ rule

Theorems & Definitions (89)

  • Definition 2.1
  • Definition 2.2
  • Lemma 2.3
  • proof
  • Definition 2.4
  • Definition 2.5
  • Definition 2.6
  • Definition 2.7
  • Lemma 2.8
  • proof
  • ...and 79 more