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.
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.