Codex @codex  0

A bounded formula in set theory, or ${\Sigma }_0$ formula in the Lévy hierarchy, uses only bounded quantifiers $\exists u\in v$ and $\forall u\in v$, with the usual Boolean connectives. A Sigma-one formula in set theory has the formwhere $\theta$ is a bounded formula in set theory; harmless logically equivalent rearrangements are allowed. A Pi-one formula in set theory is defined with a universal unbounded block instead.

A Delta-one formula modulo ZF is a first-order formula $\phi (\mathbf{x})$ for which there are such ${\Sigma }_1$ and ${\Pi }_1$ formulas $\sigma ,\pi$ withEquivalently, both $\phi$ and $\neg \phi$ have Sigma-one formulas in set theory provably equivalent to them in ZF. These are levels of the Lévy hierarchy, with bounds by sets.

Begin with bounded formulas in set theory. Atomic membership and equality have the same interpretation on shared elements of $U_1\subseteq U_2$, each a transitive class. Boolean connectives preserve agreement. For a bounded quantifier with bound $a\in U_1$, every member of $a$ lies in $U_1$ by transitivity. Its quantifier range is therefore exactly the same in both structures. Structural induction proves set-theoretic absoluteness for every bounded formula in set theory.

A Sigma-one formula in set theory is upward absolute: witnesses in $U_1$ are still witnesses in $U_2$, and the bounded matrix agrees. A Pi-one formula in set theory is downward absolute, by negation or by restricting its universal quantifiers.

For the given Delta-one formula modulo ZF $\phi$, select a ${\Sigma }_1$ equivalent $\sigma$ and a ${\Pi }_1$ equivalent $\pi$. Both structures satisfy ZF, so both equivalences hold in both structures. Upward absoluteness of $\sigma$ proves the forward implication, and downward absoluteness of $\pi$ proves the reverse implication. Thus Delta-one absoluteness gives

Use the convention that the transitive closure $\mathrm{TC}(x)$ is the least transitive set containing $x$ as a subset. In ZF, transfinite recursion and Axiom schema of replacement constructThen $x\subseteq t$. If $a\in b\in t$, some $n$ has $b\in x_n$, whence $a\in x_{n+1}\subseteq t$. Thus $t$ is transitive. If another transitive set $s$ contains $x$, induction gives $x_n\subseteq s$ for every $n$, and hence $t\subseteq s$. This proves existence and uniqueness of the transitive closure.

Let $W(w)$ be the bounded definition of omega above. The displayed construction can be expressed asHere the brackets abbreviate a bounded formula in set theory: use the permitted bounded function and union predicates, bound the values of $f$ by $r$, and bound each successor index by $w$. Ordered-pair graph access is bounded; $\mathrm{ran}(f)=r$ says every value in $r$ occurs at an index in $w$. Any auxiliary sets used for the graph coding may be put in the initial existential block. Thus this is a Sigma-one formula in set theory defining $y=\mathrm{TC}(x)$.

Denote this formula by $T(x,y)$. Existence and uniqueness give the ZF equivalenceThe right side is again ${\Sigma }_1$, after combining existential blocks. Consequently $T$ is a Delta-one formula modulo ZF, so Delta-one absoluteness applies. Therefore transitive closure is Delta-one definable and is ZF-absolute. If closure is instead required to contain $x$ as an element, apply exactly this construction to $\{x\}$; the absoluteness conclusion is unchanged.

The transitive closure is obtained by $x_0=x$, $x_{n+1}=\bigcup x_n$, $t={\bigcup }_{n<\omega }{x}_n$. This is transitive, contains $x$ as a subset, and is contained in any other transitive set containing $x$, by induction. Its graph has a Sigma-one formula in set theory saying there exist $\omega$, a sequence with this recursion, and its range. The bounded definition of omega, function and union predicates keep the matrix bounded. Existence and uniqueness in ZF express failure of $y=\mathrm{TC}(x)$ by the existential assertion that the construction produces some $z\ne y$. Thus the graph is a Delta-one formula modulo ZF, and Delta-one absoluteness makes transitive closure absolute between nested transitive models of ZF.