C. I. Lewis and C. H. Langford gave five axiom systems for modal logic, labeled S1 through S5, in their seminal book Symbolic Logic in 1932. You’ll see lots of references to S4 and S5, but it takes some research to find the definitions of S1, S2, and S3. Most interest in modal logic focuses on “normal” modal logics, which includes S4 and S5, but not the weaker systems S1 through S3.
S1 axioms
The axioms for S1 are as follows:
- (p ∧ q) → (q ∧ p)
- (p ∧ q) → p
- p → (p ∧ p)
- ((p ∧ q) ∧ r) → (p ∧ (q ∧ r))
- ((p → q) ∧ (q → r)) → (p → r)
- (p ∧ (p → q)) → q
Originally S1 had an additional axiom
p → ¬¬ p
but this was later discovered to be derivable from the other axioms.
S2 axioms
The axioms for S1 are the axioms for S1 plus
◇(p ∧ q) → ◇p.
S3 axioms
The axioms for S3 are the axioms for S1 plus
(p → q) → (¬◇q → ¬◇p).
S4 axioms
The axioms for S4 and those of S1 and
◇◇p → ◇p
Equivalently, one could replace the axiom above with its dual
□p → □□p
though Lewis and Langford didn’t use the symbol □ for ¬◇¬.
S5 axioms
Finally, S5 is S1 plus the axiom
◇p → □◇p
Related posts
For much more information on logic system axioms, see John Halleck’s compendium of logic systems.
For more on the history of modal logic, see Robert Goldblatt’s history [pdf].