The Coq mailing list

[Judicael Courant <Judicael.Courant AT lri.fr>]

Hi,

> Exactly what kind of paradox are we talking about that would require
> this
> global check, and for which using axioms instead of theorems would be
> inadequate?

I guess the problem Pierre mentions is about implicit universes. I am 
no specialist of paradoxes, but at least I can show you an example 
where "Axiom X : t1. Definition d := t2." and "Definition X : t1 := 
t3." are both valid and "Definition d : t1 := t3. Definition d := t2." 
is invalid in Coq because of universe constraints:


Axiom Y : (U:Type)U->U.

Axiom X : (U:Type)U->U.

Definition d := (Y ((U:Type)U->U) X).

is valid and so is

Axiom Y : (U:Type)U->U.
Definition X : (U:Type)U->U := Y.

But

Axiom Y : (U:Type)U->U.

Definition X : (U:Type)U->U := Y.

Definition d := (Y ((U:Type)U->U) X).

is rejected (universe inconsistency).


This means implicit universes and separate checking of theories are 
mutually incompatible (see my TPHOLs 02 paper about this if you are 
interested, it is available from 
http://www.lri.fr/~jcourant/publis/liste_publis.en.html)

Judicaël.

PS (for specialist of universes): this example has nothing to do with 
the fact Coq does not implement typical ambiguity for definitions.
--
Judicael.Courant AT lri.fr,
 http://www.lri.fr/~jcourant/
Tel (+33) (0)1 69 15 64 85
GPG public key: 7C25 D439 9F60 BC68 A131  6267 98B9 98F6 7107 2457