coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] is there a [Type] for which it is unprovable in coq if it is empty or not?

From: Thierry Martinez <thierry.martinez AT inria.fr>
To: Georgi Guninski <guninski AT guninski.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] is there a [Type] for which it is unprovable in coq if it is empty or not?
Date: Fri, 27 May 2011 09:15:44 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type; b=D0Hn2RDugv3WFyhXdN/HESRR9qe2FM52ol9GFNmT8n6dgljzmzs1VooA5FczYnlp/X TvUAKXG24vTqquv+eVQfD/eW4OYwoqSMgMAQWLB0Q8R8n8MEp9fbkMAA/Psi6t4gPK5N j/4BhIM4HHHZtRALzlzxZ929wHwGJGixOzMbY=

On Thu, May 26, 2011 at 7:16 PM, Georgi Guninski
<guninski AT guninski.com>
wrote:
> related is: is it possible to define a Prop in coq for which no one can
> prove in coq if it is True or False?

The excluded middle (the proposition that "every Prop is either
provably true or false in coq") is itself neither provably true or
false in coq.

Definition excluded_middle := forall x: Prop, x \/ ~ x.

--
Thierry.

[Coq-Club] is there a [Type] for which it is unprovable in coq if it is empty or not?, Georgi Guninski
- Re: [Coq-Club] is there a [Type] for which it is unprovable in coq if it is empty or not?, AUGER Cedric
- Re: [Coq-Club] is there a [Type] for which it is unprovable in coq if it is empty or not?, Daniel Schepler
- <Possible follow-ups>
- Re: [Coq-Club] is there a [Type] for which it is unprovable in coq if it is empty or not?, Thierry Martinez