Extending propositional and predicate logic with modal operators -- necessity and possibility, and their relatives (obligation, knowledge, belief, time). Covers Kripke possible-worlds semantics, accessibility relations, the main modal systems (K, T, S4, S5), translation from natural language, and applications in epistemic, deontic, and temporal reasoning. Use when ordinary logic is insufficient to capture distinctions like "must" vs "might," "knows" vs "believes," "always" vs "sometimes."
Install with Codex or Claude Copy this prompt, paste it into Codex, Claude, or another assistant, and let it review the skill page and install it for you.
A direct command skips the review prompt. Inspect the source before running it.
Extending propositional and predicate logic with modal operators -- necessity and possibility, and their relatives (obligation, knowledge, belief, time). Covers Kripke possible-worlds semantics, accessibility relations, the main modal systems (K, T, S4, S5), translation from natural language, and applications in epistemic, deontic, and temporal reasoning. Use when ordinary logic is insufficient to capture distinctions like "must" vs "might," "knows" vs "believes," "always" vs "sometimes."
type
skill
category
logic
status
stable
origin
tibsfox
modified
false
first_seen
"2026-04-12T00:00:00.000Z"
first_path
examples/skills/logic/modal-logic/SKILL.md
superseded_by
null
Modal Logic
Modal logic extends standard logic with operators for modes of truth -- most centrally necessity (□, "box") and possibility (◇, "diamond"). "It is possible that it will rain" is not the same claim as "it will rain," and ordinary propositional logic cannot distinguish them. Modal logic can. The framework also generalizes: the same machinery handles obligation and permission (deontic logic), knowledge and belief (epistemic logic), past and future (temporal logic), and provability (provability logic). The common semantic foundation is Saul Kripke's possible-worlds model. This skill covers the syntax, semantics, proof theory, and applications of modal logic at the level of an upper-undergraduate or early-graduate logic course.
◇φ ≡ ¬□¬φ -- "possibly φ" means "not necessarily not φ"
□φ ≡ ¬◇¬φ -- "necessarily φ" means "not possibly not φ"
These duality relations are the modal counterparts of the quantifier dualities in predicate logic, and in Kripke semantics they will turn out to be exactly that.
Possible Worlds: Kripke Semantics
Saul Kripke's 1959 paper "A Completeness Theorem in Modal Logic" gave the semantic foundation that made modal logic rigorous. The idea:
A Kripke frame is a pair ⟨W, R⟩:
W is a nonempty set of possible worlds
R ⊆ W × W is an accessibility relation between worlds
A Kripke model adds a valuation V that assigns a truth value to each atomic proposition at each world.
Truth at a world w in a model:
Atomic p is true at w iff V(w, p) = T
¬φ is true at w iff φ is not true at w
φ ∧ ψ (and other connectives) work as in propositional logic, evaluated locally at w
□φ is true at w iff φ is true at every world v such that wRv
◇φ is true at w iff φ is true at some world v such that wRv
So □ quantifies universally and ◇ quantifies existentially over accessible worlds.
The intuition. A "possible world" is a complete alternative way things might be. The actual world is one such alternative. The accessibility relation encodes which alternatives are "live" from a given standpoint. Different modal notions (necessity, obligation, knowledge, time) correspond to different accessibility relations.
The Main Modal Systems
Different modal logics result from different constraints on the accessibility relation R. Each extra constraint validates additional axioms.
System K
The minimal normal modal logic. Axioms:
All propositional tautologies
K axiom: □(φ → ψ) → (□φ → □ψ) (necessitation distributes over implication)
Necessitation rule: from ⊢ φ, infer ⊢ □φ
K imposes no constraints on R. It is sound and complete for the class of all Kripke frames.
System T (Reflexivity)
Add T axiom: □φ → φ. "Whatever is necessary is actually true."
Valid iff R is reflexive: every world accesses itself.
System S4 (Reflexive + Transitive)
T plus 4 axiom: □φ → □□φ. "What is necessary is necessarily necessary."
Valid iff R is reflexive and transitive: if wRv and vRu, then wRu.
System S5 (Equivalence Relation)
S4 plus 5 axiom: ◇φ → □◇φ. "What is possible is necessarily possible."
Valid iff R is an equivalence relation: reflexive, symmetric, and transitive.
S5 is the strongest commonly studied modal system. In S5, the accessibility structure collapses -- every world accesses every other world in its equivalence class. This matches our intuition about logical (or metaphysical) necessity: something is necessary if it holds in every possible world, period, without the filtering that weaker accessibility relations provide.
Translation from Natural Language
Translating English modal sentences requires care.
Necessity and possibility
"It is necessary that it is raining" → □R.
"It is possible that it is raining" → ◇R.
Ambiguous scope
"A bachelor is necessarily unmarried." Two readings:
De dicto (about the sentence): □∀x (Bachelor(x) → Unmarried(x)) -- "necessarily, all bachelors are unmarried"
De re (about the thing): ∀x (Bachelor(x) → □Unmarried(x)) -- "for every bachelor, he is necessarily unmarried"
These are not equivalent. De dicto says the sentence is necessarily true; de re says each bachelor has a necessary property. The de re reading is much stronger and more contentious.
"Must" is ambiguous
"It must be raining" can be epistemic (I conclude from the wet ground) or deontic (it is obligatory that it rain -- strange in English but possible in other contexts). Modal logics distinguish these with different operators.
Epistemic Logic
In epistemic logic, the modal operator is interpreted as knowledge:
Kᵢφ -- "Agent i knows that φ"
The accessibility relation connects worlds that are epistemically indistinguishable for agent i. If w and v are indistinguishable to agent i from w's standpoint, then agent i cannot rule out v as the actual world, so Kᵢφ requires φ to hold in both.
Standard axioms
K: Kᵢ(φ → ψ) → (Kᵢφ → Kᵢψ). Logical omniscience: agents know all logical consequences of what they know. (This is an idealization.)
4: Kᵢφ → KᵢKᵢφ. Positive introspection: if you know something, you know that you know it.
5: ¬Kᵢφ → Kᵢ¬Kᵢφ. Negative introspection: if you don't know something, you know that you don't.
Systems vary on which introspection axioms to accept. Most uncontroversial is T.
Distinguishing knowledge and belief
Belief is sometimes formalized with a separate operator Bᵢφ that satisfies K and 4 but not T -- you can believe falsehoods.
Deontic Logic
In deontic logic, the modal operator represents obligation:
Oφ -- "It ought to be the case that φ"
Pφ -- "It is permitted that φ"
Fφ -- "It is forbidden that φ" = O¬φ
Standard axioms
K: O(φ → ψ) → (Oφ → Oψ)
D: Oφ → ¬O¬φ. "Ought implies consistency" -- you cannot be obligated to do contradictory things. (Though real moral systems sometimes produce genuine dilemmas, which is one reason deontic logic is philosophically contested.)
The T axiom (Oφ → φ) is NOT adopted in deontic logic -- what ought to be is not always the case.
Temporal Logic
Temporal logic replaces necessity and possibility with operators about time:
Gφ -- "Always in the future, φ"
Fφ -- "Sometime in the future, φ"
Hφ -- "Always in the past, φ"
Pφ -- "Sometime in the past, φ"
The accessibility relation is an earlier-later ordering. Different temporal logics model linear vs branching time, discrete vs continuous, etc. Temporal logic is critical in verification of concurrent systems (LTL, CTL, CTL*).
Philosophical Issues
Quine's skepticism
W. V. O. Quine was a famous skeptic of modal logic, especially quantified modal logic (QML). His central worry was about de re modality: quantifying into modal contexts raises questions about whether modal properties attach to objects themselves or only to descriptions. "The number of planets is necessarily greater than 7" -- what is the "number of planets" as a referent, independent of the actual astronomical fact?
This debate drove a great deal of 20th-century philosophical logic and is why the logic department's Quine agent carries a skeptical stance as a matter of role.
Kripke's response
Kripke argued that de re modality was coherent and that rigid designators (terms that refer to the same object in every possible world) resolved Quine's puzzles. Kripke's Naming and Necessity (1980) is the landmark text.
The necessity of origin
Kripke also argued for striking metaphysical claims like "a human being could not have had different parents" (necessity of origin). These claims are modal metaphysics, not modal logic per se, but they motivate much of the field.
Worked Example: A Modal Proof
Claim: In system K, the formula □φ ∧ □ψ → □(φ ∧ ψ) is valid.
Proof sketch: Suppose □φ and □ψ are true at world w. By the semantics, φ is true at every world v with wRv, and ψ is true at every world v with wRv. Therefore at every such v, both φ and ψ are true, so φ ∧ ψ is true at v. Since this holds for every accessible v, □(φ ∧ ψ) is true at w.
This is a typical modal-semantic argument: chase the semantics across worlds.
When NOT to Use This Skill
Arguments with no modal content. Use propositional-logic or predicate-logic.
Arguments that are actually about informal persuasion. Use informal-fallacies or critical-argumentation.
Mathematical proofs that happen to mention "necessarily." Use mathematical-proof-logic -- "necessarily" in math usually means "in every model," which is first-order.
Decision Guidance
When you encounter an argument involving modality:
Identify the modal operators. Is the key word "must," "could," "ought," "knows," "sometime"?
Choose the system. Alethic (necessity/possibility)? Epistemic? Deontic? Temporal?
Pick the right strength. K, T, S4, or S5? The choice depends on what introspection or reflexivity properties are intended.
Check de dicto vs de re. Where is the quantifier with respect to the modal operator?
Evaluate in a Kripke model. If you want to show validity, prove it for arbitrary accessibility relations in the system. If you want to show invalidity, construct a countermodel.
Cross-References
frege agent: Invention of quantifiers, foundational role
quine agent: Skeptical framing, critique of QML
tarski agent: Semantic discipline, model theory
propositional-logic skill: The base system modal logic extends
predicate-logic skill: Combined with modal to give quantified modal logic
References
Hughes, G. E., & Cresswell, M. J. (1996). A New Introduction to Modal Logic. Routledge.
Kripke, S. (1959). "A Completeness Theorem in Modal Logic." Journal of Symbolic Logic 24(1), 1-14.
Kripke, S. (1980). Naming and Necessity. Harvard University Press.
Blackburn, P., de Rijke, M., & Venema, Y. (2001). Modal Logic. Cambridge University Press.
Fagin, R., Halpern, J. Y., Moses, Y., & Vardi, M. Y. (2003). Reasoning About Knowledge. MIT Press.
Quine, W. V. O. (1953). "Reference and Modality," in From a Logical Point of View. Harvard University Press.
