The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

Hi Jay,

The question is what is the justification of an impredicative universe? Per 
Martin-Loef pointed out a while ago that the only reason to  think that Prop 
is small comes from the classical idea that Prop=Bool. I can't see a better 
one. Obviously there is the fundamental question whether you only want to use 
principles for which you have positive reasons to believe in, or whether you 
are happy to use some which are not known to be inconsistent (this is 
classical reasoning on the metalevel).

One reason to be suspicious of impredicativity is that you can only have it 
once, we know from Girard that we can only have it once. That is once you 
understand impredicativity then why should it not be valid for any universe? 
However, as soon as you have 2 impredicative universes you are dead. Also if 
you look at Girard's paradox a bit more closely you find that you can 
actually encode the Russell universe an an impredicative universe and as soon 
as you have Lambek's lemma (we can prove that the destructor is inverse to 
the constructor) you can derive the paradox. Hence the somehow disconcerting 
property of impredicative encodings is that as soon as you assume them to be 
strong you are inconsistent.

Maybe you can tell us for what you actually want to use an impredicative 
universe?

Thorsten

On 15/03/2019, 18:35, 
"coq-club-request AT inria.fr
 on behalf of Jay Kruer" 
<coq-club-request AT inria.fr
 on behalf of 
kruerj AT reed.edu>
 wrote:

    Hi coq-club,
    
    I am wondering how “sketchy” the use of impredicative Set in Coq 
developments is considered. I have seen that impredicative Set is 
inconsistent with some axioms of classical mathematics (e.g. excluded 
middle), but for the careful user who avoids such axioms (or needs no axioms 
in their development at all) is there any reason to avoid it? The Coq 
reference manual alludes to some intuitionists taking issue with 
impredicative Set even before one introduces inconsistency with axioms but I 
haven't been able to find any of those arguments.
    
    Thanks,
    — Jay




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.