What assumptions are required to treat alethic boxes and diamonds as quantifiers over worlds

Short answer first

To treat alethic □ and ◇ as quantifiers over worlds you need to adopt Kripke-style semantics (or an equivalent two-sorted first-order semantics) and make a number of technical and philosophical assumptions about (i) what worlds are, (ii) how □/◇ are evaluated, and (iii) how object-quantification interacts with world-variation. Roughly:

assume a nonempty set $W$ of possible worlds and an accessibility relation $R\subseteq W\times W$;
evaluate formulas relative to a world $w\in W$ (truth-at-a-world semantics);
interpret propositional atoms as sets of worlds (or predicates over a world-sort);
define

$$ w\models \Box\varphi\quad\text{iff}\quad\forall v\in W,(R(w,v)\Rightarrow v\models\varphi), $$

$$ w\models \Diamond\varphi\quad\text{iff}\quad\exists v\in W,(R(w,v)\land v\models\varphi), $$

which is literally treating □ as a universal quantifier and ◇ as an existential quantifier over the $R$-accessible worlds of $w$.

Below I unpack those assumptions and their consequences (including the issues that arise in first-order modal logic).

1. The minimal formal assumptions (propositional modal logic)

If you only care about modal propositional logic, the assumptions are straightforward:

Worlds and accessibility: A Kripke frame $(W,R)$ where $W\neq\varnothing$ and $R\subseteq W\times W$.
Valuation: A valuation $V:\text{Prop}\to\mathcal P(W)$ assigning each atomic proposition the set of worlds where it is true.
Truth-at-a-world: The recursive clause above for □ and ◇. This is the claim “□ = ∀ (over accessible worlds), ◇ = ∃ (over accessible worlds)”.
Logical axioms/rules: If you want to recover familiar modal systems syntactically you also adopt e.g. K (distribution) and necessitation; frame properties of $R$ correspond to extra axioms (T, 4, 5, D, B etc.).

So, in propositional modal logic nothing mystical is required: □ and ◇ are literally defined as universal and existential quantification over accessible worlds.

2. Additional assumptions for first-order/modal hybrid readings

When you move to quantified modal logic (first-order modal logic), several extra assumptions matter because you now have object-quantifiers (∃x, ∀x) and modal operators.

(a) Two ways to formalize: standard translation / two-sorted FOL

You can translate modal formulas into a two-sorted first-order language with a world-sort and an object-sort:

Predicates become relations $P(w,x_1,\dots,x_n)$.
$\Box\varphi$ becomes $\forall v,(R(w,v)\rightarrow \text{ST}_v(\varphi))$.

So treating □ as a quantifier over worlds presupposes that you accept a metalanguage (or a two-sorted object language) where worlds are objects that can be quantified over.

(b) Domain assumptions (constant vs varying domains)

How object quantifiers interact with □/◇ depends crucially on whether you assume:

Constant domain semantics: Each world has the same domain $D$ of individuals. Under constant domains you can pull ∃ out/into modalities in certain ways; Barcan and converse-Barcan formulas become valid.
Varying domain semantics: Each world $w$ has domain $D_w$. Then $\exists x\Diamond P(x)$ vs $\Diamond\exists x P(x)$ behave differently and the Barcan formulas may fail.

The Barcan formula (BF) and its converse (CBF) illustrate this interaction:

BF: $\Box\forall x,\varphi(x)\to\forall x,\Box\varphi(x)$.
CBF: $\forall x,\Box\varphi(x)\to\Box\forall x,\varphi(x)$.

These are valid under particular domain/frame assumptions (constant domains, or certain monotonicity conditions), so an assumption about domains is needed if you want to treat modal operators as "world-quantifiers" that commute with object quantifiers.

(c) Rigidity of terms / names

If names are rigid designators (they denote the same object in every world), some interactions are simpler. If names are non-rigid, de re vs de dicto distinctions appear: e.g. $\exists x\Box P(x)$ (de re) versus $\Box\exists x P(x)$ (de dicto) are not interchangeable under varying domains or non-rigid designation. So you must assume something about term-rigidity if you want a clean quantifier interpretation.

3. Philosophical/ontological assumptions

To treat modal operators as quantifiers over worlds you also implicitly accept some metaphysical views:

Possible-world realism (or at least a semantics that reifies worlds): worlds are entities (abstract/concrete) that can be quantified over in the meta/theory (or in a two-sorted object language).
Accessibility as modal relevance: the $R$ relation captures the relevant modal notion (logical possibility, physical possibility, epistemic accessibility, etc.). Different choices of $R$ correspond to different modal notions.
World-indexing of truth: truth is evaluated relative to worlds; necessity = truth at all relevant worlds.

If you reject the reification of worlds (e.g. prefer an assertion-based, proof-theoretic, or substitutional account), then you cannot literally treat □ as a quantifier over worlds without moving to a more elaborate reconstruction.

4. What additional axioms correspond to which frame properties

If you want specific modal axioms to hold you must assume corresponding properties of $R$:

K (distribution) — built into Kripke semantics.
T ($\Box p\to p$) — reflexivity of $R$.
4 ($\Box p\to\Box\Box p$) — transitivity.
B — symmetry.
D ($\Box p\to\Diamond p$) — seriality.
S5 (all worlds mutually accessible) — $R$ universal (so □ becomes ∀ over all worlds, not just R-accessible).

So “□ as ∀” is sensitive to what set you quantify over: all worlds or just $R$-accessible ones. To treat □ as quantifying over all worlds you assume $R$ is universal (S5).

5. Standard translation (formal recipe)

For clarity, the standard translation $ST_w$ from modal formula $\varphi$ to first-order formula with a world variable $w$:

$ST_w(p) = P(w)$ for atomic $p$.
$ST_w(\lnot\varphi) = \lnot ST_w(\varphi)$.
$ST_w(\varphi\land\psi) = ST_w(\varphi)\land ST_w(\psi)$.
$ST_w(\Box\varphi) = \forall v,(R(w,v)\rightarrow ST_v(\varphi))$.
$ST_w(\Diamond\varphi) = \exists v,(R(w,v)\land ST_v(\varphi))$.

This makes explicit how □/◇ are replaced by first-order quantifiers over the world variable $v$.

6. Summary checklist of required assumptions (compact)

If you want to treat alethic □/◇ as quantifiers over worlds, you should adopt:

A Kripke framework: nonempty set $W$ of worlds + accessibility $R$.
Truth-at-a-world semantics (evaluation index $w\in W$).
Valuation of atomic formulas as sets (or predicates) of worlds.
The clause $w\models\Box\varphi\iff\forall v(R(w,v)\to v\models\varphi)$ (and dually for ◇).
For first-order modal logic: an account of domains (constant vs varying) and of term rigidity; choose whether Barcan and converse-Barcan hold.
(If you want particular modal axioms) impose frame conditions on $R$ (reflexive, transitive, serial, symmetric, universal, …).
(Philosophically) accept worlds as entities (or use two-sorted translation to simulate that).

7. Short note on alternatives and pitfalls

If you prefer a substitutional or proof-theoretic account, you cannot simply treat □/◇ as world-quantifiers without significant translation work.
Treating □ as ∀ over worlds is semantically simple but hides tricky de re/de dicto issues once you introduce object-quantifiers, rigid designators, and varying domains. The Barcan formulas are the canonical place where these issues surface.

If you want, I can (a) show the standard translation of a few example formulas (including how the Barcan formula looks under ST), (b) show which domain assumptions validate the Barcan / converse-Barcan formulas, or (c) sketch the philosophical options for what “worlds” are (abstract vs concrete vs ersatz). Which of those would be most useful?

Thiago’s ChatGPT Blog

Friday, August 29, 2025

Alethic modals as world-quantifiers