1

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

Arbel
  • 23
  • 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
  • 1
    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. – hmakholm left over Monica Mar 28 '16 at 14:18
  • I guess natural deduction (since wasn't mentioned otherwise) – Arbel Mar 28 '16 at 14:21
  • @Arbel: "Natural dediction" is not exactly one thing either -- but what it is is defintely not the same thing as a Hilbert-style system. Instead of guessing wildly at names, you need to show us which rules you have. There's no substitute for showing the actual rules in all their symbolic glory; the names a particular textbook uses are not so standardized that anyone can reconstruct the rules just from hearing the name of a system. – hmakholm left over Monica Mar 28 '16 at 14:23
  • We have the three known axioms, the only rule is "Modus-Ponus", and the predicates are ${\lnot, \leftrightarrow }$ – Arbel Mar 28 '16 at 14:42
  • In the answer to this post you can find the proof with the three-axioms Mendelson's system (based on $\lnot, \to$) and Modus Ponens. – Mauro ALLEGRANZA Mar 28 '16 at 14:49

1 Answers1

1

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.

Graffitics
  • 1,508
  • I didn't quite understand what you did here – Arbel Mar 28 '16 at 14:04
  • 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. – hmakholm left over Monica Mar 28 '16 at 14:20
  • @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. – Graffitics Mar 28 '16 at 14:45