Przykład fałszywej propozycji przy założeniu Type: Type

W teorii typu, jeśli pozwala się typowi być sobą, powoduje to, że teoria jest niespójna. Rozumiem to przez analogię do paradoksu Russela w Teorii Zestawów, ale wolałbym, żeby to zrobiono w Teorii Typu. Czy istnieje krótki przykład odpowiednika w teorii typów?

Odpowiednia literatura jest następująca:

Thierry Coquand Nowy paradoks w teorii typów (link) . Opisuje swój paradoks w systemie, który jest nieco słabszy niż

Type : Type

Ale można to łatwo przenieść do powyższego. Główną ideą jest zabranie Reynoldsa dowodu, że nie ma modeli systemu F w teorii mnogości. Następuje to poprzez zbudowanie początkowej algebry postaci:

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

Gdzie $\mathrm{2}$jest zbiorem z 2 elementami i wywodzącym sprzeczność argumentem liczności. Pokazy Coquand

1. Możesz przeprowadzić to rozumowanie w powyższej teorii typów
2. W tej teorii znajduje się model systemu F. Daje to sprzeczność.

Drugi artykuł pochodzi od Antoniusa Hurkensa i nosi tytuł Uproszczenie paradoksu Girarda (link) . Dowód obejmuje konstrukcję „typu wszystkich dobrze uzasadnionych typów”. Muszę przyznać, że ogólny pomysł wydaje się jasny, ale szczegóły są dość diabelskie.

Obawiam się, że nie ma prostej, łatwej do zrozumienia sprzeczności $\mathrm{Type} : \mathrm{Type}$. Jednak dowody uzyskane z sprzeczności są względnie możliwe do przełknięcia: wystarczy kilka linii, aby je zdefiniować.

Alexandre Miquel w swojej rozprawie doktorskiej wykazał, że można zbudować model naiwnej teorii zbiorów w tych niespójnych układach typów, stosując spiczastą graficzną interpretację zbiorów. Następnie może po prostu zastosować paradoks Russela bezpośrednio. Niestety konstrukcja modelu zajmuje trochę pracy, a rozprawa jest w języku francuskim.