Seorang pembangun telah memulakan projek yang bercita-cita tinggi untuk memformalkan Principia Mathematica karya Bertrand Russell menggunakan pembukti teorem Lean4, mencetuskan perbincangan tentang cabaran falsafah dan praktikal yang wujud dalam usaha sedemikian.
Projek ini bertujuan untuk menterjemahkan bukti logik kompleks Russell ke dalam rangka kerja pengkomputeran moden, dengan pembangun tersebut menyatakan bahawa mereka sangat menantikan untuk memformalkan bukti 1+1 yang terkenal. Pada masa ini, projek tersebut kelihatan masih di peringkat awal, dengan hanya teorem proposisi awal yang telah siap.
 |
|---|
| Halaman dari teks matematik yang menggambarkan teorem dan pembuktian logik formal, serupa dengan yang sedang diformalkan dari Principia Mathematica karya Russell |
Batasan Falsafah Principia
Perbincangan komuniti mendedahkan ketegangan asas pada teras projek ini. Walaupun pelaksanaan teknikal dalam Lean4 adalah mengagumkan, beberapa pengomen menunjukkan bahawa Principia Mathematica itu sendiri dianggap oleh sesetengah pihak sebagai asasnya cacat. Seorang pengomen merujuk kepada pencirian Freeman Dyson tentangnya sebagai kegagalan monumental, menghuraikan bagaimana teorem ketidaklengkapan Gödel secara berkesan melemahkan matlamat asas Principia.
Principia ditulis semasa era Logisis naif dalam falsafah matematik yang tidak dapat meramalkan isu kebolehputusan asas yang serius dalam logik seperti teorem ketidaklengkapan Godel, atau Masalah Penamatan.
Konteks sejarah ini penting untuk memahami kedua-dua kepentingan dan batasan projek pemformalan ini. Karya Russell dan Whitehead mendahului pemahaman moden kita tentang batasan yang wujud dalam sistem formal, menjadikan sebarang pemformalan lengkap secara inherennya bermasalah.
 |
|---|
| Perwakilan visual berstruktur tentang bukti logik, menekankan kerumitan dan cabaran falsafah yang dibincangkan berkaitan dengan Principia Mathematica |
Pendekatan Falsafah yang Bersaing
Komen-komen tersebut menyoroti bagaimana komuniti matematik terbahagi kepada kem falsafah yang berbeza selepas cabaran terhadap logisisme muncul. Formalis (mewakili matematik arus perdana) mengakui kenyataan yang tidak dapat diputuskan tetapi mengekalkan bahawa kebenaran matematik wujud secara bebas daripada keupayaan kita untuk membuktikannya. Sebaliknya, Konstruktivis menyamakan kebenaran matematik dengan kebolehbuktian, menolak hukum pertengahan yang dikecualikan Aristotle dan membina matematik pada asas logik alternatif.
Perbezaan falsafah ini bukan sekadar akademik—ia secara langsung mempengaruhi bagaimana seseorang mungkin mendekati pemformalan Principia. Pembangun projek ini pasti akan menghadapi keputusan tentang bagaimana menangani kenyataan yang Gödel buktikan tidak dapat diputuskan dalam sistem itu sendiri.
Pendekatan Falsafah Utama terhadap Asas Matematik
- Logisisme: Percubaan untuk menerbitkan semua matematik daripada logik tulen (pendekatan Russell)
- Formalisme: Mengakui kenyataan yang tidak dapat diputuskan tetapi mengekalkan bahawa kebenaran matematik wujud secara bebas
- Konstruktivisme: Menyamakan kebenaran matematik dengan kebolehbuktian, menolak hukum pertengahan yang dikecualikan
Status Projek
- Kemajuan semasa: Hanya teorem proposisional awal
- Matlamat: Penformalan lengkap jilid pertama Principia Mathematica
- Sasaran penting: Bukti "1+1"
Pelaksanaan Teknikal dan Alat
Walaupun menghadapi cabaran falsafah ini, aspek teknikal projek ini menunjukkan harapan. Pembangun telah melaksanakan taktik khusus dalam Lean4 untuk mencerminkan notasi Russell, terutamanya untuk penaakulan silogistik. Perhatian ini untuk mengekalkan kesetiaan kepada karya asal sambil memanfaatkan keupayaan pembuktian teorem moden menunjukkan pendekatan yang bijak.
Beberapa pengomen mencadangkan alat alternatif seperti Naproche yang mungkin sesuai untuk kerja pemformalan jenis ini. Ini menyoroti ekosistem yang semakin berkembang untuk alat pengesahan formal dan pembuktian teorem yang tersedia untuk ahli matematik dan saintis komputer moden.
Projek ini, walaupun masih di peringkat awal, mewakili persilangan menarik antara matematik sejarah, falsafah logik, dan pendekatan pengkomputeran moden untuk pengesahan formal. Sama ada ia akhirnya berjaya dalam matlamatnya yang bercita-cita tinggi atau tidak, ia memberikan pandangan berharga tentang kedua-dua kekuatan dan batasan sistem formal dalam matematik.
Rujukan: Memformalkan Principia Mathematica Bertrand Russell Menggunakan Lean4