Modal logic

Fact-checked by Grok 2 weeks ago

Modal logic is a branch of formal logic that extends classical propositional and predicate logics by incorporating modal operators to express concepts of necessity, possibility, obligation, knowledge, and related modalities.^[1] These operators, typically denoted by □ (necessity or "must") and ◇ (possibility or "may"), allow for the analysis of statements whose truth depends on circumstances beyond mere factual assertion, such as "it is necessarily true that P" or "it is possible that P."^[2] Originating in philosophical inquiries into alethic modalities, modal logic has evolved into a foundational tool in philosophy, mathematics, computer science, and linguistics for modeling intensional reasoning.^[3] The roots of modal logic trace back to Aristotle's discussions of necessity and possibility in works like De Interpretatione, where he explored how future contingents relate to modal notions, though his framework contained inconsistencies that limited its formal development.^[2] A modern revival began in the early 20th century with Clarence Irving Lewis's 1910–1932 axiomatic systems (S1 through S5), which addressed limitations in material implication by introducing "strict implication" to capture necessary connections between propositions.^[4] Saul Kripke's seminal 1959–1965 contributions revolutionized the field by providing relational semantics using possible worlds and accessibility relations, enabling rigorous model-theoretic analysis and proving completeness for key systems.^[3] At its core, propositional modal logic builds on classical syntax with propositional variables, connectives (¬, ∧, ∨, →), and modal operators, forming well-formed formulas like □(P → Q).^[3] Semantically, Kripke models consist of a set of worlds W, a binary accessibility relation R ⊆ W × W, and a valuation V assigning truth values to propositions at each world; a formula □φ is true at world w if φ holds at every world accessible from w via R.^[2] Different modal systems arise from varying axioms and corresponding frame conditions on R: for instance, system K (the minimal normal modal logic) includes the distribution axiom □(φ → ψ) → (□φ → □ψ) with no restrictions on R; T adds reflexivity (□φ → φ); S4 adds transitivity (□φ → □□φ); and S5 assumes equivalence (reflexivity, symmetry, transitivity).^[1] These systems are sound and complete with respect to their classes of frames, ensuring that theorems capture semantic validities.^[3] Beyond alethic modalities, modal logic encompasses variants like epistemic logic (for knowledge and belief), deontic logic (for obligation and permission), temporal logic (for time), and dynamic logic (for actions and programs), with applications in verifying software, reasoning about multi-agent systems, and formalizing philosophical arguments.^[4] Algebraic semantics, developed by McKinsey, Tarski, and Jónsson in the 1940s–1950s, interprets modalities as operations on Boolean algebras, while later extensions like the μ-calculus (Kozen, 1983) incorporate fixed points for recursive definitions in computation.^[4] The field's mathematical depth is evident in results like the finite model property for many systems (Segerberg, 1968) and decidability for expressive fragments like CTL* (Emerson and Halpern, 1986).^[4]

Syntax

Propositional Foundation

In classical propositional logic, the foundational elements consist of propositional variables, denoted by symbols such as p, q, r, s, which stand for atomic propositions that are either true or false but lack internal structure.^[5] These variables represent the simplest well-formed formulas (wffs), serving as the indivisible units from which all compound expressions in the language are constructed.^[6] The syntax of propositional logic employs a set of binary and unary connectives to combine these atomic propositions into more intricate formulas. Negation (\neg) is a unary connective that forms the denial of a given proposition, such as \neg p, meaning "not p".^[7] Conjunction (\wedge) and disjunction (\vee) are binary connectives that link two propositions to express "and" and "or," respectively, as in p \wedge q or p \vee q.^[8] Implication (\rightarrow), another binary connective, represents material implication, forming expressions like p \rightarrow q, which is true unless p is true and q is false.^[9] These connectives enable the systematic building of compound propositions that capture relational logical structures. Well-formed formulas are generated through a recursive definition to ensure syntactic validity and clarity. Every propositional variable is a wff; if \phi is a wff, then \neg \phi is a wff; and if both \phi and \psi are wffs, then (\phi \wedge \psi), (\phi \vee \psi), and (\phi \rightarrow \psi) are wffs.^[10] Parentheses are mandatory around compound subformulas to resolve precedence and avoid ambiguity, preventing misinterpretation of operator associations in nested expressions.^[7] An illustrative example of a valid propositional formula that exemplifies logical consistency is the tautology p \rightarrow p, which holds true for any assignment of truth values to p since the antecedent and consequent are identical. This propositional framework provides the syntactic base upon which modal logic introduces additional operators to express notions of necessity and possibility.^[5] Modal logic extends the syntax of propositional logic by incorporating unary modal operators that express notions of necessity and possibility. The primary operators are the necessity operator, denoted \Box, and the possibility operator, denoted \Diamond, where \Diamond \phi is defined equivalently as \neg \Box \neg \phi for any formula \phi.^[11] The set of modal formulas consists of all propositional formulas and is closed under the standard propositional connectives such as negation (\neg), conjunction (\land), disjunction (\lor), and implication (\to), as well as under the application of \Box and \Diamond to any modal formula.^[11] Modal operators can be nested to arbitrary depths, allowing for complex expressions such as \Box \Diamond p or \Diamond \Box \Diamond q, where p and q are propositional variables. In systems with multiple modalities—such as those distinguishing epistemic, deontic, or temporal notions—operators are often indexed, for example \Box_E \phi to denote epistemic necessity applied to \phi.^[11] A simple example of a modal formula is \Box (p \to p), which can be read as "it is necessary that p implies p." This illustrates how modal operators combine with propositional connectives to form more expressive statements.^[11]

Semantics

Kripke Semantics

Kripke semantics, introduced by Saul Kripke, offers a relational framework for interpreting modal logic formulas using structures known as possible worlds.^[12] This approach models necessity and possibility through accessibility relations between worlds, providing a foundation for evaluating modal operators like \Box (necessity) and \Diamond (possibility).^[12] A Kripke frame consists of a non-empty set W of possible worlds and a binary accessibility relation R \subseteq W \times W, which determines how worlds are connected to one another.^[12] A Kripke model extends a frame by adding a valuation function V: W \times \mathrm{Prop} \to \{\top, \bot\}, where \mathrm{Prop} is the set of propositional variables, assigning truth values to atomic propositions at each world.^[12] The truth of a modal formula \phi at a world w in a model \mathcal{M} = (W, R, V), denoted \mathcal{M}, w \models \phi, is defined recursively. For a propositional variable p, \mathcal{M}, w \models p if and only if V(w, p) = \top.^[12] For negation, \mathcal{M}, w \models \neg \phi if and only if \mathcal{M}, w \not\models \phi. For conjunction, \mathcal{M}, w \models \phi \land \psi if and only if \mathcal{M}, w \models \phi and \mathcal{M}, w \models \psi. The modal operators are interpreted via the accessibility relation: \mathcal{M}, w \models \Box \phi if and only if for all v \in W such that w R v, \mathcal{M}, v \models \phi; and \mathcal{M}, w \models \Diamond \phi if and only if there exists v \in W such that w R v and \mathcal{M}, v \models \phi.^[12] To illustrate, consider a simple model with worlds w_1 and w_2, where R = \{(w_1, w_2)\} (unidirectional accessibility from w_1 to w_2) and V(w_1, p) = \bot, V(w_2, p) = \top. At w_1, \Box p is false because w_1 R w_2 but p is false at w_2; at w_2, \Box p is vacuously true since no worlds are accessible from w_2.^[12] A modal formula \phi is valid if it is true at every world in every model; conversely, \phi is satisfiable if there exists a model and a world where it is true.^[12]

Alternative Semantics

Neighborhood semantics provides an alternative to relational Kripke frames by interpreting modal operators using a collection of subsets of the set of worlds, known as neighborhoods, assigned to each world. In this framework, a neighborhood model consists of a set W of worlds and a neighborhood function N: W \to \mathcal{P}(\mathcal{P}(W)), where for each world w \in W, N(w) is the set of neighborhoods at w.^[13] The truth condition for the necessity operator \Box is defined such that M, w \models \Box \phi if and only if the proposition set [\phi]^M = \{v \in W \mid M, v \models \phi\} belongs to N(w).^[13] This semantics allows for greater flexibility in modeling modalities that do not satisfy the standard normality conditions of Kripke semantics, such as closure under arbitrary intersections.^[13] Neighborhood frames often incorporate additional properties to capture specific logical behaviors. Monotonicity, for instance, requires that if X \in N(w) and X \subseteq Y \subseteq W, then Y \in N(w), which validates the distribution axiom \Box(\phi \to \psi) \to (\Box \phi \to \Box \psi).^[13] Other closure properties include closure under finite intersections, which ensures \Box(\phi \wedge \psi) \to \Box \phi \wedge \Box \psi, or under complements and unions for more complex logics.^[13] These properties enable the semantics to model non-normal modal logics, where the necessity operator may not behave as a normal modal operator in the Kripke sense.^[14] Topological semantics interprets modal logic over a topological space (W, \tau), where \tau \subseteq \mathcal{P}(W) is the collection of open sets, and a valuation assigns propositions to subsets of W. The necessity operator \Box is defined such that M, w \models \Box \phi if and only if \phi holds at every world in some open neighborhood of w, or equivalently, [\Box \phi]^M = \mathrm{int}([\phi]^M), where \mathrm{int} denotes the interior operator.^[15] The dual possibility operator \Diamond corresponds to the closure operator \mathrm{cl}, with \Diamond \phi true at w if w belongs to the closure of [\phi]^M, meaning that every open neighborhood of w intersects [\phi]^M.^[15] This setup naturally captures reflexive and transitive modalities, as the interior operator is always reflexive and monotonic, and in certain spaces, transitive.^[15] Neighborhood and topological semantics differ from Kripke semantics in their treatment of accessibility, replacing binary relations with set-theoretic structures, which allows validation of formulas invalid in relational models, such as those in monotonic but non-normal logics.^[13] They coincide with Kripke semantics for normal modal logics like S4, where neighborhood frames can be restricted to principal filters corresponding to accessible worlds, but diverge for non-normal logics, where Kripke frames fail to model the full range of behaviors.^[13] For instance, in S4, topological models validate the same theorems as transitive and reflexive Kripke frames.^[15] A brief historical note highlights that neighborhood semantics, including its topological variant for S4, was developed independently by Dana Scott and Richard Montague in 1970, extending earlier topological ideas from McKinsey and Tarski's work on intuitionistic logic.^[13]

Proof Systems

Axiomatic Systems

Axiomatic systems in modal logic provide a deductive framework for deriving valid modal formulas, extending the Hilbert-style approach used in classical propositional logic. These systems specify a set of axiom schemata and inference rules that allow the construction of proofs as finite sequences of formulas. Modal formulas, constructed from propositional variables, logical connectives, and modal operators, serve as the objects of these derivations.^[16] The foundational axiomatic system is K, which includes all instances of propositional tautologies as axioms, along with the modal axiom schema K: \square(\phi \to \psi) \to (\square\phi \to \square\psi). The inference rules are modus ponens—from \phi and \phi \to \psi, infer \psi—and necessitation—from \phi, infer \square\phi. A formula \theta is a theorem of K, denoted \vdash_K \theta, if there exists a finite sequence of formulas ending in \theta such that each formula in the sequence is either a propositional tautology, an instance of axiom K, or obtained from earlier formulas in the sequence via modus ponens or necessitation. System K is consistent, meaning no contradiction is derivable within it.^[16]^[17] Extensions of K are formed by adding further axiom schemata to capture specific structural properties, resulting in normal modal logics. The T axiom \square\phi \to \phi yields the system KT. The 4 axiom \square\phi \to \square\square\phi produces K4. The 5 axiom \diamond\phi \to \square\diamond\phi, where \diamond\phi \equiv \neg\square\neg\phi, gives K5. The B axiom \phi \to \square\diamond\phi leads to KB. Combinations of these, such as KT4 (S4) or KT4B (S5), define richer systems while preserving the rules of modus ponens and necessitation.^[16] A representative theorem of system K is \square(p \wedge q) \leftrightarrow (\square p \wedge \square q). The direction \square(p \wedge q) \to (\square p \wedge \square q) follows from the fact that (p \wedge q) \to p is a tautology; by necessitation, \square((p \wedge q) \to p); applying axiom K yields \square((p \wedge q) \to p) \to (\square(p \wedge q) \to \square p); and modus ponens gives \square(p \wedge q) \to \square p. A symmetric argument yields \square(p \wedge q) \to \square q, and propositional logic combines these to \square(p \wedge q) \to (\square p \wedge \square q). For the converse, p \to (q \to (p \wedge q)) is a tautology, so by necessitation, \square p \to \square(q \to (p \wedge q)); axiom K gives \square p \to (\square q \to \square(p \wedge q)); the tautology (\square p \to (\square q \to \square(p \wedge q))) \to ((\square p \wedge \square q) \to \square(p \wedge q)) then allows modus ponens twice to derive (\square p \wedge \square q) \to \square(p \wedge q). Thus, the biconditional holds.^[16]

Tableaux and Automated Methods

Semantic tableaux provide an analytic proof method for modal logic, extending the propositional case by incorporating Kripke-style semantics through labeled nodes that represent worlds and accessibility relations. In this system, tableau branches consist of signed formulas prefixed by world labels (e.g., w : T \phi indicating that formula \phi is true at world w), along with relation assertions like w R v denoting accessibility between worlds w and v. The method proceeds by refutation: to prove a formula \phi valid, construct a tableau for w_0 : F \phi (falsity at an initial world w_0) and show all branches close, where closure occurs if a branch contains both w : T \psi and w : F \psi for some atomic \psi, or contradictory relations. This approach ensures soundness and completeness relative to Kripke models for the basic modal logic K.^[19] The propositional rules mirror classical tableaux: non-branching rules for conjunctions and implications (e.g., from w : T (\alpha \land \beta), add w : T \alpha and w : T \beta), and branching for disjunctions and negated conjunctions (e.g., from w : F (\alpha \lor \beta), branch to w : F \alpha and w : F \beta). Modal rules handle necessity (\square) and possibility (\diamond) via accessibility: for the existential modality, the rule for w : T \diamond \alpha non-deterministically adds a new world v, the relation w R v, and v : T \alpha (introducing a successor where \alpha holds). For the universal modality, the rule for w : F \square \alpha adds a new world v, w R v, and v : F \alpha (witnessing a successor where \alpha fails). These rules create labeled structures that, if open, yield a countermodel; closure across all branches proves unsatisfiability.^[19]^[20] A representative example illustrates closure for an unsatisfiable formula, such as \diamond p \land \neg \diamond p, which asserts the existence and non-existence of an accessible world satisfying p. Begin the tableau with initial world w_0 : T (\diamond p \land \neg \diamond p), which branches to w_0 : T \diamond p and w_0 : T \neg \diamond p (equivalent to w_0 : T \square \neg p). Applying the rule for w_0 : T \diamond p adds a new world v, the relation w_0 R v, and v : T p. The rule for w_0 : T \square \neg p requires T \neg p (i.e., F p) at every accessible world from w_0, including the newly introduced v, so add v : F p. This creates a contradiction at v with v : T p and v : F p, closing the branch. Thus, all paths close, demonstrating the method's ability to detect modal inconsistencies through relational labeling.^[19]^[21] Automated methods for modal logic leverage these tableaux for decision procedures, often translating formulas to satisfiability problems in propositional logic (SAT) or first-order logic (FOL) to exploit existing solvers. One approach encodes modal formulas into SAT by unfolding the Kripke structure up to a bounded depth, representing worlds as propositional variables layered by modality depth, with clauses enforcing accessibility and truth propagation; this is effective for fragments with bounded tree-width models. Alternatively, translation to FOL via standard embeddings (e.g., using predicates for propositions and a binary relation for accessibility) allows first-order theorem provers to handle validity, preserving the monadic fragment's properties. The finite model property of decidable modal fragments—where every satisfiable formula has a finite model of size exponential in the formula length—ensures termination and decidability for these translations, as only finitely many models need checking up to equivalence.^[22]^[23] The computational complexity of satisfiability in multi-modal logics, including the basic logic K with multiple accessibility relations, is PSPACE-complete, reflecting the space needed to explore exponential-depth models nondeterministically while reusing storage via Savitch's theorem. This holds even for transitive or reflexive extensions like S4, though S5 drops to NP-complete due to equivalence relations allowing polynomial witnesses. These results underscore the practical challenges and theoretical limits for automated verification in modal systems.

The Logic K

The logic K, often denoted \mathbf{K}, is the minimal normal modal logic, serving as the basic system upon which stronger modal logics are built. It extends the theorems of classical propositional logic by incorporating the unary modal operator \square for necessity, along with its dual possibility operator \Diamond defined by the equivalence \Diamond \phi \equiv \neg \square \neg \phi. The distinctive axiom of K is the distribution principle:

\square (\phi \to \psi) \to (\square \phi \to \square \psi)

This axiom captures the idea that if something is necessarily true that \phi implies \psi, then necessity distributes over that implication. The system is closed under the standard rules of modus ponens and necessitation: if \vdash \phi, then \vdash \square \phi.^[11]^[3] A key property of K is that it imposes no structural constraints on the accessibility relation R in its Kripke semantics, allowing R to be any arbitrary binary relation between possible worlds. This generality contrasts with extensions of K that add axioms corresponding to properties like reflexivity or transitivity of R. Semantically, a formula \square \phi holds at a world w in a Kripke model \langle W, R, V \rangle if \phi holds at every world w' such that w R w', with no further restrictions on R. The duality between \square and \Diamond is a fundamental theorem derivable in K, enabling equivalent formulations of modal claims in terms of possibility.^[11]^[3] K is sound and complete with respect to the class of all Kripke frames: a formula is a theorem of K if and only if it is valid in every such frame. This correspondence ensures that the deductive power of K precisely captures the semantic notion of necessity and possibility across arbitrary relational structures. Additional theorems in K include distribution variants, such as \square (\phi \wedge \psi) \to (\square \phi \wedge \square \psi), which follow from the core axiom and propositional reasoning.^[11]^[3]

Common Axiomatic Extensions

Common axiomatic extensions of the basic modal logic K arise by incorporating additional axioms that enforce specific structural properties on the accessibility relation R in Kripke frames, thereby defining logics sound and complete with respect to corresponding classes of frames.^[24] These extensions, such as T, S4, B, and S5, are normal modal logics that extend K while preserving its deductive power, and they play a central role in applications requiring modalities like necessity and possibility under relational constraints.^[24] The logic T, also known as KT, extends K with the axiom T: \square \phi \to \phi. This axiom corresponds to reflexive frames, where for every world w, wRw holds.^[24] In such logics, the necessity operator exhibits idempotence in the sense that \square \square \phi \to \square \phi is provable, reflecting the stability of necessary truths across accessible worlds.^[24] T serves as a foundation for many applied modal systems, capturing basic notions of actuality alongside possibility. For transitivity, the axiom 4: \square \phi \to \square \square \phi is added to K (or T) to yield S4, which is sound and complete over transitive and reflexive frames (preorders).^[24] In S4, the accessibility relation ensures that necessity propagates indefinitely, making it suitable for cumulative modalities like knowledge or obligation.^[24] A further extension, S4.3, incorporates the .3 axiom: \square (\square \phi \to \psi) \lor \square (\square \psi \to \phi), corresponding to frames that are linear orders—reflexive, transitive, and connected, meaning that for any worlds w, v, x if wRv and wRx then either vRx or xRv.^[25] This logic captures ordered structures without branching, as in directed timelines or linear reasoning chains.^[25] Symmetry is addressed by the B axiom: \phi \to \square \diamond \phi, added to T to form B (or KT B), which validates over reflexive and symmetric frames.^[24] Combining transitivity with symmetry yields S5, equivalent to K + T + 4 + B or K + 5 (where 5 is \diamond \phi \to \square \diamond \phi), complete for equivalence relations (reflexive, transitive, symmetric).^[24] S5's equivalence classes model partitioned domains, such as possible worlds grouped by mutual accessibility, ideal for absolute modalities.^[24] The correspondence between these modal axioms and first-order properties of frames is formalized by the Goldblatt-Thomason theorem, which states that an elementary class of Kripke frames is axiomatizable by a set of modal formulas if and only if it is closed under generated subframes, p-morphic images, and disjoint unions, while reflecting ultrafilter extensions.^[26] This result highlights the expressive power of modal logic in defining frame classes via Sahlqvist formulas, linking syntactic axioms directly to semantic constraints.^[26]

Philosophical Applications

Alethic and Metaphysical Modality

Alethic modalities concern statements about necessity and possibility, where the necessity operator \square is interpreted as asserting that a proposition is true in all possible worlds, and the possibility operator \Diamond as true in at least one possible world. This framework, rooted in possible worlds semantics, provides a philosophical tool for analyzing metaphysical truths that hold independently of contingent facts. In this context, metaphysical necessity captures what must be the case due to the fundamental nature of reality, such as essential properties or identities.^[11]^[27] A key development in alethic modal logic was C.I. Lewis's introduction of strict implication, defined as A \vdash B equivalent to \square(A \to B), which avoids the paradoxes of material implication by requiring that the antecedent necessitates the consequent across all possible worlds. Lewis proposed this to better model philosophical conditionals involving necessity, influencing systems like S4 and S5. For instance, strict implication distinguishes cases where "if A, then B" holds robustly due to modal strength, rather than mere truth-functional overlap.^[11]^[28] Metaphysical necessity is often contrasted with physical (or nomic) necessity, where \square_P \phi denotes truth in all physically possible worlds governed by the laws of nature, while metaphysical necessity \square \phi applies more broadly to all logically coherent worlds. Physical necessities include propositions like "water boils at 100°C at standard pressure," which hold under current natural laws but could vary in metaphysically possible worlds with different physics. In contrast, metaphysical necessities encompass logical truths such as \square(2+2=4), which obtain regardless of physical contingencies. This distinction highlights a hierarchy of modalities, with metaphysical being stricter and more ontologically fundamental.^[29]^[29] The adoption of possible worlds semantics for alethic modalities sparked significant philosophical debate, particularly the Quine-Lewis controversy over ontological commitments. Willard Van Orman Quine argued that quantifying over possible worlds introduces unclear intensional entities and essentialist assumptions, rendering modal discourse metaphysically suspect and preferable to avoid. David Lewis countered by defending modal realism, positing concrete possible worlds as the reductive basis for modality, where necessity is simply truth across all such worlds, thereby committing ontology to their existence without primitive modal primitives. This debate underscores the tension between modal logic's explanatory power in metaphysics and concerns about its realism. Kripke semantics offers a formal interpretation aligning with these philosophical uses, treating necessity via accessibility relations among worlds.^[27]^[30]^[11]

Epistemic and Doxastic Logics

Epistemic logic is a branch of modal logic that formalizes the concept of knowledge for rational agents, using the necessity operator K_a \phi to denote that agent a knows proposition \phi.^[31] This framework originated with Jaakko Hintikka's seminal work, which distinguished knowledge from mere true belief by modeling knowledge via possible worlds semantics where accessibility relations represent an agent's indistinguishability between worlds. In standard epistemic logic, the semantics employ S5 axioms, corresponding to equivalence relations on worlds: reflexivity ensures factivity (K_a \phi \to \phi), ensuring that knowledge implies truth; transitivity captures positive introspection (K_a \phi \to K_a K_a \phi), meaning if an agent knows something, they know that they know it; and euclideaness supports negative introspection (\neg K_a \phi \to K_a \neg K_a \phi), meaning if an agent does not know something, they know that they do not know it.^[31] A key example of factivity is the axiom K_a p \to p, which states that if agent a knows proposition p, then p must be true in the actual world.^[31] For defeasible or non-idealized knowledge, variants like KD45 are used, dropping reflexivity to allow for situations where knowledge is not necessarily veridical, though S5 remains the typical system for idealized knowledge with full introspection.^[31] Doxastic logic extends this to model belief rather than knowledge, using the operator B_a \phi to indicate that agent a believes \phi.^[32] Unlike epistemic logic, doxastic logic standardly employs the KD45 system, which includes the distribution axiom (B_a (\phi \to \psi) \to (B_a \phi \to B_a \psi)) and necessitation rule, along with transitivity (axiom 4: B_a \phi \to B_a B_a \phi) and euclideaness (axiom 5: \neg B_a \phi \to B_a \neg B_a \phi), but omits the truth axiom (T: B_a \phi \to \phi), allowing beliefs to be false.^[32] This reflects that beliefs need not correspond to reality, though they satisfy introspection properties similar to knowledge.^[32] Doxastic logic encounters puzzles such as Moore sentences, exemplified by p \land \neg K_a p or p \land \neg B_a p, which assert a fact while denying knowledge or belief in it; these are assertable in natural language yet lead to inconsistencies in standard S5 epistemic logic due to factivity and introspection, prompting debates on the limits of formalizing subjective attitudes.^[33] In multi-agent settings, epistemic logic introduces group notions like common knowledge C_G \phi for a group G, defined as the fixed point of the "everyone knows" operator E_G \phi = \bigwedge_{a \in G} K_a \phi, such that C_G \phi holds if \phi is known by all, everyone knows that all know, and so on ad infinitum; this requires infinite iterations in Kripke models with transitive closures of union accessibility relations. Robert Aumann's analysis showed that common priors and common knowledge prevent rational agents from agreeing to disagree on probabilities. Distributed knowledge D_G \phi, in contrast, captures what the group would know if they pooled information perfectly, defined over the intersection of individual accessibility relations, satisfying S5-like properties but without requiring actual communication.^[31]

Deontic and Temporal Logics

Deontic logic formalizes reasoning about normative concepts such as obligation, permission, and prohibition, treating these as modalities analogous to necessity and possibility in alethic modal logic. The foundational operators include O\phi, denoting that \phi is obligatory; F\phi, defined as \neg O\neg\phi, indicating that \phi is forbidden; and P\phi, equivalent to \Diamond\phi, signifying that \phi is permitted. These operators apply to propositions or action types, enabling the expression of norms like "it ought to be the case that \phi."^[34] The standard system for deontic logic, known as Standard Deontic Logic (SDL) or the KD system, extends the modal logic K by adding the axiom O\phi \to \Diamond\phi (the D axiom), which ensures that obligations are possible, but omits the T axiom (\Box\phi \to \phi), as obligations do not necessarily entail that their content is actualized.^[34] This framework, developed through reductions to alethic modal logic, avoids assuming that what is obligatory must occur, allowing for the possibility of norm violation.^[34] Despite its influence, SDL encounters paradoxes that challenge its adequacy for normative reasoning. Ross's paradox arises from the inference O\phi \to O(\phi \lor \psi), as in the obligation to mail a letter implying an obligation to mail it or burn it, which intuitively weakens the norm without justification. Similarly, Forrester's gentle murder paradox involves premises like "if Smith murders Jones, he ought to do so gently" and "Smith will murder Jones," leading to the counterintuitive conclusion that Smith ought to murder Jones gently, conflating conditional norms with unconditional ones.^[35] To address these issues, dyadic deontic logics introduce conditional operators such as O(\phi|\alpha), expressing obligation to \phi given \alpha, which resolves paradoxes by distinguishing contexts without deriving unintended disjunctive or conditional obligations. For instance, O(p \to q) can represent a conditional obligation where p triggers the duty for q, avoiding the dilution seen in monadic systems. Temporal logic, a modal extension for reasoning about time, was pioneered to analyze tensed statements and future contingencies. Key operators include G\phi for "\phi always holds in the future," F\phi (dual of G) for "\phi holds at some future time," H\phi for "\phi has always held in the past," and P\phi (dual of H) for "\phi held at some past time." These enable formulas like G(O(p \to q)), capturing enduring conditional obligations over time. Temporal logics differ in their conception of time: linear-time logics, such as Linear Temporal Logic (LTL), assume a single timeline where paths are total orders, suitable for sequential processes.^[36] In contrast, branching-time logics like Computation Tree Logic (CTL) model time as a tree of possible futures, incorporating path quantifiers (e.g., \forall for all paths, \exists for some path) to express properties like inevitability (AG\phi) or possibility (EF\phi). This distinction allows LTL to focus on linear progressions while CTL handles nondeterminism in decision points.^[36]

Advanced Extensions

Dynamic and Hybrid Logics

Dynamic logic extends basic modal logic by incorporating the notion of programs or actions as modalities, allowing reasoning about how states change after executing certain operations. In propositional dynamic logic (PDL), the box operator [\alpha]\phi is interpreted semantically to mean that after executing the program \alpha, the formula \phi necessarily holds in all possible resulting states.^[37] Dually, the diamond operator \langle \alpha \rangle \phi asserts that there exists a possible execution of \alpha after which \phi holds.^[37] This framework builds on Kripke semantics but augments transition relations with program executions, where programs are constructed from atomic actions using operations like sequencing (\alpha;\beta), nondeterministic choice (\alpha \cup \beta), and Kleene star (\alpha^*) for iteration.^[37] Key axioms in dynamic logic capture the interaction between programs and propositions. For instance, the conjunction axiom states that [\alpha] (\phi \land \psi) \leftrightarrow [\alpha]\phi \land [\alpha]\psi, ensuring that necessity after a program preserves conjunctions.^[37] Test programs, denoted ? \phi, represent conditional assertions that succeed only if \phi holds, with the axiom [? \phi] \psi \leftrightarrow \phi \to \psi linking them to implication.^[37] Some variants of PDL, such as those incorporating concurrency, support parallel composition \alpha \| \beta to model concurrent actions, where transitions interleave those of \alpha and \beta.^[37] An illustrative example is the formula [a := x+1] (x > 0), which asserts that after assigning x+1 to variable a, the condition x > 0 holds in all resulting states, useful for verifying program semantics in computational models.^[37] Hybrid logic further enriches modal logic by adding nominals and operators that enable explicit reference to individual worlds, bridging the gap between modal and first-order expressivity without full quantification. Nominals, denoted i, are atomic formulas true at exactly one world i in a Kripke model.^[38] The binder \downarrow x . \phi binds the variable x to the current world of evaluation, allowing \phi to refer back to that specific state.^[38] The satisfaction operator @_i \phi asserts that \phi is true at the world named by nominal i, facilitating jumps to arbitrary points in the model.^[38] These features, including nominals as jumps and binders as guards, support precise state referencing and have been formalized in systems like those explored in early hybrid languages.^[38] Dynamic logic can be seen as evolving from temporal logics, which model time as actions, providing a precursor for action-based modalities.^[39]

Non-Classical Variants

Non-classical variants of modal logic deviate from the classical bivalent framework by incorporating alternative truth values, relevance conditions, or constructive principles, often to better model uncertainty, vagueness, or non-explosive reasoning. Unlike standard Kripke semantics for classical modal logic K, which assumes crisp accessibility relations and bivalent truth, these variants modify the underlying logic to handle graded or intuitionistic modalities.^[11] Intuitionistic modal logic combines the intuitionistic propositional base, which rejects the law of excluded middle and emphasizes constructive proofs, with modal operators for necessity (□) and possibility (◇). Semantics employ Kripke models featuring a partial order ≤ for monotonicity of intuitionistic connectives (if w \vdash \phi and w \leq w', then w' \vdash \phi) and a binary accessibility relation R for modalities, where w \vdash \square \phi if for all w' \geq w and all v' such that w' R v', it holds that v' \vdash \phi, and w \vdash \Diamond \phi if there exists v with w R v and v \vdash \phi. Frame conditions like confluence ensure compatibility: if w' \geq w R v, then there exists v' \geq v with w' R v'. A key distinction from classical modal logic is that \square \phi \to \phi fails, as R need not be reflexive and intuitionistic logic lacks double negation elimination, preventing necessity from implying truth at the current world without additional conditions such as reflexivity. Necessity here is constructive, requiring verifiable proofs of φ at all accessible future worlds rather than mere potential truth.^[40] Fuzzy modal logic extends the classical framework to many-valued logics with truth values in the unit interval [0,1], accommodating degrees of truth for vague or imprecise statements. In Gödel fuzzy modal logic, conjunction (∧) is interpreted as the minimum (min) and disjunction (∨) as the maximum (max), while implication (→) follows the Gödel t-norm: a \to b = 1 if a \leq b, otherwise b. Semantics use fuzzy Kripke frames with a fuzzy accessibility relation R: W \times W \to [0,1], where the truth value of necessity is e(\square \phi, w) = \inf \{ R(w, w') \to_G e(\phi, w') \mid w' \in W \}, aggregating the infimum over degrees of accessibility weighted by the Gödel implication of φ's truth in accessible worlds. This allows modalities to reflect gradual necessity or possibility, with possibility defined dually via supremum. The logic admits strong completeness and is PSPACE-complete, enabling axiomatizations that extend basic fuzzy logic BL with modal rules.^[41] Relevance modal logics, often denoted as R-mods, integrate modal operators into relevant logics to prevent the explosion principle (from a contradiction, anything follows) by enforcing relevance between premises and conclusions in implications. Building on Routley-Meyer semantics, models consist of a set of worlds W, a ternary Routley relation R ⊆ W³ for strict implication, and operations like Routley star (*) for negation, where a \models A \to B holds if for all b, c with R a b c and b \models A, it follows that c \models B, ensuring the antecedent and consequent share propositional content via relevance constraints (e.g., postulates like addition and contraction are restricted). Modal extensions incorporate binary relations for □ and ◇, with general frames providing completeness relative to relevant algebras. These logics maintain paraconsistency, avoiding irrelevant deductions, and differ from classical modal logics by using ternary relations instead of binary ones, thus modeling stricter conditions for necessity in resource-sensitive or information-theoretic contexts.^[42] An application of fuzzy modal logic arises in artificial intelligence for handling vagueness, such as modeling gradual possibility degrees for imprecise concepts like "tall" or "likely." In qualitative fuzzy modal logics like QFL2, possibility measures extend to fuzzy propositions via Zadeh's principle: the possibility of a fuzzy event A is \Pi(A) = \sup_w (\pi(w) \wedge \|A\|_w), where π(w) is the possibility of world w and ∧ is a t-norm. Modalities compare degrees, e.g., A <_l B holds if \Pi(A) \leq \Pi(B), enabling reasoning about comparative possibilities in belief or knowledge representation under uncertainty, with soundness and completeness relative to fuzzy frames. This framework supports AI systems in decision-making with vague data, such as natural language processing or expert systems.^[43]

Applications Beyond Philosophy

In Computer Science

Modal logic plays a central role in computer science, particularly in formal verification techniques for ensuring the correctness of concurrent and distributed systems. Model checking, a key application, uses branching-time modal logics like Computation Tree Logic (CTL) to verify properties of finite-state systems by exhaustively exploring their state spaces. CTL extends propositional logic with path quantifiers (such as "for all paths" and "there exists a path") and temporal operators (next, always, eventually, until), enabling the specification of safety and liveness properties in concurrent programs. The seminal algorithm for CTL model checking, which runs in time linear in the product of the model and formula sizes, was developed by Clarke, Emerson, and Sistla in 1986, allowing efficient verification of hardware and software systems against modal specifications.^[44] For more expressive needs, the propositional μ-calculus incorporates least fixed-point operators to handle recursive definitions, capturing temporal logics like CTL and Linear Temporal Logic (LTL) as fragments; this makes it foundational for advanced verification tools that translate LTL formulas into automata for on-the-fly checking. Kozen's 1983 work established the μ-calculus's decidability and equivalence to alternating Turing machines, underscoring its computational power in fixpoint-based verification.^[45] In multi-agent systems, epistemic modal logic formalizes agents' knowledge and beliefs, aiding analysis of distributed computing scenarios where agents reason about others' information. The muddy children puzzle exemplifies this: n children with muddy foreheads deduce their own muddiness through iterative public announcements, modeled using Kripke structures where accessibility relations represent indistinguishability of worlds based on agents' knowledge. This puzzle, analyzed in Fagin et al.'s 1995 framework, illustrates common knowledge as a fixed point of iterated knowledge operators, essential for protocols like coordinated attack or Byzantine agreement in distributed systems. Epistemic logics thus enable verification of knowledge-based properties in multi-agent environments, such as ensuring that agents achieve mutual knowledge after message exchanges.^[46] Dynamic modal logic supports program verification by interpreting modalities over program executions, connecting closely to Hoare logic's partial correctness assertions. Propositional dynamic logic (PDL), introduced by Harel in 1979, uses box and diamond operators to express postconditions reachable via programs, generalizing Hoare triples {P} α {Q} where α is a regular program. This framework allows proving program properties through axiomatic semantics, with test and iteration constructs handling conditionals and loops. Extensions link dynamic logic to separation logic, where modal operators like "precisely" or "at-most" quantify heap access in concurrent settings, enabling modular reasoning about shared mutable data without aliasing errors. Demri and Deterding's 2004 survey highlights how these modals bridge separation logic's separating conjunction with Kripke-style semantics for permissions and resources.^[47]^[48] Post-2000 developments integrate modal logic into programming languages and AI planning. Modal types, inspired by judgmental reconstructions of modal logics, encode computational effects, staging, and distributed protocols directly in type systems; for instance, Pfenning and Wong's 1995 work interprets modal proofs as distributed programs, using necessity modalities for local state and possibility for communication.^[49] In AI planning, extensions of the Planning Domain Definition Language (PDDL) incorporate epistemic modals to handle incomplete information and knowledge updates, as in E-PDDL, which standardizes multi-agent epistemic planning problems with Kripke models for belief states. These advancements enable planners to generate sequences achieving knowledge goals, such as coordinated actions in uncertain environments. Recent research (as of 2025) explores the integration of modal logic with large language models (LLMs) to enhance their logical reasoning capabilities. Studies evaluate LLMs' performance on modal inference tasks, revealing limitations in handling necessity and possibility, and propose frameworks to incorporate modal structures for improved reasoning in natural language processing and AI systems.^[50]^[51]

In Mathematics and Linguistics

In mathematics, modal logic finds significant applications in formalizing concepts of provability, set theory, and structural semantics. Provability logic, particularly the system GL, extends basic modal logic to capture the properties of formal provability within arithmetic systems. In GL, the necessity operator \square \phi interprets as "\phi is provable," satisfying axioms such as the necessitation rule and the distribution axiom \square(\phi \to \psi) \to (\square \phi \to \square \psi), alongside the Löb axiom \square(\square \phi \to \phi) \to \square \phi.^[52] This system provides a precise framework for interpreting Gödel's incompleteness theorems; for instance, the principle \square \phi \to \square \square \phi reflects that if a sentence is provable, then its provability is also provable, aligning with the formalized self-referential properties in Gödel's construction.^[53] Second-order modal logic extends these ideas to higher expressive power, enabling the encoding of set-theoretic structures where modalities quantify over predicates or sets. This allows for the interpretation of second-order arithmetic within modal frameworks, where necessity operators bind over higher-order variables to model concepts like set existence across possible worlds.^[54] In set theory, such logics facilitate the analysis of modal forcing, treating accessibility relations as set-theoretic functors that preserve hierarchical structures like the cumulative hierarchy. Coalgebraic semantics provides a categorical generalization of Kripke semantics for modal logics, viewing models as coalgebras over endofunctors on sets or more general categories. This approach unifies diverse modal systems by defining satisfaction through predicate liftings that correspond to the functor's structure, enabling the study of bisimulation and logical equivalence in a coalgebraic setting. Connections to category theory further integrate modal operators as functors or monads; for example, the box operator can be seen as a comonad on the category of Kripke frames, preserving limits and facilitating adjointness relations that mirror necessity-possibility dualities. In linguistics, modal logic underpins formal semantics for natural language phenomena like tense, aspect, and interrogation. Montague grammar incorporates modal operators to handle temporal and aspectual expressions, treating tenses as modalities over time points; for instance, the past tense operator shifts evaluation to an earlier reference time, formalized as \square_{past} \phi where \square accesses prior worlds in a linear time frame.^[56] This integration allows for compositional semantics of sentences involving modals, such as "John will have left," by combining tense modalities with aspectual perfectivity.^[57] Inquisitive semantics extends modal logic to questions using the possibility operator \Diamond, interpreting it as projecting inquisitive content that supports multiple propositional alternatives. In this framework, a question like "Is p or q?" is semantically \Diamond (p \lor q), where \Diamond \psi holds in a state if the state supports at least one complete resolution of \psi's alternatives, enabling a unified treatment of assertions and inquiries.^[58] This approach contrasts with traditional declarative semantics by emphasizing information states, thus capturing the dynamic updates in discourse.

Historical Development

Early Foundations

The foundations of modal logic trace back to Aristotle's development of modal syllogisms in the Prior Analytics, where he extended his assertoric syllogistic to incorporate modalities of necessity and possibility. Aristotle treated necessary propositions as those that cannot be otherwise and possible (or contingent) propositions as those that are neither necessary nor impossible, allowing premises to be qualified with these operators—such as two necessary premises yielding a necessary conclusion in figures like Barbara (NNN)—while systematically analyzing mixed cases, including necessary with assertoric or contingent premises. This framework addressed validity through demonstrations mirroring non-modal syllogisms, though with adaptations like ecthesis for certain invalid forms, establishing modal logic as an integral part of deductive reasoning about what must, may, or cannot hold.^[59] Medieval logicians built upon these Aristotelian roots, with significant advancements by Avicenna (Ibn Sina) in the 11th century, who systematized modal propositions into an eight-fold classification incorporating temporal dimensions, such as "always" (perpetual) and "sometime" (temporal possibility). Avicenna refined Aristotle's modalities by distinguishing referential (essential, tied to the subject's nature) from non-referential (accidental) readings, enabling a more nuanced treatment of temporal modals in categorical syllogisms and expanding the square of opposition to account for perpetual and absolute propositions. His innovations, detailed in works like the Shifāʾ, addressed ambiguities in Aristotle's mixed modal syllogisms and introduced quantified hypothetical syllogisms with modal conditionals, influencing subsequent Islamic and Latin traditions in logic.^[60] In the early 20th century, Clarence Irving Lewis revitalized modal logic amid dissatisfaction with the material implication of Principia Mathematica (1910–1913) by Bertrand Russell and Alfred North Whitehead, which permitted paradoxes such as a false antecedent implying any consequent. Lewis proposed strict implication in his 1918 A Survey of Symbolic Logic, defining it as the necessity of the consequent given the antecedent (¬◇(p ∧ ¬q)), to capture intuitive notions of logical consequence without these flaws, and outlined initial systems like S1 with axioms for possibility (◇) and rules like uniform substitution. Building on this, Lewis and Cooper Harold Langford provided an algebraic semantics for modal operators treated as monadic functions on propositions in their 1932 Symbolic Logic, which formalized pre-Kripke interpretations of necessity and possibility through Boolean structures extended to unary operations.^[61]^[62] The 1930s marked a pivotal formalization with Lewis and Cooper Harold Langford's Symbolic Logic (1932), which axiomatized a hierarchy of systems S1 through S5, progressing from the minimal S1 (weakest, without transitivity) to S5 (strongest, with Euclidean and reflexive properties like ◇p → □◇p). These systems used possibility as primitive and defined necessity as ¬◇¬p, with added postulates—such as S4's transitivity (□p → □□p) and S5's symmetry— to delineate varying modal strengths while avoiding the paradoxes of material implication, thus establishing a rigorous syntactic foundation for alethic modal logic that influenced subsequent philosophical and logical inquiry.^[62]^[63]

Modern Expansions

The introduction of Kripke models in 1963 marked a pivotal advancement in modal logic by providing a relational semantics that revolutionized the understanding of completeness for various modal systems. Saul Kripke's framework defined models as sets of possible worlds connected by accessibility relations, enabling precise semantic characterizations of modal operators like necessity and possibility, and establishing soundness and completeness theorems for systems such as K, T, S4, and S5.^[64] This approach addressed longstanding issues in axiomatic completeness by grounding modal validity in graph-like structures, influencing subsequent developments in non-classical logics. Building on Kripke's semantics, correspondence theory emerged in the 1960s and 1970s as a key area of expansion, linking modal formulas to first-order properties of accessibility relations. Pioneered by researchers like Johan van Benthem and Saul Kripke, this theory demonstrated how specific axioms correspond to relational constraints, such as reflexivity for the T axiom (□p → p) or transitivity for the 4 axiom (□p → □□p). The Sahlqvist theorem of 1975 provided a general method for establishing such correspondences for a broad class of modal formulas, facilitating algorithmic checks for canonicity and completeness in extended systems.^[11] During the 1970s and 1980s, refinements to epistemic and deontic logics further expanded modal frameworks, integrating them with philosophical and computational concerns. Jaakko Hintikka's 1962 work on epistemic logic, refined in subsequent analyses, formalized knowledge and belief operators using Kripke models with S5-like accessibility for idealized agents, enabling distinctions between justified true belief and mere possibility.^[31] Similarly, G.H. von Wright's foundational deontic logic from 1951 saw advancements in the 1970s, incorporating contrary-to-duty obligations and defeasible norms to better model ethical reasoning. In parallel, Amir Pnueli's 1977 introduction of linear temporal logic (LTL) adapted modal operators (e.g., "eventually" and "always") for verifying program properties, laying groundwork for model checking in computer science.^[36] The 1990s and beyond saw dynamic and hybrid logics as major extensions, enhancing expressiveness for computational and structural applications. David Harel's contributions in the 1980s, culminating in comprehensive treatments by the 1990s, developed dynamic logic to reason about program transitions using modal operators over actions, with [α]φ denoting postcondition φ after executing program α.^[65] Hybrid logics, advanced by Jerry Seligman in the 1990s, added nominals (state labels) and binders to Kripke models, allowing direct reference to worlds and bridging modal logic with first-order expressivity. Coalgebraic generalizations, initiated in the late 1990s, unified modal semantics across categories beyond sets, treating modalities as homomorphisms on coalgebras for endofunctors, thus encompassing probabilistic and game-theoretic logics. The μ-calculus, formalized by Dexter Kozen in 1983, integrated least fixed points into modal logic, providing a decidable fragment for expressing infinite behaviors in verification, such as safety properties in concurrent systems, and highlighting modal logic's deepening integration with computer science.^[66] In the 2020s, modal logic has extended to quantum and AI domains, addressing contemporary challenges. Quantum modal logics formalize superposition and measurement using orthomodular lattices with modal operators, as in Kenji Tokuo's 2024 framework.^[67] A follow-up 2025 work by Tokuo proves decidability for basic quantum modalities via Harrop's lemma.^[68] Deontic variants have been applied to AI ethics, with post-2020 works like deontic temporal logic verifying ethical constraints in autonomous systems, such as obligation persistence over time in decision-making algorithms.^[69]

References

[1]
[PDF] a brief introduction to modal logic
[3] Hughes, G. E. and M. J. Cresswell, A New Introduction to Modal Logic, New York, NY: Routledge, 1996.
[2]
[PDF] Basic Concepts in Modal Logic - Stanford University
Modal logic is the study of modal propositions and the logical relation- ships that they bear to one another. The most well-known modal propo- sitions are ...
[3]
[PDF] An Open Introduction to Modal Logic - Boxes and Diamonds
The basic concept of semantics for normal modal logics is that of a relational model. It consists of a set of worlds, which are related by a binary ...
[4]
[PDF] MATHEMATICAL MODAL LOGIC: A VIEW OF ITS EVOLUTION
Over a period of three decades or so from the early 1930's there evolved two kinds of mathematical semantics for modal logic. Algebraic semantics interprets.
[5]
Propositional Logic | Internet Encyclopedia of Philosophy
Propositional logic, also known as sentential logic, is that branch of logic that studies ways of combining or altering statements or propositions to form more ...
[6]
[PDF] 1. the propositional calculus pl - UCLA Department of Mathematics
Apr 5, 2021 · Formulas. The formulas (or well formed formulas) of PL are defined recursively by the following three clauses: (a) Each propositional ...
[7]
[PDF] CHAPTER 2 INTRODUCTION TO CLASSICAL PROPOSITIONAL ...
The syntax establishes the set of symbols, called the alphabet, and describes precisely how to form acceptable expressions, called formulas. Such established ...
[8]
Propositional Logic
Syntax. The symbols are: p q r ' < > ~ ∧ ∨ ⊃ [ ] The set of formulae, also known as well-formed strings, is defined recursively as follows, with v ranging over ...
[9]
[PDF] Lecture 1: Propositional Logic
The well-formed formulas of propositional logic are obtained by using the construction rules below: An atomic proposition is a well-formed formula.Missing: classical | Show results with:classical
[10]
[PDF] An Introduction to Classical Propositional Logic: Syntax, Semantics ...
The length of (p0 ∧ (p0 → p1)) → p1 is 7. We have just defined the syntax (language) of classical propositional logic: it is simply the set of all formulae we ...
[11]
Modal Logic - Stanford Encyclopedia of Philosophy
Feb 29, 2000 · Modal logic is, strictly speaking, the study of the deductive behavior of the expressions 'it is necessary that' and 'it is possible that'.Missing: scholarly | Show results with:scholarly
[12]
[PDF] Semantical Analysis of Modal Logic I Normal Modal Propositional ...
The present paper attempts to extend the results of [l], in the domain of the propositional calculus, to a class of modal systems called “normal.
[13]
[PDF] Neighborhood Semantics for Modal Logic An Introduction
Jul 3, 2007 · Welcome to Neighborhood Semantics for Modal Logic! The course will consist of five 90 minute lectures roughly organized as follows:.
[14]
[PDF] Neighborhood Semantics for Modal Logic - Eric Pacuit
Mar 21, 2017 · Generally speaking, there are two different ways to motivate the study of a logical frame- work. The first is to identify an interesting ...
[15]
[PDF] Topological semantics of modal logic
Modal logic admits algebraic, relational and topological semantics. Topological semantics of modal logic was introduced and developed by McKinsey and Tarski in ...
[16]
[PDF] Axiomatic Derivations - Open Logic Project Builds
For normal modal logics, all instances of tau- tologies, K, and dual count as axioms. This results in the modal system K, the smallest normal modal logic.
[17]
[PDF] 2 Modal System K
System K is named after the logician-philosopher Saul Kripke, who was among the first to systematize formal semantics for modal logic. The rules of K are ...
[18]
A New Introduction to Modal Logic - 1st Edition - M.J. Cresswell - G.E
In stock Free deliveryThis long-awaited book replaces Hughes and Cresswell's two classic studies of modal logic: An Introduction to Modal Logic and A Companion to Modal Logic.
[19]
First-order modal tableaux | Journal of Automated Reasoning
We describe simple semantic tableau based theorem provers for four standard modal logics, in both propositional and first-order versions.
[20]
[PDF] Semantic Tableaux Methods for Modal Logics That Include the B ...
(i) determine whether any just- altered branches close; if so, close the branch by placing an 'x' at the bottom of the branch. (ii) choose an un-checked complex ...
[21]
[PDF] Modal Tableaux - Open Logic Project Builds
A tableau begins with a number of assumptions. Each further signed formula is generated by applying one of the inference rules. Some inference rules add.
[22]
[PDF] Automated Reasoning in Modal and Description Logics via SAT ...
A machine program for theorem-proving. Journal of the ACM, 5(7), 394–397. 386. Page 45. Automated Reasoning in Modal and Description Logics via SAT Encoding.
[23]
[PDF] Solving the Satisfiability Problem of Modal Logic S5 Guided ... - IJCAI
In this paper, we present a novel. SAT-based approach for S5 satisfiability problem. We show a normal form for S5 formulas. Based on this normal form, a ...
[24]
[PDF] a new introduction to modal logic - STOQ
This book is intended as a replacement for our earlier two books An. Introduction to Modal Logic (Hughes and Cresswell, 1968, IML) and A. Companion to Modal ...
[25]
[PDF] Introduction to Modal Logics (Lecture Notes
Jul 22, 2015 · In what follows let S4.3 be the smallest normal modal logic that is obtained from S4 by adding the axiom. (.3) D(Dp→q)∨D(Dq→ p),. It can ...
[26]
Possible Worlds - Stanford Encyclopedia of Philosophy
Oct 18, 2013 · In Lewis's theory of modality, then, modal operators are understood semantically to be quantifiers over concrete worlds, predicates denote ...
[27]
Modern Origins of Modal Logic - Stanford Encyclopedia of Philosophy
Nov 16, 2010 · The scope of this entry is the recent historical development of modal logic, strictly understood as the logic of necessity and possibility.Missing: Hilbert- | Show results with:Hilbert-
[28]
Varieties of Modality - Stanford Encyclopedia of Philosophy
Nov 27, 2012 · Dualists distinguish between two concepts of propositional necessity, metaphysically necessity and epistemic necessity. The two notions are not ...
[29]
Ontological Commitment - Stanford Encyclopedia of Philosophy
Nov 3, 2014 · A second well-known example is Lewis's argument from Counterfactuals that modal discourse, as he understands it, is committed to possible worlds ...
[30]
[PDF] Reasoning About Knowledge - Rice University
Knowledge and common knowledge were first applied to multi-agent systems by Halpern and Moses [1990] and by Lehmann [1984]. The need for common knowledge in ...
[31]
[PDF] Moore's paradox and the logic of belief - arXiv
In that seminal work, Hintikka developed a multimodal logic for statements that express sentences containing the epistemic notions of knowledge and belief.
[32]
A Reduction of Deontic Logic to Alethic Modal Logic - jstor
It also indicates that deontic logic need not be regarded as an autonomous branch of formal logic, but may be viewed simply as a special branch of alethic modal ...
[33]
A Solution to Forrester's Paradox of Gentle Murder - jstor
(6) It is obligatory, that Smith murder Jones gently. But it is necessary that. (7) If Smith murders Jones gently, then Smith murders Jones.
[34]
The temporal logic of programs | IEEE Conference Publication
The main proof method suggested is that of temporal reasoning in which the time dependence of events is the basic concept.<|control11|><|separator|>
[35]
[PDF] Dynamic Logic - Cornell: Computer Science
Dynamic Logic. David Harel, The Weizmann Institute. Dexter Kozen, Cornell University. Jerzy Tiuryn, University of Warsaw. The MIT Press, Cambridge ...
[36]
[PDF] Hybrid Languages - Patrick Blackburn
The purpose of this paper is to introduce and explore a number of hybrid languages. These are like first-order languages in their explicit use of variables and ...
[37]
[PDF] Semantical Considerations on Floyd-Hoare Logic
SEMANTICAL CONSIDERATIONS ON FLOYD-HOARE LOGIC. Vaughan R. Pratt. Massachusetts Institute of Technology. Cambridge, MA 02139. This paper deals with logics of ...
[38]
[PDF] The Proof Theory and Semantics of Intuitionistic Modal Logic
He defined a first-order intuitionistic version of the modal logic T with the. Barcan formula. He gave the logic both a Hilbert-style axiomatization and a.
[39]
[PDF] Fuzzy bi-Gödel modal logic and its paraconsistent relatives - arXiv
Mar 7, 2024 · 3In this text, we use the term 'fuzzy modal logic' to denote the logic of all frames (i.e., crisp and fuzzy); 'crisp modal. logic' stands for ...
[40]
General Frames for Relevant Modal Logics - Project Euclid
General frames are often used in classical modal logic. Since they are duals of modal algebras, completeness follows automatically as with algebras but.Missing: mods | Show results with:mods
[41]
[PDF] On Modal Logics for Qualitative Possibility in a Fuzzy Setting - arXiv
On the other hand, vagueness (fuzziness) concerns de grees of truth, usually numerical, and therefore one is led to many-valued logics as underlying formalism.
[42]
[PDF] On Two Models of Provability - Sergei N. Artemov
The logic GL formalizes Gödel's second incompleteness the- orem ¬2(¬2 ... This principle provided the last axiom of the provability logic GL, named ...
[43]
The Logic of Provability - ScienceDirect.com
Gödel's incompleteness theorems and Church's undecidability theorem for arithmetic showed that reasonably strong formal systems cannot be complete and ...
[44]
The Expressive Power of Second-Order Propositional Modal Logic
It has been shown by Fine in [1] that second-order arithmetic can be interpreted in second-order propositional modal logic, denoted SOPML, when the modality ...
[45]
(PDF) Some Second Order Set Theory - ResearchGate
Aug 7, 2025 · This article surveys two recent developments in set theory sharing an essential second-order nature, namely, the modal logic of forcing.<|separator|>
[46]
[PDF] Methodology and Verifiability in Montague Grammar - ACL Anthology
Our observations show that a model-theoretic approach to natural language semantics is inadequate with respect to its verifiability from logical point of view.
[47]
19 Applications of modal logic in linguistics - ScienceDirect
Modal logic is known in linguistics for the light it throws on semantics; Richard Montague's use of higher-order modal logic for this purpose is widely ...
[48]
[PDF] A First-Order Framework for Inquisitive Modal Logic
The semantics for inquis- itive modal logic is given in terms of satisfaction of formulae in information states (support semantics in [6, 2]), i.e. in sets of ...
[49]
https://dl.acm.org/doi/10.1145/204382.204386
[50]
https://arxiv.org/abs/2401.17169
[51]
https://dl.acm.org/doi/10.1007/978-981-95-0014-7_2
[52]
Symbolic Logic : Lewis, Clarence Irving and Langford, Cooper Harold
Dec 14, 2022 · Symbolic Logic. by: Lewis, Clarence Irving and Langford, Cooper Harold. Publication date: 1932. Collection: internetarchivebooks; inlibrary ...
[53]
https://www.sciencedirect.com/science/article/pii/S0049237X98800220
[54]
[PDF] saul a. kripke
To get a semantics for modal logic, we introduce the notion of a (normal) model structure. A model structure (m.s.) is an ordered triple (G, K, R) where K ...
[55]
Epistemic Logic - Stanford Encyclopedia of Philosophy
Jun 7, 2019 · Knowledge and belief are represented via the modal operators K and B, often with a subscript indicating the agent that holds the attitude.
[56]
[PDF] DYNAMIC LOGIC - Weizmann Institute of Science
Dynamic Logic (DL) is a formal system for reasoning about programs. Tradition- ally, this has meant formalizing correctness specifications and proving ...<|control11|><|separator|>
[57]
[PDF] mu.pdf - CS@Cornell
The propositional µ-calculus refers collectively to a class of programming logics consisting of propositional model logic with a least fixpoint operator µ.
[58]
[PDF] Deontic Temporal Logic for Formal Verification of AI Ethics - arXiv
This paper suggests the use of deontic logic along with tem- poral operators to formalize and evaluate ethical principles in. AI. We provided fundamental ...