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$.)


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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.