Fixed-point lemma for normal functions: Difference between revisions

Revision as of 01:49, 13 March 2013

Revision as of 11:28, 5 May 2014

Line 1:

The '''fixed-point lemma for normal functions''' is a basic result in [[axiomatic set theory]] stating that any [[normal function]] has arbitrarily large [[fixed point (mathematics)|fixed point]]s (Levy 1979: p.  117). It was first proved by [[Oswald Veblen]] in 1908.

== Background and formal statement ==

A [[normal function]] is a [[proper class|class]] function ''f'' from the class Ord of [[ordinal numbers]] to itself such that:

* ''f'' is '''strictly increasing''': ''f''(&alpha;α) < f(&beta;β) whenever &alpha;α < &beta;β.

* ''f'' is '''continuous''': for every limit ordinal &lambda;λ (i.e. &lambda;λ is neither zero nor a successor), ''f''(&lambda;λ) = sup { f(&alpha;α) : &alpha;α < &lambda;λ }.

It can be shown that if ''f'' is normal then ''f'' commutes with [[supremum|suprema]]; for any nonempty set ''A'' of ordinals,

:''f''(sup ''A'') = sup {''f''(&alpha;) : &alpha; ∈ ''A'' }.

Indeed, if sup ''A'' is a successor ordinal then sup ''A'' is an element of ''A'' and the equality follows from the increasing property of ''f''. If sup ''A'' is a limit ordinal then the equality follows from the continuous property of ''f''.

A '''fixed point''' of a normal function is an ordinal &beta;β such that ''f''(&beta;β) = &beta;β.

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 ''f''(β) = β.

The continuity of the normal function implies the class of fixed points is closed (the supremum of any subset of the class of fixed points is again a fixed point). Thus the fixed point lemma is equivalent to the statement that the fixed points of a normal function form a [[club set|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 &lt;α_''n''&gt; (''n'' &lt; ω) by setting α₀ = α, and α_''n''+1 = ''f''(α_''n'') for ''n'' ∈ ω. Let β = sup {α_''n'' : ''n'' ∈ &omega;ω}, so β ≥ α. Moreover, because ''f'' commutes with suprema,

:''f''(β) = ''f''(sup {α_''n'' : ''n'' &lt; ω})

:&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; = sup {''f''(α_''n'') : ''n'' &lt; ω}