# How to show $\vdash (\neg\neg p \rightarrow p)$.

Given these axioms: where $\phi, \psi, \theta$ are formulas

$$1.:(\psi \rightarrow (\theta \rightarrow \psi))$$ $$2.: ((\neg \psi \rightarrow \neg \theta) \rightarrow (\theta \rightarrow \psi))$$

And using the deduction theorem.

So I started with trying to show that $\neg\neg p \vdash p$ (so I can use deduction theorem later).

From this:

1.$\neg\neg p$ Assumption

2.$(\neg\neg p \rightarrow (\neg\neg p \rightarrow \neg \neg p))$ Axiom #1

3.$(\neg \neg p \rightarrow \neg \neg p)$ 1,2 MP.

4.$((\neg \neg p \rightarrow \neg \neg p) \rightarrow (\neg p \rightarrow \neg p))$ Axiom #2

5.$(\neg p \rightarrow \neg p)$ 3, 4 MP.

6.$((\neg p \rightarrow \neg p) \rightarrow (p \rightarrow p))$ Axiom #2

7.$(p\rightarrow p)$ 5,6 MP.

I'm stuck here though, I have no idea how to proceed any further... Any hints?

• I'm confused. What are you asking about, is it $\neg\neg p \vdash p$ or $\vdash \neg\neg p \to p$? And do you want a formal proof or can you use the deduction theorem? Edit: Nevermind, I understood now. You want a formal proof of $\neg\neg p \vdash p$ to later use the deduction theorem to construct a formal proof of $\vdash \neg\neg p \to p$. – Git Gud Oct 1 '14 at 2:28
• I do apologize, it's my first time taking a course in logic. I'm asking about $\vdash (\neg\neg p \rightarrow p)$. From my understanding, the deduction theorem says: $\vdash (\neg\neg p \rightarrow p)$ iff $\neg\neg p \vdash p$ correct? So I thought if you can show that $\neg\neg p \vdash p$ then that means $\vdash \neg \neg p \rightarrow p$ but it seems as that's not the case. – Raymond Oct 1 '14 at 2:33
• You are correct and that is exactly the case. But meta-proving $\vdash \neg \neg p \rightarrow p$ is not the same as giving a formal proof of $\vdash \neg \neg p \rightarrow p$. Now I'm confused again as whether to you want a formal proof or not. – Git Gud Oct 1 '14 at 2:35
• I apologize then, if that's the case. I do want some sort of a formal proof using the deduction theorem and the 2 axioms. EDIT: Also thank you for clarifying that meta-proving $\vdash (\neg\neg p \rightarrow p)$ is not the same as giving a formal proof of $\vdash (\neg\neg p \rightarrow p)$! – Raymond Oct 1 '14 at 2:36
• Wait. Can I clarify something? If I show that $\neg\neg p \vdash p$, then can I use the deduction theorem to deduce that $\vdash (\neg\neg p \rightarrow p)$? If so, then yes. That's what I wanted to do in the first place. – Raymond Oct 1 '14 at 2:42

$$\neg \neg p \rightarrow (\neg \neg \neg \neg p \rightarrow \neg \neg p)$$ $$\neg \neg \neg \neg p \rightarrow \neg \neg p$$ $$(\neg \neg \neg \neg p \rightarrow \neg \neg p)\rightarrow (\neg p \rightarrow \neg \neg \neg p)$$ $$\neg p \rightarrow \neg \neg \neg p$$ $$(\neg p \rightarrow \neg \neg \neg p)\rightarrow (\neg\neg p \rightarrow p)$$ $$\neg\neg p \rightarrow p$$ $$p$$
• Summary in words, for those to whom it's helpful: From the assumed truth of $\lnot \lnot p$ you can deduce $\lnot \lnot \lnot \lnot p \to \lnot \lnot p$. From there, apply the contrapositive rule twice to peel off two layers of negation (and reverse the direction of implication twice, a no-op), giving you $\lnot \lnot p \to p$. From this and the assumed truth of $\lnot \lnot p$, deduce $p$. By the deduction theorem, if you can prove $c$ assuming $h$, you can also prove $h \to c$. – Jonas Kölker Aug 19 '17 at 11:12