I'm trying to show that $\vdash \neg\neg A \to A$. I can't seem to figure out the deduction. Mendelson proves this in his book, but I'm trying to use a different set of axioms. These are
$A\to (B\to A)$
$(\neg B\to \neg A)\to (A\to B)$
$(A\to (B\to C))\to ((A\to B)\to (A\to C))$
Using these axioms and modus ponens I've done a few problems in Mendelson's book, so I already have deductions for e.g.
$\neg A \to (A\to B)$
$A\to A$
Can anyone find a short proof for this? Even using the deduction theorem, I can't seem to be able to prove this.
Best Answer
Using the deduction theorem, assume $\lnot \lnot A$. By a rule you have proved, $$ \lnot (\lnot A) \to (\lnot A \to \lnot \top). $$ Thus, by modus ponens, $\lnot A \to \lnot \top$. By rule (2), $$ (\lnot A \to \lnot \top) \to (\top \to A), $$ Hence $\top \to A$, by modus ponens, and hence $A$ by modus ponens again. Thus, by the deduction theorem, $\lnot\lnot A \to A$.
If you do not have $\top$ in your language, you can replace it with any provable formula you like, e.g. $A \to A$.
By the way, the method I used to write this was to think in terms of $\lnot A \equiv A \to \bot$ and then translate that back to the language where $\lnot$ is primitive.