Annoying logical deduction

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.

-
I haven't read Mendelson, so may I ask what the base axioms are? If you have double negation and conditional proof then the problem is really easy. –  Josh Chen Jan 12 '13 at 4:52
They are precisely the 3 that I listed, where you can substitute anything for A, B and C plus apply modus ponens. –  asdf Jan 12 '13 at 6:09
And modus ponens? Or is that listed as a "rule of inference" or something like that? –  Josh Chen Jan 12 '13 at 6:21
Yes, modus ponens is the only allowed rule of inference. –  asdf Jan 12 '13 at 15:44

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.

-
Interesting. Proving things like this has been for me a total trial and error. Is there any known algorithm for this or is there a reason why everyone uses resolution? –  asdf Jan 12 '13 at 15:51
@asdf: one technique for handling negation in Hilbert systems is to leverage formulas such as $\top$ or $A\to A$ that are already provable, and then eliminate them with modus ponens, like here. The other trick is to peel off the negations one at a time. To make it easier to use modus ponens, replace $\lnot A$ with $A \to \bot$ (which you already proved is a correct rule). –  Carl Mummert Jan 12 '13 at 21:21

Why should there be a nice short proof? In Mendelson's original system, for example, the shortest proof of $P \land Q \vdash P$, with his definition of conjunction, is over 50 lines. You are discovering that axiomatic presentations of logic in this style are indeed annoying!

Natural Deduction Rules OK!

-

I may be missing something because I haven't studied yet mathematical logic to a deep level... but, if you have proved A->A, isnt ¬ a general operation such that ¬¬A is the same as A, so the proof must be the same.

-
The point is proving this fact about negation in an axiomatic formulation of propositional logic. –  asdf Jan 12 '13 at 1:05
This would be fine if $\lnot \lnot A$ were axiomatically defined as $A$; in many systems $\lnot \lnot A \to A$ is taken as an axiom. –  Carl Mummert Jan 12 '13 at 13:10