 As we will see in  section 4.2,  rewriting the second order formula \(X^{2}xy\) as  \(\epsilon_{2}xyX^{2}\)  is all we do when translating second-order logic into many-sorted logic; some axioms for predicates \(\epsilon _{n}\) are added and a suitable many-sorted theory for the \(\epsilon _{n}\) relations is introduced. In many-sorted logic formula