The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Here is a formalization of a simplification of Girard's Paradox, without much documentation, if you're interested: http://coq.inria.fr/stdlib/Coq.Logic.Hurkens.html  (You can find the full code at https://github.com/coq/coq/blob/trunk/theories/Logic/Hurkens.v)

-Jason

On Sun, Jun 8, 2014 at 10:26 PM, Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com> wrote:

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.