Def/Recursion

Definition of Recursion: Suppose that $k$ is a natural number. Suppose that the following data is given:

• For all $i \in k$ (i.e., for $0 \leq i \leq k-1$), a set $X_i$.
• A wff $\Phi$, with $k+1$ free variables $x_0, x_1, \ldots, x_{k-1}, n, y$.

Suppose that $\Phi$ is "functional", in the sense that: $$\forall x_0, \ldots, \forall x_{k-1}, \forall n \in \NN, n \geq k \Rightarrow \exists ! y \mbox{ such that } \Phi(x_0, \ldots, x_{k-1}, n, y ).$$

Then, there exists a unique sequence of sets $(X_i)_{i \in \NN}$, such that:

• The sequence agrees with the given $X_0, \ldots, X_{k-1}$, for $0 \leq i \leq k-1$.
• For all $i \geq k$, $\Phi(X_{i-k}, \ldots, X_{i-1}, k, X_i )$ is true.

In this situation, we say that the sequence $(X_i)$ is defined recursively, from the data $X_0, \ldots, X_k$ and $\Phi$.