AXIOMS OF MODAL LOGIC DERIVED

*****************************

 

INTRODUCTION

************

 

Here are 9 "axioms" of modal logic that I have been able to derive using DC Proof. No axioms of set theory are cited here. I made use of the standard translations from modal to first-order logic given at

https://en.wikipedia.org/wiki/Standard_translation .

 

1. []P <=> ~<>~P               (lines 6-21)

2. <>P <=> ~[]~P               (lines 22-37)

3. [](P /\ Q) <=> []P /\ []Q   (lines 38-66)

4. []P \/ []Q => [](P \/ Q)    (lines 67-86)

5. [](P => Q) => ([]P => []Q)  (lines 87-99)

6. []P => P                    (lines 100-107)

7. []P => [][]P                (lines 108-136)

8. []P => []<>P                (lines 137-160)

8b. <>P => []<>P               (lines 180-217)

9. P => []<>P                  (lines 161-178)

 

 

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

 

 

AXIOMS

******

 

Set of possible worlds

 

1     Set(w)

      Axiom

 

Properties of accessibility relation R

 

2     ALL(a):ALL(b):[R(a,b) => a e w & b e w]

      Axiom

 

Reflexive

 

3     ALL(a):[a e w => R(a,a)]

      Axiom

 

Symmetric

 

4     ALL(a):ALL(b):[a e w & b e w => [R(a,b) => R(b,a)]]

      Axiom

 

Transitive

 

5     ALL(a):ALL(b):ALL(c):[a e w & b e w & c e w => [R(a,b) & R(b,c) => R(a,c)]]

      Axiom

 

 

PROOF

*****

   

    []P <=> ~<>~P

   

    Prove: ALL(a):[a e w

           => [ALL(b):[R(a,b) => P(b)]

           <=> ~EXIST(b):[R(a,b) & ~P(b)]]]

   

    Suppose...

 

      6     x e w

            Premise

 

         Prove: ALL(b):[R(x,b) => P(b)] => ~EXIST(b):[R(x,b) & ~P(b)]

        

         Suppose...

 

            7     ALL(b):[R(x,b) => P(b)]

                  Premise

 

            8     ~EXIST(b):~[R(x,b) => P(b)]

                  Quant, 7

 

            9     ~EXIST(b):~~[R(x,b) & ~P(b)]

                  Imply-And, 8

 

            10   ~EXIST(b):[R(x,b) & ~P(b)]

                  Rem DNeg, 9

 

    As Required:

 

      11   ALL(b):[R(x,b) => P(b)] => ~EXIST(b):[R(x,b) & ~P(b)]

            4 Conclusion, 7

 

         Prove: ~EXIST(b):[R(x,b) & ~P(b)] => ALL(b):[R(x,b) => P(b)]

        

         Suppose...

 

            12   ~EXIST(b):[R(x,b) & ~P(b)]

                  Premise

 

            13   ~~ALL(b):~[R(x,b) & ~P(b)]

                  Quant, 12

 

            14   ALL(b):~[R(x,b) & ~P(b)]

                  Rem DNeg, 13

 

            15   ALL(b):~~[R(x,b) => ~~P(b)]

                  Imply-And, 14

 

            16   ALL(b):[R(x,b) => ~~P(b)]

                  Rem DNeg, 15

 

            17   ALL(b):[R(x,b) => P(b)]

                  Rem DNeg, 16

 

    As Required:

 

      18   ~EXIST(b):[R(x,b) & ~P(b)] => ALL(b):[R(x,b) => P(b)]

            4 Conclusion, 12

 

      19   [ALL(b):[R(x,b) => P(b)] => ~EXIST(b):[R(x,b) & ~P(b)]]

         & [~EXIST(b):[R(x,b) & ~P(b)] => ALL(b):[R(x,b) => P(b)]]

            Join, 11, 18

 

      20   ALL(b):[R(x,b) => P(b)]

         <=> ~EXIST(b):[R(x,b) & ~P(b)]

            Iff-And, 19

 

1. []P <=> ~<>~P

 

As Required:

 

21   ALL(a):[a e w

    => [ALL(b):[R(a,b) => P(b)]

    <=> ~EXIST(b):[R(a,b) & ~P(b)]]]

      4 Conclusion, 6

 

    <>P <=> ~[]~P

   

    Prove: ALL(a):[a e w

           => [EXIST(b):[R(a,b) & P(b)]

           <=> ~ALL(b):[R(a,b) => ~P(b)]]]

   

    Suppose...

 

      22   x e w

            Premise

 

            23   EXIST(b):[R(x,b) & P(b)]

                  Premise

 

            24   ~ALL(b):~[R(x,b) & P(b)]

                  Quant, 23

 

            25   ~ALL(b):~~[R(x,b) => ~P(b)]

                  Imply-And, 24

 

            26   ~ALL(b):[R(x,b) => ~P(b)]

                  Rem DNeg, 25

 

      27   EXIST(b):[R(x,b) & P(b)] => ~ALL(b):[R(x,b) => ~P(b)]

            4 Conclusion, 23

 

            28   ~ALL(b):[R(x,b) => ~P(b)]

                  Premise

 

            29   ~~EXIST(b):~[R(x,b) => ~P(b)]

                  Quant, 28

 

            30   EXIST(b):~[R(x,b) => ~P(b)]

                  Rem DNeg, 29

 

            31   EXIST(b):~~[R(x,b) & ~~P(b)]

                  Imply-And, 30

 

            32   EXIST(b):[R(x,b) & ~~P(b)]

                  Rem DNeg, 31

 

            33   EXIST(b):[R(x,b) & P(b)]

                  Rem DNeg, 32

 

      34   ~ALL(b):[R(x,b) => ~P(b)] => EXIST(b):[R(x,b) & P(b)]

            4 Conclusion, 28

 

      35   [EXIST(b):[R(x,b) & P(b)] => ~ALL(b):[R(x,b) => ~P(b)]]

         & [~ALL(b):[R(x,b) => ~P(b)] => EXIST(b):[R(x,b) & P(b)]]

            Join, 27, 34

 

      36   EXIST(b):[R(x,b) & P(b)]

         <=> ~ALL(b):[R(x,b) => ~P(b)]

            Iff-And, 35

 

2. <>P <=> ~[]~P

 

As Required:

 

37   ALL(a):[a e w

    => [EXIST(b):[R(a,b) & P(b)]

    <=> ~ALL(b):[R(a,b) => ~P(b)]]]

      4 Conclusion, 22

 

    [](P /\ Q) <=> []P /\ []Q

   

    Prove: ALL(a):[a e w

           => [ALL(b):[R(a,b) => P(b) & Q(b)]

           <=> ALL(b):[R(a,b) => P(b)] & ALL(b):[R(a,b) => Q(b)]]]

   

    Suppose...

 

      38   x e w

            Premise

 

         Prove: ALL(b):[R(x,b) => P(b) & Q(b)]

                => ALL(b):[R(x,b) => P(b)] & ALL(b):[R(x,b) => Q(b)]

        

         Suppose...

 

            39   ALL(b):[R(x,b) => P(b) & Q(b)]

                  Premise

 

             Prove: ALL(b):[R(x,b) => P(b)]

            

             Suppose...

 

                  40   R(x,y)

                        Premise

 

                  41   R(x,y) => P(y) & Q(y)

                        U Spec, 39

 

                  42   P(y) & Q(y)

                        Detach, 41, 40

 

                  43   P(y)

                        Split, 42

 

         As Required:

 

            44   ALL(b):[R(x,b) => P(b)]

                  4 Conclusion, 40

 

             Prove: ALL(b):[R(x,b) => Q(b)]

            

             Suppose...

 

                  45   R(x,y)

                        Premise

 

                  46   R(x,y) => P(y) & Q(y)

                        U Spec, 39

 

                  47   P(y) & Q(y)

                        Detach, 46, 45

 

                  48   P(y)

                        Split, 47

 

                  49   Q(y)

                        Split, 47

 

         As Required:

 

            50   ALL(b):[R(x,b) => Q(b)]

                  4 Conclusion, 45

 

            51   ALL(b):[R(x,b) => P(b)] & ALL(b):[R(x,b) => Q(b)]

                  Join, 44, 50

 

    As Required:

 

      52   ALL(b):[R(x,b) => P(b) & Q(b)]

         => ALL(b):[R(x,b) => P(b)] & ALL(b):[R(x,b) => Q(b)]

            4 Conclusion, 39

 

         Prove: ALL(b):[R(x,b) => P(b)] & ALL(b):[R(x,b) => Q(b)]

                => ALL(b):[R(x,b) => P(b) & Q(b)]

        

         Suppose...

 

            53   ALL(b):[R(x,b) => P(b)] & ALL(b):[R(x,b) => Q(b)]

                  Premise

 

            54   ALL(b):[R(x,b) => P(b)]

                  Split, 53

 

            55   ALL(b):[R(x,b) => Q(b)]

                  Split, 53

 

             Prove: ALL(b):[R(x,b) => P(b) & Q(b)]

            

             Suppose...

 

                  56   R(x,y)

                        Premise

 

                  57   R(x,y) => P(y)

                        U Spec, 54

 

                  58   P(y)

                        Detach, 57, 56

 

                  59   R(x,y) => Q(y)

                        U Spec, 55

 

                  60   Q(y)

                        Detach, 59, 56

 

                  61   P(y) & Q(y)

                        Join, 58, 60

 

         As Required:

 

            62   ALL(b):[R(x,b) => P(b) & Q(b)]

                  4 Conclusion, 56

 

    As Required:

 

      63   ALL(b):[R(x,b) => P(b)] & ALL(b):[R(x,b) => Q(b)]

         => ALL(b):[R(x,b) => P(b) & Q(b)]

            4 Conclusion, 53

 

      64   [ALL(b):[R(x,b) => P(b) & Q(b)]

         => ALL(b):[R(x,b) => P(b)] & ALL(b):[R(x,b) => Q(b)]]

         & [ALL(b):[R(x,b) => P(b)] & ALL(b):[R(x,b) => Q(b)]

         => ALL(b):[R(x,b) => P(b) & Q(b)]]

            Join, 52, 63

 

      65   ALL(b):[R(x,b) => P(b) & Q(b)]

         <=> ALL(b):[R(x,b) => P(b)] & ALL(b):[R(x,b) => Q(b)]

            Iff-And, 64

 

3. [](P /\ Q) <=> []P /\ []Q

 

As Required:

 

66   ALL(a):[a e w

    => [ALL(b):[R(a,b) => P(b) & Q(b)]

    <=> ALL(b):[R(a,b) => P(b)] & ALL(b):[R(a,b) => Q(b)]]]

      4 Conclusion, 38

 

    []P \/ []Q => [](P \/ Q)

   

    Prove: ALL(a):[a e w => [ALL(b):[R(a,b) => P(b)] | ALL(b):[R(a,b) => Q(b)] => ALL(b):[R(a,b) => P(b) | Q(b)]]]

   

    Suppose...

 

      67   x e w

            Premise

 

         Prove: ALL(b):[R(x,b) => P(b)] | ALL(b):[R(x,b) => Q(b)]

                => ALL(b):[R(x,b) => P(b) | Q(b)]

        

         Two cases to consider:

 

            68   ALL(b):[R(x,b) => P(b)] | ALL(b):[R(x,b) => Q(b)]

                  Premise

 

             Case 1

            

             Prove: ALL(b):[R(x,b) => P(b)]

                    => ALL(b):[R(x,b) => P(b) | Q(b)]

            

             Suppose...

 

                  69   ALL(b):[R(x,b) => P(b)]

                        Premise

 

                 Prove: ALL(b):[R(x,b) => P(b) | Q(b)]

                

                 Suppose...

 

                        70   R(x,y)

                              Premise

 

                        71   R(x,y) => P(y)

                              U Spec, 69

 

                        72   P(y)

                              Detach, 71, 70

 

                        73   P(y) | Q(y)

                              Arb Or, 72

 

             As Required:

 

                  74   ALL(b):[R(x,b) => P(b) | Q(b)]

                        4 Conclusion, 70

 

         Case 1

        

         As Required:

 

            75   ALL(b):[R(x,b) => P(b)]

             => ALL(b):[R(x,b) => P(b) | Q(b)]

                  4 Conclusion, 69

 

             Case 2

            

             Prove: ALL(b):[R(x,b) => Q(b)]

                    => ALL(b):[R(x,b) => P(b) | Q(b)]

            

             Suppose...

 

                  76   ALL(b):[R(x,b) => Q(b)]

                        Premise

 

                 Prove: ALL(b):[R(x,b) => P(b) | Q(b)]

                

                 Suppose...

 

                        77   R(x,y)

                              Premise

 

                        78   R(x,y) => Q(y)

                              U Spec, 76

 

                        79   Q(y)

                              Detach, 78, 77

 

                        80   P(y) | Q(y)

                              Arb Or, 79

 

             As Required:

 

                  81   ALL(b):[R(x,b) => P(b) | Q(b)]

                        4 Conclusion, 77

 

         Case 2

        

         As Required:

 

            82   ALL(b):[R(x,b) => Q(b)]

             => ALL(b):[R(x,b) => P(b) | Q(b)]

                  4 Conclusion, 76

 

            83   [ALL(b):[R(x,b) => P(b)]

             => ALL(b):[R(x,b) => P(b) | Q(b)]]

             & [ALL(b):[R(x,b) => Q(b)]

             => ALL(b):[R(x,b) => P(b) | Q(b)]]

                  Join, 75, 82

 

            84   ALL(b):[R(x,b) => P(b) | Q(b)]

                  Cases, 68, 83

 

    As Required:

 

      85   ALL(b):[R(x,b) => P(b)] | ALL(b):[R(x,b) => Q(b)]

         => ALL(b):[R(x,b) => P(b) | Q(b)]

            4 Conclusion, 68

 

4. []P \/ []Q => [](P \/ Q)

 

As Required:

 

86   ALL(a):[a e w

    => [ALL(b):[R(a,b) => P(b)] | ALL(b):[R(a,b) => Q(b)]

    => ALL(b):[R(a,b) => P(b) | Q(b)]]]

      4 Conclusion, 67

 

    [](P => Q) => ([]P => []Q)

   

    Prove: ALL(a):[a e w => [ALL(b):[R(a,b) => [P(b) => Q(b)]] => [ALL(b):[R(a,b) => P(b)] => ALL(b):[R(a,b) => Q(b)]]]]

   

    Suppose...

 

      87   x e w

            Premise

 

         Prove: ALL(b):[R(x,b) => [P(b) => Q(b)]]

                => [ALL(b):[R(x,b) => P(b)] => ALL(b):[R(x,b) => Q(b)]]

        

         Suppose..

 

            88   ALL(b):[R(x,b) => [P(b) => Q(b)]]

                  Premise

 

             Prove: ALL(b):[R(x,b) => P(b)] => ALL(b):[R(x,b) => Q(b)]

            

             Suppose...

 

                  89   ALL(b):[R(x,b) => P(b)]

                        Premise

 

                 Prove: ALL(b):[R(x,b) => Q(b)]

                

                 Suppose...

 

                        90   R(x,y)

                              Premise

 

                        91   R(x,y) => P(y)

                              U Spec, 89

 

                        92   P(y)

                              Detach, 91, 90

 

                        93   R(x,y) => [P(y) => Q(y)]

                              U Spec, 88

 

                        94   P(y) => Q(y)

                              Detach, 93, 90

 

                        95   Q(y)

                              Detach, 94, 92

 

             As Required:

 

                  96   ALL(b):[R(x,b) => Q(b)]

                        4 Conclusion, 90

 

         As Required:

 

            97   ALL(b):[R(x,b) => P(b)] => ALL(b):[R(x,b) => Q(b)]

                  4 Conclusion, 89

 

    As Required:

 

      98   ALL(b):[R(x,b) => [P(b) => Q(b)]]

         => [ALL(b):[R(x,b) => P(b)] => ALL(b):[R(x,b) => Q(b)]]

            4 Conclusion, 88

 

5. [](P => Q) => ([]P => []Q)

 

As Required:

 

99   ALL(a):[a e w

    => [ALL(b):[R(a,b) => [P(b) => Q(b)]]

    => [ALL(b):[R(a,b) => P(b)] => ALL(b):[R(a,b) => Q(b)]]]]

      4 Conclusion, 87

 

    []P => P

   

    Prove: ALL(a):[a e w => ALL(b):[R(a,b) => P(b)] => P(a)]

   

    Suppose...

 

      100  x e w

            Premise

 

            101  ALL(b):[R(x,b) => P(b)]

                  Premise

 

            102  R(x,x) => P(x)

                  U Spec, 101

 

            103  x e w => R(x,x)

                  U Spec, 3

 

            104  R(x,x)

                  Detach, 103, 100

 

            105  P(x)

                  Detach, 102, 104

 

    As Required:

 

      106  ALL(b):[R(x,b) => P(b)] => P(x)

            4 Conclusion, 101

 

6. []P => P

 

As Required:

 

107  ALL(a):[a e w => [ALL(b):[R(a,b) => P(b)] => P(a)]]

      4 Conclusion, 100

 

    []P => [][]P

   

    Prove: ALL(a):[a e s => [ALL(b):[R(a,b) => P(b)] => ALL(b):[R(a,b) => ALL(c):[R(b,c) => P(c)]]]]

   

    Suppose...

 

      108  x e w

            Premise

 

        

         Prove: ALL(b):[R(x,b) => P(b)]

                => ALL(b):[R(x,b) => ALL(c):[R(b,c) => P(c)]]

        

         Suppose...

 

            109  ALL(b):[R(x,b) => P(b)]

                  Premise

 

            

             Prove: ALL(b):[R(x,b) => ALL(c):[R(b,c) => P(c)]]

            

             Suppose...

 

                  110  R(x,y)

                        Premise

 

                

                 Prove: ALL(c):[R(y,c) => P(c)]

                

                 Suppose...

 

                        111  R(y,z)

                              Premise

 

                        112  R(x,z) => P(z)

                              U Spec, 109

 

                        113  ALL(b):[R(x,b) => x e w & b e w]

                              U Spec, 2

 

                        114  R(x,y) => x e w & y e w

                              U Spec, 113

 

                        115  x e w & y e w

                              Detach, 114, 110

 

                        116  x e w

                              Split, 115

 

                        117  y e w

                              Split, 115

 

                        118  ALL(b):[R(y,b) => y e w & b e w]

                              U Spec, 2

 

                        119  R(y,z) => y e w & z e w

                              U Spec, 118

 

                        120  y e w & z e w

                              Detach, 119, 111

 

                        121  y e w

                              Split, 120

 

                        122  z e w

                              Split, 120

 

                        123  x e w & y e w

                              Join, 116, 117

 

                        124  x e w & y e w & z e w

                              Join, 123, 122

 

                        125  ALL(b):ALL(c):[x e w & b e w & c e w => [R(x,b) & R(b,c) => R(x,c)]]

                              U Spec, 5

 

                        126  ALL(c):[x e w & y e w & c e w => [R(x,y) & R(y,c) => R(x,c)]]

                              U Spec, 125

 

                        127  x e w & y e w & z e w => [R(x,y) & R(y,z) => R(x,z)]

                              U Spec, 126

 

                        128  R(x,y) & R(y,z) => R(x,z)

                              Detach, 127, 124

 

                        129  R(x,y) & R(y,z)

                              Join, 110, 111

 

                        130  R(x,z)

                              Detach, 128, 129

 

                        131  R(x,z) => P(z)

                              U Spec, 109

 

                        132  P(z)

                              Detach, 131, 130

 

             As Required:

 

                  133  ALL(c):[R(y,c) => P(c)]

                        4 Conclusion, 111

 

         As Required:

 

            134  ALL(b):[R(x,b) => ALL(c):[R(b,c) => P(c)]]

                  4 Conclusion, 110

 

    As Required:

 

      135  ALL(b):[R(x,b) => P(b)]

         => ALL(b):[R(x,b) => ALL(c):[R(b,c) => P(c)]]

            4 Conclusion, 109

 

7. []P => [][]P

 

As Required:

 

136  ALL(a):[a e w

    => [ALL(b):[R(a,b) => P(b)]

    => ALL(b):[R(a,b) => ALL(c):[R(b,c) => P(c)]]]]

      4 Conclusion, 108

 

    []P => []<>P

   

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

 

      137  x e w

            Premise

 

        

         Prove: ALL(b):[R(x,b) => P(b)]

                => ALL(b):[R(x,b) => EXIST(c):[R(b,c) & P(c)]]

        

         Suppose...

 

            138  ALL(b):[R(x,b) => P(b)]

                  Premise

 

                  139  R(x,y)

                        Premise

 

                  140  R(x,y) => P(y)

                        U Spec, 138

 

                  141  P(y)

                        Detach, 140, 139

 

                  142  ALL(b):[x e w & b e w => [R(x,b) => R(b,x)]]

                        U Spec, 4

 

                  143  x e w & y e w => [R(x,y) => R(y,x)]

                        U Spec, 142

 

                  144  ALL(b):[R(x,b) => x e w & b e w]

                        U Spec, 2

 

                  145  R(x,y) => x e w & y e w

                        U Spec, 144

 

                  146  x e w & y e w

                        Detach, 145, 139

 

                  147  x e w

                        Split, 146

 

                  148  y e w

                        Split, 146

 

                  149  x e w & y e w

                        Join, 137, 148

 

                  150  R(x,y) => R(y,x)

                        Detach, 143, 149

 

                  151  R(y,x)

                        Detach, 150, 139

 

                  152  R(x,x) => P(x)

                        U Spec, 138

 

                  153  x e w => R(x,x)

                        U Spec, 3

 

                  154  R(x,x)

                        Detach, 153, 147

 

                  155  P(x)

                        Detach, 152, 154

 

                  156  R(y,x) & P(x)

                        Join, 151, 155

 

                  157  EXIST(c):[R(y,c) & P(c)]

                        E Gen, 156

 

            158  ALL(b):[R(x,b) => EXIST(c):[R(b,c) & P(c)]]

                  4 Conclusion, 139

 

    As Required:

 

      159  ALL(b):[R(x,b) => P(b)]

         => ALL(b):[R(x,b) => EXIST(c):[R(b,c) & P(c)]]

            4 Conclusion, 138

 

8. []P => []<>P

 

As Required:

 

160  ALL(a):[a e w

    => [ALL(b):[R(a,b) => P(b)]

    => ALL(b):[R(a,b) => EXIST(c):[R(b,c) & P(c)]]]]

      4 Conclusion, 137

 

    P => []<>P

   

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

   

    Suppose...

 

      161  x e w

            Premise

 

        

         Prove: P(x) => ALL(b):[R(x,b) => EXIST(c):[R(b,c) & P(c)]]

        

         Suppose...

 

            162  P(x)

                  Premise

 

            

             Prove: ALL(b):[R(x,b) => EXIST(c):[R(b,c) & P(c)]]

            

             Suppose...

 

                  163  R(x,y)

                        Premise

 

                  164  ALL(b):[x e w & b e w => [R(x,b) => R(b,x)]]

                        U Spec, 4

 

                  165  x e w & y e w => [R(x,y) => R(y,x)]

                        U Spec, 164

 

                  166  ALL(b):[R(x,b) => x e w & b e w]

                        U Spec, 2

 

                  167  R(x,y) => x e w & y e w

                        U Spec, 166

 

                  168  x e w & y e w

                        Detach, 167, 163

 

                  169  x e w

                        Split, 168

 

                  170  y e w

                        Split, 168

 

                  171  x e w & y e w

                        Join, 161, 170

 

                  172  R(x,y) => R(y,x)

                        Detach, 165, 171

 

                  173  R(y,x)

                        Detach, 172, 163

 

                  174  R(y,x) & P(x)

                        Join, 173, 162

 

                  175  EXIST(c):[R(y,c) & P(c)]

                        E Gen, 174

 

         As Required:

 

            176  ALL(b):[R(x,b) => EXIST(c):[R(b,c) & P(c)]]

                  4 Conclusion, 163

 

    As Required:

 

      177  P(x) => ALL(b):[R(x,b) => EXIST(c):[R(b,c) & P(c)]]

            4 Conclusion, 162

 

9. P => []<>P

 

As Required:

 

178  ALL(a):[a e w

    => [P(a) => ALL(b):[R(a,b) => EXIST(c):[R(b,c) & P(c)]]]]

      4 Conclusion, 161

   

 

   

    <>P => []<>P

   

    Prove: ALL(a):[a e w

           => [EXIST(b):[R(a,b) & P(b)]

           => ALL(b):[R(a,b) => EXIST(c):[R(b,c) & P(c)]]]]                                                                           

   

    Suppose...

 

      180  x e w

            Premise

 

         Prove: EXIST(b):[R(x,b) & P(b)]

                => ALL(b):[R(x,b) => EXIST(c):[R(b,c) & P(c)]]

        

         Suppose...

 

            181  EXIST(b):[R(x,b) & P(b)]

                  Premise

 

            182  R(x,y) & P(y)

                  E Spec, 181

 

            183  R(x,y)

                  Split, 182

 

            184  P(y)

                  Split, 182

 

            185  ALL(b):[R(x,b) => x e w & b e w]

                  U Spec, 3

 

            186  R(x,y) => x e w & y e w

                  U Spec, 185

 

            187  x e w & y e w

                  Detach, 186, 183

 

            188  x e w

                  Split, 187

 

            189  y e w

                  Split, 187

 

             Prove: ALL(b):[R(x,b) => EXIST(c):[R(b,c) & P(c)]]

            

             Suppose...

 

                  190  R(x,z)

                        Premise

 

                  191  R(x,z) => x e w & z e w

                        U Spec, 185

 

                  192  x e w & z e w

                        Detach, 191, 190

 

                  193  x e w

                        Split, 192

 

                  194  z e w

                        Split, 192

 

                  195  ALL(b):[x e w & b e w => [R(x,b) => R(b,x)]]

                        U Spec, 5

 

                  196  x e w & y e w => [R(x,y) => R(y,x)]

                        U Spec, 195

 

                  197  x e w & y e w

                        Join, 188, 189

 

                  198  R(x,y) => R(y,x)

                        Detach, 196, 197

 

                  199  R(y,x)

                        Detach, 198, 183

 

                  200  ALL(b):ALL(c):[y e w & b e w & c e w => [R(y,b) & R(b,c) => R(y,c)]]

                        U Spec, 6

 

                  201  ALL(c):[y e w & x e w & c e w => [R(y,x) & R(x,c) => R(y,c)]]

                        U Spec, 200

 

                  202  y e w & x e w & z e w => [R(y,x) & R(x,z) => R(y,z)]

                        U Spec, 201

 

                  203  y e w & x e w

                        Join, 189, 188

 

                  204  y e w & x e w & z e w

                        Join, 203, 194

 

                  205  R(y,x) & R(x,z) => R(y,z)

                        Detach, 202, 204

 

                  206  R(y,x) & R(x,z)

                        Join, 199, 190

 

                  207  R(y,z)

                        Detach, 205, 206

 

                  208  ALL(b):[y e w & b e w => [R(y,b) => R(b,y)]]

                        U Spec, 5

 

                  209  y e w & z e w => [R(y,z) => R(z,y)]

                        U Spec, 208

 

                  210  y e w & z e w

                        Join, 189, 194

 

                  211  R(y,z) => R(z,y)

                        Detach, 209, 210

 

                  212  R(z,y)

                        Detach, 211, 207

 

                  213  R(z,y) & P(y)

                        Join, 212, 184

 

                  214  EXIST(c):[R(z,c) & P(c)]

                        E Gen, 213

 

         As Required:

 

            215  ALL(b):[R(x,b) => EXIST(c):[R(b,c) & P(c)]]

                  4 Conclusion, 190

 

    As Required:

 

      216  EXIST(b):[R(x,b) & P(b)]

         => ALL(b):[R(x,b) => EXIST(c):[R(b,c) & P(c)]]

            4 Conclusion, 181

 

8b. <>P => []<>P

 

As Required:

 

217  ALL(a):[a e w

    => [EXIST(b):[R(a,b) & P(b)]

    => ALL(b):[R(a,b) => EXIST(c):[R(b,c) & P(c)]]]]

      4 Conclusion, 180