[Agda] Re: [Coq-Club] Agda with the excluded middle is inconsistent
?
roconnor at theorem.ca
roconnor at theorem.ca
Fri Jan 8 22:36:22 CET 2010
On Fri, 8 Jan 2010, Chung Kil Hur wrote:
> But, in this proof, we need to notice that we use "False : Prop" rather than "Empty_set : Set".
> If you change "False" to "Empty_set", then the type of R cannot be "Set -> Set", rather it should "Set -> Type".
> The reason why R is typable as Set -> Set is due to the impredicativity of Prop, because R is typepable as Set -> Prop, which is
> coercible to Set -> Set.
Ah, I didn't realize that Set was coercable to Prop otherwise I wouldn't
have done my Type1 nonsense.
> This proof does not need any axiom, but just the impredicativity of Prop.
>
> So, this idea does not aplly to Agda because it does not have any impredicative set like Prop.
> So, I applied cantor's diagonalization assuming the law of excluded middle.
>
> I think the presence of Prop is one of the fancy features of Coq as a proof assistant (at least to me).
> So, the injectivity seems unatural to me in this view point.
To be honest, the impredicativity of Prop in Coq worries me just a little
<http://r6.ca/blog/20091101T231201Z.html>
"Coq’s impredicative in Prop seems innocent because no information is
allowed to flow from the Prop universe to the Set universe; however Prop
values can witness termination of functions in Set. Perhaps there is an
inconsistency arising from the impredicativity of Prop that “proves” the
termination of some non-terminating function.
But worries about impredicativity is another story.
Thanks repeating the info on the Agda list for me.
--
Russell O'Connor <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''
More information about the Agda
mailing list