Memformalkan teori himpunan terbatas dalam teori jenis

Kebanyakan asisten pembuktian memiliki formalisasi konsep "himpunan terbatas". Namun, formalisasi ini sangat berbeda (walaupun orang berharap semua itu pada dasarnya setara!). Apa yang saya tidak mengerti pada saat ini adalah ruang desain yang terlibat, dan apa pro dan kontra dari setiap formalisasi.

Secara khusus, saya ingin memahami yang berikut:

• Dapatkah saya aksiomatiskan set berhingga (yaitu tipe yang dihuni oleh jumlah terbatas manusia) dalam teori tipe sederhana? Sistem F? Apa kelemahan melakukannya dengan cara ini?
• Saya tahu itu bisa dilakukan 'secara elegan' dalam sistem yang diketik secara dependen. Tetapi, dari sudut pandang klasik, definisi yang dihasilkan tampak sangat asing. [Saya tidak mengatakan mereka salah, jauh dari itu!]. Tapi saya juga tidak mengerti mengapa mereka 'benar'. Saya mengerti bahwa mereka memilih konsep yang benar , tetapi alasan yang lebih dalam untuk 'mengatakannya seperti itu' adalah apa yang saya tidak pahami sepenuhnya.

Pada dasarnya, saya ingin pengantar yang beralasan untuk ruang desain formalisasi konsep 'set terbatas' dalam teori tipe.

Saya tahu itu bisa dilakukan 'secara elegan' dalam sistem yang diketik secara dependen. Tetapi, dari sudut pandang klasik, definisi yang dihasilkan tampak sangat asing.

Bisakah Anda menjelaskan apa yang Anda maksud dengan "alien"? Tampak bagi saya bahwa Anda meresmikan konsep himpunan terbatas dengan cara yang persis sama dalam teori jenis dan teori himpunan.

Dalam teori himpunan, Anda melanjutkan dengan mendefinisikan himpunan sebagai Kemudian, Anda mendefinisikan predikat finiteness sebagai: Di mana berarti isomorfisma set.$Fin(n)$

Dalam teori tipe, Anda dapat melakukan hal yang persis sama! Perhatikan bahwa adalah tipe dengan elemen (karena komponen kedua dari pasangan adalah tidak relevan dengan bukti). Kemudian, Anda dapat mendefinisikan konstruktor tipe finiteness sebagai: Di mana berarti isomorfisme tipe.

Biarkan saya melihat apakah saya dapat menambahkan sesuatu yang berguna untuk jawaban Neel. "Ruang desain" untuk himpunan terbatas jauh lebih besar secara konstruktif sehingga secara klasik karena berbagai definisi "terbatas" tidak perlu setuju secara konstruktif. Berbagai definisi dalam teori tipe memberikan konsep yang sedikit berbeda. Berikut ini beberapa kemungkinan.

Himpunan terbatas Kuratowski ( -finite) dapat dikarakteristikkan sebagai free -semilattices: diberikan suatu himpunan, tipe atau objek , elemen-elemen dari free -semilattice dapat dikelompokkan sebagai subset terbatas . Memang, setiap elemen tersebut dihasilkan oleh:$K$$\lor$$X$$\lor$$K(X)$$X$

• elemen netral , yang sesuai dengan set kosong, atau$0$
• generator , yang sesuai dengan singleton , atau$x \in X$$\lbrace x \rbrace$
• a bergabung dengan dari dua elemen, yang sesuai dengan serikat pekerja.$S \lor T$

Formulasi yang setara dari adalah: adalah -finite jika, dan hanya jika, ada dan sebuah surjection .$K(X)$$S \subseteq X$$K$$n \in \mathbb{N}$ $e : \lbrace 1, \ldots, n \rbrace \to S$

Jika dibandingkan dengan definisi Neel kita melihat bahwa ia membutuhkan bijection . Ini sama dengan mengambil himpunan himpunan -finite yang memiliki persamaan kesetaraan: . Mari kita gunakan untuk koleksi decidable subset -finite dari .$e : \lbrace 1, \ldots, n \rbrace \to S$$K$$S \subseteq X$$\forall x, y \in S . x = y \lor x \neq y$$D(X)$$K$$X$

Jelas ditutup di bawah serikat terbatas, tetapi tidak perlu ditutup di bawah persimpangan terbatas. Dan tidak ditutup dalam operasi apa pun. Karena orang berharap bahwa set yang terbatas berperilaku sedikit seperti "Boolean aglebra tanpa top", kita juga bisa mencoba mendefinisikannya sebagai aljabar Boolean umum gratis ( , , dan komplemen relatif ), tetapi saya sebenarnya tidak pernah mendengar upaya seperti itu.$K(X)$$D(X)$$0$$\lor$$\land$$\setminus$

Ketika memutuskan apa definisi "benar", Anda harus memperhatikan apa yang ingin Anda lakukan dengan set yang terbatas. Dan tidak ada definisi yang benar. Sebagai contoh, dalam arti "terbatas" apa himpunan akar kompleks dari suatu polinomial terbatas ?

Lihat Hingga secara konstruktif? oleh Thierry Coquand dan Arnaud Spiwack untuk diskusi rinci tentang keterbatasan. Pelajarannya adalah bahwa keterbatasan jauh dari jelas secara konstruktif.