Countable (or omega1) is the same when lifted

Stream: Is there code for X?

[Jason Rute]

There is a PA.SX question about infinite turning machines and if it matters to define them universe polymorphically. While it is probably good to define them that way, it also probably doesn't matter since they either halt before $\omega_1$ or don't halt at all. But is $\omega_1$ the same between universes? I think this comes down to a few questions about docs#Ordinal.omega including if the following theorem is true:

import Mathlib

theorem lift_omega0 : Ordinal.lift (Ordinal.omega 1) = (Ordinal.omega 1)

I don't see it in Mathlib, but I assume it is true and just follows from docs#Ordinal.lift_lift if used correctly, right?

[Jason Rute]

And I guess one also needs to know that there aren't any new ordinals added beneath Ordinal.omega 1 after lifting. But this is docs#Ordinal.lt_lift_iff right?

[Jason Rute]

Actually, there is an X thread between Joel David Hamkins and @Andrej Bauer that suggests maybe this is not true? https://x.com/JDHamkins/status/1880190691147456525

[Yury G. Kudryashov]

Try rewriting on Ordinal.lift_omega, then Ordinal.lift_one

[Jason Rute]

Thanks!

import Mathlib

theorem lift_omega1.{u,v} : Ordinal.lift.{u,v} (Ordinal.omega.{v} 1) = (Ordinal.omega.{max v u} 1) := calc
  Ordinal.lift (Ordinal.omega 1)
    = (Ordinal.omega (Ordinal.lift.{u,v} 1)) := by rw [Ordinal.lift_omega]
  _ = (Ordinal.omega 1) := by rw [Ordinal.lift_one]

[Violeta Hernández]

Jason Rute said:

I think this comes down to a few questions about docs#Ordinal.omega including if the following theorem is true:

import Mathlib

theorem lift_omega0 : Ordinal.lift (Ordinal.omega 1) = (Ordinal.omega 1)

If simp can't solve this then something is wrong

[Violeta Hernández]

The relation between ordinals in different universes might become more clear keeping this theorem in mind: Ordinal.{u} embeds as an initial segment of Ordinal.{max u v}, and this embedding preserves all arithmetic operations.

[Violeta Hernández]

Btw I only recently added Ordinal.omega, so there might be some missing API; if such let me know!