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 G be a (class) function on V, the class of all sets. Then there exists a unique (class) function F on On, the class of ordinals, such that
F(α)=G(F|α) |
where F|α is the function whose domain is seg(α):= 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 |