 The most direct way to show that a formula (or schema) \(F\) is provable in a formal system \(\mathbf{S}\) is to construct a proof of \(F\) in \(\mathbf{S}.\) But if a formula (or some substitution instance of a schema) happens not to be provable in \(\mathbf{S},\) how can that fact be known? Our failure to find a proof may suggest unprovability, but is not in general decisive unless the proof search is a canonical one in Gentzen’s system for intuitionistic propositional logic. Usually what is needed is an interpretation with respect to which \(\mathbf{S}\) is sound, in the sense that every provable formula is valid under the interpretation. Then to show \(F\) unprovable in \(\mathbf{S}\) it suffices to show that \(F\) is invalid under the interpretation, typically by constructing a countermodel to \(F.\)