 Any higher-order mathematical theory \(T\) gives rise to a many-sorted first-order theory \(T^*\). If the theory is finite, there is a finite conjunction \(J\) formulated in \(\mathbf{EIFL}\) – equivalent to a sentence of \(\mathbf{USO}\) and therefore equivalent to the contradictory negation of an \(\mathbf{ESO}\) sentence and so indeed equivalent to the contradictory negation of an \(\mathbf{IFL}\) sentence – expressing the requirement that the standard interpretation of higher-order logic is respected. The question of the truth of the higher-order theory \(T\) is thus reduced to the truth of the sentence \((J \wedge T^*)\) of \(\mathbf{EIFL}\) (cf. Subsect. 4.6). 