Aritmetika Peano sudah memadai, karena Aritmetika Peano dapat mengenkode komputasi

• Aritmetika Peano (PA) dapat merepresentasikan proses komputasi mekanis, sehingga pemusnahan setiap deret Goodstein tunggal dapat dibuktikan di dalam PA
• Melalui bentuk normal Cantor dan notasi bilangan ordinal herediter, deret Goodstein dan sifat menurunnya dapat direpresentasikan, sehingga konstruksi bukti dengan panjang hingga menjadi mungkin
• Dengan induksi (induksi kuat/induksi transfinita), bukti dapat diperluas masing-masing hingga ordinal pada tingkat tertentu
• PA dapat membuktikan bahwa untuk setiap bilangan asli n, “G(n) mencapai 0”, tetapi pembuktian menyeluruh atas teorema Goodstein secara keseluruhan (untuk semua n) tidak dimungkinkan
• Dengan PA, pengodean komputasi, struktur data (List, Pair, dll.), bahkan bahasa pemrograman (Lisp) itu sendiri, serta pengodean proses pembuktiannya sendiri juga dapat diimplementasikan dengan cukup baik

---

Pendahuluan dan latar belakang masalah

• Tulisan ini menjelaskan bahwa Aritmetika Peano (PA) dapat membuktikan bahwa deret Goodstein “untuk setiap n mencapai 0 (G(n) terminates)”
• Ini mungkin tampak sepele bagi ahli logika, tetapi dijelaskan dari sudut pandang pengodean komputasi agar dapat dipahami oleh programmer
• Untuk setiap kasus deret Goodstein, dapat disusun rutin pembuktian yang konkret di dalam PA

Ordinal dan deret Goodstein

• Dengan pendekatan Von Neumann, ordinal (Sets as Ordinals) dibangun
  • 0 adalah himpunan kosong, 1 adalah {0}, 2 adalah {0,1}, ω adalah {0,1,2,…}, ω+1 adalah {0,1,2,…,ω}, dan seterusnya, dengan urutan yang terdefinisi baik
• Deret Goodstein dijelaskan melalui notasi basis herediter yang menggunakan bentuk normal Cantor
  • Contoh: ω^ω adalah ((1,ω)), yaitu ((1,(1,1)))
  • Urutan < ditentukan dengan perbandingan leksikografis terhadap ordinal/koefisien tiap suku

Induksi dan induksi transfinita

• Induksi dalam Aritmetika Peano: jika benar untuk 0, dan benar dari n→n+1, maka benar untuk seluruh bilangan asli
• Induksi kuat juga dapat dibuktikan di dalam PA
• Induksi transfinita: dalam ZFC dan sejenisnya, ini dapat diperluas ke ordinal tak hingga dan diterapkan pada bilangan yang ditulis dalam bentuk normal Cantor
  • Teorema 1: deret menurun dalam bentuk normal Cantor selalu berhingga
  • Teorema 2: induksi transfinita dapat digunakan untuk bilangan dalam bentuk normal Cantor

Induksi transfinita dalam PA dan panjang bukti deret Goodstein

• PA dapat menghasilkan bukti pemusnahan deret Goodstein untuk sembarang n
  • Bukti dapat disusun berdasarkan tinggi menara m=O(log* n) (iterated log) dari bentuk normal Cantor
  • Pada tiap langkah, keseluruhan panjang bukti menjadi O(m^2) dengan menggabungkan m bukti, atau dapat dipersingkat menjadi O(m log m) jika notasi khusus (ω[m]) diperkenalkan
• Namun, pembuktian teorema Goodstein secara keseluruhan (untuk semua n) tidak mungkin di dalam PA (karena induksi transfinita atas ε0 tidak dimungkinkan)
  • Jika itu mungkin, maka konsistensi PA juga akan dapat dibuktikan, yang bertentangan dengan Teorema Ketaklengkapan Kedua Gödel

Pengodean program dan struktur data dalam PA

• PA cukup mampu mengenkode komputasi/program/struktur data (angka, pasangan, daftar, dan semua struktur lain)
• Berbagai fungsi dapat diimplementasikan dengan cara seperti berikut:
  • logika dan operasi dasar (+, *, pow, //, %, min, max, dll.)
  • pattern matching dan percabangan kondisi (if, cond, dll.)
  • mengenkode satu angka menjadi dua angka (pasangan), atau memperluasnya lagi dari pasangan menjadi daftar dan struktur yang lebih kompleks secara berulang (daftar rekursif, pohon, teks, dll.)
• Dengan pengodean struktur data ini, bahkan dapat dibangun interpreter untuk mesin virtual/bahasa pemrograman arbitrer (seperti Lisp)

Bootstrap ke Lisp dan pengodean

• Dengan menggunakan Lisp sebagai contoh, dijelaskan cara mengimplementasikan operasi numerik dan logika dasar, struktur data, serta interpreter/interpretor bahasa pemrograman
• Seluruh struktur Lisp (pemetaan perintah/argumen, special form, macro, dll.) dapat diimplementasikan dalam PA melalui kombinasi fungsi yang sesuai
• Lebih jauh lagi, proses pembuktian PA itu sendiri, prosedur pembuktian logis, hingga struktur swa-rujuk juga dapat dienkode dan diimplementasikan secara simbolik di dalam PA

Pengodean logika itu sendiri di dalam PA

• Dalam logika matematika, proses pembuktian First-Order Logic dapat dienkode sebagai data bilangan di dalam PA
• Setiap langkah pembuktian/proposisi/aturan inferensi/pemeriksaan validitas bukti dikenali dan diproses sebagai rangkaian fungsi numerik/pemrosesan daftar
• Pengodean metateoretis dan swa-rujuk seperti ini terhubung hingga ke pembuktian ketaklengkapan Gödel dan masalah Halting

Kesimpulan

• Komputasi, struktur data, program, hingga proses pembuktian logis dapat dienkode, dibuktikan, dan diinterpretasikan dengan memadai di dalam PA
• Karena itu, setiap deret Goodstein arbitrer (untuk n tertentu, G(n) musnah) dapat dibuktikan secara konkret di dalam PA
• Namun, pembuktian bahwa "PA membuktikan teorema Goodstein di dalam PA" untuk teorema Goodstein secara keseluruhan (semua n) tidak mungkin dilakukan karena batas-batas logika
• Dari sudut pandang programmer, PA adalah fondasi logis yang lengkap untuk mengenkode komputasi itu sendiri

[GN⁺]

Komentar Hacker News

• Tulisan ini adalah posting blog yang saya buat dari pertanyaan yang pernah saya ajukan di Stack Overflow. Isinya mencakup penjelasan tentang batasan apa saja yang bisa dibuktikan dalam aksioma Peano dan bagaimana melakukan bootstrap Lisp di dalam aksioma Peano. Sebagian besar lelucon ada di bagian kedua. Koreksi atau pertanyaan tambahan juga sangat diterima.
  • Saat membaca ini, saya menemukan ada tanda kurung yang tidak cocok di bagian "Why Lisp?" (lihat contoh (defun not (x) (if x false true)). Begitu seseorang mulai memakai tanda kurung, saya refleks memeriksa apakah semuanya tertutup dengan benar. Lalu ketika setelah itu disebutkan bahwa "mengecek keseimbangan tanda kurung mudah diprogram dengan komputer", saya tertawa keras. Lelucon seperti ini benar-benar lucu, dan komentar ; After a while, you stop noticing that stack of closing parens. di bagian "Basic Number Theory" juga berkesan. Sudah lama saya tidak bersentuhan lagi dengan Lisp, dan tulisan ini benar-benar menyenangkan.
  • Tulisan ini sangat menarik. Saya baru membaca pengantarnya saja, tetapi menarik bahwa di dalam aksioma Peano (PA), kita bisa membuktikan bahwa setiap kasus khusus dari deret Goodstein mencapai 0, tetapi tidak bisa membuktikan bahwa 'semua' kasus mencapai 0. (Sebenarnya hasil itu cukup masuk akal, tetapi tetap sangat menarik.) Dan kenyataan bahwa komputasi bisa dienkode hanya dengan aksioma Peano juga terasa sangat aneh. (Secara prinsip memang masuk akal, tetapi sebelumnya saya belum pernah memikirkan satu lapis referensi-diri lagi.) Kebetulan akhir-akhir ini saya juga mencoba belajar teori himpunan lebih dalam dan sudah sampai bagian deret Goodstein di buku Intro to Set Theory. Kalau ada yang punya rekomendasi buku teori himpunan tingkat lanjut atau buku yang membahas aritmetika Peano secara lebih mendalam, saya akan sangat berterima kasih. Target kecil saya adalah memahami mengapa PA tidak cukup untuk membuktikan teorema Goodstein, tetapi saya juga terbuka untuk jalur lain yang direkomendasikan.
  • Ada dua tempat di mana penulisan omega lupa ditulis sebagai \omega.
• Ini sangat mirip dengan teori Boyer-Moore, yaitu teori yang membangun matematika pada tingkat aksioma Peano. Boyer dan Moore mengembangkan prover teorema otomatis yang mengimplementasikan teori ini, dan saya juga punya salinannya yang berjalan di GNU Common LISP. Tautan ke makalah "A Computational Logic" dan implementasi nqthm juga layak dilihat. Salah satu hal yang mengesankan dari makalah itu adalah contoh bahwa jika mulai dari aksioma Peano, teorema rumit seperti perkalian bilangan prima itu sulit, tetapi hukum komutatif penjumlahan, hukum distributif perkalian, dan teorema terkait fungsi GCD tetap cukup bisa dibuktikan.
• Saya punya latar belakang di matematika dan pemrograman, dan secara pribadi yang lebih menarik bagi saya adalah bahwa bagian independensi teorema Goodstein tampaknya bisa dielakkan secara self-referential. Saya menduga jika kita menambahkan asumsi PA+"PA omega-consistent" maka mungkin teorema Goodstein bisa dibuktikan, dan mungkin itu juga memungkinkan induksi transfinit hingga epsilon_0. EDIT: Atau mungkin cukup dengan menambahkan "PA konsisten" saja?
  • Sayangnya tidak begitu. Dan bukan hanya Con(PA), tetapi bahkan formula apa pun yang dikuantifikasi secara universal juga tidak cukup. Lihat jawaban Math StackExchange terkait. Terkait pertanyaan pertama, saya jadi penasaran bagaimana omega-consistency dienkode sebagai formula di dalam PA; saya tidak langsung tahu caranya.
  • Saya adalah penanya di Stack Overflow. Saya juga sudah menambahkan beberapa tautan jawaban pada pertanyaan itu. Intinya, hanya "PA konsisten" memang tidak cukup, tetapi semacam "prinsip refleksi seragam" yaitu "jika terbukti di PA maka benar" sudah cukup. Saya tidak yakin apakah prinsip ini benar-benar sama dengan omega-consistency, tetapi dari penjelasan di Wikipedia, saya membacanya seolah-olah demikian. Jika T omega-consistent, maka artinya "T + RFN_T + himpunan semua formula yang benar adalah konsisten", dan ini ditafsirkan setara dengan "T + RFN_T adalah benar".
  • Saya juga menyukai struktur induktif (rekursif) seperti ini. Pada akhirnya kita membuat meta-pembuktian tentang apa yang dibuktikan PA, dan jika kita memercayai PA, kita juga bisa memercayai meta-pembuktian itu. Bagian bahwa cukup dengan "PA konsisten" saja belum benar-benar saya pahami. Menurut saya, PA+"PA konsisten" akan tetap memungkinkan adanya model di mana teorema Goodstein benar pada bilangan asli standar, tetapi juga model di mana teorema Goodstein salah untuk suatu bilangan bulat nonstandar N. Saya kira pernyataan yang lebih kuat berupa omega-consistency dibutuhkan untuk menyingkirkan kasus seperti ini.
  • Di posting Math Exchange disebutkan bahwa pembuktian PA+induksi transfinit(epsilon_0) membuktikan PA itu sendiri. Saya rasa PA+"PA konsisten" seharusnya cukup untuk membuktikan induksi transfinit hingga epsilon_0.
  • Sepertinya topik ini sudah melewati detail yang cukup aman untuk saya komentari dengan percaya diri. Menurut ChatGPT, penjelasannya adalah bahwa "PA+PA konsisten" saja memang tidak cukup. Mengingat ChatGPT sudah menelan begitu banyak buku logika, saya rasa klaim seperti itu cukup bisa dipercaya.
• Komentar yang saya tulis untuk JoJoModding di Stack Overflow tidak benar. Saya menulis bahwa "karena model PA nonstandar punya bilangan asli tak hingga, maka walaupun PA membuktikan bahwa ia membangun suatu pembuktian, PA tidak bisa membuktikan bahwa panjangnya berhingga". Namun sebenarnya, jika PA membuktikan "PA membuktikan X", maka PA juga membuktikan X itu sendiri. Hal pentingnya bukan keberadaan model nonstandar, melainkan fakta bahwa model bilangan asli standar adalah model dari PA. Jadi jika "PA membuktikan bahwa PA membuktikan X", secara efektif terbentuk satu pembuktian yang sesuai dengan bilangan asli hingga standar, dan dari bilangan itu kita bisa membangun pembuktian nyata untuk X di dalam PA.
  • Saya belum sempat memeriksa logikanya lebih rinci, tetapi dalam bahasa alami tampaknya kuncinya adalah perbedaan antara "PA membuktikan 'forall n, G(n)'" dan "PA membuktikan 'forall n, Provable(G(n))'". Saya kurang kuat di logika, jadi kalau ada yang bisa menjelaskan secara konkret mengapa dari pembuktian forall n, Provable(P(n)) kita tidak bisa memperoleh Provable(forall n, P(n)), saya akan sangat berterima kasih.
  • Pernyataan "jika PA membuktikan 'PA membuktikan X', maka PA membuktikan X" itu tidak benar. Kita bisa membuat fungsi di dalam PA yang menelusuri semua pembuktian yang mungkin, dan saya memang membuat sketsa metode ini di bagian akhir jawaban. Dari sini kita juga bisa membuat fungsi seperti will-return, opposite-return, dan seterusnya, yang sesuai dengan pembuktian standar masalah halting. Jika mempertimbangkan kasus opposite-return(opposite-return, opposite-return), maka jika PA membuktikan bahwa opposite-return akan mengembalikan hasil, itu juga membuktikan bahwa ia sebenarnya tidak akan mengembalikan hasil; sebaliknya, jika membuktikan bahwa ia tidak akan mengembalikan hasil, maka itu juga membuktikan bahwa ia akan mengembalikan hasil. Jika PA mengadopsi pernyataan yang lebih kuat seperti "semua yang dapat dibuktikan memang benar-benar dapat dibuktikan", itu langsung menabrak teorema ketaklengkapan kedua Gödel dan berarti PA kontradiktif. Jadi "PA membuktikan" dan "PA membuktikan bahwa ia membuktikan" memang harus dibedakan.
• Kalkulus lambda murni saja juga sudah cukup, karena kalkulus lambda itu sendiri dapat mengenkode komputasi.
• Saat membicarakan tipe data induktif dengan seseorang, saya menunjukkan definisi Nat yang dibangun dari zero/succ (seperti di Lean atau Rocq). Orang itu bertanya-tanya, "Apakah ini saja cukup?", "Apakah kita benar-benar butuh aksioma Peano? Apakah ada sesuatu yang lebih primitif daripada tipe data induktif?" dan semacamnya. Ini membuat saya berpikir bahwa kita sebaiknya sering mengingatkan diri bahwa aksioma Peano bukan sesuatu yang secara esensial sudah pasti, melainkan hanya salah satu desain.
  • Sebagai jawaban atas "apakah ada sesuatu yang lebih fundamental daripada tipe data induktif?", saya cenderung berpikir bahwa bilangan asli itu sendiri lebih primitif daripada tipe data induktif. Semua tipe data induktif dapat dibangun hanya dengan bilangan asli dan beberapa konstruktor tipe primitif lainnya (Π, Σ, =, Ω).
• Lihat Q&A tentang teorema Kirby-Paris.
• Terkait konsistensi PA, ada materi video yang dibagikan tentang apa yang bisa dibuktikan di dalam PA tautan YouTube
  • Ini bagian yang wajib dijelaskan kepada orang yang bukan ahli logika. Menurut teorema ketaklengkapan kedua Gödel, jika PA bisa membuktikan konsistensinya sendiri, maka PA akan menjadi kontradiktif (dan karenanya apa pun, termasuk yang salah, bisa dibuktikan). Video ini tidak menunjukkan bahwa PA membuktikan dirinya kontradiktif, melainkan bahwa PA dapat membuktikan "konsistensinya sendiri" dalam makna yang lebih lemah. Sulit memahaminya dengan tepat tanpa mengetahui dasar-dasar logika, tetapi tetap sangat menarik.
• Topik ini mendapat 123 poin, tetapi posting aslinya di SO hanya punya 11 upvote.
  • Di Stack Overflow, seseorang harus punya 15 poin untuk bisa memberi upvote. Bisa jadi orang enggan berkontribusi karena masalah reputasi, dan batas 15 poin itu tampaknya memang menghambat upvote.
• Apakah komputasi saja cukup? Bilangan real yang dapat dihitung hanyalah subhimpunan dari semua bilangan real.
  • Saya pikir nama "bilangan real" sendiri adalah penamaan yang menyesatkan. Bilangan real bisa diartikan sebagai rasio fisik yang nyata. Misalnya, ketika kita mengatakan 180.255 pon, maksudnya adalah rasio fisik nyata antara berat badan Jones yang sebenarnya dan satuan pon standar. Rasio seperti itu juga eksis secara fisik; dalam arti itu, bilangan real bisa dipahami sebagai rasio fisik. Sebaliknya, sekarang lebih umum memandang angka sebagai konsep abstrak yang terlepas dari kenyataan, yang secara khas merupakan pandangan Platonis. Tetapi dalam dunia nyata, mustahil mengukur atau merepresentasikan sesuatu dengan presisi tak terbatas. Misalnya, pengukuran dengan presisi lebih dari 50 digit tidak mungkin karena batas mekanika kuantum. Jika ingin mengukur orbit benda-benda di tata surya tanpa galat, lewat 50 digit kita harus memperhitungkan efek massa bintang terdekat, lewat 100 digit kita harus memodelkan seluruh galaksi, dan pada akhirnya kita harus mempertimbangkan pengaruh fisik yang bahkan tak mungkin diukur. Jadi di dunia nyata, hanya matematika dengan presisi terbatas yang mungkin dilakukan. Artinya, pada prinsipnya semuanya dapat dihitung, tetapi ketika menuju tak hingga, model matematis itu sendiri menjadi tidak bermakna.
  • Benarkah begitu? Sebenarnya gagasan bahwa yang tak terhitung (uncountable) itu "lebih banyak" berangkat dari kesalahpahaman. Lihat penjelasan saya. Jika menerima bahwa yang tak terhitung itu lebih banyak, maka kita terpaksa mengambil sikap yang kontroversial tentang "eksistensi". Lihat diskusi terkait. Terakhir, bahkan jika kita menelusuri logika sampai akhir, semuanya tetap bisa direpresentasikan di komputer. Bahkan bila menambahkan himpunan besar ke ZFC, kita tetap bisa mulai dari PA dan menarik semua kesimpulan sesuka hati, jadi secara praktis saya menilai PA saja sudah cukup. Jika butuh bujukan lebih lanjut, saya merekomendasikan buku Gödel, Escher, Bach.
  • Pendekatan saya agak berbeda. Bilangan real secara umum memang tidak bisa ditangani dalam bentuk komputasi, simbolisasi, pencatatan, atau bentuk apa pun, tetapi 'pernyataan' tentang bilangan real sering kali tetap bisa diekspresikan dan dihitung dengan berguna. Saya sangat tertarik pada upaya, seperti yang dilakukan Harvey Friedman atau penulis tulisan ini, untuk menghasilkan nilai yang jauh lebih rumit daripada yang dibayangkan dari sistem yang sederhana. (Catatan: situs web audiomulch tidak bisa diakses.)
  • Tanpa target pada kata "cukup", pertanyaan ini tidak punya definisi yang jelas. Cukup untuk apa, itulah yang penting.
  • Saya pikir pertanyaan "apakah komputasi saja cukup?" sendiri salah. Tentu saja tidak cukup. Kalau cukup, maka sebagian orang yang memandang realitas seperti jam mekanis yang mudah dipercaya akan ternyata sepenuhnya benar. Kenyataannya jauh lebih menarik dan lebih kompleks daripada itu.