Can we define a function on $\mathbb{N}$ recursively from all its previous values? In set theory, the recursion principle states that a function $f$ can be defined in a way where $f\left(\boldsymbol{n}^{+}\right)$ depends on $\boldsymbol{n}$ and $f\left(\boldsymbol{n}\right)$. The complete statement goes as follows:

Let $y_{0}$ be an element of a set $Y$ and $h: \mathbb{N} \times Y \to Y$ be a function. Then there exists a unique function $f: \mathbb{N} \to Y$ such that $f\left(\boldsymbol{0}\right) = y_{0}$ and $f\left(\boldsymbol{n}^{+}\right) = h\left(\boldsymbol{n},f\left(\boldsymbol{n}\right)\right)$ for all $\boldsymbol{n} \in \mathbb{N}$.

I was thinking if there exists a strong version of the recursion principle, that is, a function $f$ can be defined in a way where $f\left(\boldsymbol{n}^{+}\right)$ is defined by all its previous values $f\left(\boldsymbol{0}\right), f\left(\boldsymbol{1}\right), \dots, f\left(\boldsymbol{n}\right)$. My thought was verified in a recent discussion. In fact, this type of definition is used in defining a Fibonacci sequence:
\begin{equation}
\begin{aligned}
&F_0 = 0,\ F_1 = 1\\
&F_{n+2} = F_{n+1} + F_{n},\ n \geq 0.
\end{aligned}
\end{equation}
I would like to seek a proof for a "strong" statement of this idea. My first difficulty was how to express this type of recursion principle formally within the language of set theory. I have come up with a statement to avoid involving $\left\{f\left(\boldsymbol{0}\right),f\left(\boldsymbol{1}\right),f\left(\boldsymbol{2}\right),\dots,f\left(\boldsymbol{n}\right)\right\}$:

Let $y_{0}$ be any element of a set $Y$ and $h: \mathscr{P}\left(\mathbb{N}\times Y\right) \to \mathscr{P}\left(\mathbb{N}\times Y\right)$ be a function. Then there exists a unique function $f: \mathbb{N} \to Y$ such that
\begin{equation*}
f\left(\boldsymbol{0}\right) = y_{0},
\end{equation*}
and
\begin{equation*}
\forall \boldsymbol{n} \geq \boldsymbol{1}, f\vert_{\boldsymbol{n}^{+}} = h\left(f\vert_{\boldsymbol{n}}\right).
\end{equation*}

I am not sure if this is a legitimate statement for what I am seeking. If so, can anyone provide hints of how to prove it? If there is anything wrong with this statement, can anyone propose a correct one?

Theorem:

Let $y_{0}$ be any element of a set $Y$ and $h: \mathscr{P}\left(\mathbb{N}\times Y\right) \to Y$ be a function. Then there exists a unique function $f: \mathbb{N} \to Y$ such that
\begin{equation*}
f\left(\boldsymbol{0}\right) = y_{0},
\end{equation*}
and
\begin{equation*}
f\left(\boldsymbol{n}^{+}\right) = h\left(f_{\vert \boldsymbol{n}^{+}}\right).
\end{equation*}

Proof:
Assume $Y$ is an arbitrary set and $y_{0} \in Y$. Also assume that we have an arbitrary function $h: \mathscr{P}\left(\mathbb{N}\times Y\right) \to Y$. We may define a function $\hat{h}: \mathbb{N} \times \mathscr{P}\left(\mathbb{N}\times Y\right) \to \mathscr{P}\left(\mathbb{N}\times Y\right)$ as
\begin{equation*}
\forall \boldsymbol{n} \in \mathbb{N}, \forall r \in \mathscr{P}\left(\mathbb{N}\times Y\right),\hat{h}\left(\boldsymbol{n},r\right) = r \cup \left\{ \langle \boldsymbol{n}^{+}, h\left(r\right) \rangle \right\}.
\end{equation*}
Note that $\left\{\langle\boldsymbol{0},y_{0}\rangle\right\} \in \mathscr{P}\left(\mathbb{N}\times Y\right)$. According to the weak recursion principle, there exists a unique function $\hat{f}: \mathbb{N} \to \mathscr{P}\left(\mathbb{N}\times Y\right)$ such that
\begin{equation*}
\hat{f}\left(\boldsymbol{0}\right) = \left\{\langle \boldsymbol{0},y_{0} \rangle\right\}
\end{equation*}
\begin{equation*}
\hat{f}\left(\boldsymbol{n}^{+}\right) = \hat{h}\left(\boldsymbol{n},\hat{f}\left(\boldsymbol{n}\right)\right).
\end{equation*}
We first prove that for any $\boldsymbol{m},\boldsymbol{n} \in \mathbb{N}$, $\boldsymbol{m} \leq \boldsymbol{n}$ implies $\hat{f}\left(\boldsymbol{m}\right) \subseteq \hat{f}\left(\boldsymbol{n}\right)$. Fix $\boldsymbol{m}$ and define the following set:
\begin{equation*}
A = \left\{\boldsymbol{n} \in \mathbb{N}: \boldsymbol{m} \leq \boldsymbol{n} \implies \hat{f}\left(\boldsymbol{m}\right) \subseteq \hat{f}\left(\boldsymbol{n}\right) \right\}.
\end{equation*}
First of all, consider the case $\boldsymbol{0}$. In this case, the only situation worth discussing is $\boldsymbol{m} = \boldsymbol{0}$. It is clear that $\hat{f}\left(\boldsymbol{0}\right) \subseteq \hat{f}\left(\boldsymbol{0}\right)$. Consequently, $\boldsymbol{0} \in A$. Next, assume that $\boldsymbol{n} \in A$. There are three cases to discuss for $\boldsymbol{n}^{+}$. If $\boldsymbol{m} \leq \boldsymbol{n}$, then $\hat{f}\left(\boldsymbol{m}\right) \subseteq \hat{f}\left(\boldsymbol{n}\right)$. Also,
\begin{equation*}
\hat{f}\left(\boldsymbol{n}^{+}\right) = \hat{h}\left(\boldsymbol{n},\hat{f}\left(\boldsymbol{n}\right)\right) = \hat{f}\left(\boldsymbol{n}\right) \cup \left\{ \langle \boldsymbol{n}^{+}, h\left(\hat{f}\left(\boldsymbol{n}\right)\right) \rangle \right\}.
\end{equation*}
It is immediately clear that $\hat{f}\left(\boldsymbol{m}\right) \subseteq \hat{f}\left(\boldsymbol{n}^{+}\right)$, and $\boldsymbol{n}^{+} \in A$. The next case to discuss is $\boldsymbol{m} = \boldsymbol{n}^{+}$. It is also immediately clear that $f\left(\boldsymbol{m}\right) \subseteq f\left(\boldsymbol{m}^{+}\right)$, and $\boldsymbol{n}^{+} \in A$. The third case is $\boldsymbol{m} > \boldsymbol{n}^{+}$. It is a trivial case, and $\boldsymbol{n}^{+} \in A$. Then we have proven that $\boldsymbol{n} \in A$ implies $\boldsymbol{n}^{+} \in A$. Thus, $A = \mathbb{N}$.
Next, we shall prove that each $\hat{f}\left({\boldsymbol{n}}\right)$ is a function on $\boldsymbol{n}^{+}$. Similarly, we define the following set:
\begin{equation*}
B = \left\{\boldsymbol{n} \in \mathbb{N}: \hat{f}\left(\boldsymbol{n}\right) \textrm{ is a function on }\boldsymbol{n}^{+}\right\}.
\end{equation*}
From the definition of $\hat{f}$, it is obvious that $\hat{f}\left(\boldsymbol{0}\right)$ is a function on $\boldsymbol{1}$. Then, $\boldsymbol{0} \in B$. Next assume that $\boldsymbol{n} \in B$, that is, for an arbitrary $\boldsymbol{n} \in \mathbb{N}$, $\hat{f}\left(\boldsymbol{n}\right)$ is a function on $\boldsymbol{n}^{+}$. According the the definition of $\hat{f}$, we have
\begin{equation*}
\hat{f}\left(\boldsymbol{n}^{+}\right) = \hat{h}\left(\boldsymbol{n},\hat{f}\left(\boldsymbol{n}\right)\right) = \hat{f}\left({\boldsymbol{n}}\right) \cup \left\{\langle\boldsymbol{n}^{+}, h\left(\hat{f}\left(\boldsymbol{n}\right)\right) \rangle\right\}.
\end{equation*}
It is immediately clear that $\hat{f}\left(\boldsymbol{n}^{+}\right)$ is a function on $\left(\boldsymbol{n}^{+}\right)^{+}$. Then $\boldsymbol{n}^{+} \in B$. We may conclude that $B = \mathbb{N}$.
Then consider the set
\begin{equation*}
f = \bigcup\operatorname{Range}\left(\hat{f}\right).
\end{equation*}
It should be noted that $f_{\vert\boldsymbol{n}^{+}}$ is of the following property:
\begin{equation*}
f_{\vert\boldsymbol{n}^{+}} = \hat{f}\left(\boldsymbol{n}\right),
\end{equation*}
given that for any $\boldsymbol{m},\boldsymbol{n} \in \mathbb{N}$, $\boldsymbol{m} \leq \boldsymbol{n}$ implies $\hat{f}\left(\boldsymbol{m}\right) \subseteq \hat{f}\left(\boldsymbol{n}\right)$, which has been proved earlier.
Assume that $\boldsymbol{n}_{1},\boldsymbol{n}_{2} \in \mathbb{N}$, $\boldsymbol{n}_{1} \neq \boldsymbol{n}_{2}$ and $\boldsymbol{n}_{1},\boldsymbol{n}_{2} \in \operatorname{domain}\left(f\right)$. It is immediately realized that $\boldsymbol{n}_{1},\boldsymbol{n}_{2} \in \operatorname{domain}\left(\hat{f}\left(\boldsymbol{n}_{3}\right)\right)$ where $\boldsymbol{n}_{3} \geq \max{\left(\boldsymbol{n}_{1},\boldsymbol{n}_{2}\right)}$. As $\hat{f}\left({\boldsymbol{n}_{3}}\right)$ is a function on ${\boldsymbol{n}_{3}}^{+}$, it is clear that $\left[\hat{f}\left(\boldsymbol{n}_{3}\right)\right]\left(\boldsymbol{n}_{1}\right) \neq \left[\hat{f}\left(\boldsymbol{n}_{3}\right)\right]\left(\boldsymbol{n}_{2}\right)$. As $\left[\hat{f}\left(\boldsymbol{n}_{3}\right)\right]\left(\boldsymbol{n}_{1}\right) = f\left(\boldsymbol{n}_{1}\right)$ and $\left[\hat{f}\left(\boldsymbol{n}_{3}\right)\right]\left(\boldsymbol{n}_{2}\right) = f\left(\boldsymbol{n}_{2}\right)$, we have $f\left(\boldsymbol{n}_{1}\right) \neq f\left(\boldsymbol{n}_{2}\right)$. So that $f$ is indeed a function.
We would like to argue that $f$ is a function with $f\left(\boldsymbol{0}\right) = y_{0}$ and $f\left(\boldsymbol{n}^{+}\right) = h\left(f_{\vert\boldsymbol{n}^{+}}\right)$. Using the fact $f_{\vert\boldsymbol{n}^{+}} = \hat{f}\left(\boldsymbol{n}\right)$, we have
\begin{equation*}
f\left(\boldsymbol{0}\right) = f_{\vert\boldsymbol{1}}\left(\boldsymbol{0}\right) = \left[\hat{f}\left(0\right)\right] = y_{0}.
\end{equation*}
Also,
\begin{equation*}
f\left(\boldsymbol{n}^{+}\right) = \left[\hat{f}\left(\boldsymbol{n}^{+}\right)\right]\left(\boldsymbol{n}^{+}\right) = h\left(\hat{f}\left(\boldsymbol{n}\right)\right) = h\left(f_{\vert\boldsymbol{n}^{+}}\right)
\end{equation*}
The uniqueness of $f$ can be easily argued from the uniqueness of $\hat{f}$.
 A: That statement is not true. For example, if we take $h$ to be the identity function we'd need an $f$ such that (for example) $f_{\vert\bf 2}=f_{\vert \bf 1}$, which can't happen. We can do nastier things too: suppose $Y=\mathbb{N}$ and consider e.g. $$h(X)=\{(n, y+1): (n,y)\in X\}.$$
Instead, what we want our "update" function to do is tell us just the next value of $f$. So $h$ should be a map $\mathcal{P}(\mathbb{N}\times Y)\rightarrow Y$, and $f$ should satisfy $$f({\bf 0})=y_0,\quad f({\bf n^+})=h(f_{\vert{\bf n^+}}).$$
And in fact this is how I've always seen the recursion theorem presented.
(Here I'm treating $g_{\vert {\bf a}}$ as $\{(x,y): x<{\bf a}$ and $g(x)=y\}$; if you're using the "$\le$"-version, replace "$h(f_{\vert {\bf n^+}})$" with "$h(f_{\vert{\bf n}})$" above.)
Just like with strong/weak induction, we can prove "strong recursion" from "weak recursion, and this is a good exercise. (HINT: given a function $f:\mathbb{N}\rightarrow Y$, consider the function $\hat{f}:\mathbb{N}\rightarrow\mathcal{P}(\mathbb{N}\times Y): {\bf n}\mapsto f_{\vert{\bf n}}$. Instead of building $f$ by strong recursion, you can build $\hat{f}$ by weak recursion and then define $f$ from $\hat{f}$.)
