A question about the (un)derivability of Cut Rule in Sequent Calculus

507 Views Asked by At

This question is motivated by a previous discussion regarding How to show that a valid rule is not derivable in Intuitionistic propositional calculus.

The reference is to Gentzen (1934-35)'s Sequent Calculi $\mathsf {LJ}$ and $\mathsf {LK}$ for Intuitionistic and Classical logics respectively, or some equivalent presentation, like those in Sara Negri and ‎Jan von Plato, Structural Proof Theory (Cambridge UP, 2008).

The basic result of structural Proof Theory is the Cut-Elimination Theorem (or Gentzen's Hauptsatz), showing that $\text {Cut Rule}$ is admissible, were admissibility of a rule in logic means that

the set of theorems of the system does not change when that rule is added to the existing rules of the system. In other words, every formula that can be derived using that rule is already derivable without that rule, so, in a sense, it is redundant.

More formally, a rule having the form:

$$\dfrac {\Sigma}{\alpha \vdash A}$$

is said to be derivable (in e.g. $\mathsf {LK}$) iff there exists a proof (in $\mathsf {LK}$) of $\alpha \vdash A$ from the hypotheses $\Sigma$.

I'll try with a silly example of derived rule in $\mathsf {LJ}$: Contraposition.

We start from $\Gamma, \varphi \vdash \psi$ and derive $\Gamma, \varphi , \lnot \psi \vdash$ followed by $\Gamma, \lnot \psi \vdash \lnot \varphi$.

This derivation amounts to the "new rule":

$\dfrac{\Gamma, \varphi \vdash \psi}{\Gamma, \lnot \psi \vdash \lnot \varphi}.$

Classical propositional calculus is structurally complete, meaning that every admissible rule is derivable, where a rule is derived if its conclusion is deducible from the premises by the rules of the calculus.

Intuitionistic propositional calculus is not.

1st Question: when we say that "Classical propositional calculus is structurally complete", does it mean CPC with $\text {Cut}$?

2nd Question: in order to show that $\text {Cut}$ is not derivable is it enough to observe that $\text {Cut}$ is the only rule that deletes a formula?

2

There are 2 best solutions below

2
On BEST ANSWER

Short answer. No, cut rule is not derivable in $\mathsf{LK} \smallsetminus \{\text{cut}\}$ (classical sequent calculus) or $\mathsf{LJ} \smallsetminus \{\text{cut}\}$ (intuitionistic sequent calculus).

More precisely, to answer your questions.

  1. When someone says that classical propositional logic is structurally complete, it refers to a family of particular proof systems, which does not include sequent calculus. Actually, sequent calculus for classical propositional logic is not structurally complete because cut rule is not derivable.

  2. Essentially, yes! See my long answer below.


Long answer. First, let us fix some definitions. Note that Wikipedia's page about admissibility and derivability of inference rules refers to rules that act on formulas (like the one of natural deduction), not on sequents (like the one of sequent calculus). Similarly, the result about structural completeness you mentioned refers to proof systems acting on formulas, not on sequents.

So, what does it mean that cut rule is admissible in a sequent calculus? There are two possible definitions.

Definition 1 (closer to the one for proof systems acting on formulas): cut rule is admissible in $\mathsf{LK} \smallsetminus \{\text{cut}\}$ if $\Gamma, \Sigma \vdash \Delta, \Theta$ is provable in $\mathsf{LK} \smallsetminus \{\text{cut}\}$ whenever both $\Gamma, A \vdash \Delta$ and $\ \Sigma \vdash A, \Theta$ are $\mathsf{LK} \smallsetminus \{\text{cut}\}$. Similarly for admissibility in $\mathsf{LJ} \smallsetminus \{\text{cut}\}$.

Definition 2 (closer to the intended meaning, from the quote in the OP): cut rule is admissible in $\mathsf{LK} \smallsetminus \{\text{cut}\}$ if $\Gamma \vdash \Delta$ is provable in $\mathsf{LK} \smallsetminus \{\text{cut}\}$ whenever $\Gamma \vdash \Delta$ is provable in $\mathsf{LK}$. Similarly for admissibility in $\mathsf{LJ} \smallsetminus \{\text{cut}\}$.

It is easy to show to the two definitions are equivalent.

What does it mean that cut rule is derivable in a sequent calculus? In my opinion, the only definition that makes sense is the one proposed in the OP. I spell it out in the case of cut rule, for the sake of completeness.

Definition. Cut rule is derivable in $\mathsf{LK} \smallsetminus \{\text{cut}\}$ if $\Gamma, \Sigma \vdash \Delta, \Theta$ is provable in $\mathsf{LK} \smallsetminus \{\text{cut}\}$ from the hypotheses $\Gamma, A \vdash \Delta$ and $\Sigma \vdash A, \Theta$ (i.e. the leaves of the derivation-tree with conclusion $\Gamma, \Sigma \vdash \Delta, \Theta$ can be either axioms of the form $B \vdash B$ or the hypotheses $\Gamma, A \vdash \Delta$ and $\Sigma \vdash A, \Theta$), for any formula $A$. Similarly for derivability in $\mathsf{LJ} \smallsetminus \{\text{cut}\}$.

Proposition. Cut rule is not derivable either in $\mathsf{LK} \smallsetminus \{\text{cut}\}$ or in $\mathsf{LJ} \smallsetminus \{\text{cut}\}$.

Proof. Let $A$ and $B$ be distinct formulas such that $A$ is not a subformula of $B$. From the hypotheses $A \vdash B$ and $\vdash A$ it is impossible to derive $\vdash B$ in $\mathsf{LK} \smallsetminus \{\text{cut}\}$ or in $\mathsf{LJ} \smallsetminus \{\text{cut}\}$, because in $\mathsf{LK} \smallsetminus \{\text{cut}\}$ and in $\mathsf{LJ} \smallsetminus \{\text{cut}\}$ there is no inference rule to eliminate the formula $A$, hence the conclusion of any derivation from the hypotheses $A \vdash B$ and $\vdash A$ in $\mathsf{LK} \smallsetminus \{\text{cut}\}$ or in $\mathsf{LJ} \smallsetminus \{\text{cut}\}$ must contain $A$ as a subformula. $ \ \square$

The point of the proof is that cut rule is the only inference rule in a sequent calculus that allows you to remove something from the premises.

Apart from the proof, there is a maybe even more convincing argument. Cut-elimination theorem (i.e. admissibility of cut rule) is a result whose proof to prove in sequent calculi such as $\mathsf{LK}$ and $\mathsf{LJ}$. It requires advanced techniques and notions. It cut rule were derivable, the proof of cut-elimination theorem would be much easier! Quoting from a paper by Ono (Proof-Theoretic Methods for Nonclassical Logic, p. 217):

the cut rule is not a derivable rule in the system obtained from LJ by deleting the cut rule. That is, it is impossible to replace the cut rule in a uniform way by repeated applications of other rules, as each application of the cut rule will play a different role in a given proof. Therefore, we have to eliminate the cut rule depending on how it is applied.


An aside comment. In my opinion, the fact that structural completeness holds for a proof system for classical propositional logic acting on formulas but does not hold for a proof system for classical propositional logic acting on sequents, shows that the notion of derivability for inference rules is not robust, because it depends on the proof system to which it refers. I would say that such a notion is too syntactical to be meaningful.

4
On

@mauro-allegranza, @taroccoesbrocco The derivation of the Cut rule is of course possible in natural deduction. See Introduction à la logique, Théorie de la démonstration, David D. & Nour K. & Raffali C., DUNOD, 2nd ed., Paris, p. 197. Here is the proof still simplified, in natural deduction as sequent calculus, note that the premisses and the conclusion is the Cut rule:

a derivation of cut