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

179 Views Asked by At

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

1

There are 1 best solutions below

4
On BEST ANSWER

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.