First-Order Modal Logic

Origin. Carnap, Kripke (1960s). Quantifiers meet modalities. Varying domains. Rigid vs non-rigid designators. Foundation for quantified intensional logic.

Models. Possible worlds with domains. Constant vs varying domains. Rigid designators: same object across worlds. Actualist vs possibilist quantification.

Formalism.

Syntax: φ ::= P(t₁,...,tₙ) | ¬φ | φ ∧ ψ | □φ | ∀x.φ

Kripke semantics: M = (W, R, D, d, I) W: worlds, R: accessibility D: total domain or D: W → domains d: world-relative domains I: interpretation at worlds

Constant domains: Same objects at all worlds. Barcan formula: ∀x□φ → □∀x.φ Converse Barcan: □∀x.φ → ∀x□φ

Varying domains: d(w): objects existing at w. Barcan fails. Actualist: quantify over d(w). Possibilist: quantify over D.

Rigid designators: I(c, w) = I(c, v) for all w, v. Names refer to same object. Kripke's argument.

De re vs de dicto: □∃x.Fx: de dicto (necessarily, something) ∃x.□Fx: de re (something necessarily) Scope matters.

Problems: Transworld identity. Contingent existence. Substitutivity failures.

Actualist quantification: ∀x.φ true at w iff φ[a/x] true for all a ∈ d(w). Existential import.

Symbols.

Metatheory. Kripke (1959) proved completeness for constant-domain quantified S5, where the Barcan formula is valid; Kripke (1963) gave the varying-domain semantics on which BF fails. The two Barcan schemas are conditions on domains rather than on accessibility: BF ∀x□φ → □∀x.φ is valid on a frame exactly when domains decrease along R, and CBF □∀x.φ → ∀x□φ exactly when they increase, so constant domains validate both and neither is available on arbitrary varying-domain models. Adding equality with rigid terms makes the necessity of identity x = y → □(x = y) a theorem, derivable from Leibniz's law together with □(x = x). Decidability is lost at once: Kripke (1962) proved monadic first-order modal logic undecidable, though classical monadic predicate logic is decidable (Löwenheim, 1915). Decidable and axiomatizable fragments must bound the free variables under a modal operator — the monodic fragments of Wolter and Zakharyaschev, in which □ applies only to formulas with at most one free variable — and the one-variable constant-domain fragment of QL is the product L × S5, hence NEXPTIME-complete when L is S5. Craig interpolation fails for most quantified modal logics, including QS4 and QS5 (Fine, 1979).

Applies to. Metaphysics. Semantics. Ontology. Necessary existence. Intensional contexts.

Limitations. Every fragment large enough to be interesting is undecidable, monadic predicates already sufficing, so there is no decision procedure and no finite model property to fall back on. The domain choice is forced and each option costs something: constant domains validate both Barcan schemas and make ∀x□∃y(y = x) a theorem, so nothing exists contingently; varying domains falsify the classical instantiation rule ∀x.φ → φ(t) whenever t denotes nothing at the world of evaluation, forcing a free logic with an explicit existence predicate. Rigidity is stipulated rather than derived, and with non-rigid terms substitutivity of identicals fails inside □. Because the necessity of identity follows from Leibniz's law alone, the formalism settles a metaphysical dispute instead of representing it, and transworld identity itself is left as an unconstrained primitive. Craig interpolation fails (Fine, 1979).

© 2026 Lingenic LLC