 Definition 1 The formulas of second-order logic are defined as follows: Atomic formulas are formulas. If \(\phi\) and \(\psi\) are formulas, then \(\neg\phi\), \(\phi\land \psi\), \(\phi\lor \psi\), \(\phi \to \psi\) and \(\phi \leftrightarrow \psi\) are formulas. If \(\phi\) is a formula, x an individual variable, X a relation variable and F a function variable, then \(\exists x\phi\), \(\forall x\phi\), \(\exists X\phi\), \(\forall X\phi, \exists F\phi\) and \(\forall F\phi\) are formulas.