The Coq mailing list

[Gérard Huet <Gerard.Huet AT inria.fr>]

Any proof of unprovability of any proposition implies consistency of the 
logic, and thus is not internally verifiable (hopefully!)
GH

Le 18 avr. 2014 à 13:02, Matej Kosik 
<5764c029b688c1c0d24a2e97cd764f AT gmail.com>
 a écrit :

> Hi all,
> 
> I am slowly going through the CoqArt book.
> In Section 3.7.2 it is claimed that Peirce's formula
> 
>    ((P -> Q) -> P) -> P
> 
> is not provable (in Coq).
> 
> I am curious, how does the proof (of Pierce's formula unprovability in Coq) 
> look like?
> (up to that point, all concepts and exercises seem clear).
> 
> Thanks in advance for whatever help.