Question about the formulation of Kenneth Kunen's "Primitive Recursion on Ordinals" Theorem In Kenneth Kunen's The Foundations of Mathematics, the subject of recursion (on ordinals) is introduced and is described using the following "recipe":

$f(\xi)=G(f_{|\xi})$, where $G$ and $f$ are functions and $f_{|\xi}$ is the function $f$ restricted to the set of ordinals less than $\xi$.

To provide an example, consider the Fibonacci sequence, traditionally written as: $f(0)=1, f(1)=1,$ and when $x \gt 1$, $f(x)=f(x-1)+f(x-2)$.
Using Kunen's definition, I believe we could rewrite this as:
$$f(0)=G(f_{|0})=1$$
$$f(1)=G(f_{|1})=1$$
$$f(x)=G(f_{|x})=f_{|x}(x-1)+f_{|x}(x-2) \text{ when } 2 \leq x \lt \omega$$
In order to let $x$ be defined for all ordinals (not just $\omega$), one could add a final rule as:
$$f(\xi)=G(f_{|\xi})=1 \text{ when } \xi \geq \omega$$
(As we will see shortly, it would also be necessary to define $G(s)$ as equaling an arbitrary default value when $s$ is some set that is not a function with a domain of some ordinal)

In the following paragraphs, Kunen seeks to demonstrate that the general form of $f(\xi)=G(f_{|\xi})$ is "legitimate"; this is accomplished by proving the following theorem:
Primitive Recursion on Ordinals
Suppose that $\color{red}{\forall s\exists!y\varphi(s,y)}$, and define $G(s)$ to be the unique $y$ such that $\varphi(s,y)$. Then we can define a formula $\psi$ for which the following are provable:

*

*$\forall x \exists ! y \psi(x,y)$, so $\psi$ defines a function $F$, where $F(x)$ is the $y$ such that $\psi(x,y)$


*$\forall \xi \in \text{ ON } [F(\xi)=G(F_{|\xi})]$ - where $\text{ ON }$ is shorthand for "is an ordinal"... a regular convention throughout this book -
In the above statement  ("1.", in particular) Kunen states that $\psi$ defines a function $F$. There are several scattered comments (in the book) that make it clear to the reader that this "function" is not really a function in the technical sense because $F$ is not really a set (my understanding is that it is a proper class).

With the necessary background provided, my question is as follows:
I am having difficulty understanding what exactly $\varphi(s,y)$ looks like in the formula $\forall s \exists ! y \varphi (s,y)$...colored in $\color{red}{\text{red}}$... and am wondering if someone could please use the Fibonacci sequence (or an easier recursive formula of your choice) to demonstrate what its corresponding $\varphi(s,y)$ would formally/pseudo-formally look like.

I'm still pretty inexperienced when it comes to constructing sentences using FOL but, using the Fibonacci sequence as my recursive function of interest, it seems like I need to encode the following 5 sub-formulas:

*

*if $s = \emptyset$, then $y=1$
This represents $G(f_{|0})=1$


*if $s=\{\langle 0, 1 \rangle \}$, then $y=1$
This represents $G(f_{|1})=1$


*if $s$ is a function that has an ordinal greater than or equal to $\omega$ as its domain, then $y=1$
This represents $G(f_{|\xi})=1 \text{ when } \xi \geq \omega$


*if $s$ is not a function with a domain of some ordinal, then $y=1$.

We mentioned this at the beginning of the post


*if $s$ is a function whose domain is an ordinal $\geq 2$ and $\lt \omega$, then $y = $ the second component of the maximal element in $s$ $+$ the second component of the next largest element in $s$
This represents $G(f_{|x})=f_{|x}(x-1)+f_{|x}(x-2) \text{ when } 2 \leq x \lt \omega$
(Edit: after playing around with this a little bit, these 5 sub-formulas would be connected via conjunctions, '$\land$')

Am I on the right track? Any help and/or insight is greatly appreciated! Thank you.
 A: The formula $\varphi$ should say what the function $G$ is. In the Fibonacci case, to simplify matters consider the formula $\theta(s)$ given by
$$
s=0\vee s=\{\langle 0,1\rangle\}\vee [\text{fun}(s)\wedge \text{dom}(s)\in \omega\setminus 2]
$$
where $\text{fun(s)}$ is a formula saying "$s$ is a function".
Now let $\varphi(s,y)$ be the formula
$$
[\neg\theta(s)\wedge y=\emptyset] \vee [s=0\wedge  y=1] \vee [s=\{\langle 0,1\rangle \}\wedge y=1]\vee[\text{fun}(s)\wedge \text{dom}(s)\in\omega\setminus 2 \wedge y=s(\text{dom}(s)-1)+s(\text{dom}(s)-2)]
$$
The first quantity in brackets is there to output the default value $\emptyset$ whenever $s$ does not have one of the interesting forms (relative to the Fibonacci sequence). Of course, there are many variations on $\varphi$, I chose this one because it shared some components with what you wrote.
Now, the sentence $\forall s\exists! y\varphi(s,y)$ is provable in ZF (or some weaker theory), and so the recursion theorem kicks in. I'll now use Kunen's choice of notation ($F$ and $G$) to check that this formula does what we want. Remember, $F\upharpoonright \omega$ should be the Fibonacci sequence.
We have:
$$
F(0)=G(F\upharpoonright0)=G(\emptyset)=1
$$
$$
F(1)=G(F\upharpoonright 1)=G(F\upharpoonright \{0\})=G(\{\langle 0,1\rangle\})=1
$$
So far so good.
Now, suppose $2\le n<\omega$. Then $F \upharpoonright n$ is a function with domain $n\in \omega\setminus 2$, and so
$$
F(n)=G(F\upharpoonright n)=(F\upharpoonright n)(n-1)+(F\upharpoonright n)(n-2)=F(n-1)+F(n-2)
$$
which is exactly what we wanted.

I hope this clarifies matters. I'll second Asaf's comment regarding finding transfinite recursion weird on the first (several) encounters. I found that writing out things explicitly (like I've done above) was very helpful in demystifying things. Once you're more comfortable with this stuff, you'll just mention how $F(\xi)$ depends on previous values of $F$ and move on with your day.
