Modal logic is the branch of logic that studies reasoning about necessity and possibility. It extends classical propositional and predicate logic by introducing modal operators that qualify the truth of a proposition. Where classical logic deals with what is actually the case, modal logic provides formal tools for reasoning about what must be the case, what could be the case, what is known to be the case, what is believed to be the case, what ought to be the case, and what has always or will eventually be the case.
The fundamental modal operators are the box (□) and the diamond (◇). These operators are interdefinable: ◇A is equivalent to ¬□¬A, and □A is equivalent to ¬◇¬A. Modal logic is not a single system but a family of systems, each characterized by different axioms that correspond to different properties of the accessibility relation between possible worlds in Kripke semantics.
The study of modality dates back to Aristotle, who analyzed modal syllogisms in the Prior Analytics, distinguishing between assertoric, apodeictic (necessary), and problematic (possible) propositions. Medieval logicians including William of Ockham and John Duns Scotus developed sophisticated theories of modality, exploring distinctions between different kinds of necessity.
Modern modal logic begins with C.I. Lewis in the early twentieth century. Dissatisfied with the material conditional of Principia Mathematica, Lewis introduced strict implication, defined as □(A → B). Between 1918 and 1932, he developed five axiomatic systems labeled S1 through S5. S4 and S5 became particularly influential and remain central to the field.
The semantic foundation of modern modal logic was established by Saul Kripke in the late 1950s and early 1960s. Kripke's possible worlds semantics provided a precise mathematical interpretation of modal formulas and enabled completeness proofs connecting axiomatic systems to classes of frames. This work transformed modal logic from a marginal philosophical curiosity into a central tool across philosophy, computer science, linguistics, and mathematics.
Other foundational contributions include Ruth Barcan Marcus's work on quantified modal logic and the Barcan formulas, Arthur Prior's creation of temporal logic, Georg Henrik von Wright's development of deontic logic, and David Lewis's modal realism. Contemporary work by Timothy Williamson, Kit Fine, Robert Stalnaker, and many others continues to advance the field.
Modal logic is essential for contemporary metaphysics (necessity, essence, possible worlds), epistemology (knowledge and belief), philosophy of language (rigid designation, conditionals), and ethics (deontic logic).
Temporal logics (LTL, CTL) are used to specify and verify hardware and software systems. Epistemic logics model distributed protocols and multi agent systems. Dynamic logic reasons about program behavior.
Natural language contains rich modal expressions. Formal semantics uses possible worlds to analyze modal auxiliaries, conditionals, and attitude verbs.
Epistemic logic models knowledge and belief in strategic situations. Common knowledge is a crucial concept in coordination games and economic theory.
Before we go any further, let's get comfortable with the language. Here are the terms and symbols that show up over and over.
Every symbol used anywhere on this site, with its name and how to say it aloud.
| □ | Box, necessity | "box" or "necessarily" |
| ◇ | Diamond, possibility | "diamond" or "possibly" |
| ¬ | Negation | "not" |
| ∧ | Conjunction | "and" |
| ∨ | Disjunction | "or" |
| → | Material implication | "implies" or "if...then" |
| ↔ | Biconditional | "if and only if" or "iff" |
| ∀ | Universal quantifier | "for all" or "every" |
| ∃ | Existential quantifier | "there exists" or "some" |
| ⊨ | Double turnstile | "models" or "entails" |
| ⊢ | Single turnstile | "proves" or "is derivable" |
| ∈ | Set membership | "is an element of" or "in" |
| ⊆ | Subset | "is a subset of" |
| ⟨W, R⟩ | Frame | "frame W, R" (angle brackets) |
| φ, ψ | Greek phi, psi (formula variables) | "fee" or "fye" / "sigh" or "see" |
| A, B, C | Propositional variables | "A" "B" "C" (as in the alphabet) |
| P, Q, R | Atomic propositions / predicates | "P" "Q" "R" |
| x, y, z | Individual variables | "x" "y" "z" |
| w, v, u | World variables | "w" "v" "u" (as in "world") |
| M | Kripke model | "M" (as in "model") |
| W | Set of possible worlds | "W" (as in "worlds") |
| R | Accessibility relation | "R" (as in "relation") |
| V | Valuation function | "V" (as in "valuation") |
| ⊂ | Proper subset / strict inclusion | "is strictly contained in" or "is a proper subset of" |
| ≡ | Logical equivalence | "is equivalent to" or "iff" |
| iff | If and only if (abbreviation) | "iff" (pronounced like "if" with an extra f) |
| K | Knowledge operator (epistemic) | "knows that" |
| B | Belief operator (doxastic) | "believes that" |
| C | Common knowledge | "it is common knowledge that" |
| D | Distributed knowledge | "it is distributed knowledge that" |
| F | Future possibility (temporal) | "it will be the case that" or "eventually" |
| G | Future necessity (temporal) | "it will always be the case that" or "globally" |
| P | Past possibility (temporal) | "it was the case that" or "once" |
| H | Past necessity (temporal) | "it has always been the case that" or "historically" |
| ○ | Next operator (temporal) | "next" |
| U | Until operator (temporal) | "until" |
| O | Obligation (deontic) | "it is obligatory that" or "ought" |
| P | Permission (deontic) | "it is permitted that" |
| F | Prohibition (deontic) | "it is forbidden that" |
| ! | Exponential (linear logic) | "bang" or "of course" |
| ? | Why not (linear logic) | "why not" |
| S, P, M | Syllogistic terms | "S" (subject), "P" (predicate), "M" (middle term) |
An agent is whoever (or whatever) is doing the knowing or believing. In everyday life, agents are people. You, me, your friend. In computer science, an agent might be a program, a process, or a robot. We label different agents with subscripts: Agent₁, Agent₂. So K₁(raining) means "Agent₁ knows it's raining."
A possible world is a complete way reality could have gone. The actual world (the one we're in) is just one among many. There are worlds where dinosaurs still roam, where you became a painter, or where the laws of physics are slightly different. A statement is necessary if it's true in every single possible world you can get to. It's possible if there's at least one world where it's true.
This is the connection between worlds, usually called R. Not every world is relevant to every statement. If you're thinking about what you know, the only worlds that matter are the ones consistent with your knowledge. If you're thinking about what's morally required, you only look at worlds where everyone follows the rules. R tells you which worlds you can "see" from where you're standing.
Box means necessity. But "necessary" how? Depends on context. Logical necessity: true in all logically possible worlds. Metaphysical necessity: true in all worlds with the same fundamental nature. Epistemic necessity: follows from what you know. Deontic necessity: what you're obligated to do. The symbol stays the same; the meaning shifts.
Diamond means possibility. And just like with box, the kind of possibility depends on context. Logical possibility (not self contradictory), metaphysical possibility (compatible with the nature of things), epistemic possibility (compatible with what you know), or deontic permission (you're allowed to do it).
C.I. Lewis's big idea. Ordinary "if A then B" is too weak. It's true whenever A is false, even if A and B have nothing to do with each other. Strict implication is stronger. A strictly implies B means that in every accessible world where A is true, B is also true. Written as □(A → B).
A formula is valid if it's true no matter what. More precisely, it's true at every world in every model built on a certain kind of frame. When something is valid, you can count on it. It's a logical truth within that system.
Soundness means: if you can prove it using the rules, it's genuinely valid. No false positives. Completeness means: if it's valid, you can prove it using the rules. No blind spots. Together they mean the rules perfectly capture the semantics.
Latin for "of the thing" versus "of what's said." De dicto: the necessity applies to the whole statement. "Necessarily, something is F." De re: the necessity attaches to the thing itself. "There is something that is necessarily F." This matters for questions about essence. What makes you fundamentally you.
A frame is the bare skeleton: just a set of worlds W and an accessibility relation R. ⟨W, R⟩. No truth values assigned yet. Just the structure. Frames are where properties like reflexivity and transitivity live.
This is what breathes life into a frame. The valuation function V tells you which atomic facts hold at which worlds. V(raining) = {w₁, w₃, w₇} means it's raining in worlds 1, 3, and 7, and not in the others.
A normal modal logic contains all propositional tautologies, contains the K axiom □(A→B) → (□A→□B), and is closed under modus ponens and necessitation. Most systems we talk about (K, T, S4, S5) are normal.
Common knowledge is what everyone knows, and everyone knows that everyone knows, and everyone knows that everyone knows that everyone knows... all the way up. It's what lets people coordinate without saying a word. Like knowing to drive on the right side of the road.
Distributed knowledge is what a group would know if they pooled everything they individually know. Even if no single person knows the whole picture, together they do.
A rigid designator is a name that points to the same individual in every possible world where that individual exists. "Socrates" picks out Socrates no matter what. Even in worlds where he never taught Plato. Definite descriptions like "the teacher of Plato" aren't rigid. In another world, someone else might have taught Plato.
The statement ◇∃x φ → ∃x ◇φ. In plain English: if it's possible that something satisfies φ, then there actually exists something that possibly satisfies φ. It has huge implications for whether things could have failed to exist.
The view that everything exists necessarily. You, me, your coffee mug. We all exist in every possible world. What changes is whether we're concrete (physically manifested) or merely abstract. Timothy Williamson is its most famous defender.
The more intuitive view: some things exist only contingently. You might never have been born. To hold this while keeping a strong modal logic like S5 requires rejecting constant domains or the Barcan formulas.
A syllogism is a form of logical argument developed by Aristotle that applies deductive reasoning to arrive at a conclusion based on two or more propositions that are asserted or assumed to be true. A classic example: "All men are mortal. Socrates is a man. Therefore, Socrates is mortal." Syllogistic logic was the dominant form of logic for over two thousand years.
Also called traditional logic or Aristotelian logic. Term logic analyzes propositions as consisting of a subject and a predicate combined by a copula. The four categorical propositions are: A (universal affirmative: All S are P), E (universal negative: No S are P), I (particular affirmative: Some S are P), and O (particular negative: Some S are not P).
A formula (often denoted by Greek letters like φ, ψ, or capital letters A, B) is any string of symbols that follows the grammatical rules of the logical language. A well formed formula (wff) is one that is syntactically correct. For example, □(A → B) is well formed, while □→A is not.
An atomic proposition (often P, Q, R) is the smallest unit of meaning in propositional logic. It cannot be broken down into simpler logical components. Examples: "It is raining," "Socrates is mortal." These are the basic building blocks that are combined using logical connectives.
A logical connective (also called a logical operator or logical constant) is a symbol used to combine or modify propositions. The standard connectives are ¬ (not), ∧ (and), ∨ (or), → (implies), and ↔ (if and only if). Modal operators □ and ◇ are also connectives.
Quantifiers specify how many individuals a predicate applies to. The universal quantifier ∀ means "for all" or "every." The existential quantifier ∃ means "there exists" or "some." Quantifiers bind variables and turn open formulas into propositions with truth values.
A predicate is a function that takes individuals and returns a proposition. For example, "Mortal(x)" means "x is mortal." Predicates can take one argument (unary, like "is mortal") or multiple arguments (binary, like "loves" in "Loves(x, y)").
Two formulas are logically equivalent (written A ≡ B or A ↔ B) if they have the same truth value in every possible situation. For example, □A ≡ ¬◇¬A. Logical equivalence means the formulas can be substituted for each other in any context without changing truth values.
The standard way to give modal logic a precise meaning is called Kripke semantics, after Saul Kripke. It's built on the idea of possible worlds connected by accessibility relations.
A Kripke frame is a pair ⟨W, R⟩. W is a set of worlds. R is the accessibility relation. Which worlds can "see" which other worlds. That's the skeleton.
A Kripke model adds a valuation function V, which tells you which atomic facts are true at which worlds. So a model is a triple ⟨W, R, V⟩. Now you can actually evaluate statements.
We write M, w ⊨ A to mean "in model M, at world w, A is true." The rules:
A formula is true in a model if it's true at every world in that model. It's valid on a frame if it's true in every model built on that frame. It's a logical truth of a system if it's valid on all frames for that system.
The accessibility relation R is where all the flexibility comes from. Change what R means, and you change what □ and ◇ mean.
| Alethic modality | □ = "necessarily", ◇ = "possibly" | R connects worlds that are possible relative to the current one. Often an equivalence relation (S5). |
| Epistemic modality | □ = "the agent knows that" | R connects worlds compatible with what the agent knows. S5 for knowledge, KD45 for belief. |
| Temporal modality | □ = "always", ◇ = "eventually" | R is the flow of time. One moment sees later moments. |
| Deontic modality | □ = "obligatory", ◇ = "permitted" | R connects worlds to deontically ideal worlds. Typically serial (KD). |
Normal modal logics all start from system K and then add extra axioms. An axiom is a formula you take as given. A basic rule.
| K | □(A → B) → (□A → □B) | If A necessarily implies B, and A is necessary, then B is necessary. Valid on all frames. |
| D | □A → ◇A | Serial: every world sees at least one world. "Ought implies can." |
| T | □A → A | Reflexivity: every world sees itself. Necessity implies actuality. Knowledge implies truth. |
| B | A → □◇A | Symmetry: if w sees v, then v sees w. Brouwer's axiom. |
| 4 | □A → □□A | Transitivity. Positive introspection: if you know, you know you know. |
| 5 | ◇A → □◇A | Euclidean. Negative introspection: if you don't know, you know you don't know. In alethic terms: if something is possibly true, then it is necessarily possible. |
| L | □(□A → A) → □A | Löb's axiom. Central to provability logic. |
| M | □◇A → ◇□A | McKinsey axiom. Not first order definable. |
If you can prove A from no assumptions, then you can prove □A. Logical truths are necessary truths.
| T axiom: □A → A | Reflexivity: ∀w (wRw) |
| B axiom: A → □◇A | Symmetry: ∀w∀v (wRv → vRw) |
| 4 axiom: □A → □□A | Transitivity: ∀w∀v∀u ((wRv ∧ vRu) → wRu) |
| 5 axiom: ◇A → □◇A | Euclidean: ∀w∀v∀u ((wRv ∧ wRu) → vRu) |
| D axiom: □A → ◇A | Serial: ∀w∃v (wRv) |
Sahlqvist's theorem guarantees that a huge class of modal formulas have this neat correspondence.
By combining the basic axioms, we get different systems. C.I. Lewis originally developed five systems, S1 through S5, with S4 and S5 becoming the most influential. Here are the major systems studied today.
| K | K only | All frames. Minimal normal modal logic. |
| KD | K + D | Serial frames. Standard deontic logic. |
| T | K + T | Reflexive frames. |
| B | K + T + B | Reflexive and symmetric frames. |
| S4 | K + T + 4 | Reflexive and transitive frames (preorders). One of Lewis's original systems. |
| S5 | K + T + 5 | Equivalence relations. All worlds connected. Standard for logical necessity. The strongest of Lewis's systems. |
| K4 | K + 4 | Transitive frames. |
| KD45 | K + D + 4 + 5 | Serial, transitive, Euclidean. Standard doxastic logic. |
| GL | K + L | Transitive, converse well founded. Provability logic. |
C.I. Lewis created systems S1 through S5 as axiomatizations of strict implication. S1 and S2 are non-normal modal logics (they lack the necessitation rule). S3 is also non-normal. S4 and S5 are normal modal logics and are the ones most widely used today. S4 adds the transitivity axiom (4) to T. S5 adds the Euclidean axiom (5) to T, which makes the accessibility relation an equivalence relation. In S5, every world can see every other world, so modal operators collapse: □□A is just □A, and ◇□A is just □A.
K ⊂ KD ⊂ T ⊂ S4 ⊂ S5
K ⊂ K4 ⊂ S4
T ⊂ B ⊂ S5
KD ⊂ KD45 ⊂ S5
S5 is the strongest of the standard normal modal logics.
Epistemic logic reads □ as "the agent knows that." Let Kφ mean "the agent knows φ."
Belief can be false, so T is dropped. KD45: Bφ → ¬B¬φ (consistency), Bφ → BBφ, ¬Bφ → B¬Bφ.
With multiple agents: K₁, K₂, etc. Common knowledge Cφ means everyone knows, everyone knows everyone knows, ad infinitum. Distributed knowledge Dφ is what the group would know if they pooled information.
Standard epistemic logic makes agents know all logical truths and consequences. Real people aren't like that. Solutions include awareness logic and impossible worlds.
Temporal logic interprets modalities as moving through time. Arthur Prior founded this field.
Used in computer science for program verification. Assumes discrete linear time.
Example: □(request → ◇grant). Whenever there's a request, eventually there's a grant.
Branching time with multiple possible futures. Path quantifiers: Aφ (on all paths), Eφ (on some path).
Deontic logic is about obligation, permission, and prohibition. Founded by von Wright.
SDL is the modal logic KD. The D axiom Oφ → Pφ captures "ought implies can."
Ross's Paradox: From "you ought to mail the letter" we get "you ought to mail the letter or burn it."
Chisholm's Paradox: Conditional obligations and contrary to duty scenarios cause contradictions.
Good Samaritan: "It ought to be that someone helps the victim" implies "it ought to be that there is a victim."
These motivate dyadic deontic logic: O(ψ / φ) meaning "given φ, it ought to be that ψ."
Adding ∀ (for all) and ∃ (there exists) to modal logic.
Constant domain: Same objects exist in every world. Simple but metaphysically bold.
Varying domain: Different worlds have different domains. More intuitive but messier.
BF: ◇∃x φ → ∃x ◇φ. If it's possible that something is φ, then there exists something that is possibly φ.
CBF: ∃x ◇φ → ◇∃x φ. If there's something that is possibly φ, then it's possible that something is φ.
Both are valid in constant domain models. In S5 with constant domains, they're theorems.
Necessitism (Williamson): Everything exists necessarily. What varies is concreteness.
Contingentism: Some things exist only contingently. Requires rejecting constant domains or the Barcan formulas.
De dicto: □∃x Fx. "Necessarily, something is F."
De re: ∃x □Fx. "There is something that is necessarily F." (Essential properties.)
Modal logic connects deeply to big philosophical questions.
Plantinga's modal version uses S5. If it's possible that a maximally great being exists (one that has all perfections necessarily), then in S5 it's necessary that one exists. And therefore one actually exists. Valid in S5. The debate is over the possibility premise.
David Lewis: possible worlds are concrete realities, just as real as ours, spatiotemporally disconnected. "Possibly P" means "P is true in some concrete world."
Most philosophers are actualists. Only the actual world exists. Possible worlds are abstract representations. Maximal consistent sets of propositions.
Kripke: proper names are rigid designators. They point to the same object in every world. This led to the necessary a posteriori. "Water is H₂O" is necessarily true but known empirically. Shattered the old equation of necessity with analyticity and apriority.
Primary intension (epistemic possibility): consider worlds as actual. Secondary intension (metaphysical necessity): hold reference fixed, consider worlds as counterfactual. Untangles conceivability from genuine possibility.
Modal logic is just one branch of a much larger logical landscape. Here are other important systems of logic that have shaped human reasoning across centuries.
Syllogistic logic, developed by Aristotle in the 4th century BCE, was the dominant form of logic in the Western world for over two thousand years. A syllogism is a form of deductive reasoning consisting of a major premise, a minor premise, and a conclusion. Each premise is a categorical proposition taking one of four forms:
A classic syllogism: "All men are mortal. Socrates is a man. Therefore, Socrates is mortal." This is valid because the middle term ("man" or "men") connects the major and minor premises. Aristotle identified 24 valid syllogistic forms out of 256 possible combinations. The square of opposition illustrates the logical relationships between the four categorical propositions: contradictories (A and O, E and I), contraries (A and E), subcontraries (I and O), and subalternation (A implies I, E implies O).
Propositional logic analyzes logical relationships at the level of whole propositions rather than terms. It uses connectives like ¬ (not), ∧ (and), ∨ (or), → (if...then), and ↔ (if and only if). The Stoic philosophers developed an early form of propositional logic, but modern propositional logic was formalized in the 19th and early 20th centuries by George Boole, Gottlob Frege, and Bertrand Russell. Truth tables provide a complete decision procedure for propositional logic. A formula is a tautology if it is true under all possible truth value assignments.
Predicate logic extends propositional logic by analyzing the internal structure of propositions. It introduces quantifiers (∀ for "all" and ∃ for "some"), variables, predicates, and constants. This allows us to express statements like "All humans are mortal" as ∀x (Human(x) → Mortal(x)). Frege's Begriffsschrift (1879) introduced the first complete system of predicate logic. Predicate logic is the foundation of modern mathematics and much of contemporary analytic philosophy.
Developed by L.E.J. Brouwer and formalized by Arend Heyting, intuitionistic logic rejects the law of excluded middle (A ∨ ¬A) as a universal logical principle. In intuitionistic logic, a statement is true only if there is a constructive proof of it. Double negation elimination (¬¬A → A) is not valid. Intuitionistic logic is closely connected to constructive mathematics and the Curry Howard correspondence, which identifies proofs with programs and propositions with types.
Relevance logic (also called relevant logic) addresses the paradoxes of material implication by requiring that the premises of a valid argument be relevant to the conclusion. In classical logic, a false statement implies anything, and a true statement is implied by anything. Relevance logic introduces a relevant conditional → where A → B is true only if A is actually used in deriving B. Systems include R (the standard relevance logic), E (entailment), and NR.
Paraconsistent logic rejects the principle of explosion (A ∧ ¬A → B), which says that from a contradiction anything follows. In paraconsistent logics, contradictions do not trivialize the system. This allows for reasoning about inconsistent but non trivial theories, such as early set theory before axiomatization, or databases with conflicting information. Key systems include LP (Logic of Paradox) and da Costa's C systems.
Fuzzy logic, introduced by Lotfi Zadeh in 1965, allows for degrees of truth rather than strict true false bivalence. Truth values range continuously from 0 (completely false) to 1 (completely true). Fuzzy logic is used extensively in control systems, artificial intelligence, and applications where precise thresholds are unnatural.
Many valued logics extend beyond the two truth values of classical logic. Three valued logics (such as Kleene's and Lukasiewicz's) add a third value like "unknown" or "indeterminate." More generally, n valued logics and infinite valued logics are possible. These systems are useful for modeling vagueness, partial information, and the semantics of programming languages.
Linear logic, developed by Jean Yves Girard in 1987, treats logical assumptions as resources that are consumed when used. This makes it ideal for reasoning about resource sensitive processes, state changes, and concurrent computation. Linear logic introduces modalities (! and ?) to recover classical reasoning when needed. It has deep connections to category theory and the semantics of programming languages.
Substructural logics restrict or eliminate the structural rules of classical logic: weakening (adding premises), contraction (duplicating premises), and exchange (reordering premises). Relevance logic restricts weakening (premises must be used). Linear logic restricts both weakening and contraction. Lambek calculus, used in linguistics, restricts all three structural rules. These logics provide fine grained control over how assumptions can be used in derivations.
| K | Complete for all frames. |
| T | Complete for reflexive frames. |
| S4 | Complete for reflexive, transitive frames. |
| S5 | Complete for equivalence relations. |
| KD45 | Complete for serial, transitive, Euclidean frames. |
| GL | Complete for transitive, converse well founded frames. |