Konsistensi New Foundations – Bukti matematis sulit yang dibuktikan menggunakan Lean

Here is a summary of the key points from the given article, organized using Markdown:

Bukti konsistensi teori himpunan New Foundations

• Randall Holmes telah mengklaim sejak setelah 2010 bahwa ia membuktikan konsistensi teori himpunan "New Foundations (NF)" yang diajukan oleh Quine pada 1937
• Repositori ini membuktikan bahwa NF memang bebas kontradiksi dengan memverifikasi bagian-bagian sulit dari bukti Holmes menggunakan pembukti teorema interaktif Lean
• Bukti kini telah selesai, dan pernyataan teoremanya dapat ditemukan di ConNF/Model/Result.lean

Tujuan

• Diketahui bahwa NF konsisten jika dan hanya jika Tangled Type Theory (TTT) konsisten
• Dengan secara formal membangun model TTT di Lean, dibuktikan bahwa NF konsisten
• Pekerjaan ini didasarkan pada beberapa versi bukti Holmes, tetapi ada banyak perubahan dan tambahan agar kompatibel dengan teori tipe Lean
• Proyek ini bergantung pada mathlib, pustaka matematika komunitas yang ditulis dalam Lean, sehingga hasil-hasil yang sudah dikenal tentang kardinal, grup, dan sebagainya dapat digunakan tanpa harus dibuktikan langsung
• Semua definisi dan teorema di mathlib maupun proyek ini telah diverifikasi oleh kernel Lean yang tepercaya, tetapi Lean tidak dapat memeriksa apakah penjelasan definisi dan teorema sesuai dengan deskripsi bahasa Inggris yang dimaksud, sehingga perlu berhati-hati saat menarik kesimpulan dari kode proyek ini terhadap penjelasan berbahasa Inggrisnya

Tangled Type Theory (TTT)

• TTT adalah teori himpunan multi-sort dengan relasi kesetaraan "=" dan relasi keanggotaan "∈"
• Sort diindeks oleh ordinal limit λ, dan elemen λ disebut indeks tipe
• Rumus "x = y" terbentuk dengan baik ketika x dan y memiliki tipe yang sama, dan rumus "x ∈ y" terbentuk dengan baik ketika x memiliki tipe arbitrer yang lebih kecil daripada y
• Salah satu aksioma TTT adalah ekstensionalitas: sebuah himpunan bertipe α ditentukan secara unik oleh elemennya yang bertipe β arbitrer dengan β < α
• Sebagai contoh, jika dua himpunan bertipe α berbeda, maka untuk setiap β < α keduanya memiliki elemen bertipe β yang berbeda; sifat ini membuat model TTT sulit dibangun

Strategi

• Pembangunan model menggunakan strategi kasar berikut:

  • Konstruksi tipe dasar

    • Tetapkan λ sebagai ordinal limit, κ > λ sebagai ordinal reguler, dan μ > κ sebagai kardinal limit kuat dengan kofinalitas setidaknya κ
    • Himpunan yang lebih kecil dari κ disebut kecil
    • Pada level -1 dibangun tipe bantu yang disebut tipe dasar, yang pada akhirnya berada di bawah semua tipe yang menjadi bagian model akhir
    • Elemen tipe ini disebut atom (bukan atom dalam arti ZFU atau NFU), ada μ atom dan mereka dibagi menjadi litter berukuran κ

  • Konstruksi tiap tipe

    • Pada setiap level tipe α, dibentuk koleksi elemen model untuk model TTT yang dimaksud, yang kadang disebut t-himpunan
    • Dibentuk grup permutasi yang disebut permutasi yang diizinkan, yang bekerja pada t-himpunan
    • Relasi keanggotaan dipertahankan di bawah aksi permutasi yang diizinkan
    • Setiap t-himpunan disyaratkan memiliki support di bawah aksi permutasi yang diizinkan, yaitu himpunan kecil objek yang disebut alamat, sehingga kapan pun permutasi yang diizinkan menetapkan semua elemen support, t-himpunan itu juga tetap
    • Setiap t-himpunan di level α diberi ekstensi preferen bertipe β < α, dan dari elemen-elemen t-himpunan dapat dipulihkan ekstensi mana yang dipilih
    • Ekstensi dari subtipe lain pada t-himpunan ini dapat disimpulkan dari β-ekstensi, sehingga aksioma ekstensionalitas TTT dapat dipenuhi

  • Pengendalian ukuran tiap tipe

    • Setiap tipe α hanya dapat dibangun dengan asumsi bahwa semua tipe β < α memiliki ukuran tepat μ, di samping hipotesis lain
    • Mudah dibuktikan bahwa koleksi t-himpunan di level α memiliki kardinalitas setidaknya μ, jadi perlu ditunjukkan bahwa elemen himpunan ini paling banyak μ
    • Hal ini dapat dilakukan dengan menunjukkan bahwa tidak ada terlalu banyak deskripsi yang pada dasarnya berbeda tentang kekusutan di bawah aksi permutasi yang diizinkan
    • Untuk ini diperlukan teorema teknis bantu, yaitu teorema kebebasan aksi, yang memungkinkan konstruksi permutasi yang diizinkan
    • Hasil utama pada bagian ini ada di sini

  • Menutup induksi

    • Dengan menjalankan proses di atas secara rekursif, tipe-tipe tangled dapat dibangkitkan pada semua level tipe α
    • Dalam teori himpunan ini langkah yang mudah, tetapi dalam teori tipe diperlukan banyak pekerjaan karena keterkaitan berbagai hipotesis induktif yang dibutuhkan
    • Kemudian diperiksa apakah konstruksi ini benar-benar menghasilkan model TTT dengan memenuhi aksiomatisasi hingga dari teori tersebut
    • Dipilih untuk mengubah aksiomatisasi hingga Hailperin bagi skema komprehensi NF menjadi aksiomatisasi hingga TTT, dan ini disajikan dalam berkas hasil
    • Namun pilihan ini bersifat arbitrer, dan aksiomatisasi hingga lain dapat dengan mudah dibuktikan menggunakan infrastruktur yang sudah disiapkan

Opini GN⁺

• Bukti ini sangat bermakna karena secara formal membuktikan konsistensi teori himpunan NF, yang selama ini hanya diketahui pada tingkat yang sangat abstrak. Ini penting secara matematis murni sekaligus menunjukkan kemajuan nyata dalam alat bantu pembuktian dan pembuktian teorema otomatis
• Pekerjaan formalisasi menggunakan Lean menjamin ketepatan dan kelengkapan bukti, tetapi pada saat yang sama dapat sulit dipahami karena ditulis dalam bahasa yang tidak akrab bagi banyak matematikawan. Perlu diiringi dengan upaya menjelaskan ide inti bukti secara jelas dalam bahasa alami
• Penjelasan intuitif tentang teori latar juga masih kurang, misalnya mengapa aksioma ekstensionalitas TTT yang ganjil itu diperlukan dan bagaimana hubungannya dengan teori himpunan lain. Selain bukti formal, pembahasan konteks filosofis dan historis akan makin membantu pemahaman terhadap teori NF
• Topik riset lanjutan juga tampak menarik, seperti hubungan model yang dibangun dengan model teori himpunan ZFC yang standar, atau bagaimana konsistensi NF terhubung dengan konsistensi sistem aksioma lain
• Contoh formalisasi bukti serumit ini dalam Lean dapat menjadi teladan bagi otomatisasi bukti di bidang matematika lain. Jika pekerjaan serupa diterapkan pada teorema-teorema yang sebelumnya belum dipahami dengan baik proses pembuktiannya, dampaknya bagi komunitas matematika bisa sangat besar

[GN⁺]

Komentar Hacker News

• Risiko bahwa bukti yang menggunakan Lean itu salah sangat kecil. Namun, terlepas dari bug di Lean, tetap perlu membaca kesimpulannya dengan cermat dan memastikan bahwa yang benar-benar dibuktikan memang sesuai, karena ini adalah masalah yang dikenal dalam verifikasi perangkat lunak dan matematika.
• Kasus ini tampaknya merupakan contoh pertama penggunaan proof assistant untuk menyelesaikan status sebuah bukti yang sulit. Sebelumnya memang ada proyek yang memverifikasi bukti yang sudah ada dan mencakup unsur komputasi skala besar yang diproses dengan perangkat lunak yang tidak tepercaya, tetapi kasus ini adalah contoh pertama ketika status epistemologis hasilnya masih belum pasti di komunitas matematika.
• Muncul rasa ingin tahu tentang perbedaan mendasar antara Coq dan Lean, serta apakah keduanya bekerja dalam jenis logika yang sama. Dalam diskusi terkait, disebutkan hal-hal yang sulit dipahami.
• Para pendukung Lean cenderung terlalu berlebihan dalam menekankan bahwa Lean adalah metode pembuktian yang unggul. Lean hanyalah metode pembuktian alternatif, dan sebagai bahasa pemrograman serta sistem, Lean memiliki bugnya sendiri dan sangat bergantung pada berbagai lapisan library yang ditulis orang lain.
• Daripada mengatakan bahwa Lean menyatakan buktinya bagus, akan lebih akurat dan jujur untuk mengatakan bahwa bukti yang ditulis telah diverifikasi oleh matematikawan manusia, lalu bukti itu dikonversi ke Lean dan diverifikasi di sana juga. Penjelasan bahwa Lean memberikan verifikasi yang tunggal dan sempurna tidak akurat, atau setidaknya saya belum melihat penjelasan yang mengatakan demikian.
• Diminta penjelasan singkat tentang apa yang istimewa atau baru dari formalisasi teori himpunan "New Foundations" dibandingkan formalisasi lainnya, dalam bentuk yang bisa dibaca oleh mahasiswa sarjana matematika atau profesional teknik.
• Ada yang bertanya-tanya apakah pendekatan ini pada akhirnya akan mengarah pada pembuktian kolaboratif dan 'perbaikan bug', sehingga membuat matematika menjadi proses yang mirip dengan kode di GitHub.
• Menurut teorema Gödel, semua sistem yang cukup kuat tidak dapat menunjukkan konsistensinya sendiri, dan ada pertanyaan tentang hal ini.
• Ingin terus mengikuti proyek mathlib, tetapi tidak punya waktu. Ada yang penasaran apakah ada cara untuk berpartisipasi dengan sangat pasif.