# HPC: Prove that $\vdash A\to \lnot\lnot A$

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$.

• Are you using natural deduction or other proof systems ? – Mauro ALLEGRANZA Mar 28 '16 at 13:35
• It's Hilbert Calculus. – Arbel Mar 28 '16 at 13:39
• See Elliott Mendelson, Introduction to Mathematical Logic (6th ed 2015), page 31. – Mauro ALLEGRANZA Mar 28 '16 at 13:51
• @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. – Henning Makholm Mar 28 '16 at 14:18
• I guess natural deduction (since wasn't mentioned otherwise) – 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.
• 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. – Graffitics Mar 28 '16 at 14:13
• @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. – Henning Makholm Mar 28 '16 at 14:20