THEOREM

*******

1+1=2

This machine-verified formal proof was written with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com

AXIOMS REQUIRED

***************

1 0 e n

Axiom

2 ALL(a):[a e n => EXIST(b):[b e n & next(a)=b]]

Axiom

3 ALL(a):[a e n => a+0=a]

Axiom

4 ALL(a):ALL(b):[a e n & b e n => a+next(b)=next(a+b)]

Axiom

PROOF

*****

Apply Axiom 2 for a=0

5 0 e n => EXIST(b):[b e n & next(0)=b]

U Spec, 2

6 EXIST(b):[b e n & next(0)=b]

Detach, 5, 1

7 1 e n & next(0)=1

E Spec, 6

Define: 1

8 1 e n

Split, 7

9 next(0)=1

Split, 7

Apply Axiom 2 for a=1

10 1 e n => EXIST(b):[b e n & next(1)=b]

U Spec, 2

11 EXIST(b):[b e n & next(1)=b]

Detach, 10, 8

12 2 e n & next(1)=2

E Spec, 11

Define: 2

13 2 e n

Split, 12

14 next(1)=2

Split, 12

Apply Axiom 3 for a=1

15 1 e n => 1+0=1

U Spec, 3

16 1+0=1

Detach, 15, 8

Apply Axiom 4 for a=1 and b=0

17 ALL(b):[1 e n & b e n => 1+next(b)=next(1+b)]

U Spec, 4

18 1 e n & 0 e n => 1+next(0)=next(1+0)

U Spec, 17

19 1 e n & 0 e n

Join, 8, 1

20 1+next(0)=next(1+0)

Detach, 18, 19

Substituting...

21 1+1=next(1+0)

Substitute, 9, 20

22 1+1=next(1)

Substitute, 16, 21

As Required:

23 1+1=2

Substitute, 14, 22