Veblen hierarchy

We define the two-arguments Veblen function, which satisfies veblen 0 a = ω ^ a and that for o ≠ 0, veblen o enumerates the common fixed points of veblen o' for o' < o.

We use this to define two important functions on ordinals: the epsilon function ε_ o = veblen 1 o, and the gamma function Γ_ o enumerating the fixed points of veblen · 0.

Main definitions

• veblenWith: The Veblen hierarchy with a specified initial function.
• veblen: The Veblen hierarchy starting with ω ^ ·.

Notation

The following notation is scoped to the Ordinal namespace.

• ε_ o is notation for veblen 1 o. ε₀ is notation for ε_ 0.
• Γ_ o is notation for gamma o. Γ₀ is notation for Γ_ 0.

TODO

• Prove that ε₀ and Γ₀ are countable.
• Prove that the exponential principal ordinals are the epsilon ordinals (and 0, 1, 2, ω).
• Prove that the ordinals principal under veblen are the gamma ordinals (and 0).

Veblen function with a given starting function

@[irreducible]

def Ordinal.veblenWith (f : Ordinal.{u} → Ordinal.{u}) (o : Ordinal.{u}) : Ordinal.{u} → Ordinal.{u}

veblenWith f o is the o-th function in the Veblen hierarchy starting with f. This is defined so that

• veblenWith f 0 = f.
• veblenWith f o for o ≠ 0 enumerates the common fixed points of veblenWith f o' over all o' < o.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ordinal.veblenWith_zero (f : Ordinal.{u_1} → Ordinal.{u_1}) : veblenWith f 0 = f

theorem Ordinal.veblenWith_of_ne_zero {o : Ordinal.{u}} (f : Ordinal.{u} → Ordinal.{u}) (h : o ≠ 0) : veblenWith f o = derivFamily fun (x : ↑(Set.Iio o)) => veblenWith f ↑x

theorem Ordinal.isNormal_veblenWith' {o : Ordinal.{u}} (f : Ordinal.{u} → Ordinal.{u}) (h : o ≠ 0) : IsNormal (veblenWith f o)

veblenWith f o is always normal for o ≠ 0. See isNormal_veblenWith for a version which assumes IsNormal f.

theorem Ordinal.isNormal_veblenWith {f : Ordinal.{u} → Ordinal.{u}} (hf : IsNormal f) (o : Ordinal.{u}) : IsNormal (veblenWith f o)

veblenWith f o is always normal whenever f is. See isNormal_veblenWith' for a version which does not assume IsNormal f.

theorem Ordinal.IsNormal.veblenWith {f : Ordinal.{u} → Ordinal.{u}} (hf : IsNormal f) (o : Ordinal.{u}) : IsNormal (veblenWith f o)

Alias of Ordinal.isNormal_veblenWith.

---

veblenWith f o is always normal whenever f is. See isNormal_veblenWith' for a version which does not assume IsNormal f.

theorem Ordinal.veblenWith_veblenWith_of_lt {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ : Ordinal.{u}} (hf : IsNormal f) (h : o₁ < o₂) (a : Ordinal.{u}) : veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a

theorem Ordinal.veblenWith_succ {f : Ordinal.{u} → Ordinal.{u}} (hf : IsNormal f) (o : Ordinal.{u}) : veblenWith f (Order.succ o) = deriv (veblenWith f o)

theorem Ordinal.veblenWith_right_strictMono {f : Ordinal.{u} → Ordinal.{u}} (hf : IsNormal f) (o : Ordinal.{u}) : StrictMono (veblenWith f o)

@[simp]

theorem Ordinal.veblenWith_lt_veblenWith_iff_right {f : Ordinal.{u} → Ordinal.{u}} {o a b : Ordinal.{u}} (hf : IsNormal f) : veblenWith f o a < veblenWith f o b ↔ a < b

@[simp]

theorem Ordinal.veblenWith_le_veblenWith_iff_right {f : Ordinal.{u} → Ordinal.{u}} {o a b : Ordinal.{u}} (hf : IsNormal f) : veblenWith f o a ≤ veblenWith f o b ↔ a ≤ b

theorem Ordinal.veblenWith_injective {f : Ordinal.{u} → Ordinal.{u}} (hf : IsNormal f) (o : Ordinal.{u}) : Function.Injective (veblenWith f o)

@[simp]

theorem Ordinal.veblenWith_inj {f : Ordinal.{u} → Ordinal.{u}} {o a b : Ordinal.{u}} (hf : IsNormal f) : veblenWith f o a = veblenWith f o b ↔ a = b

theorem Ordinal.right_le_veblenWith {f : Ordinal.{u} → Ordinal.{u}} (hf : IsNormal f) (o a : Ordinal.{u}) : a ≤ veblenWith f o a

theorem Ordinal.veblenWith_left_monotone {f : Ordinal.{u} → Ordinal.{u}} (hf : IsNormal f) (a : Ordinal.{u}) : Monotone fun (x : Ordinal.{u}) => veblenWith f x a

theorem Ordinal.veblenWith_pos {f : Ordinal.{u} → Ordinal.{u}} {o a : Ordinal.{u}} (hf : IsNormal f) (hp : 0 < f 0) : 0 < veblenWith f o a

theorem Ordinal.veblenWith_zero_strictMono {f : Ordinal.{u} → Ordinal.{u}} (hf : IsNormal f) (hp : 0 < f 0) : StrictMono fun (x : Ordinal.{u}) => veblenWith f x 0

theorem Ordinal.veblenWith_zero_lt_veblenWith_zero {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ : Ordinal.{u}} (hf : IsNormal f) (hp : 0 < f 0) : veblenWith f o₁ 0 < veblenWith f o₂ 0 ↔ o₁ < o₂

theorem Ordinal.veblenWith_zero_le_veblenWith_zero {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ : Ordinal.{u}} (hf : IsNormal f) (hp : 0 < f 0) : veblenWith f o₁ 0 ≤ veblenWith f o₂ 0 ↔ o₁ ≤ o₂

theorem Ordinal.veblenWith_zero_inj {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ : Ordinal.{u}} (hf : IsNormal f) (hp : 0 < f 0) : veblenWith f o₁ 0 = veblenWith f o₂ 0 ↔ o₁ = o₂

theorem Ordinal.left_le_veblenWith {f : Ordinal.{u} → Ordinal.{u}} (hf : IsNormal f) (hp : 0 < f 0) (o a : Ordinal.{u}) : o ≤ veblenWith f o a

theorem Ordinal.IsNormal.veblenWith_zero {f : Ordinal.{u} → Ordinal.{u}} (hf : IsNormal f) (hp : 0 < f 0) : IsNormal fun (x : Ordinal.{u}) => veblenWith f x 0

theorem Ordinal.cmp_veblenWith {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ a b : Ordinal.{u}} (hf : IsNormal f) : cmp (veblenWith f o₁ a) (veblenWith f o₂ b) = match cmp o₁ o₂ with | Ordering.eq => cmp a b | Ordering.lt => cmp a (veblenWith f o₂ b) | Ordering.gt => cmp (veblenWith f o₁ a) b

theorem Ordinal.veblenWith_lt_veblenWith_iff {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ a b : Ordinal.{u}} (hf : IsNormal f) : veblenWith f o₁ a < veblenWith f o₂ b ↔ o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a < b

veblenWith f o₁ a < veblenWith f o₂ b iff one of the following holds:

• o₁ = o₂ and a < b
• o₁ < o₂ and a < veblenWith f o₂ b
• o₁ > o₂ and veblenWith f o₁ a < b

theorem Ordinal.veblenWith_le_veblenWith_iff {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ a b : Ordinal.{u}} (hf : IsNormal f) : veblenWith f o₁ a ≤ veblenWith f o₂ b ↔ o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a ≤ b

veblenWith f o₁ a ≤ veblenWith f o₂ b iff one of the following holds:

• o₁ = o₂ and a ≤ b
• o₁ < o₂ and a ≤ veblenWith f o₂ b
• o₁ > o₂ and veblenWith f o₁ a ≤ b

theorem Ordinal.veblenWith_eq_veblenWith_iff {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ a b : Ordinal.{u}} (hf : IsNormal f) : veblenWith f o₁ a = veblenWith f o₂ b ↔ o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a = b

veblenWith f o₁ a = veblenWith f o₂ b iff one of the following holds:

• o₁ = o₂ and a = b
• o₁ < o₂ and a = veblenWith f o₂ b
• o₁ > o₂ and veblenWith f o₁ a = b

Veblen function

def Ordinal.veblen : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}

veblen o is the o-th function in the Veblen hierarchy starting with ω ^ ·. That is:

• veblen 0 a = ω ^ a.
• veblen o for o ≠ 0 enumerates the fixed points of veblen o' for o' < o.

Equations

• Ordinal.veblen = Ordinal.veblenWith fun (x : Ordinal.{?u.6}) => Ordinal.omega0 ^ x

@[simp]

theorem Ordinal.veblen_zero : veblen 0 = fun (a : Ordinal.{u_1}) => omega0 ^ a

theorem Ordinal.veblen_zero_apply (a : Ordinal.{u_1}) : veblen 0 a = omega0 ^ a

theorem Ordinal.veblen_of_ne_zero {o : Ordinal.{u}} (h : o ≠ 0) : veblen o = derivFamily fun (x : ↑(Set.Iio o)) => veblen ↑x

theorem Ordinal.isNormal_veblen (o : Ordinal.{u_1}) : IsNormal (veblen o)

theorem Ordinal.veblen_veblen_of_lt {o₁ o₂ : Ordinal.{u}} (h : o₁ < o₂) (a : Ordinal.{u}) : veblen o₁ (veblen o₂ a) = veblen o₂ a

theorem Ordinal.veblen_succ (o : Ordinal.{u_1}) : veblen (Order.succ o) = deriv (veblen o)

theorem Ordinal.veblen_right_strictMono (o : Ordinal.{u_1}) : StrictMono (veblen o)

@[simp]

theorem Ordinal.veblen_lt_veblen_iff_right {o a b : Ordinal.{u}} : veblen o a < veblen o b ↔ a < b

@[simp]

theorem Ordinal.veblen_le_veblen_iff_right {o a b : Ordinal.{u}} : veblen o a ≤ veblen o b ↔ a ≤ b

theorem Ordinal.veblen_injective (o : Ordinal.{u_1}) : Function.Injective (veblen o)

@[simp]

theorem Ordinal.veblen_inj {o a b : Ordinal.{u}} : veblen o a = veblen o b ↔ a = b

theorem Ordinal.right_le_veblen (o a : Ordinal.{u_1}) : a ≤ veblen o a

theorem Ordinal.veblen_left_monotone (o : Ordinal.{u_1}) : Monotone fun (x : Ordinal.{u_1}) => veblen x o

@[simp]

theorem Ordinal.veblen_pos {o a : Ordinal.{u}} : 0 < veblen o a

theorem Ordinal.veblen_zero_strictMono : StrictMono fun (x : Ordinal.{u_1}) => veblen x 0

@[simp]

theorem Ordinal.veblen_zero_lt_veblen_zero {o₁ o₂ : Ordinal.{u}} : veblen o₁ 0 < veblen o₂ 0 ↔ o₁ < o₂

@[simp]

theorem Ordinal.veblen_zero_le_veblen_zero {o₁ o₂ : Ordinal.{u}} : veblen o₁ 0 ≤ veblen o₂ 0 ↔ o₁ ≤ o₂

@[simp]

theorem Ordinal.veblen_zero_inj {o₁ o₂ : Ordinal.{u}} : veblen o₁ 0 = veblen o₂ 0 ↔ o₁ = o₂

theorem Ordinal.left_le_veblen (o a : Ordinal.{u_1}) : o ≤ veblen o a

theorem Ordinal.isNormal_veblen_zero : IsNormal fun (x : Ordinal.{u_1}) => veblen x 0

theorem Ordinal.cmp_veblen {o₁ o₂ a b : Ordinal.{u}} : cmp (veblen o₁ a) (veblen o₂ b) = match cmp o₁ o₂ with | Ordering.eq => cmp a b | Ordering.lt => cmp a (veblen o₂ b) | Ordering.gt => cmp (veblen o₁ a) b

theorem Ordinal.veblen_lt_veblen_iff {o₁ o₂ a b : Ordinal.{u}} : veblen o₁ a < veblen o₂ b ↔ o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < veblen o₂ b ∨ o₂ < o₁ ∧ veblen o₁ a < b

veblen o₁ a < veblen o₂ b iff one of the following holds:

• o₁ = o₂ and a < b
• o₁ < o₂ and a < veblen o₂ b
• o₁ > o₂ and veblen o₁ a < b

theorem Ordinal.veblen_le_veblen_iff {o₁ o₂ a b : Ordinal.{u}} : veblen o₁ a ≤ veblen o₂ b ↔ o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ veblen o₂ b ∨ o₂ < o₁ ∧ veblen o₁ a ≤ b

veblen o₁ a ≤ veblen o₂ b iff one of the following holds:

• o₁ = o₂ and a ≤ b
• o₁ < o₂ and a ≤ veblen o₂ b
• o₁ > o₂ and veblen o₁ a ≤ b

theorem Ordinal.veblen_eq_veblen_iff {o₁ o₂ a b : Ordinal.{u}} : veblen o₁ a = veblen o₂ b ↔ o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = veblen o₂ b ∨ o₂ < o₁ ∧ veblen o₁ a = b

veblen o₁ a ≤ veblen o₂ b iff one of the following holds:

• o₁ = o₂ and a = b
• o₁ < o₂ and a = veblen o₂ b
• o₁ > o₂ and veblen o₁ a = b

Epsilon function

@[reducible, inline]

abbrev Ordinal.epsilon : Ordinal.{u_1} → Ordinal.{u_1}

The epsilon function enumerates the fixed points of ω ^ ⬝. This is an abbreviation for veblen 1.

Equations

• Ordinal.epsilon = Ordinal.veblen 1

def Ordinal.termε_ : Lean.ParserDescr

The epsilon function enumerates the fixed points of ω ^ ⬝. This is an abbreviation for veblen 1.

Equations

• Ordinal.termε_ = Lean.ParserDescr.node `Ordinal.termε_ 1024 (Lean.ParserDescr.symbol "ε_ ")

def Ordinal.termε₀ : Lean.ParserDescr

ε₀ is the first fixed point of ω ^ ⬝, i.e. the supremum of ω, ω ^ ω, ω ^ ω ^ ω, …

Equations

• Ordinal.termε₀ = Lean.ParserDescr.node `Ordinal.termε₀ 1024 (Lean.ParserDescr.symbol "ε₀")

theorem Ordinal.epsilon_eq_deriv (o : Ordinal.{u_1}) : o.epsilon = deriv (fun (a : Ordinal.{u_1}) => omega0 ^ a) o

theorem Ordinal.epsilon0_eq_nfp : epsilon 0 = nfp (fun (a : Ordinal.{u_1}) => omega0 ^ a) 0

theorem Ordinal.epsilon_succ_eq_nfp (o : Ordinal.{u_1}) : (Order.succ o).epsilon = nfp (fun (a : Ordinal.{u_1}) => omega0 ^ a) (Order.succ o.epsilon)

theorem Ordinal.epsilon0_le_of_omega0_opow_le {o : Ordinal.{u}} (h : omega0 ^ o ≤ o) : epsilon 0 ≤ o

@[simp]

theorem Ordinal.omega0_opow_epsilon (o : Ordinal.{u_1}) : omega0 ^ o.epsilon = o.epsilon

theorem Ordinal.lt_epsilon0 {o : Ordinal.{u}} : o < epsilon 0 ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) => omega0 ^ a)^[n] 0

ε₀ is the limit of 0, ω ^ 0, ω ^ ω ^ 0, …

theorem Ordinal.iterate_omega0_opow_lt_epsilon0 (n : ℕ) : (fun (a : Ordinal.{u_1}) => omega0 ^ a)^[n] 0 < epsilon 0

ω ^ ω ^ … ^ 0 < ε₀

theorem Ordinal.omega0_lt_epsilon (o : Ordinal.{u_1}) : omega0 < o.epsilon

theorem Ordinal.natCast_lt_epsilon (n : ℕ) (o : Ordinal.{u_1}) : ↑n < o.epsilon

theorem Ordinal.epsilon_pos (o : Ordinal.{u_1}) : 0 < o.epsilon

Gamma function

def Ordinal.gamma (o : Ordinal.{u_1}) : Ordinal.{u_1}

The gamma function enumerates the fixed points of veblen · 0.

Of particular importance is Γ₀ = gamma 0, the Feferman-Schütte ordinal.

Equations

• o.gamma = Ordinal.deriv (fun (x : Ordinal.{?u.7}) => Ordinal.veblen x 0) o

def Ordinal.termΓ_ : Lean.ParserDescr

The gamma function enumerates the fixed points of veblen · 0.

Of particular importance is Γ₀ = gamma 0, the Feferman-Schütte ordinal.

Equations

• Ordinal.termΓ_ = Lean.ParserDescr.node `Ordinal.termΓ_ 1024 (Lean.ParserDescr.symbol "Γ_ ")

def Ordinal.termΓ₀ : Lean.ParserDescr

The Feferman-Schütte ordinal Γ₀ is the smallest fixed point of veblen · 0, i.e. the supremum of veblen ε₀ 0, veblen (veblen ε₀ 0) 0, etc.

Equations

• Ordinal.termΓ₀ = Lean.ParserDescr.node `Ordinal.termΓ₀ 1024 (Lean.ParserDescr.symbol "Γ₀")

theorem Ordinal.isNormal_gamma : IsNormal gamma

theorem Ordinal.strictMono_gamma : StrictMono gamma

theorem Ordinal.monotone_gamma : Monotone gamma

@[simp]

theorem Ordinal.gamma_lt_gamma {a b : Ordinal.{u}} : a.gamma < b.gamma ↔ a < b

@[simp]

theorem Ordinal.gamma_le_gamma {a b : Ordinal.{u}} : a.gamma ≤ b.gamma ↔ a ≤ b

@[simp]

theorem Ordinal.gamma_inj {a b : Ordinal.{u}} : a.gamma = b.gamma ↔ a = b

@[simp]

theorem Ordinal.veblen_gamma_zero (o : Ordinal.{u_1}) : veblen o.gamma 0 = o.gamma

theorem Ordinal.gamma0_eq_nfp : gamma 0 = nfp (fun (x : Ordinal.{u_1}) => veblen x 0) 0

theorem Ordinal.gamma_succ_eq_nfp (o : Ordinal.{u_1}) : (Order.succ o).gamma = nfp (fun (x : Ordinal.{u_1}) => veblen x 0) (Order.succ o.gamma)

theorem Ordinal.gamma0_le_of_veblen_le {o : Ordinal.{u}} (h : veblen o 0 ≤ o) : gamma 0 ≤ o

theorem Ordinal.lt_gamma0 {o : Ordinal.{u}} : o < gamma 0 ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) => veblen a 0)^[n] 0

Γ₀ is the limit of 0, veblen 0 0, veblen (veblen 0 0) 0, …

theorem Ordinal.iterate_veblen_lt_gamma0 (n : ℕ) : (fun (a : Ordinal.{u_1}) => veblen a 0)^[n] 0 < gamma 0

veblen (veblen … (veblen 0 0) … 0) 0 < Γ₀

theorem Ordinal.epsilon0_lt_gamma (o : Ordinal.{u_1}) : epsilon 0 < o.gamma

theorem Ordinal.omega0_lt_gamma (o : Ordinal.{u_1}) : omega0 < o.gamma

theorem Ordinal.natCast_lt_gamma {o : Ordinal.{u}} (n : ℕ) : ↑n < o.gamma

@[simp]

theorem Ordinal.gamma_pos {o : Ordinal.{u}} : 0 < o.gamma