NextjournalFrom Zero to Factorial
Constructing the natural numbers, from scratch (part 1)
This notebook is Copyright © Frederic Peschanski under the Creative Commons CC-BY-SA 4.0.
Introduction
In this series my objective is to discuss questions which, from a mathematical point of view, may appear as trivial :
What is a natural number ?
How to calculate with numbers, e.g. adding two numbers ?
There are very easy answers :
the natural numbers are inline_formula not implemented onto infinity !
inline_formula not implemented, etc.
it's a joke of course, but this is not far from the way we implicitly assume the existence and properties of natural numbers. This is of course because of our education : we know how to drive the car without knowing much about the engine... In this series, my goal is to explain a little bit of the engine.
If we adopt a more explicit and formal point of view, the questions we asked can be refined in a more interesting way :
how to define the set of natural numbers ?
how to define the function of addition, that takes two natural numbers inline_formula not implemented and inline_formula not implemented as input, and outputs their sum inline_formula not implemented ?
In the first part of our study (this document), I will address the first question, and I will tackle the second issue in a follow-up study.
In this document, our starting point is set theory, the standard foundation of mathematics. I will use and assume the common notations for sets, and I will not discuss foundational issues (besides the numbers themselves). In the mean time, I will develop a more formal treatment based on the LaTTe proof assistant. LaTTe is a type theory based on the lambda-calculus. It is thus not based on set theory, but it is easy to recover much of set theory thanks to the companion library for (typed) set theory : latte-sets.
One of my primary goals, with this document, is to show that the distance between day-to-day (mostly informal) mathematics and formal, mechanized, mathematics is not always as large as we might guess. Note, however, that there is no need to learn LaTTe first, since everything will be explained twice, first using quite classical mathematics, and then in LaTTe.
Before digging into the subject, I want to motivate a little bit more this study. First, there are in fact few documents/textbooks dealing with the formal construction of number systems. There are of course exceptions (cf. the references section at the end of the document) but the presentation is often quite informal. On the other hand, the formalization of mathematical concepts in proof assistants is often rather technique, and somewhat remote from the standard practice of informal mathematics. One example of this gap is undoubtedly the recursion theorem, which is maybe the most important concept I will present in this series. Most (informal) descriptions I've seen lead to the somewhat unpleasing feeling that the proof of the theorem is at the same time:
too hard for apprentice mathematicians (undergraduates, hobbyists, ...)
too simple, and uninteresting, for actual mathematicians (set theory is old, boring, ...)
In both case, I think the end result is that the knowledge is missing... We (mathematicians, programmers, ...) use recursion all the time, without really knowing (or having interest in) what it is fundamentally. So let's try to fill this gap.
About the LaTTe proof assistant
While I hope the explanations that follow are sufficient to understand the construction of natural numbers, it is even more interesting to understand (at least roughly) how the actual formalization is developed using a proof assistant.
LaTTe is a (hobby) software made for experimenting the formalization of mathematics on a computer. It is not a stand-alone software but rather a kind of an extension of the Clojure programming language (to sound smart we say that it is a DSL : a domain-specific language, embedded in its host). Even better, thanks to my friend and nextjournal fame Andrea Amantini (and of course the whole NJ-team!), anyone can play with LaTTe (and more generally Clojure) directly in the web browser. Really, it's awesome!
An important remark is that I will not explain directly how LaTTe works in this document, but I will show what it looks like, and hopefully convey the idea that it is a very nice complement to the more classical mathematical discourse.
First of all, I need to install LaTTe in this document, which is done thanks to the following declaration in Clojure, called a namespace.
(ns latte-next.nats.part1 "A formalization of the type natural numbers." (:refer-clojure :exclude [not int =]) (:require [latte.core :as latte :refer [defaxiom defthm deflemma definition proof assume have pose qed]] [latte-prelude.prop :as p :refer [not]] [latte-prelude.equal :as eq] [latte-prelude.quant :as q :refer [exists]])))These declarations introduce the basic library of LaTTe, named the prelude, and also a few notations.
The Set of Natural Numbers
In the dedicated Wikipedia page we find the most common "definitions" for the set of natural numbers, we have either :
the natural number with 0 included, denoted by inline_formula not implemented
or alternatively the ones without 0, denoted by inline_formula not implemented
We might ask, then, what is inline_formula not implemented itself ? But there is a more pressing question : what are these dots inline_formula not implemented ? Informally, and for most people, they introduce two distinct pieces information :
the series of numbers continues in the same way (increased by 1 each time)
it never stops, ultimately reaching infinity.
If we want to give a more precise meaning to such information, we have to adopt a more constructive approach. I see mostly two ways to introduce the set of natural numbers in a constructive way.
First, it is possible to introduce a (set-based) theory of inductive sets, and define the set of natural numbers as an instance of this general construction.
Alternatively, we can follow a more direct axiomatic approach : introduce the minimal known foundations for the natural numbers.
Since our objective is to discuss just the natural numbers, and not all possible inductive constructions, we will adopt the second approach. In a separate study I intend to discuss the construction of inductive sets in general (and in LaTTe, of course), so stay tuned !
The Peano arithmetic
Arguably the simplest and most elegant axiomatic construction of the natural numbers is based on the axioms of Peano arithmetic. In this section I introduce a variation of the Pean axioms, and I implement them in LaTTe.
Our first axiom is the name of the set itself, so we assume that inline_formula not implemented exists and is a set.
Axiom 1 : inline_formula not implemented is a set
In LaTTe this can be done as follows :
(defaxiom ℕ [] :type)This says that ℕ is a type, the basic construction in LaTTe, and that it has no argument (hence the empty square brackets).
The notion of equality is defined in the LaTTe prelude, under the name equal. We will rely on a more classical notation :
(definition = [[n ℕ] [m ℕ]] (eq/equal n m))Also, we will talk about inequality.
(definition ≠ [[n ℕ] [m ℕ]] (not (= n m)))The second axiom of the Peano arithmetic is that there is a special number, named zero and denoted by inline_formula not implemented, which is introduced as a natural number.
Axiom 2 : inline_formula not implemented
I must confess I revisit history here because Peano started from 1, although 0 is undoubtedly better : it is added without any trouble and for Gödel's sake, this is the unit element of addition, the absorbing element of multiplication, the cardinal of the emptyset, and so on and so forth!
In LaTTe, by pure computer contingency (the computer already takes 0 and 1), we do not use the classical notation but a more textual one.
(defaxiom zero [] ℕ)This says, of course, that zero is of type ℕ hence it is, by the type-theoretic point of view, a natural number.
We need now to give meaning to the sentence "the series of (natural) numbers continues in the same way (increased by 1 each time)". For this, Peano defined a principle of successor, introduced as a function.
Axiom 3 : there is a function inline_formula not implemented from ℕ to ℕ.
In LaTTe this can be introduced as follows.
(defaxiom succ [n ℕ] ℕ)This is a function, taking as input a natural number n, and with output a corresponding successor, also in the set/type ℕ we are constructing.
Of course, this does not provides much information, only that we assume a function from natural numbers to natural numbers. We would like to give a precise meaning to the successor function. Intuitively, we would like to describe the calculation from a natural number inline_formula not implemented to its successor inline_formula not implemented. However we have a kind of a chicken-and-egg problem here. One of our ultimate objective is to explain how to calculate a sum in pure mathematics, which means we cannot yet do so. So taking inline_formula not implemented literally does not work. We need to explain the notion of a successor without relying on calculation. This begins with the next Peano axiom.
Axiom 4 : for any inline_formula not implemented, inline_formula not implemented.
The number zero plays a special part in this series of successors : it has no predecessor. Equivalently we can says that no successor of a natural number can be equal to zero.
It is almost immediate to translate this in LaTTe.
(defaxiom zero-not-succ [] (∀ [n ℕ] (≠ (succ n) zero)))Probably the most important property of the successor is the following.
Axiom 5 : the successor function is injective
In a little bit more formal terms, this means that if we take two natural numbers inline_formula not implemented and inline_formula not implemented, if inline_formula not implemented then we can conclude that inline_formula not implemented. We will see in the next section why (and how) this "does the trick". For now let's just assume this axiom, and define it more formally.
(defaxiom succ-injective [] (∀ [n m ℕ] (==> (= (succ n) (succ m)) (= n m))))The main piece of the puzzle is probably the most famous, and most employed, axiom of the Peano arithmetic : the principle of induction for natural numbers. In many sources, a purely set-theoretic definition is proposed rather than the more practical predicative one. Because everything we aim to build can be built using the predicative version, which is more directly useful, this is the one we will introduce.
Axiom 6 : Given a predicate inline_formula not implemented over natural numbers,
if inline_formula not implemented is true for inline_formula not implemented, and, moreover,
if from the assumption that inline_formula not implemented holds for inline_formula not implemented then it also holds for inline_formula not implemented
then inline_formula not implemented is true for the whole set of natural numbers.
We will discuss and illustrate this very important axiom in a further section.
For now, let's find a formulation of this axiom in LaTTe.
(defaxiom ℕ-induct [P (==> ℕ :type)] (==> (P zero) (∀ [n ℕ] (==> (P n) (P (succ n)))) (∀ [n ℕ] (P n))))Note that instead of writing something like you would do in standard mathematics :
inline_formula not implemented
In type theory you will rather write :
inline_formula not implemented
(which is logically consistent with the former)
And in LaTTe this becomes :
(==> Hypothesis1 (==> Hypothesis2 (==> ... (==> HypothesisN Conclusion))))which can be simplified as follows :
(==> Hypothesis1 Hypothesis2 ... HypothesisN Goal)And that's it ! Beyond the axioms of set theory itself (that we assume implicitly here, through type theory), this is all we need to define the set of natural numbers. However, we will justify a little bit more that the axiomatic construction is, indeed, effective.
Reflecting on the construction
We will now take each axiom in turn, trying to understand why each one is required to construct the whole set of natural numbers.
By Axiom 1 we know that inline_formula not implemented exists as a set, and it can thus be manipulated using the constructions of set theory. However with only this axiom the set can be a set of basically anything. Axiom 2 indicates that inline_formula not implemented contains at least the element inline_formula not implemented. Axiom 3 introduces the function inline_formula not implemented but apart from that does not provide any new information about inline_formula not implemented itself. And for now the successor function can be basically any function that takes a natural number as input, and returns also a natural number as output. Axiom 4 adds an important constraint : zero is the successor of no other natural number. In a way, the numbers are built incrementally, starting from 0 and arriving at some successor (we know it should be called one but we don't yet know what is precisely), then related to its successor, and so on until ... infinity! But that's only an expectation. What's sure for now is that we cannot arrive at zero.
The successor function cannot be defined by calculation because addition is not yet available. Its definition is based on injectivity by Axiom 5. One of our expectation about the successor function, is that given a natural number inline_formula not implemented, its successor inline_formula not implemented (commonly denoted by inline_formula not implemented) should : (1) exists, and (2) be unique. So every time we "have" a natural number inline_formula not implemented, we can "find" yet another one, its successor inline_formula not implemented.
Let's put this in a little bit more formal terms. What we would like to prove (if possible formally), is that:
there is at least a number inline_formula not implemented for each inline_formula not implemented (the existence part)
there is at most one such number (the "singleness" part)
Which, taken together, would make the successor unique among numbers.
The first part is trivial since inline_formula not implemented is defined as a function. We will still state and prove the property a little bit more formally.
Lemma 1 : inline_formula not implemented
Proof : We assume inline_formula not implemented. We know by reflexivity that inline_formula not implemented. Hence, there is indeed a natural number inline_formula not implemented such that inline_formula not implemented, namely inline_formula not implemented □
(deflemma succ-ex [] (∀ [n ℕ] (exists [m ℕ] (= (succ n) m))))(proof succ-ex (assume [n ℕ] (have <a> (= (succ n) (succ n)) :by (eq/eq-refl (succ n))) (have <b> (exists [m ℕ] (= (succ n) m)) :by ((q/ex-intro (λ [m ℕ] (= (succ n) m)) (succ n)) <a>))) (qed <b>))Proof reading tip : try to compare the informal proof with the different (have ...) steps. The bit after the :by keyword is the (formal) justification of the step, whose details can be safely skipped while reading the proof.
When LaTTe answers with :qed, you have all reasons to be happy: your lemma or theorem is correct!
Hacking tip : try to change something in the proof, and see how it goes...
The constraint of injectivity provides the "singleness" part of the property.
Lemma 2 : inline_formula not implemented
Proof : We assume that inline_formula not implemented and inline_formula not implemented. We have inline_formula not implemented by symmetry of equality. And by transitivity, we have inline_formula not implemented. And since by Axiom 5 inline_formula not implemented is injective we conclude that inline_formula not implemented □
This theorem and its proof can be translated almost literally to LaTTe.
(deflemma succ-single [] (∀ [n ℕ] (∀ [m1 m2 ℕ] (==> (= (succ m1) n) (= (succ m2) n) (= m1 m2)))))And now the proof.
(proof succ-single (assume [n ℕ m1 ℕ m2 ℕ Hm1 (= (succ m1) n) Hm2 (= (succ m2) n)] (have <a> (= n (succ m2)) :by (eq/eq-sym Hm2)) (have <b> (= (succ m1) (succ m2)) :by (eq/eq-trans Hm1 <a>)) (have <c> (= m1 m2) :by (succ-injective m1 m2 <b>))) (qed <c>))The proof has been certified by LaTTe proof checker, it is now a formal proof of our theorem.
This is enough to construct the whole natural numbers, starting from 0 and discovering "new" successors... One thing, though, is to be sure the process really is infinite, i.e. there is no "loop" somewhere. We can convince ourselves that this is the case, considering the following property.
Theorem 1 : inline_formula not implemented
(defthm succ-neq [] (∀ [n ℕ] (≠ (succ n) n)))Proof : to prove this property, we will need the last axiom, the one that enables proving by induction over natural numbers. The property we want to prove is : inline_formula not implemented with inline_formula not implemented. We of course proceed by induction on inline_formula not implemented.
(base case) inline_formula not implemented which is true according to Axiom 4.
(inductive case) Suppose inline_formula not implemented and assume inline_formula not implemented, our hypothesis of induction. We now have to demonstrate inline_formula not implemented. We proceed by contradiction and assume inline_formula not implemented i.e. inline_formula not implemented. According to Axiom 5 we have inline_formula not implemented (through injectivity). But this is in contradiction with our assumption inline_formula not implemented. Thus inline_formula not implemented is true and the inductive case is demonstrated.
According to Axiom 6 this is enough to conclude that inline_formula not implemented □
(proof succ-neq (pose P := (λ [n ℕ] (≠ (succ n) n))) "Base case" (have <a> (P zero) :by (zero-not-succ zero)) ; Axiom 4 "Inductive case" (assume [n ℕ Hn (P n)] ; induction hypothesis "We have to proove `(P (succ n))`" "We proceed by contradiction." (assume [Hcontra (= (succ (succ n)) (succ n))] (have <b1> (= (succ n) n) :by (succ-injective (succ n) n Hcontra)) ; axiom 5 "Contradiction with induction hypothesis" (have <b2> p/absurd :by (Hn <b1>))) (have <b> (P (succ n)) :by <b2>)) "Applycation of the induction principle (axiom 6)" (qed ((ℕ-induct P) <a> <b>)))What we this obtain is a construction process such that, starting from 0, every time we "discover" a successor, it is a "new" one not yet encountered. This way, the incremental construction of inline_formula not implemented is indeed an infinite process, and in fact the "smallest" of such constructions, as expected.
Before concluding our first installment of this natural numbers from the group up series, we will derive a weaker but still useful reasoning principle : proof by case.
Theorem 2 : Proof by case (for natural numbers)
Given a predicate inline_formula not implemented over natural numbers,
if inline_formula not implemented is true for inline_formula not implemented, and, moreover inline_formula not implemented is true for any inline_formula not implemented,
then inline_formula not implemented is true for the whole set of natural numbers.
(defthm ℕ-case [P (==> ℕ :type)] (==> (P zero) (∀ [n ℕ] (P (succ n))) (∀ [n ℕ] (P n))))Proof : This is demonstrated by induction on inline_formula not implemented, directly in LaTTe.
(proof ℕ-case (assume [Hz (P zero) Hsucc (∀ [n ℕ] (P (succ n)))] "Base case" (have <a> (P zero) :by Hz) "Inductive case" (assume [n ℕ Hn (P n)] "No need for the induction hypothesis" (have <b> (P (succ n)) :by (Hsucc n))) "We apply the induction principle" (have <c> (∀ [n ℕ] (P n)) :by ((ℕ-induct P) <a> <b>))) (qed <c>))We now have established the set of natural numbers, both using classical mathematical principles and more formally using the LaTTe proof assistant. At least for this construction, the gap between the informal, day-to-day, mathematical style and the formalization is not so large.
In the next installment, we will introduce the recursion theorem for natural numbers, which will allow us to define precisely what, exactly, are calculations on natural numbers, so stay tuned!
References
The Wikipedia page about Natural numbers is okay-ish if not a little bit verbose, and so is the page about Peano axioms. Note that we did not consider the actual axioms Peano came up with. The first difference is that we started from zero and not one, and zero is an important numbe! Moreover, we use the predicative variant of the inductive principle, instead of relying on a purely set-theoretic variant. This will prove to be a good choice for all (of our) intent and purpose.
One source of inspiration for this series is the book Logic, Sets and Recursion by Robert L. Causey (1994, Jones and Bartlett Publishers). This is a very accessible textbook, and the proofs are very detailed, although mostly using conversational english, which may help or not depending on who is reading. Also the book shows a little bit its age (there is a second edition published in 2006 but I don't know whether it changed a lot or not).
The book The Foundations of Mathematics by Ian Stewart and David Tall (Oxford University Press) contains a rather thorough development of the natural numbers (as well as the rational and real numbers). The authors have decided to be very "philosophical" about the issue, which may of may not be a positive aspect. All in all, this is also a fine book.
I also rely on two books in french that I will cite for completeness: Les Objets Fondamentaux en Mathématiques - Les Nombres, by Marcel Grangé (2017, Editions Ellipses) and simply Les Nombres by Samuel Nicolay (2015, Hermann éditeurs). These books are fine but more like traditional mathematical expositions : a large number of (numbered) theorems and somewhat cryptic (idiosyncratic) proofs. These are still fine books, very thorough and full of interesting details (especially the second one).
Last but not least, the LaTTe proof assistant has been largely inspired by the book Type Theory and Formal Proofs: an Introduction, by Rob Nederpelt and Herman Geuvers (2014, Cambridge University Press). This is the book to read if you are interested in type theory and the lambda-calculs (from the logical point of view). A theory of arithmetic for integers (the set inline_formula not implemented) is developed thoroughly. I have implemented this theory in LaTTe, cf. latte-integers. Note that the recursion theorem is introduced there as an axiom, and not a theorem with a proof. For natural numbers, an alternative library is latte-nats (under development), which does provide a complete proof. However, this is a spoiler since we will cover this theorem next.