Sigma-one formulas admit existential bounded matrices

A bounded formula already has the required form with an empty existential block. Rename bound variables fresh before combining normal forms. For conjunction of $\mathrm{\exists }\bar{u}\delta$ and $\mathrm{\exists }\bar{v}ϵ$, use $\mathrm{\exists }\bar{u}\bar{v}(\delta \wedge ϵ)$. For disjunction use $\mathrm{\exists }\bar{u}\bar{v}(\delta \vee ϵ)$: unused witness variables can be filled with the empty set in either true branch. An added unbounded existential joins the prefix.

A bounded existential $\mathrm{\exists }x\in a\mathrm{\exists }\bar{u}\delta$ is $\mathrm{\exists }x\bar{u}(x\in a\wedge \delta )$. To treat a bounded universal, encode a finite tuple of witnesses as a set using successive ordered pairs, whose coordinate assertions are bounded by F2. For $\mathrm{\forall }x\in a\mathrm{\exists }u\delta (x,u)$, Collection (F1) supplies a set $b$ meeting the witness class for every $x\in a$. Thus this formula implies $\mathrm{\exists }b\mathrm{\forall }x\in a\mathrm{\exists }u\in b\delta (x,u)$. Conversely any such $b$ supplies the original witnesses by dropping the bound. If $a=\mathrm{\varnothing }$, take $b=\mathrm{\varnothing }$.

The matrix in the last display is bounded, and decoding a fixed finite tuple adds only bounded quantifiers over its pair components. Induction over the closure clauses now gives the claimed normal form, in both directions at every clause. The only collection of an arbitrary family of witnesses was step 2.1, where Collection selected a bounding set rather than a choice function.