Least witness ranks give choice-free bounds

For each existential matrix ${\psi }_i(y,\bar{x})$ define $r_i(\bar{x})=0$ when no witness exists, and otherwise let it be the least rank of a witness. F1 supplies that least ordinal and a witness at that rank. Because the list of formulas is fixed externally, this is a separate definable function for each $i$, with no appeal to truth for arbitrary formulas.

The union of the finitely many sets of parameter tuples from $V_{\alpha }$ is a set, including a singleton empty tuple for a sentence. Replacement collects all $r_i(\bar{a})$ in a set $R_{\alpha }$. Put $b(\alpha )=\sup (R_{\alpha }\cup \{\alpha \})+1$. Then $b(\alpha )>\alpha$ and every required least-rank witness has rank below $b(\alpha )$; by F2 it lies in $V_{b(\alpha )}$. No particular witness has been selected as a function of the tuple.

For $W$, replace least witness rank by the least stage containing a witness in $W$ whose matrix holds relativized to $W$. Exhaustion gives such a stage; it has a least value by the well-order of ordinals. Replacement over tuples in $W_{\alpha }$ and the same successor-supremum formula give $b(\alpha )$. By monotonicity, for every true instance at least one witness lies in $W_{b(\alpha )}$; witnesses of larger rank need not lie there. With no existential formulas or no true instances, the same formula still gives a bound above $\alpha$.