In 1889, the Italian mathematician Giuseppe Peano — also a logician, also the inventor of much modern mathematical notation (∈, ∪, ∩, ∃) — published a thirty-six-page Latin booklet titled Arithmetices principia, nova methodo exposita. In it, Peano did something nobody had quite done before: he wrote down a small set of axioms from which all of arithmetic could, in principle, be derived. The natural numbers, until that moment, had been informal — universally understood, but never formally pinned down. After Peano, they were axiomatic — defined precisely enough that proofs about them could be checked mechanically.
Peano's axioms have a striking economy. There is a starting element, conventionally zero, which is not the successor of any other element; every element has a unique successor; distinct elements have distinct successors; and there is a principle of mathematical induction saying that any property that holds at zero and is preserved under taking successors holds for every natural number. From this small kit, all of arithmetic falls out. Addition is defined recursively from successor — n + 0 = n, n + S(m) = S(n + m) — and multiplication, order, and the familiar laws of commutativity, associativity, and distributivity all follow by induction. The natural numbers, informal until 1889, were after Peano axiomatic — defined precisely enough that any proof about them could in principle be checked by a machine, and embedded inside set theory as the von Neumann ordinals where each integer is the set of its predecessors and the successor of n is n ∪ {n}.
The deeper story comes from the difference between two readings of the induction axiom. Second-order Peano arithmetic, in which induction quantifies over all properties, is categorical — any two models are isomorphic, so the axioms genuinely pin down the natural numbers up to relabelling. First-order Peano arithmetic, in which induction is restricted to formulae of the language, is weaker; it admits non-standard models containing infinite "natural numbers" larger than every standard one. The first-order theory is the one that became Gödel's target. Because Peano arithmetic is rich enough to encode statements about itself, Gödel's incompleteness theorems apply directly: no consistent extension can prove every true arithmetic statement, and no such system can prove its own consistency. PA is the canonical example of a formal system whose internal expressive power generates its own limitations, and the axiomatic style Peano introduced — start with a small set of axioms, derive everything else mechanically — has since become the standard practice in mathematics, from group theory to topology to the way modern theorem provers like Coq, Lean, and Agda implement inductive types as primitives.
Functional programming languages often define natural numbers Peano-style: in Haskell, `data Nat = Zero | Succ Nat` is a literal transcription of axioms (1)–(2), and recursive definitions of addition and multiplication follow Peano's recipe. Theorem provers — Coq, Lean, Isabelle, Agda — implement Peano-like inductive types as primitives, with the induction principle as a derivation rule. Reverse mathematics studies which axioms beyond Peano are necessary to prove which theorems of analysis. The axiomatic foundation tradition that Peano started has become the standard practice in mathematics; everything from group theory to topology now starts with axioms in his style, and the discipline of checking that all the axioms are needed and sufficient has shaped modern mathematical exposition.