Constructing the Postive Rational Numbers Q+ from N

Introduction
------------

Here, we construct the set of postive rational numbers qpos from the set of
natural numbers using only the axioms of set theory. 

In DC Proof, there are only 3 ways to construct a set from other sets: 

1. The Cartesian Product Axiom
2. The Power Set Axiom 
3. The Subset Axiom

Each of these axioms are used here.

We begin with a list of Peano-like axioms for the set of natural numbers n, with 
operators + and * defined on n. Then we use the Cartesian Product Axiom to construct
the set n2, the set of ordered pairs of natural numbers. Then we use the Power Set 
Axiom to construct the set pn2, the power set of n2. Finally, we use the Subset Axiom
to construct qpos, a subset of pn2 that will comprise the set of postive rational 
numbers.

Informally: 1/2 = {(1,2), (2,4), (3,6)...}
            2/3 = {(2,3), (4,6), (6,9)...}
            etc.


Axioms of the natural numbers 
-----------------------------

Introduce n, 1, +, *

1	Set(n)
	Axiom

2	1 ε n
	Axiom

Define: '+' on n

3	ALL(a):ALL(b):[a ε n & b ε n => a+b ε n]
	Axiom

4	ALL(a):[a ε n => ~a+1=1]
	Axiom

5	ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b]
	Axiom

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

Principle of mathematical induction

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

Define: '*' on n

8	ALL(a):ALL(b):[a ε n & b ε n => a*b ε n]
	Axiom

9	ALL(a):[a ε n => a*1=a]
	Axiom

10	ALL(a):ALL(b):[a ε n & b ε n => a*(b+1)=a*b+a]
	Axiom


Use the Cartesian Product Axiom to construct the set of ordered pairs of natural numbers

11	ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) ε b <=> c1 ε a1 & c2 ε a2]]]
	Cart Prod

12	ALL(a2):[Set(n) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) ε b <=> c1 ε n & c2 ε a2]]]
	U Spec, 11

13	Set(n) & Set(n) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) ε b <=> c1 ε n & c2 ε n]]
	U Spec, 12

14	Set(n) & Set(n)
	Join, 1, 1

15	EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) ε b <=> c1 ε n & c2 ε n]]
	Detach, 13, 14

16	Set'(n2) & ALL(c1):ALL(c2):[(c1,c2) ε n2 <=> c1 ε n & c2 ε n]
	E Spec, 15

Define: n2, the set of ordered pairs of natural numbers

17	Set'(n2)
	Split, 16

18	ALL(c1):ALL(c2):[(c1,c2) ε n2 <=> c1 ε n & c2 ε n]
	Split, 16


Use the Power Set axiom to construct the powerset of n2

19	ALL(a):[Set'(a) => EXIST(b):[Set(b)
	& ALL(c):[c ε b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) ε c => (d1,d2) ε a]]]]
	Power Set

20	Set'(n2) => EXIST(b):[Set(b)
	& ALL(c):[c ε b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) ε c => (d1,d2) ε n2]]]
	U Spec, 19

21	EXIST(b):[Set(b)
	& ALL(c):[c ε b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) ε c => (d1,d2) ε n2]]]
	Detach, 20, 17

22	Set(pn2)
	& ALL(c):[c ε pn2 <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) ε c => (d1,d2) ε n2]]
	E Spec, 21

Define: pn2, the power set of n2

23	Set(pn2)
	Split, 22

24	ALL(c):[c ε pn2 <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) ε c => (d1,d2) ε n2]]
	Split, 22


Use the Subset Axiom to construct the set of postive rational numbers

25	EXIST(sub):[Set(sub) & ALL(a):[a ε sub <=> a ε pn2 & [EXIST(b):EXIST(c):(b,c) ε a
	& ALL(b):ALL(c):ALL(d):ALL(e):[(b,c) ε a & d ε n & e ε n => [(d,e) ε a <=> b*e=d*c]]]]]
	Subset, 23

Define: qpos, the set of postive rational numbers

Informally: 1/2 = {(1,2), (2,4), (3,6)...}
            2/3 = {(2,3), (4,6), (6,9)...}
            etc.

26	Set(qpos) & ALL(a):[a ε qpos <=> a ε pn2 & [EXIST(b):EXIST(c):(b,c) ε a
	& ALL(b):ALL(c):ALL(d):ALL(e):[(b,c) ε a & d ε n & e ε n => [(d,e) ε a <=> b*e=d*c]]]]
	E Spec, 25