5

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
    I have a fairly good idea what it means for the cut rule to be admissible. Alas, I have no idea what it would mean for the cut rule to be derivable, even after reading the linked thread and Rozière's paper. Would you provide an explicit definition of derivability, perhaps even specialized to the cut rule? – Z. A. K. Jan 18 '21 at 12:38
  • 2
    @Z.A.K. - added def and references. My concern is: if Cut is not derivable, what does it mean that "Classical propositional calculus is structurally complete, meaning that every admissible rule is derivable"? – Mauro ALLEGRANZA Jan 18 '21 at 12:46
  • 1
    I'm perplexed, because if Cut is derivable, why I've not found this result in the "usual" Proof-Theory literature? Thus, my basic question: what I've misunderstood? – Mauro ALLEGRANZA Jan 18 '21 at 12:49
  • 2
    When we say "Classical propositional calculus is structurally complete, meaning that every admissible rule is derivable" does "CPC" refer to LK, its cut-free fragment, or something else altogether? After all, the cut rule is derivable in LK simply because Cut is one of the rules of LK. Cut is eliminated from LK by the Hauptsatz, which shows that it is admissible in the cut-free fragment of LK. – Z. A. K. Jan 18 '21 at 13:09
  • 2
    Okay, I think I'm on the same page with you regarding derivability now. You're right to be skeptical, I'd be very surprised if cut was derivable in this sense in any of the usual cut-free calculi. My only thought is that structural completeness must refers to some other classical calculus, say LK with cut or possibly another system altogether. E.g. classical Hilbert calculi should satisfy the analogous property. It's night-time down under, but if this remains unanswered, I'll try to chase down some references for these results tomorrow. – Z. A. K. Jan 18 '21 at 13:27

2 Answers2

6

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.

1

@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

  • Some subtle difference. This is an admissible derived rule in ND called substitution rule which admits composability of certain derivations to chain each other to arrive at a new judgement, but is rarely used in ND (Fitch style). Even you actually use this rule in ND with sequent calculus style, the active formula may not be immediately next to the conclusion as you idealized above as a general rule, it may appear in any earlier step of the derivation tree, while cut elimination always ensures its last step is cut free. Finally some Hilbert systems can only use cut rule to derive theorems... – cinch Sep 23 '21 at 06:18
  • Differences of styles in natural deduction should be superficial. The important point of the above derivation is its abnormality: the occurrence of $B \to C$ is both application of conditional introduction and major premiss for conditional elimination (Prawitz); therefore, it is a useless detour. Hence the translation of Cut elimination theorem in natural deduction: a normal derivation in natural deduction is a derivation in which all major premisses are proper assumptions i.e. underivable assumptions. See Negri & von Plato, Structural Proof Theory, p. 201. – Joseph Vidal-Rosset Sep 23 '21 at 08:04
  • thx for your elaboration about in ND such a rule is indeed abnormal. I just saw an old post in this site referencing same Negri's book, saying he's emphasizing Elimination of substitution is very different from the elimination of cut. So apparently seems Negri thinks their style difference is not that superficial... – cinch Sep 23 '21 at 17:10
  • @mohottnad : the point is the derivation of the Cut rule, not providing in natural deduction a rule immediately similar to Cut, as substitution for example. I persist in saying that difference of styles are superficial, that is to say logically without importance, because finally the logical deduction is exactly the same: the above deduction can be expressed in Fitch style as well as in Gentzen-Prawitz tree style. – Joseph Vidal-Rosset Sep 24 '21 at 06:57