coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Not sure if this is the right forum for beginners' questions, however .....

From: t x <txrev319 AT gmail.com>
To: Satrajit Roy <satrajit.roy AT gmail.com>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Not sure if this is the right forum for beginners' questions, however .....
Date: Fri, 6 Sep 2013 23:39:09 +0000

I believe you need the law of excluded middle. In general, you can't prove

forall (P: Type), P \/ ~P.

Software Foundtaions / Pierce has a nice exercise showing that 5 statements (related to law of excluded middle) are equivalent.

On Fri, Sep 6, 2013 at 11:27 PM, Satrajit Roy <satrajit.roy AT gmail.com> wrote:

Why can't I prove:

forall p:Type->Prop, ~(forall q:Type, (p q))->(exists q:Type, ~(p q))

When I can easily prove:

forall p:Type->Prop, exists q, ~p q->~forall q, p q

or prove:

forall p:Type->Prop, ~exists q, p q->forall q, ~p q

or even prove:

forall p:Type->Prop, forall q, p q->~exists q, ~p q

--

Satrajit

[Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., Satrajit Roy, 09/07/2013
- Re: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., t x, 09/07/2013
- Re: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., Adam Chlipala, 09/07/2013
  - Re: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., Andrew Hirsch, 09/08/2013
    - RE: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., Shigeo Nishi, 09/08/2013
      - Re: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., Adam Chlipala, 09/08/2013
        
        RE: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., Shigeo Nishi, 09/08/2013
        
        Re: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., t x, 09/08/2013