S5 (Modal Logic)

S5 is the strongest of the five standard systems of modal logic, originally proposed by Clarence Irving Lewis and Cooper Harold Langford in their 1932 book Symbolic Logic. It is a normal modal logic — meaning it includes the necessitation rule and the distribution axiom (K) — built on propositional calculus with the modal operators □ (“necessarily”) and ◇ (“possibly”). Its defining feature is that any sequence of modal operators, no matter how long or mixed, collapses to the last operator in the string. ¹

A Simplifying Introduction

Think of modal logic as a system for reasoning about what must be true versus what merely could be true. The operator □ means “in all possible worlds” and ◇ means “in at least one possible world.” Now, what happens when you stack these? Is something that is “possibly necessarily possibly true” the same as something that is “possibly true”? In most modal logics, you cannot simplify such chains. But S5 says you can: any string of modal operators reduces to its last member. So □◇□◇A = ◇A, and ◇□A = □A. This makes S5 the mathematically cleanest modal system, and it is the natural choice when “necessity” means truth in all possible worlds without restriction — what Leibniz envisioned. The cost is that this reduction has philosophically provocative consequences: if something is possibly necessary, then it is necessary. This is the formal backbone of modal versions of the ontological argument. ^{1 2}

Axioms

S5 is characterized by the following axioms:

1. K (Distribution): □(A → B) → (□A → □B)
2. T (Reflexivity): □A → A — whatever is necessary is true
3. 5 (Euclidean): ◇A → □◇A — whatever is possible is necessarily possible

Alternatively, axiom (5) can be replaced by the combination of:

• 4 (Transitivity): □A → □□A — if A is necessary, then it is necessarily necessary
• B (Symmetry): A → □◇A — if A is true, then it is necessarily possible

Both formulations yield the same system. ¹

Plus the Necessitation Rule: if A is a theorem, then □A is a theorem.

Kripke Semantics

In kripke-semantics, S5 is characterized by frames where the accessibility relation R is an equivalence relation — it is simultaneously:

• Reflexive (wRw): every world is accessible from itself → corresponds to axiom (T)
• Transitive (wRv ∧ vRu → wRu): → corresponds to axiom (4)
• Symmetric (wRv → vRw): → corresponds to axiom (B)

Equivalently, R being reflexive and Euclidean (axiom 5) suffices. When R is an equivalence relation, the set of possible worlds is partitioned into equivalence classes. Within each class, every world sees every other. This means the modal status of any proposition is constant within a class: if A is necessary at one world in a class, it is necessary at all worlds in that class. This is why iterated modal operators collapse — there is no “deeper” level of possibility or necessity to access by stacking operators. ¹

Determining the satisfiability of an S5 formula is NP-complete. The hardness proof is trivial (S5 includes propositional logic); membership follows from showing that any satisfiable formula has a model with at most linearly many worlds (in the size of the formula). ¹

Reduction of Modal Operators

The signature feature of S5 is its reduction principles. In S4, strings of the same operator collapse (□□A = □A, ◇◇A = ◇A). In S5, this extends to mixed strings:

Any sequence of □ and ◇ reduces to the last operator in the sequence.

Expression	S5 Reduction
□□A	□A
◇◇A	◇A
□◇A	◇A
◇□A	□A
□◇□◇A	◇A
◇□◇□A	□A

This is because, under the equivalence-relation semantics, there is no distinction between “possibly necessary” and “necessary,” or between “necessarily possible” and “possible.” The accessibility relation does not stratify — every world in an equivalence class is mutually accessible. ²

Philosophical Significance

The Ontological Argument

S5’s reduction principle — specifically ◇□A → □A (“if possibly necessary, then necessary”) — underpins modern modal formulations of the ontological argument. alvin-plantinga has argued this is not counter-intuitive: if X is possibly necessary, it is necessary in at least one possible world; but necessity means truth in all possible worlds; therefore X is necessary in all worlds, i.e., actually true. Leibniz similarly argued: “If a necessary being is possible, it follows that it exists actually.” ¹

Limits of S5

S5 is appropriate when the modality is alethic (concerning genuine necessity and possibility) and the accessibility relation is unrestricted. However, S5 is not appropriate for:

• Deontic logic (obligation): what ought to be need not actually be, so axiom (T) fails
• Temporal logic: the future is not symmetric — tomorrow is accessible from today, but not vice versa
• Epistemic/doxastic logic (single agent): knowing that you know is not the same as knowing (though S5 is sometimes used as an idealized model of knowledge)
• Multimodal logic: when combining different modalities (e.g., “X is possibly [epistemically] necessary [alethically]”), the S5 reduction no longer applies across modality types ¹

Relationship to Other Systems

S5 sits at the top of the standard modal logic hierarchy:

K ⊂ T(K+M) ⊂ S4(T+4) ⊂ S5(T+5)
                   S5 = S4+B = T+4+B = T+5

Every theorem of S4 is a theorem of S5, but not vice versa. S5 is equivalent to T+B+4 and to T+5. ²

See Also

• modal-logic — Overview of the modal logic family and the hierarchy of systems
• kripke-semantics — Possible worlds semantics; the formal framework grounding modal axioms in frame conditions
• alvin-plantinga — Philosopher who used S5’s reduction principles in modal ontological arguments
• gottfried-wilhelm-leibniz — Originated the modal ontological argument using S5’s ◇□A → □A
• possibilism-actualism — Ontological debate concerning the status of merely possible objects
• ontological-arguments — Arguments for God’s existence from a priori premises; the modal version uses S5
• aristotle — Aristotelian essentialism and the modal notions of essence and necessity
• psychophysical-harmony — Bayesian a posteriori argument for theism from consciousness

References

• Lewis, C. I. & Langford, C. H. (1932). Symbolic Logic. — Original proposal of S1–S5.
• Chellas, B. F. (1980). Modal Logic: An Introduction. Cambridge University Press. ¹
• Hughes, G. E. & Cresswell, M. J. (1996). A New Introduction to Modal Logic. Routledge. ¹
• Kracht, M. (1999). Tools and Techniques in Modal Logic. Elsevier. ¹
• Carnielli, W. & Pizzi, C. (2008). Modalities and Multimodalities. Springer. ¹

Footnotes

1. raw/articles/wikipedia-s5-modal-logic.md ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶ ↩⁷ ↩⁸ ↩⁹ ↩¹⁰ ↩¹¹

2. raw/articles/sep-modal-logic.md ↩ ↩² ↩³