Skip to content
Axiomatic Wiki
Theorem·T07

The recursion theorem

A start value and a step rule determine a unique function on the naturals.

Let be a set, , and a function. Then there is exactly one function with
In words
Given a set X, a starting value a in X, and a step rule h, there is exactly one function f from the naturals to X such that f at zero is the starting value and, for every n, if n is a natural number then f at the successor of n is h applied to n and the current value f(n).
Rests onF02F03F04F06F08F09F14A01A02A06A08
Never needed: F05 · F10 · F11 · F12 · F13 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    Call a subset (product) admissible when and, whenever with , also . The full product is admissible: and by (P1), (P2), and since is a function (D013).
  2. 2
    Let , a set by Separation. By construction for every admissible . Moreover is itself admissible: lies in every admissible set, hence in ; and if , then for every admissible we have , so ; as was arbitrary, .
  3. 3
    Let (Separation). We show by induction; this says assigns exactly one value to each natural.
  4. 4
    Base, : by step 2. Suppose with , and let (D009). Then is admissible: because by L01 (second coordinates differ); and if then , and because by (P3) and L01. So . But then by step 2, contradicting (negation). So is the unique value at .
  5. 5
    Step: let , with unique such that . Admissibility gives . Suppose with , and let . Again since by (P3). For closure, let ; we must rule out . If they were equal, L01 gives and ; then by (P4), so by uniqueness at , so , contradicting the choice of . Hence is admissible, , contradiction. So .
  6. 6
    By T05, . Thus is total and single-valued on : a function (D013). Its equations: because and values are unique; and for each , by admissibility, so .
  7. 7
    Uniqueness: suppose also satisfies both equations. Let (Separation). Then as , and if then by substitutivity, so . T05 gives ; two functions on with equal values everywhere have the same members (pairs), so by Extensionality.
∎

Remarks

Dedekind's recursion theorem (1888), the license behind every definition "by recursion". Induction alone proves that values are unique if they exist; the substance here is existence of the function as a completed set of pairs, obtained as the intersection of all admissible sets. Addition, multiplication and the factorial are all defined by instances of this theorem. The parameter in the step rule costs nothing extra and is exactly what the factorial needs.
Wikipedia ↗Nat.rec ↗

Used by

L67T17
Propose an edit1 published revision