 Each terminal node or leaf of a Kripke model is a classical model, because a leaf forces every formula or its negation. Only those proposition letters which occur in a formula \(E,\) and only those nodes \(k'\) such that \(k\le k',\) are relevant to deciding whether or not \(k\) forces \(E.\) Such considerations allow us to associate effectively with each formula \(E\) of \(L(\mathbf{IPC})\) a finite class of finite Kripke structures which will include a countermodel to \(E\) if one exists. Since the class of all theorems of \(\mathbf{IPC}\) is recursively enumerable, we conclude that: