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.

Main definitions

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

TODO

• Define the epsilon numbers and gamma numbers.
• 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