In Intuitionistic Kripke semantics, is proving a formula not forced at one node the same as proving it not derivable/invalid

intuitionistic-logiclogicproof-explanation

I am having trouble understanding whether proving a formula not forced at one node in Kripke semantics is the same as proving that it is not derivable/invalid in Intuitionistic logic.

For example, consider the following diagram from van Dalan's Logic and Structure. $k_0 \not\Vdash \varphi \lor \lnot \varphi$ because $k_0 \not\Vdash \varphi$ and also $k_0 \not\Vdash \lnot\varphi$ since $\exists y \gt k_0$ st $y\Vdash \varphi$.

What I am not sure of is whether this constitute a proof that the law of excluded middle is invalid in Intuitionistic logic (IL). Because this is only one frame among possibly infinitely many in IL, surely just because we can prove that it is false at one node in a frame does not extend that to all frames surely?

And if this is not the way to do it, how do we do it?

enter image description here

Best Answer

In general, a formula is not forced by a given node of a frame does not mean it is not forced by any node of arbitrary frames.

Despite that, just finding a frame which does not satisfy a given formula is sufficient to show the unprovability. This is due to the contraposition of the soundness theorem of Kripke frames:

Soundness Theorem. Let $(P,\le,\Vdash)$ be a frame and $p\in P$ be a node. If $\phi$ be a theorem of intuitionistic logic then $p\Vdash\phi$.

Therefore, if $p\nVdash\phi$ for some frame $(P,\le,\Vdash)$ and a node $p\in P$, then $\phi$ is not a theorem of intuitionistic logic. Of course, we do not need to find any other frames if we have already found a frame witnessing the unprovability.

Related Question