coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] unprovable propositions in Coq

From: David Monniaux <david.monniaux AT imag.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] unprovable propositions in Coq
Date: Fri, 18 Apr 2014 13:11:19 +0200 (CEST)
Mailscanner-null-check: 1398424279.22326@FJbXK74YT+ZyQlwR0ES9Sg

----- Mail original -----
> 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 suspect you can try looking for a normal form (no redex) of such a proof,
then find that there is none.

[Coq-Club] unprovable propositions in Coq, Matej Kosik, 04/18/2014
- Re: [Coq-Club] unprovable propositions in Coq, David Monniaux, 04/18/2014
- Re: [Coq-Club] unprovable propositions in Coq, Gabriel Scherer, 04/18/2014
  - Re: [Coq-Club] unprovable propositions in Coq, Daniel Schepler, 04/18/2014
    - Re: [Coq-Club] unprovable propositions in Coq, Gérard Huet, 04/18/2014
      - Re: [Coq-Club] unprovable propositions in Coq, Daniel Schepler, 04/18/2014
  - Re: [Coq-Club] unprovable propositions in Coq, Matej Kosik, 04/18/2014
- Re: [Coq-Club] unprovable propositions in Coq, Gérard Huet, 04/18/2014
- Re: [Coq-Club] unprovable propositions in Coq, Altenkirch Thorsten, 04/18/2014