Marko Rauhamaa <ma...@pacujo.net>: > Steven D'Aprano <steve+comp.lang.pyt...@pearwood.info>: > >> The contemporary standard approach is from Zermelo-Fraenkel set >> theory: define 0 as the empty set, and the successor to n as the >> union of n and the set containing n: >> >> 0 = {} (the empty set) >> n + 1 = n ∪ {n} > > That definition barely captures the essence of what a number *is*. In > fact, there have been different formulations of natural numbers.
Rehashing this old discussion. I ran into this wonderful website: <URL: http://at.metamath.org/mpeuni/mmset.html> It is an absolute treasure for those of us who hate handwaving in math textbooks. The database of computer-checked theorems proves everything starting from the very bottom. An interesting, recurring dividing line among the proofs is a layer of "provable" axioms. For example, this proof http://at.metamath.org/mpeuni/2p2e4.html (for "⊢ (2 + 2) = 4") references the axiom (<URL: http://at.metamath.org/mpeuni/ax-1cn.html>): ⊢ 1 ∈ ℂ The axiom is "justified by" a set-theoretic theorem: Description: 1 is a complex number. Axiom 2 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1cn 7963. <URL: http://at.metamath.org/mpeuni/ax1cn.html> In other words, since there is no canonical way to define numbers in set theory, Metamath insulates its proofs from a particular definition by circumscribing numbers with construction-independent axioms. Anyway, ob. Python reference: Using the design ideas implemented in Metamath, Raph Levien has implemented what might be the smallest proof checker in the world, mmverify.py, at only 500 lines of Python code. <URL: https://en.wikipedia.org/wiki/Metamath> Marko -- https://mail.python.org/mailman/listinfo/python-list