a natural number is any element of the set which is the set of all the numbers created by starting with 0 and then counting forward indefinitely. we call the set of natural numbers.
in some texts the natural numbers start at 1 instead of 0, but this is a matter of notational convention more than anything else. in (terence tao, 2022) we refer to the set as the positive integers rather than the natural numbers.
natural numbers are sometimes also known as whole numbers.
in a sense, def-natural-set-inf solves the problem of what the natural numbers are: a natural number is any element of the set . however, it is not really that satisfactory, because it begs the question of what is. This definition of "start at 0 and count indefinitely" seems like an intuitive enough definition of , but it is not entirely acceptable, because it leaves many questions unanswered. for instance: how do we know we can keep counting indefinitely, without cycling back to 0? Also, how do you perform operations such as addition, multiplication, or exponentiation?
we can answer the latter question first: we can define complicated operations in terms of simpler operations. exponentiation is nothing more than repeated multiplication: is nothing more than three fives multiplied together. multiplication is nothing more than repeated addition; is nothing more than three fives added together. (subtraction and division are not be covered here, because they are not operations which are well-suited to the natural numbers; they are defined for the integers and rationals, respectively.) and addition? it is nothing more than the repeated operation of counting forward, or incrementing. if you add three to five, what you are doing is incrementing five three times. on the other hand, incrementing seems to be a fundamental operation, not reducible to any simpler operation; indeed, it is the first operation one learns on numbers, even before learning to add.
we define 1 to be the number , 2 to be the number , 3 to be the number , etc. (in other words, , , , etc.
there exists a number system , whose elements we call natural numbers, for which the peano axioms are true.
3 is a natural number.
by axi-peano-zero, 0 is a natural number. by axi-peano-inc, 0++ = 1 is a natural number. by axi-peano-inc again, 1++ = 2 is a natural number. by axi-peano-inc again, 2++ = 3 is a natural number.
the principle of induction gives us a way to prove that a property is true for every natural number . we see many proofs which have a form similar to this:
a certain property is true for every natural number .
we use induction. we first verify the base case , i.e., we prove . (insert proof of here.) now suppose inductively that is a natural number, and has already been proven. we now prove . (insert proof of , assuming that is true, here.) this closes the induction, and thus is true for all numbers n.
suppose for each natural number , we have some function from the natural numbers to the natural numbers. let be a natural number. then we can assign a unique natural number to each natural number , such that and for each natural number .
we use induction. we first observe that this procedure gives a single value to , namely . (none of the other definitions will redefine the value of , because of axi-peano-diff) now suppose inductively that the procedure gives a single value to . then it gives a single value to , namely . (none of the other definitions will redefine the value of , because of axi-peano-induction) this completes the induction, and so an is defined for each natural number , with a single value assigned to each .
the definition we proposed here isnt circular because the concept of a function doesnt require the peano axioms.
let be a natural number. to add zero to , we define . now suppose inductively that we have defined how to add to . then we can add to by defining .
it is implicitly defined in def-natural-add that the addition of two natural number yields a third natural number, as yields which is assumed to be a natural number, and by the induction hypothesis is defined and also yields a natural number, then is defined to be which is a natural number by axi-peano-inc and the inductive hypthesis.
this means that any operations that apply to natural numbers also apply to a parenthesized addition of natural numbers such as , we can increment them, e.g. , or add additions of natural numbers to other additions of natural numbers, e.g. , and so on.
for any natural number , .
we induct on , for the base case, by def-natural-add, we assume (the induction hypothesis) and need to show , by def-natural-add we know and by the induction hypothesis we know so which means .
the base case follows since we know that for every natural number , and 0 is a natural number. now suppose inductively that . we wish to show that . but by definition of addition, is equal to , which is equal to since . this closes the induction.
for any natural numbers and ,
we induct on , keeping fixed, for the base case we need to show , by def-natural-add we know and so which means the base case is true as both equal , we assume the induction hypothesis, , and have to show , by def-natural-add we know and by the induction hypothesis and by def-natural-add.
for any natural numbers and , .
we induct on , keeping fixed, for the base case, we must show , but we already know both equal by def-natural-add and lem-natural-add-zero. we assume the inductive hypotheis and we have to show : by def-natural-add and by def-natural-add-suc and by the inductive hypothesis .
for any natural numbers , we have .
we induct on , keeping and fixed, for the base case , we need to show , by def-natural-add we know so and we know , so both sides are equal. we assume the inductive hypothesis and have to show , by def-natural-add, , again by def-natural-add and by the inductive hypothesis , by def-natural-add, .
let be natural numbers such that , then .
we fix and induct on , for the base case, implies by def-natural-add, we assume the inductive hypothesis, implies , and need to show implies , by def-natural-add, and again by def-natural-add , so we have , by axi-peano-diff , and so by the inductive hypothesis , which closes the induction.
a natural number is said to be positive iff it is not equal to 0.
if is a positive natural number, and is a natural number, then is positive (and hence is also, by pro-natural-add-com).
we fix and induct on , for the base case , is positive, we assume the inductive hypothesis; i.e. that is positive, and have to show that is positive, by lem-natural-add-suc , and by axi-peano-nosuc is positive as zero isnt the successor of any natural number, this closes the induction.
if and are natural numbers such that , then and .
assume in contradiction that or (that one of them is non-zero, i.e. one of them is positive), then we would get a contradiction by pro-natural-pos-add which says would be positive but we have .
let be a positive number. then there exists exactly one natural number such that .