Is there a way to prove the cut rule in LK sequent calculus without converting to implications?

Question

The cut rule is given as follows by these two wikipedia articles 1, 2:

$$\Gamma \vdash \Delta, A \qquad \Sigma, A \vdash \Pi \over \Gamma, \Sigma \vdash \Delta, \Pi$$

I have the following proof which converts to and from implications.

Starting with the two sequents,

\begin{align} & \Gamma \vdash \Delta, A \qquad & \Sigma, A \vdash \Pi \\ & \Gamma \rightarrow \Delta \vee A \qquad & \Sigma \wedge A \rightarrow \Pi \\ & \neg \Gamma \vee (\Delta \vee A) \qquad & \neg (\Sigma \wedge A) \vee \Pi \\ & \neg \Gamma \vee \Delta \vee A \qquad & \neg \Sigma \vee \neg A \vee \Pi \\ \end{align}

IIUC, the original sequents ($\Gamma \vdash \Delta, A$ and $\Sigma, A \vdash \Pi$) must each be true, so we must have

$$(\neg \Gamma \vee \Delta \vee A) \wedge (\neg \Sigma \vee \neg A \vee \Pi)$$

Doing some case work, $A$ must be true or $A$ must be false (i.e. $A \vee \neg A$):

• if $A$ is true, the above reduces to $\neg \Sigma \vee \Pi$
• if $A$ is false, the above reduces to $\neg \Gamma \vee \Delta$

\begin{align} A & \vee \neg A \\ (A \rightarrow \neg \Sigma \vee \Pi) & \wedge (\neg A \rightarrow \neg \Gamma \vee \Delta) \\ (\neg \Sigma \vee \Pi) & \vee (\neg \Gamma \vee \Delta) \\ \neg \Sigma \vee \neg \Gamma & \vee \Delta \vee \Pi \\ \end{align}

Which can be converted back into a sequent:

\begin{align} & \vdash \neg \Sigma, \neg \Gamma, \Delta, \Pi \\ \Sigma, \Gamma & \vdash \Delta, \Pi \\ \Gamma, \Sigma & \vdash \Delta, \Pi \end{align}

Thus proving the cut rule.

---

Would there have been a way to prove the cut rule without converting the sequents into implications?

Answer 1

What you tried to "prove" above semantically is actually called the admissibility of the cut rule in sequent calculus as referenced in this Wikipedia article:

In proof theory, admissibility is often considered in the context of sequent calculi, where the basic objects are sequents rather than formulas. For example, one can rephrase the cut-elimination theorem as saying that the cut-free sequent calculus admits the cut rule

However, cut rule as a basic rule is not derivable from other inference rules of the same system, otherwise Gentzen's cut-elimination theorem will be much easier to get. And your above "proof" is not acceptable to derive cut rule within $LK$ (not by translating to another Hilbert or mixed system), you need to try to use other clearly specified rules of $LK$ and you'll be certain to fail.

Your above effort makes sense in the context of the end of the linked Wikipedia article, which states:

(By abuse of language, it is also sometimes said that the (full) sequent calculus admits cut, meaning its cut-free version does.) However, admissibility in sequent calculi is usually only a notational variant for admissibility in the corresponding logic: any complete calculus for (say) intuitionistic logic admits a sequent rule if and only if IPC admits the formula rule which we obtain by translating each sequent to its characteristic formula.

In conclusion cut rule is an admissible but not derivable rule in most sequent calculi.