More precisely, the axioms of Dedekind arithmetic assert (1) zero is not a successor; (2) the successor operation is one-to-one, meaning that S x = Sy exactly when x = y; and (3) every number is eventually generated from 0 by the application of the successor operation, in the sense that every collection A of numbers containing 0 and closed under the successor operation contains all the numbers. This is the second-order induction axiom, which is expressed in second-order logic because it quantifies over arbitrary sets of natural numbers.
