coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] is there a [Type] for which it is unprovable in coq if it is empty or not?

From: Daniel Schepler <dschepler AT gmail.com>
To: coq-club AT inria.fr
Cc: Georgi Guninski <guninski AT guninski.com>
Subject: Re: [Coq-Club] is there a [Type] for which it is unprovable in coq if it is empty or not?
Date: Thu, 26 May 2011 10:42:52 -0700
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=from:to:subject:date:user-agent:cc:references:in-reply-to :mime-version:content-type:content-transfer-encoding:message-id; b=hILKPF4PQmd23dRkFVCFyK5bhDm3yS5gkhp8SdXkqsOYDVYuvXRr0sXrGaWdeeRK33 4x+LSA9l1gc6ol3QZ9U6kGYDxxRIrdEP22/sTPR//TrmxAa1TXiDuOqsR7FpD5OTep2v M8oxoKy2doQWiyEqkOL6ETWgk0IF20SVSRQ54=

On Thursday 26 May 2011 10:16:09 Georgi Guninski wrote:
> please excuse my dumbness.
>
> is there a [Type] for which it is unprovable in coq if it is empty or not?
>
> is it possible to define a [Type] in coq for which no one can prove in coq
> if it is empty or not?
>
> related is: is it possible to define a Prop in coq for which no one can
> prove in coq if it is True or False?

How about using the continuum hypothesis?

Inductive Cardinal : Type :=
| cardinality : Type -> Cardinal.

Inductive cardinal_le : Cardinal -> Cardinal -> Prop :=
| inj_cardinal_le : forall `(f:X->Y), injective f ->
  cardinal_le (cardinality X) (cardinality Y).
Definition cardinal_lt (kappa lambda:Cardinal) : Prop :=
  cardinal_le kappa lambda /\ ~ cardinal_le lambda kappa.

Definition emptyness_undecidable :=
  { X : Type | cardinal_lt (cardinality nat) (cardinality X) /\
       cardinal_lt (cardinality X) (cardinality (nat->bool)) }.
Definition undecidable_Prop :=
  exists X:Type, cardinal_lt ... /\ cardinal_lt ...

That's undecidable even assuming classic /\ choice.
--
Daniel Schepler

[Coq-Club] is there a [Type] for which it is unprovable in coq if it is empty or not?, Georgi Guninski
- Re: [Coq-Club] is there a [Type] for which it is unprovable in coq if it is empty or not?, AUGER Cedric
- Re: [Coq-Club] is there a [Type] for which it is unprovable in coq if it is empty or not?, Daniel Schepler
- <Possible follow-ups>
- Re: [Coq-Club] is there a [Type] for which it is unprovable in coq if it is empty or not?, Thierry Martinez