Follow

You can't have two impredicative universes. You can't have Type: Type. You can't have impredicative strong pairs. You can't have large elimination of an impredicative universe. You can't have positive datatypes when you have an impredicative universe. You can't this, you can't that. When will it end?

Interesting to note is that the only reason you can't eliminate something in Prop to something in a larger type in Coq is because they allow any inductive definition to be in Prop
If you restrict what kind of inductive definitions are allowed to be in Prop (in the same way Def. Proof Irrel. w/o K does*), then you can do large elimination of Props, because there's nothing meaningful you can eliminate it to in a larger universe

* i.e. constructors are orthogonal, non-forced arguments are in Prop, something something about termination

Coq actually has this "you can eliminate Props if it has no constructors or only a singleton constructor with Prop arguments" exception to eliminating Props that's basically a subset of the larger conditions from Def. Proof Irrel.
It doesn't seem to cover the termination thing but I'm not sure if that'll lead to an inconsistency or if it's just a decidable type checking thing

One more to add: You can't have both impredicative Prop and propositional extensionality, but that only yields a non-normalization, not an inconsistency
I don't think non-normalization implies inconsistency? The same way consistency doesn't necessarily imply normalization... I think?

Thinking about this again. Type: Type gives you Girard's paradox, and so does arbitrary large elimination of something in an impredicative universe, since that lets you squish something from a bigger universe to a smaller universe, which is basically the effect of Type: Type
You can't have negative datatypes because you can prove false pretty easily, and you can't have non-strictly-positive datatypes with impredicativity because... why? I did it once in Coq but I don't understand what it is I did
And finally I don't know you can't have strong impredicative pairs but I suspect it's along the same lines as large elimination of impredicative universes

Yeah that sounds right: if you have strong impredicative pairs, you can stick a bigger thing and pretend it's a Prop, and then later on pop the thing out, which is the same as being able to eliminate things in Prop to arbitrary universes, which is the same as Type in Type

@ionchy I am convinced non-normalization does not mean inconsistency (proof: otherwise my PhD work in Lean would be worthless and we can't have that!)

But yes, since consistency doesn't necessarily imply normalization, the contrapositive (non-normalizing implies inconstency) also doesn't hold.

Sign in to participate in the conversation
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.