Apr 3, 2018 - We present a sequent calculus for the weak Grzegorczyk logic Go allowing ... sequent calculus allowing non-well-founded proofs Goâ and...

0 downloads 0 Views 212KB Size

Cut Elimination for Weak Modal Grzegorczyk Logic via Non-Well-Founded Proofs Yury Savateev 1 National Research University Higher School of Economics

Daniyar Shamkanov Steklov Mathematical Institute of the Russian Academy of Sciences National Research University Higher School of Economics

Abstract We present a sequent calculus for the weak Grzegorczyk logic Go allowing non-wellfounded proofs and obtain the cut-elimination theorem for it by constructing a continuous cut-elimination mapping acting on these proofs. Keywords: non-well-founded proofs, weak Grzegorczyk logic, logic Go, cut-elimination, cyclic proofs.

1

Introduction

The logic Go, also known as the weak Grzegorzyk logic, is the smallest normal modal logic containing the axiom K and the axioms ◻A → ◻ ◻ A and ◻(◻(A → ◻A) → A) → ◻A. A survey of results on Go can be found in [5]. The logic is sound and complete with respect to the class of transitive frames with no proper clusters and infinite ascending chains [2], and it is a proper sublogic of both G¨ odel-L¨ob logic GL (also known as provability logic) and Grzegorzyk logic Grz. Recently a new proof-theoretic presentation for the logic GL in the form of a sequent calculus allowing non-well-founded proofs was given in [10,4]. Later, the same ideas were applied to the modal Grzegorczyk logic Grz in [8,7], where it allowed to prove several proof-theoretic properties of this logic syntactically. In this paper we use the same approach for the logic Go. We consider a sequent calculus allowing non-well-founded proofs Go∞ and present the cutelimination theorem for it. We consider the set of non-well-founded proofs of Go∞ and various sets of operations acting on theses proofs as ultrametric spaces and define our cut-elimination operator using the Prieß-Crampe fixedpoint theorem (see [6]), which is a strengthening of the Banach’s theorem. 1

This work is supported by the Russian Foundation for Basic Research, grant 15-01-09218a.

2

Cut Elimination for Weak Modal Grzegorczyk Logic via Non-Well-Founded Proofs

In [3] Gor´e and Ramanayake remark that their method for cut elimination for the logic Go is more complex than the similar methods for the logics GL and Grz. This difference in complexity seems to be present in our approach as well. The proofs of cut-elimination for Go∞ and Grz∞ turn out to be almost the same, but the system Go∞ itself seems to be more complex (it includes rules of arbitrary arity, where Grz∞ has at most binary) and the translation from Go∞ to the standart system seems to require bigger induction measure.

2

Preliminaries

In this section we recall the weak Grzegorczyk logic Go and define an ordinary sequent calculus for it. Formulas of Go, denoted by A, B, C, are built up as follows: A ∶∶= ∣ p ∣ (A → A) ∣ ◻ A , where p stands for atomic propositions. The Hilbert-style axiomatization of Go is given by the following axioms and inference rules: Axioms: (i) Boolean tautologies; (ii) ◻(A → B) → (◻A → ◻B); (iii) ◻A → ◻ ◻ A; (iv) ◻(◻(A → ◻A) → A) → ◻A. Rules: modus ponens, A/ ◻ A. Now we define an ordinary sequent calculus for Go. A sequent is an expression of the form Γ ⇒ ∆, where Γ and ∆ are finite multisets of formulas. For a multiset of formulas Γ = A1 , . . . , An , we set ◻Γ ∶= ◻A1 , . . . , ◻An . The system GrzSeq , is defined by the following initial sequents and inference rules: Γ, A ⇒ A, ∆ , →L

Γ, B ⇒ ∆ Γ ⇒ A, ∆ , Γ, A → B ⇒ ∆

◻Go

◻Π, Π, ◻(A → ◻A) ⇒ A . Γ, ◻Π ⇒ ◻A, ∆

Γ, ⇒ ∆ , →R

Γ, A ⇒ B, ∆ , Γ ⇒ A → B, ∆

Fig. 1. The system GoSeq The cut rule has the form Γ ⇒ A, ∆ Γ, A ⇒ ∆ , Γ⇒∆ where A is called the cut formula of the given inference. cut

Savateev and Shamkanov

3

Lemma 2.1 GoSeq + cut ⊢ Γ ⇒ ∆ if and only if Go ⊢ ⋀ Γ → ⋁ ∆. ◻

Proof. Standard transformations of proofs. Theorem 2.2 If GoSeq + cut ⊢ Γ ⇒ ∆, then GoSeq ⊢ Γ ⇒ ∆.

A syntactic cut-elimination for Go was obtained by R. Gor´e and R. Ramanayake in [3]. In this paper, we will give another proof of this cut-elimination theorem.

3

Non-well-founded proofs

Now we define a sequent calculus for Go allowing non-well-founded proofs. Inference rules and initial sequents of the sequent calculus Go∞ have the following form: Γ, p ⇒ p, ∆ , Γ, ⇒ ∆ , →L

Γ, B ⇒ ∆ Γ ⇒ A, ∆ , Γ, A → B ⇒ ∆

→R

Γ, A ⇒ B, ∆ , Γ ⇒ A → B, ∆

◻Π, Π ⇒ A1 , . . . , An , ◻A1 , . . . ◻ An ◻Π, Π ⇒ A1 Γ, ◻Π ⇒ ◻A1 , . . . , ◻An , ∆

...

◻Π, Π ⇒ An

Fig. 2. The system Go∞ The system Go∞ +cut is defined by adding the rule (cut) to the system Go∞ . The will refer to all but the leftmost premises of the rule (◻) as ”right”. An ∞–proof in Go∞ (Go∞ +cut) is a (possibly infinite) tree whose nodes are marked by sequents and whose leaves are marked by initial sequents and that is constructed according to the rules of the sequent calculus. In addition, every infinite branch in an ∞–proof must pass through a right premise of the rule (◻) infinitely many times. A sequent Γ ⇒ ∆ is provable in Go∞ (Go∞ + cut) if there is an ∞–proof in Go∞ (Go∞ + cut) with the root marked by Γ ⇒ ∆. For a multiset of formulas Γ = A1 , . . . , An , we set ⊠Γ ∶= A1 , . . . , An , ◻A1 , . . . , ◻An . Then the rule (◻) can be written as ⊠Π ⇒ ⊠(A1 , . . . , An ) ⊠Π ⇒ A1 ... Γ, ◻Π ⇒ ◻A1 , . . . , ◻An , ∆

⊠Π ⇒ An

.

Let us construct an ∞–proof of the sequent ◻(◻(p → ◻p) → p) ⇒ ◻p. Let F = ◻(p → ◻p) → p and let ψ be the following proof:

→R

Ax ⊠F, p ⇒ p, ◻p, ◻p, ◻(p → ◻p) . ⊠F ⇒ ⊠(p, p → ◻p)

Let φ be the following proof part:

4

Cut Elimination for Weak Modal Grzegorczyk Logic via Non-Well-Founded Proofs

→L

(1) (2) F, p, ◻F ⇒ ◻p →R ⊠F ⇒ p → ◻p ⊠F ⇒p ψ Ax ◻ ◻F ⇒ ◻(p → ◻p), ◻p, p ◻F, p ⇒ p, ◻p ◻F, ◻(p → ◻p) → p ⇒ p, ◻p

Let ξ be the following proof part: (1) (2) F, p, ◻F ⇒ ◻p →R ψ ⊠F ⇒ p → ◻p ⊠F ⇒ p ◻ p, ⊠F ⇒ ◻p, ◻(p → ◻p) →R ⊠F ⇒ ⊠(p → ◻p) Let θ be the following proof part: (2) F, p, ◻F ⇒ ◻p →R ⊠F ⇒ ⊠(p → ◻p) ⊠F ⇒ p → ◻p Ax ◻ ◻F ⇒ ◻(p → ◻p), p ◻F, p ⇒ p ◻F, ◻(p → ◻p) → p ⇒ p (1)

→L

An ∞–proof of the sequent ◻(◻(p → ◻p) → p) ⇒ ◻p can be constructed as follows: ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ φ θ ◻ ⋮ F, p, ◻F ⇒ ◻p θ φ θ φ θ . ◻ ◻ F, p, ◻F ⇒ ◻p θ ξ F, p, ◻F ⇒ ◻p φ θ . ◻ ◻(◻(p → ◻p) → p) ⇒ ◻p The n-fragment of an ∞–proof is a finite tree obtained from the ∞–proof by cutting every branch at the nth from the root right premise of a ◻-rule. The 1-fragment of an ∞–proof is also called its main fragment. The local height ∣π∣ of an ∞–proof π is the length of the longest branch in its main fragment. An ∞–proof only consisting of an initial sequent has height 0. The local height of the ∞–proof constructed for the sequent ◻(◻(p → ◻p) → p) ⇒ ◻p equals to 4 and its main fragment has the form ◻F, p ⇒ p, ◻p, ◻p, ◻(p → ◻p) ◻F ⇒ p, p → ◻p, ◻p, ◻(p → ◻p) ◻ ◻F ⇒ ◻(p → ◻p), ◻p, p ◻F, p ⇒ p, ◻p ◻F, ◻(p → ◻p) → p ⇒ p, ◻p ◻ ◻(◻(p → ◻p) → p) ⇒ ◻p →R

→L

.

Savateev and Shamkanov

5

We denote the set of all ∞-proofs in the system Go∞ + cut by P. For π, τ ∈ P, we write π ∼n τ if n-fragments of these ∞-proofs coincide. For any π, τ ∈ P, we also set π ∼0 τ . For every ∞-proof π ∈ P one of the following holds: (i) π consists of a single initial sequent. (ii) π has the form →R

π0 Γ, A ⇒ B, ∆ Γ ⇒ A → B, ∆

with ∣π0 ∣ < ∣π∣. We denote this by π = →R(A→B) (π0 ). (iii) π has the form →L

π0 π1 Γ, B ⇒ ∆ Γ ⇒ A, ∆ Γ, A → B ⇒ ∆

with ∣π0 ∣, ∣π1 ∣ < ∣π∣. We denote this by π = →L(A→B) (π0 , π1 ). (iv) π has the form cut

Γ ⇒ A, ∆ Γ, A ⇒ ∆ , Γ⇒∆

with ∣π0 ∣, ∣π1 ∣ < ∣π∣. We denote this by π = cutA (π0 , π1 ). (v) π has the form ⊠Π ⇒ ⊠(A1 , . . . , An ) ⊠Π ⇒ A1 ... Γ, ◻Π ⇒ ◻A1 , . . . , ◻An , ∆

⊠Π ⇒ An

.

with ∣π0 ∣ < ∣π∣. We denote this by π = ◻Γ;∆ (π0 , π1 , . . . , πn ). Now we define two translations that connect ordinary and non-well-founded sequent calculi for the logic Go. Lemma 3.1 We have Go∞ ⊢ Γ, A ⇒ A, ∆ for any sequent Γ ⇒ ∆ and any formula A. Proof. Standard induction on the structure of A.

◻

Lemma 3.2 We have Go∞ ⊢ ◻(◻(A → ◻A) → A) ⇒ ◻A for any formula A. Proof. Consider an example of ∞–proof for the sequent ◻(◻(p → ◻p) → p) ⇒ ◻p given above. We transform this example into an ∞–proof for ◻(◻(A → ◻A) → A) ⇒ A by replacing p with A and adding required ∞–proofs instead ◻ of initial sequents using Lemma 3.1. Recall that an inference rule is called admissible (in a given proof system) if, for any instance of the rule, the conclusion is provable whenever all premises are provable. Lemma 3.3 The rule wk

Γ⇒∆ Π, Γ ⇒ ∆, Σ

6

Cut Elimination for Weak Modal Grzegorczyk Logic via Non-Well-Founded Proofs

is admissible in the systems GoSeq and Go∞ + cut. The rule Γ, Π, Π ⇒ ∆ ctr Γ, Π ⇒ ∆ is admissible in the system GoSeq . Proof. Standard induction on the structure (local height) of a proof of Γ ⇒ ∆. ◻ Theorem 3.4 If GoSeq + cut ⊢ Γ ⇒ ∆, then Go∞ + cut ⊢ Γ ⇒ ∆. Proof. Assume π is a proof of Γ ⇒ ∆ in GoSeq + cut. By induction on the size of π we prove Go∞ + cut ⊢ Γ ⇒ ∆. If Γ ⇒ ∆ is an initial sequent of GoSeq + cut, then it is provable in Go∞ + cut by Lemma 3.1. Otherwise, consider the last application of an inference rule in π. The only non-trivial case is when the proof π has the form

◻Go

π′ ◻Π, Π, ◻(A → ◻A) ⇒ A , Σ, ◻Π ⇒ ◻A, Λ

where Σ, ◻Π = Γ and ◻A, Λ = ∆. By the induction hypothesis there is an ∞–proof ξ of ⊠Π, ◻(A → ◻A) ⇒ A in Go∞ + cut. The required ∞–proof for Σ, ◻Π ⇒ ◻A, ∆ has the form:

→R

ξ ⊠Π, ◻(A → ◻A) ⇒ A χ ξ ⊠Π ⇒ F →R wk ◻F ⇒ ◻A ⊠Π ⇒ ⊠F ⊠Π ⇒ F ◻ wk Σ, ◻Π ⇒ ◻F, ◻A, Λ Σ, ◻Π, ◻F ⇒ ◻A, Λ cut Σ, ◻Π ⇒ ◻A, Λ

where F = ◻(A → ◻A) → A and χ is an ∞–proof of ◻F ⇒ ◻A, which exists by Lemma 3.2. The cases of other inference rules being last in π are straightforward, so we omit them. ◻ For a sequent Γ ⇒ ∆, let Sub(Γ ⇒ ∆) be the set of all subformulas of the formulas from Γ ∪ ∆. For a finite set of formulas Λ, let Λ∗ be the set {A → ◻A ∣ A ∈ Λ}. Lemma 3.5 If Go∞ ⊢ Γ ⇒ ∆, then GoSeq ⊢ ◻(Λ∗1 ), Λ∗2 , ⊠Ω, Γ ⇒ ∆ for any finite sets of formulas Λ1 , Λ2 , and Ω such that Λ2 ⊂ Λ1 . Proof. Assume π is an ∞–proof of the sequent Γ ⇒ ∆ in Go∞ and Λ1 , Λ2 , and Ω are finite sets of formulas, such that Λ2 ⊂ Λ1 . We prove that GoSeq ⊢ ◻(Λ∗1 ), Λ∗2 , ⊠Ω, Γ ⇒ ∆ by quadruple induction: by induction on the number of elements in the finite set Sub(Γ ⇒ ∆)/Λ1 with a

Savateev and Shamkanov

7

subinduction on on the number of elements in the finite set Sub(Γ ⇒ ∆)/Λ2 , subinduction on the number of elements in the finite set Sub(Γ ⇒ ∆)/Ω, and with subinduction on ∣π∣. If ∣π∣ = 0, then Γ ⇒ ∆ is an initial sequent. We see that the sequent ◻(Λ∗1 ), Λ∗2 , ⊠Ω, Γ ⇒ ∆ is an initial sequent and it is provable in GoSeq . Otherwise, consider the last application of an inference rule in π. Case 1. Suppose that π = →R(A→B) (π0 ). Notice that ∣π0 ∣ < ∣π∣. By the induction hypothesis for Λ2 , Λ1 , Ω, and π0 , the sequent ◻(Λ∗1 ), Λ∗2 , ⊠Ω, Γ, A ⇒ B, Σ, where A → B, Σ = ∆, is provable in GoSeq . Applying the rule (→R ) to it, we obtain that the sequent ◻(Λ∗1 ), Λ∗2 , ⊠Ω, Γ ⇒ ∆ is provable in GoSeq . Case 2. Suppose that π = →L(A→B) (π0 , π1 ) We see that ∣π0 ∣ < ∣π∣. By the induction hypothesis for Λ2 , Λ1 , Ω, and π0 , the sequent ◻(Λ∗1 ), Λ∗2 , ⊠Ω, Σ, B ⇒ ∆, where Σ, A → B = Γ, is provable in GoSeq . Analogously, we have GrzSeq ⊢ ◻(Λ∗1 ), Λ∗2 , ⊠Ω, Σ ⇒ A, ∆. Applying the rule (→L ), we obtain that the sequent ◻(Λ∗1 ), Λ∗2 , ⊠Ω, Γ ⇒ ∆ is provable in GoSeq . Case 3. Suppose that π has the form π0 π1 ⊠Π ⇒ ⊠(A1 , . . . , An ) ⊠Π ⇒ A1 ... Φ, ◻Π ⇒ ◻A1 , . . . , ◻An , Σ

πn ⊠Π ⇒ An

where Φ, ◻Π = Γ and ◻A1 , . . . , ◻An , Σ = ∆. Subcase 3.1: For some i, we have Ai ∉ Λ1 . We have that the number of elements in Sub(◻Π, Π ⇒ A)/(Λ1 ∪ {Ai }) is strictly less than the number of elements in Sub(Φ, ◻Π ⇒ ◻A1 , . . . , ◻An , Σ)/Λ1 . By the induction hypothesis for Λ1 ∪ {Ai }, Λ1 , ∅ and πi , the sequent ◻(Λ∗1 ), ◻(Ai → ◻Ai ), Λ∗1 , ◻Π, Π ⇒ A is provable in GoSeq . Then we have ◻Go

◻(Λ∗1 ), ◻(Ai → ◻Ai ), Λ∗1 , ◻Π, Π ⇒ Ai ∗ Λ2 , ◻(Λ∗1 ), ⊠Ω, Φ, ◻Π ⇒ ◻A1 , . . . , ◻Ai , . . . , ◻An , Σ

.

Subcase 3.2: For all i, we have Ai ∈ Λ1 , but there is i, such that Ai ∉ Λ2 . We have that the number of elements in Sub(◻Π, Π ⇒ Ai )/Λ1 is strictly less than the number of elements in Sub(Φ, ◻Π ⇒ ◻A1 , . . . , ◻An , Σ)/Λ2 . By the induction hypothesis for Λ1 , Λ1 , ∅ and πi , the sequent ◻(Λ∗1 ), Λ∗1 , ◻Π, Π ⇒ Ai is provable in GoSeq . Then we have ◻(Λ∗1 ), Λ∗1 , ◻Π, Π ⇒ Ai ◻(Λ∗1 ), Λ∗1 , ◻Π, Π, ◻(Ai → ◻Ai ) ⇒ Ai . ∗ Λ2 , ◻(Λ∗1 ), ⊠Ω, Φ, ◻Π ⇒ ◻A1 , . . . , ◻Ai , . . . , ◻An , Σ

weak ◻Go

Subcase 3.3: For all i, we have Ai ∈ Λ2 ⊂ Λ1 , but there is a formula F in Π, such that F ∉ Ω. We have that the number of elements in Sub(◻Π, Π ⇒ A1 )/(Ω ∪ Π) is strictly less than the number of elements in Sub(Φ, ◻Π ⇒ ◻A1 , . . . , ◻An , Σ)/Ω. By the induction hypothesis for Λ1 , Λ1 , Ω ∪ Π and π1 , the sequent ◻(Λ∗1 ), Λ∗1 , ⊠Ω, ⊠(Π/Ω), ⊠Π ⇒ A1 is provable in

8

Cut Elimination for Weak Modal Grzegorczyk Logic via Non-Well-Founded Proofs

GoSeq . Then we have weak

◻Go ctr

◻(Λ∗1 ), Λ∗1 , ⊠Ω, ⊠(Π/Ω), ⊠Π ⇒ A1 ∗ ◻(Λ1 ), Λ∗1 , ⊠Ω, ⊠(Π/Ω), ⊠Π, ◻(A → ◻A)

⇒ A1 ∗ ∗ Λ2 , ◻(Λ1 ), ◻Ω, Ω, Φ, ◻(Π/Ω), ◻(Π/Ω), ◻(Π ∩ Ω) ⇒ ◻A1 , . . . , ◻An , Σ Λ∗2 , ◻(Λ∗1 ), ⊠Ω, Φ, ◻Π ⇒ ◻A1 , . . . , ◻An , Σ

.

Subcase 3.4: For all i, we have Ai ∈ Λ2 ⊂ Λ1 and Π ⊂ Ω. We see that ∣π0 ∣ < ∣π∣. By the induction hypothesis for Λ1 , Λ2 , Ω and π0 the sequent ◻(Λ∗1 ), Λ∗2 , ⊠Ω, ⊠Π ⇒ ⊠(A1 , . . . , An ) is provable in GoSeq . Let Ψ = ◻(Λ∗1 ), Λ∗2 , ⊠Ω. Then we have Ax Ψ, ⊠Π, ◻A1 ⇒ ⊠(A1 , . . . , An ) Ψ, ⊠Π ⇒ ⊠(A1 , . . . , An ) →L ◻(Λ∗1 ), Λ∗2 , A1 → ◻A1 , ⊠Ω, ⊠Π ⇒ ◻A1 , ⊠(A2 , . . . , An ) ctr ◻(Λ∗1 ), Λ∗2 , ⊠Ω, ⊠Π ⇒ ◻A1 , ⊠(A2 , . . . , An ) ⋮ ∗ ∗ ◻(Λ1 ), Λ2 , An → ◻An , ⊠Ω, ⊠Π ⇒ ◻A1 , . . . , ◻An ctr ◻(Λ∗1 ), Λ∗2 , ◻Ω, Ω/Π, Π, ◻Π, Π ⇒ ◻A1 , . . . , ◻An ctr ◻(Λ∗1 ), Λ∗2 , ⊠Ω, ◻Π ⇒ ◻A1 , . . . , ◻An . weak ◻(Λ∗1 ), Λ∗2 , ⊠Ω, Φ, ◻Π ⇒ ◻A1 , . . . , ◻An , Σ ◻ From Lemma 3.5 we immediately obtain the following theorem. Theorem 3.6 If Go∞ ⊢ Γ ⇒ ∆, then GoSeq ⊢ Γ ⇒ ∆.

4

Ultrametric spaces

In this section we define ultrametrics on some spaces concerning ∞-proofs. For some basic notions of the theory of ultrametric spaces (cf. [9]) and proofs please see Appendix. Consider the set P of all ∞-proofs of the system Go∞ + cut. An ultrametric dP ∶ P × P → [0, 1] on P is defined by dP (π, τ ) = inf{

1 ∣ π ∼n τ }. 2n

Proposition 4.1 (P, dP ) is a (spherically) complete ultrametric space. For m ∈ N, let Fm denote the set of all non-expansive functions from P m to P. For a, b ∈ Fm , we write a ∼n,k b if a(π) ∼n b(π) for any π ∈ P m and, in 2 An ultrametric lm on Fm is addition, a(π) ∼n+1 b(π) whenever Σm i=1 ∣πi ∣ < k. defined by 1 1 1 lm (a, b) = inf{ n + n+k ∣ a ∼n,k b}. 2 2 2 2

This definition is inspired by [1, Subsection 2.1].

Savateev and Shamkanov

9

Proposition 4.2 (Fm , lm ) is a spherically complete ultrametric space. Notice that any operator U∶ Fm → Fm is strictly contractive if and only if for any a, b ∈ Fm , and any n, k ∈ N we have a ∼n,k b ⇒ U(a) ∼n,k+1 U(b). Now we state a generalization of the Banach’s fixed-point theorem for ultrametric spaces that will be used in the next sections. Theorem 4.3 (Prieß-Crampe [6]) Let (M, d) be a non-empty spherically complete ultrametric space. Then every strictly contractive mapping f ∶ M → M has a unique fixed-point.

5

Admissible Rules and Mappings

In this section, for the system Go∞ + cut, we state admissibility of auxiliary inference rules, which will be used in the proof of the cut-elimination theorem. Recall that the set P of all ∞-proofs of the system Go∞ + cut can be considered as an ultrametric space with the metric dP . By Pn we denote the set of all ∞-proofs that do not contain applications of the cut rule in their n-fragments. We also set P0 = P. A mapping u ∶ P m → P is called adequate if for any n ∈ N we have u(π1 , . . . , πn ) ∈ Pn , whenever πi ∈ Pn for all i ⩽ n. In Go∞ + cut, we call a single-premise inference rule strongly admissible if there is a non-expansive adequate mapping u∶ P → P that maps any ∞-proof of the premise of the rule to an ∞-proof of the conclusion. The mapping u must also satisfy one additional condition: ∣u(π)∣ ⩽ ∣π∣ for any π ∈ P. In the following lemmata, non-expansive mappings are defined in a standard way by induction on the local heights of ∞-proofs for the premises. So we omit further details. Lemma 5.1 For any finite multisets of formulas Π and Σ, the inference rule wkΠ;Σ

Γ⇒∆ Π, Γ ⇒ ∆, Σ

is strongly admissible in Go∞ + cut. Lemma 5.2 For any formulas A and B, the rules liA→B

Γ, A → B ⇒ ∆ Γ, B ⇒ ∆

iA→B

Γ ⇒ A → B, ∆ Γ, A ⇒ B, ∆

riA→B

i

Γ, A → B ⇒ ∆ Γ ⇒ A, ∆ Γ ⇒ , ∆ Γ⇒∆

are strongly admissible in Go∞ + cut. Lemma 5.3 For any atomic proposition p, the rules aclp

Γ, p, p ⇒ ∆ Γ, p ⇒ ∆

acrp Γ ⇒ p, p, ∆ Γ ⇒ p, ∆

10

Cut Elimination for Weak Modal Grzegorczyk Logic via Non-Well-Founded Proofs

are strongly admissible in Go∞ + cut. Let us also define the mapping clip∶ P → P. Consider an ∞-proof π. If the last rule application in π is not of the rule (◻) then we put clip(π) = π. If the ∞-proof π has the form π0 π1 πn ⊠Π ⇒ ⊠(A1 , . . . , An ) ⊠Π ⇒ A1 ... ⊠Π ⇒ An Γ, ◻Π ⇒ ◻A1 , . . . , ◻An , ∆ we define clip(π) = π to be π0 π1 ⊠Π ⇒ ⊠(A1 , . . . , An ) ⊠Π ⇒ A1 ... ◻Π ⇒ ◻A1 , . . . , ◻An

πn ⊠Π ⇒ An

.

Clearly this mapping is non-expansive, adequate, and ∣clip(π)∣ ⩽ ∣π∣ for any π ∈ P.

6

Cut elimination

In this section, we construct a continuous function from P to P, which maps any ∞-proof of the system Go∞ +cut to a cut-free ∞-proof of the same sequent. Let us call a pair of ∞-proofs (π, τ ) a cut pair if π is an ∞-proof of the sequent Γ ⇒ ∆, A and τ is an ∞-proof of the sequent A, Γ ⇒ ∆ for some Γ, ∆, and A. For a cut pair (π, τ ), we call the sequent Γ ⇒ ∆ its cut result and the formula A its cut formula. For a modal formula A, a non-expansive mapping u from P × P to P is called A-removing if it maps every cut pair (π, τ ) with the cut formula A to an ∞-proof of its cut result. By RA , let us denote the set of all A-removing mappings. Lemma 6.1 For each formula A, the pair (RA , l2 ) is a non-empty spherically complete ultrametric space. Proof. The proof of spherical completeness of the space (RA , l2 ) is analoguos to the proof of the spherical completeness of (Fm , Lm ). We only need to check that the set RA is non-empty. Consider the mapping ucut ∶ P 2 → P that is defined as follows. For a cut pair (π, τ ) with the cut formula A, it joins the ∞-proofs π and τ with an appropriate instance of the rule (cut). For all other pairs, the mapping ucut returns the first argument. Clearly, ucut is non-expansive and therefore lies in RA . ◻ In what follows, we use nonexpansive adequate mappings wkΠ;Σ , liA→B , riA→B , iA→B , i , aclp , acrp from Lemma 5.1, Lemma 5.2, and Lemma 5.3. Lemma 6.2 For any atomic proposition p, there exists an adequate p-removing mapping rep . Proof. Assume we have two ∞-proofs π and τ . If the pair (π, τ ) is not a cut pair or is a cut pair with the cut formula being not p, then we put rep (π, τ ) = π.

Savateev and Shamkanov

11

Otherwise, we define rep (π, τ ) by induction on ∣π∣. Let the cut result of the pair (π, τ ) be Γ ⇒ ∆. If ∣π∣ = 0, then Γ ⇒ ∆, p is an initial sequent. Suppose that Γ ⇒ ∆ is also an initial sequent. Then rep (π, τ ) is defined as the ∞-proof consisting only of the sequent Γ ⇒ ∆. If Γ ⇒ ∆ is not an initial sequent, then Γ has the form p, Φ, and τ is an ∞-proof of the sequent p, p, Φ ⇒ ∆. Applying the non-expansive adequate mapping aclp from Lemma 5.3, we put rep (π, τ ) ∶= aclp (τ ). Now suppose that ∣π∣ > 0. We define rep (π, τ ) according to the last application of an inference rule in π:

(→R(B→C) (π0 ), τ ) z→

rep (π0 , iB→C (τ )) Γ, B ⇒ C, Σ , →R Γ ⇒ B → C, Σ

(→L(B→C) (π0 , π1 ), τ ) z→

rep (π0 , liB→C (τ )) rep (π1 , riB→C (τ )) Σ, C ⇒ ∆ Σ ⇒ B, ∆ , Σ, B → C ⇒ ∆

(cutB (π0 , π1 ), τ ) z→

rep (π0 , wk∅;B (τ )) rep (π1 , wkB;∅ (τ )) Γ ⇒ B, ∆ Γ, B ⇒ ∆ , cut Γ⇒∆

(◻Φ;Σ,p (π0 , π1 , . . . , πn ), τ ) z→ ◻Φ;Σ (π0 , π1 , . . . , πn )

The mapping rep is well defined, adequate and non-expansive.

◻

Lemma 6.3 Given an adequate B-removing mapping reB , there exists an adequate ◻B-removing mapping re◻B . Proof. Assume we have an adequate B-removing mapping reB . The required ◻B-removing mapping re◻B is obtained as the fixed-point of a contractive operator G◻B ∶ R◻B → R◻B . For a mapping u ∈ R◻B and a pair of ∞-proofs (π, τ ), the ∞-proof G◻B (u)(π, τ ) is defined as follows. If (π, τ ) is not a cut pair or a cut pair with the cut formula being not ◻B, then we put G◻B (u)(π, τ ) = π. Now let (π, τ ) be a cut pair with the cut formula ◻B and the cut result Γ ⇒ ∆. If ∣π∣ = 0 or ∣τ ∣ = 0, then Γ ⇒ ∆ is an initial sequent. In this case, we define G◻B (u)(π, τ ) as the ∞-proof consisting only of the sequent Γ ⇒ ∆. Suppose that ∣π∣ > 0 and ∣τ ∣ > 0. We define G◻B (u)(π, τ ) according to the last application of an inference rule in π:

12

Cut Elimination for Weak Modal Grzegorczyk Logic via Non-Well-Founded Proofs

(→R(C→D) (π0 ), τ ) z→

→R

u(π0 , iC→D (τ )) Γ, C ⇒ D, Σ , Γ ⇒ C → D, Σ

(→L(C→D) (π0 , π1 ), τ ) z→

u(π0 , liC→D (τ )) u(π1 , riC→D (τ )) Σ, D ⇒ ∆ Σ ⇒ C, ∆ , →L Σ, C → D ⇒ ∆

(cutC (π0 , π1 ), τ ) z→

u(π0 , wk∅;C (τ )) u(π1 , wkC;∅ (τ )) Γ ⇒ C, ∆ Γ, C ⇒ ∆ , cut Γ⇒∆

(◻Φ;Σ,◻B (π0 , π1 , . . . , πn ), τ ) z→ ◻Φ;Σ (π0 , π1 , . . . , πn ) Consider the case when π has the form π0 πB π1 ⊠Π ⇒ ⊠(B, A1 , . . . , An ) ⊠Π ⇒ B ⊠Π ⇒ A1 ◻ Φ, ◻Π ⇒ ◻B, ◻A1 , . . . , ◻An , Σ

...

⊠Π ⇒ ⊠An

.

We define G◻B (u)(π, τ ) according to the last application of an inference rule in τ .

(π, →R(C→D) (τ0 )) z→

(π, →L(C→D) (τ0 , τ1 )) z→

(π, cutC (τ0 , τ1 )) z→

→R

u(iC→D (π), τ0 ) Γ, C ⇒ D, Σ , Γ ⇒ C → D, Σ

u(liC→D (π), τ0 ) u(riC→D (π1 ), τ1 ) Σ, D ⇒ ∆ Σ ⇒ C, ∆ , →L Σ, C → D ⇒ ∆ u(wk∅;C (π), τ0 ) u(wkC;∅ (π), τ1 ) Γ ⇒ C, ∆ Γ, C ⇒ ∆ , cut Γ⇒∆

(π, ◻Φ′ ,◻B;Σ′ (τ0 , τ1 , . . . , τk )) z→ ◻Φ′ ;Σ′ (τ0 , τ1 , . . . , τk ) It remains to consider the case when τ has the form τ0 τ1 ⊠Λ, ⊠B ⇒ ⊠(C1 , . . . , Ck ) ⊠Λ, ⊠B ⇒ C1 ... ◻ ′ Φ , ◻Λ, ◻B ⇒ ◻C1 , . . . , ◻Ck , Σ′

⊠Λ, ⊠B ⇒ ⊠Ck

.

Savateev and Shamkanov

13

Notice that the sequent Γ ⇒ ∆, the sequent Φ, ◻Π ⇒ ◻A1 , . . . , ◻An , Σ, and the sequent Φ′ , ◻Λ ⇒ ◻C1 , . . . , ◻Ck , Σ′ are the same. ′ Let I ∶= {i ∣ Ai ∉ C1 , . . . , Ck } and J ∶= {i ∣ Ci ∉ A1 , . . . , An }, let πB be the followind ∞-proof: wk∅,◻B (πB ) πB ⊠Π ⇒ ⊠B ⊠Π ⇒B , ◻ ⊠Π ⇒ ◻B and condsider the following ∞-proofs: ψ1 ∶= u(wkΛ/Π,◻Λ/Π;{⊠Ci }i∈J (π0 ), wkΠ∪Λ,◻(Π/Λ);{⊠Ai }i∈I ,{Ci } (clip(τ ))), ψ2 ∶= u(wkΠ∪Λ,◻Λ/Π;{⊠Ci }i∈J ,{Ai } (clip(π)), wkΠ/Λ,◻(Π/Λ);{⊠Ai }i∈I (τ0 )), ′ ), reB (wk⊠(Λ/Π,◻B;∅) (πB ), wk⊠(Π/Λ;∅) (τj ))). φj ∶= u(wk⊠(Λ/Π);Cj (πB

We define G◻B (u)(π, τ ) as

◻

reB (ψ1 , ψ2 ) ⊠(Π ∪ Λ) ⇒ ⊠Ai , {⊠Cj }j∈J

(wk⊠(Λ/Π) (πi ))

φj

(⊠(Π ∪ Λ) ⇒ Ai ) Γ⇒∆

(⊠(Π ∪ Λ) ⇒ Cj ))j∈J

Now the operator G◻B is well-defined. By the case analysis according to the definition of G◻B , we see that G◻B (u) is non-expansive and belongs to R◻B whenever u ∈ R◻B . We claim that G◻B is contractive. It sufficient to check that for any u, v ∈ R◻B and any n, k ∈ N we have u ∼n,k v ⇒ G◻B (u) ∼n,k+1 G◻B (v), which we prove by case analysis. Now we define the required ◻B-removing mapping re◻B as the fixed-point of the the operator G◻B ∶ R◻B → R◻B , which exists by Lemma 6.1 and Theorem 4.3. It remains to check that the mapping re◻B is adequate. For some n, k ∈ N, let us call a mapping u ∈ R◻B (n, k)-adequate if it satisfies the following two conditions: u(π, τ ) ∈ Pi for any i ⩽ n and any π, τ ∈ Pi ; u(π, τ ) ∈ Pn+1 whenever π, τ ∈ Pn+1 and ∣π∣ + ∣τ ∣ < k. By case analysis we establish that G◻B (u) is (n, k + 1)-adequate for any (n, k)-adequate u ∈ R◻B . Notice that if a mapping u is (n, k)-adequate for all k ∈ N, then it is also (n + 1, 0)-adequate. Now by induction on n with a subinduction on k, we immediately obtain that the mapping re◻B , which is a fixed-point of G◻B , is (n, k)-adequate for all n, k ∈ N. Therefore the mapping re◻B is adequate. ◻ Lemma 6.4 For any formula A, there exists an adequate A-removing mapping reA .

.

14

Cut Elimination for Weak Modal Grzegorczyk Logic via Non-Well-Founded Proofs

Proof. We define reA by induction on the structure of the formula A. Case 1: A has the form p. In this case, rep is defined by Lemma 6.2. Case 2: A has the form . Then we put re (π, τ ) ∶= i (π), where i is a non-expansive adequate mapping from Lemma 5.2. Case 3: A has the form B → C. Then we put reB→C (π, τ ) ∶= reC (reB (wk∅,C (riB→C (τ )), iB→C (π)), liB→C (τ )) where riB→C , iB→C , liB→C are non-expansive adeqate mappings from Lemma 5.2 and wk∅,C is a non-expansive adequate mapping from Lemma 5.1. Case 4: A has the form ◻B. By the induction hypothesis, there is an adequate B-removing mapping reB . The required ◻B-removing mapping re◻B ◻ exists by Lemma 6.3. A mapping u∶ P → P is called root-preserving if it maps ∞-proofs to ∞proofs of the same sequents. Let T denote the set of all root-preserving nonexpansive mappings from P to P. Lemma 6.5 The pair (T , l1 ) is a non-empty spherically complete ultrametric space. Theorem 6.6 (cut-elimination) If Grz∞ +cut ⊢ Γ ⇒ ∆, then Grz∞ ⊢ Γ ⇒ ∆. Proof. We obtain the required cut-elimination mapping ce as the fixed-point of a contractive operator F∶ T → T . For a mapping u ∈ T and an ∞-proof π, the ∞-proof F(u)(π) is defined as follows. If ∣π∣ = 0, then we define F(u)(π) to be π. Otherwise, we define F(u)(π) according to the last application of an inference rule in π: →R(A→B) (π0 ) z→ →R(A→B) (u(π0 )) →L(A→B) (π0 , π1 ) z→ →L(A→B) (u(π0 ), u(π1 )) ◻A1 ,...,An (π0 , π1 , . . . , πn ) z→ ◻A1 ,...,An (u(π0 ), u(π1 ), . . . , u(πn )) cutA (π0 , π1 ) z→ reA (π0 , π1 ) Now the operator F is well-defined. By the case analysis according to the definition of F, we see that F(u) is non-expansive and belongs to T whenever u∈T. We claim that F is contractive. It sufficient to check that for any u, v ∈ T and any n, k ∈ N we have u ∼n,k v ⇒ F(u) ∼n,k+1 F(v). which is done by case analysis. Now we define the required cut-elimination mapping ce as the fixed-point of the the operator F∶ T → T , which exists by Lemma 6.5 and Theorem 4.3. For some n, k ∈ N, let us call a mapping u ∈ T (n, k)-free if it satisfies the following two conditions: u(π) ∈ Pn for any π ∈ P; u(π) ∈ Pn+1 whenever ∣π∣ < k.

Savateev and Shamkanov

15

By case analysis we established that F(u) is (n, k +1)-free for any (n, k)-free u ∈ T . Notice that if a mapping u is (n, k)-free for all k ∈ N, then it is also (n+1, 0)-free. Now by induction on n with a subinduction on k, we immediately obtain that the mapping ce, which is a fixed-point of F, is (n, k)-free for all n, k ∈ N. Therefore, for any ∞-proof π, the ∞-proof ce(π) does not contain instances of the rule (cut). Now assume Grz∞ + cut ⊢ Γ ⇒ ∆. Take an ∞-proof of the sequent Γ ⇒ ∆ in the system Grz∞ + cut and apply the mapping ce to it. We obtain an ∞-proof of the same sequent in the system Grz∞ . ◻ Theorem 2.2 is now established as a direct consequence of Theorem 3.4, Theorem 6.6, and Theorem 3.6.

7

Conclusions and Future Work

We have proven the cut elimination theorem for the logic Go syntacticly by constructing a continuous cut eliminating mapping for proofs in a system allowing non-well-founded proofs. This method seems to provide uniform approach to cut-elimination in different logics. Indeed — we can write systems for logics K4, GL, and Grz by slightly modifying the system GoSeq , define appropriate ultrametrics on them, and leave the proof of cut elimilation virtually unchanged. The next step is to take this method to more complicated logics like the logic of transitive closure.

References [1] Gianantonio, P. D. and M. Miculan, A unifying approach to recursive and co-recursive definitions, in: Geuvers H., Wiedijk F. (eds). Types for Proofs and Programs. TYPES 2002, Lecture Notes in Computer Science 2646 (2002), pp. 148–161. [2] Gor´ e, R., Tableau methods for modal and temporal logics, in: Handbook of Tableau Methods (1999), pp. 297–396. [3] Gor´ e, R. and R. Ramanayake, Cut-elimination for weak grzegorczyk logic go, Studia Logica 102 (2014), pp. 1–27. [4] Iemhoff, R., Reasoning in circles, Tributes. Liber Amicorum Alberti. A tribute to Albert Visser. 30 (2016), pp. 165–176. [5] Litak, T., The non-reflexive counterpart of grz, Bulletin of the Section of Logic 36 (2007), pp. 195–208. [6] Prieß-Crampe, S., Der banachsche fixpunktsatz f¨ ur ultrametrische r¨ aume, Results in Mathematics 18 (1990), pp. 178–186. [7] Savateev, Y. and D. Shamkanov, Non-well-founded proofs for the grzegorczyk modal logic, submitted to: The Review of Symbolic Logic . [8] Savateev, Y. and D. Shamkanov, Cut-elimination for the modal grzegorczyk logic via nonwell-founded proofs, in: Kennedy J., de Queiroz R. (eds) Logic, Language, Information, and Computation. WoLLIC 2017, Lecture Notes in Computer Science 10388 (2017), pp. 321–335. [9] Sch¨ orner, E., Ultrametric fixed point theorems and applications, Valuation Theory and Its Applications, Volume II 33 (2003), pp. 353–359. [10] Shamkanov, D., Circular proofs for the g¨ odel-l¨ ob provability logic, Mathematical Notes 96 (2014), pp. 575–585.

16

Cut Elimination for Weak Modal Grzegorczyk Logic via Non-Well-Founded Proofs

Appendix Here we recall basic notions of the theory of ultrametric spaces (cf. [9]) and consider several examples concerning ∞-proofs. An ultrametric space (M, d) is a metric space that satisfies a stronger version of the triangle inequality: for any x, y, z ∈ M d(x, z) ⩽ max{d(x, y), d(y, z)}. For x ∈ M and r ∈ [0, +∞), the set Br (x) = {y ∈ M ∣ d(x, y) ⩽ r} is called the closed ball with center x and radius r. Recall that a metric space (M, d) is complete if any descending sequence of closed balls, with radii tending to 0, has a common point. An ultametric space (M, d) is called spherically complete if an arbitrary descending sequence of closed balls has a common point. For example, consider the set P of all ∞-proofs of the system Go∞ + cut. We can define an ultrametric dP ∶ P × P → [0, 1] on P by putting dP (π, τ ) = inf{

1 ∣ π ∼n τ }. 2n

We see that dP (π, τ ) ⩽ 2−n if and only if π ∼n τ . Thus, the ultrametric dP can be considered as a measure of similarity between ∞-proofs. Proposition 1 (4.1) (P, dP ) is a (spherically) complete ultrametric space. Consider the following characterization of spherically complete ultrametric spaces. Let us write x ≡r y if d(x, y) ⩽ r. Trivially, the relation ≡r is an equivalence relation for any ultrametric space and any number r ⩾ 0. Proposition 2 An ultametric space (M, d) is spherically complete if and only if for any sequence (xi )i∈N of elements of M , where xi ≡ri xi+1 and ri ⩾ ri+1 for all i ∈ N, there is a point x of M such that x ≡ri xi for any i ∈ N. Proof. (⇒) Assume (M, d) is a spherically complete ultrametric space. Consider a sequence (xi )i∈N of elements of M such that xi ≡ri xi+1 and ri ⩾ ri+1 for all i ∈ N. Then the sequence (Bri (xi )) is a descending sequence of closed balls, and therefore by spherical completeness has a common point x. Trivially, the point x satisfies the desired conditions. (⇐) Assume there is a descending sequence of closed balls (Bri (xi )). We have that x0 ≡r0 x1 ≡r1 . . . and ri ⩾ ri+1 for all i ∈ N. So there is an element ◻ x ∈ M such that x ≡ri xi , meaning it lies in all the balls. In an ultrametric space (M, d), a function f ∶ M → M is called non-expansive if d(f (x), f (y)) ⩽ d(x, y) for all x, y ∈ M . For ultrametric spaces (M, dM ) and (N, dN ), the Cartesian product M ×N can be also considered as an ultrametric space with the metric dM×N ((x1 , y1 ), (x2 , y2 )) = max{dM (x1 , x2 ), dN (y1 , y2 )}. Let us consider another example. For m ∈ N, let Fm denote the set of all non-expansive functions from P m to P. Note that any function u∶ P m → P is

Savateev and Shamkanov

17

non-expansive if and only if for any tuples π and π ′ , and any n ∈ N we have ′ π1 ∼n π1′ , . . . , πm ∼n πm ⇒ u(π) ∼n u(π′ ).

Now we introduce an ultrametric for Fm . For a, b ∈ Fm , we write a ∼n,k b if a(π) ∼n b(π) for any π ∈ P m and, in addition, a(π) ∼n+1 b(π) whenever 3 An ultrametric lm on Fm is defined by Σm i=1 ∣πi ∣ < k. lm (a, b) =

1 1 1 inf{ n + n+k ∣ a ∼n,k b}. 2 2 2

We see that lm (a, b) ⩽ 2−n−1 + 2−n−k−1 if and only if a ∼n,k b. Proposition 3 (4.2) (Fm , lm ) is a spherically complete ultrametric space. Proof. Assume we have a series a0 ∼n0 ,k0 a1 ∼n1 ,k1 . . . , where the sequence ri = 2−ni + 2−ni −ki −1 is non-increasing. From Proposition 2, it is sufficient to find a function a ∈ Fm such that a ∼ni ,ki ai for all i ∈ N. Suppose limi→∞ ri = 0. Consider a tuple π ∈ P m . We have that limi→∞ ni = +∞ and a0 (π) ∼n0 a1 (π) ∼n1 . . . . By Proposition 1, there is an ∞-proof τ such that τ ∼ni ai (π) for all i ∈ N. We define a(π) = τ . We need to check that the mapping a is non-expansive. If for tuples π and π ′ we have ′ π1 ∼n π1′ , . . . , πm ∼n πm for some n ∈ N, then we can choose i such that ni > n. We have a(π) ∼n ai (π) ∼n ai (π′ ) ∼n a(π′ ). Therefore a(π) ∼n a(π ′ ) and the mapping a is non-expansive. If limi→∞ ri > 0, then limi→∞ ni = n for some n ∈ N. We have two cases: either limi→∞ ki = k for a number k ∈ N, or limi→∞ ki = +∞. In the first case, there is j ∈ N such that (ni , ki ) = (nj , kj ) for all i > j, and we can take aj as a. Here the mapping a is obviously non-expansive. In the second case, for a tuple π we define a(π) to be aj (π), where j = min{i ∈ N ∣ ni = n and ∑m s=1 ∣πs ∣ < ki }. For all tuples π and π ′ we have a(π) ∼0 a(π′ ). If for tuples π and π ′ and m ′ ′ some n ⩾ 1 we have π1 ∼n π1′ , . . . , πm ∼n πm , then ∑m s=1 ∣πs ∣ = ∑s=1 ∣πs ∣ = t and ′ ′ a(π) = aj (π) ∼n aj (π ) = a(π ), where j = min{i ∈ N ∣ ni = n and t < ki }. Therefore a(π) ∼n a(π ′ ) and the mapping a is non-expansive. ◻ In an ultrametric space (M, d), a function f ∶ M → M is called (strictly) contractive if d(f (x), f (y)) < d(x, y) when x ≠ y.

3

This definition is inspired by [1, Subsection 2.1].