THEOREM

*******

0+0 = 0

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 / DEFINITIONS USED

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

Define: +

*********

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

      Axiom

2     ALL(a):[a e n => a+2=next(next(a))]

      Axiom

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

      Axiom

Define: next

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

next is a function n  (the succesor function)

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

      Axiom

next is injective

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

      Axiom

Define: 0, 1, 2

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

6     0 e n

      Axiom

7     1 e n

      Axiom

8     1=next(0)

      Axiom

9     2 e n

      Axiom

10    2=next(1)

      Axiom

PROOF

*****

First...

Prove: 0+1=1

Apply definition of +

11    0 e n => 0+2=next(next(0))

      U Spec, 2

12    0+2=next(next(0))

      Detach, 11, 6

13    0+next(1)=next(next(0))

      Substitute, 10, 12

Apply definition of +

14    ALL(b):[0 e n & b e n => 0+next(b)=next(0+b)]

      U Spec, 3

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

      U Spec, 14

16    0 e n & 1 e n

      Join, 6, 7

17    0+next(1)=next(0+1)

      Detach, 15, 16

18    next(0+1)=next(next(0))

      Substitute, 17, 13

19    next(0+1)=next(1)

      Substitute, 8, 18

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

      U Spec, 5

21    0+1 e n & 1 e n => [next(0+1)=next(1) => 0+1=1]

      U Spec, 20

22    ALL(b):[0 e n & b e n => 0+b e n]

      U Spec, 1

23    0 e n & 1 e n => 0+1 e n

      U Spec, 22

24    0 e n & 1 e n

      Join, 6, 7

25    0+1 e n

      Detach, 23, 24

26    0+1 e n & 1 e n

      Join, 25, 7

27    next(0+1)=next(1) => 0+1=1

      Detach, 21, 26

As Required:

28    0+1=1

      Detach, 27, 19

Prove: 0+0=0

Apply definition of +

29    ALL(b):[0 e n & b e n => 0+next(b)=next(0+b)]

      U Spec, 3

30    0 e n & 0 e n => 0+next(0)=next(0+0)

      U Spec, 29

31    0 e n & 0 e n

      Join, 6, 6

32    0+next(0)=next(0+0)

      Detach, 30, 31

33    0+1=next(0+0)

      Substitute, 8, 32

34    1=next(0+0)

      Substitute, 28, 33

35    next(0)=next(0+0)

      Substitute, 8, 34

Apply definition of next

36    ALL(b):[0 e n & b e n => [next(0)=next(b) => 0=b]]

      U Spec, 5

37    0 e n & 0+0 e n => [next(0)=next(0+0) => 0=0+0]

      U Spec, 36

Apply definition of +

38    ALL(b):[0 e n & b e n => 0+b e n]

      U Spec, 1

39    0 e n & 0 e n => 0+0 e n

      U Spec, 38

40    0+0 e n

      Detach, 39, 31

41    0 e n & 0+0 e n

      Join, 6, 40

42    next(0)=next(0+0) => 0=0+0

      Detach, 37, 41

43    0=0+0

      Detach, 42, 35

As Required:

44    0+0=0

      Sym, 43