The Coq mailing list

[Robert Dockins <robdockins AT fastmail.fm>]

On Sep 12, 2014, at 3:19 PM, Jonathan 
<jonikelee AT gmail.com>
 wrote:

> On 09/12/2014 06:10 PM, Adam Chlipala wrote:
>> On 09/12/2014 06:04 PM, Jonathan wrote:
>>> 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.
>> 
>> We did the same thing in Ynot, and I think this axiom turned out to be 
>> inconsistent, period.  You don't need to assume any others to run into 
>> trouble.  I don't remember the details of the proof, though.
> 
> Wow - really?  Does anyone remember those details?

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.