Edward Nelson, eksiklik teoremlerini kabul etti mi?
Edward Nelson, üslenmenin bütünlüğünü kanıtlayamayan zayıf aritmetiğin (öngörülü aritmetik olarak adlandırılır) versiyonlarını savundu. Onun teorisi Robinson aritmetiğini genişlettiğinden, eksiklik teoremleri ona uygulanır. Ancak eksiklik teoremleri, kabul ettiğinden daha güçlü teorilerde kanıtlanırsa, muhtemelen onları reddedebilir. Öyleyse sorularım ilk önce, Nelson eksiklik teoremlerinden herhangi birinden şüphe etti mi? İkincisi, eksiklik teoremleri, üslenmenin bütünlüğünü kanıtlamayan zayıf aritmetik sistemlerinde kanıtlanabilir mi?
Bir cevaba en yakın bulabildiğim şey, 81. sayfada "sonlu matematiksel mantığın bu iki sütunundan en az biri olan Hilbert-Ackermann Tutarlılık Teoremi ve Gödel'in İkinci Teoremi," yazdığı Predicative Aritmetik kitabından bir alıntıdır. impredicative kavramlara bir çağrı. "
Yanıtlar
Gödel'in ikinci eksiklik teoremi ne üs alma ne de “impredikatif kavramlar” gerektirir. Nelson'ın çalıştığı sistemler, tanımlanabilir kesintiler üzerinde yorumlanabilen aritmetik parçalarıdır.$Q$; böyle bir parça sınırlı aritmetiktir$I\Delta_0+\Omega_1$ (bu Nelson'ın dediği gibi görünüyor $Q_4$içinde yüklemlik aritmetik kitabı). Teori$I\Delta_0+\Omega_1$ (ve hatta daha kısıtlı indüksiyona sahip zayıf parçaları, örneğin $PV_1$) ikinci eksiklik teoremini mükemmel bir şekilde ispatlayabilir (gerçek bir kısıtlama olmayan polinom zamanlı aksiyomlar kümesine sahip teoriler için).
( DÜZENLEME: Bu cevabı Emil Jeřábek'ten öğrendiklerimin ışığında ve ilgili referansların bazılarını daha dikkatli okuyarak büyük ölçüde yeniden yazdım.)
Emil Jeřábek'in dediği gibi, ikinci sorunuzun kısa cevabı evet, ancak dikkat edilmesi gereken bazı uyarılar var.
Her şeyden önce, o bile ne kadar belki hemen açık değildir devlet dursun, böyle zayıf bir sistemde Gödel'in eksiklik teoremleri olağan ifadeleri hesaplanabilir aksiyomların setleri üzerinde ölçmek beri onları kanıtlamak. Aksiyomun ancak aşırı derecede pahalı bir hesaplamayla karar verilebildiği bir dizi aksiyomdan çok zayıf bir sistemde anlamlı bir şekilde bahsetmek zor olacaktır. Matematiğin temellerinde pratik açıdan ilgi çekici olan tüm aksiyom dizilerini içerdiği için, dikkati aksiyomların “evcilleştirilmesi” dizileriyle sınırlandırarak bu sorundan kaçabiliriz. Bu kısıtlamayla bile, aksiyom kümeleri üzerinden nicelleştirmede teknik bir zorluk vardır, ancak eksiklik teoremi şemasından bahsederek de bunu bir kenara bırakabiliriz ; yani, her bir ilgili aksiyom seti için, aksiyomluğu ifade etmek için bir (sınırlı) aritmetik formülü yazıyoruz ve bu tür her formül için ayrı bir eksiklik teoremi şemasına sahibiz.
İkinci bir zorluk, çok zayıf sistemler için, eksiklik teoremlerinin, onların ne anlama gelmelerini istediğimizi ifade edip etmediği sorusunun ortaya çıkmasıdır. Örneğin, Bezboruah ve Shepherdson ispat için Gödel'in ikinci teoremi Q , Q, Robinson aritmetik. Ancak Q o kadar zayıftır ki sözdiziminin temel özelliklerini düzgün bir şekilde resmileştiremez, bu nedenle Q'nun Con ( Q ) 'yu kanıtlamaması tartışmalı bir şekilde pek bir şey ifade etmez.
Bununla birlikte, olumlu tarafta, sözdiziminin aritmetizasyonu için üs alma gerekli değildir. Örneğin, Ph.D. Tez Sınırlı Aritmetik , Samuel Buss sözdiziminin aritmetizasyonunu, adı verilen zayıf bir sistem kullanarak ayrıntılı olarak gerçekleştirdi.$S^1_2$ve Gödel'in ikinci eksiklik teoreminin bir versiyonunu kanıtladı. $S^1_2$. (Nitekim, Nelson'ın kitabı, kendi “öngörücü aritmetik” sistemini kullanarak temel sözdizimini nasıl aritmetize edeceğini göstermektedir.)
Poz gibi sadece eksiklik teoremleri olmadığını bilmek istedim çünkü Buss kanıtı hala oldukça, sorunuza cevap vermez tutun zayıf sistemler için; Eksiklik teoremlerinin ispatlarının üs almanın toplam bir fonksiyon olduğunu kanıtlamayan bir sistemde resmileştirilip biçimlendirilemeyeceğini sordunuz. Bu nokta bir süre kafamı karıştırdı çünkü Buss'un ispatı aslında Gentzen'in sınırlandırılmış aritmetikte ispatlanamayan kesme-eleme teoremine hitap ediyor. Bununla birlikte, Emil Jeřábek'in işaret ettiği gibi, bunun nedeni Buss'un ikinci eksiklik teoreminin normalden biraz daha güçlü bir versiyonunu kanıtlamasıdır. Olağan eksiklik teoremini ele alırsak, o zaman bir uzman ispatın sınırlı aritmetiğin yeteneklerini aşmadığını "inceleyerek" görebilir.
Hala literatürde, eksiklik teoremlerinin sınırlı aritmetikte ispatlanabilir olduğuna dair açık bir ifade görmedim; bu "folklor" gibi görünüyor. Sınırlı ters matematik denen bir alandaki bir sonuçtur . Sınırlı ters matematik programını açıkça takip eden bir kitap, Stephen Cook ve Phuong Nguyen tarafından yazılan Mantıksal Kanıt Karmaşıklığının Mantıksal Temelleri'dir , ancak bunlar eksiklik teoremlerini kanıtlamazlar. Zayıf sistemler için eksiklik teoremlerini tartışan bir başka kitap da Pavel Pudlák ve Petr Hájek'in Birinci Derece Aritmetiğin Metamatematik'i, ancak orada da açık bir ifade bulamadım.
( DÜZENLEME: Foundations of Mathematics posta listesinde yayınlanmış bir referans istedim ve Richard Heck beni AJ Wilkie ve JB Paris, Ann. Pure Appl. Logic 35 (1987) tarafından sınırlandırılmış aritmetik formüller için indüksiyon şemasına işaret etti . 261–302. Bu makale, eksiklik teoremlerinin sistem temelinde kanıtlanabileceğine dair oldukça ayrıntılı bir kanıt sunmaktadır.$I\Delta_0 + \Omega_1$ sınırlı aritmetik için.)
Şimdi ilk sorunuzla ilgili bazı yorumlar için. Nelson hala hayattayken bile tam olarak neye inandığını tespit etmenin her zaman kolay olmadığını kabul etmek önemlidir. Zayıf bir aritmetik sistemi bile keyfi olarak büyük sayıları kabul eder, ancak Nelson aslında tekli olarak yazılamayacak sayılardan şüphelendiğini gösteren şeyler söyledi. Tahmin Edici Aritmetik adlı kitabında sayı hakkındaki bir yorumu takiben$80^{5000}$, Bir keresinde Nelson sorulan sayısı hakkında$80\cdot 80 \cdots 80$ açıkça yazdığımız yer $5000$ Kopyaları $80$. Üs alma söz konusu olmamasına rağmen, bunun gerçek bir sayı olduğundan şüpheliydi. Bu şartlar altında Nelson'ın buna inanıp inanmadığından bile emin değilim.$\sqrt{2}$sen ve benim buna inandığımız gibi mantıksız. Eğer Nelson ve ben ispatın üzerinden birlikte geçersek, o zaman elbette ispatın her adımının resmen doğru olduğu konusunda hemfikir olur, ama ispatın sonucu ne “söyler”? Sen ve ben, keyfi olarak büyük doğal sayılar hakkında bir şeyler söylediğini düşünüyoruz, ancak Nelson olmayabilir. Ve eğer yapmadıysa, neden kısa bir biçimsel manipülasyon dizisinin doğruluğunun bize bir bilgisayarın pozitif tamsayılar arayıp aramadığına dair (örneğin) bir şey söylemesi gerektiğine bile inansın.$a$ ve $b$ öyle ki $a^2 = 2b^2$başarılı mı yoksa başarısız mı? Kısacası, Nelson'ın şahsen neye inandığını veya şüphe duyduğunu tam olarak anlamaya çalışmanın özellikle verimli olacağını düşünmüyorum, çünkü o, bu inançlar hakkında yeterince ayrıntılı ve tutarlı bir açıklama yapmadı.
Fernando Ferreira ve Gilda Ferreira tarafından yazılan Robinson's Q'da Yorumlanabilirlik adlı makalede, Nelson'ın “öngörücülüğü” hakkında ilginç bir tartışma var . Nelson'ın Tahmine Dayalı Aritmetik'te tartıştığı şey, matematiksel bir ifadeyi , Q'da yorumlanmadığı sürece anlamlı olarak görmememiz gerektiğiydi . Ferreira ve Ferreira, üs alma toplamının Q'da yorumlanamayacağının (Wilkie tarafından) gösterildiğine işaret ederken, üs alma toplamının olumsuzlanması Q'da yorumlanabilir (ikincisi Solovay'ın bir sonucudur). Bu, Nelson'un üslüp kazanmanın kararlı tahminci için "aşılmaz bir engel" teşkil ettiği görüşünü doğruluyor gibi görünüyor. Öte yandan, Ferreira ve Ferreira da, Nelson'un görüşünün belirli bir “istikrarsızlıktan” muzdarip olduğu, çünkü örneğin kavuşum alma altında kapalı olmadığı iddialarını ortaya koyuyor. Daha ayrıntılı bir tartışma için okuyucuyu makalelerine yönlendiriyorum. Her durumda, Nelson'ın eksiklik teoremlerini kabul etmesi için gerekli bir koşul, bunların Q'da yorumlanabilir olmaları olabilir . Bunun doğru olduğunu tahmin ediyorum, ancak yine açık bir referans bilmiyorum.
İkinci sorunuz Emil Jerabek tarafından doğru bir şekilde yanıtlandı diyebilirim. Bazı yorumları okurken, ilk sorunuzla ilgili olarak şunları yazmam gerektiğini düşünüyorum:
Ed Nelson'la ve onu iyi tanıyan insanlarla konuştuğumdan, Ed Nelson'ın uzun süredir üstel işlevin bir şekilde tutarsızlığa yol açtığına kesin olarak ikna olduğunu söyleyebilirim (ve bu nedenle PA tutarsızdır). Bu konu hakkında uzun uzadıya yazılar yazdı ve bu görüş için Bellantoni-Cook'un işlev karmaşıklığının karakterizasyonu ve öngörülebilirlik üzerine yazıları gibi bazı motivasyonlara işaret etti.
Ed Nelson'ın görüşüne yönelik daha derin motivasyonu şöyleydi: bir şekilde sabit nokta yapılarının (tüm kısmi özyinelemeli fonksiyonların bir listesi veya Goedel'in eksiklik teoremlerinin bir listesi gibi) 'içselleştirilebileceği' veya 'bütünleştirilebileceği' hissine sahipti. '0 = 1' gibi çelişki. Böyle bir çelişki ancak üstel fonksiyon göz önüne alındığında mümkün olabilirdi. En temel düzeyde, Ed Nelson, tamamlanmış sonsuz küme kavramının biçimsel olarak tutarlı olduğuna inanmıyordu.