Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • 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
  • Subject: Re: [Coq-Club] Agda with the excluded middle is inconsistent ?
  • Date: Fri, 8 Jan 2010 09:50:45 -0500 (EST)

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.''



Archive powered by MhonArc 2.6.16.

Top of Page