 One way to show this is as follows. Suppose for the sake of contradiction that the set of valid \(\mathbf{IFL}\) sentences is recursively enumerable. Recall that the sentence \(\phi_{inf}\) discussed in Subsection 4.1 is true in all and only infinite models. Note, then, that an \(\mathbf{FO}\) sentence \(\chi\) is true in all finite models iff the \(\mathbf{IFL}\) sentence \((\phi_{inf} \vee \chi)\) is valid. Given a valid \(\mathbf{IFL}\) sentence, it can be effectively checked whether the sentence is syntactically of the form \((\phi_{inf} \vee \chi)\), where \(\chi\) is a first-order sentence. Hence the recursive enumeration of all valid \(\mathbf{IFL}\) sentences yields a recursive enumeration of first-order sentences \(\chi\) true in all finite models. But this contradicts Trakhtenbrot’s theorem, according to which the set of \(\mathbf{FO}\) sentences true in all finite models is not recursively  enumerable.[47]