Sigma-one formula in set theory (source code)

= Sigma-one formula in set theory
{title2=$\Sigma_1$}

= Sigma-one formulas in set theory
{synonym}

A <first-order formula> is syntactically $\Sigma_1$ when it is an unbounded existential quantifier block followed by a <bounded formula in set theory>. Equivalence provable in a specified theory gives the corresponding modulo-theory notion. Existential witnesses show upward absoluteness between <transitive models> containing the parameters.