%0 Journal Article %T Veblen Hierarchy %A Grzegorz Bancerek %J Formalized Mathematics %@ 1898-9934 %D 2011 %I %R 10.2478/v10037-011-0014-5 %X 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 ¦Õ0(¦Â) = ¦Ø¦Â and ¦Õ1(¦Â) = ¦Å¦Â. The sequence of fixpoints of ¦Õ1 function form ¦Õ2, 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 ¦Â. %U http://versita.metapress.com/content/g2871n9824586948/?p=e63014958e714f888c6227088fa87423&pi=3