Knowlpedia

Theorem

Recursion on the natural numbers

An initial value and a specified next-step rule determine a unique sequence.

Statement

Let XX be a set, x0∈Xx_0\in X, and F:N×X→XF:\mathbb N\times X\to X a function. There exists a unique (xn)n≥0(x_n)_{n\ge0} such that

xn+1=F(n,xn)(n≥0)x_{n+1}=F(n,x_n)\qquad(n\ge0)

with the given initial value. This is recursion on the natural numbers.

Construction and uniqueness

Construct each finite list by appending the value specified by FF. Induction shows that these finite lists agree on overlaps; their union defines the infinite sequence. If two sequences obey the same initial value and step rule, induction gives equality at every index.

The rule must supply a value for every input it is asked to process. A procedure saying only to choose a parameter requires a proof that an admissible value exists; choosing the least admissible integer, when available, turns it into a specified rule.