Section 1.13 Natural numbers
In mathematics, pretty much every object is a set. In particular, we will define the natural numbersThere is a first, or rather zeroeth, natural number called
which has no elements at all.For any natural number
there is a next or successor natural number, which we might write as or which has exactly one more element than does.
Definition 1.13.1. Zero.
The natural number
Definition 1.13.2. Successor.
Let
It holds us to an extremely high standard of verification. When we reduce all concepts to a small number of primitive ones with a small number of rules for their interaction, then we can be very confident that the things we derive in this way are actually true.
Being able to encode things in ways similar to this makes it possible to encode these ideas on a computer, and use the computer to verify our proofs. This is a growing part of pure mathematics.
While this approach to the natural numbers may not be how we start off thinking about them, very often the act of formalization reveals a different and new set of intuitions we can have toward even familiar mathematical objects. In this case, our strategy for defining the natural numbers in this iterative fashion provides us with a blueprint for proving certain kinds of statements β induction.
Lastly, formalization gives us the opportunity to generalize notions in surprising directions. In this case, the way we've defined the natural numbers generalizes to what are called the von Neumann ordinals, which permit us to talk about various infinite structures, and even to do an infinite kind of induction, called transfinite induction.
for everyThe setwe have if and only if