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?

  • 1
    $\begingroup$ 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$. $\endgroup$ – Git Gud Oct 1 '14 at 2:28
  • $\begingroup$ 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. $\endgroup$ – Raymond Oct 1 '14 at 2:33
  • $\begingroup$ 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. $\endgroup$ – Git Gud Oct 1 '14 at 2:35
  • $\begingroup$ 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)$! $\endgroup$ – Raymond Oct 1 '14 at 2:36
  • 2
    $\begingroup$ 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. $\endgroup$ – 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$$

  • $\begingroup$ Wow, that's something I didn't expect. Thank you! $\endgroup$ – Raymond Oct 1 '14 at 2:54
  • $\begingroup$ 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$. $\endgroup$ – Jonas Kölker Aug 19 '17 at 11:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.