Zulip Chat Archive

Stream: general

Topic: universe enlargement


view this post on Zulip Reid Barton (Apr 22 2020 at 13:12):

Suppose I have a universe-polymorphic proposition P.{u} : Prop and a proof of P.{u0} as a term (either in the empty context, or, ideally, in a context which only contains variables whose types are Type v for v <= u0). Is it then true that I can also prove P.{u1}, for any u1 >= u0?

view this post on Zulip Reid Barton (Apr 22 2020 at 13:12):

Is this something I could prove just by inducting over the proof term?

view this post on Zulip Reid Barton (Apr 22 2020 at 13:12):

Obviously it depends on my axioms, since for example I could consistently assume that Type 0 has no inaccessibles, which I can prove is false in Type 1. I mean using the usual axioms of Lean.

view this post on Zulip Mario Carneiro (Apr 22 2020 at 14:01):

Let P.{u} = |Type u| < |Type 1| and u0 = 0

view this post on Zulip Mario Carneiro (Apr 22 2020 at 14:03):

You need only the usual axioms to prove that P.{0} is true and P.{1} is false

view this post on Zulip Reid Barton (Apr 22 2020 at 14:12):

Hmm, right. I need to find a better way to express what I mean.

view this post on Zulip Mario Carneiro (Apr 22 2020 at 14:17):

One true thing is that there is a model of lean where the universes are any increasing countable sequence of inaccessibles, not necessarily the minimal one, which suggests that it is possible to convert any proof using universes Type 0, ..., Type k into one using Type u_0, ..., Type u_k where u_0 < ... < u_k. However this is not so easy because of the existence of the universe successor function: Type 0 has type Type 1 but Type u_0 does not have type Type u_1. So this doesn't work without modification


Last updated: May 06 2021 at 21:09 UTC