Peano aritmetiği yeterlidir, çünkü Peano aritmetiği hesaplamayı kodlayabilir

• Peano aritmetiği (PA), mekanik hesaplama sürecini ifade edebildiği için, her bir tekil Goodstein dizisinin sonlanması PA içinde ispatlanabilir
• Cantor standart formu ve kalıtsal ordinal gösterimi aracılığıyla Goodstein dizileri ve bunların azalanlığı ifade edilir; bu sayede sonlu uzunlukta ispat inşası mümkündür
• Tümevarım (güçlü tümevarım/aşkın tümevarım) yoluyla ispatlar belirli ordinal derecelerine kadar ayrı ayrı genişletilebilir
• PA, her doğal sayı n için “G(n) 0'a ulaşır” önermesini ispatlayabilir; ancak Goodstein teoreminin tamamına ilişkin (tüm n'ler için) bütünsel bir ispat mümkün değildir
• PA ile hesaplama, veri yapıları (List, Pair vb.), hatta programlama dilinin kendisinin (Lisp) kodlanması ve kendi ispat sürecinin kodlanması dahi yeterince gerçekleştirilebilir

---

Giriş ve problem arka planı

• Bu yazı, Peano aritmetiğinin (PA) Goodstein dizilerinin “her n için 0'a ulaştığını (G(n) terminates)” ispatlayabildiğini anlatır
• Bu, mantıkçılar için apaçık görünebilir; ancak programcıların anlayabilmesi için hesaplama kodlaması perspektifinden açıklanır
• Goodstein dizilerinin her bir durumu için PA içinde somut ispat rutinleri kurulabilir

Ordinals (sıra sayıları) ve Goodstein dizileri

• Von Neumann yöntemiyle sıra sayıları (Sets as Ordinals) üretilir
  • 0 boş kümedir, 1 = {0}, 2 = {0,1}, ω = {0,1,2,…}, ω+1 = {0,1,2,…,ω} vb.; böylece sıralama iyi tanımlıdır
• Goodstein dizileri, Cantor standart formunu kullanan kalıtsal taban gösterimi ile tanımlanır
  • Örnek: ω^ω, ((1,ω)) yani ((1,(1,1)))
  • < sırası, her terimin ordinali/katsayısı için leksikografik karşılaştırmayla belirlenir

Tümevarım ve aşkın tümevarım (Transfinite Induction)

• Peano aritmetiğinde tümevarım: 0 için doğruysa ve n→n+1 için doğruysa tüm doğal sayılar için doğrudur
• Güçlü tümevarım da PA ile ispatlanabilir
• Aşkın tümevarım (Transfinite induction): ZFC vb. sistemlerde sonsuz ordinallere kadar genişletilebilir ve Cantor standart formunda yazılan sayılara uygulanabilir
  • Theorem 1: Cantor standart formundaki azalan diziler her zaman sonludur
  • Theorem 2: Cantor standart formundaki sayılar için aşkın tümevarım kullanılabilir

PA'da aşkın tümevarım ve Goodstein dizisi ispat uzunluğu

• PA, herhangi bir n için Goodstein dizisinin sonlanış ispatını üretebilir
  • Cantor standart formundaki kule yüksekliği m=O(log* n) (iterated log) olduğunda buna göre ispat kurulabilir
  • Her aşamada m adet ispatın birleştirilmesiyle toplam ispat uzunluğu O(m^2) olur; ya da özel bir gösterim (ω[m]) kullanılırsa O(m log m)'ye indirilebilir
• Ancak Goodstein teoreminin tamamının (tüm n'ler için) ispatı PA içinde mümkün değildir (ε0 için aşkın tümevarım yapılamaz)
  • Eğer mümkün olsaydı PA'nın tutarlılığı da ispatlanabilirdi ve bu da Gödel'in ikinci eksiklik teoremiyle çelişirdi

PA'nın program, veri yapısı kodlaması

• PA, hesaplamayı/programları/veri yapılarını (sayılar, çiftler, listeler ve diğer tüm yapılar) yeterince kodlayabilir
• Şu tür işlevler çeşitli yollarla gerçekleştirilebilir:
  • temel mantık ve işlemler (+, *, pow, //, %, min, max vb.)
  • desen eşleme ve koşullu dallanma (if, cond vb.)
  • bir sayıyı iki sayıyla (çift) kodlamak ya da çiftten tekrar liste gibi daha karmaşık yapılara genişlemek (özyinelemeli listeler, ağaçlar, metin vb.)
• Bu veri yapısı kodlamalarıyla keyfi bir sanal makine/programlama dili (Lisp vb.) yorumlayıcısı bile kurulabilir

Lisp'e bootstrap ve kodlama

• Lisp örneği üzerinden temel sayısal ve mantıksal işlemlerin, veri yapılarının, programlama dili yorumlayıcısının/interpreter'ının nasıl gerçekleştirilebileceği açıklanır
• Lisp'in yapısı (komut/argüman eşlemesi, special form, macro vb.) bütünüyle PA içinde uygun fonksiyon bileşimleriyle gerçekleştirilebilir
• Daha da ileri gidilerek PA içinde PA'nın kendi ispat süreci, mantıksal ispat prosedürleri, kendine gönderimli yapılar da bütünüyle simgesel olarak kodlanıp uygulanabilir

PA içinde mantığın kendisinin kodlanması

• Matematiksel mantıktaki First-Order Logic ispat süreci, PA sayılarının verisi olarak kodlanabilir
• Her ispat adımı/önerme/çıkarım kuralı/geçerli ispat denetimi, bir dizi sayısal fonksiyon/liste işlemi olarak tanınıp işlenebilir
• Bu tür üst-düzey ve kendine gönderimli kodlamalar, Gödel'in eksiklik teoremleri ve Halting problemi ispatlarına kadar uzanır

Sonuç

• Hesaplama, veri yapıları, programlar ve mantıksal ispat süreçleri bile PA içinde yeterince kodlanabilir, ispatlanabilir ve yorumlanabilir
• Dolayısıyla herhangi bir Goodstein dizisinin (n için G(n)'in sonlanması) PA içinde somut olarak ispatlanması mümkündür
• Ancak Goodstein teoreminin tamamı için (tüm n'ler adına) "PA, PA içinde Goodstein teoremini ispatlar" biçiminde bir ispat, mantığın sınırları nedeniyle mümkün değildir
• Programcı bakış açısından PA, hesaplamanın kendisini kodlayabilen tam bir mantıksal temeldir

[GN⁺]

Hacker News görüşü

• Bu yazı, Stack Overflow'da sorduğum bir soruyu blog gönderisine dönüştürmüş halim; Peano aksiyom sistemiyle ispatlanabileceklerin sınırlarını ve Peano aksiyom sistemi içinde Lisp'in nasıl bootstrap edileceğini açıklıyor. Şakaların çoğu ikinci bölümde. Düzeltme ya da ek sorular da memnuniyetle karşılanır.
  • Bu yazıyı okurken "Why Lisp?" bölümünde parantezlerin eşleşmediği bir yer fark ettim ((defun not (x) (if x false true) örneğine bakın). Biri parantez kullanmaya başladığında içgüdüsel olarak düzgün kapanıp kapanmadığını kontrol ediyorum. Sonrasında "parantezlerin dengeli olup olmadığını bilgisayarla programlamak kolaydır" denmesi beni çok güldürdü. Bu tür şakalar gerçekten hoştu; ayrıca "Basic Number Theory" bölümündeki ; After a while, you stop noticing that stack of closing parens. yorumu da akılda kaldı. Uzun zaman sonra yeniden Lisp görmek keyifliydi ve yazı gerçekten eğlenceliydi.
  • Bu yazı gerçekten çok ilginç. Daha giriş kısmındayım ama Peano aksiyomatiği (PA) içinde Goodstein dizilerinin her bir özel durumunun 0'a ulaştığı ispatlanabiliyorken, "tüm" durumların 0'a ulaştığı ispatlanamıyor olması ilginç. (Aslında beklenen bir sonuç olsa da yine de heyecan verici.) Ve yalnızca Peano aksiyomatiğiyle hesaplamanın kodlanabiliyor olması gerçekten tuhaf. Teoride bakınca doğal geliyor ama daha önce bir kat daha öz-gönderimi düşünmemiştim. Tam da yakın zamanda kümeler kuramını biraz daha öğrenmek için Intro to Set Theory kitabında Goodstein dizilerine kadar gelmiştim. Önerebileceğiniz ileri seviye bir kümeler kuramı kitabı ya da Peano aritmetiğine derinlemesine giren bir kaynak varsa duymak isterim. Goodstein teoreminin ispatı için PA'nın neden yetersiz olduğunu anlamak küçük bir hedefim, ama bunun yerine önerebileceğiniz başka yollar da olur.
  • Yazıda omega'nın iki yerde \omega olarak yazılması unutulmuş.
• Boyer-Moore teorisine çok benziyor. Bu teori, matematiği Peano aksiyomları düzeyinde inşa ediyor. Boyer ve Moore, bu teoriyi uygulayan bir otomatik teorem ispatlayıcısı geliştirdi ve GNU Common LISP üzerinde çalışan bir kopyası da var. "A Computational Logic" makalesi ile nqthm uygulaması da bakmaya değer. Makaledeki örneklerden biri olarak, Peano aksiyomlarıyla başlandığında asal sayıların çarpımı gibi karmaşık teoremler zorlayıcı olsa da, toplamın değişme özelliği, çarpmanın dağılım özelliği ve GCD fonksiyonuyla ilgili teoremler gibi şeylerin rahatlıkla ispatlanabildiği etkileyiciydi.
• Hem matematik hem programlama geçmişim var; kişisel olarak Goodstein teoreminin bağımsızlık kısmında, bunun öz-gönderim üzerinden dolaylı biçimde aşılabiliyor olması daha ilginç geliyor. PA+"PA omega-consistent'tır" varsayımı eklenirse Goodstein teoremi ispatlanabilir diye düşünüyorum; hatta bunun epsilon_0'a kadar aşkın tümevarımı da mümkün kılabileceğini tahmin ediyorum. EDIT: Belki de yalnızca "PA tutarlıdır" demek bile yeterli olabilir mi?
  • Maalesef değil. Ve yalnızca Con(PA) ile değil, keyfi bir evrensel nicemlenmiş formülle de bunun yeterli olmadığı biliniyor. Şu ilgili Math StackExchange yanıtına bakın. İlk soruyla ilgili olarak, omega-tutarlılığın PA'nın bir formülü olarak nasıl kodlandığını merak ediyorum; aklıma hemen gelmedi, o yüzden ilgimi çekti.
  • Stack Overflow'daki soru sahibi benim. Sorunun altına bazı ek yanıt bağlantıları koydum. Özünde yalnızca "PA tutarlıdır" yeterli değil, ama "PA'da ispatlanıyorsa doğrudur" türünden bir "uniform reflection principle" yeterli. Bunun omega-tutarlılıkla tamamen aynı olduğundan emin değilim ama Wikipedia'daki açıklamadan öyle anlaşılıyor. T omega-tutarlıysa bunun anlamı "T + RFN_T + tüm doğru formüller kümesi tutarlıdır" oluyor ve bu da "T + RFN_T doğrudur" ile eşdeğer diye okunuyor.
  • Bu tür tümevarımsal (özyinelemeli) yapıları da seviyorum. Sonuçta PA'nın neyi ispatladığına dair bir meta-ispat kuruyorsunuz ve PA'ya güveniyorsanız bu meta-ispata da güvenebileceğinizi düşünüyorsunuz. Sadece "PA tutarlıdır"ın yeterli olduğu kısmını net biçimde anladığımdan emin değilim. Bana göre PA+"PA tutarlılığı", standart doğal sayılar üzerinde Goodstein teoreminin doğru olduğu bir modele izin verir ama aynı zamanda bazı standart olmayan tamsayılar N için Goodstein teoreminin yanlış olduğu modellere de izin veriyor gibi görünüyor. Omega-tutarlılığın daha güçlü ifadesi bu tür durumları dışlar diye düşünüyorum.
  • Math Exchange gönderisinde, PA+epsilon_0'a kadar aşkın tümevarım ispatının PA'nın kendisini ispatladığı söyleniyor. Bana göre PA+"PA tutarlılığı" varsa epsilon_0'a kadar aşkın tümevarım da ispatlanabilir olmalı.
  • Bu konu artık rahatça konuşabileceğim ayrıntı düzeyini aşıyor gibi. ChatGPT'ye göre "PA+PA tutarlılığı" tek başına yeterli değilmiş. ChatGPT mantık kitaplarını epey sindirmiştir herhalde; böyle diyorsa güvenilebilir gibi.
• Stack Overflow'da JoJoModding'e yazdığım yorum doğru değil. "Standart olmayan PA modellerinde sonsuz doğal sayılar olduğu için, PA kendi içinde bir ispat ürettiğini ispatlasa bile bunun sonlu uzunlukta olduğunu ispatlayamaz" demiştim; ama gerçekte PA, "PA X'i ispatladı"yı ispatlarsa, PA X'in kendisini de ispatlar. Önemli nokta standart olmayan modellerin varlığı değil, standart doğal sayılar modelinin PA'nın bir modeli olmasıdır. Bu yüzden "PA, X'i ispatladığını ispatlarsa" fiilen standart sonlu doğal sayılara karşılık gelen bir ispat üretmiş olur ve bu sayı kullanılarak PA içinde X için gerçek bir ispat kurulabilir.
  • Mantığı daha ayrıntılı inceleyecek vaktim yok ama doğal dil düzeyinde sanki kritik fark şurada: "PA, 'forall n, G(n)'i ispatlar" değil de "PA, 'forall n, Provable(G(n))'i ispatlar". Mantık konusunda zayıfım; biri neden forall n, Provable(P(n))'in ispatlanmasının Provable(forall n, P(n))'i ispatlamaya yetmediğini somut biçimde açıklarsa sevinirim.
  • "PA, 'PA X'i ispatlar'ı ispatlarsa, PA X'i ispatlar" önermesi doğru değil. PA içinde bütün olası ispatları tarayan bir fonksiyon yazabilirsiniz; yanıtın son kısmında da bunu kabaca anlattım. Buradan will-return, opposite-return gibi fonksiyonlar da kurulabilir ve bu, durma probleminin standart ispatıyla örtüşür. opposite-return(opposite-return, opposite-return) durumunu düşünün: PA, opposite-return'ın döndüğünü ispatlarsa aslında dönmediğini de ispatlamış olur; tersine, dönmediğini ispatlarsa döndüğünü ispatlamış olur. Eğer PA, "ispatlanabilir olan her şey gerçekten ispatlanabilir" gibi daha güçlü bir ilkeyi benimseseydi bu doğrudan Gödel'in ikinci eksiklik teoremine çarpar ve PA'nın çelişkili olduğu anlamına gelirdi. Bu yüzden sadece "PA ispatlıyor" ile "PA, ispatladığını ispatlıyor" mutlaka ayrılmalı.
• Salt lambda hesabı da yeterli; çünkü lambda hesabı zaten hesaplamayı kodlayabiliyor.
• Biriyle tümevarımsal veri tipleri hakkında konuşurken zero/succ ile kurulan Nat tanımını gösterdim (Lean ya da Rocq'ta görüldüğü gibi). Karşı taraf "Bu gerçekten yeterli mi?", "Peano aksiyomatiği gerekli mi? Tümevarımsal veri tiplerinden daha ilkel bir şey var mı?" gibi sorular sordu. Peano aksiyomatiğini özünde apaçık bir şey sanmamak, bunun sadece bir tasarım olduğunu sık sık kendime hatırlatmam gerektiğini düşündürdü.
  • "Tümevarımsal veri tiplerinden daha temel bir şey var mı?" sorusuna cevaben, doğal sayıların kendisinin tümevarımsal veri tiplerinden daha ilkel olduğunu düşünüyorum. Bütün tümevarımsal veri tipleri, doğal sayılar ve birkaç başka ilkel tip kurucusu (Π, Σ, =, Ω) varsa inşa edilebilir.
• Kirby-Paris teoremi hakkında Soru-Cevap bağlantısına bakın.
• PA tutarlılığıyla ilgili olarak, bunun PA içinde ispatlanabilir olduğunu anlatan bir video paylaşıyorum: YouTube bağlantısı
  • Mantıkçı olmayanlara özellikle açıklanması gereken kısım bu. Gödel'in ikinci eksiklik teoremine göre, eğer PA kendi tutarlılığını ispatlayabilseydi PA çelişkili olurdu (yanlışlar dahil her şeyi ispatlayabilir hale gelirdi). Bu video, PA'nın çelişkili olduğunu ispatlamıyor; bunun yerine PA'nın daha zayıf bir anlamda "kendi tutarlılığını" ispatlayabildiğini gösteriyor. Mantığın temellerini bilmiyorsanız tam olarak kavramak zor, ama yine de yeterince ilginç.
• Bu konu burada 123 puan almış ama asıl SO gönderisinde sadece 11 oy var.
  • Stack Overflow'da oy verebilmek için 15 puan gerekiyor. İnsanlar itibar sistemi yüzünden gönderi yazmak istemiyor olabilir ve 15 puan sınırı da oy vermeyi engelliyor gibi.
• Yalnızca komputasyon yeterli mi? Hesaplanabilir reel sayılar, tüm reel sayıların bir alt kümesidir.
  • "Reel sayı" adının kendisinin yanıltıcı olduğunu düşünüyorum. Reel sayılar, gerçek fiziksel oranlar olarak da yorumlanabilir. Örneğin 180.255 pound dediğinizde, bunun Jones'un gerçek vücut ağırlığıyla standart pound arasındaki gerçek fiziksel oran anlamına geldiği düşünülebilir. Bu tür oranlar da fiziksel olarak vardır; yani reel sayılar fiziksel oranlar olarak yorumlanabilir. Buna karşılık günümüzde baskın görüş, sayıları gerçeklikten bağımsız soyut kavramlar olarak görmek; bu da tipik olarak Platoncu bir yaklaşım. Ama pratikte bir şeyi sonsuz hassasiyetle ölçmek ya da ifade etmek imkânsızdır. Örneğin 50 basamaktan fazla hassasiyetle ölçüm yapmak kuantum mekaniği sınırları nedeniyle mümkün değildir. Güneş Sistemi cisimlerinin yörüngelerini hatasız ölçmek isteseniz 50 basamağın ötesinde komşu yıldızların kütle etkisini, 100 basamakta ise tüm galaksiyi modellemeniz gerekir; sonunda doğrudan ölçülemeyen fiziksel etkileri de hesaba katmanız gerekir. Bu yüzden gerçek dünyada ancak sonlu hassasiyetli matematik mümkündür. Yani ilke olarak her şey hesaplanabilir olsa da, sonsuza gidildikçe matematiksel modelin kendisi de anlamsızlaşır.
  • Gerçekten öyle mi? Aslında sayılamayanların daha fazla olduğu fikri bir yanlış anlamadan doğuyor. Benim açıklamama bakın. Sayılamayanların daha fazla olduğunu kabul ederseniz, "varlık" hakkında tartışmalı bir pozisyon almak zorunda kalırsınız. İlgili tartışma da burada. Son olarak, mantıksal çıkarımı sonuna kadar götürsek bile her şeyi bilgisayarla ifade etmek mümkün. ZFC'ye büyük kardinal aksiyomları eklense bile PA'dan başlayıp herhangi bir sonuca kadar bütün çıkarımları yürütebiliriz; bu yüzden pratikte yalnızca PA'nın yeterli olduğu kanaatindeyim. Biraz daha ikna edici bir şey isterseniz Gödel, Escher, Bach kitabını öneririm.
  • Ben biraz farklı düşünüyorum. Genel olarak reel sayılar hesaplama, simgeleştirme, kayıt altına alma gibi hiçbir biçimde tümüyle ele alınamaz; ama reel sayılar hakkında kurulan "önermeler" çoğu zaman yararlı biçimde ifade edilebilir ve hesaplanabilir. Harvey Friedman ya da bu yazının yazarı gibi, basit sistemlerden hayal edilenden çok daha karmaşık değerler üretmeye çalışan kişiler gerçekten ilginç. (Not: audiomulch sitesi açılmıyor.)
  • "Yeterli" sözcüğü belirli bir amaçla birlikte gelmedikçe bu soru tanım olarak belirsizdir. Ne için yeterli olduğu önemli.
  • "Yalnızca komputasyon yeterli mi?" sorusunun kendisinin yanlış olduğunu düşünüyorum. Elbette yeterli değil; eğer yeterli olsaydı, gerçekliği kurulmuş bir saat mekanizması gibi görmeye meyilli bazı insanların düşündüğü her şey doğru çıkardı. Gerçeklik bundan çok daha ilginç ve karmaşık.