The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Hello,

I just ported Herman's Lego formalization [1] to Coq. Together with the 
Type-in-Type patch [2], this gives a nice proof of False.

Robbert

[1] http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz
[2] 
https://raw.github.com/vladimirias/Foundations/master/Coq_patches/patch.type-in-type

Definition V :=
  forall A : Type, ((A->Type)->(A->Type))->A->Type.
Definition U :=
  V->Type.
Definition sb (A : Type) (r : (A->Type)->(A->Type)) (a : A) : U :=
  fun z : V => r (z _ r) a.
Definition le (i : U->Type) (x : U) : Type :=
  x (fun (A : Type) (r : (A->Type)->(A->Type)) (a : A) => i (sb _ r a)).
Definition induct (i : U->Type) : Type :=
  forall x : U, le i x->i x.
Definition WF : U :=
  fun (z : V) => induct (z _ le).

Section hurkens.
  Context (B : Type).

  Definition I (x : U) : Type :=
    (forall i : U->Type, le i x->i (sb _ le x))->B.

  Definition omega (i : U->Type) (y : induct i) : i WF :=
    y WF (fun x => y (sb _ le x)).
  Definition lemma : induct I :=
    fun x p q => q I p (fun i => q (fun y => i (sb _ le y))).
  Definition lemma2 (x : forall (i : U->Type), induct i->i WF) : B :=
    x I lemma (fun (i : U->Type) => x (fun y => i (sb _ le y))).
  Definition paradox : B := lemma2 omega.
End hurkens.

Goal False.
Proof. apply paradox. Qed.

On 05/05/2012 12:26 PM, James McKinna wrote:
> Daniel,
>
> and friends on the co-club list.
>
> Please find below the LEGO formalisation (1995ish?) by Herman Geuvers of
> Tonny Hurkens' argument.
> Needs Type in Type (obv.),and should be readily translatable into
> Coq/Gallina.
> Bindings [x:A] correspond to Hypothesis/Axiom declarations,
> [x:A= M] to Definitions, etc.
>
> best,
>
> James McKinna
>
> Daniel Schepler wrote:
> > On Fri, May 4, 2012 at 9:36 PM, Randy Pollack 
> > <rpollack0 AT gmail.com>
> > wrote:
> > > Hurken's paradox, TLCA 1995.
> >
> > Umm, could you be more specific? When I tried a Google search on
> > those terms, all I got was some random Agda patch where "Hurken's
> > paradox" was just by itself in the middle with no context. And afaict
> > HurkensParadox.v in the Coq source would require something like
> > Axiom classicT : forall {X:Type}, X + (X -> False).
> ===============
>
>
> [V = {A|Type}((A->Type)->(A->Type))->A->Type];
>
> [U = V->Type];
>
> [sb [A|Type][r:(A->Type)->(A->Type)][a:A] = [z:V]r (z r) a : U];
>
> [le [i:U->Type][x:U] =
> x ([A|Type][r:(A->Type)->(A->Type)][a:A]i (sb r a)) : Type];
>
> [induct [i:U->Type] = {x:U}(le i x)->i x : Type];
>
> [WF = [z:V]induct (z le) : U];
>
> [B:Type];
> [I [x:U] = ({i:U->Type}(le i x)->i (sb le x))->B : Type];
>
> Goal {i:U->Type}(induct i)->i WF;
> intros i y;
> Refine y WF ([x:U]y (sb le x));
> Save omega;
>
> Goal induct I;
> Intros x p q;
> Refine q I p ([i:U->Type]q ([y:U]i (sb le y)));
> Save lemma;
>
> Goal ({i:U->Type}(induct i)->i WF)->B;
> intros x;
> Refine x I lemma ([i:U->Type]x ([y:U]i (sb le y)));
> Save lemma2;
>
> Goal B;
> Refine lemma2 omega;
> Save paradox;