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:
It can be shown that if is normal then commutes with suprema; for any nonempty set of ordinals,
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 f ≥ γ for all ordinals γ and that f commutes with suprema. Given these results, inductively define an increasing sequence <αn> by setting α0 = α, and αn+1 = f for n ∈ ω. Let β = sup, so β ≥ α. Moreover, because f commutes with suprema,
The last equality follows from the fact that the sequence <αn> increases.
As an aside, it can be demonstrated that the β found in this way is the smallest fixed point greater than or equal to α.

Example application

The function f : Ord → Ord, f = ωα is normal. Thus, there exists an ordinal θ such that θ = ωθ. In fact, the lemma shows that there is a closed, unbounded class of such θ.