On Bimodal Provability Logics

Katsumi Sasaki

                        sasaki@ms.nanzan-u.ac.jp

Department of Mathematical Sciences, Nanzan University

Provability logic GL is one of the normal modal logics, which is obtained from the smallest normal modal logic K by adding Löb’s axiom. The name “provability logic” derives from Solovay’s theorem in Solovay [Sol76]. He proved that GL is complete for the formal provability interpretation in Peano arithmetic PA. By his theorem, we might as well say a formula □A asserts that A^{∗} is provable in PA, where A^{∗} is an arithmetic sentence corresponding to A.

Smoryński [Sym85] considered bimodal provability logics by extending GL with another modal operator ∇. An arithmetic interpretation of ∇A is a provability of another arithmetic theory. After that, bimodal provability logics for other arithmetic theories have been considered in several papers, especially Beklemishev [Bek96] gives a detailed survey of this topic.

Here we treat two bimodal provability logics MOS and PRL_{1} among the logics in [Sym85] and give cut-free sequent systems for these two logics.

1 Bimodal provability logics

In this section, we introduce bimodal provability logics MOS and PRL_{1} and their Kripke semantics(cf. [Sym85]). The language of the bimodal provability logics consists of propositional variables, ⊥, ∧, ∨, ⊃, □ and ∇. Formulas are defined as usual.

Definition. The modal logic MOS is the smallest set of formulas containing all tautologies, K: □(A ⊃ B) ⊃ (□A ⊃ □B), L: □(□A ⊃ A) ⊃ □A, A1: ∇A ⊃ □∇A, A2: □A ⊃ ∇A and A3: □(A ⊃ B) ⊃ (∇A ⊃ ∇B)

and closed under modus ponens and necessitation.

Definition. The modal logic PRL_{1} is the smallest set of formulas containing all tautologies, K, L, A1, A2 and

A4: ∇(A ⊃ B) ⊃ (∇A ⊃ ∇B) and closed under modus ponens and necessitation.

Definition. A Kripke model for MOS is a tuple K = ⟨K, <, F, ⊧⟩, where (1) K is a non-empty set,

(2) < is an irreflexive and transitive binary relation on K,

(3) F is a mapping from K to P(P(K)) satisfying (3.1) X ∈ F (α) implies X ⊆ {γ | α < γ}, (3.2) {γ | α < γ} ∈ F (α) and (3.3) α < β and X ∈ F (α) imply X ∩ {γ | β < γ} ∈ F (β),

(4) ⊧ is a valuation satisfying, in addition to the usual boolean laws, (4.1) α ⊧ □A iff for any β ∈ {γ | α < γ}, β ⊧ A and

(4.2) α ⊧ ∇A iff there exists X ∈ F (α) such that for any β ∈ X, β ⊧ A.

Definition. A Kripke model for PRL_{1} is a tuple K = ⟨K, <, R, ⊧⟩, where (1) ⟨K, <⟩ is as in the above definition,

(2) R is a binary relation on K satisfying (2.1) αRβ implies α < β and (2.2) α < βRγ implies αRγ

(3) ⊧ is a valuation satisfying, in addition to the usual boolean laws, (3.1) α ⊧ □A iff for any β ∈ {γ | α < γ}, β ⊧ A and (3.2) α ⊧ ∇A iff for any β ∈ {γ | αRγ}, β ⊧ A.

Let K be a Kripke model for MOS or PRL_{1}. We say that a formula A is valid in a Kripke model if α ⊧ A for any α ∈ K.

Lemma 1.1([sym85]).

(1) A ∈ MOS iff A is valid for any Kripke model for MOS.

(2) A ∈ PRL_{1} iff A is valid for any Kripke model for PRL_{1}.

2 Sequent systems

In this section, we introduce sequent systems for MOS and PRL_{1} and prove cut-elimination theorems. For a finite set of formulas, we use Greek letters Γ, Δ, Σ, · · ·. The expressions □Γ and ∇Γ denote the set {□A | A ∈ Γ} and {∇A | A ∈ Γ}. By a sequent, we mean an expression Γ → Δ. For brevity’s sake, we write

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

instead of

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

The sequent system GMOS is the system obtained from LK by adding the following inference rules.

\frac{□A, Γ, □Γ, ∇Σ → A}{□Γ, ∇Σ → □A}(□)

\frac{∇A, B, ∇B, Γ, □Γ, ∇Σ → A}{∇B, □Γ, ∇Σ → ∇A}(∇_{1})

\frac{∇A, Γ, □Γ, ∇Σ → A}{□Γ, ∇Σ → ∇A}(∇_{2})

The sequent system PRL_{1} is the system obtained from LK by adding the above inference rule (□) and the following inference rule.

\frac{∇A, Γ, □Γ, Σ, ∇Σ → A}{□Γ, ∇Σ → ∇A}(∇_{3})

Lemma 2.1.

(1) If a sequent A_{1}, ⋯, A_{m} → B_{1}, ⋯, B_{n} is provable in GMOS, then (A_{1}∧⋯∧A_{m}) ⊃ (B_{1}∨⋯∨B_{n}) is valid for any Kripke model for MOS.

(2) If a sequent A_{1}, ⋯, A_{m} → B_{1}, ⋯, B_{n} is provable in GPRL_{1}, then (A_{1}∧⋯∧A_{m}) ⊃ (B_{1}∨⋯∨B_{n}) is valid for any Kripke model for PRL_{1}.

For a proof of the above lemma, we use Lemma 1.1 and the sequent system for GL described in Valentini [Val83] and Avron [Avr84].

Theorem 2.2.

(1) If there exists no cut-free proof figure for Γ → Δ in GMOS, then there exist Kripke model K for MOS and α ∈ K such that α ⊧ A for A ∈ Γ and α |̸= B for B ∈ Δ.

(2) If there exists no cut-free proof figure for Γ → Δ in GPRL_{1}, then there exist Kripke model K for PRL_{1} and α ∈ K such that α ⊧ A for A ∈ Γ and α |̸= B for B ∈ Δ.

For a proof of the above theorem, we use the method in [Avr84]. We construct a Kripke model K with a set K of saturated sequents, and for the least saturated sequent α, we show that α ⊧ A for A ∈ Γ and that α |̸= B for B ∈ Δ.

Corollary 2.3.

(1) A_{1}, ⋯, A_{m} → B_{1}, ⋯, B_{n} is provable in GMOS iff (A_{1} ∧ ⋯ ∧ A_{m}) ⊃ (B_{1} ∨ ⋯ ∨ B_{n}) ∈ MOS.

(2) A_{1}, ⋯, A_{m} → B_{1}, ⋯, B_{n} is provable in GPRL_{1} iff (A_{1} ∧ ⋯ ∧ A_{m}) ⊃ (B_{1} ∨ ⋯ ∨ B_{n}) ∈ PRL_{1}.

Corollary 2.4.

(1) If a sequent Γ → Δ is provable in GMOS, then there exists a cut-free proof figure for Γ → Δ.

(2) If a sequent Γ → Δ is provable in GPRL_{1}, then there exists a cut-free proof figure for Γ → Δ.

References

[Avr84] A. Avron, On modal systems having arithmetical interpretations, The Journal of Symbolic Logic, 49, 1984, pp. 935–942.

[Bek96] L. D. Beklemishev, Bimodal logics for extensions of arithmetical theories, The Journal of Symbolic Logic, 61, 1996, pp. 91–124.

[Smo85] C. Smoryński, Self-reference and Modal logic, Springer-Verlag, 1985.

[Sol76] R. M. Solovay, Provability interpretations of modal logic, Israel Journal of Mathematics, 25, 1976, pp. 287–304.

[Val83] S. Valentini, The modal logic of provability: cut-elimination, Journal of Philosophical logic, 12, 1983, pp. 471–476.