 Propositional Kripke semantics is particularly simple, since an arbitrary propositional formula is intuitionistically provable if and only if it is forced by the root of every Kripke model whose frame (the set \(K\) of nodes together with their partial ordering) is a finite tree with a least element (the root). For example, the Kripke model with \(K = \{k, k', k''\}, k \lt k'\) and \(k \lt k'',\) and with \(P\) true only at \(k',\) shows that both \(P \vee \neg P\) and \(\neg P \vee \neg \neg P\) are unprovable in \(\mathbf{IPC}.\)