If we aren't taking 1+1=2 as axiomatic, then I'd hate to see what kinds of axioms you start with that are both simpler than it and lead to a proof of it.
Usually, when you dive deep into Foundations of Mathematics, you try to define objects as abstractly as possible and with as few requirements as possible. The idea being that any kind of "intuitive" truths are suspect and you want to formally derive all of mathematics formally from first principles¹. Presupposing an enumeration of objects 0, 1, 2, ... and a suitable operation on those objects is already more than we want in that context.
In set theory (which you can use as a first approximation of PM), you start with a single object: The empty set ∅. Let's give it a name, and because it is so simple, we will call it '0'.
Set theory also gives you an operation, set construction x ↦ {x}
. How do we use this to construct the rest of our numbers? Here is one way: Given a set X, define the successor of X as succ(X) = {X}. We can use this to obtain a sequence ∅, succ(∅) = {∅}, succ(succ(∅) = {{∅}}. Note that all of these have different depths of nesting, so they are in fact distinct objects. We can therefore give them unique names. Let's call succ(∅) '1', succ(succ(∅)) '2', and so on.²
You can see that we now have a set of objects ℕ = {0, 1, 2, ...}, but no addition yet. Let's get around to that. Given two sets X, Y from ℕ, we observe that either Y is 0 (in which case X + Y = X + 0 = X), or Y is of the shape succ(Z) for some Z in ℕ. In that case we say X + Y = succ(X + Z).³
But we defined this operation from first principles. How do we know that it actually matches our intuitive understanding of addition? Formally we'd have to show that (ℕ, +) is a commutative monoid, but for the purposes of this post, maybe we'll accept just a proof that 1+1=2:
1 + 1
= succ(∅) + succ(∅) [by the definition of 1]
= succ(succ(∅) + ∅) [by the second case of +]
= succ(succ(∅) ) [by the first case of +]
= 2 [by the definition of 2]
QED.
¹ Look out, there comes
Gödel with a steel chair
² These are called
Zermelo ordinals. There are other ways to define the natural numbers, for example
von Neumann ordinals, which have succ(X) = X ∪ {X}. That definition is a bit more complicated but often preferred for other reasons.
³ This way of defining arithmetic is called
Peano arithmetic
