Aristotle and the medievals discussed modal logic; but its modern form developed with Hugh MacColl in the late 19th century, and then especially in the work of C.I. Lewis beginning with his dissertation in 1910. (In this document, he is the only Lewis who will be discussed.) Lewis was in the first place trying to develop a notion of implication closer to the English conditional than Russell and Whitehead's ⊃. Lewis's notion(s) are called "strict conditionals" and symbolized as ⥽, which we can define as:
φ ⥽ ψ =def □(φ ⊃ ψ)
The behavior of this conditional will obviously depend on the strength of the underlying modal framework (the behavior of □). Lewis published a book A Survey of Symbolic Logic in 1918, but the system there had a flaw that trivialized the modality; Lewis fixed the flaw resulting in a system that he later called S3. In 1932 Lewis published a book with Langford Symbolic Logic that described five systems S1 -- S5, and stated his preference for S2 being the correct logic for ⥽. At the time it wasn't known whether S2 was weaker than S3, but this was verified later; all of these systems get progressively stronger.
Modal logic flourished after Lewis's initial work, and one high point was Kripke's work in the late 50s and early 60s establishing completeness proofs for semantics that he and others had developed for the many logical systems then being investigated, and his identification of what is now known as the weakest "normal" modal logic, nowadays called K. Lewis's S4 and S5 are strengthenings of K, among some other systems whose names you may have encountered (especially D, T, and B); and all of these systems are amenable to the kind of semantic analysis you're probably familiar with, in terms of possible worlds and accessibility relations. Lewis's S2 and S3 have to receive a different kind of semantics that lets in some "non-normal" possible worlds, and Lewis's S1 has to receive an even more different semantics. So although S4/S5 can be reached by adding axioms to Lewis's weaker systems, it's more natural to group S4 and S5 together with the other "normal" modal logics, which are strengthenings of K, as a natural family of logics (with many members, some more to be described below). Lewis's S2 and S3 belong to a weaker family of logics, which we'll explain below (Segerberg 1971 called this family "quasi-regular" logics). There is also a parallel, even weaker family with names like E2, E3 and so on, developed in Lemmon 1957. (Segerberg called this family "regular" logics.)
There are also many other modal logics, like Lewis's S1, that don't fit into those three natural groups. For Lewis, the key difference between S1 and S2 was that the latter validated ◇(φ ∧ ψ) ⥽ (◇φ ∧ ◇ψ).) One especially weak system is S0.50 from Lemmon 1957 (Priest 2008 Ch.4 calls it "System L"). We won't be discussing these systems here.
All of the modal logics we will discuss contain the non-modal classical propositional calculus. Also, in all the logics we'll discuss, ◇φ can be defined in the usual way as ¬□¬φ. (In some weaker logics we're ignoring, that is not so straightforward; see Priest 2008 §4.4a.10--12.)
Here are some inference rules that modal logics may or may not include. I express the material biconditional as ⊂⊃ and the strict biconditional as ⥼⥽, with ⥽ defined as above.
RE. From ⊢ φ ⊂⊃ ψ, infer ⊢ □φ ⊂⊃ □ψ.
RM. From ⊢ φ ⊃ ψ, infer ⊢ □φ ⊃ □ψ. (This rule is sometimes called "R*". It is equivalent to RE together with axiom M, described below.)
RK. From ⊢ φ1 ∧ ... ∧ φk ⊃ ψ, for k ≥ 0, infer ⊢ □φ1 ∧ ... ∧ □φk ⊃ □ψ. (This has Rules RM and Nec as special cases.)
Becker's Rule. From ⊢ φ ⥽ ψ, infer ⊢ □φ ⥽ □ψ.
Nec[essitation]. From ⊢ φ, infer ⊢ □φ.
Restricted Nec. If φ is an axiom, or is a theorem in virtue of its non-modal form, infer ⊢ □φ.
The weakest normal modal logic K is standardly axiomatized as an extension of classical propositional logic that adds the rule of Necessitation and the following axiom:
K. □(φ ⊃ ψ) ⊃ (□φ ⊃ □ψ)
All of the other rules listed above can be derived in this system. (A different axiomitization of the same system would use RM (or RE and M) instead of Nec, plus the axiom N (which says □⊤), plus either the axiom K or the axiom C, described below. Another strategy uses simply the rule RK.)
The semantics for system K are what you're familiar with, with □φ being true at a world w (in a given model) iff φ is true at every world accessible from w; and φ ⊨ ψ (in a given model) iff every world where φ is true is also a world where ψ is true.
Strengthenings of K can be specified by adding axioms to the logic, or by placing constraints on the accessibility relation in the semantic models.
Constraints commonly considered include:
extendability or seriality: for all w, ∃u where wRu (in other words, the relation has no "dead ends")
reflexivity: for all w, wRw
symmetry: for all u,v: if uRv then vRu
transitivity: for all w,u,v: if wRu and uRv then wRv
density: for all w,v: if wRv then ∃u where wRu and uRv (note that u doesn't need to be distinct from w and v)
right Euclidean: for all w,u,v: if wRu and wRv then uRv
Another constraint I'll mention is:
left Euclidean: for all w,u,v: if uRw and vRw then uRv
In modal logic discussions, "Euclidean" is often used without any prefix to mean "right Euclidean."
Here are some interesting entailments, that you can verify: If a relation is reflexive, it's extendable (w itself is always a world that w stands in R to) and dense. If a relation is extendable and symmetric and transitive, then it's reflexive. If a relation is reflexive and (either left or right) Euclidean, then it's symmetric. And finally, if a relation is symmetric, then it has either all or none of the following properties: transitivity, right Euclideaness, left Euclideaness.
Here are some interesting formulas, which are theorems of some modal systems:
M. □(φ ∧ ψ) ⊃ (□φ ∧ □ψ)
As indicated, this formula is sometimes called M, but that name has also been used for a variety of other axioms and systems, too. The converse of this formula is sometimes called C. Both of these are theorems of K. C is much less popular than M.
The following formulas are not theorems of K:
D. □φ ⊃ ◇φ
This is called D because it's the basis of the Standard Deontic Logic, where it's understood to be saying that if there's an obligation for φ, there's not also an obligation for ¬φ. (Or in brief, "ought implies may.") The modal system D can be gotten by adding axiom D to K, or equivalently, by adding the axiom P, which says ◇⊤ (in brief, "something is permitted"). This corresponds to requiring that the accessibility relation in the semantics is extendable/serial.
T. □φ ⊃ φ
This is a theorem in all of Lewis's systems S1 -- S5. The modal system T can be gotten by adding T to K (or equivalently, by adding the axiom φ ⊃ ◇φ). This corresponds to requiring that the accessibility relation in the semantics is reflexive. System T is a proper strengthening of D (so all theorems of D are theorems of T, but not vice versa). That's what you'd expect, given that reflexive relations are always extendable, but not vice versa.
B. φ ⊃ □◇φ
This is called B because of a tenuous connection to Brouwer's intuitionistic logic. (See McKinsey and Tarski 1948 for a deeper connection between intuitionistic logic and modal system S4.) Adding axiom B to a normal modal system (or equivalently, adding ◇□φ ⊃ φ, or □(◇φ ⊃ ψ) ⊃ (φ ⊃ □ψ), corresponds to requiring that the accessibility relation in the semantics is symmetric. If B is added to K, the result is called KB; if added to D, the result is called DB (or KDB); if added to T, the result is called simply B (or KTB).
4. □φ ⊃ □□φ
Adding axiom 4 to a normal modal system (or equivalently, adding ◇◇φ ⊃ ◇φ) corresponds to requiring that the accessibility relation in the semantics is transitive. If 4 is added to K, the result is called K4; if added to D, the result is called D4 (or KD4); if added to T, the result is Lewis's system S4. (That's why this axiom is called 4).
The converse of axiom 4, called C4, corresponds to requiring that the accessibility relation in the semantics is dense.
5. ◇φ ⊃ □◇φ
Adding axiom 5 to a normal modal system (or equivalently, adding ◇□φ ⊃ □φ) corresponds to requiring that the accessibility relation in the semantics is right Euclidean. If 5 is added to K, the result is called K5; if added to D, the result is called D5 (or KD5); if added to T, the result is Lewis's system S5. (That's why this axiom is called 5; some authors instead call it E for "Euclidean".)
Here are some interesting entailments. As we already mentioned, in system K T entails D; so all strengthenings of T will contain the corresponding strengthenings of D. Next, sometimes we add both axiom 4 and 5 to a modal system. If they're added to K, the result is K45 (this is properly stronger than both K4 and K5); if they're added to D, the result is D45 (or KD45; this is properly stronger than both D4 and D5). In any strengthening of K that includes B, 4 is a theorem iff 5 is. (As you'd expect, given that a symmetric relation is transitive iff it's right Euclidean.) In any strengthening of T, the converse of 4 and 5 are already theorems. Finally, in any strengthening of T, 5 entails each of 4 and B.
This diagram from the SEP article on Modal Logic illustrates some of these relationships. When a system X occurs connected by a line below and/or to the left of a system Y, then Y is a proper strengthening of X:
Note that the author of that article and diagram (James Garson) calls system T "System M".
Next let's consider some modal logics weaker than K.
Chellas 1980 defines a "classical modal logic" as one validating at least the rule RE, and having □ and ◇ as duals. He named the weakest such logic E. Some interesting facts about E and its strengthenings:
Giving a semantics for these logics in full generality requires different methods than the ones we've been discussing so far, that have used accessibility relations. (You need to use "neighborhood models," also sometimes called "minimal" or "Scott-Montague" models.) But an interesting subset of them can be handled with only a small variation on our existing techniques. None of these systems have the Rule of Necessitation, and moreover none have any theorems of the form ⊢ □□φ.
The systems we'll consider can all be given a semantics like this: In addition to "normal" possible worlds, a model may also contain some "non-normal" possible worlds. Any non-normal world must be "seen by" (accessible to) some normal worlds. In normal worlds, the interpretation of formulas is as it was before, including that □φ is true there iff φ is true at all accessible worlds (both normal and non-normal). If there are non-normal worlds, nonmodal formulas are interpreted there as usual. But modal formulas are interpreted specially, namely: □φ is always false, and ◇φ is always true. (So non-normal worlds are ones where "everything is possible.")
If we then define entailment such that ⊨ means truth-preservation in all worlds (Segerberg 1971 called such systems "regular", see esp. his Ch. 4), we get the series of modal systems E20, E2, E30, and so on. If we instead define entailment such that ⊨ means truth-preservation in all normal worlds (Segerberg called such systems "quasi-regular"), we get the series of modal systems S20, S2, S30, and so on. The latter series includes Lewis's systems S2 and S3. There is systematicity to the way these systems are named; but because Lewis didn't "leave enough space" in his original enumeration, the numbering system does have some quirks.
The natural way to organize these systems is to see the E-systems as coming in two groups of six, and the corresponding S-systems as being semantic strengthenings of them (the S-systems have more theorems). The base group of six consists of E20, E2, E30, E3, E3.50 and E3.5. (I've only seen some of these names in the literature; I posit the others for systematicity.) This group has further internal structure, and corresponds roughly to the normal modal systems K, T, K4, S4, KB4/KB5, and S5. That is:
E20 has no constraints on the accessibility relation (this is equivalent to Chellas's EMC)
E2 = E20 + the accessibility relation is reflexive (as in T)
E30 = E20 + the accessibility relation is transitive (as in K4)
E3 = E30 + the accessibility relation is also reflexive (as in S4)
E3.50 = E20 + the accessibility relation is transitive/Euclidean and symmetric (as in KB4/KB5)
E3.5 = E3.50 + the accessibility relation is also reflexive (as in S5)
The systems S20 -- S3.5 differ only in their definition of ⊨. (Most of these names have been used in the literature. Priest 2008 Ch.4 calls S20 "System N".)
Note that with all of the systems just mentioned, a model may have non-normal worlds, but need not do so. With the next group of six E-systems, models are required to have non-normal worlds. (This corresponds to adding the axiom ◇◇φ.) These systems can be called E60, E6, E70, E7, E7.50 and E7.5; and mutatis mutandis for the systems S60 -- S7.5. Note that even though these systems are numbered greater than 5, S6 for example isn't a strengthening of Lewis's S4 or S5. This is one of the numbering quirks. Some authors call S7.5 "S9". They skip the number 8 because S8 was used to name a different strengthening of S3 than S7 or S9. (In S8, every normal world sees an non-normal world.)
How about axiomatizations?
As mentioned before, none of these non-normal systems include the Rule of Necessitation. The "regular" modal systems (the E2-series) all instead include the rule:
RM. From ⊢ φ ⊃ ψ, infer ⊢ □φ ⊃ □ψ.
The E2-series also include the K axiom. The "quasi-regular" modal systems (the S2-series) also include the K axiom, but have different rules:
Restricted Nec. If φ is an axiom or a theorem in virtue of its non-modal form, infer ⊢ □φ.
Becker's Rule. From ⊢ φ ⥽ ψ, infer ⊢ □φ ⥽ □ψ.
These rules and axioms give you the minimal systems in each series (E20 and S20). You can get the logics that are sound and complete for the models with reflexive accessibility relations (the ones without the 0) by adding axiom T. This applies to both the E2-systems and the S2-systems.
You can get the logics that are sound and complete for the models with transitive accessibility relations by adding an axiom version of Becker's Rule: (φ ⥽ ψ) ⊃ (□φ ⥽ □ψ). Again, this applies to both the E2-systems and the S2-systems.
You can get S3.5 by adding either axiom 5 or axiom B to system S3. But to get E3.5, you'd have to add a weaker axiom to E3, which we haven't yet identified. (If you added 5 to E3, you'd get the normal modal logic S5.)
Thanks to Harvey Lederman and Graham Priest for suggestions and help sorting out some confusions!
Brian F. Chellas, Modal Logic: An Introduction, Cambridge, 1980
Ian Hacking, "What is strict implication?" Journal of Symbolic Logic 28 (1963), 51-71
G.E. Hughes and Max J. Cresswell, A New Introduction to Modal Logic, Routledge, 1996
E.J. Lemmon, "New Foundations for Lewis Modal Systems," Journal of Symbolic Logic 22 (1957), 176–186
C.I. Lewis, A Survey of Symbolic Logic, Univ of California, 1918
C.I. Lewis and C.H. Langford, Symbolic Logic, New York: Dover, 1932
J.C.C. McKinsey and Alfred Tarski, "Some Theorems About the Sentential Calculi of Lewis and Heyting," Journal of Symbolic Logic 13 (1948), 1-15
Graham Priest, An Introduction to Non-Classical Logic, 2nd ed., Cambridge Univ. Press, 2001
Krister Segerberg, An Essay in Classical Modal Logic, Uppsala: Filosotiska studier, 1971