Modal logic, narrowly conceived, is the study of principles of reasoning involving necessity and possibility. More broadly, it encompasses a number of structurally similar inferential systems. In this sense, deontic logic (which concerns obligation, permission and related notions) and epistemic logic (which concerns knowledge and related notions) are branches of modal logic. Still more broadly, modal logic is the study of the class of all possible formal systems of this nature.
It is customary to take the language of modal logic to be that obtained by adding one-place operators ‘□’ for necessity and ‘◇’ for possibility to the language of classical propositional or predicate logic. Necessity and possibility are interdefinable in the presence of negation:
□A↔¬◊¬A and
◊A↔¬□¬A
hold. A modal logic is a set of formulas of this language that contains these biconditionals and meets three additional conditions: it contains all instances of theorems of classical logic; it is closed under modus ponens (that is, if it contains A and A→B it also contains B); and it is closed under substitution (that is, if it contains A then it contains any substitution instance of A; any result of uniformly substituting formulas for sentence letters in A). To obtain a logic that adequately characterizes metaphysical necessity and possibility requires certain additional axiom and rule schemas:
K □(A→B)→(□A→□B)
T □A→A
5 ◊A→□◊A
Necessitation A/□A.
By adding these and one of the □–◇ biconditionals to a standard axiomatization of classical propositional logic one obtains an axiomatization of the most important modal logic, S5, so named because it is the logic generated by the fifth of the systems in Lewis and Langford’s Symbolic Logic (1932). S5 can be characterized more directly by possible-worlds models. Each such model specifies a set of possible worlds and assigns truth-values to atomic sentences relative to these worlds. Truth-values of classical compounds at a world w depend in the usual way on truth-values of their components. □A is true at w if A is true at all worlds of the model; ◇A, if A is true at some world of the model. S5 comprises the formulas true at all worlds in all such models. Many modal logics weaker than S5 can be characterized by models which specify, besides a set of possible worlds, a relation of ‘accessibility’ or relative possibility on this set. □A is true at a world w if A is true at all worlds accessible from w, that is, at all worlds that would be possible if w were actual. Of the schemas listed above, only K is true in all these models, but each of the others is true when accessibility meets an appropriate constraint.
The addition of modal operators to predicate logic poses additional conceptual and mathematical difficulties. On one conception a model for quantified modal logic specifies, besides a set of worlds, the set Dw of individuals that exist in w, for each world w. For example, ∃x□A is true at w if there is some element of Dw that satisfies A in every possible world. If A is satisfied only by existent individuals in any given world ∃x□A thus implies that there are necessary individuals; individuals that exist in every accessible possible world. If A is satisfied by non-existents there can be models and assignments that satisfy A, but not ∃xA. Consequently, on this conception modal predicate logic is not an extension of its classical counterpart.
The modern development of modal logic has been criticized on several grounds, and some philosophers have expressed scepticism about the intelligibility of the notion of necessity that it is supposed to describe.
Well-definedness and observational equivalence for inductive–coinductive programs