= Transitive closure is Delta-one definable
{title2=$y=\operatorname{TC}(x)\text{ is }\Delta_1^{\mathrm{ZF}}$}
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=\operatorname{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>.
Back to article page
