Mengapa aritmetika Peano saja sudah cukup: PA dapat mengodekan komputasi

 (math.stackexchange.com)
1 poin oleh GN⁺ 2025-06-15 | 1 komentar | Bagikan ke WhatsApp
  • PA tidak dapat membuktikan keseluruhan teorema Goodstein ∀n G(n), tetapi untuk setiap bilangan asli standar n, keberadaan bukti PA untuk G(n) dapat ditunjukkan di dalam PA
  • Intinya adalah konstruksi yang secara mekanis menghasilkan bukti induksi transfinit hanya sampai menara pangkat ω dengan tinggi hingga batas hingga yang diperlukan untuk n
  • Tinggi yang dibutuhkan m bersesuaian dengan tinggi hereditary base notation dari n dan bernilai O(log*(n)), dan bila memakai notasi singkat ω^[m], panjang bukti dapat diperkecil hingga sekitar O(m log m)
  • Hasil ini berarti “bukti untuk tiap kasus bisa dibuat”, bukan bahwa PA membuktikan seluruh teorema Goodstein
  • PA dapat mengodekan bilangan, pasangan, daftar, status program, dan bukti logika formal semuanya ke dalam satu bilangan asli, sehingga apakah bukti yang dihasilkan benar-benar merupakan bukti PA juga dapat diverifikasi di dalam PA

Bentuk matematis dari pertanyaan

  • Objek yang dibahas adalah pernyataan G(n) bahwa barisan Goodstein pada akhirnya mencapai 0

  • Pembedaan yang sudah diketahui adalah sebagai berikut

    • PA dapat membuktikan tiap kasus konkret untuk bilangan asli standar, seperti G(15) dan G(268)
    • PA tidak dapat membuktikan pernyataan keseluruhan ∀n ∈ N: G(n)

  • Pertanyaannya adalah apakah PA dapat membuktikan pernyataan dengan bentuk berikut

    ∀n ∈ N: ∃p ∈ N: P_PA(p, ⌜G(n)⌝)

  • P_PA(p, ⌜φ⌝) berarti bahwa p adalah kode bukti dari φ di dalam PA

  • Kesimpulannya adalah bahwa pada tingkat ini, PA saja sudah cukup

Apa yang harus dibuktikan oleh PA

  • Untuk setiap n, ada tiga hal berikut yang perlu ditunjukkan oleh PA
    • dapat menghitung panjang bukti yang diperlukan untuk membuktikan G(n)
    • prosedur yang menyusun bukti tersebut berhenti
    • kalimat terakhir dari bukti yang disusun menyatakan terminasi G(n)
  • Untuk setiap G(n), dapat disusun bukti PA dengan panjang O(log*(n) log(log*(n)))
  • log* adalah iterated logarithm dan merupakan fungsi yang tumbuh sangat lambat
  • Karena makin besar n memerlukan bukti yang makin panjang, hal ini saja tidak berarti PA dapat membuktikan seluruh teorema Goodstein

Barisan Goodstein dan notasi ordinal

  • Barisan Goodstein menggunakan hereditary base notation, dan ini terhubung dengan representasi ordinal yang ditulis dalam bentuk normal Cantor

  • Dalam konstruksi ala John von Neumann, ordinal dibangun sebagai himpunan

    • 0 adalah himpunan kosong
    • jika ada ordinal ord, maka ord ∪ {ord} juga ordinal
    • jika ada himpunan ordinal X, maka gabungan dari X juga ordinal

  • Bentuk normal Cantor merepresentasikan ordinal sebagai berikut

    ((n1, ord1), (n2, ord2), ..., (nk, ordk))
    • setiap ni adalah bilangan asli positif
    • setiap ordi adalah ordinal
    • ord1 > ord2 > ... > ordk

  • Notasi ini menyatakan ordinal berikut

    n1·ω^ord1 + n2·ω^ord2 + ... + nk·ω^ordk

  • Perbandingan ditangani dengan perbandingan leksikografis dalam urutan ord1, n1, ord2, n2, dan jika salah satu sisi berakhir lebih dulu maka yang lebih pendek lebih kecil

Dari induksi ke induksi transfinit

  • Aksioma kelima PA menyediakan induksi pada bilangan asli
    • S(0) benar
    • jika S(n) maka S(s n) juga benar
    • maka S benar untuk semua bilangan asli
  • Dari sini PA dapat mendefinisikan < secara rekursif dan juga membuktikan induksi kuat
    • jika untuk semua n, dari kebenaran S pada semua bilangan yang lebih kecil dari n dapat disimpulkan S(n), maka S benar pada semua bilangan asli
  • Dalam ZFC, dapat dibuktikan induksi transfinit, yaitu induksi kuat pada seluruh ordinal
  • Untuk objek yang ditulis dalam bentuk normal Cantor, dipakai dua sifat berikut
    • setiap barisan menurun yang ditulis dalam bentuk normal Cantor pasti berhingga
    • induksi transfinit dapat diterapkan pada objek dalam bentuk normal Cantor

Cakupan induksi transfinit yang mungkin di dalam PA

  • PA tidak dapat membuktikan induksi transfinit untuk semua ordinal
  • Sebagai gantinya, rentang ordinal tertentu dengan tinggi hingga dapat ditangani di dalam PA
    • karena PA dapat membuktikan induksi kuat, PA dapat menangani induksi transfinit sampai ω
    • dengan logika yang sama, induksi transfinit untuk ω^ω juga dapat dibuktikan
    • dengan cara yang sama lagi, ini dapat diulang untuk ω^(ω^ω), ω^(ω^(ω^ω)), dan seterusnya pada menara dengan tinggi hingga
  • Bukti pada tiap tahap hanya berbeda pada tinggi menara dan dihasilkan secara mekanis
  • Jika menara ke-m ditulis apa adanya, panjang keseluruhan bukti adalah O(m^2)
  • Jika dipakai notasi singkat seperti ω^[m], penulisan m hanya memerlukan panjang O(log m), sehingga keseluruhan bukti menjadi O(m log m)
  • Untuk setiap ordinal di bawah ε₀, memang ada bukti induksi transfinit di dalam PA, tetapi untuk menggabungkan semuanya menjadi satu diperlukan bukti dengan panjang tak hingga
  • Jika PA dapat membuktikan induksi transfinit untuk ε₀, maka PA akan dapat membuktikan konsistensinya sendiri, yang bertentangan dengan teorema ketaklengkapan kedua Gödel

Prosedur pembangkitan bukti untuk tiap G(n)

  • Untuk n tertentu, yang diperlukan hanya sampai tinggi menara dari hereditary base notation tersebut
  • Tinggi ini adalah O(log*(n)) dan diperlakukan sebagai fungsi yang mudah dihitung oleh PA
  • Program, untuk masukan n, dapat menghasilkan hal-hal berikut
    • bukti fakta-fakta umum tentang PA
    • bukti bahwa G(n) melacak barisan menurun di dalam ω^[m] untuk suatu m
    • proses perhitungan m beserta bukti nilai m
    • bukti induksi transfinit untuk ω^[0]
    • bukti bahwa induksi transfinit pada ω^[i] mengimplikasikan induksi transfinit pada ω^[i+1]
    • bukti induksi transfinit untuk tiap tahap dari i = 0 sampai m-2
    • bukti bahwa induksi transfinit pada ω^[m-1] mengimplikasikan fakta bahwa semua barisan menurun di dalam ω^[m] berhingga
    • kesimpulan bahwa G(n) berhenti
  • PA dapat membuktikan hal-hal berikut tentang prosedur ini
    • prosedur tersebut berhenti
    • prosedur tersebut menghasilkan daftar kalimat
    • daftar itu diawali dengan aksioma Peano
    • setiap kalimat mengikuti secara logis dari kalimat-kalimat sebelumnya
    • dengan induksi, semua kalimat terbukti
    • kalimat terakhir adalah “G(n) berhenti”
  • Karena itu, untuk sembarang bilangan asli n, PA membuktikan fakta bahwa PA membuktikan terminasi G(n)

Cara PA mengodekan komputasi

  • “Pengodean” berarti menetapkan agar suatu bilangan asli tertentu mewakili struktur tertentu
  • Bahan dasar PA adalah sebagai berikut
    • 0
    • fungsi suksesor (s n)
    • kesamaan
    • pendahulu (p n) untuk bilangan yang bukan 0
    • definisi rekursif yang dibenarkan oleh induksi
    • kondisional yang bercabang menurut 0 atau 1
  • Di dalam PA, fungsi-fungsi aritmetika dasar berikut dapat didefinisikan secara rekursif
    • <
    • min, max
    • +
    • *
    • perpangkatan
    • sisa bagi %
    • pembagian bulat //
  • Sifat-sifat dasar fungsi-fungsi ini dapat dibuktikan di dalam PA dengan induksi

Membangun struktur data dari satu bilangan asli

  • Untuk mengodekan dua bilangan asli menjadi satu bilangan asli, bisa dipakai cara menyelang-selingkan bit biner
    • bit pada posisi ganjil adalah head
    • bit pada posisi genap adalah tail
  • Dari pasangan yang dibuat dengan cara ini, head dan tail dapat diambil kembali
  • Jika pasangan dapat dibuat, maka linked list juga bisa direpresentasikan
    • memakai 0 sebagai nil
    • daftar kosong
    • menambahkan elemen di depan
    • membaca kepala dan ekor
    • menghitung panjang
    • mengakses posisi sebarang
    • penyisipan dan penghapusan
  • Jika ada bilangan, pasangan, dan daftar, maka struktur seperti stack, queue, tree, dokumen teks, dan mesin virtual juga dapat direpresentasikan sebagai satu bilangan asli

Lisp dan pengodean prosedur komputasi

  • Lisp dipakai sebagai bahasa yang mudah untuk menjelaskan parsing dan interpretasi karena struktur tanda kurungnya dan bentuk command and arguments
  • Bilangan asli di dalam PA dapat ditafsirkan sebagai pasangan (type, value)
    • angka
    • boolean
    • pasangan
    • daftar
    • teks, dan sebagainya
  • Sebagian bilangan asli mungkin bukan nilai yang valid untuk tipe tertentu, tetapi nilai-nilai yang valid dapat secara unik merepresentasikan suatu struktur
  • Di atas pengodean ini, dapat dibangun struktur data Lisp, mesin virtual Lisp, dan interpreter Lisp
  • Karena Lisp Turing complete, melalui jalur ini setiap prosedur yang dapat dihitung beserta status prosedur itu dapat dikodekan di dalam PA
  • Status komputasi setelah sejumlah langkah tertentu juga dapat direpresentasikan dan dilacak di dalam PA

PA juga mengodekan bukti PA

  • Bukti dalam logika orde pertama dapat dipandang sebagai daftar kalimat
    • setiap kalimat adalah satu langkah inferensi
    • kalimat salah atau inferensi yang salah pun bisa saja ditulis, tetapi prosedur verifikasi dapat menyaringnya
  • Di dalam PA, dapat dibuat tipe seperti type-proof dan bukti dapat dikodekan sebagai daftar kalimat
  • Prosedur verifikasi berikut juga dapat dikodekan di dalam PA
    • memeriksa apakah bukti terbentuk dengan benar
    • memeriksa apakah tiap langkah bukti valid
    • memeriksa aksioma apa yang diasumsikan
    • memeriksa apakah kesimpulan terakhir adalah kalimat yang diinginkan
  • Jika dari aksioma tertentu ada bukti untuk suatu kalimat tertentu, maka ada pula suatu bilangan asli PA tertentu yang merepresentasikan bukti itu
  • Karena PA dapat merepresentasikan komputasi yang memeriksa apakah bilangan itu benar-benar kode bukti, maka “bukti di dalam PA” itu sendiri dapat diperlakukan di dalam PA
  • Gödel mengodekan logika di dalam PA tanpa harus mengodekan seluruh komputasi, tetapi dari sudut pandang programmer, memahami ini lewat pengodean komputasi merupakan jalur yang alami

Bacaan terkait

1 komentar

 
GN⁺ 2025-06-15
Komentar Hacker News

  • Ini adalah tulisan yang memperluas sebuah pertanyaan Stack Overflow menjadi artikel blog
    Membahas batas-batas yang bisa dibuktikan dengan aksioma Peano, dan bagaimana mulai melakukan bootstrap Lisp di dalamnya
    Semua lelucon buruk ada di bagian kedua, dan koreksi maupun pertanyaan lanjutan dipersilakan

    • Setelah membaca seluruh tulisannya, saya melihat ada satu bagian pada contoh (defun not (x) ...) di bagian "Why Lisp?" yang pasangan tanda kurungnya tidak cocok
      Ini cukup lucu jika dikaitkan dengan bagian berikutnya yang menulis “membuat komputer menemukan tanda kurung yang seimbang itu sangat mudah”, dan komentar di bagian "Basic Number Theory" tentang “tumpukan tanda kurung penutup menjadi tidak terlihat” juga menghibur
      Walau sudah lama tidak memakai Lisp, tulisannya bagus karena saya masih bisa mengikutinya lagi dan menangkap intinya
    • Saya belum banyak membaca setelah bagian pengantar, tetapi premis bahwa setiap kasus konkret barisan Goodstein berakhir di 0 dapat dibuktikan di dalam PA, sedangkan proposisi bahwa semua barisan berakhir tidak dapat dibuktikan, terasa menarik
      Fakta bahwa komputasi bisa dikodekan hanya dengan aksioma Peano juga terasa aneh sekaligus menakjubkan, seperti ada satu lapisan referensi-diri tambahan
      Belakangan saya mulai mempelajari teori himpunan lebih jauh hingga sampai pada barisan Goodstein, dan saya penasaran dengan rekomendasi buku teks teori himpunan tingkat lanjut tahap berikutnya atau buku yang membahas aritmetika Peano secara mendalam
    • Lisp sektor boot juga melakukan bootstrap dirinya sendiri: https://justine.lol/sectorlisp2/
      Berbagai Lisp di https://t3x.org juga mengimplementasikan angka dan sisanya dengan sel cons serta apply/eval
      Evaluator metasirkular John McCarthy adalah kode yang disebut Alan Kay sebagai “persamaan Maxwell untuk perangkat lunak”, dan di SectorLISP diimplementasikan dalam bentuk seperti ASSOC EVAL EVCON APPLY EVLIS PAIRLIS
      Sebagian Forth juga mirip, dan Zenlisp dari T3X menjelaskannya dengan berpusat pada cara eval/apply saling memanggil secara rekursif: http://t3x.org/zsp/index.html
    • Ada dua tempat yang menulis “omega”, sepertinya sebaiknya ditulis \omega

  • Sebagai orang yang pernah mengerjakan matematika maupun pemrograman, yang lebih menarik daripada pengodean komputasi itu sendiri adalah bahwa independensi teorema Goodstein bisa diputar lewat cara referensi-diri seperti ini
    Sepertinya PA + “PA bersifat ω-konsisten” dapat membuktikan teorema Goodstein, dan mungkin induksi transfinit hingga ε₀ juga dapat dilakukan secara umum
    Sunting: saya bertanya-tanya apakah PA + “PA konsisten” saja sudah cukup

    • Dari posisi sebagai penulis pertanyaan SO asli, saya menambahkan beberapa tautan jawaban terkait ke pertanyaan tersebut
      Intinya, “PA konsisten” saja tidak cukup; yang cukup adalah prinsip refleksi seragam bahwa “jika PA membuktikan sesuatu, maka itu benar”
      Saya tidak 100% yakin apakah prinsip ini ekuivalen dengan ω-konsistensi, tetapi dari bagian berikut ini tampaknya bisa dibaca begitu: https://en.wikipedia.org/wiki/%CE%A9-consistent_theory#Relation_to_other_consistency_principles
      Wikipedia menjelaskan bahwa T bersifat ω-konsisten sebagai “T + RFN_T + himpunan semua kalimat benar bersifat konsisten”, yang tampaknya berarti sama dengan “T + RFN_T benar”
    • Saya suka struktur rekursif ini
      Pada dasarnya kita membuat bukti-meta tentang apa yang dibuktikan PA, dan jika kita memercayai PA, kita juga akan memercayai bukti-meta itu
      Namun saya kurang paham bagaimana PA + “PA konsisten” bisa cukup
      Sistem itu tampaknya mengizinkan model di mana teorema Goodstein benar pada bilangan asli standar, tetapi salah pada suatu bilangan bulat nonstandar N, dan tampaknya justru kasus itulah yang dikecualikan oleh ω-konsistensi yang lebih kuat
    • Sayangnya tampaknya tidak demikian, dan dengan rumus universal murni saja hal lain pun tidak bisa dilakukan
      Jadi ini bukan masalah khusus Con(PA), melainkan fenomena yang lebih umum: https://math.stackexchange.com/questions/5003237/can-goodsteins-theorem-be-proven-in-mathrmpa-conpa
      Terkait pertanyaan pertama, saya penasaran bagaimana ω-konsistensi dikodekan sebagai rumus PA
    • Tulisan Math Exchange mengatakan bahwa PA + induksi transfinit untuk ε₀ membuktikan konsistensi PA
      Karena itu, tampaknya PA + “PA konsisten” mungkin bisa membuktikan induksi transfinit untuk ε₀
    • Pada titik ini, detailnya sudah sedikit di luar wilayah yang bisa saya bicarakan dengan percaya diri
      ChatGPT mengatakan bahwa PA + “PA konsisten” saja tidak cukup, dan karena mestinya ia sudah mencerna cukup banyak buku teks logika, sepertinya klaim itu boleh dipercaya

  • Saat pertama kali memakai aritmetika Peano, saya cukup terkejut dengan daya ungkapnya
    Awalnya terlihat seperti sistem dasar, tetapi setelah menyadari bahwa komputasi itu sendiri bisa dikodekan di dalam PA dan berbagai jenis komputasi dapat disimulasikan, hal-hal yang tampak rumit mulai saling tersambung
    Saya penasaran dengan rekomendasi materi yang menjelaskan teknik pengodean semacam ini dengan ramah untuk pemula

  • Ini sangat mirip dengan teori Boyer-Moore. Teori ini juga membangun matematika dari tingkat aksioma Peano.
    Boyer dan Moore juga membuat pembukti teorema otomatis yang disesuaikan untuk teori ini, dan salinan yang berjalan di GNU Common Lisp tersedia di https://github.com/John-Nagle/nqthm/tree/master
    Menurut penjelasan mereka, cara mudah memahaminya adalah menganggap program seperti mahasiswa matematika yang cukup baik. Jika hanya diberi aksioma Peano, sulit berharap ia membuktikan atau menemukan teorema faktorisasi prima, tetapi jika bersama aksioma Peano juga diberi daftar teorema seperti “buktikan hukum komutatif penjumlahan”, “buktikan bahwa perkalian distributif terhadap penjumlahan”, “buktikan bahwa hasil fungsi GCD membagi kedua argumennya”, maka ia dapat menanganinya dengan baik.
    Makalah: https://www.cs.utexas.edu/~boyer/acl.pdf

  • Komentar yang ditujukan kepada JoJoModding di Math StackExchange itu keliru.
    Penjelasan bahwa “PA bisa membuktikan bahwa ia membuat sebuah bukti, tetapi mungkin tidak bisa membuktikan bahwa bukti itu berdurasi/berpanjang hingga” salah menangkap inti masalah.
    Jika PA membuktikan “PA membuktikan X”, maka PA dapat membuktikan X.
    Poin pentingnya bukan bahwa ada model nonstandar, melainkan bahwa model bilangan asli standar adalah model PA.
    Jadi jika PA membuktikan “PA membuktikan X”, maka memang ada bilangan asli hingga yang standar yang sesuai dengan bukti terenkode dari “PA membuktikan X”, dan dengan bilangan asli itu kita dapat menyusun bukti X di dalam PA.

    • Versi bahasa alami yang diajukan bersifat ambigu, jadi pembedaan ini penting.
      Yang ditunjukkan bukanlah “PA membuktikan Provable(forall n, G(n))”, melainkan “PA membuktikan forall n, Provable(G(n))”.
      Untuk yang pertama, memang akan mengikuti bahwa “PA membuktikan forall n, G(n)”, tetapi yang kedua berbeda.
      Tanpa merujuk pada barisan Goodstein, saya ingin melihat argumen bahwa untuk proposisi umum P, dari membuktikan forall n, Provable(P(n)) tidak berarti bisa membuktikan Provable(forall n, P(n)).
    • Pernyataan “jika PA membuktikan ‘PA membuktikan X’, maka PA membuktikan X” tidak benar.
      Di dalam PA, kita dapat membangun fungsi yang mencari semua bukti yang dapat dibuat PA, dan berdasarkan itu membuat fungsi will-return yang menganalisis apakah suatu fungsi dan input akan mengembalikan hasil.
      Ini mirip dengan upaya memecahkan masalah halting, sehingga tidak selalu bekerja, tetapi dalam banyak kasus bekerja.
      Jika di sini kita membuat opposite-return, ia dapat dikonstruksi agar mencoba mengembalikan hasil ketika fungsi dan input yang diberikan tidak mengembalikan hasil, dan agar tidak mengembalikan hasil ketika ia mengembalikan hasil.
      Dengan cara yang sama seperti pembuktian standar masalah halting, jika mempertimbangkan (opposite-return opposite-return opposite-return), PA dapat membuktikan “jika PA dapat membuktikan bahwa opposite-return mengembalikan hasil, maka sebenarnya ia tidak mengembalikan hasil”, “jika PA dapat membuktikan bahwa ia tidak mengembalikan hasil, maka sebenarnya ia mengembalikan hasil”, “jika PA benar-benar dapat membuktikan semua hal yang ia buktikan bahwa ia buktikan, maka ia harus memiliki bukti salah satu dari dua proposisi sebelumnya”, “maka dalam kasus seperti itu PA tidak konsisten”.
      Ini adalah salah satu bentuk teorema ketaklengkapan kedua Gödel, sehingga “PA membuktikan” dan “PA membuktikan bahwa dirinya membuktikan” harus dibedakan.
    • Bahwa model standar adalah model PA hanya berlaku jika PA konsisten, dan PA tidak dapat membuktikan bahwa dirinya konsisten. Selama tidak inkonsisten, ini mustahil karena teorema Gödel.
      Jadi pembuktian yang diusulkan tidak bekerja di dalam PA, dan inti komentar itu tampaknya justru ada di bagian tersebut.

  • https://math.stackexchange.com/questions/4408124/what-does-the-kirby-paris-theorem-mean

  • Saat berbicara dengan seseorang tentang tipe data induktif, saya menunjukkan definisi zero/succ seperti Nat di Lean atau Rocq.
    Orang itu bertanya, “Apakah hanya itu? Bagaimana dengan aksioma Peano? Apakah ada sesuatu yang lebih primitif daripada tipe data induktif?”, dan itu menarik.
    Ini mengingatkan bahwa lebih baik memandang aksioma Peano sebagai salah satu dari beberapa desain, bukan sesuatu yang otomatis sudah inheren.

    • Saya memandang bilangan asli sebagai lebih primitif daripada tipe data induktif.
      Sebab semua tipe data induktif dapat dibangun menggunakan bilangan asli bersama pembentuk tipe primitif dari bilangan prima, misalnya Π, Σ, =, Ω, dan sebagainya.

  • Kalkulus lambda murni saja sudah cukup. Sebab kalkulus lambda mengodekan komputasi.

  • Terkait konsistensi PA, hal ini dapat dibuktikan di dalam PA: https://youtu.be/6pjLmmkZnIA

    • Untuk orang yang bukan logikawan, konteksnya sangat diperlukan.
      Teorema ketaklengkapan kedua Gödel menunjukkan bahwa jika PA dapat membuktikan konsistensinya sendiri, maka PA tidak konsisten, sehingga dapat membuktikan apa saja, termasuk yang salah.
      Karya yang ditautkan bukan menunjukkan inkonsistensi PA, melainkan mendefinisikan makna baru yang lebih lemah dari pernyataan bahwa PA “membuktikan konsistensinya sendiri”, lalu menunjukkan bahwa PA dapat melakukan hal yang lebih lemah itu.
      Ini karya yang menarik, tetapi maknanya baru terasa jika sudah cukup banyak mengetahui logika.

  • Tulisan ini mendapat 123 poin, sementara tulisan SO yang ditautkan hanya punya 11 upvote.

    • Stack Overflow mensyaratkan reputasi 15 poin untuk bisa memberi upvote.
      Dengan ditambah reputasi bahwa tulisan yang diposting di sana mudah dihapus dan batas 15 poin itu, tampaknya banyak orang tidak bisa memberi upvote.