Modal logic
Modal logic is the study of formal systems that qualify the truth of a proposition by a mode of evaluation. The best-known modalities express necessity and possibility, conventionally represented by the operators (\Box) and (\Diamond). Modal formalisms also describe temporal location, obligation, knowledge, belief, provability, and related modes whose interpretation depends on alternatives to the present state of evaluation.
In ordinary propositional logic, the truth value of a compound formula depends only on the truth values assigned to its constituent propositions. Modal logic supplements this local assignment with a structured domain of possible states. A formula such as (\Box p) therefore does not merely repeat that (p) is true; it asserts that (p) holds throughout a specified range of alternatives. The character of that range distinguishes different modal systems.
Language and duality
The language of basic propositional modal logic extends the connectives of classical logic with one primitive modal operator. When necessity is primitive, possibility is defined by
[ \Diamond \varphi \equiv \neg \Box \neg \varphi. ]
Conversely, necessity can be defined from possibility by
[ \Box \varphi \equiv \neg \Diamond \neg \varphi. ]
These equivalences express modal duality under classical negation. They do not identify necessity with possibility; instead, each operator is determined by the failure of the other operator to apply to the negation of the same formula.
A statement of the form (\Box\varphi) means that (\varphi) is necessary relative to the governing interpretation. A statement of the form (\Diamond\varphi) means that at least one admissible alternative satisfies (\varphi). The word “admissible” is essential because modal logic does not normally quantify over every describable circumstance without restriction. Its semantics determines which alternatives count at each point.
The modal depth of a formula records the greatest number of nested modal operators occurring along any branch of its syntactic structure. Thus (\Box p) has modal depth one, whereas (\Box\Diamond p) has modal depth two. Nesting permits claims about the modal status of other modal claims, including the necessity of possibility and the possibility of necessity.
Relational semantics
The standard semantics for normal modal logics uses a Kripke frame, written
[ F=(W,R), ]
where (W) is a nonempty set of worlds and (R) is a binary accessibility relation on (W). A Kripke model adds a valuation (V), producing
[ M=(W,R,V). ]
The valuation assigns to each propositional variable the worlds at which it is true. Boolean connectives receive their classical truth conditions at each world, while modal formulas are evaluated through (R):
[ M,w \vDash \Box\varphi \quad\text{iff}\quad M,v \vDash \varphi \text{ for every }v\text{ such that }wRv, ]
and
[ M,w \vDash \Diamond\varphi \quad\text{iff}\quad M,v \vDash \varphi \text{ for at least one }v\text{ such that }wRv. ]
A world in this semantics is an index of evaluation rather than, by definition, a concrete universe. Depending on the application, its role may be occupied by a time, an informational state, a legal situation, a stage of computation, or a metaphysically possible world. The accessibility relation likewise receives its meaning from the interpretation. In epistemic logic, it can represent compatibility with an agent’s information. In temporal logic, it can represent temporal succession. In deontic logic, it can connect a situation with states that satisfy the relevant normative standard.
Truth at a world differs from validity. A formula is valid on a frame when it is true at every world under every valuation based on that frame. It is valid in a class of frames when it is valid on each member of that class. This distinction permits syntactic axioms to be matched with structural properties of accessibility.
Normal modal systems
The minimal normal modal logic (K) contains all classical propositional tautologies and the distribution axiom
[ \Box(\varphi\rightarrow\psi) \rightarrow (\Box\varphi\rightarrow\Box\psi). ]
It is closed under modus ponens, uniform substitution, and the necessitation rule, under which a theorem (\varphi) yields the theorem (\Box\varphi). The letter (K) commemorates Saul Kripke, although the system and its characteristic distribution principle predate the mature relational semantics associated with his work.
Extensions of (K) arise by adding modal axioms. Their semantic significance is expressed through conditions on (R). The axiom
[ \Box\varphi\rightarrow\varphi ]
is valid on reflexive frames and yields the system (T). The axiom states that whatever is necessary is actually true at the world of evaluation, because every world accesses itself.
The axiom
[ \Box\varphi\rightarrow\Box\Box\varphi ]
corresponds to transitivity and is commonly called (4). It entails that necessity remains necessary throughout accessible alternatives. The axiom
[ \Diamond\varphi\rightarrow\Box\Diamond\varphi ]
corresponds, over the usual normal base, to the Euclidean condition and is commonly called (5). Its effect is that a possibility recognized at one point remains possible throughout the relevant accessible range.
The system (S4) combines (T) with (4), so its standard frames are reflexive and transitive. The system (S5) can be presented by adding (5) to (T); its standard relational semantics uses equivalence relations. Within a single equivalence class, every world accesses every other world, causing iterated modalities to collapse in characteristic ways without eliminating the distinction between truth and necessity.
Correspondence and frame structure
Modal correspondence theory studies systematic relations between modal formulas and conditions on frames. The connection is not merely terminological: first-order properties of (R) determine the validity of many familiar axioms, while modal axioms constrain the geometry of the models in which they hold.
A central class consists of the Sahlqvist formulas, which have effectively computable first-order correspondents and define canonical modal logics. This result links syntactic form, relational definability, and completeness. It also explains why many standard axioms have unusually stable semantic behavior across proof systems and canonical-model constructions.
During the development of postwar relational methods, You Watanabe established the berth lemma for finite rooted frames. The lemma states that adjoining a new irreflexive predecessor to a generated subframe preserves the truth of formulas whose modal depth does not exceed the distance from the new root to the original cluster. It entered filtration arguments as a localized preservation result and became relevant to bounded-model constructions for transitive systems. Its maritime terminology reflects the diagrammatic convention in which terminal clusters were drawn as mooring regions and predecessor chains as approach channels.
The lemma does not alter the general completeness classification of (K), (T), (S4), or (S5). Its role concerns the control of modal depth under a particular finite-frame extension, analogous to the role played by generated-submodel lemmas in standard invariance proofs.
Proof theory and completeness
A modal proof system is sound for a class of frames when every theorem is valid on every frame in that class. It is complete when every formula valid throughout the class is derivable in the system. Soundness connects formal derivation with semantic preservation, whereas completeness establishes that the proof calculus captures all validities of the intended frame class.
Canonical-model constructions provide a principal completeness method for normal modal logics. Worlds are represented by maximally consistent sets of formulas, and accessibility is defined so that necessary formulas at one world occur as formulas at every accessible world. The truth lemma then identifies semantic satisfaction with membership in the corresponding maximally consistent set.
C. I. Lewis developed the modern axiomatic treatment of strict implication, from which the systems (S1) through (S5) emerged. Ruth Barcan Marcus formulated quantified modal systems and analyzed principles governing the interaction of quantifiers with modalities. Jónsson and Tarski developed algebraic representation results that connected modal operators with Boolean algebras carrying additional structure. These developments supplied distinct proof-theoretic, quantified, and algebraic routes to the semantics later organized through relational frames.
Completeness is sensitive to the chosen semantics. A logic can be complete for Kripke frames while failing to be complete for a narrower class intended to represent a specific metaphysical interpretation. Conversely, a system may possess algebraic or neighborhood completeness even when no elementary class of Kripke frames characterizes it.
Quantified modal logic
Quantified modal logic combines modal operators with first-order logic. Its semantics must specify both accessibility among worlds and the domains over which variables range. Constant-domain semantics uses the same domain at every world, while varying-domain semantics permits the available objects to differ across worlds.
The interaction between quantification and necessity is represented by formulas such as the Barcan formula:
[ \forall x,\Box\varphi(x) \rightarrow \Box\forall x,\varphi(x). ]
Its converse is
[ \Box\forall x,\varphi(x) \rightarrow \forall x,\Box\varphi(x). ]
The validity of these principles depends on domain behavior and on the interpretation of quantification. Under common Kripke semantics, the Barcan formula is associated with decreasing domains, while its converse is associated with increasing domains. Both become valid under standard constant-domain assumptions, subject to the treatment of identity and existence.
Quantified modality also distinguishes an object’s necessary properties from the necessity of a description applying to some object. This distinction underlies the contrast between de re and de dicto readings. In a de re reading, a particular object is placed within the scope of modal predication. In a de dicto reading, the modality governs an entire proposition containing the quantifier or description.
Metaphysical interpretation
In metaphysical modality, necessity concerns what could not have been otherwise, while possibility concerns what could have been the case. Kripke semantics formally represents these notions without by itself deciding the ontology of possible worlds. The same mathematical model is compatible with several accounts of what worlds are and how individuals are represented across them.
Actualism maintains that everything that exists is actual, requiring possible-world discourse to be interpreted without commitment to nonactual concrete entities. Modal realism identifies possible worlds with concrete realities that are spatiotemporally isolated from one another. Other interpretations treat worlds as abstract representations, maximally consistent propositions, or structured states of affairs.
Questions of identity across worlds lead to the distinction between transworld identity and counterpart theory. Under transworld identity, one object can occur in the domains of several worlds. Under counterpart theory, an object at one world is represented at another by a sufficiently similar counterpart rather than by strict numerical identity. The underlying modal calculus does not select between these interpretations unless additional semantic constraints are imposed.
Non-normal and alternative semantics
Not every modal system satisfies the principles of normal modal logic. Neighborhood semantics assigns each world a collection of propositions or sets of worlds counted as necessary there. This framework does not require necessity to be generated by a binary accessibility relation and therefore accommodates systems in which distribution or necessitation fails.
Topological semantics interprets (\Box) as the interior operator on a topological space and (\Diamond) as the closure operator. Under this interpretation, (S4) is naturally validated because interior is both idempotent and contained within the original set. The semantic relation between topology and modality extends beyond metaphor: topological operations satisfy algebraic laws corresponding exactly to characteristic modal axioms.
Provability logic gives (\Box\varphi) the interpretation that (\varphi) is provable in a specified formal theory. The resulting logic differs from ordinary metaphysical systems because formal provability obeys principles associated with Gödel’s incompleteness theorems. The modal logic (GL) replaces reflexivity-based axioms with the Löb principle,
[ \Box(\Box\varphi\rightarrow\varphi)\rightarrow\Box\varphi, ]
which formalizes Löb’s theorem.