"?>

A formal proof that 1+1=2

Some related reading
cover
The table below gives a proof of 1+1=2 based on the proof system described in Formal proofs of Arithmetic. Since 1 and 2 don't occur as basic symbols of that system, we need to define them as 0' and 0'', so the statement to be proved is 0'+0'=0''. Remember that proofs in this sense are just about manipulating symbols. (That said, I don't tend to be too fussy about the use of parentheses). Even the equals sign is just a symbol - we can't assume anything about it that can't be deduced from the axioms. Hence one of the first things in the proof is to show that equality is reflexive (x=x) and symmetric x=y⇒y=x .

The third column shows the axiom used, where the arguments of MP, and the second argument of Gen refer to previous line numbers (or to an integer axiom if preceeded by an I)

1 ∀x;x=y⇒(x=z⇒y=z)Gen(x,I1)
2 ∀x;x=y⇒(x=z⇒y=z)⇒x+0=y⇒(x+0=z⇒y=z)Ax4(x,x+0,x=y⇒(x=z⇒y=z))
3 x+0=y⇒(x+0=z⇒y=z)MP(1,2)
4 ∀y x+0=y⇒(x+0=z⇒y=z) Gen(y,2)
5 ∀y x+0=y⇒(x+0=z⇒y=z)⇒ x+0=x⇒(x+0=z⇒x=z)Ax4(y,x,x+0=y⇒(x+0=z⇒y=z))
6 x+0=x⇒(x+0=z⇒x=z)MP(4,5)
7 x+0=z⇒x=zMP(I5,6)
8 ∀z x+0=z⇒x=zGen(z,7)
9(∀z x+0=z⇒x=z)⇒( x+0=x⇒x=x)Ax4(z,x,x+0=z⇒x=z))
10( x+0=x⇒x=x) MP(8,9)
11x=xMP(-5,10)
12∀z x=y⇒(x=z⇒y=z)Gen(z,I1)
13∀z x=y⇒(x=z⇒y=z)⇒x=y⇒(x=x⇒y=x)Ax4(z,x,x=y⇒(x=z⇒y=z))
14x=y⇒(x=x⇒y=x)MP(12,13)
15x=y⇒(x=x⇒y=x)⇒(x=y⇒x=x)⇒(x=y⇒y=x)Ax2(x=y,x=x,y=x)
16(x=y⇒x=x)⇒(x=y⇒y=x)MP(14,15)
17x=x⇒(x=y⇒x=x)Ax1(x=x,x=y)
18x=y⇒x=xMP(11,17)
19x=y⇒y=xMP(18,16)
20∀x (x+y')=(x+y)'Gen(x,I6)
21∀x (x+y')=(x+y)'⇒(0'+y')=(0'+y)'Ax4(x,0', (x+y')=(x+y)')
22(0'+y')=(0'+y)' MP(20,21)
23∀y (0'+y')=(0'+y)' Gen(y,22)
24 ∀(0'+y')=(0'+y)'⇒(0'+0')=(0'+0)'Ax4(y,0,(0+y')=(0+y)')
25(0'+0')=(0'+0)' MP(23,24)
26∀x (x+0)=x Gen(y,I5)
27∀x (x+0)=x ⇒ (0'+0)=0' Ax4(x,0',(x+0)=x)
28(0'+0)=0' MP(26,27)
29∀x (x=y⇒x'=y') Gen(x,I2)
30∀x (x=y⇒x'=y')⇒ ((0'+0)=y⇒(0'+0)'=y')Ax4((x,0'+0,x=y⇒x'=y'))
31((0'+0)=y⇒(0'+0)'=y')MP(29,30)
32∀y ((0'+0)=y⇒(0'+0)'=y')Gen(y,31)
33∀y (0'+0)=y⇒(0'+0)'=y')⇒((0'+0)=0'⇒(0'+0)'=0'')Ax4(y,0',(0'+0)=y⇒(0'+0)'=y')
34((0'+0)=0'⇒(0'+0)'=0'')MP(32,33)
35(0'+0)'=0''MP(28,34)
36∀x x=y⇒y=xGen(x,19)
37(∀x x=y⇒y=x)⇒( (0'+0')=y⇒y=(0'+0'))Ax4(x,(0'+0')(∀x x=y⇒y=x))
38(0'+0')=y⇒y=(0'+0')MP(36,37)
39∀y (0'+0')=y⇒y=(0'+0') Gen(y,38)
40∀y (0'+0')=y⇒y=(0'+0') ⇒ ((0'+0')=(0'+0)'⇒(0'+0)'=(0'+0') Ax4(y,(0'+0)',(0'+0')=y⇒y=(0'+0'))
41((0'+0')=(0'+0)'⇒(0'+0)'=(0'+0') MP(39,40)
42(0'+0)'=(0'+0')MP(25,41)
43(∀z x=y⇒(x=z⇒y=z)) ⇒ x=y⇒(x=0''⇒y=0'') Ax4(z,0'',x=y⇒(x=z⇒y=z))
44x=y⇒(x=0''⇒y=0'')MP(12,43)
45∀x x=y⇒(x=0''⇒y=0'')Gen(x,44)
46∀x x=y⇒(x=0''⇒y=0'')⇒( (0'+0)' =y⇒((0'+0)' =0''⇒y=0'')) Ax4(x,x,(0'+0)',x=y⇒(x=0''⇒y=0'') )
47(0'+0)' =y⇒((0'+0)' =0''⇒y=0'')MP(45,46)
48∀y (0'+0)'=y⇒((0'+0)' =0''⇒y=0'')Gen(y,47)
49∀y (0'+0)' =y⇒((0'+0)' =0''⇒y=0'')⇒
((0'+0)' =(0'+0')⇒((0'+0)' =0''⇒(0'+0')=0''))
Ax4( y,(0'+0'),
(0'+0)' =y⇒((0'+0)' =0''⇒y=0''),)
50(0'+0)' =(0'+0')⇒((0'+0)' =0''⇒(0'+0')=0'')MP(48,49)
51(0'+0)' =0''⇒(0'+0')=0''MP(42,50)
52(0'+0')=0''MP(35,51)

This certainly isn't the longest proof that 1+1=2: that honour probably goes to Alfred North Whitehead and Bertrand Russell in Principia Mathematica, where they develop mathematics from an abstract version of set theory, and get around to proving 1+1=2 on page 362.

Gödel's incompleteness theorem project