# Intuitionistic proof of $((p\rightarrow q)\rightarrow p)\rightarrow\neg \neg p$

I need to prove that the $$\psi=((p\rightarrow q)\rightarrow p)\rightarrow\neg \neg p$$ is intuitionistically valid. I tried using the topology of open sets of $$\mathbb{R}$$ and an arbitrary valuation, but couldn't prove that $$v(\psi)=\mathbb{R}$$ or superset of $$\mathbb{R}$$. I tried proving that $$\Gamma=\{(p\rightarrow q)\rightarrow p,\neg p \}\vdash \bot$$. Reached up to a point where $$\Gamma, p\rightarrow q\vdash \bot$$ and $$\Gamma, p\vdash \bot$$ and I was thinking that there must be formulas $$\sigma, \tau$$ s.t. $$\Gamma, p\rightarrow q\vdash \sigma$$ (or $$\Gamma, p\vdash \sigma$$) and $$\Gamma \vdash \tau$$ so that I can then use firstly use $$(\rightarrow I)$$ and then $$(\rightarrow E)$$ and prove what I want, i.e. $$\Gamma \vdash (p\rightarrow q) \rightarrow\sigma$$, $$\Gamma \vdash \tau$$ and from $$(\rightarrow E)$$, I have $$\Gamma \vdash \bot$$. However I can't think of any. Plus I haven't fully understood Kripke semantics, so I haven't tried it. It seems though that it might be easier than what I have tried since now.

Could anyone help, because my brain isn't working and I have been stuck for over two hours?

• All you need to prove is that $\neg p \vdash p \rightarrow q$. Aug 29 at 16:39
• Thanks tried both answers and worked! Aug 29 at 17:23

Here's a sketch:

We want to prove $$\cdot \vdash ((p \to q) \to p) \to \lnot \lnot p$$, which is intuitionstically the same as $$\cdot \vdash ((p \to q) \to p) \to (p \to \bot) \to \bot$$.

We can move our assumptions into the context, so it suffices to show $$((p \to q) \to p), \ (p \to \bot) \vdash \bot$$. But how can we do this? Well, we only have one way of making a $$\bot$$. We need to use modus ponens with our assumption $$(p \to \bot)$$ and some $$p$$. So we've simplifed the goal again, and we want to find a way to make a $$p$$. Of course, the only thing we have that makes a $$p$$ is modus ponens with our assumption $$((p \to q) \to p)$$, and something of type $$p \to q$$... But where can we get a $$p \to q$$?

At this point it's easy to get stuck, but remember that false implies anything! So we can freely add the axiom $$\bot \to q$$ to our context, meaning it's enough to prove

$$((p \to q) \to p), \ (p \to \bot), \ (\bot \to q) \vdash \bot$$

And now we see how to do it! We compose $$(p \to \bot)$$ and $$(\bot \to q)$$ to get a $$(p \to q)$$ in context. We use this with our $$((p \to q) \to p$$ to get a $$p$$ in context, which we use with our $$(p \to \bot)$$ to prove $$\bot$$!

I'll leave it to you to make the details precise enough for your purposes.

I hope this helps ^_^

• Argh, beat me to it. +1 Aug 29 at 16:56
• @NoahSchweber, good to see you! ^_^ Aug 29 at 17:00
• Thanks! I tried both your answer and the comment above and worked! Aug 29 at 17:23