The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Thu, 26 May 2011 20:16:09 +0300,
Georgi Guninski 
<guninski AT guninski.com>
 a écrit :

> please excuse my dumbness.
> 
> is there a [Type] for which it is unprovable in coq if it is empty or
> not?
> 
> is it possible to define a [Type] in coq for which no one can prove
> in coq if it is empty or not?
> 
> 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?
> 

I have no good reference for that but you should take a look at this:

http://en.wikipedia.org/wiki/Gödel's_incompleteness_theorems

So as a consequence, as Coq is not a trivial axiomatic system, there
is a statement P (expressible in Coq) you cannot prove and for which you
cannot prove (P→False).

I guess there is a way to cast such a statement to True if there is a
proof and False else.

You can also consider the halting problem to try to build such a term.