The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

On 03/05/14 13:19, AUGER Cédric wrote:
> Le Sat, 03 May 2014 10:44:12 +0100,
> 
> I guess it is related to Girard paradox.
> 

As a non-mathematician (by profession), I failed to follow this trail in the 
maze.

  <where I got lost>

    Ok, Girard's Paradox is a special case of Burati-Forti paradox. Fine.

    Girard paradox was formulated within certain version of certain Per 
Martin-Löf axiomatic system.
    It is cited, but for me it is not trivial to judge whether I really 
reading the right version of that system. Not fine.

    Burati-Forti paradox is concerned with ordinal numbers, where again I was 
lost with an analogous problem
    --- non-obviousness of the axioms holding for ordinal numbers. Not fine.
    (What I liked was the idea of order types. That's interesting.)

    Russell's paradox was fine.

  </where I got lost>

On 05/05/14 19:49, Eddy Westbrook wrote:
> Requiring k to be greater than or equal to both i and j is just another way 
> to say that k must be at least the maximum of i and j.
> he idea here is that (unless B is a Prop, where you can use 
> impredicativity) in order to form a type
> forall (a:A), B, you need to go to a universe that is at least big enough 
> (high enough i) to contain both A and B.
> If k were less than the universe level i for A, then k wouldn’t be big 
> enough to even get A, let alone to get forall (a:A), B.

From this point of view, I almost got it, but not quite.
It is non-obvious why universes has to form total order.

Since GEB (Gödel Escher Bach) heavily references Russell's paradox, I have 
tried my luck there.
What helped me to see essentiality of side-condition of the 
Prod(Type,Type,Type) rule was Escher's "Drawing Hands" lithography.
(Regardless of Girard's paradox, it is obvious that the universes has to form 
at least join-semilattice if we choose union (of universes) as the join 
operation.
 If we have the term "A -> B", where "A" belongs to universe "U1" and "B" 
belongs to universe "U2", it is possible to see why term "A -> B" must belong 
to universe "U1 \/ U2"
 Similarly, if we have the term "forall a:A,B", where A belongs to "U1" and 
"B" belongs to universe "U2", it is possible to see why term "forall a:A,B" 
must belong to universe "U1 \/ U2".
 To justify that axiom, we can project the problem to the world of pictures 
within pictures or dreams within dreams or virtual realities within virtual 
realitites.
 The universe where the term "A -> B" or "forall a:A,B" would belong would be 
determined the same way in all those cases.)

Many thanks.