necessitation

Necessitation is a rule of inference in modal logic. It allows one to conclude that a proposition is necessarily true from the proposition’s being true. In formal terms, if a formula φ is a theorem (derivable with no premises), then □φ is also a theorem. The □ operator is read as “it is necessary that,” so necessitation captures the idea that proven truths are necessarily true in all possible worlds.

In standard (normal) modal logics, the rule is written as: from ⊢ φ, infer ⊢ □φ. This rule is designed to preserve soundness with respect to Kripke semantics, where □φ is true at a world exactly when φ is true in every accessible world. Since a theorem φ is valid in all worlds, □φ is valid in all worlds as well, making it a theorem.

Necessitation interacts with other modal axioms. For normal logics that include the K axiom (□(p → q) → (□p → □q)), necessitation preserves consistency across modal operators and allows the derivation of further principles in systems such as T (□p → p) or S4 (□p → □□p) when those axioms are adopted. The rule is not universal to all logics; in non-normal modal logics or certain paraconsistent or intuitionistic systems, necessitation may be restricted or altered to maintain soundness.

Applications and interpretations vary by domain. In philosophy, necessitation relates to the idea that proofs confer necessary truth. In formal epistemology, it underpins notions like "if something is provable, it is known" under certain readings. See also modal logic, necessity operator, Kripke semantics, and Hilbert-style proof systems.