[Agda] Agda with the excluded middle is inconsistent ?

[Chung Kil Hur]

Hi,

I need to mention one more thing.

Indeed, the injectivity of inductive type constructor is inconsistent in the prsence of Prop without LEM.

Actually, the original idea came from Alexandre Miquel.
He told Hugo that the injectivity of type constroctors for inductive familes of Prop is inconsistent without any help of axioms like "P <-> Q" -> "P = Q".

His proof in Coq is as follows:

----------------------------------------------------------------------
Inductive I : (Prop -> Prop) -> Prop := .

Axiom inj_I : forall x y, I x = I y -> x = y.

Definition R (x : Prop) := forall p, x = I p -> ~ p x.

Lemma R_eqv :
  forall p, R (I p) <-> ~ p (I p).

Proof.
split; intros.
 unfold R; apply H.
 reflexivity.
 unfold R; intros q H0.
 rewrite <- (inj_I p q H0).
 assumption.
Qed.

Lemma R_eqv_not_R :
  R (I R) <-> ~ R (I R).

Proof (R_eqv R).

Lemma absurd : False.

Proof.
destruct R_eqv_not_R.
exact (H (H0 (fun x => H x x)) (H0 (fun x => H x x))).
Qed.
-----------------------------------------------------

From this proof, I realized it can be applied to Set as well.

-----------------------------------------------------
Inductive I : (Set -> Set) -> Set := 
| i1 : I (fun x => x)
| i2 : I (fun x => x)
.

Axiom inj_I : forall x y, I x = I y -> x = y.

Definition R (x : Set) : Set := forall p: Set -> Set, x = I p -> p x -> False.

Lemma R_eqv_1 :
  forall p, R (I p) -> (p (I p) -> False).

Proof.
intros ? ?. 
  apply H. reflexivity.
Qed.

Lemma R_eqv_2 :
  forall p, (p (I p) -> False) -> R (I p).

intros.
 unfold R; intros q H0.
 rewrite <- (inj_I p q H0).
 assumption.
Qed.

Lemma R_eqv_not_R_1 :
  R (I R) -> R (I R) -> False.

Proof (R_eqv_1 R).

Lemma R_eqv_not_R_2 :
  (R (I R) -> False) -> R (I R).

Proof (R_eqv_2 R).

Lemma absurd : False.

Proof.
set (H := R_eqv_not_R_1).
set (H0 := R_eqv_not_R_2).

exact (H (H0 (fun x => H x x)) (H0 (fun x => H x x))).
Qed.
------------------------------------------------

But, in this proof, we need to notice that we use "False : Prop" rather than "Empty_set : Set".
If you change "False" to "Empty_set", then the type of R cannot be "Set -> Set", rather it should "Set -> Type".
The reason why R is typable as Set -> Set is due to the impredicativity of Prop, because R is typepable as Set -> Prop, which is
coercible to Set -> Set.
This proof does not need any axiom, but just the impredicativity of Prop.

So, this idea does not aplly to Agda because it does not have any impredicative set like Prop.
So, I applied cantor's diagonalization assuming the law of excluded middle.

I think the presence of Prop is one of the fancy features of Coq as a proof assistant (at least to me).
So, the injectivity seems unatural to me in this view point.

Cheers,
Chung-Kil Hur


----- Original Message ----- 
  From: Chung Kil Hur 
  To: Agda mailing list ; coq-club at inria.fr 
  Sent: Thursday, January 07, 2010 12:59 AM
  Subject: [Agda] Agda with the excluded middle is inconsistent ?


  Hi everyone,

  I proved the absurdity in Agda assuming the excluded middle.
  Is it a well-known fact ?
  It seems that Agda's set theory is weird.

  This comes from the injectivity of inductive type constructors.

  The proof sketch is as follows.

  Define a family of inductive type

  data I : (Set -> Set) -> Set where

  with no constructors.

  By injectivity of type constructors, I can show that I : (Set -> Set) -> Set is injective.

  As you may see, there is a size problem with this injectivity.

  So, I just used the cantor's diagonalization to derive absurdity in a classical way.

  Does anyone know whether cantor's diagonalization essentially needs the classical axiom, or can be done intuitionistically ?
  If the latter is true, then the Agda system is inconsistent.

  Please have a look at the Agda code below, and let me know if there's any mistakes.

  All comments are wellcome.

  Thanks,
  Chung-Kil Hur


  ============== Agda code ===============

  module cantor where

    data Empty : Set where

    data One : Set where
      one : One

    data coprod (A : Set1) (B : Set1) : Set1 where
      inl : ∀ (a : A) -> coprod A B
      inr : ∀ (b : B) -> coprod A B 

    postulate exmid : ∀ (A : Set1) -> coprod A (A -> Empty)

    data Eq1 {A : Set1} (x : A) : A -> Set1 where
      refleq1 : Eq1 x x

    cast : ∀ { A B } -> Eq1 A B -> A -> B
    cast refleq1 a = a

    Eq1cong : ∀ {f g : Set -> Set} a -> Eq1 f g -> Eq1 (f a) (g a)
    Eq1cong a refleq1 = refleq1

    Eq1sym : ∀ {A : Set1} { x y : A } -> Eq1 x y -> Eq1 y x
    Eq1sym refleq1 = refleq1

    Eq1trans : ∀ {A : Set1} { x y z : A } -> Eq1 x y -> Eq1 y z -> Eq1 x z
    Eq1trans refleq1 refleq1 = refleq1

    data I : (Set -> Set) -> Set where

    Iinj : ∀ { x y : Set -> Set } -> Eq1 (I x) (I y) -> Eq1 x y 
    Iinj refleq1 = refleq1

    data invimageI (a : Set) : Set1 where
      invelmtI : forall x -> (Eq1 (I x) a) -> invimageI a

    J : Set -> (Set -> Set)
    J a with exmid (invimageI a)
    J a | inl (invelmtI x y) = x
    J a | inr b = λ x → Empty

    data invimageJ (x : Set -> Set) : Set1 where
      invelmtJ : forall a -> (Eq1 (J a) x) -> invimageJ x

    IJIeqI : ∀ x -> Eq1 (I (J (I x))) (I x)
    IJIeqI x with exmid (invimageI (I x))
    IJIeqI x | inl (invelmtI x' y) = y
    IJIeqI x | inr b with b (invelmtI x refleq1)
    IJIeqI x | inr b | ()

    J_srj : ∀ (x : Set -> Set) -> invimageJ x
    J_srj x = invelmtJ (I x) (Iinj (IJIeqI x))

    cantor : Set -> Set
    cantor a with exmid (Eq1 (J a a) Empty)
    cantor a | inl a' = One
    cantor a | inr b = Empty

    OneNeqEmpty : Eq1 One Empty -> Empty
    OneNeqEmpty p = cast p one

    cantorone : ∀ a -> Eq1 (J a a) Empty -> Eq1 (cantor a) One 
    cantorone a p with exmid (Eq1 (J a a) Empty)
    cantorone a p | inl a' = refleq1
    cantorone a p | inr b with b p
    cantorone a p | inr b | ()

    cantorempty : ∀ a -> (Eq1 (J a a) Empty -> Empty) -> Eq1 (cantor a) Empty
    cantorempty a p with exmid (Eq1 (J a a) Empty)
    cantorempty a p | inl a' with p a'
    cantorempty a p | inl a' | ()
    cantorempty a p | inr b = refleq1

    cantorcase : ∀ a -> Eq1 cantor (J a) -> Empty
    cantorcase a pf with exmid (Eq1 (J a a) Empty)
    cantorcase a pf | inl a' = OneNeqEmpty (Eq1trans (Eq1trans (Eq1sym (cantorone a a')) (Eq1cong a pf)) a')
    cantorcase a pf | inr b = b (Eq1trans (Eq1sym (Eq1cong a pf)) (cantorempty a b))

    absurd : Empty
    absurd with (J_srj cantor)
    absurd | invelmtJ a y = cantorcase a (Eq1sym y)

  =====================================




------------------------------------------------------------------------------


  _______________________________________________
  Agda mailing list
  Agda at lists.chalmers.se
  https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100107/e3310d04/attachment-0001.html