THEOREM

*******

 

EXIST(f):[Set'(f) & ALL(a):ALL(b):~(a,b) e f & ALL(a):[a e null => f(a) e null]]

 

where null is a set such that ALL(a):~a e null  

 

 

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

******

 

Axiom of functionality for 1 variable

 

1     ALL(f):ALL(a):ALL(b):[Set'(f) & Set(a) & Set(b)

    => [ALL(c):ALL(d):[(c,d) e f => c e a & d e b]

    & ALL(c):[c e a => EXIST(d):[d e b & (c,d) e f]]

    & ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]

    => ALL(c):ALL(d):[c e a & d e b => [d=f(c) <=> (c,d) e f]]]]

      Axiom

 

 

Define: The null set

 

2     Set(null)

      Axiom

 

3     ALL(a):~a e null

      Axiom

 

 

PROOF

*****

 

Construct the Cartesian product null x null

 

Apply the Cartesian Product Axiom

 

4     ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]

      Cart Prod

 

5     ALL(a2):[Set(null) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e null & c2 e a2]]]

      U Spec, 4

 

6     Set(null) & Set(null) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e null & c2 e null]]

      U Spec, 5

 

7     Set(null) & Set(null)

      Join, 2, 2

 

8     EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e null & c2 e null]]

      Detach, 6, 7

 

9     Set'(null2) & ALL(c1):ALL(c2):[(c1,c2) e null2 <=> c1 e null & c2 e null]

      E Spec, 8

 

 

Define: null2  (null x null)

 

10   Set'(null2)

      Split, 9

 

11   ALL(c1):ALL(c2):[(c1,c2) e null2 <=> c1 e null & c2 e null]

      Split, 9

 

As Required:

 

23   ~EXIST(a):EXIST(b):(a,b) e null2

      5 Conclusion, 12

 

 

Prove: ALL(a):ALL(b):~(a,b) e null2

 

Apply Quantifier Switch and Remove Double Negation Axioms

 

24   ~~ALL(a):~EXIST(b):(a,b) e null2

      Quant, 23

 

25   ALL(a):~EXIST(b):(a,b) e null2

      Rem DNeg, 24

 

26   ALL(a):~~ALL(b):~(a,b) e null2

      Quant, 25

 

 

As Required:

 

null2 is a set of ordered pairs that is empty

 

27   ALL(a):ALL(b):~(a,b) e null2

      Rem DNeg, 26

 

 

Apply functionality axiom

 

28   ALL(a):ALL(b):[Set'(null2) & Set(a) & Set(b)

    => [ALL(c):ALL(d):[(c,d) e null2 => c e a & d e b]

    & ALL(c):[c e a => EXIST(d):[d e b & (c,d) e null2]]

    & ALL(c):ALL(d1):ALL(d2):[(c,d1) e null2 & (c,d2) e null2 => d1=d2]

    => ALL(c):ALL(d):[c e a & d e b => [d=null2(c) <=> (c,d) e null2]]]]

      U Spec, 1

 

29   ALL(b):[Set'(null2) & Set(null) & Set(b)

    => [ALL(c):ALL(d):[(c,d) e null2 => c e null & d e b]

    & ALL(c):[c e null => EXIST(d):[d e b & (c,d) e null2]]

    & ALL(c):ALL(d1):ALL(d2):[(c,d1) e null2 & (c,d2) e null2 => d1=d2]

    => ALL(c):ALL(d):[c e null & d e b => [d=null2(c) <=> (c,d) e null2]]]]

      U Spec, 28

 

30   Set'(null2) & Set(null) & Set(null)

    => [ALL(c):ALL(d):[(c,d) e null2 => c e null & d e null]

    & ALL(c):[c e null => EXIST(d):[d e null & (c,d) e null2]]

    & ALL(c):ALL(d1):ALL(d2):[(c,d1) e null2 & (c,d2) e null2 => d1=d2]

    => ALL(c):ALL(d):[c e null & d e null => [d=null2(c) <=> (c,d) e null2]]]

      U Spec, 29

 

31   Set'(null2) & Set(null)

      Join, 10, 2

 

32   Set'(null2) & Set(null) & Set(null)

      Join, 31, 2

 

 

Sufficient: For functionality of null2

 

33   ALL(c):ALL(d):[(c,d) e null2 => c e null & d e null]

    & ALL(c):[c e null => EXIST(d):[d e null & (c,d) e null2]]

    & ALL(c):ALL(d1):ALL(d2):[(c,d1) e null2 & (c,d2) e null2 => d1=d2]

    => ALL(c):ALL(d):[c e null & d e null => [d=null2(c) <=> (c,d) e null2]]

      Detach, 30, 32

 

Part 1

 

As Required:

 

39   ALL(c):ALL(d):[(c,d) e null2 => c e null & d e null]

      5 Conclusion, 34

 

Part 2

 

As Required:

 

44   ALL(c):[c e null => EXIST(d):[d e null & (c,d) e null2]]

      5 Conclusion, 40

 

Part 3

 

As Required:

 

52   ALL(c):ALL(d1):ALL(d2):[(c,d1) e null2 & (c,d2) e null2 => d1=d2]

      5 Conclusion, 45

 

53   ALL(c):ALL(d):[(c,d) e null2 => c e null & d e null]

    & ALL(c):[c e null => EXIST(d):[d e null & (c,d) e null2]]

      Join, 39, 44

 

54   ALL(c):ALL(d):[(c,d) e null2 => c e null & d e null]

    & ALL(c):[c e null => EXIST(d):[d e null & (c,d) e null2]]

    & ALL(c):ALL(d1):ALL(d2):[(c,d1) e null2 & (c,d2) e null2 => d1=d2]

      Join, 53, 52

 

 

null2 is a function mapping the null set to itself

 

55   ALL(c):ALL(d):[c e null & d e null => [d=null2(c) <=> (c,d) e null2]]

      Detach, 33, 54

 

 

As Required:

 

71   ALL(a):[a e null => null2(a) e null]

      5 Conclusion, 56

 

 

Joining previous results...

 

72   Set'(null2) & ALL(a):ALL(b):~(a,b) e null2

      Join, 10, 27

 

73   Set'(null2) & ALL(a):ALL(b):~(a,b) e null2

    & ALL(a):[a e null => null2(a) e null]

      Join, 72, 71

 

 

Generalizing...

 

As Required:

 

74   EXIST(f):[Set'(f) & ALL(a):ALL(b):~(a,b) e f

    & ALL(a):[a e null => f(a) e null]]

      E Gen, 73