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

Question

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?

Answer 1

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 ^_^