Im Jahr 1889 veröffentlichte der italienische Mathematiker Giuseppe Peano — zugleich Logiker, zugleich Schöpfer eines großen Teils der modernen mathematischen Notation (∈, ∪, ∩, ∃) — ein sechsunddreißigseitiges lateinisches Heftchen mit dem Titel Arithmetices principia, nova methodo exposita. Darin tat Peano etwas, was vor ihm noch niemand so getan hatte: er schrieb eine kleine Menge von Axiomen nieder, aus denen sich die gesamte Arithmetik im Prinzip herleiten ließe. Die natürlichen Zahlen waren bis dahin informell gewesen — überall verstanden, nirgends formal festgehalten. Nach Peano waren sie axiomatisch — so präzise gefasst, dass Beweise über sie maschinell prüfbar wurden.
Peanos Axiome haben eine eindrucksvolle Sparsamkeit. Es gibt ein Anfangselement, üblicherweise null, das von keinem anderen Element Nachfolger ist; jedes Element hat einen eindeutigen Nachfolger; verschiedene Elemente haben verschiedene Nachfolger; und es gibt das Prinzip der vollständigen Induktion, das besagt: jede Eigenschaft, die bei null gilt und unter dem Nachfolgerübergang erhalten bleibt, gilt für jede natürliche Zahl. Aus diesem kleinen Werkzeugkasten fällt die ganze Arithmetik heraus. Die Addition wird rekursiv aus dem Nachfolger definiert — n + 0 = n, n + S(m) = S(n + m) — und Multiplikation, Ordnung sowie die vertrauten Gesetze von Kommutativität, Assoziativität und Distributivität folgen per Induktion. Die natürlichen Zahlen, bis 1889 informell, waren nach Peano axiomatisch — präzise genug gefasst, dass sich jeder Beweis über sie im Prinzip von einer Maschine prüfen lässt, und in der Mengenlehre als von-Neumann-Ordinalzahlen einbettbar, in denen jede ganze Zahl die Menge ihrer Vorgänger ist und der Nachfolger von n gerade n ∪ {n} lautet.
Die tiefere Geschichte sitzt im Unterschied zwischen zwei Lesarten des Induktionsaxioms. Zweite Stufe der Peano-Arithmetik, in der die Induktion über alle Eigenschaften quantifiziert, ist kategorisch — je zwei Modelle sind isomorph, die Axiome legen die natürlichen Zahlen bis auf Umbenennung wirklich fest. Die erste Stufe, in der die Induktion auf Formeln der Sprache eingeschränkt wird, ist schwächer; sie lässt Nichtstandard-Modelle zu, in denen unendliche „natürliche Zahlen“ vorkommen, die größer sind als jede Standardzahl. Die Theorie erster Stufe wurde Gödels Ziel. Weil die Peano-Arithmetik reich genug ist, um Aussagen über sich selbst zu codieren, greifen Gödels Unvollständigkeitssätze unmittelbar: keine widerspruchsfreie Erweiterung beweist jede wahre arithmetische Aussage, und kein solches System beweist die eigene Widerspruchsfreiheit. PA ist das kanonische Beispiel eines formalen Systems, dessen innere Ausdruckskraft die eigenen Grenzen erzeugt, und der axiomatische Stil, den Peano einführte — beginne mit einer kleinen Menge von Axiomen, leite alles Weitere mechanisch ab —, ist seither die gängige Praxis der Mathematik geworden, von der Gruppentheorie bis zur Topologie und bis dahin, wie moderne Theorembeweiser à la Coq, Lean und Agda induktive Typen als Primitive einbauen.
Funktionale Programmiersprachen definieren natürliche Zahlen oft im Peano-Stil: in Haskell ist `data Nat = Zero | Succ Nat` eine wörtliche Übertragung der Axiome (1)–(2), und rekursive Definitionen von Addition und Multiplikation folgen Peanos Rezept. Theorembeweiser — Coq, Lean, Isabelle, Agda — bauen peano-artige induktive Typen als Primitive ein, mit dem Induktionsprinzip als Ableitungsregel. Die umgekehrte Mathematik fragt, welche Axiome jenseits von Peano nötig sind, um welche Sätze der Analysis zu beweisen. Die Tradition des axiomatischen Fundaments, die Peano in Gang setzte, ist zu der Praxis der Mathematik geworden; alles von der Gruppentheorie bis zur Topologie startet heute mit Axiomen in seinem Stil, und die Disziplin, zu prüfen, dass alle Axiome nötig und hinreichend sind, hat die moderne mathematische Darstellung geprägt.