The SlugMath Wiki is under heavy development!

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

## Logical Connections

This definition logically relies on the following definitions and statements: Def/Natural number

The following statements and definitions logically rely on the material of this page: Def/Binary operation, Def/Factorial, and Def/Rooted ordered binary tree

To visualize the logical connections between this definition and other items of mathematical knowledge, you can visit any of the following clusters, and click the "Visualize" tab: Clust/Properties of natural numbers, Clust/Logic and foundations