= Solution
Write $H(\vec v)$ for the proposed stage-comparison <logical formula> and fix a standard <tuple> $\vec a$. If $\vec a\in A$, <numeralwise enumeration in arithmetic> supplies a standard $m$ with $S\vdash F(\bar{\vec a},\bar m)$. Disjointness gives $\vec a\notin B$, so $S\vdash\neg G(\bar{\vec a},\bar j)$ for every standard $j$, in particular $j=0,\ldots,m$. The source's finite initial-segment axiom combines this finite list into
$$
S\vdash\forall y\le\bar m\,\neg G(\bar{\vec a},y).
$$
Use $\bar m$ as the <existential witness> to obtain $S\vdash H(\bar{\vec a})$.
If instead $\vec a\in B$, choose $n$ with $S\vdash G(\bar{\vec a},\bar n)$. Disjointness gives refutations of $F(\bar{\vec a},\bar j)$ for all $j$, so the finitely many $j\le n$ give
$$
S\vdash\forall x\le\bar n\,\neg F(\bar{\vec a},x).
$$
For an arbitrary $x$, the source's comparison axiom gives $x\le\bar n$ or $\bar n\le x$. In the first case the first conjunct of the proposed witness condition is false. In the second case $y=\bar n$ witnesses failure of its bounded universal conjunct, since $G(\bar{\vec a},\bar n)$ is provable. Generalization over $x$ therefore gives $S\vdash\neg H(\bar{\vec a})$.
Thus \b[the <logical formula> separates $A$ from $B$]. The <formal proof> uses the enumerators' numeralwise positive and negative <formal proof> properties and the two explicit order principles supplied in the source; it does not assume the <first-order theory> can decide arbitrary unbounded existential <logical formulas>.
Back to article page
