INTRODUCTION

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

The so-called McKinsey Axiom of Modal Logic []<>P => <>[]P or equivalently,

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

is not true in general. If the set of possible worlds w contains to just two worlds x and y such that R(x,y), P(x)

and ~P(x) then this “axiom” is false.

This machine-verified formal proof was prepared with the use of author’s DC Proof 2.0 freeware that is available at http://www.dcproof.com

AXIOMS

******

Set of possible worlds

1 Set(w)

Axiom

Properties of R (accessibility relation)

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

Axiom

Reflexivity

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

Axiom

Symmetry

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

Axiom

Properties of worlds x and y

w = {x, y}

5 ALL(a):[a e w <=> a=x | a=y]

Axiom

6 ~x=y

Axiom

7 P(x)

Axiom

8 ~P(y)

Axiom

9 R(x,y)

Axiom

PROOF

*****

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

Suppose...

10 R(x,z)

Premise

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

U Spec, 2

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

U Spec, 11

13 x e w & z e w

Detach, 12, 10

14 x e w

Split, 13

15 z e w

Split, 13

Two cases:

16 z=x | ~z=x

Or Not

Case 1

17 z=x

Premise

18 R(z,z)

Substitute, 17, 10

19 R(z,x)

Substitute, 17, 18

20 R(z,x) & P(x)

Join, 19, 7

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

E Gen, 20

Case 1

As Required:

22 z=x => EXIST(c):[R(z,c) & P(c)]

4 Conclusion, 17

Case 2:

Prove: ~z=x => EXIST(c):[R(z,c) & P(c)]

Suppose...

23 ~z=x

Premise

24 z e w <=> z=x | z=y

U Spec, 5

25 [z e w => z=x | z=y] & [z=x | z=y => z e w]

Iff-And, 24

26 z e w => z=x | z=y

Split, 25

27 z=x | z=y => z e w

Split, 25

28 z=x | z=y

Detach, 26, 15

29 ~z=x => z=y

Imply-Or, 28

30 z=y

Detach, 29, 23

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

U Spec, 4

32 R(x,z) => R(z,x)

U Spec, 31

33 R(z,x)

Detach, 32, 10

34 R(z,x) & P(x)

Join, 33, 7

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

E Gen, 34

Case 2

As Required:

36 ~z=x => EXIST(c):[R(z,c) & P(c)]

4 Conclusion, 23

37 [z=x => EXIST(c):[R(z,c) & P(c)]]

& [~z=x => EXIST(c):[R(z,c) & P(c)]]

Join, 22, 36

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

Cases, 16, 37

As Required:

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

4 Conclusion, 10

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

Suppose...

40 R(x,z)

Premise

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

U Spec, 2

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

U Spec, 41

43 x e w & z e w

Detach, 42, 40

44 x e w

Split, 43

45 z e w

Split, 43

Two cases to consider:

46 z=y | ~z=y

Or Not

Case 1

47 z=y

Premise

48 z e w => R(z,z)

U Spec, 3

49 R(z,z)

Detach, 48, 45

50 R(z,y)

Substitute, 47, 49

51 R(z,y) & ~P(y)

Join, 50, 8

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

E Gen, 51

Case 1

As Required:

53 z=y => EXIST(c):[R(z,c) & ~P(c)]

4 Conclusion, 47

Case 2

Prove: ~z=y => EXIST(c):[R(z,c) & ~P(c)]

Suppose...

54 ~z=y

Premise

55 z e w <=> z=x | z=y

U Spec, 5

56 [z e w => z=x | z=y] & [z=x | z=y => z e w]

Iff-And, 55

57 z e w => z=x | z=y

Split, 56

58 z=x | z=y => z e w

Split, 56

59 z=x | z=y

Detach, 57, 45

60 ~z=x => z=y

Imply-Or, 59

61 ~z=y => ~~z=x

Contra, 60

62 ~z=y => z=x

Rem DNeg, 61

63 z=x

Detach, 62, 54

64 R(z,y)

Substitute, 63, 9

65 R(z,y) & ~P(y)

Join, 64, 8

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

E Gen, 65

Case 2

As Required:

67 ~z=y => EXIST(c):[R(z,c) & ~P(c)]

4 Conclusion, 54

68 [z=y => EXIST(c):[R(z,c) & ~P(c)]]

& [~z=y => EXIST(c):[R(z,c) & ~P(c)]]

Join, 53, 67

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

Cases, 46, 68

As Required:

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

4 Conclusion, 40

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

U Spec, 2

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

U Spec, 71

73 x e w & y e w

Detach, 72, 9

74 x e w

Split, 73

75 y e w

Split, 73

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

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

Join, 39, 70

77 x e w

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

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

Join, 74, 76

78 EXIST(a):[a e w

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

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

E Gen, 77

79 ~ALL(a):~[a e w

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

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

Quant, 78

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

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

Imply-And, 79

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

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

Rem DNeg, 80

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

Imply-And, 81

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

Rem DNeg, 82

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

Quant, 83

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

Rem DNeg, 84

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

Imply-And, 85

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

Rem DNeg, 86

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

Quant, 87

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

Rem DNeg, 88

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

Imply-And, 89

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

Rem DNeg, 90

As Required:

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

Rem DNeg, 91