Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

[Martin Escardo <m.escardo@cs.bham.ac.uk>]

Some claims quoted below need to be rectified, given that this is a
public forum:

On 29/07/15 06:54, Patrik Eklund wrote:
>> Yes, we cannot create the set of all sets, similarly as we shouldn't
> even try out creating the type of all types. Nevertheless, Martin-L??f
> took the liberty of doing that, and was opportunistic enough to publish
> it. Things went wrong but it was not called a paradox.

It is called Girard's Paradox, and the construction resembles
Burali-Forti's Paradox, rather than Russell's paradox.

The idea was to have a type U of all types, including U itself,
written U:U. This may seem naive given Russell's Paradox was known.

However, there is more to U:U than Russell's paradox, because "U:U" is
not a proposition (it is a so-called judgment), and hence it cannot be
true or false, or taken as a hypothesis in a mathematical
statement. In particular, using U:U, you cannot form the type of all
types that don't belong to themselves, because there is no "belong"
relation in type theory, and for instance writing something such as
"not(X:X)" is not even grammatically correct.

To derive a contradiction using U:U (in a type theory extended with
this judgement) is much harder than to derive a contradiction from the
hypothetical existence of a set of all sets (in set theory).

> Constructions were "improved" over decades, but the HoTT community
> still uses universality, so that paradox just appears as the
> emperors new clothes.

The improvement adopted both in MLTT in the 1980's, and in MLTT+HoTT
axioms now, was already available, and is the same as the one Russell
proposed a century ago to avoid his paradox, and adopted in Principia
Mathematica, namely to instead have a hierarchical stratification
U_0 : U_1 : U_2 : U_3 : ... by "size", where U_0 is the type of all
small types, which lives in the type U_1 of large types, which lives
in the type U_2 of even larger types, etc.

The idea is at least 107 years old.

M.





[For admin and other information see: http://www.mta.ca/~cat-dist/ ]