Exemplo de uma proposição falsa ao assumir Type: Type

Na teoria dos tipos, se alguém permite que o tipo seja um membro de si mesmo, isso torna a teoria inconsistente. Eu o entendo por analogia ao paradoxo de Russel na Teoria dos Conjuntos, mas preferiria ver isso na Teoria dos Tipos. Existe um pequeno exemplo do equivalente na teoria dos tipos?

A literatura relevante é a seguinte:

Thierry Coquand Um novo paradoxo na teoria dos tipos (link) . Ele descreve seu paradoxo em um sistema um pouco mais fraco do que

Type : Type

Mas isso pode ser facilmente transportado para o acima. A idéia principal é provar a Reynolds que não existem modelos do sistema F na teoria dos conjuntos. Isso prossegue construindo uma álgebra inicial do formulário:

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

Onde é um conjunto com 2 elementos e deriva de uma contradição por um argumento de cardinalidade. Coquand shows$\mathrm{2}$

1. Você pode executar esse raciocínio na teoria de tipos acima
2. Não é um modelo de sistema de F em que a teoria. Isso gera uma contradição.

O segundo artigo é de Antonius Hurkens e é intitulado Uma simplificação do paradoxo de Girard (link) . A prova envolve uma construção do "tipo de todos os tipos bem fundamentados". Devo admitir que a ideia geral parece clara, mas os detalhes são bastante diabólicos.

Receio que não haja contradição simples e fácil de entender em . No entanto, os termos de prova obtidos a partir da contradição são relativamente tratáveis: apenas algumas linhas são suficientes para defini-los.$\mathrm{Type} : \mathrm{Type}$

Alexandre Miquel, em sua dissertação de tese , mostrou que era possível construir um modelo de teoria dos conjuntos ingênua nesses sistemas de tipos inconsistentes usando uma interpretação de conjuntos de conjuntos de gráficos. Ele pode simplesmente aplicar o paradoxo de Russel diretamente. Infelizmente, a construção do modelo exige um pouco de trabalho e a dissertação é em francês.