Proving $\lnot \lnot (\psi \lor \lnot \psi)$ is a theorem of intuitionistic propositional logic

Question

Here, $\psi$ is some arbitrary formula.

The proof I've come up with is as follows.

Assume $\lnot \lnot (\psi \lor \lnot \psi)$ is not a theorem of IPL, which means there exists some Kripke model where

$$\exists w: w \not\models \lnot \lnot (\psi \lor \lnot \psi),$$

which, by definition of negation being truthful in Kripke models, is equivalent to

$$\exists w: \exists u \geq w: u \models \lnot (\psi \lor \lnot \psi).$$

This, again by definition of negation truthfulness, implies for this $u$ that

$$\forall v \geq u : v \not \models \psi \lor \lnot \psi.$$

By definition of truthfulness of $\lor$ in Kripke models, this, in turn, implies

$$\forall v \geq u : v \not \models \psi, v \not \models \lnot \psi.$$

But if $\forall v \geq u : v \not \models \psi$, then $u \models \lnot\psi$, which contradicts $\forall v \geq u : v \not \models \lnot \psi$.

Hence, the original assumption is false, and $\lnot \lnot (\psi \lor \lnot \psi)$ is a theorem of IPL.

Is this reasoning correct?

Answer 1

To prove $\lnot \lnot (P \lor \lnot P)$, assume $\lnot (P \lor \lnot P)$ and show that it leads to a contradiction.

Under that assumption, you can show both $\lnot P$ holds by contradiction as well as $\lnot \lnot P$ holds, which is the desired contradiction. In long form:

$$ \begin{array} {rl} % Markup \begin{array} {r} \begin{array} {r|} \text{Assumption } \\ \hline \begin{array} {r|} \text{Assumption } \\ \hline \text{Or Intro } \\ \text{Contradiction } \\ \end{array} \\ \text{Negation Intro } \\ \begin{array} {r|} \text{Assumption } \\ \hline \text{Or Intro } \\ \text{Contradiction } \\ \end{array} \\ \text{Negation Intro } \\ \text{Contradiction } \\ \end{array} \\ \text{Negation Intro } \end{array} & % Proof \begin{array} {l} \begin{array} {|l} \lnot (P \lor \lnot P) \\ \hline \begin{array} {|l} P \\ \hline P \lor \lnot P \\ \bot \\ \end{array} \\ \lnot P \\ \begin{array} {|l} \lnot P \\ \hline P \lor \lnot P \\ \bot \\ \end{array} \\ \lnot \lnot P \\ \bot \\ \end{array} \\ \lnot \lnot (P \lor \lnot P) \end{array} % End Proof \end{array}$$