Tell me more ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.
up vote 2 down vote favorite
1

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.

share|improve this question
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 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 at 6:09
And modus ponens? Or is that listed as a "rule of inference" or something like that? – Josh Chen Jan 12 at 6:21
Yes, modus ponens is the only allowed rule of inference. – asdf Jan 12 at 15:44

3 Answers

up vote 3 down vote accepted

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.

share|improve this answer
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 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 at 21:21
up vote 1 down vote

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!

share|improve this answer
up vote 0 down vote

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.

share|improve this answer
3  
The point is proving this fact about negation in an axiomatic formulation of propositional logic. – asdf Jan 12 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 at 13:10

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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