Konsistensi New Foundations – Pembuktian matematika rumit yang diverifikasi dengan Lean
(leanprover-community.github.io)- Bagian sulit dari pembuktian konsistensi New Foundations, teori himpunan yang diajukan Quine pada 1937, telah diverifikasi dengan Lean; teorema intinya dirangkum di
ConNF/Model/Result.lean - Pendekatannya memanfaatkan hasil bahwa konsistensi New Foundations dan Tangled Type Theory(TTT) adalah ekuivalen, dengan membangun model TTT secara formal di dalam Lean
- Model TTT sulit dibangun karena ekstensionalitas, yaitu himpunan harus ditentukan secara unik oleh elemen-elemen bertipe lebih rendah
- Konstruksi model memakai base type, t-set, allowable permutations, support kecil, dan preferred extension; untuk mengendalikan ukuran tipe dengan μ, diperlukan freedom of action theorem
- Kernel Lean memeriksa pembuktian yang diformalkan, tetapi tidak menjamin bahwa pernyataan formal sesuai dengan makna bahasa Inggris yang dimaksud, sehingga interpretasi hasil memerlukan peninjauan terjemahan
Verifikasi konsistensi New Foundations yang diselesaikan dengan Lean
- Pada 1937, Quine mengajukan teori himpunan New Foundations, dan Randall Holmes sejak 2010 mengklaim memiliki pembuktian konsistensinya
- Proyek ini berfokus pada verifikasi bagian sulit dari pembuktian Holmes dengan interactive theorem prover Lean untuk menunjukkan konsistensi New Foundations
- Pembuktiannya telah selesai, dan pernyataan teoremanya dapat dilihat di
ConNF/Model/Result.lean - Materi terkait juga disediakan
Menjalankan kode secara lokal
- Untuk menjalankannya secara lokal, pasang elan, clone repositorinya, lalu jalankan perintah berikut dari root repositori
lake exe cache get
- Setelah itu, kode dapat ditelusuri di editor seperti Visual Studio Code, dan dari command line dapat dikompilasi langsung dengan
lake build
Kaitan antara New Foundations dan TTT
- New Foundations diketahui konsisten jika dan hanya jika Tangled Type Theory(TTT) konsisten
- Hasil terkait ada di theorem 1 milik Holmes
- Proyek ini secara formal membangun model TTT di Lean, dan dari situ memperoleh konsistensi New Foundations, yaitu Con(NF), sebagai kesimpulan di atas kertas
- Pekerjaan ini didasarkan pada beberapa dokumen pembuktian Holmes, tetapi banyak perubahan dan tambahan diperlukan agar sesuai dengan type theory milik Lean
Dasar verifikasi Lean dan catatan interpretasi
- Proyek ini bergantung pada mathlib, pustaka matematika komunitas yang ditulis dalam Lean
- Berkat mathlib, hasil-hasil yang umum seperti kardinal dan grup dapat digunakan tanpa perlu dibuktikan ulang di dalam proyek
- Definisi dan teorema dalam mathlib serta proyek ini diperiksa oleh trusted kernel Lean
- Kernel Lean memverifikasi secara komputasional bahwa pembuktian yang dibangun benar-benar valid
- Namun, Lean tidak dapat memeriksa sampai sejauh apakah pernyataan formal cocok dengan padanan bahasa Inggris yang dimaksud
- Saat menarik kesimpulan dari kode, terjemahan antara uraian bahasa Inggris dan pernyataan formal perlu diperiksa dengan cermat
Struktur dan kesulitan Tangled Type Theory
- TTT adalah teori himpunan multi-sort dengan kesetaraan
=dan relasi keanggotaan∈ - Sort diindeks oleh ordinal limit λ, dan elemen λ disebut indeks tipe
- Syarat pembentukan ekspresi dibatasi oleh tipe
x = ywell-formed jika tipexdanysamax ∈ ywell-formed jika tipexlebih rendah daripada tipey
- Kesulitan utama berasal dari aksioma ekstensionalitas TTT
- Himpunan bertipe α harus ditentukan secara unik oleh elemen-elemen sembarang tipe β < α
- Misalnya, jika dua himpunan bertipe α berbeda, maka untuk setiap β < α, keduanya harus memiliki elemen bertipe β yang berbeda
- Karena persyaratan ini, konstruksi model TTT menjadi lebih rumit daripada konstruksi model teori himpunan sederhana
Tahap utama konstruksi model
-
Konstruksi base type
- Ambil λ sebagai ordinal limit, κ > λ sebagai ordinal regular, dan μ > κ sebagai kardinal strong limit dengan kofinalitas setidaknya κ
- Himpunan berukuran lebih kecil dari κ disebut small
- Pertama-tama dibangun base type pada level -1, yaitu tipe pembantu di bawah semua tipe model
- Elemen tipe ini disebut atoms, tetapi bukan atom dalam arti ZFU atau NFU
- Ada μ atom, dan atom-atom itu dipartisi menjadi litters berukuran κ
-
t-set dan allowable permutations
- Pada setiap level tipe α, dibuat koleksi yang akan menjadi elemen model TTT, disebut t-set
- Secara bersamaan dibangun allowable permutations, yaitu grup permutasi yang bekerja pada t-set
- Relasi keanggotaan dipertahankan di bawah aksi allowable permutations
- Setiap t-set ditetapkan agar memiliki support terhadap aksi allowable permutations
- Support adalah himpunan kecil objek yang disebut addresses
- Jika suatu allowable permutation menetapkan semua elemen support, maka ia juga menetapkan t-set tersebut
-
Menyesuaikan ekstensionalitas dengan preferred extension
- t-set pada setiap level α memiliki preferred extension dari suatu tipe β < α
- Dari elemen-elemen t-set, dapat dipulihkan extension mana yang dipreferensikan, dan extension dari tipe-tipe lebih rendah lainnya diturunkan dari β-extension tersebut
- Struktur ini digunakan untuk memenuhi aksioma ekstensionalitas TTT
-
Mengendalikan ukuran tipe
- Setiap tipe α dapat dibangun jika ada asumsi bahwa ukuran semua tipe β < α tepat μ, dan asumsi lain yang diperlukan
- Mudah dibuktikan bahwa ukuran koleksi t-set pada level α setidaknya μ, sehingga yang perlu ditunjukkan adalah jumlahnya paling banyak μ
- Untuk itu, ditunjukkan bahwa tidak ada terlalu banyak deskripsi tangles yang secara fundamental berbeda di bawah aksi allowable permutations
- Tahap ini memerlukan freedom of action theorem, lemma teknis yang memungkinkan konstruksi allowable permutations
- Hasil utama bagian ini ada di ConNF.mk_tSet
-
Penutup induksi dan pemeriksaan aksioma
- Proses di atas dijalankan secara rekursif untuk menghasilkan tipe tangles pada semua level tipe α
- Ini langkah yang mudah dalam teori himpunan, tetapi dalam type theory dibutuhkan banyak pekerjaan karena berbagai asumsi induksi yang diperlukan saling terkait
- Setelah itu, untuk memastikan konstruksi tersebut merupakan model TTT, diperiksa apakah ia memenuhi aksiomatisasi hingga dari teori tersebut
- Proyek ini menggunakan aksiomatisasi hingga skema comprehension NF oleh Hailperin yang diubah menjadi aksiomatisasi hingga TTT
- File hasilnya ada di results file
- Pilihan ini bersifat arbitrer, dan dengan infrastruktur yang sudah dibangun, aksiomatisasi hingga lain juga dapat dibuktikan dengan mudah
1 komentar
Komentar Hacker News
Saya menilai risiko bahwa bukti dalam Lean itu salah sangat kecil.
Namun, terlepas dari bug Lean, ada risiko yang sudah lama dikenal baik dalam verifikasi perangkat lunak maupun matematika: membaca kesimpulan dengan tepat untuk memastikan bahwa proposisi yang benar-benar dibutuhkan memang telah dibuktikan.
Saya telah membaca kesimpulan akhir Wilshaw dengan saksama, dan menilai bahwa ia memang membuktikan hal yang perlu dibuktikan.
Makalahnya juga mengatakan hal serupa: semua definisi dan teorema di mathlib dan proyek ini diperiksa oleh trusted kernel Lean, dan secara komputasional memverifikasi bahwa bukti yang kami susun memang benar.
Namun, Lean tidak dapat memeriksa apakah proposisi dalam definisi dan teorema sesuai dengan ungkapan bahasa Inggris yang dimaksud, jadi saat menarik kesimpulan dari kode proyek ini perlu berhati-hati dengan penerjemahannya ke bahasa Inggris.
Masalah yang saya maksud terhubung dengan kekhawatiran terkait library: ketika memakai suatu konsep yang didefinisikan, kita harus yakin bahwa definisinya benar, yakni bahwa yang benar-benar dibutuhkan memang telah dibuktikan.
Formalisasi Wilshaw memang memakai library, tetapi tidak rentan terhadap sanggahan ini. Yang dibuktikan adalah bahwa suatu konsep terdefinisi memenuhi sekumpulan formula logika orde pertama tertentu, dan jika ada predikat yang memenuhi formula-formula itu maka NF konsisten.
Risiko lain adalah bug di Lean itu sendiri. Ini juga bukan sesuatu yang belum pernah terjadi pada theorem prover 1.
Mungkin sulit terjadi secara kebetulan, tetapi kolaborasi skala besar tempat banyak orang sembarang mengisi langkah-langkah seperti 3 terus membesar. Situasi ketika seseorang mengganggu dengan mengisi satu langkah memakai bug yang ia temukan bisa jadi layak dikhawatirkan.
Dari sudut pandang fondasi matematika, penting juga bahwa bukti ini merupakan bukti tentang ekuikonsistensi antara NF dan kernel Lean. Kernel Lean sendiri ditinjau manusia.
Theorem prover yang dimekanisasi bekerja dengan mempertahankan tingkat kebenaran yang disuntikkan melalui manusia atau sistem eksternal lain.
Kalau saya tidak keliru, ini tampaknya kasus pertama ketika proof assistant digunakan untuk membereskan status sebuah bukti sulit yang selama bertahun-tahun berada dalam keadaan ambigu.
Memang sudah ada proyek yang memverifikasi bukti yang sudah ada, seperti teorema empat warna di Coq, ketika perangkat lunak yang tidak tepercaya menangani bagian komputasi besar; tetapi untuk kasus ketika status epistemik hasilnya sendiri tidak pasti bagi komunitas matematika yang lebih luas, rasanya ini yang pertama.
Saya juga teringat Liquid Tensor Experiment.
https://www.nature.com/articles/d41586-021-01627-2
https://leanprover-community.github.io/blog/posts/lte-final/
Ini mirip dengan dugaan Kepler (https://en.m.wikipedia.org/wiki/Kepler_conjecture).
Buktinya sudah diketahui, tetapi sebelum diformalkan orang belum yakin apakah itu benar.
Sepertinya berikutnya giliran dugaan abc.
Pada 2012 diklaim sudah dibuktikan, dan ada makalah daring lebih dari 400 halaman, tetapi tampaknya tidak banyak orang yang menerima bukti itu.
Bisakah seseorang menjelaskan secara garis besar apa yang istimewa atau baru dari formalisasi teori himpunan “New Foundations” dibandingkan formalisasi lain?
Atau tautan penjelasan yang layak dibaca mahasiswa S1 matematika atau profesional teknik juga boleh.
Intinya menurut saya adalah keberadaan himpunan semesta. Dalam sistem tipe bahasa pemrograman yang saya gunakan, himpunan semesta seperti ini sangat berguna.
Berbagai akal-akalan pada sistem yang ada, seperti cumulative universes atau type-in-type, terasa tidak memuaskan. Sebagai gantinya, kita cukup memeriksa apakah signature tipenya bertingkat, lalu bisa melupakan fakta bahwa tipe itu memiliki tingkat numerik.
Pada dasarnya, ia mensyaratkan bahwa predikat yang dipakai untuk memilih subhimpunan harus mematuhi sistem tipe yang sangat ringan. “x bukan elemen dari dirinya sendiri” bukanlah pertanyaan yang well-typed dalam sistem tipe yang masuk akal, dan khususnya juga tidak memenuhi syarat “stratifiability” NF, sehingga kita tidak bisa membentuk himpunan paradoks Russell, yaitu himpunan semua himpunan yang tidak memuat dirinya sendiri.
Definisi “dapat distratifikasi” juga tidak terlalu rumit. Sebaliknya, ZF memiliki delapan aksioma/skema aksioma yang terlihat cukup ad hoc.
Saya menemukan tulisan ini karena penasaran apa perbedaan mendasar Coq dan Lean, dan apakah keduanya berjalan di atas jenis logika yang sama 1.
Saya hampir tidak memahami diskusi itu dan tidak benar-benar memakai keduanya. Kalau ada penjelasan tambahan terkait itu atau perbandingan dengan proof assistant lain, saya ingin mendengarnya.
1 https://proofassistants.stackexchange.com/questions/153/what...
Ada perbedaannya, dan diskusi ini juga layak dilihat 1
1 https://github.com/coq/coq/issues/10871
Sepertinya para pendukung Lean agak melebih-lebihkan cara mereka menggambarkannya. Lean bukanlah metode pembuktian yang lebih unggul seperti yang sering diisyaratkan, melainkan cara pembuktian alternatif.
Saat mencoba mempelajari Lean, Anda segera menyadari bahwa ia adalah bahasa pemrograman sekaligus sistem yang memiliki bug sendiri, dan sangat bergantung pada berbagai tumpukan pustaka yang ditulis manusia lain. Pustaka-pustaka itu melibatkan pilihan tertentu, dan bisa saja memiliki celah atau bug.
Karena itu, saya kurang setuju dengan ungkapan seperti “Lean mengatakan bahwa bukti itu bagus”. Ungkapan yang lebih tepat dan jujur menurut saya adalah bahwa bukti yang ditulis itu telah diverifikasi oleh matematikawan manusia, lalu diterjemahkan oleh manusia ke dalam Lean dan diverifikasi juga di sana. Gagasan bahwa Lean memberikan satu-satunya verifikasi emas tidak sepenuhnya akurat, atau setidaknya saya belum melihat penjelasan yang membuktikannya. Subjudul “Digitalisasi bukti Randall Holmes” tampaknya adalah ungkapan yang paling akurat.
Saya memandang bukti yang diverifikasi mesin dalam sistem kuat seperti Lean jauh lebih unggul daripada bukti yang hanya diverifikasi manusia. Manusia memang luar biasa, tetapi mereka bosan dan kadang melewatkan detail.
Ini bukan sekadar klaim teoretis. Orang-orang membaca Elements karya Euclid selama lebih dari 2.000 tahun sebelum menyadari ada aksioma yang hilang. Itu adalah kesalahan mendasar yang semestinya akan langsung terlihat oleh sistem verifikasi bukti mesin yang berfungsi baik.
Banyak bukti matematika yang sudah dipublikasikan juga kemudian terbukti salah. Seiring matematika makin rumit, manusia makin sulit memverifikasi setiap langkah dengan benar. Mesin memang belum sebagus manusia dalam menghasilkan bukti, tetapi untuk verifikasi, tidak ada tandingannya.
Ada juga sistem yang “bersaing” dengan Lean, jadi saya tidak akan bilang Lean adalah “satu-satunya jalan yang benar”. Saya juga menyukai Metamath, misalnya. Namun “persaingan” di antara sistem-sistem ini memang perlu diberi tanda kutip. Masing-masing punya kelebihan dan kekurangan, dan ada banyak orang yang menyukai, memakai, atau berkontribusi pada beberapa sistem sekaligus. Semuanya bisa memverifikasi teorema dengan tingkat ketelitian yang tidak realistis bagi manusia.
Mungkin saja ada bug, tetapi menurut pemahaman saya, yang perlu dipercaya hanyalah kernel.
Jika “berbagai tumpukan pustaka yang ditulis manusia lain” itu merujuk pada mathlib, saya rasa itu kurang tepat. Kode mathlib pada akhirnya dikompilasi menjadi kode yang diproses oleh kernel juga.
Draf makalah di situs web 0 juga menegaskan hal ini: Lean memang proyek besar, tetapi untuk menjamin bahwa bukti yang diterima itu benar, cukup percaya pada kernel. Bahkan jika taktik menghasilkan term bukti yang salah, kernel masih punya kesempatan untuk menemukan kesalahan itu sebelum menerima buktinya.
Perbedaannya adalah bahwa di Lean, Anda hanya perlu mempercayai kernel. Sisanya dibangun di atasnya. Jika kernel itu sound, maka semua yang lain juga sound.
Ini sangat berbeda dari bahasa pemrograman pada umumnya. Dalam bahasa biasa, bug bisa masuk kapan saja. Ini juga sangat berbeda dari matematika, di mana lemma mana pun bisa memuat kesalahan.
Hal keren dari pembukti teorema adalah, dengan asumsi kernel benar, bukti yang salah bahkan tidak akan bisa dikompilasi.
Untuk bukti, tidak ada bug yang hanya muncul saat runtime seperti pada perangkat lunak tradisional. Bahkan tidak ada runtime sama sekali.
Lean memang bisa dipakai sebagai bahasa pemrograman “umum”, dan dalam konteks itu ada risiko bug runtime, tetapi di sini bukan itu yang sedang dibahas.
Anda salah paham tentang pembukti teorema. Ini bukan persoalan setingkat “semua abstraksi pasti bocor”. Tidak perlu mempercayai pustaka; yang perlu dipercaya hanya kernel.
Mempercayai kernel pun bukan hal sepele, tetapi dibanding bukti informal, ini adalah lompatan besar. Dalam bukti informal, Anda memang harus mempercayai “pustaka”, yakni budaya dan pengetahuan orang lain, karena tidak ada cara praktis untuk benar-benar merebus semuanya hingga ke level aksioma.
Apakah ini berarti ZFC mati dan hiduplah NF?
Sebagai matematikawan amatir yang terutama menggunakan himpunan sebagai bahasa umum untuk menjelaskan hal-hal lain, saya tidak benar-benar tahu implikasinya bagi bidang matematika yang lebih luas. Terutama jika kegunaan NF mirip dengan ZFC yang ada sekarang dan berbagai variannya.
Apakah NF diperkirakan akan menjadi sama populernya dengan ZFC dalam pembuktian mesin? Keberadaan himpunan semesta terasa lebih intuitif, jadi setidaknya berkat bukti ini minat pribadi saya terhadap formalisasi hidup lagi.
Dari sudut pandang amatir yang naif, karena semua model ZFC bisa diperluas menjadi model NF, hasil konsistensi relatif ini tampaknya membuat NF setidaknya sama bergunanya dengan ZFC.
Tetapi saya rasa NF tidak akan menjadi jauh lebih berguna kecuali salah satu dari hal berikut terjadi:
NF terbukti kontradiktif. Kalau begitu ZFC juga kontradiktif. Bintang-bintang di langit malam mulai padam satu per satu ;)
ZFC terbukti kontradiktif. Kalau begitu masih ada kemungkinan NF konsisten. Semoga beruntung.
Tentu saja, besar kemungkinan saya melewatkan keunggulan “kualitas hidup” NF yang lebih praktis, seperti bisa berbicara tentang proper class, atau menghindari paradoks Russell dengan rumus bertingkat.
Sama sekali tidak ada niat untuk mendorong NF sebagai sistem fondasi yang berdiri sendiri. NF adalah sistem yang cukup aneh.
Meski begitu, jika ada yang ingin mendorongnya, saya akan bilang bahwa hasil konsistensi ini setidaknya berarti risikonya tidak lebih besar daripada risiko mencapai kontradiksi di ZFC.
Saya sangat menyukai ini.
Saya jadi bertanya-tanya apakah pada akhirnya ini akan mengarah ke pembuktian kolaboratif dan “perbaikan bug”, sehingga matematika menjadi proses yang mirip dengan kode di GitHub.
Andai saya punya waktu luang untuk mengikuti proyek mathlib. Ini benar-benar keren.
Apakah ada cara untuk ikut terlibat meskipun sangat santai?
Anda bisa mulai dari Natural numbers game.
https://adam.math.hhu.de/#/g/leanprover-community/NNG4
Saya bukan orang di bidang ini, tapi bukankah ada teorema Gödel yang mengatakan bahwa semua sistem yang cukup kuat tidak bisa menunjukkan konsistensinya sendiri?
Namun, meskipun sistem X tidak bisa membuktikan konsistensinya sendiri, sistem Y yang lebih kuat bisa membuktikan konsistensi X. Dan sistem lain yang lebih kuat lagi juga bisa membuktikan konsistensi Y. Dengan begitu terbentuk rantai di mana tiap sistem membuktikan konsistensi sistem yang lebih lemah
Ini tidak membuktikan bahwa sistem tersebut konsisten secara absolut. Jika Y kontradiktif, maka bisa dibuktikan baik bahwa X konsisten maupun bahwa X kontradiktif. Meski begitu tetap ada nilainya. Lagipula salah satu alasan kita memakai Y adalah karena kita tidak mengetahui adanya kontradiksi di dalamnya. Sistem formal sering kali bisa kontradiktif secara halus, jadi “konsisten dengan asumsi sistem lain konsisten” jauh lebih baik daripada “sama sekali tidak ada bukti konsistensi”
Sistem yang kontradiktif pun bisa membuktikan konsistensinya sendiri. Jadi meskipun suatu sistem memiliki pembuktian bahwa dirinya konsisten, kita tetap tidak tahu apakah ia benar-benar konsisten
Diskusi di Reddit yang juga diikuti salah satu pembuatnya layak dibaca 0
https://old.reddit.com/r/math/comments/1ca6bj8/new_foundatio...