Proving the Glivenko theorem via Kripke models

We'll prove it in just one direction, since the other one is obvious. So, assume $\psi$ is a theorem of classical propositional logic. Prove that $\lnot \lnot \psi$ is a theorem of intuitionistic propositional logic.

My proof sketch is as follows. Assume $\lnot \lnot \psi$ is not a theorem of IPL. Then there exists a Kripke model (with a finite worlds count) such that within that model $$\exists w : w \not \Vdash \lnot \lnot \psi,$$ implying $$\exists u \geq w : u \Vdash \lnot \psi,$$ implying again $$\exists u \geq w : \forall v \geq u : v \not \Vdash \psi.$$

Since the model we're in is finite, there exists some maximal world $\mu \geq u$, in which, by assumption, $\mu \not \Vdash \psi$. Since this world is maximal, the definitions of truthfulness for $\rightarrow, \lnot$ decay to the classical ones, and the values of the propositional variables in this world can naturally be viewed as a counterexample to $\psi$, which is a tautology and hence has no counterexamples! So, contradiction, and our original assumption is invalid.

Does this sound like a reasonable approach?

I can already prove the theorem by using (1) that $\lnot \lnot (\psi \lor \lnot \psi)$ is a theorem if IPL and (2) that if $\lnot \lnot \phi$ and $\lnot \lnot (\phi \rightarrow \psi)$ are theorems of IPL, then $\lnot \lnot \psi$ is too, so using these two facts I can rewrite any derivation of $\psi$ in CPL to a derivation of $\lnot \lnot \psi$ in IPL, but personally I find Kripke models more straightforward, hence the question.

• Yes, that works. The key thing you need here is that the logic has the finite model property but you seem to be consciously using that fact. – spaceisdarkgreen Jun 3 '18 at 21:26
• The syntactic proof has the nice property that it immediately applies if we consider a sublanguage of an intuitionistic first-order logic, and it's easy to add the case for $\exists$ and extend the syntactic proof to all of the first-order logic. The semantic proof, on the other hand, would essentially have to be completely redone. Also, the syntactic proof is directly constructive, while the semantic proof that you've given is only constructive paired with a constructive completeness proof, i.e. it doesn't actually (directly) tell you what the intuitionistic proof of $\neg\neg\psi$ is. – Derek Elkins Jun 3 '18 at 22:09