Contoh proposisi palsu ketika mengasumsikan Tipe: Jenis

Dalam Type Theory jika seseorang memungkinkan Type untuk menjadi anggota dari dirinya sendiri, itu membuat teori tidak konsisten. Saya memahaminya dengan analogi dengan paradoks Russel dalam Set Theory, tetapi lebih suka melihatnya dilakukan dalam Type Theory. Apakah ada contoh singkat dari yang setara dalam Type Theory?

Literatur yang relevan adalah sebagai berikut:

Thierry Coquand Suatu paradoks baru dalam teori tipe (tautan) . Dia menggambarkan paradoksnya dalam suatu sistem yang agak lebih lemah dari

Type : Type

Tapi itu bisa dengan mudah diangkut ke atas. Gagasan utamanya adalah mengambil bukti Reynolds bahwa tidak ada model sistem F dalam teori himpunan. Itu hasil dengan membangun aljabar awal dari bentuk:

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

Di mana adalah himpunan dengan 2 elemen, dan menurunkan kontradiksi dengan argumen kardinalitas. Coquand menunjukkan$\mathrm{2}$

1. Anda dapat melakukan alasan ini dalam teori tipe di atas
2. Ada adalah model sistem F dalam teori itu. Ini menghasilkan kontradiksi.

Artikel kedua adalah dari Antonius Hurkens, dan berjudul A simplification of Girard's paradox (link) . Buktinya melibatkan konstruksi "tipe semua tipe yang beralasan". Saya harus mengakui bahwa ide umumnya tampak jelas, tetapi detailnya cukup jahat.

$\mathrm{Type} : \mathrm{Type}$

Alexandre Miquel, dalam disertasi tesisnya , menunjukkan bahwa seseorang dapat membangun model teori himpunan naif dalam sistem tipe yang tidak konsisten ini dengan menggunakan interpretasi grafik runcing set. Dia kemudian dapat langsung menerapkan paradoks Russel secara langsung. Sayangnya pembangunan model membutuhkan sedikit pekerjaan, dan disertasi dalam bahasa Perancis.