Veblen Hierarchy

The Veblen hierarchy is an extension of the construction of epsilon numbers (fixpoints of the exponential map: ω^ε = ε). It is a collection φ_α of the Veblen Functions where φ₀(β) = ω^β and φ₁(β) = ε_β. The sequence of fixpoints of φ₁ function form φ₂, etc. For a limit non empty ordinal λ the function φ_λ is the sequence of common fixpoints of all functions φ_α where α < λ.

The Mizar formalization of the concept cannot be done directly as the Veblen functions are classes (not (small) sets). It is done with use of universal sets (Tarski classes). Namely, we define the Veblen functions in a given universal set and φ_α(β) as a value of Veblen function from the smallest universal set including α and β.