The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

I stand corrected, thanks!

Le samedi 13 septembre 2014, Jonathan <jonikelee AT gmail.com> a écrit :

On 09/12/2014 07:59 PM, Robert Dockins wrote:

You can get this from the Hurkens paradox; see below.

Cheers,
   Rob

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


Require Hurkens.

Inductive Erasable(A : Type) : Prop := erasable: A -> Erasable A.
Arguments erasable [A] _.
Axiom Erasable_inj : forall {A : Type}{a b : A}, erasable a=erasable b -> a=b.


Definition er_out (X:Erasable Prop) : Prop
    := exists P, X = @erasable Prop P /\ P.

Theorem inconsistent : False.
Proof.
   apply (Hurkens.paradox (Erasable Prop) (@erasable Prop) er_out).

   intros.
   destruct H as [P [H1 H2]].
   apply Erasable_inj in H1.
   subst A. trivial.

   red; intros.
   exists A; split; auto.
Qed.

Check inconsistent.
Print Assumptions inconsistent.

I needed to add Import Hurkens.NoRetractFromSmallPropositionToProp. and use "paradox" unqualified, for some reason - but otherwise it does work (I'm using a trunk version).  Are things just as bad if I limit Erasable to be over Set instead of Type?  That would be somewhat limiting, but maybe still sufficiently useful.  Or, if there was a way to limit it to non-universe instances of Type?

Still - the proof (in Daniel Shepler's response) that it is incompatible with specific proof irrelevance is also upsetting - and that would remain even if limited to Set.  Although I haven't yet required any variety of proof irrelevance.

Well, either I have to hope reality is sufficiently paraconsistent, or investigate an alternative erasability mechanism.  Maybe the one Daniel Shepler is suggesting is suitable.

Or switch to Idris.

-- Jonathan

--