 where the arity of Y is one higher than the arity of X, and \(\phi'\) is obtained from \(\phi\) by replacing everywhere \(X(t_1,\ldots,t_n)\) by \(Y(x,t_1,\ldots,t_n)\), one can bring every second-order logic formula to a logically equivalent normal form 