transfinite recursion
Transfinite recursion, roughly speaking, is a statement about the ability to define a function recursively using transfinite induction![]()
. In its most general and intuitive form, it says
Theorem 1.
Let be a (class) function on , the class of all sets. Then there exists a unique (class) function on , the class of ordinals![]()
, such that
where is the function whose domain is and whose values coincide with on every . In other words, is the restriction of to .
Notice that the theorem above is not provable in ZF set theory![]()
, as and are both classes, not sets. In order to prove this statement, one way of getting around this difficulty is to convert both and into formulas
![]()
, and modify the statement, as follows:
Let be a formula such that
Think of . Then there is a unique formula (think of as ) such that the following two sentences![]()
are derivable
using ZF axioms:
-
1.
where means “ is an ordinal”,
-
2.
, where
-
–
is the formula “ is a function”,
-
–
is the formula “”,
-
–
is the formula , and
-
–
is the formula .
-
–
A stronger form of the transfinite recursion theorem says:
Theorem 2.
Let be any formula (in the language of set theory). Then the following is a theorem: assume that satisfies property that, for every , there is a unique such that . If be a well-ordered set (well-ordered by ), then there is a unique function defined on such that
for every . Here, , the initial segment of in .
The above theorem is actually a collection![]()
of theorems, or known as a theorem schema, where each theorem corresponds to a formula. The other difference between this and the previous theorem is that this theorem is provable in ZF, because the domain of the function is now a set.
| Title | transfinite recursion |
|---|---|
| Canonical name | TransfiniteRecursion |
| Date of creation | 2013-03-22 17:53:51 |
| Last modified on | 2013-03-22 17:53:51 |
| Owner | CWoo (3771) |
| Last modified by | CWoo (3771) |
| Numerical id | 12 |
| Author | CWoo (3771) |
| Entry type | Theorem |
| Classification | msc 03E45 |
| Classification | msc 03E10 |
| Related topic | WellFoundedRecursion |
| Related topic | TransfiniteInduction |