# Given p, how do I use the Fitch system to prove $\neg \neg p$?

Given p, how do I use the Fitch system to prove $\neg \neg p$?

I thought it should be as simple as assuming the negative, introducing a contradiction and eliminating the negation to end up with $\neg \neg p$, but I can't even get to step 3 with the Stanford Fitch system:

1) $p$ ---------------------premise
2) | $\neg p$ -----------------assumption
3) | $p \implies \neg p$ -------implication introduction 1,2
4) $\neg \neg p$ -----------------negation elimination 3

Obviously I am not quite getting it with the Fitch system, so any explanation would be greatly appreciated. It does seem trivially obvious that $p \Leftrightarrow \neg \neg p$ but I am having trouble expressing this with Fitch:

1) $p$ ---------------------premise
2) | $\neg p$ -----------------assumption
3) | $p$ -------------------reiteration 1
4) $\neg p \implies p$ ---------implication introduction 2,3

...from here tho, I can't figure out how to get $p \implies \neg p$ which I assume would which along with 4 I think would give me what I need to get $\neg \neg p$ from the negation elimination.

• The Nat Deduction proof is: assume $p$ and assume $\lnot p$. Derive a contradiction (usually symbolized with $\bot$) and then apply "negation" introduction to derive $\lnot \lnot p$, discharging assumption $\lnot p$. Conclude with $\to$-intro. Details can depend on the implementation... – Mauro ALLEGRANZA Apr 28 '17 at 6:18
• In "usual" implementation of Nat Ded the negation-intro rule is: from $\Gamma, \varphi \vdash \bot$, derive: $\Gamma \vdash \lnot \varphi$. – Mauro ALLEGRANZA Apr 28 '17 at 6:32
• Other forms can be : from $\Gamma, \varphi \vdash \psi$ and $\Gamma, \varphi \vdash \lnot \psi$, derive $\Gamma \vdash \lnot \varphi$. – Mauro ALLEGRANZA Apr 28 '17 at 6:34
• @MauroALLEGRANZA how would I squeeze that into Fitch? – Mr. Kennedy Apr 28 '17 at 6:49
• If the rule you are allowed to use is the second one, the proof must be (i) $p, \lnot p \vdash p$, (ii) $p, \lnot p \vdash \lnot p$ and then apply the rule to conclude with: $p \vdash \lnot \lnot p$. – Mauro ALLEGRANZA Apr 28 '17 at 6:52

You're so close! Here's how to proceed:

1) $p$ ---------------------premise
2) | $\neg p$ -----------------assumption
3) | $p$ -------------------reiteration 1
4) $\neg p \implies p$ ---------implication introduction 2-3
5) | $\neg p$ -----------------assumption
6) | $\neg p$ -------------------reiteration 5
7) $\neg p \implies \neg p$ -------implication introduction 5-6
8) $\neg \neg p$ ----------------negation introduction 4,7

• Thanks - I'm glad to see I was at least on the right track. Color me obtuse, but steps 5 and 6 just seem ...very counter-intuitive. Any resources you could recommend on getting proficient with the Fitch System? The Stanford online course gives a very cursory explanation prior to throwing a bunch of problems at the student and I am having trouble getting a feel for it. – Mr. Kennedy Apr 28 '17 at 20:02
• @Mr.Kennedy Yeah, formal proofs can certainly be that way: you'd think it would be all logical ... and yet sometimes you have to do these weird moves to make it fir the formal 'straightjacket' of formal logic. Unfortunately, there is really just only 1 way to get good at these: do lots of them, and build up your 'repertoire' of strategies and common proof patterns. – Bram28 Apr 28 '17 at 20:07
• thanks, I'm nowhere near anyone that uses formal logic, so I appreciate your comments. The Stanford course is fine for being free and all, but a little frustrating for lack of instruction... Also the discussion forum there has not been a great resource, but hey, I wanted to get to know Fitch - thank goodness for stack exchange! – Mr. Kennedy Apr 28 '17 at 21:03
• Interesting... reworking the proof with the Stanford tool it seems step 6 is redundant as it allows implication introduction with just the assumption of 5... But the essential point seems to be that where phi implies psi and not psi, a negation of phi can be introduced...? Neither this nor sub-proof/super-proof relationships are very clearly explained in the course... – Mr. Kennedy Apr 29 '17 at 5:44
• @Mr.Kennedy Yes, the first step of a subproof can be regarded as the last step of a subproof as well, so Reiteration would indeed be unnecessary. It does help readability though I think. – Bram28 Apr 29 '17 at 11:38

\begin{align} (1) & \quad P & \text{Assumption} \\ (2) & \quad \quad \lnot P & \text{Assumption} \\ (3) & \quad \lnot \lnot P & \text{Contradiction of } 1,2 \\ (4) & P \implies \lnot \lnot P & \implies-\text{Intro} \end{align}

• Is 3 a contradiction of 1,2? It is a contradiction of 2, certainly, but I'm not following how you derive this, nor how you would derive $\neg \neg p$ from 1-4. Can you elaborate? Thanks! – Mr. Kennedy Apr 28 '17 at 20:04
• @Mr.Kennedy 3 is obtained by a proof by contradiction kind of rule just as in my proof above: since the assumption of $\neg P$ 2 leads to a contradiction with the $P$ in 1, we can reject the assumption of $\neg P$, and thus obtain $\neg \neg P$ in 3, and thus by conditional introduction obtain 4 from the subproof 1-3. But: this proof uses rules that are different from the Stanford rules. They're valid rules, but not how they are formally defined in your formal proof system. – Bram28 Apr 28 '17 at 20:11
• @Mr.Kennedy 3 is obtained from the rule $\dfrac{ a \vdash \{b, \lnot b\} } {\lnot a}$ , it just happens in this case $a = b = p$, and $b$ and $a$ are the same reference. – DanielV Apr 29 '17 at 4:34