 Kripke’s Soundness and Completeness Theorems establish that a sentence of \(L\) is provable in intuitionistic predicate logic if and only if it is forced by every node of every Kripke structure. Thus to show that \(\neg \forall x \neg P(x) \rightarrow \exists x P(x)\) is intuitionistically unprovable, it is enough to consider a Kripke structure with \(K = \{k, k'\},\) \(k \lt k',\) \(D(k) = D(k') = \{0\},\) \(T(P, k)\) empty but \(T(P, k') = \{0\}.\) And to show the converse is intuitionistically provable (without actually exhibiting a proof), one only needs the consistency and monotonicity properties of arbitrary Kripke models, with the definition of \(\Vdash.\)