Proving $\lnot \lnot (\psi \lor \lnot \psi)$ is a theorem of intuitionistic propositional logic 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?
 A: 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}$$
