coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Deriving False from bool : Prop?

From: roux cody <cody.roux AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Deriving False from bool : Prop?
Date: Wed, 27 Jan 2016 09:49:16 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=cody.roux AT gmail.com; spf=Pass smtp.mailfrom=cody.roux AT gmail.com; spf=None smtp.helo=postmaster AT mail-ob0-f169.google.com
Ironport-phdr: 9a23:ssoRCByLqLMxYTfXCy+O+j09IxM/srCxBDY+r6Qd0ekUIJqq85mqBkHD//Il1AaPBtWEraoewLSH+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStGU1578ibH60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mosVHSODxe7kyZb1eFjUvdW4vt+PxshyWVwyS9jMXVWkH2k5DBATUqgv9Q4fZvS7zt+470y6fa56lBYsoUCivuv84ACTjjz0KYmY0

The consistency proof is quite tricky though, even without universes. Impredicative set is quite brittle, being in particular anti-classical. On a related note, does anyone know of a proof of consistency *with* universes? The only proofs that I know of are Werner's proof of normalization and Altenkirch's Lambda-set model, which afaik haven't been generalized to systems with universes.

Thanks,

Cody

On Wed, Jan 27, 2016 at 4:26 AM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

It's consistent. Set with --impredicative-set is like that.

On 27 January 2016 at 08:44, Jason Gross <jasongross9 AT gmail.com> wrote:
Is it possible to derive [False] from the assumption that you have [T : Prop] with [a b : T] and [a <> b]? (On the flip side, is it possible to show that it's consistent to assume this?)

Thanks,
Jason

[Coq-Club] Deriving False from bool : Prop?, Jason Gross, 01/27/2016
- Re: [Coq-Club] Deriving False from bool : Prop?, Arnaud Spiwack, 01/27/2016
  - Re: [Coq-Club] Deriving False from bool : Prop?, roux cody, 01/27/2016
    - Re: [Coq-Club] Deriving False from bool : Prop?, Eddy Westbrook, 01/27/2016
      - Re: [Coq-Club] Deriving False from bool : Prop?, Thorsten Altenkirch, 01/27/2016
        
        Re: [Coq-Club] Deriving False from bool : Prop?, Eddy Westbrook, 01/27/2016
        
        Re: [Coq-Club] Deriving False from bool : Prop?, roux cody, 01/27/2016
        
        Re: [Coq-Club] Deriving False from bool : Prop?, Thorsten Altenkirch, 01/28/2016
        Re: [Coq-Club] Deriving False from bool : Prop?, Bob Atkey, 01/28/2016