 The validity and satisfiability problems of the full second-order can be effectively reduced to the corresponding problems concerning \(\mathbf{EIFL}\). Namely, why cannot a second-order sentence simply be thought of as a two-sorted first-order sentence? Because in order to capture the standard interpretation of second-order  logic,[63]  it must be said that for every extensionally possible set of \(n\)-tuples of elements of sort 1 there exists a member of sort 2 having those and only those elements as members, for all arities \(n\) such that the second-order sentence contains a quantifier \((\exists R)\) where \(R\) is  \(n\)-ary.[64]  Now, such additional conditions can be expressed by a finite conjunction \(X\) of \(\mathbf{USO}\) sentences, where \(\mathbf{USO}\) (universal second-order logic) is obtained from \(\mathbf{FO}\) by allowing universal quantification over relation and function symbols in a first-order formula. Each of these \(\mathbf{USO}\) sentences can be expressed as the contradictory negation of an \(\mathbf{ESO}\) sentence and therefore as the contradictory negation of an \(\mathbf{IFL}\) sentence. Consequently, there is an \(\mathbf{IFL}\) sentence \(Y\) such that \(X\) itself is logically equivalent to \(\neg Y\). And here \(\neg Y\) is a sentence of \(\mathbf{EIFL}\). Therefore, if \(\phi\) is a second-order sentence and \(\phi^*\) its reconstruction in two-sorted first-order logic, we have: \(\phi\) is satisfiable iff \((X \wedge \phi^*)\) is satisfiable iff \((\neg Y \wedge \phi^*)\) is satisfiable. And: \(\phi\) is valid iff \(\phi^*\) is a logical consequence of \(X\) iff \((\neg X \vee \phi^*)\) is valid iff \((Y \vee \phi^*)\) is valid. Here, both \((\neg Y \wedge \phi^*)\) and \((Y \vee \phi^*)\) are sentences of \(\mathbf{EIFL}\), the latter even a sentence of \(\mathbf{IFL}\). It follows that the satisfiability (validity) of any second-order sentence can be expressed as the satisfiability (respectively, validity) of a sentence of  \(\mathbf{EIFL}\).[65]