The Coq mailing list

["Carlos.SIMPSON" <carlos AT math.unice.fr>]

Hi. Thanks very much to Alexandre Miquel for a beautiful suggestion.

In case anybody is interested, here is the reason I was asking the
question. (I am sorry if this point has already been discussed...)
 If you prove a proposition in one file, and that proposition
contains two or more instances of the word Type, then it can be
dangerous to transpose that proposition to another file as an Axiom.
This is because the proof of the proposition introduces constraints
on the indexing of the words ``Type'' occuring in the proposition 
but the constraints are lost when the proposition is stated as an axiom.

My example is missing a part which I assume exists, basically saying
that the statement Type : Type (without a hierarchy) is inconsistent
due to Russell's paradox. (Somebody should correct me if I am wrong about 
this).
 Apart from that, try compiling the file two times, one with line AAA
(which is the proof of the proposition)
commented out and one with it put back in. 

Sincerely,
Carlos Simpson


Here is the file: 


Definition Type2 := Type.
Definition Type1 : Type2 := Type.


Definition DOESNT_EXIST := [A:Type][P:A-> Prop] (a:A) ((P a) -> False).

(* Here is existence *)
Definition EXISTS : (A:Type)(P:A->Prop)Prop 
        := [A:Type][P:A->Prop](DOESNT_EXIST A P)-> False.
        
(* Here is the type of thing which illustrates how to obtain a problem
if you don't use the above type indexing convention *)

        
Definition strange_prop : Prop := (A : Type) (EXISTS Type ([B:Type] (A == B)) 
).

Section now_we_prove_it_locally.

Variable A : Type.
Local Q: Type -> Prop := ([B:Type] (A == B)).
Variable hyp : (DOESNT_EXIST Type Q).
Local hyp2 : (a: Type) ((Q a) -> False) := hyp.
Local step1 : ((Q A) -> False) := (hyp2 A).
Local step2 : (Q A) := (refl_eqT Type A).
Definition step3 : False := (step1 step2).

End now_we_prove_it_locally.

(* The following line is denoted AAA below 
---if you remove the comments then it compiles, saying that
strange_prop can be proved   *)
(*
Definition strange_prop_proof : strange_prop := step3. 
*)


Axiom strange_axiom : strange_prop.


Definition p :(EXISTS Type ([B:Type]Type1==B)) := (strange_axiom Type1).



(* it seems to me that one can prove the following 
statement using Russell's paradox if excluded middle is assumed *)
(* of course my example isnt complete until I furnish this proof! *)
(* Note however that following Werner's principle the projection of this
statement into ZFC_2 is certainly consistent...*)


Parameter contra : (DOESNT_EXIST Type1 ([B:Type1]Type1==B)  ).

(* If line AAA is commented out then the following line goes through;
however if line AAA is put in then the following line generates
a UI.  *)

Local strange_conclusion : False := (p contra).