Soundness of the three word rules and density-preserving finite thinning

For $B_i\subseteq T_i$ and $n_i<\omega$, put ${\mathcal{C}}_i(n_i,B_i)=\{B_i\cap \{u:t{\le }_{T_i}u\}:t\in T_i(n_i)\}$. Interpret a word from left to right: $\mathrm{\exists }{A}_i$ means “there is $A_i\subseteq B_i$ that is $n_i$-dense”; $\mathrm{\forall }{x}_i$ ranges over $A_i$; $\mathrm{\forall }{a}_i$ ranges over ${\mathcal{C}}_i(n_i,B_i)$; and $\mathrm{\exists }{x}_i$ ranges over $a_i$. At the empty word assert $(x_1,\dots ,x_d)\in Q$. Let $W(\mathbf{n},\mathbf{B})$ be the resulting sentence, and let $\mathrm{\Phi }(W,\mathbf{n},p)$ say that $W(\mathbf{n},\mathbf{B})$ holds whenever every $B_i$ is $p$-dense.

If a subformula has $A_i$ only through a quantifier $\mathrm{\forall }{x}_i\in A_i$, replacing $A_i$ by $A_i^{\mathrm{\prime }}\subseteq A_i$ preserves its truth, because fewer values of $x_i$ must be checked. Repeating this argument proves simultaneous monotonicity in every such coordinate.

Rule 1 preserves the scheme: like quantifiers commute, and a witness for $\mathrm{\exists }\alpha \mathrm{\forall }\beta$ is independent of $\beta$ and therefore witnesses $\mathrm{\forall }\beta \mathrm{\exists }\alpha$. The side condition that the result lies in $L_d$ ensures that all variable domains in step 1.1 are already defined when used.

Rule 2 is pointwise valid. If $\mathrm{\forall }{a}_i\in {\mathcal{C}}_i(n_i,B_i)$ there is $x_i\in a_i$ satisfying the tail, choose one witness from each member of this one finite cone family and collect the witnesses as $A_i$; it lies in $B_i$, meets every height-$n_i$ cone, hence is $n_i$-dense, and the tail holds for all its members. Conversely, an $n_i$-dense $A_i\subseteq B_i$ meets every cone in ${\mathcal{C}}_i(n_i,B_i)$, so a member of the intersection supplies the matched existential. Finite induction supplies the finitely many witnesses and uses no choice axiom.

Consider Rule 3 with $1\le r<d$, after relabelling its permutation: $W=(\mathrm{\forall }{a}_i{)}_{i=1}^r(\mathrm{\exists }{A}_i{)}_{i=r+1}^{d}V$ and $W^{\mathrm{\prime }}=(\mathrm{\exists }{A}_i{)}_{i=r+1}^d(\mathrm{\forall }{a}_i{)}_{i=1}^{r}V$. Assume $\mathrm{\forall }\mathbf{k}\mathrm{\exists }p\mathrm{\Phi }(W,\mathbf{k},p)$. Because a $p^{\mathrm{\prime }}$-dense set is $p$-dense when $p^{\mathrm{\prime }}\ge p$, let $F(\mathbf{k})$ be the least witness exceeding every $k_i$. For fixed $\mathbf{n}$, define $G(0)={\max }_{i>r}{n}_i$ and $G(j+1)=F(n_1,\dots ,n_r,G(j),\dots ,G(j))$. This uses least natural witnesses and recursion on $\omega$, not a choice function.

Put $m={\prod }_{i=1}^r\mathrm{\mid }{T}_i(n_i)\mathrm{\mid }$ and $p_j=G(m-j)$ for $0\le j\le m$. Given $p_0$-dense $B_i$, enumerate the $m$ tuples of height-$n_i$ roots in the first $r$ trees; their associated cone tuples may repeat. Before any tuple is processed, take $A_i^0=B_i$ for $i>r$. These sets are $p_0$-dense and the preservation requirement for the empty list is vacuous.

Suppose $j<m$ cone tuples have been processed and $A_i^j\subseteq B_i$ is $p_j$-dense for every $i>r$, with the tail $V$ true for all earlier tuples. Apply $\mathrm{\Phi }(W,(n_1,\dots ,n_r,p_{j+1},\dots ,p_{j+1}),p_j)$ to the next cone tuple and to $B_1,\dots ,B_r,A_{r+1}^j,\dots ,A_d^j$. It yields $A_i^{j+1}\subseteq A_i^j$ that are $p_{j+1}$-dense and make $V$ true for the new tuple. Step 2.1 preserves all earlier instances. Finite induction gives final sets $A_i^m$ working for all cone tuples.

Since $p_m=G(0)\ge n_i$ for $i>r$, each $A_i^m$ is $n_i$-dense: extend any height-$n_i$ node to height $p_m$ and use $p_m$-density. Hence the $A_i^m$ witness the leading existential block of $W^{\mathrm{\prime }}$, and the universal block holds because step 4.1 processed every root tuple. Therefore $\mathrm{\Phi }(W^{\mathrm{\prime }},\mathbf{n},p_0)$ holds. The vector $\mathbf{n}$ was arbitrary, proving Rule 3 preserves the quantified scheme.

A derivation is finite. Apply steps 2.2, 2.3, or 5.1 successively to its rule steps; transitivity gives the displayed implication for $W{⊢}_d{W}^{\mathrm{\prime }}$.