 \(\mathbf{IPC}\) is effectively decidable. There is a recursive procedure which determines, for each propositional formula \(E,\) whether or not \(E\) is a theorem of \(\mathbf{IPC},\) concluding with either a proof of \(E\) or a (finite) Kripke countermodel. 