Beispiel für einen falschen Satz bei der Annahme von Typ: Typ

Wenn man in der Typentheorie zulässt, dass Typ ein Mitglied von sich selbst ist, macht dies die Theorie inkonsistent. Ich verstehe es in Analogie zu Russels Paradoxon in der Mengenlehre, würde es aber vorziehen, es in der Typentheorie zu sehen. Gibt es ein kurzes Beispiel für das Äquivalent in der Typentheorie?

Die relevante Literatur ist die folgende:

Thierry Coquand Ein neues Paradoxon in der Typentheorie (Link) . Er beschreibt sein Paradoxon in einem System, das etwas schwächer ist als

Type : Type

Aber das kann leicht nach oben transportiert werden. Die Hauptidee besteht darin, Reynolds zu beweisen, dass es in der Mengenlehre keine Modelle für System F gibt. Dazu wird eine anfängliche Algebra der Form erstellt:

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

Wobei eine Menge mit 2 Elementen ist und durch ein Kardinalitätsargument einen Widerspruch herleitet. Coquand zeigt$\mathrm{2}$

1. Sie können diese Argumentation in der obigen Typentheorie ausführen
2. In dieser Theorie gibt es ein Modell des Systems F. Dies ergibt einen Widerspruch.

Der zweite Artikel stammt von Antonius Hurkens und trägt den Titel Eine Vereinfachung von Girards Paradoxon (Link) . Der Beweis beinhaltet eine Konstruktion des "Typs aller fundierten Typen". Ich muss zugeben, dass die allgemeine Idee klar zu sein scheint, aber die Details sind ziemlich teuflisch.

Ich fürchte, es gibt keinen einfachen, leicht verständlichen Widerspruch in . Die aus dem Widerspruch gewonnenen Beweisbegriffe sind jedoch relativ leicht nachvollziehbar: Nur wenige Zeilen reichen aus, um sie zu definieren.$\mathrm{Type} : \mathrm{Type}$

Alexandre Miquel hat in seiner Dissertation gezeigt, dass man in diesen inkonsistenten Typsystemen ein Modell der naiven Mengenlehre konstruieren kann, indem man eine spitze graphische Interpretation von Mengen verwendet. Er kann dann einfach Russels Paradox direkt anwenden. Leider erfordert der Modellbau ein wenig Arbeit und die Dissertation ist in französischer Sprache.