A formal proof of a+b=b+a
I’ve recently noticed a failure in communication between mathematicians and people who aren’t that familiar with math. It all starts with some mathematical claim, say 0! = 1. Often a doubtful person takes issue with the statement and constructs a one-page essay on why intuitively 0! = 0.
So, is it true that 0! = 1? The answer is pretty boring. It completely depends on the definition of the factorial (!):
- if n! is defined as 1 ⋅ 2 ⋅ 3 ⋅ … ⋅ n, then 0! is not defined,
- if n! is defined as the number of all permutations of a set with n elements, then 0! is 1 as the empty function is the only permutation on the empty set {}.
Is there really a function from {} to {}? A function is defined as a set of pairs (x,f(x)). An empty function is thus an empty set {}.
The moral is you should always know how your objects are defined. If you talk about things without knowing their definitions, you quite literally don’t know what you’re talking about.
Though there is a problem. We never reach the end of our definitions. Above, we didn’t define what a set is, so how do we talk about it? We have to set something at the bottom of our mathematics. A foundation that everyone can agree on. One such foundation is called Zermelo-Fraenkel set theory, which builds mathematics by axiomatizing our intuitive notions about sets.
In this age, a foundation can be set through computers. If a computer can interpret the math (e.g. through a programming language like agda, coq, or lean), we’re satisfied with its formality and agree with the results.
In this post, we’ll look at an example of one formal proof for commutativity of addition. Its goal is to teach you how to respond when someone asks a question like “why is 1+1=2?” and how to prove such low-level statements. It may also cause some suffering :)
Natural numbers
First, we have to explain what natural numbers are. They are defined as
ℕ = {0, 1, 2, 3, 4, 5, …},
though this will not be good enough for us. We’ll define them inductively:
- 0 is a natural number,
- if n is a natural number, then suc n is a natural number.
We call suc n the successor of n. In this way, we have defined
- 0 = 0,
- 1 = suc 0,
- 2 = suc (suc 0),
- 3 = suc (suc (suc 0)),
- …
Why is this a good definition? Because it allows us to always split two cases (zero or successor) when considering natural numbers. We’ll see how this allows us to define and prove things recursively (via self-reference).
We want to talk about addition, so let’s define it and see how the definition of natural numbers helps us in the process. Fixing m allows us to separate two cases for n and define:
- m + 0 = m,
- m + (suc n) = suc (m + n).
This is a recursive definition! It calls itself, but on smaller arguments, which means the calls eventually terminate. An example:
1 + 2 = 1 + (suc 1) =
= suc (1 + 1) = suc (1 + suc 0) =
= suc(suc(1 + 0)) =
= suc(suc 1) = suc(suc(suc 0)) = 3.
At every line break, the definition of + was used, while everything else was just by the definition of our natural numbers.
We can also use our definition of natural numbers when proving their properties. To prove that some statement A holds for all natural numbers, we prove it holds for zero, and then that it holding for n implies it holding for suc n. This is called induction on natural numbers. I’m going to write such proofs as:
zero-case:
A holds for 0 [ comment ]successor-case:
A holds for n [ inductive assumption ]
A holds for (suc n) [ comment ]
You should think of proofs as definitions and induction as a way for them to use themselves recursively. In this way, induction is not a new concept.
Our goal is to prove commutativity, or that m + n = n + m. We’ll do it by using induction. First, we leave n alone and do induction on m. We need to prove two things:
- [1]: 0 + n = n + 0,
- [2]: m + n = n + m ⇒ (suc m) + n = n + (suc m).
Notice the statement [1] is independent of m and says something about every natural number n. To prove it, we use induction on n:
zero-case:
0 + 0 = 0 + 0 = 0 [ by definition of + ]successor-case:
0 + n = n + 0 [ inductive assumption ]
0 + (suc n) = [ by definition of + ]
= suc (0 + n) = [ by inductive assumption ]
= suc (n + 0) = [ by definition of + ]
= suc n = [ by definition of + ]
= (suc n) + 0
Now, we have to prove a side result (suc m) + n = suc (m + n) by using induction on n:
zero-case:
(suc m) + 0 = [ by definition of + ]
= suc m = [ by definition of + ]
= suc (m + 0)successor-case:
(suc m) + n = suc (m + n) [ inductive assumption ]
(suc m) + (suc n) = [ by definition of + ]
= suc ((suc m) + n) = [ by inductive assumption ]
= suc (suc (m + n)) = [ by definition of + ]
= suc (m + (suc n))
Finally, we can prove [2] as:
m + n = n + m [ inductive assumption ]
(suc m) + n = [ by our side result ]
= suc (m + n) = [ by inductive assumption ]
= suc (n + m) = [ by definition of + ]
= n + (suc m)Below I’ve translated our arguments into agda. I also had to formalize what an equivalence (≡) is and express our statement as an equivalence between two expressions. Then I had to prove two properties we took for granted:
k ≡ m and m ≡ n ⇒ k ≡ n
m ≡ n ⇒ (suc m) ≡ (suc n)
The first one allows us to formally squash the equalities in the above proofs together and produce equality between the relevant expressions (the first and last). The second one, we’ve used implicitly throughout our proofs.
I’m not going to say it’s easy to understand the code, but if you are going to try, do imagine types as statements and their members as proofs. And do realize that agda figured out some things by itself (mostly the equalities we explained by definition of +).
Similarly, we can also define multiplication × and prove
m × n = n × m.
The proof is a bit lengthier and is omitted here, but the high-level procedure is similar to our previous one.
Integers, rationals, and reals
We did most of the back-breaking labor and now all it remains is fun. We’re going to define all other numbers from natural numbers and preserve their commutativity.
We express an integer as a pair of natural numbers (n, m). Intuitively this means n - m. We then define:
(n, m) + (u, w) = (n + u, m + w).
In this way, the commutativity of + for integers is inherited from the commutativity of + for natural numbers:
(n, m) + (u, w) = (n + u, m + w) =
= (u + n, w + m) =
= (u, w) + (n, m).
Also, we can define × for integers as:
(n, m) × (u, w) = (n × u + m × w, n × w + m × u).
From the commutativity of × and + in the case of natural numbers, we also get the commutativity of × in the case of integers:
(n, m) × (u, w) =
= (n × u + m × w, n × w + m × u) =
= (u × n + w × m, u × m + w × n) =
= (u, w) × (n, m).
For rational numbers, i.e. fractions, we proceed similarly. For two integers u and v ≠ (0,0), we define a rational number as (u, v), which is intuitively u / v. We define addition as
(u, v) + (x, y) = (u × y + x × v, v × y).
You should recognize that this is how we normally add two rational numbers. From the commutativity of × and + in the case of integers, we get
(u, v) + (x, y) = (u × y + x × v, v × y) =
= (x × v + u × y, y × v) =
= (x, y) + (u, v).
Again, we made rationals inherit the commutativity of + from integers.
Real numbers can be defined as limits of convergent rational sequences. We can skip the limits and just define them as convergent sequences:
(a1, a2, a3, a4, …)
We define addition by components
a + b = (a1, a2, a3, …) + (b1, b2, b3, …) =
= (a1 + b1, a2 + b2, a3 + b3, …) =
= (b1 + a1, b2 + a2, b3 + a3, …) =
= (b1, b2, b3, …) + (a1, a2, a3, …) = b + a.
As every component commutes by the commutativity of + in the rational case, we have that also the sequences commute.
Formally, we should have defined what pairs and sequences are. Pairs are done below (sequences are trickier and are ommitted).
Conclusion
We’ve seen an extremely technical proof of commutativity for real numbers. This technicality is harder for us, but easy to automate. We’re at an age where this automation has a real possibility of producing theorems and making contributions to mathematics.
Besides that, every mathematician’s dream is to completely formalize mathematics. And nothing formalizes a language as well as a programming language syntax.
