Definition: 2=1+1

Here we define the number 2 starting from the axioms for the natural numbers. We make use 
of a modified form of Peano's axioms without any explicit successor function. We start with
the addition operator as a given. Informally, we say that x+1 is the successor of x. And
that x is the predecessor of x+1.

Note: Statements are in black, comments in blue, rules used and line references in gray.


The axioms for the natural numbers:

1	Set(n)
	& 1 ε n
	& ALL(a):ALL(b):[a ε n & b ε n => a+b ε n]
	& ALL(a):[a ε n => ~a+1=1]
	& ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b]
	& ALL(a):ALL(b):[a ε n & b ε n => a+(b+1)=a+b+1]
	& ALL(a):[Set(a) & 1 ε a & ALL(b):[b ε n & b ε a => b+1 ε a]
	=> ALL(b):[b ε n => b ε a]]
	Premise

Splitting the above premise into 7 separate axioms...

A1: n is a set (the set of natural numbers).

2	Set(n)
	Split, 1

A2: 1 is a natural number

3	1 ε n
	Split, 1

A3: + is a binary function on n

4	ALL(a):ALL(b):[a ε n & b ε n => a+b ε n]
	Split, 1

A4: The number 1 has no predecessor. It is the "first" natural number.

5	ALL(a):[a ε n => ~a+1=1]
	Split, 1

A5: Adding 1 is right-cancelable

6	ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b]
	Split, 1

A6: Adding 1 is associative

7	ALL(a):ALL(b):[a ε n & b ε n => a+(b+1)=a+b+1]
	Split, 1

A7: The principle of mathematical induction

8	ALL(a):[Set(a) & 1 ε a & ALL(b):[b ε n & b ε a => b+1 ε a]
	=> ALL(b):[b ε n => b ε a]]
	Split, 1

Apply A3 for a=1 and b=1

9	ALL(b):[1 ε n & b ε n => 1+b ε n]
	U Spec, 4

10	1 ε n & 1 ε n => 1+1 ε n
	U Spec, 9

Apply A2

11	1 ε n & 1 ε n
	Join, 3, 3

From A2 and A3...

12	1+1 ε n
	Detach, 10, 11

Apply the Reflex Axiom of Equality for 1+1

13	1+1=1+1
	Reflex

14	1+1 ε n & 1+1=1+1
	Join, 12, 13

Apply Existential Generalization

15	EXIST(c):[c ε n & c=1+1]
	E Gen, 14

Define: 2

Apply Existential Specification

16	2 ε n & 2=1+1
	E Spec, 15