The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

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.