Delta-one formula modulo ZFC (source code)

= Delta-one formula modulo ZFC
{title2=$\Delta_1^{\mathrm{ZFC}}$}

= Delta-one formulas modulo ZFC
{synonym}

A <first-order formula> is $\Delta_1$ modulo <ZFC> if that theory proves it equivalent, with the same free variables, both to a <Sigma-one formula in set theory> and to a universal unbounded quantifier block with a <bounded formula in set theory> as matrix. The theory used for provable equivalence matters: modulo <ZF> is a stronger requirement.