202308141458

type :Example tags :

P implies not-not P - Intuitionistic Logic

---

Question: $\Gamma ⊢p\to \neg \neg p$

Answer:

The question is a shorthand for $p\to ((p\to \perp )\to \perp )$ which can be proved in the following way

$$\frac{}{⊢p\to ((p\to \perp )\to \perp )}(\to \mathcal{I})$$

---

Related