Talk:Veblen function

Where is the definition?

I hope someone improves this article so that it defines the Veblen function. Right now it simply seems to state a bunch of properties of this function, without asserting that some set of properties characterizes it. John Baez (talk) 06:08, 4 November 2012 (UTC)

In the lead it gives the general definition, "If φ₀ is any normal function, then for any non-zero ordinal α, φ_α is the function enumerating the common fixed points of φ_β for β<α.". In the first section, it defines "Veblen hierarchy" by specifying that "In the special case when φ₀(α)=ω^α, this family of functions is known as the Veblen hierarchy.". JRSpriggs (talk) 10:15, 4 November 2012 (UTC)

Formal definitions

For the binary Veblen hierarchy, a formal definition using recursion on α and β is:

$\phi _{\alpha }(\beta )=\gamma \,\Leftrightarrow \,\operatorname {Ord} (\alpha )\land \operatorname {Ord} (\beta )\land \operatorname {Ord} (\gamma )\land 0<\gamma \land \forall \delta <\gamma (\delta +\delta <\gamma )\land \forall \delta <\alpha (\phi _{\delta }(\gamma )=\gamma )\land \forall \delta <\beta (\phi _{\alpha }(\delta )<\gamma )\land \lnot \exists \rho <\gamma \left(0<\rho \land \forall \delta <\rho (\delta +\delta <\rho )\land \forall \delta <\alpha (\phi _{\delta }(\rho )=\rho )\land \forall \delta <\beta (\phi _{\alpha }(\delta )<\rho )\right)$.

OK? JRSpriggs (talk) 23:13, 15 July 2022 (UTC)

Assuming the previous definition, the Γ function may be defined by:

$\Gamma _{\alpha }=\gamma \,\Leftrightarrow \,\operatorname {Ord} (\alpha )\land \phi _{\gamma }(0)=\gamma \land \forall \delta <\alpha (\Gamma _{\delta }<\gamma )\land \lnot \exists \rho <\gamma (\phi _{\rho }(0)=\rho \land \forall \delta <\alpha (\Gamma _{\delta }<\rho ))$.

OK? JRSpriggs (talk) 07:15, 3 August 2022 (UTC)

If Κ is an uncountable regular cardinal, then the finitary Veblen hierarchy on Κ maps Κ^ω to Κ according to:

$\phi (\mu )=\nu \,\Leftrightarrow \,\mu <\mathrm {K} ^{\omega }\land \nu <\mathrm {K} \land \exists \alpha <\omega \,\exists \sigma <\mathrm {K} ^{\omega }\,\exists \beta <\mathrm {K} \,\exists \gamma <\mathrm {K} (\mu =\mathrm {K} ^{\alpha +2}\cdot \sigma +\mathrm {K} ^{\alpha +1}\cdot \beta +\gamma \land (0<\beta \lor (\alpha =0\land \sigma =0\land \beta =0))\land 0<\nu \land \forall \delta <\nu (\delta +\delta <\nu )\land \forall \delta <\beta (\phi (\mathrm {K} ^{\alpha +2}\cdot \sigma +\mathrm {K} ^{\alpha +1}\cdot \delta +\mathrm {K} ^{\alpha }\cdot \nu )=\nu )\land \forall \delta <\gamma (\phi (\mathrm {K} ^{\alpha +2}\cdot \sigma +\mathrm {K} ^{\alpha +1}\cdot \beta +\delta )<\nu )\land$

$\lnot \exists \rho <\nu \left(0<\rho \land \forall \delta <\rho (\delta +\delta <\rho )\land \forall \delta <\beta (\phi (\mathrm {K} ^{\alpha +2}\cdot \sigma +\mathrm {K} ^{\alpha +1}\cdot \delta +\mathrm {K} ^{\alpha }\cdot \rho )=\rho )\land \forall \delta <\gamma (\phi (\mathrm {K} ^{\alpha +2}\cdot \sigma +\mathrm {K} ^{\alpha +1}\cdot \beta +\delta )<\rho )\right))$.

OK? JRSpriggs (talk) 13:02, 5 August 2022 (UTC)

If Κ is an uncountable regular cardinal, then the transfinitary Veblen hierarchy on Κ maps Κ^Κ to Κ according to:

$\phi (\mu )=\nu \,\Leftrightarrow \,\mu <\mathrm {K} ^{\mathrm {K} }\land \nu <\mathrm {K} \land \exists \alpha <\mathrm {K} \,\exists \sigma <\mathrm {K} ^{\mathrm {K} }\,\exists \beta <\mathrm {K} \,\exists \gamma <\mathrm {K} (\mu =\mathrm {K} ^{\alpha +1}\cdot \sigma +\mathrm {K} ^{\alpha }\cdot \beta +\gamma \land ((0<\alpha \land 0<\beta )\lor (\alpha =1\land \sigma =0\land \beta =0))\land 0<\nu \land \forall \delta <\nu (\delta +\delta <\nu )\land \forall \delta <\beta \,\forall \eta <\alpha (\phi (\mathrm {K} ^{\alpha +1}\cdot \sigma +\mathrm {K} ^{\alpha }\cdot \delta +\mathrm {K} ^{\eta }\cdot \nu )=\nu )\land \forall \delta <\gamma (\phi (\mathrm {K} ^{\alpha +1}\cdot \sigma +\mathrm {K} ^{\alpha }\cdot \beta +\delta )<\nu )\land$

$\lnot \exists \rho <\nu \left(0<\rho \land \forall \delta <\rho (\delta +\delta <\rho )\land \forall \delta <\beta \,\forall \eta <\alpha (\phi (\mathrm {K} ^{\alpha +1}\cdot \sigma +\mathrm {K} ^{\alpha }\cdot \delta +\mathrm {K} ^{\eta }\cdot \rho )=\rho )\land \forall \delta <\gamma (\phi (\mathrm {K} ^{\alpha +1}\cdot \sigma +\mathrm {K} ^{\alpha }\cdot \beta +\delta )<\rho )\right))$.

OK? JRSpriggs (talk) 21:34, 6 August 2022 (UTC)

The small Veblen ordinal (SVO) is φ(Κ^ω) and the large Veblen ordinal (LVO) is $\sup\{\phi (\mathrm {K} ^{\omega }),\phi (\mathrm {K} ^{\phi (\mathrm {K} ^{\omega })}),\phi (\mathrm {K} ^{\phi (\mathrm {K} ^{\phi (\mathrm {K} ^{\omega })})}),\ldots \}$. JRSpriggs (talk) 21:54, 6 August 2022 (UTC)