 Contradictory negation and finite models. Certain major open questions in logic and theoretical computer science can be formulated in terms of \(\mathbf{IFL}\). It is an open question in complexity theory whether \(\mathbf{NP} = \mathbf{coNP}\), that is, whether the class of \(\mathbf{NP}\)-solvable problems is the same as the class of problems whose complement is solvable in \(\mathbf{NP}\). By Fagin’s theorem (1974), this open problem can be equivalently formulated as follows: Is \(\mathbf{IFL}\) closed under negation over finite models? That is, is there for every IF sentence \(\phi\) another IF sentence \(neg(\phi)\) such that for any finite model \(M\), \(neg(\phi)\) is true in \(M\) iff \(\phi\) is not true in \(M\)? Proving that the answer is negative would settle the notorious \(\mathbf{P} = \mathbf{NP}\) problem, i.e., establish that there are computational problems for which one can efficiently verify whether a proposed solution is correct although one cannot efficiently find a  solution.[44]