Cut-Elimination for the Modal Grzegorczyk Logic via Non-well-founded Proofs

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.

D. Shamkanov—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

1.1 Proof of Lemma 4.1

Let $\pi ^\prime$ be an $\infty$-proof of $\varGamma \Rightarrow \varDelta , p$ and $\pi ^{\prime \prime }$ be an $\infty$-proof of $p, \varGamma \Rightarrow \varDelta$.

We define $\mathcal R_{p}(\pi ^\prime ,\pi ^{\prime \prime })$ by induction on $|\pi ^\prime |$.

If $|\pi ^\prime |=0$, then $\varGamma \Rightarrow \varDelta , p$ is an initial sequent. Suppose that $\varGamma \Rightarrow \varDelta$ 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, $\varGamma$ has the form $p,\varPhi$, and $\pi ^{\prime \prime }$ is an $\infty$-proof of $p,p,\varPhi \Rightarrow \varDelta$. Applying the nonexpansive mapping $acl _p$ from Lemma 3.6, we put $\mathcal R_{p}(\pi ^\prime ,\pi ^{\prime \prime }) := acl _p (\pi ^{\prime \prime })$.

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

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

where $A\rightarrow B,\varSigma = \varDelta$. Notice that $|\pi ^\prime _0 |< |\pi ^\prime |$. In addition, $\pi ^{\prime \prime }$ is an $\infty$-proof of $p,\varGamma \Rightarrow A\rightarrow B,\varSigma$. We define $\mathcal R_{p}(\pi ^\prime ,\pi ^{\prime \prime })$ as

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

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

where $\varSigma , A\rightarrow B = \varGamma$. We see that $|\pi ^\prime _0 |< |\pi ^\prime |$ and $|\pi ^\prime _1 |< |\pi ^\prime |$. Also, $\pi ^{\prime \prime }$ is an $\infty$-proof of $p,\varSigma , A\rightarrow B\Rightarrow \varDelta$. We define $\mathcal R_{p}(\pi ^\prime ,\pi ^{\prime \prime })$ as

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

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

where $\varSigma , \Box \, A = \varGamma$. We have that $|\pi ^\prime |< |\pi |$. Define $\mathcal R_{p}(\pi ^\prime ,\pi ^{\prime \prime })$ as

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

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

where $\varPhi , \Box \varPi = \varGamma$ and $\Box \, A, \varSigma =\varDelta$. Notice that $|\pi ^\prime _0 |< |\pi ^\prime |$. In addition, $\pi ^{\prime \prime }$ is an $\infty$-proof of $p,\varPhi , \Box \varPi \Rightarrow \Box \, A, \varSigma$. We define $\mathcal R_{p}(\pi ^\prime ,\pi ^{\prime \prime })$ as

where $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$

$$(\pi ^\prime \sim _n \tau ^\prime \wedge \pi ^{\prime \prime } \sim _n \tau ^{\prime \prime }) \Rightarrow \mathcal {R}_p(\pi ^\prime , \pi ^{\prime \prime }) \sim _n \mathcal {R}_p(\tau ^\prime , \tau ^{\prime \prime })\;. $$

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.    $\square$

1.2 Proof of Lemma 4.2

Let $\pi ^\prime$ be an $\infty$-proof of $\varGamma \Rightarrow \varDelta , \Box B$ and $\pi ^{\prime \prime }$ be an $\infty$-proof of $\Box B, \varGamma \Rightarrow \varDelta$.

We define $\mathcal {R}_{\Box B}(\pi ^\prime ,\pi ^{\prime \prime })$ by induction on $|\pi ^\prime |+ |\pi ^{\prime \prime } |$.

If $|\pi ^\prime |=0$ or $|\pi ^{\prime \prime } |=0$, then $\varGamma \Rightarrow \varDelta$ 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.

The only interesting cases are when the formula $\Box B$ is the principal formula in both $\pi ^\prime$ and $\pi ^{\prime \prime }$.

So the $\infty$-proof $\pi ^\prime$ has the form

The cases for the $\infty$-proof $\pi ^{\prime \prime }$ are the following:

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

Since that $|\pi ^{\prime \prime }_0 |< |\pi ^{\prime \prime } |$, we can define $\mathcal R_{\Box B}(\pi ^\prime ,\pi ^{\prime \prime })$ as

$$\mathcal R_{B}(\pi ^\prime _0,\mathcal R_{\Box B}( wk_{B,\emptyset } (\pi ^\prime ),\pi ^{\prime \prime }_0)).$$

where $wk _{-,-}$ is a nonexpansive mapping from Lemma 3.4.

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

Since $|\pi ^{\prime \prime }_0 |< |\pi ^{\prime \prime } |$ and the sequent $\varPhi ^\prime , \Box \varPi ^\prime \Rightarrow \Box C, \varSigma ^\prime$, the sequent $\varPhi , \Box \varPi \Rightarrow \varSigma$, and the sequent $\varGamma \Rightarrow \varDelta$ are equal, we can define $\mathcal R_{\Box B}(\pi ^\prime ,\pi ^{\prime \prime })$ as

where $wk _{-,-}$ is a nonexpansive mapping from Lemma 3.4 and $li _{\, \Box \, A}$ is a nonexpansive mapping from Lemma 3.5. Since the instance of the rule $\mathsf {cut}$ is not in the main fragment, this proof is in $\mathcal P_1$.    $\square$