SIMPLIFIED CUT-ELIMINATION FOR MODAL PROVABILITY LOGICS

Abstract. We give simple, uniform and modular proofs of cut-elimination for GL, Go and Grz. The existing proofs in the literature are highly intricate and specialised.

1. Problem?

What does the cut-elimination procedure produce for the following cut:

\begin{matrix}p, □q ⇒ □¬¬q & □¬¬q ⇒ □q, p \\ p, □q ⇒ □q, p \end{matrix}

It appears to produce this:

\begin{matrix}q, □q ⇒ q \\ p, □q ⇒ □q, p \end{matrix}

But this is NOT a derivation since it breaks the (*) condition?

It may be that you need to keep an eye out for instances of (id) at every step of the proof ? For example, the base case is “if U, X ⇒ Y, V is an instance of (id) then stop”.

Another possible problem is that mh is not respected upwards by cut!

2. Introduction

Modal provability logics extend the basic normal modal logic K with axioms which interpret the □ connective as the mathematical notion of being “provable” in Peano Arithmetic [?]. There are several variants with characteristic axioms named after Gödel, Löb and Grzegorczyk:

Name of Logic Characteristic Axiom
GL  □(□p → p) → □p
Go  □(□(p → □p) → p) → □p
Grz  □(□(p → □p) → p) → p

While the “provability” interpretation is now well-understood, the proof-theory of these logics is intricate and somewhat controversial as we explain next.

Following Gentzen [?], the literature abounds with proofs of cut-elimination for various logics using size of the cut formula and height of the premise derivations. But these measures proved inadequate for proving cut-elimination for GL, so Valentini introduced a third novel measure called width, and showed that cut-elimination for GL now required a triple induction over size, height and width [?].

Controversy arose when it was (erroneously) claimed that Valentini’s proofs contained a gap [?] and various authors provided alternative proofs of cut-elimination in response [?, ?, ?]. The question was resolved in Valentini’s favour, with all proofs verfied using an interactive theorem prover Isabelle/HOL [?].

His??? proofs for the logic Go are even more intricate, involving .... Rev, can you please fill in this part as I can’t remember the details any more.

1

\begin{aligned}(id) \\ & X, A ⇒ A, Y \end{aligned}

\begin{aligned}X ⇒ Y, A & B, X ⇒ Y \\ (→ l) \\ & A → B, X ⇒ Y \end{aligned}  \begin{aligned}& A, X ⇒ Y, B \\ (→ r) \\ & X ⇒ Y, A → B \end{aligned}

\begin{aligned}A, X ⇒ Y & B, X ⇒ Y \\ (∨ l) \\ & A ∨ B, X ⇒ Y \end{aligned}  \begin{aligned}& X ⇒ Y, A, B \\ (∨ r) \\ & X ⇒ Y, A ∨ B \end{aligned}

\begin{aligned}& A, B, X ⇒ Y \\ (∧ l) \\ & A ∧ B, X ⇒ Y \end{aligned}  \begin{aligned}X ⇒ A, Y & X ⇒ B, Y \\ (∧ r) \\ & X ⇒ A ∧ B, Y \end{aligned}

\begin{aligned}& X ⇒ Y, A \\ (¬ l) \\ & ¬A, X ⇒ Y \end{aligned}  \begin{aligned}& A, X ⇒ Y \\ (¬r) \\ & X ⇒ Y, ¬A \end{aligned}

□X, X, □B ⇒ B

(GLR)  U non-boxed multiset

U, □X ⇒ □B, V

□X, X, □(B → □B) ⇒ B
(GoR)  U non-boxed multiset

U, □X ⇒ □B, V

A, □A, X ⇒ Y
(T)  need some side-conditions for mh-argument
□A, X ⇒ Y

Figure 1. Sequent Rules

Thus the proof-theory of provability logics was significantly more complicated than the proof-theory of numerous other modal logics.

Recently, Brighton [] gave yet another method for proving cut-elimination for GL which is significantly shorter and simpler than any of the existing proofs of cut-elimination in the literature because it uses only a double induction on weight and “maximum height of regress trees”.

Here, we finesse Brighton’s argument by porting it to a sequent calculus, rather than “regress-trees”, and fix some errors in Valentini’s original proof. Moreover we show how this argument extends to Go where the only extant proof [?] is highly intricate.

**more story and citations**

3. Syntax and Axiomatisations of Provability Logics

Modal formulae are constructed from an infinite set P of atomic formulae using the Backus-Naur form below where p ∈ P:

A, B ::= p | ¬A | A → B | A ∨ B | A ∧ B | □A

The ♢ connective does not appear explicitly but is defined via ♢A := ¬□¬A.

A boxed formula has □ as its main connective while a non-boxed formula does not. A boxed/non-boxed multiset contains only boxed/non-boxed formulae.

The Hilbert-calculus for the basic normal modal logic K is obtained by extending a Hilbert-calulus for classical propositional logic with the axiom □(p → q) → (□p → □q) and the inference rule of neccessitation: from A infer □A. The various provability logics are then obtained by adding further axioms as shown below:

X, X, Y ⇒ Z ; (lc) ; X, Y ⇒ Z  X ⇒ Y, Z, Z ; (rc) ; X ⇒ Y, Z
\begin{aligned}X ⇒ Y \\ & (w) \\ U, X ⇒ Y, V \end{aligned} \begin{aligned}X ⇒ Y, A & A, U ⇒ V \\ & (cut) \\ X, U ⇒ Y, V \end{aligned}

Figure 2. Structural Rules

Name of Logic  Axioms
GL  □(□p → p) → □p
GL_{lin} □(□p → p) → □p □(□p → q) ∨ □(□q → q)
Go  □(□(p → □p) → p) → □p
Grz  □(□(p → □p) → p) → □p □p → p

The axiomatisation of Grz given above is indirect since the characteristic axiom □(□(p → □p) → p) → p is actually obtained by chaining the two axioms shown in the table above. This axiomatisation justifies the sequent rules for Grz to follow.

4. Sequent Caluli, Semi-derivations and Maximum Height

A sequent is a tuple (X, Y) of formula multisets, written X ⇒ Y. Let X ∩Y, X ∪ Y and ∅ denote, respectively, the multiset intersection, union and empty multiset. So {A} ∪ {A} is the multiset consisting of two occurrences of A. In sequents, we also write A, X or X, A to stand for A ∪ X, and similarly write X, Y for X ∪ Y.

The various sequent calculi are shown below using rules from Figure 1:

Name Sequent Calculus Rules
PC  (id) (¬L) (¬R) (→L) (→R) (∧L) (∧R) (∨L) (∨R)
GLS PC + (GLR)
GoS PC + (GoR)
GrzS PC + (GoR) + (T)

Definition 1 (semi-derivation, derivation). A semi-derivation in the sequent calculus is defined inductively as a sequent, or a rule applied upwards to a leaf of a semi-derivation, that additionally satisfies

(∗) an initial sequent occurs only as a leaf If every leaf of the semi-derivation is an initial sequent, then it is called a derivation and its end-sequent (root) is said to be derivable.

Note that (∗) ensures that only minimal derivations are permitted: no rule is applied upwards to an initial sequent as captured by the (id) rule. Apart from this, the definition of derivation above is the standard one. The following definition of height is also standard.

Definition 2 (height). The height of a semi-derivation is the number of sequents along its longest branch.

In both (GLR) and (GoR), the purpose of restricting U to a non-boxed multiset is to ensure that all boxed formulae in the antecedent persist upwards in the semiderivation via □X. This will be exploited in the proof of Lemma 2 to show that every sequent has a semi-derivation of maximum height.

A single premise sequent rule is admissible in a calculus if the conclusion is derivable whenever the premise is derivable. An admissible rule is height preserving if the height of the derivation of the conclusion is no greater than that of the derivation of the premise.

It is easy to see via a standard proof theoretic induction on height that the rules (lc), (rc) of contraction and (w) of weakening from Figure 2 are admissible in both GLS and GoS. Using these rules, it is easy to establish the following.

Theorem 1. The sequent calculi GLS+(cut) and GoS+(cut) are sound and complete for the axiomatically formulated logics GL and Go respectively.

In the sequel we show how to replace GLS + (cut) and GoS + (cut) with GLS and GoS, respectively, by showing how to transform a derivation with cuts into a derivation of the same end-sequent without cuts.

While height-preserving contraction suffices for most proof theoretic arguments, the use of “maximum height of a semi-derivation of a sequent” as an induction parameter requires a more precise result. A rule is perfectly height preserving (php) admissible if the derivations of the conclusion and premise have identical heights.

Lemma 1. The contraction rule is php-admissible in both GLS and GoS.

Will you not need an Proof. Induction on the height of a derivation. ⊣ inversion lemma for this ?

The complexity of a sequent s is the number |s| of logical connectives in s.

Lemma 2. [semi-derivation maximum height mh] In C (C ∈ {GLS, GoS}), every sequent s has a semi-derivation of maximum height, denoted by mh(s). Moreover, for every rule instance with a premise s_{1} and conclusion s_{0}: mh(s_{1}) < mh(s_{0}).

Proof. The proofs for GLS and GoS are almost identical so we only consider GL.

Certainly for every sequent s, there is a semi-derivation ending with s: consider the semi-derivation comprising of the single sequent s. To prove the first claim, we will show that every semi-derivation of s has height bounded by a function in |s|.

First note that any boxed formula in the antecedent of a sequent persists in all sequents above it since no rule removes a formula □B upwards from the antecedent. This means that the number of (GLR) rules along every branch is bounded by the number of boxed formulae in s, for otherwise, some branch would contain two (GLR) rules with the same diagonal formula □B and hence the conclusion of the upper rule would have the form U, □B ⇒ □B, V violating (∗).

Observe that the complexity of the premise of a (GLR) rule is at most twice the complexity of the conclusion: the doubling is because the premise contains □X, X, □B, B whenever the conclusion has the form □X ⇒ □B. N.B. In the case of GoS, “at most twice” should be replaced by “at most four times” to account for the larger formula □(B → □B) in the premise.

Next, note that the number of propositional rules that can be applied upwards from a given sequent is finite since each such rule results in a sequent with strictly less complexity. We can bound the number of propositional rules that can occur above a sequent s′ by its complexity |s′|.

Putting this all together, and bounding the number of boxed formulae in s by |s|, the height of a semi-derivation of a sequent s in GLS (GoS) is bounded by below left (resp. below right).

|s| · 2|s| · 4|s| · 8|s| ⋯ 2^{|s|} · |s|  |s| · 4|s| · 16|s| · 64|s| ⋯ 4^{|s|} · |s|

For the second claim, suppose s_{1}/s_{0} is an instance of some rule (r) and let d_{max} be a semi-derivation witnessing the maximum height of the premise s_{1}. Then the semi-derivation obtained from d_{max} by applying (r) to its end-sequent is a semiderivation of s_{0} with greater height. ⊣

5. Cut-elimination for GLS

Theorem 2 (Cut-elimination for GLS). The cut rule is eliminable from GLS.

Proof. Without loss of generality, it suffices to eliminate cut from a derivation concluding with the cut-rule with cut-free left premise X ⇒ Y, A and cut-free right premise A, U ⇒ V. We proceed via primary induction (PI) on the size of the cut-formula and secondary induction (SI) on the maximum height of the combined context mh(X, U ⇒ Y, V). Now, consider the last rule in each premise.

If X ⇒ Y, A is an instance of (id) because X ∩Y ≠ ∅, or A, U ⇒ V is an instance of (id) because U ∩ V ≠ ∅, then so is X, U ⇒ Y, V.

If X ⇒ Y, A is an instance of (id) because A ∈ X and A, U ⇒ V is an instance of (id) because A ∈ V, then so is X, U ⇒ Y, V.

If the cut-formula A is not principal in either premises of the the last rule, then the cut is shifted upwards following the usual Gentzen reductions. Of course, we need to verify that this does not increase the maximum height. To see that it does not, we illustrate with a generic binary rule (r). Suppose that the left premise of cut ends as below left, so A is not principal in this instance of (r):

\begin{aligned}X′ ⇒ Y′, A & X′′ ⇒ Y′′, A \\ & (r) \\ X ⇒ Y, A \end{aligned} \begin{aligned}X′, U ⇒ Y′, V & X′′, U ⇒ Y′′, V \\ & (r) \\ X, U ⇒ Y, V \end{aligned}

Consider the rule instance of (r) above right, which is what every one of Gentzen’s transformations will produce, with the proviso that the derivations of the two premises may now contain an instance of cut on A. Since the cut-formulae is still A, the size of the cut-formula has not changed. Moreover, from part two of Lemma 2, it follows that mh(X′, U ⇒ Y′, V) < mh(X, U ⇒ Y, V) and mh(X′′, U ⇒ Y′′, V) < mh(X, U ⇒ Y, V), which means that we can apply the SIH to the premises to obtain cut-free derivations of X′, U ⇒ Y′, V and X′′, U ⇒ Y′′, V. Apply (r) to these to obtain a cut-free derivation of X, U ⇒ Y, V, as shown above right.

If the cut-formula A is principal in both premises by propositional rules then the usual Gentzen reductions suffice, since the new cuts are on smaller formulae and hence the primary induction hypothesis applies. For example the derivation below containing a cut on A = B ∧ C

\begin{matrix}\begin{matrix}X ⇒ Y, B & X ⇒ Y, C \\ X ⇒ Y, B ∧ C \end{matrix} & \begin{matrix}B, C, U ⇒ V \\ B ∧ C, U ⇒ V \end{matrix} \\ X, U ⇒ Y, V \end{matrix}

can be transformed to the following containing a cut on the smaller formula B:

X ⇒ Y, B  \begin{aligned}X ⇒ Y, C & B, C, U ⇒ V \\ & (cut) \\ B, X, U ⇒ Y, V \end{aligned} (cut) X, X, U ⇒ Y, Y, V Contraction Lemma 1 X, U ⇒ Y, V

which falls under the PIH, giving a cut-free derivation of X, U ⇒ Y, V. Finally consider when the cut-formula A = □B is principal in both premises:

\begin{aligned}□X, X, □B ⇒ B \\ & (GLR) \\ L, □X ⇒ □B, M \end{aligned} □B, B, □U, U, □C ⇒ C ; (GLR) ; R, □B, □U ⇒ □C, S (cut) L, R, □X, □U ⇒ □C, M, S

The two (GLR) rule premises give an instance of cut with a smaller cut-formula B. The PIH gives a cut-free derivation of □X, X, □B, □B, □U, U, □C ⇒ C, and hence by contraction admissibility, a cut-free derivation of □X, X, □B, □U, U, □C ⇒ C.

But observe that the left premise can also be derived without weakening in L and M as shown below left, and that php-contraction on □X, X, □X, □U, U, □C ⇒ C gives L, R, □X, □U ⇒ □C, M, S via (GLR) as shown below right:

□X, X, □B ⇒ B ; (GLR) ; □X ⇒ □B □X, X, □X, □U, U, □C ⇒ C php-ctr (Lem 1) □X, X, □U, U, □C ⇒ C (GLR) L, R, □X, □U ⇒ □C, M, S

So mh(□X, X, □X, □U, U, □C ⇒ C) < mh(L, R, □X, □U ⇒ □C, M, S). Applying SIH to □X, X, □B, □U, U, □C ⇒ C and □X ⇒ □B we get a cut-free derivation of □X, X, □X, □U, U, □C ⇒ C. By contraction admissibility there is a cut-free derivation of □X, X, □U, U, □C ⇒ C. Applying (GLR) we get a cut-free derivation of L, R, □X, □U ⇒ □C, M, S. ⊣

6. Cut elimination for GoS

If we try to apply directly to GoS the cut-elimination argument for GLS, we encounter the following obstacle in the case when □ is principal in both premises and we apply the PIH using the premises of each (GoS) rule:

□X, X, □(B → □B) ⇒ B  □B, B, □U, U, □(C → □C) ⇒ C PIH □X, X, □(B → □B), □B, □U, U, □(C → □C) ⇒ C

The issue is the occurrence of □(B → □B) in the antecedent that we did not

I don’t see the issue? encounter before. To resolve this, we will need a standard invertibility lemma.

Lemma 3. If X, A → B ⇒ Y is derivable in GoS, then so is X, B ⇒ Y.

Proof. Induction on the height of the derivation of X, A → B ⇒ Y. ⊣

The following lemma shows that the occurrence of □(B → □B) can be removed.

This effectively says that GoR reduces to GLR! That is, every GoS derivation can be transformed into a GLS derivation. Now apply the previous cut-elimination result and then undo the GLS rules into GoR rules!

Lemma 4. If X, □(C → □C) ⇒ Y is derivable in GoS, then so is X, □C ⇒ Y.

Induction on the height of the given derivation.

Base case: If X ∩ Y ≠ ∅ then X, □C ⇒ Y is the required derivation. Otherwise, Y = Y′ ∪ □(C → □C), so use the following derivation of X, □C ⇒ Y, where X = □X_{1} ∪ U with U non-boxed:

□C ⇒ □C (w) C, □X_{1}, □C, C, □((C → □C) → □(C → □C)) ⇒ □C (→R) □X_{1}, X_{1}, □C, C, □((C → □C) → □(C → □C)) ⇒ C → □C (GoR) □X_{1}, U, □C ⇒ □(C → □C), Y′

Suppose that the last rule is (GoR) with X = U ∪ □X_{1} and Y = {□B} ∪ V:

□X_{1}, X_{1}, □(C → □C), C → □C, □(B → □B) ⇒ B (GoR) U, □(C → □C), □X_{1} ⇒ □B, V

By IH on the premise, we obtain □X_{1}, X_{1}, □C, C → □C, □(B → □B) ⇒ B. Furthermore, by invertibility of (→l) we get □X_{1}, X_{1}, □C, □C, □(B → □B) ⇒ B. By contraction and weakening admissibility we get □X_{1}, X_{1}, □C, C, □(B → □B) ⇒ B. Now apply (GoR) to get U, □X_{1}, □C ⇒ □B, V, which is X, □C ⇒ Y.

Suppose the last rule is some other generic (binary) rule below.

X′, □(C → □C) ⇒ Y′  X′′, □(C → □C) ⇒ Y′′ (r) X, □(C → □C) ⇒ Y

Then proceed as follows

X′, □(C → □C) ⇒ Y′ ; IH ; X′, □C ⇒ Y′  X′′, □(C → □C) ⇒ Y′′ ; IH ; X′′, □C ⇒ Y′′ (r) X, □C ⇒ Y

Theorem 3 (Cut-elimination for GoS). The cut rule is eliminable from GoS.

Proof. Once again, without loss of generality, it suffices to eliminate cut from a derivation concluding with the cut-rule with cut-free left premise X ⇒ Y, A and cutfree right premise A, U ⇒ V. Primary induction on the size of the cut-formula and secondary induction on the maximum height of the combined contexts mh(X, U ⇒ Y, V). The proof is identical to that of Theorem 2 except the following case.

Consider the case when the cut formula □B is principal in both premises.

\begin{matrix}□X, X, □(B → □B) ⇒ B ; (GoR) ; L, □X ⇒ □B, M & □B, B, □U, U, □(C → □C) ⇒ C ; (GoR) ; R, □B, □U ⇒ □C, S \\ L, R, □X, □U ⇒ □C, M, S \end{matrix}

By PIH using the premises of each (GoR) rule, we obtain a cut-free derivation of □X, X, □(B → □B), □B, □U, U, □(C → □C) ⇒ C. By Lemma 4 we have a cutfree derivation of □X, X, □B, □B, □U, U, □(C → □C) ⇒ C. Hence by contraction admissibility, a cut-free derivation of □X, X, □B, □U, U, □(C → □C) ⇒ C.

Observe that

□X, X, □X, □U, U, □(C → □C) ⇒ C php contraction (Lem. 1) □X, X, □U, U, □(C → □C) ⇒ C (GoR) L, R□X, □U ⇒ □C, M, S

So mh(□X, X, □X, □U, U, □(C → □C) ⇒ C) < mh(L, R, □X, □U ⇒ □C, M, S). Applying SIH to □X, X, □B, □U, U, □(C → □C) ⇒ C and □X ⇒ □B we get a cut-free derivation of □X, X, □X, □U, U, □(C → □C) ⇒ C. By contraction admissibility there is a cut-free derivation of □X, X, □U, U, □(C → □C) ⇒ C. Applying (GoR) we get a cut-free derivation of □X, □U ⇒ □C. ⊣

References

   E-mail address: revantha@logic.at

Tuesday 19^{th} February, 2019. 12:04