Exemple d'une fausse proposition en supposant Type: Type

Dans la théorie des types, si l'on permet à Type d'être membre de lui-même, cela rend la théorie incohérente. Je le comprends par analogie avec le paradoxe de Russel dans Set Theory, mais je préférerais que cela se fasse dans Type Theory. Existe-t-il un court exemple de l'équivalent dans la théorie des types?

La littérature pertinente est la suivante:

Thierry Coquand Un nouveau paradoxe en théorie des types (lien) . Il décrit son paradoxe dans un système un peu plus faible que

Type : Type

Mais cela peut être facilement transporté vers ce qui précède. L'idée principale est de prendre la preuve de Reynolds qu'il n'y a pas de modèles de système F dans la théorie des ensembles. Cela passe par la construction d'une algèbre initiale de la forme:

$$A\simeq (A \rightarrow \mathrm{2}) \rightarrow \mathrm{2}$$

Où est un ensemble à 2 éléments, et dérivant une contradiction par un argument de cardinalité. Coquand montre$\mathrm{2}$

1. Vous pouvez effectuer ce raisonnement dans la théorie des types ci-dessus
2. Il existe un modèle du système F dans cette théorie. Cela donne une contradiction.

Le deuxième article est d'Antonius Hurkens, et s'intitule Une simplification du paradoxe de Girard (lien) . La preuve implique une construction du "type de tous les types fondés". Je dois admettre que l'idée générale semble claire, mais les détails sont assez diaboliques.

J'ai peur qu'il n'y ait pas de contradiction simple et facile à comprendre dans $\mathrm{Type} : \mathrm{Type}$ . Cependant les termes de preuve obtenus à partir de la contradiction sont relativement traitables: seules quelques lignes suffisent pour les définir.

Alexandre Miquel, dans sa thèse , a montré que l'on pouvait construire un modèle de théorie naïve des ensembles dans ces systèmes de types incohérents en utilisant une interprétation pointue des ensembles. Il peut alors simplement appliquer directement le paradoxe de Russel. Malheureusement, la construction du modèle demande un peu de travail et la thèse est en français.