INTRODUCTION

============

 

By Dan Christensen

http://www.dcproof.com

 

Here we prove that

 

EXIST(b):[b e u & ALL(a):[a e u => P(a,b)]]  (1)

 

does not necessarily follow from

 

ALL(a):[a e u => EXIST(b):[b e u & P(a,b)]]  (2)

 

where u is the domain of quantification.

 

While, for some relations P, (1) and (2) can both be true, here we construct an example for which (1) is false and (2) is true:

 

We have the domain of quantification u = {0, 1}, and relation P such that P(a,b) iff a=b.

 

 

Outline

-------

 

First we list the required axioms/definitions.

 

Then we establish certain essential facts from these axioms/definitions:

 

 0 e u

 1 e u

 P(0,0)

~P(0,1)

~P(1,0)

 P(1,1) 

 

Then we prove (2) is true: Every element of u has an equal, namely itself.

 

Finally, we prove (1) if false: No element of u is the equal of every element of u since ~0=1 and ~1=0.

 

 

AXIOMS/DEFINITIONS

==================

 

0 and 1 are distinct

 

1     ~0=1

      Axiom

 

 

Define: u

 

2     ALL(a):[a e u <=> a=0 | a=1]

      Axiom

 

 

Define: P

 

3     ALL(a):ALL(b):[a e u & b e u => [P(a,b) <=> a=b]]

      Axiom

 

 

PROOF

=====

 

Establish essential facts

-------------------------

 

Prove: 0 e u

 

Apply definition of u

 

4     0 e u <=> 0=0 | 0=1

      U Spec, 2

 

5     [0 e u => 0=0 | 0=1] & [0=0 | 0=1 => 0 e u]

      Iff-And, 4

 

6     0 e u => 0=0 | 0=1

      Split, 5

 

7     0=0 | 0=1 => 0 e u

      Split, 5

 

8     0=0

      Reflex

 

9     0=0 | 0=1

      Arb Or, 8

 

As Required:

 

10    0 e u

      Detach, 7, 9

 

 

Prove: 1 e u

 

Apply definition of u

 

11    1 e u <=> 1=0 | 1=1

      U Spec, 2

 

12    [1 e u => 1=0 | 1=1] & [1=0 | 1=1 => 1 e u]

      Iff-And, 11

 

13    1 e u => 1=0 | 1=1

      Split, 12

 

14    1=0 | 1=1 => 1 e u

      Split, 12

 

15    1=1

      Reflex

 

16    1=0 | 1=1

      Arb Or, 15

 

As Required:

 

17    1 e u

      Detach, 14, 16

 

 

Prove: P(0,0)

 

Apply definition of P

 

18    ALL(b):[0 e u & b e u => [P(0,b) <=> 0=b]]

      U Spec, 3

 

19    0 e u & 0 e u => [P(0,0) <=> 0=0]

      U Spec, 18

 

20    0 e u & 0 e u

      Join, 10, 10

 

21    P(0,0) <=> 0=0

      Detach, 19, 20

 

22    [P(0,0) => 0=0] & [0=0 => P(0,0)]

      Iff-And, 21

 

23    P(0,0) => 0=0

      Split, 22

 

24    0=0 => P(0,0)

      Split, 22

 

As Required:

 

25    P(0,0)

      Detach, 24, 8

 

 

Prove: ~P(0,1)

 

Apply definition of P

 

26    0 e u & 1 e u => [P(0,1) <=> 0=1]

      U Spec, 18

 

27    0 e u & 1 e u

      Join, 10, 17

 

28    P(0,1) <=> 0=1

      Detach, 26, 27

 

29    [P(0,1) => 0=1] & [0=1 => P(0,1)]

      Iff-And, 28

 

30    P(0,1) => 0=1

      Split, 29

 

31    0=1 => P(0,1)

      Split, 29

 

32    ~0=1 => ~P(0,1)

      Contra, 30

 

As Required:

 

33    ~P(0,1)

      Detach, 32, 1

 

 

Prove: ~P(1,0)

 

Apply definition of P

 

34    ALL(b):[1 e u & b e u => [P(1,b) <=> 1=b]]

      U Spec, 3

 

35    1 e u & 0 e u => [P(1,0) <=> 1=0]

      U Spec, 34

 

36    1 e u & 0 e u

      Join, 17, 10

 

37    P(1,0) <=> 1=0

      Detach, 35, 36

 

38    [P(1,0) => 1=0] & [1=0 => P(1,0)]

      Iff-And, 37

 

39    P(1,0) => 1=0

      Split, 38

 

40    1=0 => P(1,0)

      Split, 38

 

41    ~1=0 => ~P(1,0)

      Contra, 39

 

42    ~0=1 => ~P(1,0)

      Sym, 41

 

As Required:

 

43    ~P(1,0)

      Detach, 42, 1

 

 

Prove: P(1,1)

 

44    1 e u & 1 e u => [P(1,1) <=> 1=1]

      U Spec, 34

 

45    1 e u & 1 e u

      Join, 17, 17

 

46    P(1,1) <=> 1=1

      Detach, 44, 45

 

47    [P(1,1) => 1=1] & [1=1 => P(1,1)]

      Iff-And, 46

 

48    P(1,1) => 1=1

      Split, 47

 

49    1=1 => P(1,1)

      Split, 47

 

As Required:

 

50    P(1,1)

      Detach, 49, 15

 

    

     Prove: ALL(a):[a e u => EXIST(b):[b e u & P(a,b)]]

    

     Suppose...

 

      51    x e u

            Premise

 

     Apply definition of u

 

      52    x e u <=> x=0 | x=1

            U Spec, 2

 

      53    [x e u => x=0 | x=1] & [x=0 | x=1 => x e u]

            Iff-And, 52

 

      54    x e u => x=0 | x=1

            Split, 53

 

      55    x=0 | x=1 => x e u

            Split, 53

 

     Two cases:

 

      56    x=0 | x=1

            Detach, 54, 51

 

         

          Case 1

         

          Prove: x=0 => EXIST(b):[b e u & P(x,b)]

         

          Suppose...

 

            57    x=0

                  Premise

 

            58    0 e u & P(0,0)

                  Join, 10, 25

 

            59    0 e u & P(x,0)

                  Substitute, 57, 58

 

            60    EXIST(b):[b e u & P(x,b)]

                  E Gen, 59

 

     As Required:

 

      61    x=0 => EXIST(b):[b e u & P(x,b)]

            4 Conclusion, 57

 

         

          Case 2

         

          Prove: x=1 => EXIST(b):[b e u & P(x,b)]

         

          Suppose...

 

            62    x=1

                  Premise

 

            63    1 e u & P(1,1)

                  Join, 17, 50

 

            64    1 e u & P(x,1)

                  Substitute, 62, 63

 

            65    EXIST(b):[b e u & P(x,b)]

                  E Gen, 64

 

     As Required:

 

      66    x=1 => EXIST(b):[b e u & P(x,b)]

            4 Conclusion, 62

 

     Join results

 

      67    [x=0 => EXIST(b):[b e u & P(x,b)]]

          & [x=1 => EXIST(b):[b e u & P(x,b)]]

            Join, 61, 66

 

     Apply Cases Rule

 

      68    EXIST(b):[b e u & P(x,b)]

            Cases, 56, 67

 

As Required:

 

69    ALL(a):[a e u => EXIST(b):[b e u & P(a,b)]]

      4 Conclusion, 51

 

    

     Prove: ALL(b):[b e u => EXIST(a):[a e u & ~P(a,b)]]

 

      70    y e u

            Premise

 

     Apply definition of u

 

      71    y e u <=> y=0 | y=1

            U Spec, 2

 

      72    [y e u => y=0 | y=1] & [y=0 | y=1 => y e u]

            Iff-And, 71

 

      73    y e u => y=0 | y=1

            Split, 72

 

      74    y=0 | y=1 => y e u

            Split, 72

 

     Two cases:

 

      75    y=0 | y=1

            Detach, 73, 70

 

         

          Case 1

         

          Prove: y=0 => EXIST(a):[a e u & ~P(a,y)]

         

          Suppose...

 

            76    y=0

                  Premise

 

            77    1 e u & ~P(1,0)

                  Join, 17, 43

 

            78    1 e u & ~P(1,y)

                  Substitute, 76, 77

 

            79    EXIST(a):[a e u & ~P(a,y)]

                  E Gen, 78

 

     As Required:

 

      80    y=0 => EXIST(a):[a e u & ~P(a,y)]

            4 Conclusion, 76

 

         

          Case 2

         

          Prove: y=1 => EXIST(a):[a e u & ~P(a,y)]

         

          Suppose...

 

            81    y=1

                  Premise

 

            82    0 e u & ~P(0,1)

                  Join, 10, 33

 

            83    0 e u & ~P(0,y)

                  Substitute, 81, 82

 

            84    EXIST(a):[a e u & ~P(a,y)]

                  E Gen, 83

 

     As Required:

 

      85    y=1 => EXIST(a):[a e u & ~P(a,y)]

            4 Conclusion, 81

 

     Join results

 

      86    [y=0 => EXIST(a):[a e u & ~P(a,y)]]

          & [y=1 => EXIST(a):[a e u & ~P(a,y)]]

            Join, 80, 85

 

     Apply Cases Rule

 

      87    EXIST(a):[a e u & ~P(a,y)]

            Cases, 75, 86

 

As Required:

 

88    ALL(b):[b e u => EXIST(a):[a e u & ~P(a,b)]]

      4 Conclusion, 70

 

Prove: ~EXIST(b):[b e u & ALL(a):[a e u => P(a,b)]]

 

89    ~EXIST(b):~[b e u => EXIST(a):[a e u & ~P(a,b)]]

      Quant, 88

 

90    ~EXIST(b):~~[b e u & ~EXIST(a):[a e u & ~P(a,b)]]

      Imply-And, 89

 

91    ~EXIST(b):[b e u & ~EXIST(a):[a e u & ~P(a,b)]]

      Rem DNeg, 90

 

92    ~EXIST(b):[b e u & ~~ALL(a):~[a e u & ~P(a,b)]]

      Quant, 91

 

93    ~EXIST(b):[b e u & ALL(a):~[a e u & ~P(a,b)]]

      Rem DNeg, 92

 

94    ~EXIST(b):[b e u & ALL(a):~~[a e u => ~~P(a,b)]]

      Imply-And, 93

 

95    ~EXIST(b):[b e u & ALL(a):[a e u => ~~P(a,b)]]

      Rem DNeg, 94

 

As Required:

 

96    ~EXIST(b):[b e u & ALL(a):[a e u => P(a,b)]]

      Rem DNeg, 95