Proof of The Recursion Theorem on Omega

Throughout, every element of a class is a set by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §objects. Membership in a class formed by class abstraction is unfolded by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted; class abstractions are unfolded without further mention. For a function $F$ and $u\in\operatorname{dom}F$, $F(u)$ is the unique set $v$ with $(u,v)\in F$, by Functions, Values of a Function, and Functions from One Class to Another §value; in particular, if $F$ is a function, $(u,v)\in F$ implies $v=F(u)$. By The Successor of a Set §successor, for all sets $u$ and $x$,

$$u\in S(x)\quad\text{if and only if}\quad u\in x\ \text{or}\ u=x.\qquad(\mathrm{S})$$

Preliminaries on $S(n)$. Let $n\in\omega$. Then $S(n)\in\omega$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §inductive, so every element of $S(n)$ lies in $\omega$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §omega-transitive, and $n\in S(n)$ by $(\mathrm{S})$. Moreover:

(P1) $0\in S(n)$: by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §zero-least, $0\le n$, so $0<S(n)$ by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §successor; as $0\in\omega$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §inductive, $0\in S(n)$ by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §segment, applied to $S(n)$.

(P2) If $k$ is a set with $S(k)\in S(n)$, then $k\in S(n)$ and $k\in\omega$: indeed $k\in S(k)$ by $(\mathrm{S})$, so $k\in S(n)$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §element-transitive, applied to $S(n)\in\omega$, and $k\in\omega$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §omega-transitive.

(P3) $m\notin m$ for every $m\in\omega$: if $m\in m$, then $m<m$ by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §segment, which by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §strict requires $m\neq m$.

Attempts. For $n\in\omega$, a set $h$ is an $n$-attempt if $h$ is a map $h:S(n)\to a$ with $h(0)=c$ and $h(S(k))=g(k,h(k))$ for every set $k$ with $S(k)\in S(n)$. These values exist: $0\in S(n)=\operatorname{dom}h$ by (P1); for $S(k)\in S(n)$, (P2) gives $k\in\operatorname{dom}h$ and $k\in\omega$, and $h(k)\in\operatorname{ran}h\subseteq a$ by Relations, Domain, Range, Inverse and Composition §range and Functions, Values of a Function, and Functions from One Class to Another §map, so $(k,h(k))\in\omega\times a=\operatorname{dom}g$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership. "$h$ is an $n$-attempt" is a predicative formula in the set variables $h$ and $n$ with the parameters $a$, $c$ and $g$: being a function, $\operatorname{dom}h=S(n)$ and $\operatorname{ran}h\subseteq a$ unfold by Functions, Values of a Function, and Functions from One Class to Another §function, Relations, Domain, Range, Inverse and Composition §relation, Relations, Domain, Range, Inverse and Composition §domain, Relations, Domain, Range, Inverse and Composition §range and Subclasses and Subsets §subclass into formulas quantifying over set variables only, and the two value conditions may be written as $(0,c)\in h$ and $\forall k\,\forall u\,\forall w\,((S(k)\in S(n)\wedge(k,u)\in h\wedge((k,u),w)\in g)\Rightarrow(S(k),w)\in h)$, which are equivalent to them for a map $h:S(n)\to a$ by Functions, Values of a Function, and Functions from One Class to Another §value. Here $0$, $S(\cdot)$ and the ordered pair are defined set symbols, by The Empty Set, the Unordered Pair and the Singleton §empty, The Successor of a Set §successor and The Ordered Pair of Two Sets and Nested Tuples §pair. The same holds for every class formed below, so all of them are predicative as Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §comprehension requires.

(i) Agreement. Let $h$ be an $n$-attempt and $h'$ an $n'$-attempt. Let $D=\{k\in\omega:(k\in S(n)\wedge k\in S(n'))\Rightarrow h(k)=h'(k)\}$, formed with the parameters $\omega$, $n$, $n'$, $h$ and $h'$; the values are used properly, under the antecedent. Then $0\in D$, since $h(0)=c=h'(0)$. Let $k\in\omega$ with $k\in D$, and suppose $S(k)\in S(n)$ and $S(k)\in S(n')$. By (P2), $k\in S(n)$ and $k\in S(n')$, so $h(k)=h'(k)$ since $k\in D$, and therefore $h(S(k))=g(k,h(k))=g(k,h'(k))=h'(S(k))$. As $S(k)\in\omega$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §inductive, $S(k)\in D$. By Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §induction, $\omega\subseteq D$. Since the elements of $S(n)$ lie in $\omega$, $h(k)=h'(k)$ for every set $k$ with $k\in S(n)$ and $k\in S(n')$.

(ii) Existence of attempts. Let $E=\{n\in\omega:\exists h\,(h\text{ is an }n\text{-attempt})\}$, with $h$ a set variable.

Base. Let $h_{0}=\{(0,c)\}$, a set by The Empty Set, the Unordered Pair and the Singleton §singleton, whose only element is $(0,c)$. It is a relation, and if $(u,v),(u,v')\in h_{0}$, then both equal $(0,c)$, so $v=c=v'$ by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic; so $h_{0}$ is a function by Functions, Values of a Function, and Functions from One Class to Another §function. By Relations, Domain, Range, Inverse and Composition §domain, Relations, Domain, Range, Inverse and Composition §range and The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic, the only element of $\operatorname{dom}h_{0}$ is $0$ and the only element of $\operatorname{ran}h_{0}$ is $c\in a$. Since $0$ has no element by The Empty Set, the Unordered Pair and the Singleton §empty, $(\mathrm{S})$ shows that the only element of $S(0)$ is $0$, so $\operatorname{dom}h_{0}=S(0)$ by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality, and $\operatorname{ran}h_{0}\subseteq a$; thus $h_{0}:S(0)\to a$ by Functions, Values of a Function, and Functions from One Class to Another §map, and $h_{0}(0)=c$. If $S(k)\in S(0)$, then $S(k)=0$, contrary to Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §successor-nonzero; so the successor condition holds vacuously, $h_{0}$ is a $0$-attempt, and $0\in E$ (with $0\in\omega$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §inductive).

Step. Let $n\in\omega$ with $n\in E$, and let $h$ be an $n$-attempt. Since $n\in S(n)=\operatorname{dom}h$ and $n\in\omega$, $h(n)\in a$ and $w=g(n,h(n))$ exists, as in the paragraph on attempts, with $w\in\operatorname{ran}g\subseteq a$ by Relations, Domain, Range, Inverse and Composition §range and Functions, Values of a Function, and Functions from One Class to Another §map. Let $h^{*}=h\cup\{(S(n),w)\}$, a set by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper §binary-union; by The Boolean Operations on Classes, Disjointness, and the Universal Class §operations and The Empty Set, the Unordered Pair and the Singleton §singleton, $p\in h^{*}$ if and only if $p\in h$ or $p=(S(n),w)$. Every element of $h^{*}$ is an ordered pair, so $h^{*}$ is a relation. Let $(u,v),(u,v')\in h^{*}$. If both lie in $h$, then $v=v'$. If both equal $(S(n),w)$, then $v=w=v'$ by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic. If one lies in $h$ and the other equals $(S(n),w)$, then $u=S(n)$ by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic and $u\in\operatorname{dom}h=S(n)$ by Relations, Domain, Range, Inverse and Composition §domain, so $S(n)\in S(n)$, contrary to (P3) since $S(n)\in\omega$. So $h^{*}$ is a function. By Relations, Domain, Range, Inverse and Composition §domain and The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic, a set $u$ lies in $\operatorname{dom}h^{*}$ if and only if $u\in\operatorname{dom}h=S(n)$ or $u=S(n)$, that is, by $(\mathrm{S})$, if and only if $u\in S(S(n))$; so $\operatorname{dom}h^{*}=S(S(n))$ by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality. Likewise every element of $\operatorname{ran}h^{*}$ lies in $\operatorname{ran}h\subseteq a$ or equals $w\in a$, so $h^{*}:S(S(n))\to a$ by Functions, Values of a Function, and Functions from One Class to Another §map. For $u\in S(n)$, $(u,h(u))\in h\subseteq h^{*}$, so $h^{*}(u)=h(u)$; and $h^{*}(S(n))=w$. Hence $h^{*}(0)=h(0)=c$, using (P1). Let $k$ be a set with $S(k)\in S(S(n))$; by $(\mathrm{S})$, $S(k)\in S(n)$ or $S(k)=S(n)$. In the first case $k\in S(n)$ by (P2), so $h^{*}(S(k))=h(S(k))=g(k,h(k))=g(k,h^{*}(k))$. In the second case $k=n$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §successor-injective, so $h^{*}(S(k))=w=g(n,h(n))=g(k,h^{*}(k))$, since $n\in S(n)$. Thus $h^{*}$ is an $S(n)$-attempt, and $S(n)\in E$ as $S(n)\in\omega$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §inductive.

By Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §induction, $\omega\subseteq E$: for every $n\in\omega$ there is an $n$-attempt.

(iii) Construction. Let $f=\{p:\exists n\,\exists h\,(n\in\omega\wedge h\text{ is an }n\text{-attempt}\wedge p\in h)\}$, formed with the parameters $\omega$, $a$, $c$ and $g$; $n$ and $h$ are set variables.

$f$ is a map. Each element of $f$ lies in some attempt, which is a relation, so $f$ is a relation. Let $(u,v),(u,v')\in f$, say $(u,v)\in h$ for an $n$-attempt $h$ and $(u,v')\in h'$ for an $n'$-attempt $h'$. Then $u\in\operatorname{dom}h=S(n)$ and $u\in\operatorname{dom}h'=S(n')$ by Relations, Domain, Range, Inverse and Composition §domain, $v=h(u)$ and $v'=h'(u)$, so $v=v'$ by (i); thus $f$ is a function. If $u\in\operatorname{dom}f$, then $u\in S(n)$ for some $n\in\omega$ as just seen, so $u\in\omega$. Conversely, for $u\in\omega$, (ii) gives a $u$-attempt $h$, and $u\in S(u)=\operatorname{dom}h$, so $(u,h(u))\in h\subseteq f$ and $u\in\operatorname{dom}f$. Hence $\operatorname{dom}f=\omega$ by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality. If $v\in\operatorname{ran}f$, then $(u,v)\in h$ for some attempt $h$, so $v\in\operatorname{ran}h\subseteq a$. So $f:\omega\to a$ by Functions, Values of a Function, and Functions from One Class to Another §map.

$f$ extends every attempt. If $h$ is an $n$-attempt and $u\in S(n)$, then $(u,h(u))\in h\subseteq f$, so $f(u)=h(u)$. Call this $(\mathrm{E})$.

Recursion equations. By (ii) there is a $0$-attempt $h$, and $0\in S(0)$, so $f(0)=h(0)=c$ by $(\mathrm{E})$. Let $n\in\omega$. Then $S(n)\in\omega$, and by (ii) there is an $S(n)$-attempt $h$. Since $S(n)\in S(S(n))$ by $(\mathrm{S})$, the successor condition with $k=n$ gives $h(S(n))=g(n,h(n))$, and $n\in S(S(n))$ by (P2), applied to $S(n)\in\omega$. By $(\mathrm{E})$, $f(S(n))=h(S(n))$ and $f(n)=h(n)$, so $f(S(n))=g(n,f(n))$.

(iv) Uniqueness. Let $f':\omega\to a$ be a map with $f'(0)=c$ and $f'(S(n))=g(n,f'(n))$ for every $n\in\omega$. Let $U=\{n\in\omega:f(n)=f'(n)\}$, formed with the parameters $\omega$, $f$ and $f'$; the values are used properly since $\operatorname{dom}f=\operatorname{dom}f'=\omega$. Then $0\in U$, since $f(0)=c=f'(0)$. If $n\in\omega$ and $n\in U$, then $f(S(n))=g(n,f(n))=g(n,f'(n))=f'(S(n))$, and $S(n)\in\omega$, so $S(n)\in U$. By Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §induction, $\omega\subseteq U$, so $f(n)=f'(n)$ for every $n\in\omega$. As $\operatorname{dom}f=\omega=\operatorname{dom}f'$ by Functions, Values of a Function, and Functions from One Class to Another §map, Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality gives $f'=f$. Hence $f$ is the only map with the stated properties.