Forcing relation for all formulas

In ZF fix a nonempty forcing preorder P. Start with the atomic relations in Atomic forcing is well-founded and definable. For each fixed finite membership formula, use its syntax from Terms and formulas as finite set codes to extend forcing by

$p⊩(\psi \wedge \theta )(\vec{\tau })⟺(p⊩\psi (\vec{\tau })\wedge p⊩\theta (\vec{\tau })),$ $p⊩\mathrm{\neg }\psi (\vec{\tau })⟺\mathrm{\nexists }q\le p(q⊩\psi (\vec{\tau })),$ $p⊩\mathrm{\exists }x\psi (x,\vec{\tau })⟺\mathrm{\forall }q\le p\mathrm{\exists }r\le q\mathrm{\exists }\text{ P-name }\sigma (r⊩\psi (\sigma ,\vec{\tau }))\mathrm{.}$

Boolean and universal abbreviations expand using negation, conjunction and existential quantification. Substitution is capture-avoiding, with bound variables renamed as necessary; pure membership terms are variables.

This is an external induction on a fixed finite formula. If its subformula forcing relations are definable, each displayed clause is a first-order formula: quantification over names is restricted by the definable namehood predicate. Separation on P forms the set of conditions having some name witness, despite the absence of a set of all names. Thus the clauses define one predicate for each formula, rather than a single satisfaction predicate uniformly ranging over all formulas of the universe.

In a transitive ZF ground model M, interpret every clause internally and denote the result by ${⊩}^M$. In particular the existential name ranges over M's names. Only the atomic relation is asserted to agree with the external recursion; the quantified forcing relations need not agree between different ground models. Existential forcing requires dense witnesses and makes no maximal-antichain selection and no assertion of one globally selected witnessing name. No AC is assumed.