THEOREM

*******

 

The intersection of {{0, 1, ...}, {1, 2, ...}, {2, 3, ...}, ...} = {}

 

where {0, 1, ...}, {1, 3, ...}, {2, 3, ...}, etc. are the "end segments" in N.

 

Here, we prove:

 

     ~EXIST(a):ALL(b):[b e ends => a e b]

 

where (informally)

 

     ends = {{0, 1, ...}, {1, 2, ...}, {2, 3, ...}, ...}

 

The following proof makes use of the set theoretic axioms for subsets (lines 12, 18) and power sets (line 6).

 

 

This formal, machine-verified proof was write with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com

 

 

AXIOMS

******

 

1     Set(n)

      Axiom

 

2     0 e n

      Axiom

 

3     ALL(a):[a e n => ~a<a]

      Axiom

 

4     ALL(a):ALL(b):[a e n & b e n => [a<=b <=> a<b | a=b]]

      Axiom

 

5     ALL(a):[a e n => 0<=a]

      Axiom

 

 

PROOF

*****

 

Construct the power set of n

 

Apply the Power Set Axiom

 

6     ALL(a):[Set(a) => EXIST(b):[Set(b)

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

      Power Set

 

7     Set(n) => EXIST(b):[Set(b)

    & ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e n]]]

      U Spec, 6

 

8     EXIST(b):[Set(b)

    & ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e n]]]

      Detach, 7, 1

 

9     Set(pn)

    & ALL(c):[c e pn <=> Set(c) & ALL(d):[d e c => d e n]]

      E Spec, 8

 

Define: pn

 

10   Set(pn)

      Split, 9

 

11   ALL(c):[c e pn <=> Set(c) & ALL(d):[d e c => d e n]]

      Split, 9

 

Construct the set of end segments

 

12   EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e pn & EXIST(b):[b e n & ALL(c):[c e a => b<=c]]]]

      Subset, 10

 

13   Set(ends) & ALL(a):[a e ends <=> a e pn & EXIST(b):[b e n & ALL(c):[c e a => b<=c]]]

      E Spec, 12

 

Define: ends

 

Informally, ends = {{0, 1, ...}, {1, 2, ...}, {2, 3, ...}, ...}

 

14   Set(ends)

      Split, 13

 

15   ALL(a):[a e ends <=> a e pn & EXIST(b):[b e n & ALL(c):[c e a => b<=c]]]

      Split, 13

 

   

    Prove: ~EXIST(a):ALL(b):[b e ends => a e b]

   

    Suppose to the contrary...

 

      16   EXIST(a):ALL(b):[b e ends => a e b]

            Premise

 

    Define: x

 

      17   ALL(b):[b e ends => x e b]

            E Spec, 16

 

    Construct y

   

    Apply the Subset Axiom

 

      18   EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & x<a]]

            Subset, 1

 

      19   Set(y) & ALL(a):[a e y <=> a e n & x<a]

            E Spec, 18

 

    Define: y

 

      20   Set(y)

            Split, 19

 

      21   ALL(a):[a e y <=> a e n & x<a]

            Split, 19

 

    Prove: ~x e y

   

    Apply the definition of y

 

      22   x e y <=> x e n & x<x

            U Spec, 21

 

      23   [x e y => x e n & x<x] & [x e n & x<x => x e y]

            Iff-And, 22

 

      24   x e y => x e n & x<x

            Split, 23

 

      25   x e n & x<x => x e y

            Split, 23

 

      26   ~[x e n & x<x] => ~x e y

            Contra, 24

 

      27   ~~[x e n => ~x<x] => ~x e y

            Imply-And, 26

 

      28   x e n => ~x<x => ~x e y

            Rem DNeg, 27

 

      29   x e n => ~x<x

            U Spec, 3

 

    As Required:

 

      30   ~x e y

            Detach, 28, 29

 

    Sufficient: For x e y  (to obtain contradiction)

 

      31   y e ends => x e y

            U Spec, 17

 

    Prove: y e ends 

   

    Apply definition of ends

 

      32   y e ends <=> y e pn & EXIST(b):[b e n & ALL(c):[c e y => b<=c]]

            U Spec, 15

 

      33   [y e ends => y e pn & EXIST(b):[b e n & ALL(c):[c e y => b<=c]]]

         & [y e pn & EXIST(b):[b e n & ALL(c):[c e y => b<=c]] => y e ends]

            Iff-And, 32

 

      34   y e ends => y e pn & EXIST(b):[b e n & ALL(c):[c e y => b<=c]]

            Split, 33

 

    Sufficient: For y e ends

 

      35   y e pn & EXIST(b):[b e n & ALL(c):[c e y => b<=c]] => y e ends

            Split, 33

 

    Prove: y e pn

   

    Apply definition of pn

 

      36   y e pn <=> Set(y) & ALL(d):[d e y => d e n]

            U Spec, 11

 

      37   [y e pn => Set(y) & ALL(d):[d e y => d e n]]

         & [Set(y) & ALL(d):[d e y => d e n] => y e pn]

            Iff-And, 36

 

      38   y e pn => Set(y) & ALL(d):[d e y => d e n]

            Split, 37

 

    Sufficient: For y e pn

 

      39   Set(y) & ALL(d):[d e y => d e n] => y e pn

            Split, 37

 

        

         Prove: ALL(d):[d e y => d e n]

        

         Suppose...

 

            40   z e y

                  Premise

 

         Apply definition of y

 

            41   z e y <=> z e n & x<z

                  U Spec, 21

 

            42   [z e y => z e n & x<z] & [z e n & x<z => z e y]

                  Iff-And, 41

 

            43   z e y => z e n & x<z

                  Split, 42

 

            44   z e n & x<z => z e y

                  Split, 42

 

            45   z e n & x<z

                  Detach, 43, 40

 

            46   z e n

                  Split, 45

 

    As Required:

 

      47   ALL(d):[d e y => d e n]

            4 Conclusion, 40

 

    Joining results...

 

      48   Set(y) & ALL(d):[d e y => d e n]

            Join, 20, 47

 

    As Required:

 

      49   y e pn

            Detach, 39, 48

 

        

         Prove: ALL(c):[c e y => 0<=c]

        

         Suppose...

 

            50   z e y

                  Premise

 

         Apply definition of y

 

            51   z e y <=> z e n & x<z

                  U Spec, 21

 

            52   [z e y => z e n & x<z] & [z e n & x<z => z e y]

                  Iff-And, 51

 

            53   z e y => z e n & x<z

                  Split, 52

 

            54   z e n & x<z => z e y

                  Split, 52

 

            55   z e n & x<z

                  Detach, 53, 50

 

            56   z e n

                  Split, 55

 

            57   x<z

                  Split, 55

 

         Apply axiom

 

            58   z e n => 0<=z

                  U Spec, 5

 

            59   0<=z

                  Detach, 58, 56

 

    As Required:

 

      60   ALL(c):[c e y => 0<=c]

            4 Conclusion, 50

 

    Joining results...

 

      61   0 e n & ALL(c):[c e y => 0<=c]

            Join, 2, 60

 

      62   EXIST(b):[b e n & ALL(c):[c e y => b<=c]]

            E Gen, 61

 

      63   y e pn

         & EXIST(b):[b e n & ALL(c):[c e y => b<=c]]

            Join, 49, 62

 

      64   y e ends

            Detach, 35, 63

 

      65   x e y

            Detach, 31, 64

 

    Obtain the contradiction...

 

      66   x e y & ~x e y

            Join, 65, 30

 

As Required:

 

67   ~EXIST(a):ALL(b):[b e ends => a e b]

      4 Conclusion, 16