Cut-elimination for the modal Grzegorczyk logic via non-well-founded   proofs

Yury Savateev; Daniyar Shamkanov

arXiv:1704.03258·math.LO·April 12, 2017·WoLLIC

Cut-elimination for the modal Grzegorczyk logic via non-well-founded proofs

Yury Savateev, Daniyar Shamkanov

PDF

Open Access

TL;DR

This paper introduces a sequent calculus for the modal Grzegorczyk logic that permits non-well-founded proofs and establishes a cut-elimination theorem through a continuous transformation of these proofs.

Contribution

It develops a novel sequent calculus with non-well-founded proofs for Grz logic and proves cut-elimination using a continuous proof transformation.

Findings

01

Cut-elimination theorem established for the calculus

02

Continuous cut-elimination mapping constructed

03

Non-well-founded proofs enabled for Grz logic

Abstract

We present a sequent calculus for the modal Grzegorczyk logic Grz allowing non-well-founded proofs and obtain the cut-elimination theorem for it by constructing a continuous cut-elimination mapping acting on these proofs.

Equations107

A ::= ⊥ ∣ p ∣ (A \to A) ∣ □ A,

A ::= ⊥ ∣ p ∣ (A \to A) ∣ □ A,

\neg A := A \to ⊥, ⊤ := \neg⊥, A \land B := \neg (A \to \neg B),

\neg A := A \to ⊥, ⊤ := \neg⊥, A \land B := \neg (A \to \neg B),

A \lor B := (\neg A \to B), ◊ A := \neg □ \neg A .

Γ, A \Rightarrow A, Δ

Γ, A \Rightarrow A, Δ

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 25.54443 pt \vbox Γ, A \Rightarrow B, Δ \vskip -2.32889pt \nointerlineskip \lower 2.41556pt \to_{R} to68.72548pt \xleaders \hrule \hfill \lower -0.2pt \vskip -2.32889pt \nointerlineskip Γ \Rightarrow A \to B, Δ \ignorespaces,

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 25.54443 pt \vbox Γ, A \Rightarrow B, Δ \vskip -2.32889pt \nointerlineskip \lower 2.41556pt \to_{R} to68.72548pt \xleaders \hrule \hfill \lower -0.2pt \vskip -2.32889pt \nointerlineskip Γ \Rightarrow A \to B, Δ \ignorespaces,

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 25.38887 pt \vbox □ Π, □ (A \to □ A) \Rightarrow A \vskip -2.13167pt \nointerlineskip \lower 2.21834pt □_{Grz} to99.111pt \xleaders \hrule \hfill \lower -0.2pt \vskip -2.13167pt \nointerlineskip Γ, □ Π \Rightarrow □ A, Δ \ignorespaces .

Γ \Rightarrow A, Δ

Γ \Rightarrow A, Δ

Γ, p \Rightarrow p, Δ

Γ, p \Rightarrow p, Δ

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 25.54443 pt \vbox Γ, B \Rightarrow Δ Γ \Rightarrow A, Δ \vskip -2.32889pt \nointerlineskip \lower 2.41556pt \to_{L} to114.09592pt \xleaders \hrule \hfill \lower -0.2pt \vskip -2.32889pt \nointerlineskip Γ, A \to B \Rightarrow Δ \ignorespaces, \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 25.54443 pt \vbox Γ, A \Rightarrow B, Δ \vskip -2.32889pt \nointerlineskip \lower 2.41556pt \to_{R} to68.72548pt \xleaders \hrule \hfill \lower -0.2pt \vskip -2.32889pt \nointerlineskip Γ \Rightarrow A \to B, Δ \ignorespaces,

\ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 25.38887 pt \vbox Γ, A, □ A \Rightarrow Δ \vskip -1.27223pt \nointerlineskip \lower 3.27222pt refl to68.69435pt \xleaders \hrule \hfill \lower -0.2pt \vskip -1.27222pt \nointerlineskip Γ, □ A \Rightarrow Δ \ignorespaces, \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 25.38887 pt \vbox Γ, □ Π \Rightarrow A, Δ □ Π \Rightarrow A \vskip -1.175pt \nointerlineskip \lower 3.175pt □ to129.48138pt \xleaders \hrule \hfill \lower -0.2pt \vskip -1.175pt \nointerlineskip Γ, □ Π \Rightarrow □ A, Δ \ignorespaces .

F, p \Rightarrow p

F, p \Rightarrow p

F, p \Rightarrow p

F, p \Rightarrow p

π_{1} \sim_{n} τ_{1}, \dots, π_{k} \sim_{n} τ_{k} \Rightarrow U (π_{1}, \dots, π_{k}) \sim_{n} U (τ_{1}, \dots, τ_{k}),

π_{1} \sim_{n} τ_{1}, \dots, π_{k} \sim_{n} τ_{k} \Rightarrow U (π_{1}, \dots, π_{k}) \sim_{n} U (τ_{1}, \dots, τ_{k}),

d (U (π_{1}, \dots, π_{k}), U (τ_{1}, \dots, τ_{k})) ⩽ max {d (π_{1}, τ_{1}), \dots, d (π_{k}, τ_{k})} .

d (U (π_{1}, \dots, π_{k}), U (τ_{1}, \dots, τ_{k})) ⩽ max {d (π_{1}, τ_{1}), \dots, d (π_{k}, τ_{k})} .

Γ \Rightarrow Δ

Γ \Rightarrow Δ

Γ, A \to B \Rightarrow Δ

Γ, A \to B \Rightarrow Δ

Γ \Rightarrow A \to B, Δ

Γ, p, p \Rightarrow Δ

Γ, p, p \Rightarrow Δ

R_{B \to C} (π^{'}, π^{''}) := R_{C} (R_{B} (missing w k_{\emptyset, C} (ri_{B \to C} (π^{''})), i_{B \to C} (π^{'})), li_{B \to C} (π^{''})),

R_{B \to C} (π^{'}, π^{''}) := R_{C} (R_{B} (missing w k_{\emptyset, C} (ri_{B \to C} (π^{''})), i_{B \to C} (π^{'})), li_{B \to C} (π^{''})),

d (U, V) = π \in P sup d (U (π), V (π)) .

d (U, V) = π \in P sup d (U (π), V (π)) .

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.43332 pt \vbox \vbox π_{1} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, B \Rightarrow Δ \vbox π_{2} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ \Rightarrow A, Δ \vskip -2.32889pt \nointerlineskip \lower 2.41556pt \to_{L} to114.09592pt \xleaders \hrule \hfill \lower -0.2pt \vskip -2.32889pt \nointerlineskip Γ, A \to B \Rightarrow Δ \ignorespaces ⟼ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.43332 pt \vbox \vbox E^{*} (π_{1}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Δ, A \vbox E^{*} (π_{2}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ \Rightarrow A, Δ \vskip -2.32889pt \nointerlineskip \lower 2.41556pt \to_{L} to95.61772pt \xleaders \hrule \hfill \lower -0.64444pt, \vskip -2.32889pt \nointerlineskip Γ, A \to B \Rightarrow Δ \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.43332 pt \vbox \vbox π_{1} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, B \Rightarrow Δ \vbox π_{2} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ \Rightarrow A, Δ \vskip -2.32889pt \nointerlineskip \lower 2.41556pt \to_{L} to114.09592pt \xleaders \hrule \hfill \lower -0.2pt \vskip -2.32889pt \nointerlineskip Γ, A \to B \Rightarrow Δ \ignorespaces ⟼ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.43332 pt \vbox \vbox E^{*} (π_{1}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Δ, A \vbox E^{*} (π_{2}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ \Rightarrow A, Δ \vskip -2.32889pt \nointerlineskip \lower 2.41556pt \to_{L} to95.61772pt \xleaders \hrule \hfill \lower -0.64444pt, \vskip -2.32889pt \nointerlineskip Γ, A \to B \Rightarrow Δ \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.43332 pt \vbox \vbox π_{0} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, A \Rightarrow B, Δ \vskip -2.32889pt \nointerlineskip \lower 2.41556pt \to_{R} to68.72548pt \xleaders \hrule \hfill \lower -0.2pt \vskip -2.32889pt \nointerlineskip Γ \Rightarrow A \to B, Δ \ignorespaces ⟼ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.43332 pt \vbox \vbox E^{*} (π_{0}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, A \Rightarrow B, Δ \vskip -2.32889pt \nointerlineskip \lower 2.41556pt \to_{R} to68.72548pt \xleaders \hrule \hfill \lower -0.64444pt, \vskip -2.32889pt \nointerlineskip Γ \Rightarrow A \to B, Δ \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.43332 pt \vbox \vbox π_{0} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, A \Rightarrow B, Δ \vskip -2.32889pt \nointerlineskip \lower 2.41556pt \to_{R} to68.72548pt \xleaders \hrule \hfill \lower -0.2pt \vskip -2.32889pt \nointerlineskip Γ \Rightarrow A \to B, Δ \ignorespaces ⟼ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.43332 pt \vbox \vbox E^{*} (π_{0}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, A \Rightarrow B, Δ \vskip -2.32889pt \nointerlineskip \lower 2.41556pt \to_{R} to68.72548pt \xleaders \hrule \hfill \lower -0.64444pt, \vskip -2.32889pt \nointerlineskip Γ \Rightarrow A \to B, Δ \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.27776 pt \vbox \vbox π_{0} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, A, □ A \Rightarrow Δ \vskip -1.27223pt \nointerlineskip \lower 3.27222pt refl to68.69435pt \xleaders \hrule \hfill \lower -0.2pt \vskip -1.27222pt \nointerlineskip Γ, □ A \Rightarrow Δ \ignorespaces ⟼ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.27776 pt \vbox \vbox E^{*} (π_{0}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, A, □ A \Rightarrow Δ \vskip -1.27223pt \nointerlineskip \lower 3.27222pt refl to68.69435pt \xleaders \hrule \hfill \lower -0.64444pt, \vskip -1.27222pt \nointerlineskip Γ, □ A \Rightarrow Δ \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.27776 pt \vbox \vbox π_{0} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, A, □ A \Rightarrow Δ \vskip -1.27223pt \nointerlineskip \lower 3.27222pt refl to68.69435pt \xleaders \hrule \hfill \lower -0.2pt \vskip -1.27222pt \nointerlineskip Γ, □ A \Rightarrow Δ \ignorespaces ⟼ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.27776 pt \vbox \vbox E^{*} (π_{0}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, A, □ A \Rightarrow Δ \vskip -1.27223pt \nointerlineskip \lower 3.27222pt refl to68.69435pt \xleaders \hrule \hfill \lower -0.64444pt, \vskip -1.27222pt \nointerlineskip Γ, □ A \Rightarrow Δ \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.27776 pt \vbox \vbox π_{1} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, □ Π \Rightarrow A, Δ \vbox π_{2} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip □ Π \Rightarrow A \vskip -1.175pt \nointerlineskip \lower 3.175pt □ to129.48138pt \xleaders \hrule \hfill \lower -0.2pt \vskip -1.175pt \nointerlineskip Γ, □ Π \Rightarrow □ A, Δ \ignorespaces ⟼ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.27776 pt \vbox \vbox E^{*} (π_{1}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, □ Π \Rightarrow A, Δ \vbox π_{2} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip □ Π \Rightarrow A \vskip -1.175pt \nointerlineskip \lower 3.175pt □ to129.48138pt \xleaders \hrule \hfill \lower -0.64444pt, \vskip -1.175pt \nointerlineskip Γ, □ Π \Rightarrow □ A, Δ \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.27776 pt \vbox \vbox π_{1} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, □ Π \Rightarrow A, Δ \vbox π_{2} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip □ Π \Rightarrow A \vskip -1.175pt \nointerlineskip \lower 3.175pt □ to129.48138pt \xleaders \hrule \hfill \lower -0.2pt \vskip -1.175pt \nointerlineskip Γ, □ Π \Rightarrow □ A, Δ \ignorespaces ⟼ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.27776 pt \vbox \vbox E^{*} (π_{1}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, □ Π \Rightarrow A, Δ \vbox π_{2} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip □ Π \Rightarrow A \vskip -1.175pt \nointerlineskip \lower 3.175pt □ to129.48138pt \xleaders \hrule \hfill \lower -0.64444pt, \vskip -1.175pt \nointerlineskip Γ, □ Π \Rightarrow □ A, Δ \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 47.30553 pt \vbox \vbox π_{1} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ \Rightarrow Δ, A \vbox π_{2} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip A, Γ \Rightarrow Δ \vskip -0.8754pt \nointerlineskip \lower 2.8754pt cut to114.62024pt \xleaders \hrule \hfill \lower -0.2pt \vskip -0.8754pt \nointerlineskip Γ \Rightarrow Δ \ignorespaces ⟼ R_{A} (E^{*} (π_{1}), E^{*} (π_{2})) .

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 47.30553 pt \vbox \vbox π_{1} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ \Rightarrow Δ, A \vbox π_{2} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip A, Γ \Rightarrow Δ \vskip -0.8754pt \nointerlineskip \lower 2.8754pt cut to114.62024pt \xleaders \hrule \hfill \lower -0.2pt \vskip -0.8754pt \nointerlineskip Γ \Rightarrow Δ \ignorespaces ⟼ R_{A} (E^{*} (π_{1}), E^{*} (π_{2})) .

π \sim_{n} τ \Rightarrow E^{*} (π) \sim_{n} E^{*} (τ) .

π \sim_{n} τ \Rightarrow E^{*} (π) \sim_{n} E^{*} (τ) .

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.43332 pt \vbox \vbox π_{1} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, B \Rightarrow Δ \vbox π_{2} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ \Rightarrow A, Δ \vskip -2.32889pt \nointerlineskip \lower 2.41556pt \to_{L} to114.09592pt \xleaders \hrule \hfill \lower -0.2pt \vskip -2.32889pt \nointerlineskip Γ, A \to B \Rightarrow Δ \ignorespaces ⟼ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.43332 pt \vbox \vbox F (U) (π_{1}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Δ, A \vbox F (U) (π_{2}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ \Rightarrow A, Δ \vskip -2.32889pt \nointerlineskip \lower 2.41556pt \to_{L} to101.71774pt \xleaders \hrule \hfill \lower -0.64444pt, \vskip -2.32889pt \nointerlineskip Γ, A \to B \Rightarrow Δ \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.43332 pt \vbox \vbox π_{1} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, B \Rightarrow Δ \vbox π_{2} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ \Rightarrow A, Δ \vskip -2.32889pt \nointerlineskip \lower 2.41556pt \to_{L} to114.09592pt \xleaders \hrule \hfill \lower -0.2pt \vskip -2.32889pt \nointerlineskip Γ, A \to B \Rightarrow Δ \ignorespaces ⟼ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.43332 pt \vbox \vbox F (U) (π_{1}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Δ, A \vbox F (U) (π_{2}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ \Rightarrow A, Δ \vskip -2.32889pt \nointerlineskip \lower 2.41556pt \to_{L} to101.71774pt \xleaders \hrule \hfill \lower -0.64444pt, \vskip -2.32889pt \nointerlineskip Γ, A \to B \Rightarrow Δ \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.43332 pt \vbox \vbox π_{0} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, A \Rightarrow B, Δ \vskip -2.32889pt \nointerlineskip \lower 2.41556pt \to_{R} to68.72548pt \xleaders \hrule \hfill \lower -0.2pt \vskip -2.32889pt \nointerlineskip Γ \Rightarrow A \to B, Δ \ignorespaces ⟼ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.43332 pt \vbox \vbox F (U) (π_{0}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, A \Rightarrow B, Δ \vskip -2.32889pt \nointerlineskip \lower 2.41556pt \to_{R} to68.72548pt \xleaders \hrule \hfill \lower -0.64444pt, \vskip -2.32889pt \nointerlineskip Γ \Rightarrow A \to B, Δ \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.43332 pt \vbox \vbox π_{0} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, A \Rightarrow B, Δ \vskip -2.32889pt \nointerlineskip \lower 2.41556pt \to_{R} to68.72548pt \xleaders \hrule \hfill \lower -0.2pt \vskip -2.32889pt \nointerlineskip Γ \Rightarrow A \to B, Δ \ignorespaces ⟼ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.43332 pt \vbox \vbox F (U) (π_{0}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, A \Rightarrow B, Δ \vskip -2.32889pt \nointerlineskip \lower 2.41556pt \to_{R} to68.72548pt \xleaders \hrule \hfill \lower -0.64444pt, \vskip -2.32889pt \nointerlineskip Γ \Rightarrow A \to B, Δ \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.27776 pt \vbox \vbox π_{0} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, A, □ A \Rightarrow Δ \vskip -1.27223pt \nointerlineskip \lower 3.27222pt refl to68.69435pt \xleaders \hrule \hfill \lower -0.2pt \vskip -1.27222pt \nointerlineskip Γ, □ A \Rightarrow Δ \ignorespaces ⟼ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.27776 pt \vbox \vbox F (U) (π_{0}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, A, □ A \Rightarrow Δ \vskip -1.27223pt \nointerlineskip \lower 3.27222pt refl to68.69435pt \xleaders \hrule \hfill \lower -0.64444pt, \vskip -1.27222pt \nointerlineskip Γ, □ A \Rightarrow Δ \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.27776 pt \vbox \vbox π_{0} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, A, □ A \Rightarrow Δ \vskip -1.27223pt \nointerlineskip \lower 3.27222pt refl to68.69435pt \xleaders \hrule \hfill \lower -0.2pt \vskip -1.27222pt \nointerlineskip Γ, □ A \Rightarrow Δ \ignorespaces ⟼ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.27776 pt \vbox \vbox F (U) (π_{0}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, A, □ A \Rightarrow Δ \vskip -1.27223pt \nointerlineskip \lower 3.27222pt refl to68.69435pt \xleaders \hrule \hfill \lower -0.64444pt, \vskip -1.27222pt \nointerlineskip Γ, □ A \Rightarrow Δ \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.27776 pt \vbox \vbox π_{1} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, □ Π \Rightarrow A, Δ \vbox π_{2} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip □ Π \Rightarrow A \vskip -1.175pt \nointerlineskip \lower 3.175pt □ to129.48138pt \xleaders \hrule \hfill \lower -0.2pt \vskip -1.175pt \nointerlineskip Γ, □ Π \Rightarrow □ A, Δ \ignorespaces ⟼ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.27776 pt \vbox \vbox F (U) (π_{1}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, □ Π \Rightarrow A, Δ \vbox U (π_{2}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip □ Π \Rightarrow A \vskip -1.175pt \nointerlineskip \lower 3.175pt □ to129.48138pt \xleaders \hrule \hfill \lower 0.32777pt . \vskip -1.175pt \nointerlineskip Γ, □ Π \Rightarrow □ A, Δ \ignorespaces

\ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.27776 pt \vbox \vbox π_{1} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, □ Π \Rightarrow A, Δ \vbox π_{2} \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip □ Π \Rightarrow A \vskip -1.175pt \nointerlineskip \lower 3.175pt □ to129.48138pt \xleaders \hrule \hfill \lower -0.2pt \vskip -1.175pt \nointerlineskip Γ, □ Π \Rightarrow □ A, Δ \ignorespaces ⟼ \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \ignorespaces \leavevmode \lower 48.27776 pt \vbox \vbox F (U) (π_{1}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip Γ, □ Π \Rightarrow A, Δ \vbox U (π_{2}) \vskip 2.0pt \nointerlineskip \lower -0.5pt \vbox \vskip 1.0pt \lower -0.5pt \vskip 2.0pt \nointerlineskip □ Π \Rightarrow A \vskip -1.175pt \nointerlineskip \lower 3.175pt □ to129.48138pt \xleaders \hrule \hfill \lower 0.32777pt . \vskip -1.175pt \nointerlineskip Γ, □ Π \Rightarrow □ A, Δ \ignorespaces

U \sim_{n} V \Rightarrow F (U) \sim_{n + 1} F (V) .

U \sim_{n} V \Rightarrow F (U) \sim_{n + 1} F (V) .

\forall n (U \sim_{n} V \Rightarrow F (U) \sim_{n + 1} F (V))

\forall n (U \sim_{n} V \Rightarrow F (U) \sim_{n + 1} F (V))

π^{'}

Peer Reviews

No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.

Videos

No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.

Taxonomy

TopicsAdvanced Algebra and Logic · Logic, Reasoning, and Knowledge · Logic, programming, and type systems

Full text

11institutetext: National Research University Higher School of Economics 22institutetext: Steklov Mathematical Institute of the Russian Academy of Sciences

Cut-elimination for the modal Grzegorczyk logic via non-well-founded proofs

Yury Savateev 11

Daniyar Shamkanov 1122

Abstract

We present a sequent calculus for the modal Grzegorczyk logic $\mathsf{Grz}$ allowing non-well-founded 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, Grzegorczyk logic, cut elimination.

1 Introduction

The Grzegorczyk logic $\mathsf{Grz}$ is a well-known modal logic [3], which can be characterized by reflexive partially ordered Kripke frames without infinite ascending chains. This logic is complete w.r.t. the arithmetical semantics, where the modal connective $\Box$ corresponds to the strong provability operator ”… is true and provable” in Peano arithmetic.

Recently a new proof-theoretic description for the Gödel-Löb provability logic $\mathsf{GL}$ in the form of a sequent calculus allowing so-called cyclic, or circular, proofs was given in [6]. A feature of cyclic proofs is that the graph underlying a proof is not a finite tree but is allowed to contain cycles. Since $\mathsf{GL}$ and $\mathsf{Grz}$ are closely connected, we wonder whether cyclic and, more generally, non-well-founded proofs can be fruitfully considered in the case of $\mathsf{Grz}$ .

In this paper, we present a sequent calculus for the modal Grzegorczyk logic allowing non-well-founded proofs and obtain the cut-elimination theorem for it by constructing a continuous cut-elimination mapping acting on these proofs.

In Section 2, we recall an ordinary sequent calculus for $\mathsf{Grz}$ . In Section 3 we introduce the infinitary proof system $\mathsf{Grz_{\infty}}$ . In Section 4 we establish the cut elimination result for $\mathsf{Grz_{\infty}}$ syntactically. Then, in Section 5 we prove the equivalence of the two systems. In Section 6 we discuss possible applications of the new system.

2 Preliminaries

In this section we recall the modal Grzegorczyk logic $\mathsf{Grz}$ and define an ordinary sequent calculus for it.

Formulas of $\mathsf{Grz}$ , denoted by $A$ , $B$ , $C$ , are built up as follows:

[TABLE]

where $p$ stands for atomic propositions. We treat other boolean connectives and the modal operator $\Diamond$ as abbreviations:

[TABLE]

The Hilbert-style axiomatization of $\mathsf{Grz}$ is given by the following axioms and inference rules:

Axioms:

(i)

Boolean tautologies;

(ii)

$\Box(A\rightarrow B)\rightarrow(\Box A\rightarrow\Box B)$ ;

(iii)

$\Box A\rightarrow\Box\Box A$ ;

(iv)

$\Box A\rightarrow A$ ;

(v)

$\Box(\Box(A\rightarrow\Box A)\rightarrow A)\rightarrow\Box A$ .

Rules: modus ponens, $A/\Box A$ .

Now we define an ordinary sequent calculus for $\mathsf{Grz}$ . A sequent is an expression of the form $\Gamma\Rightarrow\Delta$ , where $\Gamma$ and $\Delta$ are finite multisets of formulas. For a multiset of formulas $\Gamma=A_{1},\dotsc,A_{n}$ , we set $\Box\Gamma:=\Box A_{1},\dotsc,\Box A_{n}$ .

The system $\mathsf{Grz_{Seq}}$ , which is a variant of the sequent calculus from [2], is defined by the following initial sequents and inference rules:

[TABLE]

Fig. 1. The system $\mathsf{Grz_{Seq}}$

The cut rule has the form

[TABLE]

where $A$ is called the cut formula of the given inference.

Lemma 2.1

$\mathsf{Grz_{Seq}}+\mathsf{cut}\vdash\Gamma\Rightarrow\Delta$ * if and only if $\mathsf{Grz}\vdash\bigwedge\Gamma\to\bigvee\Delta$ .*

Proof

Standard transformations of proofs.

Theorem 2.2

If $\mathsf{Grz_{Seq}}+\mathsf{cut}\vdash\Gamma\Rightarrow\Delta$ , then $\mathsf{Grz_{Seq}}\vdash\Gamma\Rightarrow\Delta$ .

A syntactic cut-elimination for the logic $\mathsf{Grz}$ was obtained by M. Borga and P. Gentilini in [2]. In this paper, we will give another proof of this cut-elimination theorem in the next sections.

3 Non-well-founded proofs

Now we define a sequent calculus for the logic $\mathsf{Grz}$ allowing non-well-founded proofs. The cut-elimination theorem for it will be proved in the next section.

Inference rules and initial sequents of the sequent calculus $\mathsf{Grz_{\infty}}$ have the following form:

[TABLE]

Fig. 2. The system $\mathsf{Grz}_{\infty}$

The system $\mathsf{Grz}_{\infty}+\mathsf{cut}$ is defined by adding the rule ( $\mathsf{cut}$ ) to the system $\mathsf{Grz_{\infty}}$ . An $\infty$ –proof in $\mathsf{Grz}_{\infty}$ ( $\mathsf{Grz}_{\infty}+\mathsf{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 $\infty$ –proof must pass through a right premise of the rule $\Box$ infinitely many times. A sequent $\Gamma\Rightarrow\Delta$ is provable in $\mathsf{Grz}_{\infty}$ ( $\mathsf{Grz}_{\infty}+\mathsf{cut}$ ) if there is an $\infty$ –proof in $\mathsf{Grz}_{\infty}$ ( $\mathsf{Grz}_{\infty}+\mathsf{cut}$ ) with the root marked by $\Gamma\Rightarrow\Delta$ .

The main fragment of an $\infty$ –proof is a finite tree obtained from the $\infty$ –proof by cutting every infinite branch at the nearest to the root right premise of the rule ( $\Box$ ). The local height $\lvert\pi\rvert$ of an $\infty$ –proof $\pi$ is the length of the longest branch in its main fragment. An $\infty$ –proof only consisting of an initial sequent has height 0.

For instance, consider an $\infty$ –proof of the sequent $\Box(\Box(p\rightarrow\Box p)\rightarrow p)\Rightarrow p$ :

[TABLE]

where $F=\Box(\Box(p\rightarrow\Box p)\rightarrow p)$ . The local height of this $\infty$ –proof equals to 4 and its main fragment has the form

[TABLE]

By $\mathcal{P}$ denote the set of all $\infty$ -proofs in $\mathsf{Grz}_{\infty}+\mathsf{cut}$ . For $n\in\mathbb{N}$ , we define binary relations $\sim_{n}$ on $\mathcal{P}$ by simultaneous induction:

$\pi\sim_{0}\tau$ for any $\pi,\tau$ ; 2. 2.

if $\lvert\pi\rvert=0$ , then $\pi\sim_{n}\pi$ ; 3. 3.

if $\pi$ and $\tau$ are obtained by the same instance of inference rules ( $\mathsf{\to_{L}}$ ), ( $\mathsf{cut}$ ) from $\pi^{\prime}$ , $\pi^{\prime\prime}$ and $\tau^{\prime}$ , $\tau^{\prime\prime}$ , where $\pi^{\prime}\sim_{n}\tau^{\prime}$ and $\pi^{\prime\prime}\sim_{n}\tau^{\prime\prime}$ , then $\pi\sim_{n}\tau$ ; 4. 4.

if $\pi$ and $\tau$ are obtained by the same instance of inference rules ( $\mathsf{\to_{R}}$ ), ( $\mathsf{refl}$ ) from $\pi^{\prime}$ and $\tau^{\prime}$ , where $\pi^{\prime}\sim_{n}\tau^{\prime}$ , then $\pi\sim_{n}\tau$ ; 5. 5.

if $\pi$ and $\tau$ are obtained by the same instance of an inference rule ( $\mathsf{\Box}$ ) from $\pi^{\prime}$ , $\pi^{\prime\prime}$ and $\tau^{\prime}$ , $\tau^{\prime\prime}$ , where $\pi^{\prime}$ , $\tau^{\prime}$ are $\infty$ -proofs for the left premises of ( $\mathsf{\Box}$ ), and $\pi^{\prime}\sim_{n+1}\tau^{\prime}$ , $\pi^{\prime\prime}\sim_{n}\tau^{\prime\prime}$ , then $\pi\sim_{n+1}\tau$ .

Notice that $\pi\sim_{1}\tau$ if and only if $\pi$ and $\tau$ have the same main fragment.

Lemma 3.1

For any $n\in\mathbb{N}$ , we have that

the relation $\sim_{n}$ is an equivalence relation; 2. 2.

the relation $\sim_{n+1}$ is finer than the relation $\sim_{n}$ .

In addition, the intersection of all relations $\sim_{n}$ is exactly the equality relation over $\mathcal{P}$ .

Now we define a sequence $\mathcal{P}_{n}$ of subsets of $\mathcal{P}$ by simultaneous induction:

$\pi\in\mathcal{P}_{0}$ for any $\pi$ ; 2. 2.

if $\lvert\pi\rvert=0$ , then $\pi\in\mathcal{P}_{n}$ ; 3. 3.

if $\pi$ is obtained by an instance of an inference rule ( $\mathsf{\to_{L}}$ ) from $\pi^{\prime}$ and $\pi^{\prime\prime}$ , where $\pi^{\prime},\pi^{\prime\prime}\in\mathcal{P}_{n}$ , then $\pi\in\mathcal{P}_{n}$ ; 4. 4.

if $\pi$ is obtained by an instance of inference rules ( $\mathsf{\to_{R}}$ ), ( $\mathsf{refl}$ ) from $\pi^{\prime}$ , where $\pi^{\prime}\in\mathcal{P}_{n}$ , then $\pi\in\mathcal{P}_{n}$ ; 5. 5.

if $\pi$ is obtained by an instance of an inference rule ( $\mathsf{\Box}$ ) from $\pi^{\prime}$ and $\pi^{\prime\prime}$ , where $\pi^{\prime}$ is an $\infty$ -proof for the left premise of ( $\mathsf{\Box}$ ), and $\pi^{\prime}\in\mathcal{P}_{n+1}$ , $\pi^{\prime\prime}\in\mathcal{P}_{n}$ , then $\pi\in\mathcal{P}_{n+1}$ .

Notice that $\mathcal{P}_{0}=\mathcal{P}$ and $\mathcal{P}_{1}$ consists of the $\infty$ -proofs that do not contain the cut rule in their main fragment.

Lemma 3.2

We have that $\mathcal{P}_{n}\subset\mathcal{P}_{n+1}$ for any $n\in\mathbb{N}$ . In addition, the intersection of all sets $\mathcal{P}_{n}$ consists exactly of the $\infty$ -proofs in $\mathsf{Grz}_{\infty}$ .

For $\pi,\tau\in\mathcal{P}$ , we define $d(\pi,\tau)=2^{-\sup\{n\in\mathbb{N}\>\mid\>\pi\sim_{n}\tau\}}$ , where by convention $2^{-\infty}=0$ . We see that an equivalence $\pi\sim_{n}\tau$ holds if and only if $d(\pi,\tau)\leqslant 2^{-n}$ .

Proposition 3.3

$(\mathcal{P},d)$ * is a complete metric space.*

A mapping $\mathcal{U}\colon\mathcal{P}^{k}_{m}\to\mathcal{P}_{m}$ is nonexpansive if for any $n\in\mathbb{N}$

[TABLE]

which is equivalent to the standard condition

[TABLE]

Trivially, any nonexpansive mapping is continuous.

A nonexpansive mapping $\mathcal{U}\colon\mathcal{P}\to\mathcal{P}$ is called adequate if $\mathcal{U}(\mathcal{P}_{1})\subset\mathcal{P}_{1}$ and $\lvert\mathcal{U}(\pi)\rvert\leqslant\lvert\pi\rvert$ for any $\pi\in\mathcal{P}$ .

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. In $\mathsf{Grz}_{\infty}+\mathsf{cut}$ , we call a single-premise inference rule strongly admissible if there is an adequate mapping $\mathcal{U}\colon\mathcal{P}\to\mathcal{P}$ that maps any $\infty$ -proof of the premise of the rule to an $\infty$ -proof of the conclusion.

Lemma 3.4

For any finite multisets of formulas $\Pi$ and $\Sigma$ , the inference rule

[TABLE]

is strongly admissible in $\mathsf{Grz}_{\infty}+\mathsf{cut}$ .

Lemma 3.5

For any formulas $A$ and $B$ , the rules

[TABLE]

are strongly admissible in $\mathsf{Grz}_{\infty}+\mathsf{cut}$ .

Lemma 3.6

For any atomic proposition $p$ , the rules

[TABLE]

are strongly admissible in $\mathsf{Grz}_{\infty}+\mathsf{cut}$ .

These lemmata can be obtained in a standard way, so we omit the proofs.

4 Cut elimination

In this section we construct a continuous cut elimination mapping from $\mathcal{P}$ to $\mathcal{P}$ , which eliminates all applications of the cut rule from any $\infty$ -proof in $\mathsf{Grz}_{\infty}+\mathsf{cut}$ . In what follows, we use nonexpansive mappings $\mathcal{\mathit{missing}}{wk}_{\Pi,\Sigma}$ , $\mathit{li}_{A\to B}$ , $\mathit{ri}_{A\to B}$ , $\mathit{i}_{A\to B}$ , $\mathit{i}_{\bot}$ , $\mathit{li}_{\Box A}$ , $\mathit{acl}_{p}$ , $\mathit{acr}_{p}$ from Lemma 3.4, Lemma 3.5 and Lemma 3.6.

For a modal formula $A$ , a nonexpansive mapping $\mathcal{R}$ from $\mathcal{P}_{1}\times\mathcal{P}_{1}$ to $\mathcal{P}_{1}$ is called $A$ -reducing if $\mathcal{R}(\pi^{\prime},\pi^{\prime\prime})$ is an $\infty$ -proof of $\Gamma\Rightarrow\Delta$ whenever $\pi^{\prime}$ is an $\infty$ -proof of $\Gamma\Rightarrow\Delta,A$ and $\pi^{\prime\prime}$ is an $\infty$ -proof of $A,\Gamma\Rightarrow\Delta$ .

Lemma 4.1

For any atomic proposition $p$ there is a $p$ -reducing mapping $\mathcal{R}_{p}$ .

Lemma 4.2

Given a $B$ -reducing mapping $\mathcal{R}_{B}$ , there is a $\Box B$ -reducing mapping $\mathcal{R}_{\Box B}$ .

The proof of these two Lemmas can be found in the Appendix.

Lemma 4.3

For any formula $A$ , there is an $A$ -reducing mapping $\mathcal{R}_{A}$ .

Proof

We define $\mathcal{R}_{A}$ by induction on the structure of the formula $A$ .

Case 1: $A$ has the form $p$ . In this case, $\mathcal{R}_{p}$ is defined in Lemma 4.1.

Case 2: $A$ has the form $\bot$ . Then we put $\mathcal{R}_{\bot}(\pi^{\prime},\pi^{\prime\prime}):=\mathit{i}_{\bot}(\pi^{\prime})$ , where $\mathit{i}_{\bot}$ is a nonexpansive mapping from Lemma 3.5.

Case 3: $A$ has the form $B\to C$ . Then we put

[TABLE]

where $\mathit{ri}_{B\to C}$ , $\mathit{i}_{B\to C}$ , $\mathit{li}_{B\to C}$ are nonexpansive mappings from Lemma 3.5 and $\mathit{wk}_{\emptyset,C}$ is a nonexpansive mapping from Lemma 3.4.

Case 4: $A$ has the form $\Box B$ . By the induction hypothesis, there is a $B$ -reducing mapping $\mathcal{R}_{B}$ . By Lemma 4.2 there is a $\Box B$ -reducing mapping $\mathcal{R}_{\Box B}$ .

A mapping $\mathcal{U}\colon\mathcal{P}\to\mathcal{P}$ is called root-preserving if it maps $\infty$ -proofs to $\infty$ -proofs of the same sequents. The set of all root-preserving nonexpansive mappings from $\mathcal{P}$ to $\mathcal{P}$ is denoted by $\mathcal{N}$ . We consider $\mathcal{N}$ as a metric space with the uniform metric:

[TABLE]

Lemma 4.4

$(\mathcal{N},d)$ * is a non-empty complete metric space.*

Proof

By Lemma 3.3, $\mathcal{P}$ is a complete metric space. Consequently the set $\mathit{C}(\mathcal{P},\mathcal{P})$ of all continuous mappings from $\mathcal{P}$ to $\mathcal{P}$ with the uniform metric forms a complete metric space. The reader will easily prove that $\mathcal{N}$ is a closed subset of $\mathit{C}(\mathcal{P},\mathcal{P})$ . In addition, the set $\mathcal{N}$ is non-empty, because the identity mapping belongs to $\mathcal{N}$ . Thus $(\mathcal{N},d)$ is a non-empty complete metric space.

We define $\mathcal{N}_{n}:=\{\mathcal{U}\in\mathcal{N}\>\mid\>\mathcal{U}(\mathcal{P})\subset\mathcal{P}_{n}\}$ .

Lemma 4.5

There exists a mapping $\mathcal{E}^{\ast}\in\mathcal{N}_{1}$ .

Proof

Assume we have an $\infty$ -proof $\pi$ . We define $\mathcal{E}^{\ast}(\pi)$ by induction on $\lvert\pi\rvert$ .

If $\lvert\pi\rvert=0$ , then we put $\mathcal{E}^{\ast}(\pi)=\pi$ . Otherwise, consider the last application of an inference rule in $\pi$ and define $\mathcal{E}^{\ast}$ as follows:

[TABLE]

Clearly, the mapping $\mathcal{E}^{\ast}$ is root-preserving, and $\mathcal{E}^{\ast}(\mathcal{P})\subset\mathcal{P}_{1}$ . We also see that $\mathcal{E}^{\ast}$ is nonexpansive, i.e. for any $n\in\mathbb{N}$ and any $\pi,\tau\in\mathcal{P}$

[TABLE]

Now we define a contractive operator $\mathcal{F}\colon\mathcal{N}\to\mathcal{N}$ . The required cut-elimination mapping will be obtained as the fixed-point of $\mathcal{F}$ .

For a root-preserving nonexpansive mapping $\mathcal{U}$ and an $\infty$ -proof $\pi$ of a sequent $\Gamma\Rightarrow\Delta$ , we define $\mathcal{F}(\mathcal{U})(\pi)$ . In the case $\pi\in\mathcal{P}_{1}$ , $\mathcal{F}(\mathcal{U})(\pi)$ is introduced by induction on $\lvert\pi\rvert$ . If $\lvert\pi\rvert=0$ , then we put $\mathcal{F}(\mathcal{U})(\pi)=\pi$ . Otherwise, consider the last application of an inference rule in $\pi$ and define $\mathcal{F}(\mathcal{U})$ as follows:

[TABLE]

The mapping $\mathcal{F}(\mathcal{U})$ is well defined on the set $\mathcal{P}_{1}$ . If $\pi\notin\mathcal{P}_{1}$ , then we put $\mathcal{F}(\mathcal{U})(\pi):=\mathcal{F}(\mathcal{U})(\mathcal{E}^{\ast}(\pi))$ .

It can easily be checked that $\mathcal{F}(\mathcal{U})$ is a root-preserving nonexpansive mapping.

Lemma 4.6

We have that $d(\mathcal{F}(\mathcal{U}),\mathcal{F}(\mathcal{V}))\leqslant\frac{1}{2}\cdot d(\mathcal{U},\mathcal{V})$ for any mappings $\mathcal{U},\mathcal{V}\in\mathcal{N}$ .

Proof

Let us write $\mathcal{U}\sim_{n}\mathcal{V}$ if $\mathcal{U}(\pi)\sim_{n}\mathcal{V}(\pi)$ for any $\pi\in\mathcal{P}$ . We claim that for any $n\in\mathbb{N}$

[TABLE]

Assume we have an $\infty$ -proof $\pi$ and $\mathcal{U}\sim_{n}\mathcal{V}$ . Now it can be easily proved by induction on $\lvert\pi\rvert$ that $\mathcal{F}(\mathcal{U})(\pi)\sim_{n+1}\mathcal{F}(\mathcal{V})$ .

Further, we see that $\mathcal{U}\sim_{n}\mathcal{V}$ if and only if $d(\mathcal{U},\mathcal{V})\leqslant 2^{-n}$ . Thus, the condition

[TABLE]

is equivalent to $d(\mathcal{F}(\mathcal{U}),\mathcal{F}(\mathcal{V}))\leqslant\frac{1}{2}\cdot d(\mathcal{U},\mathcal{V})$ .

Lemma 4.7

If $\mathcal{U}\in\mathcal{N}_{n}$ , then $\mathcal{F}(\mathcal{U})\in\mathcal{N}_{n+1}$ .

Proof

Assume we have an $\infty$ -proof $\pi$ and $\mathcal{U}\in\mathcal{N}_{n}$ . We claim $\mathcal{F}(\mathcal{U})(\pi)\in\mathcal{P}_{n}$ .

If $\pi\in\mathcal{P}_{1}$ , then it is not hard to prove by induction on $\lvert\pi\rvert$ that $\mathcal{F}(\mathcal{U})(\pi)\in\mathcal{P}_{n}$ . If $\pi\notin\mathcal{P}_{1}$ , then $\mathcal{E}^{\ast}(\pi)\in\mathcal{P}_{1}$ by Lemma 4.5. Thus $\mathcal{F}(\mathcal{U})(\pi)=\mathcal{F}(\mathcal{U})(\mathcal{E}^{\ast}(\pi))\in\mathcal{P}_{n}$ by the previous case.

Lemma 4.8

There exists a mapping $\mathcal{E}$ such that $\mathcal{E}\in\mathcal{N}_{n}$ for any $n\in\mathbb{N}$ .

Proof

We have that $\mathcal{F}\colon\mathcal{N}\to\mathcal{N}$ is a contractive operator. By the Banach fixed-point theorem, there exists a root-preserving nonexpansive mapping $\mathcal{E}$ such that $\mathcal{F}(\mathcal{E})=\mathcal{E}$ . Trivially, $\mathcal{E}\in\mathcal{N}_{0}=\mathcal{N}$ . Hence $\mathcal{E}$ belongs to the intersection of all $\mathcal{N}_{n}$ for $n\in\mathbb{N}$ by Lemma 4.7.

Theorem 4.9 (cut-elimination)

If $\mathsf{Grz_{\infty}}+\mathsf{cut}\vdash\Gamma\Rightarrow\Delta$ , then $\mathsf{Grz_{\infty}}\vdash\Gamma\Rightarrow\Delta$ .

Proof

Take an $\infty$ -proof of the sequent $\Gamma\Rightarrow\Delta$ in the system $\mathsf{Grz_{\infty}}+\mathsf{cut}$ and apply the mapping $\mathcal{E}$ to it. You will get an $\infty$ -proof of the same sequent in the system $\mathsf{Grz_{\infty}}$ .

5 Ordinary and non-well-founded proofs

In this section we define two translations that connect ordinary and non-well-founded sequent calculi for $\mathsf{Grz}$ .

Lemma 5.1

We have $\mathsf{Grz}_{\infty}\vdash\Gamma,A\Rightarrow A,\Delta$ for any sequent $\Gamma\Rightarrow\Delta$ and any formula $A$ .

Proof

Standard induction on the structure of $A$ .

Lemma 5.2

We have $\mathsf{Grz}_{\infty}\vdash\Box(\Box(A\rightarrow\Box A)\rightarrow A)\Rightarrow A$ for any formula $A$ .

Proof

Consider an example of $\infty$ –proof for the sequent $\Box(\Box(p\rightarrow\Box p)\rightarrow p)\Rightarrow p$ from Section 3. We transform this example into an $\infty$ –proof for $\Box(\Box(A\rightarrow\Box A)\rightarrow A)\Rightarrow A$ by replacing $p$ with $A$ and adding required $\infty$ –proofs instead of initial sequents using Lemma 5.1.

Theorem 5.3

If $\mathsf{Grz_{Seq}}+\mathsf{cut}\vdash\Gamma\Rightarrow\Delta$ , then $\mathsf{Grz}_{\infty}+\mathsf{cut}\vdash\Gamma\Rightarrow\Delta$ .

Proof

Assume $\pi$ is a proof of $\Gamma\Rightarrow\Delta$ in $\mathsf{Grz_{Seq}}+\mathsf{cut}$ . By induction on the size of $\pi$ we prove $\mathsf{Grz}_{\infty}+\mathsf{cut}\vdash\Gamma\Rightarrow\Delta$ .

If $\Gamma\Rightarrow\Delta$ is an initial sequent of $\mathsf{Grz_{Seq}}+\mathsf{cut}$ , then it is provable in $\mathsf{Grz}_{\infty}+\mathsf{cut}$ by Lemma 5.1. Otherwise, consider the last application of an inference rule in $\pi$ .

The only non-trivial case is when the proof $\pi$ has the form

[TABLE]

where $\Sigma,\Box\Pi=\Gamma$ and $\Box A,\Lambda=\Delta$ . By the induction hypothesis there is an $\infty$ –proof $\xi$ of $\Box\Pi,\Box(A\to\Box A)\Rightarrow A$ in $\mathsf{Grz}_{\infty}+\mathsf{cut}$ .

We have the following $\infty$ –proof $\lambda$ of $\Box\Pi\Rightarrow A$ in $\mathsf{Grz}_{\infty}+\mathsf{cut}$ :

[TABLE]

where $G=\Box(A\rightarrow\Box A)\rightarrow A$ , $\xi^{\prime}$ is an $\infty$ –proof of $\Box\Pi,\Box(A\to\Box A)\Rightarrow A,A$ obtained from $\xi$ by Lemma 3.4 and $\theta$ is an $\infty$ –proof of $\Box\Pi,\Box G\Rightarrow A$ , which exists by Lemma 5.2 and Lemma 3.4.

The required $\infty$ –proof for $\Sigma,\Box\Pi\Rightarrow\Box A,\Delta$ has the form

[TABLE]

where $\lambda^{\prime}$ is an $\infty$ –proof for the sequent $\Gamma,\Box\Pi\Rightarrow A,\Delta$ obtained from $\lambda$ by Lemma 5.4.

The cases of other inference rules being last in $\pi$ are straightforward, so we omit them.

Lemma 5.4

The rule

[TABLE]

is admissible in $\mathsf{Grz_{Seq}}$ .

Proof

Standard induction on the structure of a proof of $\Gamma\Rightarrow\Delta$ .

For a sequent $\Gamma\Rightarrow\Delta$ , let $Sub(\Gamma\Rightarrow\Delta)$ be the set of all subformulas of the formulas from $\Gamma\cup\Delta$ . For a finite set of formulas $\Lambda$ , set $\Lambda^{\ast}:=\{\Box(A\to\Box A)\mid A\in\Lambda\}$ .

Lemma 5.5

If $\mathsf{Grz_{\infty}}\vdash\Gamma\Rightarrow\Delta$ , then $\mathsf{Grz_{Seq}}\vdash\Lambda^{\ast},\Gamma\Rightarrow\Delta$ for any finite set of formulas $\Lambda$ .

Proof

Assume $\pi$ is an $\infty$ –proof of the sequent $\Gamma\Rightarrow\Delta$ in $\mathsf{Grz}_{\infty}$ and $\Lambda$ is a finite set of formulas. By induction on the number of elements in the finite set $Sub(\Gamma\Rightarrow\Delta)\setminus\Lambda$ with a subinduction on $\lvert\pi\rvert$ , we prove $\mathsf{Grz_{Seq}}\vdash\Lambda^{\ast},\Gamma\Rightarrow\Delta$ .

If $\lvert\pi\rvert=0$ , then $\Gamma\Rightarrow\Delta$ is an initial sequent. We see that the sequent $\Lambda^{\ast},\Gamma\Rightarrow\Delta$ is an initial sequent and it is provable in $\mathsf{Grz_{Seq}}$ . Otherwise, consider the last application of an inference rule in $\pi$ .

Case 1. Suppose that $\pi$ has the form

[TABLE]

where $A\to B,\Sigma=\Delta$ . Notice that $\lvert\pi^{\prime}\rvert<\lvert\pi\rvert$ . By the induction hypothesis for $\pi^{\prime}$ and $\Lambda$ , the sequent $\Lambda^{\ast},\Gamma,A\Rightarrow B,\Sigma$ is provable in $\mathsf{Grz_{Seq}}$ . Applying the rule ( $\mathsf{\to_{R}}$ ) to it, we obtain that the sequent $\Lambda^{\ast},\Gamma\Rightarrow\Delta$ is provable in $\mathsf{Grz_{Seq}}$ .

Case 2. Suppose that $\pi$ has the form

[TABLE]

where $\Sigma,A\to B=\Gamma$ . We see that $\lvert\pi^{\prime}\rvert<\lvert\pi\rvert$ . By the induction hypothesis for $\pi^{\prime}$ and $\Lambda$ , the sequent $\Lambda^{\ast},\Sigma,B\Rightarrow\Delta$ is provable in $\mathsf{Grz_{Seq}}$ . Analogously, we have $\mathsf{Grz_{Seq}}\vdash\Lambda^{\ast},\Sigma\Rightarrow A,\Delta$ . Applying the rule ( $\mathsf{\to_{L}}$ ), we obtain that the sequent $\Lambda^{\ast},\Sigma,A\to B\Rightarrow\Delta$ is provable in $\mathsf{Grz_{Seq}}$ .

Case 3. Suppose that $\pi$ has the form

[TABLE]

where $\Sigma,\Box A=\Gamma$ . We see that $\lvert\pi^{\prime}\rvert<\lvert\pi\rvert$ . By the induction hypothesis for $\pi^{\prime}$ and $\Lambda$ , the sequent $\Lambda^{\ast},\Sigma,A,\Box A\Rightarrow\Delta$ is provable in $\mathsf{Grz_{Seq}}$ . Applying the rule ( $\mathsf{refl}$ ), we obtain $\mathsf{Grz_{Seq}}\vdash\Lambda^{\ast},\Sigma,\Box A\Rightarrow\Delta$ .

Case 4. Suppose that $\pi$ has the form

[TABLE]

where $\Phi,\Box\Pi=\Gamma$ and $\Box A,\Sigma=\Delta$ .

Subcase 4.1: the formula $A$ belongs to $\Lambda$ . We see that $\lvert\pi^{\prime}\rvert<\lvert\pi\rvert$ . By the induction hypothesis for $\pi^{\prime}$ and $\Lambda$ , the sequent $\Lambda^{\ast},\Phi,\Box\Pi\Rightarrow A,\Sigma$ is provable in $\mathsf{Grz_{Seq}}$ . Then we see

[TABLE]

where the rule ( $\mathsf{weak}$ ) is admissible by Lemma 5.4.

Subcase 4.2: the formula $A$ doesn’t belong to $\Lambda$ . We have that the number of elements in $Sub(\Box\Pi\Rightarrow A)\setminus(\Lambda\cup\{A\})$ is strictly less than the number of elements in $Sub(\Phi,\Box\Pi\Rightarrow\Box A,\Sigma)\setminus\Lambda$ . Therefore, by the induction hypothesis for $\pi^{\prime\prime}$ and $\Lambda\cup\{A\}$ , the sequent $\Lambda^{\ast},\Box(A\to\Box A),\Box\Pi\Rightarrow A$ is provable in $\mathsf{Grz_{Seq}}$ . Then we have

[TABLE]

From Lemma 5.5 we immediately obtain the following theorem.

Theorem 5.6

If $\mathsf{Grz_{\infty}}\vdash\Gamma\Rightarrow\Delta$ , then $\mathsf{Grz_{Seq}}\vdash\Gamma\Rightarrow\Delta$ .

Theorem 2.2 is now established as a direct consequence of Theorem 5.3, Theorem 4.9, and Theorem 5.6.

6 Conclusion and Future Work

Recall that the Craig interpolation property for a logic $\mathsf{L}$ says that if $A$ implies $B$ , then there is an interpolant, that is, a formula $I$ containing only common variables of $A$ and $B$ such that $A$ implies $I$ and $I$ implies $B$ . The Lyndon interpolation property is a strengthening of the Craig one that also takes into consideration negative and positive occurrences of the shared propositional variables; that is, the variables occurring in $I$ positively (negatively) must also occur both in $A$ and $B$ positively (negatively).

Though the Grzegorczyk logic has the Lyndon interpolation property [4], there were seemingly no syntactic proofs of this result. It is unclear how Lyndon interpolation can be obtained from previously introduced sequent systems for $\mathsf{Grz}$ [1, 2, 5] by direct proof-theoretic arguments because these systems contain inference rules in which a polarity change occurs under the passage from the principal formula in the conclusion to its immediate ancestors in the premise. Using our system $\mathsf{Grz}_{\infty}$ we believe that we can obtain a syntactic proof of Lyndon interpolation for the modal Grzegorczyk logic as an application of our cut-elimination theorem.

We also believe that every provable $\mathsf{Grz}_{\infty}$ sequent has a proof that is a regular tree (has only finite amout of distinct subtrees). This gives a possibility of proof system for the logic $\mathsf{Grz}$ with cyclical proofs, like the system introduced in [6].

7 Acknoledgements

The article was prepared within the framework of the Basic Research Program at the National Research University Higher School of Economics (HSE) and supported within the framework of a subsidy by the Russian Academic Excellence Project ’5-100’. Both authors also acknowledge support from the Russian Foundation for Basic Research (grant no. 15-01-09218a).

Appendix.

Proof of Lemma 4.1

Assume we have two $\infty$ -proofs $\pi^{\prime}$ and $\pi^{\prime\prime}$ from $\mathcal{P}_{1}$ . If there is no application of the cut rule to these $\infty$ -proofs with the cut formula $p$ , then we put $\mathcal{R}_{p}(\pi^{\prime},\pi^{\prime\prime}):=\pi^{\prime}$ . In the converse case, there is a sequent $\Gamma\Rightarrow\Delta$ such that $\pi^{\prime}$ is an $\infty$ -proof of $\Gamma\Rightarrow\Delta,p$ and $\pi^{\prime\prime}$ is an $\infty$ -proof of $p,\Gamma\Rightarrow\Delta$ . We define $\mathcal{R}_{p}(\pi^{\prime},\pi^{\prime\prime})$ by induction on $\lvert\pi^{\prime}\rvert$ .

If $\lvert\pi^{\prime}\rvert=0$ , then $\Gamma\Rightarrow\Delta,p$ is an initial sequent. Suppose that $\Gamma\Rightarrow\Delta$ is also an initial sequent. Then $\mathcal{R}_{p}(\pi^{\prime},\pi^{\prime\prime})$ is defined as the $\infty$ -proof consisting only of this initial sequent. Otherwise, $\Gamma$ has the form $p,\Phi$ , and $\pi^{\prime\prime}$ is an $\infty$ -proof of $p,p,\Phi\Rightarrow\Delta$ . Applying the nonexpansive mapping $\mathit{acl}_{p}$ from Lemma 3.6, we put $\mathcal{R}_{p}(\pi^{\prime},\pi^{\prime\prime}):=\mathit{acl}_{p}(\pi^{\prime\prime})$ .

Now suppose that $\lvert\pi^{\prime}\rvert>0$ . We consider the last application of an inference rule in $\pi^{\prime}$ .

Case 1. The $\infty$ -proof $\pi^{\prime}$ has the form

[TABLE]

where $A\to B,\Sigma=\Delta$ . Notice that $\lvert\pi^{\prime}_{0}\rvert<\lvert\pi^{\prime}\rvert$ . In addition, $\pi^{\prime\prime}$ is an $\infty$ -proof of $p,\Gamma\Rightarrow A\to B,\Sigma$ . We define $\mathcal{R}_{p}(\pi^{\prime},\pi^{\prime\prime})$ as

[TABLE]

where $\mathit{i}_{A\to B}$ is a nonexpansive mapping from Lemma 3.5.

Case 2. The $\infty$ -proof $\pi^{\prime}$ has the form

[TABLE]

where $\Sigma,A\to B=\Gamma$ . We see that $\lvert\pi^{\prime}_{0}\rvert<\lvert\pi^{\prime}\rvert$ and $\lvert\pi^{\prime}_{1}\rvert<\lvert\pi^{\prime}\rvert$ . Also, $\pi^{\prime\prime}$ is an $\infty$ -proof of $p,\Sigma,A\to B\Rightarrow\Delta$ . We define $\mathcal{R}_{p}(\pi^{\prime},\pi^{\prime\prime})$ as

[TABLE]

where $\mathit{li}_{A\to B}$ and $\mathit{ri}_{A\to B}$ are nonexpansive mappings from Lemma 3.5.

Case 3. The $\infty$ -proof $\pi^{\prime}$ has the form

[TABLE]

where $\Sigma,\Box A=\Gamma$ . We have that $\lvert\pi^{\prime}\rvert<\lvert\pi\rvert$ . Define $\mathcal{R}_{p}(\pi^{\prime},\pi^{\prime\prime})$ as

[TABLE]

where $\mathit{wk}_{A,\emptyset}$ is the nonexpansive mapping from Lemma 3.4.

Case 4. Now consider the final case when $\pi^{\prime}$ has the form

[TABLE]

where $\Phi,\Box\Pi=\Gamma$ and $\Box A,\Sigma=\Delta$ . Notice that $\lvert\pi^{\prime}_{0}\rvert<\lvert\pi^{\prime}\rvert$ . In addition, $\pi^{\prime\prime}$ is an $\infty$ -proof of $p,\Phi,\Box\Pi\Rightarrow\Box A,\Sigma$ . We define $\mathcal{R}_{p}(\pi^{\prime},\pi^{\prime\prime})$ as

[TABLE]

where $\mathit{li}_{\>\Box A}$ is a nonexpansive mapping from Lemma 3.5.

The mapping $\mathcal{R}_{p}$ is well defined. It remains to check that $\mathcal{R}_{p}$ is nonexpansive, i.e. for any $n\in\mathbb{N}$ and any $\pi^{\prime}$ , $\pi^{\prime\prime}$ , $\tau^{\prime}$ , $\tau^{\prime\prime}$ from $\mathcal{P}_{0}$

[TABLE]

This condition is checked by structural induction on the inductively defined relation $\pi^{\prime}\sim_{n}\tau^{\prime}$ in a straightforward way. So we omit further details.

Proof of Lemma 4.2

Assume we have two $\infty$ -proofs $\pi^{\prime}$ and $\pi^{\prime\prime}$ from $\mathcal{P}_{1}$ . If there is no application of the cut rule to these $\infty$ -proofs with the cut formula $\Box B$ , then we put $\mathcal{R}_{\Box B}(\pi^{\prime},\pi^{\prime\prime}):=\pi^{\prime}$ . In the converse case, we define $\mathcal{R}_{\Box B}(\pi^{\prime},\pi^{\prime\prime})$ by induction on $\lvert\pi^{\prime}\rvert+\lvert\pi^{\prime\prime}\rvert$ .

If $\lvert\pi^{\prime}\rvert=0$ or $\lvert\pi^{\prime\prime}\rvert=0$ , then $\Gamma\Rightarrow\Delta$ is an initial sequent. Then $\mathcal{R}_{\Box B}(\pi^{\prime},\pi^{\prime\prime})$ is defined as the $\infty$ -proof consisting only of this initial sequent.

Now suppose that $\lvert\pi^{\prime}\rvert>0$ . We consider the last application of an inference rule in $\pi^{\prime}$ . If the principal formula of this inference is not $\Box B$ , then $\mathcal{R}_{\Box B}(\pi^{\prime},\pi^{\prime\prime})$ is defined similarly to the four cases of Lemma 4.1.

We can now assume that $\pi^{\prime}$ has the form

[TABLE]

Consider the last application of an inference rule in $\pi^{\prime\prime}$ . If the rule used was $\mathsf{\to_{L}}$ , $\mathsf{\to_{R}}$ , $\mathsf{refl}$ with the principal formula being not $\Box B$ , or the rule $\mathsf{\Box}$ without the formula $\Box B$ in the right premise, then $\mathcal{R}_{\Box B}(\pi^{\prime},\pi^{\prime\prime})$ can also be defined similarly to the previous case.

Otherwise, we have the following cases.

Case A. The $\infty$ -proof $\pi^{\prime\prime}$ has the form

[TABLE]

Since that $\lvert\pi^{\prime\prime}_{0}\rvert<\lvert\pi^{\prime\prime}\rvert$ , we can define $\mathcal{R}_{\Box B}(\pi^{\prime},\pi^{\prime\prime})$ as

[TABLE]

Case B. The $\infty$ -proof $\pi^{\prime\prime}$ has the form

[TABLE]

Since $\lvert\pi^{\prime\prime}_{0}\rvert<\lvert\pi^{\prime\prime}\rvert$ and the sequents $\Phi^{\prime},\Box\Pi^{\prime}\Rightarrow\Box C,\Sigma^{\prime}$ and $\Gamma\Rightarrow\Delta$ are equal, we can define $\mathcal{R}_{\Box B}(\pi^{\prime},\pi^{\prime\prime})$ as

[TABLE]

where $\mathit{wk}_{-,-}$ is a nonexpansive mapping from Lemma 3.4. Since the instance of the rule $\mathsf{cut}$ is not in the main fragment, this proof is in $\mathcal{P}_{1}$ .

Bibliography6

The reference list from the paper itself. Each links out to its DOI / PubMed record.

1[1] A. Avron: On modal systems having arithmetical interpretations, Journal of Symbolic Logic , 49, (3), 935–942, 1984
2[2] M. Borga, P. Gentilini: On the Proof Theory of the Modal Logic Grz, Mathematical Logic Quarterly , 32, (10–12), 145–148, 1986
3[3] Maksimova, L. L.: On Modal Grzegorczyk Logic, Fundamenta Informaticae , Topics in Logic, Philosophy and Foundations of Mathematics and Computer Science, In Recognition of Professor Andrzej Grzegorczyk, 81, (1–3), 203–210, 2008
4[4] Maksimova, L. L.: The Lyndon property and uniform interpolation over the Grzegorczyk logic, Siberian Mathematical Journal , 55, (1), 118–124, 2014
5[5] Roy Dyckhoff, Sara Negri: A cut-free sequent system for Grzegorczyk logic, with an application to the Gödel–Mc Kinsey–Tarski embedding, Journal of Logic and Computation , 26, (1), 169–187, 2016
6[6] Shamkanov, D. S.: Circular proofs for the Gödel-Löb provability logic, Mathematical Notes , 96, (3), 575–585, 2014

TL;DR

Contribution

Findings

Abstract

Peer Reviews

Videos

Taxonomy

Cut-elimination for the modal Grzegorczyk logic via non-well-founded proofs

Abstract

1 Introduction

2 Preliminaries

Lemma 2.1

Proof

Theorem 2.2

3 Non-well-founded proofs

Lemma 3.1

Lemma 3.2

Proposition 3.3

Lemma 3.4

Lemma 3.5

Lemma 3.6

4 Cut elimination

Lemma 4.1

Lemma 4.2

Lemma 4.3

Proof

Lemma 4.4

Proof

Lemma 4.5

Proof

Lemma 4.6

Proof

Lemma 4.7

Proof

Lemma 4.8

Proof

Theorem 4.9** (cut-elimination)**

Proof

5 Ordinary and non-well-founded proofs

Lemma 5.1

Proof

Lemma 5.2

Proof

Theorem 5.3

Proof

Lemma 5.4

Proof

Lemma 5.5

Proof

Theorem 5.6

6 Conclusion and Future Work

7 Acknoledgements

Appendix.

Proof of Lemma 4.1

Proof of Lemma 4.2

Theorem 4.9 (cut-elimination)