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?