THEOREM

*******

 

ALL(s):[Set(s)

=> EXIST(null):EXIST(f):[Set(null) & Set'(f)

& [ALL(a):~a e null & ALL(a):ALL(b):~(a,b) e f

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

 

The proof could be shortened considerably since anything whatsoever would follow from the presumed existence of any element of an empty set. Here, however, we actually construct the function f using the axioms of set theory.

 

 

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

 

   

    PROOF

    *****

   

    Suppose...

 

      2     Set(s)

            Premise

 

    Construct empty subset of s

   

    Apply Subset Axiom

 

      3     EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e s & ~a e s]]

            Subset, 2

 

      4     Set(null) & ALL(a):[a e null <=> a e s & ~a e s]

            E Spec, 3

 

   

    Define: null  (empty subset of s)

 

      5     Set(null)

            Split, 4

 

      6     ALL(a):[a e null <=> a e s & ~a e s]

            Split, 4

 

        

         Prove: ~EXIST(a):a e null

        

         Suppose to the contrary...

 

            7     x e null

                  Premise

 

         Apply definition of null

 

            8     x e null <=> x e s & ~x e s

                  U Spec, 6

 

            9     [x e null => x e s & ~x e s]

             & [x e s & ~x e s => x e null]

                  Iff-And, 8

 

            10   x e null => x e s & ~x e s

                  Split, 9

 

            11   x e s & ~x e s => x e null

                  Split, 9

 

            12   x e s & ~x e s

                  Detach, 10, 7

 

    As Required:

 

      13   ~EXIST(a):a e null

            4 Conclusion, 7

 

    Change quantifier

 

      14   ~~ALL(a):~a e null

            Quant, 13

 

    As Required:

 

      15   ALL(a):~a e null

            Rem DNeg, 14

 

    Construct Cartesian product of null and s

   

    Apply Cartesian Product Axiom

 

      16   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

 

      17   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, 16

 

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

            U Spec, 17

 

      19   Set(null) & Set(s)

            Join, 5, 2

 

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

            Detach, 18, 19

 

      21   Set'(nullxs) & ALL(c1):ALL(c2):[(c1,c2) e nullxs <=> c1 e null & c2 e s]

            E Spec, 20

 

   

    Define: nullxs  (Cartesian product of null and s)

 

      22   Set'(nullxs)

            Split, 21

 

      23   ALL(c1):ALL(c2):[(c1,c2) e nullxs <=> c1 e null & c2 e s]

            Split, 21

 

        

         Prove: ~EXIST(a):EXIST(b):(a,b) e nullxs

        

         Suppose to the contrary...

 

            24   (x,y) e nullxs

                  Premise

 

         Apply definition of nullxs

 

            25   ALL(c2):[(x,c2) e nullxs <=> x e null & c2 e s]

                  U Spec, 23

 

            26   (x,y) e nullxs <=> x e null & y e s

                  U Spec, 25

 

            27   [(x,y) e nullxs => x e null & y e s]

             & [x e null & y e s => (x,y) e nullxs]

                  Iff-And, 26

 

            28   (x,y) e nullxs => x e null & y e s

                  Split, 27

 

            29   x e null & y e s => (x,y) e nullxs

                  Split, 27

 

            30   x e null & y e s

                  Detach, 28, 24

 

            31   x e null

                  Split, 30

 

            32   y e s

                  Split, 30

 

         Apply definition of null

 

            33   ~x e null

                  U Spec, 15

 

         Obtain the contradiction...

 

            34   x e null & ~x e null

                  Join, 31, 33

 

    As Required:

 

      35   ~EXIST(a):EXIST(b):(a,b) e nullxs

            4 Conclusion, 24

 

   

    Change quantifiers

 

      36   ~~ALL(a):~EXIST(b):(a,b) e nullxs

            Quant, 35

 

      37   ALL(a):~EXIST(b):(a,b) e nullxs

            Rem DNeg, 36

 

      38   ALL(a):~~ALL(b):~(a,b) e nullxs

            Quant, 37

 

   

    As Required:

 

      39   ALL(a):ALL(b):~(a,b) e nullxs

            Rem DNeg, 38

 

    Apply Axiom of Functionality

 

      40   ALL(a):ALL(b):[Set'(nullxs) & Set(a) & Set(b)

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

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

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

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

            U Spec, 1

 

      41   ALL(b):[Set'(nullxs) & Set(null) & Set(b)

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

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

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

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

            U Spec, 40

 

      42   Set'(nullxs) & Set(null) & Set(s)

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

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

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

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

            U Spec, 41

 

      43   Set'(nullxs) & Set(null)

            Join, 22, 5

 

      44   Set'(nullxs) & Set(null) & Set(s)

            Join, 43, 2

 

   

    Sufficient: For functionality of nullxs

 

      45   ALL(c):ALL(d):[(c,d) e nullxs => c e null & d e s]

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

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

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

            Detach, 42, 44

 

        

         Part 1

        

         Prove: ALL(c):ALL(d):[(c,d) e nullxs => c e null & d e s]

        

         Suppose...

 

            46   (x,y) e nullxs

                  Premise

 

         Apply definition of nullxs

 

            47   ALL(c2):[(x,c2) e nullxs <=> x e null & c2 e s]

                  U Spec, 23

 

            48   (x,y) e nullxs <=> x e null & y e s

                  U Spec, 47

 

            49   [(x,y) e nullxs => x e null & y e s]

             & [x e null & y e s => (x,y) e nullxs]

                  Iff-And, 48

 

            50   (x,y) e nullxs => x e null & y e s

                  Split, 49

 

            51   x e null & y e s => (x,y) e nullxs

                  Split, 49

 

            52   x e null & y e s

                  Detach, 50, 46

 

   

    Part 1

   

    As Required:

 

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

            4 Conclusion, 46

 

        

         Part 2

        

         Prove: ALL(c):[c e null => EXIST(d):[d e s & (c,d) e nullxs]]

        

         Suppose...

 

            54   x e null

                  Premise

 

         Apply definition of null

 

            55   ~x e null

                  U Spec, 15

 

         Apply principle of explosion

 

            56   ~x e null => EXIST(d):[d e s & (x,d) e nullxs]

                  Arb Cons, 54

 

            57   EXIST(d):[d e s & (x,d) e nullxs]

                  Detach, 56, 55

 

   

    Part 2

   

    As Required:

 

      58   ALL(c):[c e null => EXIST(d):[d e s & (c,d) e nullxs]]

            4 Conclusion, 54

 

        

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

        

         Suppose...

 

            59   (x,y1) e nullxs & (x,y2) e nullxs

                  Premise

 

            60   (x,y1) e nullxs

                  Split, 59

 

            61   (x,y2) e nullxs

                  Split, 59

 

         Apply definition of nullxs

 

            62   ALL(c2):[(x,c2) e nullxs <=> x e null & c2 e s]

                  U Spec, 23

 

            63   (x,y1) e nullxs <=> x e null & y1 e s

                  U Spec, 62

 

            64   [(x,y1) e nullxs => x e null & y1 e s]

             & [x e null & y1 e s => (x,y1) e nullxs]

                  Iff-And, 63

 

            65   (x,y1) e nullxs => x e null & y1 e s

                  Split, 64

 

            66   x e null & y1 e s => (x,y1) e nullxs

                  Split, 64

 

            67   x e null & y1 e s

                  Detach, 65, 60

 

            68   x e null

                  Split, 67

 

            69   y1 e s

                  Split, 67

 

         Apply definition of null

 

            70   ~x e null

                  U Spec, 15

 

         Apply principle of explosion

 

            71   ~x e null => y1=y2

                  Arb Cons, 68

 

            72   y1=y2

                  Detach, 71, 70

 

   

    Part 3

   

    As Required:

 

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

            4 Conclusion, 59

 

   

    Joining results...

 

      74   ALL(c):ALL(d):[(c,d) e nullxs => c e null & d e s]

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

            Join, 53, 58

 

      75   ALL(c):ALL(d):[(c,d) e nullxs => c e null & d e s]

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

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

            Join, 74, 73

 

   

    As Required:

   

    nullxs is function

 

      76   ALL(c):ALL(d):[c e null & d e s => [d=nullxs(c) <=> (c,d) e nullxs]]

            Detach, 45, 75

 

        

         Prove: ALL(a):[a e null => nullxs(a) e s]

        

         Suppose...

 

            77   x e null

                  Premise

 

         Apply Part 2

 

            78   x e null => EXIST(d):[d e s & (x,d) e nullxs]

                  U Spec, 58

 

            79   EXIST(d):[d e s & (x,d) e nullxs]

                  Detach, 78, 77

 

            80   y e s & (x,y) e nullxs

                  E Spec, 79

 

            81   y e s

                  Split, 80

 

            82   (x,y) e nullxs

                  Split, 80

 

         Apply functionality of nullxs

 

            83   ALL(d):[x e null & d e s => [d=nullxs(x) <=> (x,d) e nullxs]]

                  U Spec, 76

 

            84   x e null & y e s => [y=nullxs(x) <=> (x,y) e nullxs]

                  U Spec, 83

 

            85   x e null & y e s

                  Join, 77, 81

 

            86   y=nullxs(x) <=> (x,y) e nullxs

                  Detach, 84, 85

 

            87   [y=nullxs(x) => (x,y) e nullxs]

             & [(x,y) e nullxs => y=nullxs(x)]

                  Iff-And, 86

 

            88   y=nullxs(x) => (x,y) e nullxs

                  Split, 87

 

            89   (x,y) e nullxs => y=nullxs(x)

                  Split, 87

 

            90   y=nullxs(x)

                  Detach, 89, 82

 

            91   nullxs(x) e s

                  Substitute, 90, 81

 

    As Required:

 

      92   ALL(a):[a e null => nullxs(a) e s]

            4 Conclusion, 77

 

   

    Joining results...

 

      93   Set(null) & Set'(nullxs)

            Join, 5, 22

 

      94   ALL(a):~a e null & ALL(a):ALL(b):~(a,b) e nullxs

            Join, 15, 39

 

      95   ALL(a):~a e null & ALL(a):ALL(b):~(a,b) e nullxs

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

            Join, 94, 92

 

      96   Set(null) & Set'(nullxs)

         & [ALL(a):~a e null & ALL(a):ALL(b):~(a,b) e nullxs

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

            Join, 93, 95

 

 

As Required:

 

97   ALL(s):[Set(s)

    => EXIST(null):EXIST(f):[Set(null) & Set'(f)

    & [ALL(a):~a e null & ALL(a):ALL(b):~(a,b) e f

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

      4 Conclusion, 2