coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Excluded middle and decidable equality

From: "N. Raghavendra" <raghu AT hri.res.in>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Excluded middle and decidable equality
Date: Wed, 02 Oct 2013 19:07:45 +0530
Cancel-lock: sha1:nq1aMO696SCXsA/FsRApv9mm4Mk=

At 2013-10-02T14:36:05+02:00, Cedric Auger wrote:

> I guess he meant "(exmid_eq X → exmid_appears_in X) ∧
> (exmid_appears_in X → pingeonhole_principle X) ∧
> (pigeonhole_principle X → exmid_eq X)"

Yes, that's what I meant! Anyway, it has been pointed out that I'd
assumed another axiom in my proof of the last implication, and that in
fact the pigeonhole principle as stated doesn't need any decidability
hypotheses for its proof.

Best regards,
Raghu.

--
N. Raghavendra
<raghu AT hri.res.in>,
http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/

Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 10/02/2013
- Re: [Coq-Club] Excluded middle and decidable equality, Daniel Schepler, 10/02/2013
  - Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 10/02/2013
    - Re: [Coq-Club] Excluded middle and decidable equality, Jason Gross, 10/02/2013
      - Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 10/02/2013
    - Re: [Coq-Club] Excluded middle and decidable equality, Alan Schmitt, 10/02/2013
      - Re: [Coq-Club] Excluded middle and decidable equality, Cedric Auger, 10/02/2013
        
        Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 10/02/2013
  - Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 10/04/2013