Beispiel eines falschen Satzes bei der Annahme von Typ: Typ: Typ

Question

In der Typtheorie, wenn man es zulässt, dass Typ ein Mitglied von sich selbst ist, macht es die Theorie inkonsistent. Ich verstehe es analog zu Russels Paradox in der festgelegten Theorie, würde es aber lieber in der Typtheorie sehen. Gibt es ein kurzes Beispiel für das Äquivalent in der Typtheorie?

Answer 1

Die relevante Literatur ist die folgende:

Thierry Coquand Ein neues Paradox in der Typtheorie (Verknüpfung). Er beschreibt sein Paradox in einem System, das etwas schwächer ist als

Type : Type

Aber das kann leicht zum oben genannten transportiert werden. Die Hauptidee besteht darin, Reynolds Beweis zu nehmen, dass es in der festgelegten Theorie keine Modelle des Systems F gibt. Das erfolgt durch den Bau einer anfänglichen Algebra der Form:

$$ a simenq (a rightarrow mathhrm {2}) rightarrow mathrm {2} $$

Wobei $ mathrm {2} $ ein Set mit 2 Elementen ist und einen Widerspruch durch ein Kardinalitätsargument ableitet. Coquand zeigt

1. Sie können diese Argumentation in der oben genannten Typtheorie durchführen
2. Dort ist ein Modell des Systems F in dieser Theorie. Dies ergibt einen Widerspruch.

Der zweite Artikel stammt von Antonius Hurkens und trägt den Titel " Eine Vereinfachung von Girards Paradoxon (Verknüpfung). Der Beweis beinhaltet eine Konstruktion der "Art aller begründeten Typen". Ich muss zugeben, dass die allgemeine Idee klar erscheint, aber die Details sind ziemlich teuflisch.

Ich fürchte, es gibt keinen einfachen, leicht verständlichen Widerspruch in $ mathrm {type}: mathrm {type} $. Die aus dem Widerspruch gewonnenen Proofs sind jedoch relativ verfolgbar: Nur wenige Linien reichen aus, um sie zu definieren.

Alexandre Miquel in seinem Dissertation von These, zeigten, dass man in diesen inkonsistenten Typsystemen ein Modell der naiven Set -Theorie konstruieren könnte, indem man eine gezielte Grapheninterpretation von Mengen verwendet. Er kann dann einfach Russels Paradoxon direkt anwenden. Leider erfordert die Modellkonstruktion ein wenig Arbeit, und die Dissertation ist in Französisch.