[Agda] Re: [Coq-Club] Agda with the excluded middle is inconsistent ?

[Chung Kil Hur]

----- Original Message ----- 
From: <roconnor at theorem.ca>
To: "Chung Kil Hur" <ckh25 at cam.ac.uk>
Cc: "Agda mailing list" <agda at lists.chalmers.se>; <coq-club at inria.fr>
Sent: Friday, January 08, 2010 3:50 PM
Subject: Re: [Coq-Club] Agda with the excluded middle is inconsistent ?


>I spent some time trying to extend Chung-Kil's proof to an outright 
> contradiction, but Agda's predicativity thwarted my attempts.  If Agda had 
> an impredictiave Prop universe like Coq does, there would be an outright 
> contradiciton.  Below is my proof that Coq has non-injective type 
> constructors:
> 
> Definition Type1 := Type.
> 
> Inductive I : (Type1 -> Type1) -> Type1 := .
> 
> Section ChungKil.
> 
> Hypothesis InjI : forall x y, I x = I y -> x = y.
> 
> Definition P (x:Type1) : Type1 := exists a, I a = x /\ (inhabited (a x) -> False).
> 
> Definition p := I P.
> 
> Lemma contradiction : inhabited (P p) <-> (inhabited (P p) -> False).
> Proof.
> unfold P at 1.
> unfold p at 1.
> split.
>  intros [[a [Ha0 Ha1]]].
>  replace a with P in Ha1; [assumption|].
>  firstorder.
> intros H.
> constructor.
> exists P.
> firstorder.
> Qed.
> 
> Lemma absurd : False.
> assert (Z:=contradiction).
> tauto.
> Qed.
> 
> End ChungKil.
> 
> -- 
> Russell O'Connor                                      <http://r6.ca/>
> ``All talk about `theft,''' the general counsel of the American Graphophone
> Company wrote, ``is the merest claptrap, for there exists no property in
> ideas musical, literary or artistic, except as defined by statute.''

Hi Russel,

I posted a similar proof yesterday, which is originally from Alexandre Miquel's idea.
But, I think I sent it to the Agda list only.

Here is what I wrote.

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

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

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