 As is well known, \(\mathbf{FO}\) admits of a sound and complete proof procedure: there is a mechanical way of generating precisely those first-order sentences that are valid (true in all models). This fact can also be expressed by saying that \(\mathbf{FO}\) is axiomatizable, or that the set of valid sentences of \(\mathbf{FO}\) is recursively  enumerable.[45]  Due to its greater expressive power, axiomatizability fails for \(\mathbf{IFL}\). In other words, \(\mathbf{IFL}\) is semantically  incomplete.[46]