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.
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.
The axioms for S1 are the axioms for S1 plus
◇(p ∧ q) → ◇p.
The axioms for S3 are the axioms for S1 plus
(p → q) → (¬◇q → ¬◇p).
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 ¬◇¬.
Finally, S5 is S1 plus the axiom
◇p → □◇p
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].