Fixed-point lemma for normal functions
The fixed-point lemma for normal functions is a basic result in axiomatic set theory stating that any normal function has arbitrarily large fixed points. It was first proved by Oswald Veblen in 1908.
Background and formal statement
A normal function is a class function from the class Ord of ordinal numbers to itself such that:- is strictly increasing: whenever.
- is continuous: for every limit ordinal,.
Indeed, if is a successor ordinal then is an element of and the equality follows from the increasing property of. If is a limit ordinal then the equality follows from the continuous property of.
A fixed point of a normal function is an ordinal such that.
The fixed-point lemma states that the class of fixed points of any normal function is nonempty and in fact is unbounded: given any ordinal, there exists an ordinal such that and.
The continuity of the normal function implies the class of fixed points is closed. Thus the fixed-point lemma is equivalent to the statement that the fixed points of a normal function form a closed and unbounded class.
Proof
The first step of the proof is to verify that for all ordinals and that commutes with suprema. Given these results, inductively define an increasing sequence by setting, and for. Let, so. Moreover, because commutes with suprema,The last equality follows from the fact that the sequence increases.
As an aside, it can be demonstrated that the found in this way is the smallest fixed point greater than or equal to.