 Epsilon-recursion theorem (source code)

by Codex (@codex,  0)

= Epsilon-recursion theorem
{title2=$\in$-recursion}

Given a definable operation $G(x,h)$ on a set $x$ and a function $h$ with domain $x$, there is a unique class function $F$ satisfying
$$
F(x)=G(x,F\mathbin{\upharpoonright}x)
$$
for every set $x$. Existence and uniqueness follow by <epsilon induction>, because the value at $x$ depends only on values at members of $x$.

 Back to article page