well order on universes

Stream: lean4

[Dean Young]

Are Lean 4 universes well ordered?

[Reid Barton]

It's not really a meaningful question because you can't quantify over collections of universe levels

[Reid Barton]

Another answer would be "it depends on the model of Lean's type theory you pick"

[Chris Hughes]

I guess it depends on your point of view. In some models of Lean there is a universe for every Natural number, so the universes are well ordered in those models. However, all we know about universe is that they have a 0 a succ and max and imax satisfying a few inequalities, and there are non-well-ordered models of this, so probably you could make a model of Lean with a universe for every nonnegative rational or something like that maybe.

[Mario Carneiro]

One property that is assumed by #leantt at least is that you can prove universe inequalities by "case analysis" on whether a universe variable u is 0 or succ u', i.e. proof by nat.cases_on. This would cause problems for a nonnegative rational model

[Mario Carneiro]

this is important for dealing with imax since it essentially has a definition by cases

[Mario Carneiro]

that's still not nearly enough to ensure that it is well founded though. An example non-well-founded model would be $\mathbb{N}\sqcup\mathbb{Z}$

[Mario Carneiro]

actually even $\mathbb{N}\sqcup\mathbb{Q}$ would probably work. You need it to start with the natural numbers but after that there aren't a whole lot of constraints

[Mario Carneiro]

I would be interested to know if there are partial order models too

[Gabriel Ebner]

Obviously every set-theoretic model of Lean has well-founded universes.

[Gabriel Ebner]

And if you don't need the model to be nice, you could just use (FOL) compactness to create models with nonstandard universes.

[Mario Carneiro]

Gabriel Ebner said:

Obviously every set-theoretic model of Lean has well-founded universes.

I don't think this is necessarily true - you are assuming each universe is in a $\in$ relation wrt all larger universes which isn't a requirement (I think?). For example you could have a bunch of universes $u_i$ such that $\dots<u_{i+1}<u_i<u_0<v$ and such that $\mathrm{suc}(u_i) = v$ for all $i$

[Gabriel Ebner]

Ah I guess we didn't specify the order on the universes.. edit: oh you mean via max..

[Gabriel Ebner]

My thought was that the cardinality strictly increases when you go the successor universe. But that doesn't work in the situation you've sketched.

[Mario Carneiro]

yeah, I think all the U_i can even be modeled as the same set

[Dean Young]

What an interesting discussion. Thanks for these helpful answers.

[Adam Topaz]

I’m still dreaming of being able to use universe inequalities in lean… but I’m starting to lose hope :(