For last few days I've been working on the proof that addition is commutative. It might sound like a simple thing to do, but I wanted to do it formally - you know, full and exact formality of every deduction step, starting from basic axioms and ending on the final conclusion that indeed \(\forall x\forall y:x+y=y+x\). This monster is almost 3 meters wide.

X y=y x

To put this short, what I do is first prove by induction that \(y+0=0+y\), then, as a lemma, I show inductively that \(x+S(y)=S(x)+y\), and ultimately I use it to show, by induction, that \(x+y=y+x\). 

The whole proof was written in \(\LaTeX\), as you can guess, and used pretty much only the proof package, which included \infer command which is responsible for all the horizontal bars. In writing I used 4 macros, but the whole proof still took 6749 7144 characters, including spaces. You can find the whole code on my pastebin.

What relation does this have to googology? First, the size - it is 2,7 meters wide. Second, it can be used to visualize one thing. Friedman has said that TREE(3) cannot be proven to exist in \(ACA_0+\Pi^1_2-BI\) when using less than \(^{1000}2\) characters. Of course, this is an enormous length, but when we look at how long the proof of commutativity of addition is, and this fact is really basic principle, we can be less surprised by the fact that this number actually has so long proof of existence.

Inference rules

Here is the list of inference/deduction rules I have used, along with short explanation on how they work.

Peano axioms

Out of 7 of Peano axioms, I have used 5, out of which 3 were from induction schema:

  • \(A_3\) is an axiom stating \(\forall x:x+0=x\).
  • \(A_4\) is an axiom stating \(\forall x\forall y:x+S(y)=S(x+y). This and previous one provide inductive definition of addition.
  • \(I_{\varphi(x)}\), where \(\varphi(x)\) is a formula in variable \(x\), is an instance of axiom schema of induction, which says \((\varphi(0)\land\forall x:\varphi(x)\Rightarrow\varphi(x+1))\Rightarrow\forall x:\varphi(x)\).

Equality axioms

These are axioms which concern properties of equality of objects.

  • \(R_=\) is an axiom stating that \(\forall x:x=x\) - every object is equal to itself, or reflexivity of equality.
  • \(S_=\) is an axiom \(\forall x\forall y:x=y\Rightarrow y=x\) - equality is symmetric.
  • \(T_=\) - arguably the most useful axiom, \(\forall x\forall y\forall z:x=y\land y=z\Rightarrow x=z\) - transitivity of equality.
  • \(S\) - this is the rule that says that we can apply functional symbol to equal objects to get equal objects - \(\forall x\forall y:x=y\Rightarrow S(x)=S(y)\).

"Proper" inference rules

These are the rules which aren't axioms - they don't come out of thin air, but they are based on other statements.

  • \(\forall_E\) states that we can drop a universal quantifier and replace its variable by any object (usually a constant) - for example, from \(\forall x\exists y: y=S(x)\) we can deduce that \(\exists y:y=S(a)\), where \(a\) is not a variable, but single number.
  • \(\forall_I\) is a way of creating universal statements. Suppose that we don't make any assumptions (I'll say a bit more on assumptions in a second) about some constant symbol, or all such assumptions where already used to introduce implication. Then, if we can show some statement about this general object, then we know that it hold for every object. For example, from \(\forall x:x=x\) we can deduce \(a=a\), and from this deduce \(\forall y:y=y\), where the latter deduction was \(\forall_I\).
  • \(\land_I\) - if we have deduced two statements, we can deduce that their conjunction is true. Simple as that.
  • \(MP\) - modus ponens. If we know that \(P\Rightarrow Q\), and we also know that \(P\) holds, then we can deduce \(Q\). 

Now it's time to tell more about assumptions. There are two kinds of these: one appears when using rule of existential specification, which hasn't been used here, and other one is used for \(\Rightarrow_I\). The other one looks as follows: we can take any statement \(P\). It can be true or false, contradictory or not, we don't care. This statement will be our assumption. It appears in deduction tree without bar over it, so it is different from axioms. Now we can use \(P\) as if it was a statement we already derived, and make further derivations about it.

  • \(\Rightarrow_I\): if \(P\) is an assumption, and from \(P\) we can deduce that \(Q\) holds, then we know that \(P\Rightarrow Q\) holds unconditionally.

If we have made an assumption which we used in the above rule, then it doesn't really matter further, and variables appearing in it can again be used in \(\forall_I\). As an example, if we have assumption that \(11=S(a)\), then we cannot generalize it to say \(\forall x: 11=S(x)\), because we had an assumption of \(a\). But if we now deduce from \(11=S(a)\) that \(10=a\), then we have implication \(11=S(a)\Rightarrow 10=a\), and we now can generalize over it - \(\forall x:11=S(x)\Rightarrow 10=x\).