[TYPES] Impredicative Set and large elimination

[Thomas Streicher]

Though I am not fully aware of what pecisely is the precise type
system form general type theoretic knowledge my anser is as follows.

As long as Prop is not an element of Set there is no problem to assume
both Set and Prop as impredicative. Look at the realizability model
where types are interpreted as assemblies, Set as modest sets and Prop
as subterminal modes sets.
These models all validate large elimination.

But if Prop \in Set then then Girard's papardox applies.

Thomas



> I'm trying to find some references for what is and isn't allowed with
> what's known as an impredicative Set universe in Coq.
> There's several references and explanations such as this issue [1] that
> say that an impredicative Prop universe combined with unrestricted
> elimination and excluded middle yields a contradiction.
> I've also found this [2] saying that in Coq, "large" inductives in an
> impredicative Set with constructors with arguments in larger universes
> have elimination restricted to Prop and Set only,
> presumably to also allow postulating an excluded middle axiom. 
> 
> Suppose I had a large inductive in impredicative Set and I do not
> postulate excluded middle (or double negation elimination, or choice, or
> indefinite description, etc.):
> can I eliminate my inductive into large universes, i.e. Type, while
> maintaining consistency?
> Are there any references that discuss the consequences of having an
> impredicative Set and other inconsistencies I should watch out for?
> I will not be postulating any axioms that aren't part of CIC, but I am
> wondering about whether I can have an impredicative Prop subtype an
> impredicative Set,
> and whether making the theory extensional (with equality reflection)
> would at all interfere with consistency. 
> 
> Regards,
> Jonathan 
> 
> [1] https://github.com/FStarLang/FStar/issues/360
> [2] http://adam.chlipala.net/cpdt/html/Universes.html#lab80