Simple proofs of intuitionistic logic - applying rules

Question

I am trying to prove many rules, but I can't start with this one:
$$p\to \neg \neg p$$. Look at my approach and try to help me:
$$\overline{p\vdash (p\to \bot)\to\bot}$$ $$\overline{p\vdash \neg (p\to \bot)}$$ $$\overline{p\vdash \neg \neg p}$$ $$\overline{\vdash p\to \neg \neg p}$$
I don't know how to finish it.

Answer 1

You have unfolded $\neg\neg p$ correctly.

You're not saying which proof system you're working in, but your punctuation looks like it's probably either (intuitionistic) sequent calculus or natural deduction. Both of these have the same rule for how to prove an implication: $$ \frac{\Gamma, A\vdash B}{\Gamma\vdash A\to B}$$ and if you apply this once to your goal gives you the conclusion of your sought-for proof: $$ \frac{\dfrac{p,\; p\to\bot \vdash \bot}{p\vdash (p\to\bot)\to \bot}}{\vdash p \to \neg\neg p} $$ How to prove the premise here differs in detail between natural deduction and sequent calculus, but in either case it is simply a matter of "plumbing" to bring the two assumptions $p\to \bot$ and $p$ together such that you can use modus ponens to conclude $\bot$.

---

In Haskell syntax, through the Curry-Howard isomorphism, the proof corresponds to

data Bot = Explode(forall a.a) -- standard representation of bottom type
type Not a = a -> Bot          -- standard abbreviation of negation

f :: p -> Not(Not p)
f :: p -> (p -> Bot) -> Bot
f = \x -> \g -> g x