Ejemplo de una proposición falsa al asumir Tipo: Tipo

En la teoría de tipos, si se permite que Type sea miembro de sí mismo, la teoría es inconsistente. Lo entiendo por analogía con la paradoja de Russel en Set Theory, pero preferiría verlo hecho en Type Theory. ¿Hay un breve ejemplo del equivalente en la teoría de tipos?

La literatura relevante es la siguiente:

Thierry Coquand Una nueva paradoja en la teoría de tipos (enlace) . Describe su paradoja en un sistema que es algo más débil que

Type : Type

Pero eso se puede transportar fácilmente a lo anterior. La idea principal es tomar la prueba de Reynolds de que no hay modelos del sistema F en la teoría de conjuntos. Eso procede construyendo un álgebra inicial de la forma:

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

Donde es un conjunto con 2 elementos, y deriva una contradicción por un argumento de cardinalidad. Coquand muestra$\mathrm{2}$

1. Puede llevar a cabo este razonamiento en la teoría de tipos anterior.
2. No es un modelo de sistema de F en la que la teoría. Esto produce una contradicción.

El segundo artículo es de Antonius Hurkens y se titula Una simplificación de la paradoja de Girard (enlace) . La prueba implica una construcción del "tipo de todos los tipos bien fundados". Debo admitir que la idea general parece clara, pero los detalles son bastante diabólicos.

Me temo que no hay una contradicción simple y fácil de entender en . Sin embargo, los términos de prueba obtenidos de la contradicción son relativamente manejables: solo unas pocas líneas son suficientes para definirlos.$\mathrm{Type} : \mathrm{Type}$

Alexandre Miquel, en su disertación de tesis , demostró que uno podría construir un modelo de teoría de conjuntos ingenua en estos sistemas de tipos inconsistentes mediante el uso de una interpretación gráfica puntiaguda de conjuntos. Entonces puede simplemente aplicar la paradoja de Russel directamente. Lamentablemente, la construcción del modelo requiere un poco de trabajo, y la disertación es en francés.