Quantified Modal Logic and the Barcan Formulas

Propositional modal logic asks what follows from what when sentences can be necessary. Adding quantifiers asks a harder question, because a quantifier ranges over a domain and a modal operator shifts the world, and nothing in either apparatus settles whether the domain shifts too.

The formal choice is small and the consequences are metaphysical. This article sets out the choice, the formulas that track it, and the one result in the area that almost everyone accepts and few find comfortable.

The two semantics

Variable domains are the natural formalisation of the thought that things might not have existed. There are no talking donkeys, there might have been, so some world contains an object no world of ours does. Constant domains say instead that the objects are fixed and what varies is which of them are concrete, or instantiated, or actual, so that the possible talking donkey exists at our world too and simply is not a donkey here.

Each choice validates a formula the other does not, and the formulas were identified before the semantics that explains them.

The Barcan formulas

Ruth Barcan Marcus introduced the first as an axiom in 1946, in the earliest axiomatisation of quantified modal logic, before Kripke semantics existed to explain what it meant. The semantic characterisation came later and is exact: constant domain models validate both, and validating both forces the domains accessible from any world to be identical to it.

The converse formula is the awkward one, because it is very nearly forced. From $\forall x\, \varphi \rightarrow \varphi[t/x]$ and necessitation one obtains $\Box(\forall x\, \varphi \rightarrow \varphi)$, and distribution gives $\Box \forall x\, \varphi \rightarrow \Box \varphi$, and generalising yields the converse Barcan formula. Every step is standard. Rejecting the conclusion therefore requires rejecting one of them, and the usual casualty is the quantifier axiom, replaced by a version carrying an existence assumption. That move is free logic, and the fact that variable domain semantics needs it is the clearest case of a metaphysical position forcing a change to the underlying logic rather than merely to the axioms added on top.

The necessity of identity

One result in this area is a theorem rather than a stipulation, and it constrains any position in the debate.

The derivation is three lines. Identity is reflexive, so $a = a$, and by necessitation $\Box\, a = a$. Suppose $a = b$. By Leibniz's law, whatever holds of $a$ holds of $b$, and what holds of $a$ is the property of being necessarily identical to $a$. Hence $\Box\, a = b$.

The conclusion is not a claim about names. Barcan Marcus drew the distinction in 1961 and Kripke pressed it in 1970: the theorem says that the objects, however designated, are necessarily identical, and it is compatible with a competent speaker's not knowing that Hesperus is Phosphorus. Epistemic possibility is not metaphysical possibility, and the sentence "Hesperus might not have been Phosphorus" is true only on the epistemic reading. The framework that makes this available is the theory of rigid designation, on which a name picks out the same object at every world at which it picks out anything, and the contingency of a discovery attaches to the descriptions used rather than to the identity discovered.

The necessity of distinctness follows by a similar argument, and the necessity of self-identity is what starts it. What does not follow is the necessity of any other kind of identification, and in particular the theorem tells one nothing about whether a statue is identical to its clay.

Next

Every system so far has been normal: closed under necessitation and validating distribution. Both closure conditions can be questioned, and the systems that drop them were the first modal logics to be studied. Their semantics is not the relational one.