# Does cut elimination fail here?

Proving $\lnot\lnot(A\lor\lnot A)$ in intuitionistic sequent calculus with cut seems to be easy: We use cut to prove $\lnot(A\lor\lnot A)\vdash \bot$ from $\lnot(A\lor\lnot A)\vdash \lnot A \land\lnot\lnot A$ and $\lnot A \land\lnot\lnot A\vdash \bot$.

But how can one ever prove $\lnot(A\lor\lnot A)\vdash \bot$ without using cut? Without cut, the only way to prove it seems to be to derive it from $\vdash A\lor\lnot A$. But that sequent is not valid. I guess there must be some other way to prove it without cut that I just fail to see. (My reasoning is that I am pretty certain that $\lnot\lnot(A\lor\lnot A)$ and $\lnot(A\lor\lnot A)\vdash \bot$ are valid in intuitionistic logic, even if my proof with cut should be incorrect.)

I initially suspected that I am missing some rule(s) related to $\bot$, but the proof with cut still seems to go through unchanged if $\bot$ is replaced by $C$ and $\lnot X$ by $X\to C$. (Both $B\land(B\to C)\vdash C$ and $(A\lor B)\to C \vdash (A\to C) \land (B\to C)$ are easy to prove, and replacing $B$ by $(A\to C)$ and using cut like before still gives $(A\lor(A\to C))\to C\vdash C$.)

## 1 Answer

$$\dfrac{\dfrac{\dfrac{\dfrac{}{A\vdash A}}{A\vdash A\lor(A\to C)}\qquad\dfrac{}{C\vdash C}}{\dfrac{\dfrac{(A\lor(A\to C))\to C,A\vdash C}{(A\lor(A\to C))\to C\vdash A\to C}}{(A\lor(A\to C))\to C\vdash A\lor(A\to C)}}\qquad\lower3em\hbox{\dfrac{}{C\vdash C}}}{\dfrac{(A\lor(A\to C))\to C\vdash C}{\vdash((A\lor(A\to C))\to C)\to C}}$$

(There is an implicit contraction near the end.)