Though quite common, Z \(_{2}\) is only one possible version of Peano Second-Order Arithmetic. Another common version—which we could call ‘ \(\mathsf {PA}_{2}^{\mathsf {D}}\) ’, for brevity’s sake—results from adopting a system \(\mathsf {L}_{2}^{\mathsf {D}}\) of full second-order logic including identity for terms, both monadic and dyadic predicate variables, and parameters in comprehension, and extending it though the admission of three proper axioms involving no more than two non-logical constants: the individual constant ‘ \(\mathbf {0}\) ’, obviously denoting zero, and the functional constant ‘ \(^{\prime }\) ’, taking whatever term and giving a term, and designating the successor function.