Chapter 3. The Brouwerian System

G.E. Hughes & M.J. Cresswell, A New Introduction to Modal Logic, London and New York: Routledge, 1996, pp. 62-64.

 

(8) The Brouwerian System

① B p ⊃ LMp

B (or S5 (8)) p ⊃ LMp

 

② Translation into quantification theory

 

③ S5 (9) MLp ⊃ p

S5 (9) MLp ⊃ p

 

④ Neither of these theorems is in S4. Indeed, if we were to add either as an extra axiom to S4 we should obtain a system at least as strong as S5. (In fact we should obtain exactly S5.)

S5 Mp ⊃ LMp

 

⑤ If we were to add either of them to T instead of to S4 we should obtain not S5 but a system which is weaker than S5 and which neither contains nor is contained in S4. This system has been called the Brouwerian system, and S5(8) the Brouwerian axiom. We shall use ‘B’ to refer to the system and ‘B’ (in bold face) to refer to the axiom.

 

⑥ DR4

 

⑦ DR4 as a primitive transformation rule to S4

Yet another way of obtaining S.5 would be to add DR4 as a primitive transformation rule to S4, without any new axioms; for then, since MMp ⊃ Mp (S4(1)) is a theorem of S4, DR4 would immediately give us Mp ⊃ LMp (i.e. E).

1. MMp ⊃ Mp                           S4(1)
2. Mp ⊃ LMp                            1, DR 4

 

(9) Validity for B

① We show first that B is valid on every frame in which R is symmetrical.

 

② We already know that T is valid on every reflexive frame; so, since the system B is K + T + B, theorem 2.2 gives us the result that B is sound with respect to the class of all frames which are both reflexive and symmetrical. Such frames we shall call B-frames, and we define B-validity as validity on every B-frame.

③ S4 and B are independent systems

∴ S4 and B are independent systems in the sense that neither contains the other, and yet each lies between T and S5.

 

Appendix: K, T, D, S4, S5, and B