 The metalogical properties of \(\mathbf{IFL}\) have been discussed in several publications, by Hintikka as well as  Sandu.[32]  When presenting them, reference will be made to existential second-order logic  \((\mathbf{ESO})\);[33]  further important notions are those of the skolemization and Skolem normal form of an \(\mathbf{IFL}\) formula. For precise definitions of these notions,  the supplementary document  can be consulted. In brief, \(\mathbf{ESO}\) is obtained from \(\mathbf{FO}\) by allowing existential quantification over relation and function symbols in a first-order formula. The skolemization \(\mathrm{sk}[\phi]\) of an \(\mathbf{IFL}\) formula \(\phi\) is a first-order formula of a larger vocabulary. It explicates in terms of function symbols how existential quantifiers and disjunction symbols of \(\phi\) depend on preceding universal quantifiers. For example, a skolemization of the \(\mathbf{IFL}\) sentence \(\phi = (\forall x)(\exists y)(\forall z)(\exists v/\forall x)R(x, y, z, v)\) of vocabulary \(\{R\}\) is the \(\mathbf{FO}\) sentence \(\mathrm{sk}[\phi] = (\forall x)(\forall z)R(x, f(x), z, h(z))\) of vocabulary \(\{R, f, h\}\). Its Skolem normal form, again, is the \(\mathbf{ESO}\) sentence \(\mathrm{SK}[\phi] = (\exists f)(\exists h)(\forall x)(\forall z)R(x, f(x), z, h(z))\). The first-order sentence \(\mathrm{sk}[\phi]\) must not be confused with the second-order sentence \(\mathrm{SK}[\phi]\). 