Universe of pi type

Stream: general

[Sebastian Reichelt]

I have a basic question about universes in Lean: Would any known inconsistency arise if the type of (x : α) → β x with α : Sort u and β : α → Sort v was simply Sort v instead of Sort (imax u v)?
(I guess the answer must be "yes" because otherwise imax wouldn't need to exist, but I'd like to be sure because it seems to be a blocker for something I would like to do.)

[Yaël Dillies]

Do you mean Sort (max u v)?

[Sebastian Reichelt]

No, max would be much "worse" than imax of course; there wouldn't be any universally quantified propositions then as far as I understand. You can interpret my question as asking if "universally quantified data" can be treated in the same way as universally quantified propositions, or equivalently if the "size" of a function could just be the "size" of its output. I hope there is not some obvious type-theoretic reason why it cannot work.

[Reid Barton]

It can't be because e.g. Type -> bool has to be bigger than Type, so at least in the same universe as Type.

[Reid Barton]

You need LEM to cook up this kind of example, I think without it a system like this might be consistent, but it would be anticlassical.

[Reid Barton]

(the key phrase is "impredicative universe")

[Sebastian Reichelt]

Thanks, I'll check that out.
Just curious, is the Type -> bool example problematic only in the presence of choice, via propDecidable or something? (Assuming LEM as you say.)

[Reid Barton]

I mean there are definitely systems with an impredicative universe out there, but they are unsuitable for mathematics in the strong sense of proving classically false statements, so I don't know that much about exactly what you can and can't put into such a theory.

[Reid Barton]

But computer scientists often don't care about classical mathematics (because they cannot compute LEM anyways), so they think it is reasonable. System F is one of these systems, I understand.

[Sebastian Reichelt]

Ah, now I understand, you are arguing that α → Bool is set-theoretically larger than α, right? I missed that, oops. :-)

[Trebor Huang]

if you do that, there cannot be more than two universes (in which case we get the CoC). Otherwise your system contains a subsystem named System $U^-$, where you can formulate Girards paradox.

[Trebor Huang]

(I haven't really checked all the axioms of $U^-$ because I simply can't remember them, so correct me if I'm wrong.)

[Mario Carneiro]

@Trebor Huang See docs#girard

[Mario Carneiro]

Oh shoot, since it's been moved to the archive I can't find it in the docs anymore. @Rob Lewis What are your thoughts on this? Can we add the mathlib archive to docgen?

[Mario Carneiro]

You can find it at an old version of the mathlib docs: https://cs.brown.edu/courses/cs1951x/docs/logic/girard.html

[Yaël Dillies]

Exactly the same happened to Bhavik and I yesterday :sweat_smile:

[Yaël Dillies]

And, yes, documentation for the archive would be great.

[Eric Wieser]

https://github.com/leanprover-community/doc-gen/issues/147 tracks that task

[Eric Wieser]

Mario Carneiro said:

Trebor Huang See docs#girard

https://leanprover-community.github.io/mathlib_docs_demo/girard.html

[Mario Carneiro]

Oh, you fixed the archive links? :tada:

[Eric Wieser]

Yes, see https://github.com/leanprover-community/doc-gen/pull/176 and #general > docs archive.