coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proof Irrelevance <-> Function Extensionality?

From: Bas Spitters <b.a.w.spitters AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Proof Irrelevance <-> Function Extensionality?
Date: Tue, 20 Dec 2016 11:29:25 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=b.a.w.spitters AT gmail.com; spf=Pass smtp.mailfrom=b.a.w.spitters AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f179.google.com
Ironport-phdr: 9a23:W+oBkxDR76LeN7yk34uOUyQJP3N1i/DPJgcQr6AfoPdwSP77r8bcNUDSrc9gkEXOFd2CrakV0KyJ4uu5AiRAuc/H6y9SNsQUFlcssoY/oU8JOIa9E0r1LfrnPWQRPf9pcxtbxUy9KlVfA83kZlff8TWY5D8WHQjjZ0IufrymUqabtcm81viz9pvPeE0IwWPlOfIhZCmx+C7Wr4E9hZZoYvI6zQKMqX9VccxXw3lpLBSdhUCvyN23+ctJ+j8YgOog69JNS76yK65+RPpHSi8+Mnwp6dfwnRbGRAqLoHAbVzNFwVJzHwHZ4USiDd/KuSzgu784gXHCMA==

Without really thinking about it, I guess the following techniques
should work to show that neither is provable:
http://www.pédrot.fr/articles/cpp2017.pdf

On Tue, Dec 20, 2016 at 3:44 AM, Abhishek Anand
<abhishek.anand.iitg AT gmail.com>
wrote:
> Without using any axiom, can one prove either of the following?
>
> 1) Proof Irrelevance -> Function Extensionality
> 2) Function Extensionality -> Proof Irrelevance
>
> If not, is there a meta-theoretic argument about the unprovability of both
> of them?
>
> Thanks,
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/

[Coq-Club] Proof Irrelevance <-> Function Extensionality?, Abhishek Anand, 12/20/2016
- Re: [Coq-Club] Proof Irrelevance <-> Function Extensionality?, Bas Spitters, 12/20/2016
  - Re: [Coq-Club] Proof Irrelevance <-> Function Extensionality?, Talia Ringer, 12/20/2016
    - Re: [Coq-Club] Proof Irrelevance <-> Function Extensionality?, Talia Ringer, 12/20/2016
    - Re: [Coq-Club] Proof Irrelevance <-> Function Extensionality?, Bas Spitters, 12/20/2016
      - Re: [Coq-Club] Proof Irrelevance <-> Function Extensionality?, Abhishek Anand, 12/20/2016
        
        Re: [Coq-Club] Proof Irrelevance <-> Function Extensionality?, Jason Gross, 12/21/2016