On interpretability logics

Katsumi Sasaki

                        sasaki@iq.nanzan-u.ac.jp

Department of Information Systems and Quantitative Sciences, Nanzan University

The idea of interpretability logics arose in Visser [Vis90]. He introduced the logics as extensions of the provability logic GL with a binary modality ▷. The arithmetic realization of A ▷ B in a theory T will be that T plus the realization of B is interpretable in T plus the realization of A. (T + A interprets T + B). More precisely, there exists a function f (the relative interpretation) on the formulas of the language of T such that T + B ⊢ C implies T + A ⊢ f(C).

The basic interpretability logic IL is the smallest set of formulas containing GL and axioms (J1) : □(p ⊃ q) ⊃ (p ▷ q), (J2) : (p ▷ q) ∧ (q ▷ r) ⊃ (p ▷ r), (J3) : (p ▷ r) ∧ (q ▷ r) ⊃ (p ∨ q ▷ r), (J4) : (p ▷ q) ⊃ (◇p ⊃ ◇q), (J5) : ◇p ▷ p,

and closed under modus ponens, substitution and necessitation. The principles of IL are arithmetically sound for a wide class of theories and for various interpretations of its main connective ▷. The theory is not arithmetically complete for any known interpretation. The motivation for studying this specific set of formulas comes form its modal simplicity and elegance.

The modality ▷ has more than one interpretation. Another most salient interpretation is Π_{1}-conservativity. More precisely, the arithmetic realization of A ▷ B in a theory T, containing IΣ_{1}, will be that T plus the realization of B is Π_{1}-conservative over T plus the interpretation of A. In Berarducci [Ber90] and Shavrukov [Sha88], it was proved that the interpretability logic (ILM) obtained by adding Montagna’s axiom

M : (p ▷ q) ⊃ (p ∧ □r) ▷ (q ∧ □r)

to IL is complete for this arithmetic interpretation. The definition of the arithmetic interpretation ∗ given for the proof of Solovay’s theorem was extended to the language of interpretability logics by stipulating that

(A ▷ B)^{∗} = Conserv(⟨A^{∗}⟩, ⟨B^{∗}⟩), where Conserv(⟨A^{∗}⟩, ⟨B^{∗}⟩) is an intensional formalization of “T + B^{∗} is Π_{1}-conservative over T + A^{∗}”, and it was proved

A ∈ ILM if and only if T ⊢ A^{∗} for any ∗.

The interpretability logic ILP, an extension of IL by adding the axiom

P : (p ▷ q) ⊃ □(p ▷ q),

is also complete for another arithmetic interpretation. P is valid for interpretations in finitely axiomatized arithmetical theories extending, say, IΔ_{0} + Ω_{1}, and an arithmetic completeness for this interpretation was proved in [Vis90].

The completeness with respect to Kripke semantics due to Veltman was, for IL, ILM and ILP, proved in de Jongh and Veltman [JV90]. The fixed point theorem of GL can be extended to IL and hence ILM and ILP(de Jongh and Visser [JV91]). The unary pendant “T interprets T + A” is much less expressive and was studied in de Rijke [Rij92]. For an overview of interpretability logic, see Visser [Vis97], and Japaridze and de Jongh [JJ98].

Here we give a cut-free sequent system for the basic interpretability logic IL. First, we give a cut-free system for a sublogic IK4, whose ▷-free fragment is the modal logic K4. In other words, IK4 is the logic obtained from K4 by adding the axioms (J1), (J2), (J3), (J4) and (J5). Using the system and a property of Löb’s axiom presented in [Sas99c] we obtain a cut-free system for IL.

Let us define a sequent system for IK4. We use Greek letters, possibly with suffixes, for finite sets of formulas, in particular, we use Σ, possibly with suffices, for finite set of ▷-formulas^{1}. The expression Γ_{A} denotes Γ − {A}. For each prefix ◯ ∈ {□, ¬}, the expression ◯Γ denotes the set {◯X|X ∈ Γ}. By a sequent, we mean the expression

Γ → Δ.

For brevity’s sake, we write

A_{1}, ⋯, A_{n}, Γ_{1}, ⋯, Γ_{m} → B_{1}, ⋯, B_{ℓ}, Δ_{1}, ⋯, Δ_{k}

instead of

{A_{1}, ⋯, A_{n}} ∪ Γ_{1} ∪ ⋯ ∪ Γ_{m} → {B_{1}, ⋯, B_{ℓ}} ∪ Δ_{1} ∪ ⋯ ∪ Δ_{k}.

Let S_{1}, ⋯, S_{n} be a sequence of sequents. The depth d_{S_{1},···,S_{n}}(o_{i}) of the occurrence o_{i} of S_{i} denotes n + 1 − i. If there is no confusion, we omit the subscript of d.

Let Σ be a finite set of ▷-formulas. A sequent is said to be a sequent on a sequent Σ, □Γ → A ▷ B if it is of the form

C, □¬(B^{∗}, Δ), Γ, □Γ → B^{∗}, Δ,

where C ∈ {A} ∪ {Y |X ▷ Y ∈ Σ}, Δ ⊆ {X|X ▷ Y ∈ Σ} and

B^{∗} = \{ \begin{matrix}∅ & if B = ⊥ \\ B & otherwise. \end{matrix}

We put

cl(C, □¬(B^{∗}, Δ), Γ, □Γ → B^{∗}, Δ) = C,
cr(C, □¬(B^{∗}, Δ), Γ, □Γ → B^{∗}, Δ) = Δ.

Immediately, a sequent S on Σ, □Γ → A ▷ B is of the form

cl(S), □¬(B^{∗}, cr(S)), Γ, □Γ → B^{∗}, cr(S).

For an occurrence o of a sequent S in SEQ, we also use the expressions cl(o) and cr(o) for cl(S) and cr(S), respectively. We say that a sequence SEQ of sequents is on a sequent Σ, □Γ → A ▷ B if it is finite sequence of sequents on Σ, □Γ → A ▷ B and cl(o) = A for some occurrence o of a sequent in SEQ.

Let Σ′ be a subset of Σ. A mapping

f : {(o, X)|o is an occurrence of a sequent in SEQ, X ∈ cr(o)}

→ {o|o is an occurrence of a sequent in SEQ, cl(o) ≠ A}

is called a mapping on SEQ/Σ′ if X ▷ cl(f(o, X)) ∈ Σ′ and d(o) > d(f(o, X)) for any occurrence o and an formula X ∈ cr(o).

We say that a sequence SEQ of sequents is essential on a sequent Σ, □Γ → A ▷ B if it is on Σ, □Γ → A ▷ B and the following two conditions hold:

(I) there exists an onto mapping on SEQ/Σ,

(II) cl(o_{1}) ≠ cl(o_{2}) for any different occurrences o_{1} and o_{2} of sequents in SEQ.

Let SEQ be an essential sequence on Σ, □Γ → A ▷ B and let f be an onto mapping on SEQ/Σ. Since SEQ is finite, we can see a sequent

C, □¬(B^{∗}, Δ), Γ, □Γ → B^{∗}, Δ

1formulas of the form A ▷ B

at the end occurrence o of SEQ. If X ∈ Δ, then 0 = d(o) > d(f(o, X)). This is a contradiction. So, we have Δ = ∅, i.e., we can see a sequent

Y, □¬B^{∗}, Γ, □Γ → B^{∗}

at the end of the sequence SEQ.

Here we show some examples of essential sequences. A sequence of a sequent

p, □¬q, r, □r → q

is only one essential sequence on

□r → p ▷ q.

Two sequences of sequents

p, □¬q, □¬p_{1} → q, p_{1} q_{1}, □¬q → q

and

p, □¬q → q

are essential on

p_{1} ▷ q_{1} → p ▷ q.

Also two sequences

p, □¬q, □¬p_{1} → q, p_{1} q_{1}, □¬q, □¬p_{2}, → q, p_{2} q_{2}, □¬q → q

and

p, □¬q, □¬p_{1}, □¬p_{2} → q, p_{1}, p_{2} q_{1}, □¬q → q q_{2}, □¬q → q

are essential on

p_{1} ▷ q_{1}, p_{2} ▷ q_{2} → p ▷ q.

Our system GIK4 is defined from the following axioms and inference rules in the usual way.

Axioms of GIK4

A → A
⊥ →

Inference rules of GIK4

\frac{Γ → Δ}{A, Γ → Δ}(T →) \frac{Γ → Δ}{Γ → Δ, A}(→ T)

\frac{Γ → Δ, A A, Π → Λ}{Γ, Π_{A} → Δ_{A}, Λ}(cut)

\frac{A_{i}, Γ → Δ}{A_{1} ∧ A_{2}, Γ → Δ}(∧ →_{i}) \frac{Γ → Δ, A Γ → Δ, B}{Γ → Δ, A ∧ B} (→ ∧)

\frac{A, Γ → Δ B, Γ → Δ}{A ∨ B, Γ → Δ}(∨ →) \frac{Γ → Δ, A_{i}}{Γ → Δ, A_{1} ∨ A_{2}} (→ ∨_{i})

\frac{Γ → Δ, A B, Γ → Δ}{A ⊃ B, Γ → Δ}(⊃→) \frac{A, Γ → Δ, B}{Γ → Δ, A ⊃ B} (→⊃)

\frac{SEQ}{X_{1} ▷ Y_{1}, ⋯, X_{n} ▷ Y_{n}, □Γ → A ▷ B} (▷_{IK4})

where SEQ is essential on the lower sequent,

\frac{SEQ}{X_{1} ▷ Y_{1}, ⋯, X_{n} ▷ Y_{n}, □Γ → □A}(□_{IK4})

where SEQ is essential on

X_{1} ▷ Y_{1}, ⋯, X_{n} ▷ Y_{n}, □Γ → ¬A ▷ ⊥

A proof figure for a sequent Γ → Δ is defined as usual. We say that Γ → Δ is provable in GIK4, and write Γ → Δ ∈ GIK4, if there exists a proof figure for Γ → Δ.

Then we have the following two theorems.

Theorem 1. A ∈ IK4 if and only if → A ∈ GIK4.

Theorem 2. If Γ → Δ ∈ GIK4, then there exists a cut-free proof figure for Γ → Δ in GIK4.

Next, we define a sequent system GIL for IL. The system GIL is obtained from GIK4 by replacing (□_{IK4}) and (▷_{IK4}) by the following two inference rules, respectively:

\frac{SEQ}{X_{1} ▷ Y_{1}, ⋯, X_{n} ▷ Y_{n}, □Γ → A ▷ B} (▷_{IL})

where SEQ is essential on the sequent X_{1} ▷ Y_{1}, ⋯, X_{n} ▷ Y_{n}, □Γ → (A ∧ □¬A) ▷ B,

\frac{SEQ}{X_{1} ▷ Y_{1}, ⋯, X_{n} ▷ Y_{n}, □Γ → □A}(□_{IL})

where SEQ is essential on the sequent X_{1} ▷ Y_{1}, ⋯, X_{n} ▷ Y_{n}, □Γ → (¬A ∧ □A) ▷ ⊥.

Theorem 3. A ∈ IL if and only if → A ∈ GIL.

For cut-elimination theorem, we use the method in [Sas99c]. By sketching his proof, we obtain

Theorem 4. If Γ → Δ ∈ GIL, then there exists a cut-free proof figure for Γ → Δ.

References

[Ber90] A. Berarducci, The interpretability logic of Peano arithmetic, The Journal of Symbolic Logic, 55, 1990, pp. 1059–1089.

[JJ98] G. Japaridze and D. H. J. de Jongh, The Logic of Provability, in Handbook of proof theory, edited by S. R. Buss, University of California, 1998, pp. 475–546.

[JV90] D. H. J. de Jongh and F. Veltman, Provability logics for relative interpretability, in Mathematical logic, Proceedings of the Heyting 1988 Summer School, edited by P. Petkov, Plenum Press, 1990, pp. 31–42.

[JV91] D. H. J. de Jongh and A. Visser, Explicit fixed points in interpretability logic, Studia Logica, 50, 1991, pp. 39–50.

[Rij92] M. de Rijke, Unary interpretability logic, Notre Dame Journal of Formal Logic, 33, 1992 pp. 249–272.

[Sas99c] K. Sasaki, On a property of Löb’s axiom in propositional logics, submitted.

[Sha88] V. Yu. Shavrukov, The logic of relative interpretability over Peano arithmetic (Russian), Technical Report No. 5, Stekhlov Mathematical Institute, Moscow, 1988.

[Vis90] A. Visser, Interpretability logic, in Mathematical logic, Proceedings of the Heyting 1988 Summer School, edited by P. Petkov, Plenum Press, 1990, pp. 175–209.

[Vis97] A. Visser, An overview of interpretability logic, in Advances in Modal Logic ’96, edited by M. Kraft, M. de Rijke, and H. Wansing, CSLI Publications, 1997.