SMBC and 2 + 2
Image Attribution:
Zach Weinersmith. ["Untitled Comic"](http://www.smbc-comics.com/?id=3227). Jan. 2, 2014. Under a [Creative Commons Attribution-Share Alike Unported 3.0 License](http://creativecommons.org/licenses/by-sa/3.0/) (NOT a CC-BY 3.0 License).
January 6, 2014
math, peano_axioms, smbc, xkcd
Awesome! He let me use the original comic as the cover image. Thanks!
The web comic Saturday Morning Breakfast Cereal came out with this comic, which presented a hilarious cute child unfortunately asked to prove that 4 is the unique answer to 2 + 2. Luckily, for the child, he or she (it’s rather difficult to tell) could probably have just said “because.” The question of why 2 + 2 is really a definitional one; that is because Peano addition of the natural numbers is a function from ℕ × ℕ → ℕ, by definition all finite sums are unique.
A quick look at the Peano axioms is sufficient to see why this is the case. In particular because addition a + b is defined recursively on b such that b decrements by 1 each time and each number consists of a finite number of applications of the successor function (σ) on zero, we get as an end result that a + b is σ ∘ σ ∘ ⋯ ∘ σ(x) which is a unique natural number.
However, we should be quick to point out that we have only shown that addition is unique up to isomorphism. This is because the successor function is not unique, but only unique up to set isomorphism. In particular, if I happened to label two particular natural numbers x and y, there might be one successor function that maps x to y and another that doesn’t. Of course, “labeling” the natural numbers without the aid of the successor function is usually irrelevant to what we’re studying, so for all intents and purposes addition is unique.
Disregarding the math, perhaps the easiest practical demonstration that addition is a function and hence 2 + 2 has a unique answer is that you can code it in Haskell as below.
data Natural = Zero | Succ Natural deriving (Show)
(-+-) :: Natural -> Natural -> Natural
x -+- Zero = x
x -+- (Succ y) = Succ (x -+- y)Unfortunately, apparently nobody uses Haskell.