A formal proof that 1+1=2
Some related reading |
---|
|
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=z | MP(I5,6) |
8 | ∀z x+0=z⇒x=z | Gen(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) |
11 | x=x | MP(-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)) |
14 | x=y⇒(x=x⇒y=x) | MP(12,13) |
15 | x=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) |
17 | x=x⇒(x=y⇒x=x) | Ax1(x=x,x=y) |
18 | x=y⇒x=x | MP(11,17) |
19 | x=y⇒y=x | MP(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=x | Gen(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)) |
44 | x=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.