 A formula of \(\mathbf{FO}[\tau]\) is in negation normal form, if all occurrences of the negation symbol \({\sim}\) immediately precede an atomic formula. The set of formulas of IF first-order logic of vocabulary \(\tau\) (or \(\mathbf{IFL}[\tau])\) can be defined as the smallest set such that: