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