Axioms for the Real Numbers

Field Axioms
************

Define: real, 0, 1  and operators +, _, *, 1/

1	Set(real)
	& ALL(a):ALL(b):[a  real & b  real => a+b  real]
	& ALL(a):ALL(b):ALL(c):[a  real & b  real & c  real => a+b+c=a+(b+c)]
	& ALL(a):ALL(b):[a  real & b  real => a+b=b+a]
	& 0  real
	& ALL(a):[a  real => a+0=a]
	& ALL(a):[a  real => _a  real]
	& ALL(a):[a  real => a+_a=0]
	& ALL(a):ALL(b):[a  real & b  real => a*b  real]
	& ALL(a):ALL(b):ALL(c):[a  real & b  real & c  real => a*b*c=a*(b*c)]
	& ALL(a):ALL(b):[a  real & b  real => a*b=b*a]
	& ALL(a):ALL(b):ALL(c):[a  real & b  real & c  real => a*(b+c)=a*b+a*c]
	& 1  real
	& ~0=1
	& ALL(a):[a  real => a*1=a]
	& ALL(a):[a  real & ~a=0 => 1/a  real]
	& ALL(a):[a  real & ~a=0 => a*(1/a)=1]
	Premise

Order Axioms
************

2	Set(pos)
	& ALL(a):[a  pos => a  real]
	& ALL(a):[a  real
	=> [a=0 | a  pos | _a  pos]
	& ~[a=0 & a  pos]
	& ~[a=0 & _a  pos]
	& ~[a  pos & _a  pos]]
	& ALL(a):ALL(b):[a  pos & b  pos => a+b  pos]
	& ALL(a):ALL(b):[a  pos & b  pos => a*b  pos]
	& ALL(a):ALL(b):[a  real & b  real => [a<b <=> b+_a  pos]]
	& ALL(a):ALL(b):[a  real & b  real => [a<=b <=> a<b | a=b]]
	Premise

Completeness Axiom
******************

3	ALL(a):[Set(a)
	& ALL(b):[b  a => b  real]
	& EXIST(b):b  a
	& EXIST(b):[b  real & ALL(c):[c  a => c<=b]]
	=> EXIST(b):[b  real & ALL(c):[c  a => c<=b]
	& ALL(c):[c  real & ALL(d):[d  a => d<=c] => b<=c]]]
	Premise

Define: n, the set of natural numbers

4	Set(n)
	& ALL(a):[a  n <=> a  real
	& [0<a
	& ALL(b):[Set(b) & ALL(c):[c  b => c  real]
	& 1  b
	& ALL(c):[c  b => c+1  b]
	=> a  b]]]
	Premise

Define: int, the set of integers

5	Set(int)
	& ALL(a):[a  int <=> a  real & [a=0 | a  n | _a  n]]
	Premise

Define: rat, the set of rational numbers

6	Set(rat)
	& ALL(a):[a  rat <=> a  real & EXIST(b):EXIST(c):[b  int & c  int & a*c=b]]
	Premise

Define: The - operator for real numbers

7	ALL(a):ALL(b):[a  real & b  real => a-b=a+_b]
	Premise

Define: The / operator for real numbers

8	ALL(a):ALL(b):[a  real & b  real & ~b=0 => a/b=a*(1/b)]
	Premise