Timeline for first-order definability transitive closure operator

4 events

when toggle format	what		by	license	comment
Mar 17, 2013 at 0:48	comment	added	Andreas Blass		That covers, in particular, the definition of $V_\alpha$ and the definition if iterated unions that leads (as in Joel's answer) to $TC$. Once one has $TC$, it can serve as the $H$ for definitions by $\in$-recursion. [Technical note: By using a definable function $H$ instead of a "predecessor" relation, I've built in the assumption that $H(x)$ is always a set, which otherwise would have to be added. Also, if $G$ and $H$ are $\Delta_1^{ZF}$-definable, then so is $F$; $\Delta_1^{ZF}$-definability cannot be replaced here with $\Delta_1^{ZF}$-definability of the predecessor relation.]
Mar 17, 2013 at 0:42	comment	added	Andreas Blass		Although "turning recursive definitions into explicit definitions may not be possible" is true, a very broad class of recursive definitions can be made explicit. Specifically, if $F$ is defined recursively by $F(x)=G(x,F\upharpoonright H(x))$ where $G$ and $H$ are definable in ZFC and where $H$ is well-founded (in the sense that every nonempty set $u$ has an element $x$ with $H(x)\cap u=\varnothing$), then $F$ admits an explicit definition in ZFC. In particular, recursions over (von Neumann) ordinals can be made explicit. [Continued in next comment]
Jun 22, 2010 at 6:45	history	edited	Philip Welch	CC BY-SA 2.5	Addition of alternate definition
Jun 21, 2010 at 9:03	history	answered	Philip Welch	CC BY-SA 2.5