Atomic forcing relation

Work in ZF with a nonempty forcing preorder $P$, with $q\le p$ meaning that q is stronger. Names have the coordinates $(\text{name},\text{condition})$ and rank convention of Forcing names and their rank. Write $q\perp s$ for incompatibility. Density, nonempty filters and ground-model genericity have the conventions of Dense open sets and generic filters over a model.

For names $\sigma ,\tau$, the following clauses specify atomic forcing:

$p⊩\sigma \subseteq \tau ⟺\mathrm{\forall }⟨u,s⟩\in \sigma \mathrm{\forall }q\le p,s\mathrm{\exists }r\le q\mathrm{\exists }⟨v,t⟩\in \tau (r\le t\wedge r⊩u=v)\mathrm{.}$

Here $q\le p,s$ abbreviates $q\le p$ and $q\le s$; if there is no such q the corresponding requirement is vacuous. Define

$p⊩\sigma =\tau ⟺(p⊩\sigma \subseteq \tau \wedge p⊩\tau \subseteq \sigma ),$ $p⊩\sigma \in \tau ⟺\mathrm{\forall }q\le p\mathrm{\exists }r\le q\mathrm{\exists }⟨v,t⟩\in \tau (r\le t\wedge r⊩\sigma =v)\mathrm{.}$

Subset is an auxiliary clause, not an additional symbol in the membership language. In the equality clause, substituting the displayed subset clauses leaves only equality calls on two proper subnames. First solve that rank recursion, then define auxiliary subset and membership by the displays. Atomic forcing is well-founded and definable ↗ proves that this prescription exists, is unique and is definable. No largest condition is required.

For a transitive ZF ground model M containing P, ${⊩}^M$ denotes the internally defined relation. The clauses do not quantify over generic filters or assume their existence. Their semantic relation to the valuation in Valuation of names and M[G] is proved later. Empty names are allowed: an empty left subset clause is vacuous, whereas no condition forces membership in the empty name.