 where \(F\approx G\) says there is a relation that one-to-one correlates the \(F\)s and the \(G\)s. The second-order theory with (HP) as an axiom is consistent and allows us to derive all of ordinary (second-order Peano-Dedekind) arithmetic, using some very natural definitions (see the entry on  Frege’s Logic, Theorem, and Foundations for Arithmetic).