# 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. – chiaroscuro 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? – chiaroscuro 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!

-
There exists a 12 step condensed detachment proof for this problem: math.stackexchange.com/questions/1466226/… – Doug Spoonwood Oct 8 '15 at 23:36
Does your last line mean that you prefer natural deduction? If so, I fully agree with you! Better still, Fitch-style natural deduction, which would eliminate a lot of students' logical errors in all areas of mathematics if followed. – user21820 Oct 12 '15 at 2:15

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