Prove that $\vdash A\to \lnot\lnot A$

By Deduction Rule we know that it is sufficient to show that ${A}\vdash \lnot\lnot A$

I am also familiar with the formula: $\lnot A \vdash (A\to B)$. So if I set $B:= \lnot\lnot A$ I get: $$\lnot A\to (A\to \lnot\lnot A)$$

I could use $MP$ but I assumed before $A$ and not $\lnot A$.

I'd be glad for help

  • $\begingroup$ Are you using natural deduction or other proof systems ? $\endgroup$ – Mauro ALLEGRANZA Mar 28 '16 at 13:35
  • $\begingroup$ It's Hilbert Calculus. $\endgroup$ – Arbel Mar 28 '16 at 13:39
  • 1
    $\begingroup$ See Elliott Mendelson, Introduction to Mathematical Logic (6th ed 2015), page 31. $\endgroup$ – Mauro ALLEGRANZA Mar 28 '16 at 13:51
  • $\begingroup$ @Arbel: "Hilbert calculus" is not one thing -- rather, it is a family of proof systems that have some similarities, but different details in how their axioms are chosen -- in particular, there are several different (but equivalent) ways to deal with negation. So you need to reveal exactly which logical axioms you have before you can hope to get a relevant answer. $\endgroup$ – Henning Makholm Mar 28 '16 at 14:18
  • $\begingroup$ I guess natural deduction (since wasn't mentioned otherwise) $\endgroup$ – Arbel Mar 28 '16 at 14:21

Let's rewrite $\neg A$ as $A \to \bot$. Then $\neg \neg A$ is $(A \to \bot)\to \bot$. You eliminate the implication, and get $A, A \to \bot \vdash \bot$. You need to prove false, and you have both $A$ and that $A$ implies false.

  • $\begingroup$ I didn't quite understand what you did here $\endgroup$ – Arbel Mar 28 '16 at 14:04
  • $\begingroup$ You don't say much on the system you are working on, but usually (at least often) $\neg A$ is defined as being syntactic sugar for $A \to \bot$. Or is it something else that you don't understand? If you just rewrite $\neg \neg A$ as above, then there are not to many rules that you can apply to complete the proof. $\endgroup$ – Graffitics Mar 28 '16 at 14:13
  • $\begingroup$ @Graffitics: Treating $\neg A$ as an abbreviation for $A\to\bot$ is not unusual, but it is on the other hand not so universal that you can simply assume that it will be the case in the (undisclosed) formalization the OP uses. $\endgroup$ – Henning Makholm Mar 28 '16 at 14:20
  • $\begingroup$ @HenningMakholm You are completely right, but sometimes asking for the OP to ask a well-formed question is actually harder than to answer it and get him to collect the pieces together (because he may not understand how it's not well-formed, and you go down the rabbit hole). In this case it seemed easier to go this way, but it apparently it was a wrong assumption. $\endgroup$ – Graffitics Mar 28 '16 at 14:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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