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 |