Doesn't cut elimination make intuitionistic logic equivalent to classical logic?

139 Views Asked by At

Suppose we have a proof by contradiction of $A$, meaning we've proven $(A \to \bot) \to \bot$.

If we eliminate all cuts in the proof, then the last step of the proof will be an implication elimination involving $A \to \bot$ and $A$, meaning that the proof will contain proof of $A$.

Equivalently, if we have a lambda calculus term of type $(A \to \bot) \to \bot$, then its $\beta$-normal form must be of the form $\lambda f : A \to \bot. fX$ where $X : A$.

Doesn't this mean that any proof involving double negation elimination can be rewritten (using cut elimination) to not require it?

1

There are 1 best solutions below

2
On

Intuitionistic logic does have cut elimination and is not equivalent to classical logic. I’m not sure I completely understand your remarks, but best I can tell, you are arguing the only way we can get a (hypothetical) proof of $\bot$ is to apply our proof of $A\to \bot$ to a proof of $A.$ But one problem with this argument is that this proof of $A$ need not be unconditional. The best way to proceed would probably be to examine a normal form intuitionistic proof of $\lnot\lnot(A\lor \lnot A)$ $$ \dfrac{\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{}{\hspace{5mm}A\hspace{5mm}}v}{A\lor \lnot A}\lor i\hspace{4mm} \dfrac{}{\lnot(A\lor\lnot A)}u}{\bot}\to e}{\lnot A}\to i,v}{A\lor\lnot A} \lor i\hspace{4mm} \dfrac{}{\lnot(A\lor \lnot A)}u}{\bot}\to e}{\lnot\lnot(A\lor\lnot A)}\to i ,u$$ Notice that assumption $u$ is open in the proof of $A\lor \lnot A.$

In a cut-free sequent calculus proof this double discharge may require some opportunistic use of contraction, depending on what exact system you are using. Here is the same proof in sequent calculus:

$$ \dfrac{\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{}{A\Rightarrow A}ax}{A\Rightarrow (A\lor\lnot A)}\lor R\hspace{4mm}\dfrac{}{\bot\Rightarrow\bot}ax}{\lnot(A\lor\lnot A), A\Rightarrow \bot}\to L}{\lnot(A\lor\lnot A)\Rightarrow \lnot A}\to R}{\lnot (A\lor \lnot A)\Rightarrow (A\lor \lnot A)}\lor R\hspace{4mm} \dfrac{}{\bot\Rightarrow \bot}ax}{\lnot(A\lor\lnot A),\lnot(A\lor\lnot A)\Rightarrow\bot}\to L}{\lnot(A\lor\lnot A)\Rightarrow\bot}contrL}{\Rightarrow \lnot\lnot(A\lor\lnot A)}\to R$$

Note again that at no point was $ \Rightarrow (A\lor \lnot A)$ derived, only $\lnot (A\lor \lnot A)\Rightarrow (A\lor \lnot A).$