One plus one equals two

Suppose one of your programmer friends comes to you and says: “Hey, convince me that 1 + 1 = 2!”.

What a request. You start by “Okay, I have one apple in my hand. I grab another one. Now I have two apples”.

Your friend proceeds: “I am still not convinced”. Now you turn to formalities.

You say “Ok, we have to agree on a framework. How about Peano’s axioms?”. Your friend nods but you can tell they have no idea what you’re saying.

You throw at them a random definition: “Peano arithmetic has a constant 0, a unary function symbol S, a binary function symbol +, and the equality symbol =.”. It makes sense to them but they can’t see where this is going.

You make a comment “So 0 is 0, 1 is S0, 2 is SS0, etc” and throw few axioms at random: $\text{Ax1:} x + 0 = x$ , $\text{Ax2:} S(x + y) = x + Sy$ .

You proceed: “Set $x = S0, y = 0$ and apply $\text{Ax2}$ to get to $S(S0 + 0) = S0 + S0$ . Now, apply $\text{Ax1}$ to get to $SS0 = S0 + S0$ , which is $2 = 1 + 1$ .”

Your friend is stunned. However, they think you cheated a bit because they don’t believe that 2 = 1 + 1 is the same as 1 + 1 = 2. You tell them that equality is symmetric, which means that if we have a = b then we also have b = a.

You can tell they’re bored by these formalities, but since they enjoy programming you proceed: “Here’s the same proof in Idris”:

data Natural = S Natural | Z

total plusN : Natural -> Natural -> Natural
plusN x Z = x
plusN x (S y) = S (plusN x y)

proof_1 : S Z `plusN` S Z = S (S Z)
proof_1 = Refl

“Connecting it to the previous definition: Z is 0, S is S, plusN is + (which is Ax1 and Ax2), and = is = (in proof_1, which is an Idris built-in)”.

Your friend is amazed. You notice they start understanding and finally see the beauty in all of this 🙂

EDIT: Thanks to u/nictytan for clearing a confusing paragraph where symmetricity of equality should have been used instead of commutativity.

3 thoughts on “One plus one equals two”

I’ll admit I didn’t understand most of this but its fascinating how difficult it can be to prove even some of the most fundamental concepts of mathematics

LikeLiked by 1 person

Boro Sitnikovski says:

20/09/2019 at 17:46

Sometimes I find it much easier to read code than actual formal math, where both represent the same idea 🙂 I was hoping to capture that in this article.

LikeLiked by 1 person

Reply

My favourite way to prove that 1 + 1 = 2 is through surreal numbers.

There’s an excellent article on surreal numbers at:

Click to access sur16.pdf

Claus Tøndering proves that 1 + 1 = 2 in (3.7) on page 27.

The summary below requires understanding the notation, but:

1 ≡ {0 | }
2 ≡ {1 | }
a + b = {AL + b, a + BL | AR + b, a + BR}
1 + 1 = {0 | } + {0 | } = {0 + 1, 1 + 0 | ∅ + 1, 1 + ∅} = {1 | } = 2

It is also shown that the real numbers map to the surreal numbers of the same symbols such that the ordering of the natural numbers corresponds to the ordering of their surreal counterparts. Otherwise we wouldn’t be proving that 1 + 1 = 2 for the same kinds of 1s and 2s that we normally assume.

LikeLike