@misc{ORDINAL6.MIZ,
  AUTHOR = {Bancerek, Grzegorz},
  TITLE = {Veblen Hierarchy},
  SECTION1 = {Preliminaries},
  SECTION2 = {Fixpoints of a Normal Function},
  SECTION3 = {Fixpoints in a Universal Set},
  SECTION4 = {Sequences of Sequences of Ordinals},
  SECTION5 = {Veblen Hierarchy},
  SECTION6 = {Epsilon Numbers},
  ADDRESS1 = {Bia{\l}ystok Technical University},
  YEAR = {2010},
  MONTH = {October},
  DAY = {18},
  SUMMARY = {The Veblen hierarchy is an extension of the construction of
  epsilon numbers (fixpoints of the exponential
  map: $\omega^\epsilon = \epsilon$).
  It is a collection $\varphi_\alpha$ of the Veblen Functions
  where $\varphi_0(\beta) = \omega^\beta$
  and $\varphi_1(\beta) = \epsilon_\beta$.
  The sequence of fixpoints of $\varphi_1$ function form $\varphi_2$, etc.
  For a limit non empty ordinal $\lambda$ the function $\varphi_\lambda$ is
  the sequence of common fixpoints of all functions $\varphi_\alpha$
  where $\alpha < \lambda$.\par
  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 $\varphi_\alpha(\beta)$
  as a value of Veblen function from the smallest universal set including
  $\alpha$ and $\beta$.}}
