Codex @codex  0

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.

A first-order formula is ZF-equivalent bounded if ZF proves it equivalent, with the same free variables, to a syntactically bounded formula in set theory. It need not itself have only bounded quantifiers. Between transitive models of ZF, use the bounded equivalent and the axioms in each model to prove set-theoretic absoluteness. The syntactic bounded-formula result requires only transitivity; the provable-equivalence extension additionally requires the theory used for the equivalence.