Solution (source code)

= Solution

A $\Sigma_1$ <logical formula> has the form
$$
\boxed{\exists z_1\cdots\exists z_n\,\psi,\qquad\psi\text{ a }\Sigma_0\text{ formula},}
$$
up to the standard logical transformations defining the hierarchy. The initial existential <quantifiers> may be unbounded; all <quantifiers> inside the matrix are bounded. A finite tuple of witnesses can be encoded by one <set> if desired, and <logical formulas> with no initial unbounded <quantifier> are included as the level-zero special case.

The dual $\Pi_1$ <class in set theory> has an initial universal block with a bounded matrix. Negation interchanges these two classes, but does not in general preserve the existential <class in set theory>. Part (iii) supplies an explicit reason for the failure in this setting.