Gentzen'in tutarlılık kanıtı - Gentzen's consistency proof

Gentzen en tutarlılık geçirmez bir sonucudur kanıtı teori içinde matematiksel mantık tarafından yayınlanan, Gerhard Gentzen o 1936 Bu gösterilerde Peano birinci dereceden aritmetik aksiyomları (yani "olduğu bir çelişki içermeyen tutarlı bir diğer bazı sürece,") İspatta kullanılan sistem de herhangi bir çelişki içermez. Bugün " sıralı ε 0'a kadar nicelik belirteçsiz sonsuz sonlu tümevarım " ek prensibiyle ilkel özyinelemeli aritmetik olarak adlandırılan bu diğer sistem, Peano aksiyomlarının sisteminden ne daha zayıf ne de daha güçlüdür. Gentzen, Peano aritmetiğinde bulunan şüpheli çıkarım modlarından kaçındığını ve bu nedenle tutarlılığının daha az tartışmalı olduğunu savundu.

Gentzen teoremi

Gentzen'in teoremi birinci dereceden aritmetik ile ilgilidir: birinci dereceden Peano aksiyomları ile aksiyom haline getirilmiş , toplama ve çarpma dahil doğal sayılar teorisi . Bu "birinci dereceden" bir teoridir: niceleyiciler doğal sayılar üzerinde uzanır, ancak doğal sayıların kümeleri veya işlevleri üzerinde değil. Teori, üs alma, faktöriyeller veya Fibonacci dizisi gibi yinelemeli olarak tanımlanmış tamsayı fonksiyonlarını tanımlayacak kadar güçlüdür .

Gentzen, birinci dereceden Peano aksiyomlarının tutarlılığının, ilkel özyinelemeli aritmetiğin temel teorisi üzerinde , ordinal ε 0'a kadar niceleyici içermeyen sonlu tümevarım ek prensibi ile kanıtlanabilir olduğunu gösterdi . İlkel özyinelemeli aritmetik, tartışmasız olan çok basitleştirilmiş bir aritmetik biçimidir. Ek ilke, gayri resmi olarak, sonlu köklü ağaçlar kümesinde iyi bir sıralama olduğu anlamına gelir . Resmi olarak, ε 0 , büyük sayılabilir sıra sayılarından çok daha küçük olan ve sayılabilir bir sıra sayısı olan ilk sıradır . Sıranın sınırı:

Sıralamaları aritmetik dilinde ifade etmek için, sıralı gösterime ihtiyaç vardır, yani ε 0'dan küçük sıra sayılarına doğal sayılar atamanın bir yolu . Bu, Cantor'un normal form teoremi tarafından sağlanan bir örnek gibi çeşitli şekillerde yapılabilir . Herhangi bir niceleyici içermeyen formül A (x) için gerekliyiz: A (a) 'nın yanlış olduğu bir ordinal a <ε 0 varsa, o zaman en azından böyle bir sıra vardır.

Gentzen, Peano aritmetiğindeki ispatlar için bir "indirgeme prosedürü" nosyonunu tanımlar. Belirli bir ispat için, böyle bir prosedür, verili olanı ağacın kökü olarak hizmet eden ve diğer ispatlar bir anlamda verilenden "daha basit" olan bir ispat ağacı üretir. Bu artan basitlik, her ispata ordinal <ε 0 eklenerek ve ağaçtan aşağı doğru hareket edildiğinde bu sıra sayılarının her adımda küçüldüğünü göstererek resmileştirilir . Daha sonra, bir çelişkinin kanıtı varsa, indirgeme prosedürünün, niceleyici içermeyen bir formüle karşılık gelen ispatlar üzerinde ilkel özyinelemeli bir işlemle üretilen, ε 0'dan küçük sonsuz bir azalan sıra dizisi ile sonuçlanacağını gösterir .

Gentzen'in ispatını oyun-kuramsal terimlerle yorumlamak mümkündür ( Tait 2005 ).

Hilbert programı ve Gödel'in teoremi ile ilişkisi

Gentzen'in kanıtı, Gödel'in ikinci eksiklik teoreminin sıkça gözden kaçan bir yönünü vurguluyor . Bazen bir teorinin tutarlılığının ancak daha güçlü bir teoride kanıtlanabileceği iddia edilir. Gentzen'in ilkel özyinelemeli aritmetiğe nicelik belirteçsiz sonlu tümevarım ekleyerek elde edilen teorisi, birinci dereceden Peano aritmetiğinin (PA) tutarlılığını kanıtlar ancak PA içermez. Örneğin, tüm formüller için sıradan matematiksel tümevarımı kanıtlamaz, oysa PA bunu yapar (çünkü tüm tümevarım örnekleri PA'nın aksiyomlarıdır). Gentzen'in teorisi, PA'nın yapamadığı sayı-teorik bir gerçeği - PA'nın tutarlılığını - kanıtlayabildiğinden, PA'da da yer almıyor. Bu nedenle, iki teori bir anlamda karşılaştırılamaz .

Bununla birlikte, teorilerin gücünü karşılaştırmanın başka, daha güçlü yolları da var, bunlardan en önemlisi yorumlanabilirlik kavramı ile tanımlanıyor . Gösterilebilir ki, eğer bir T teorisi başka bir B'de yorumlanabilirse, o zaman B ise T tutarlıdır. (Aslında, bu yorumlanabilirlik kavramının büyük bir noktasıdır.) Ve T'nin aşırı derecede zayıf olmadığını varsayarsak, T'nin kendisi bu koşullu olduğunu kanıtlayabilir: Eğer B tutarlıysa, T de öyledir. Dolayısıyla, T olamaz. İkinci eksiklik teoremi ile B'nin tutarlı olduğunu kanıtlayın, oysa B, T'nin tutarlı olduğunu kanıtlayabilir. Teorileri karşılaştırmak için yorumlanabilirliği kullanma fikrini motive eden şey budur, yani eğer B, T'yi yorumlarsa, o zaman B'nin en azından T kadar güçlü ('tutarlılık gücü' anlamında) olduğu düşüncesi.

Solomon Feferman'ın önceki çalışmalarına dayanan Pavel Pudlák tarafından kanıtlanan ikinci eksiklik teoreminin güçlü bir biçimi , Robinson aritmetiği Q içeren hiçbir tutarlı teori T'nin Q artı Con (T) 'yi yorumlayamayacağını belirtir. tutarlıdır. Buna karşılık, Q + Con (T) , T'yi aritmetize edilmiş tamlık teoreminin güçlü bir formu ile yorumlar . Yani Q + Con (T) her zaman T'den daha güçlüdür (iyi bir anlamda). Ancak Gentzen'in teorisi Q + Con (PA) 'yı önemsiz bir şekilde yorumluyor, çünkü Q + Con (PA) içeriyor ve Con (PA)' yı kanıtlıyor ve bu nedenle Gentzen'in teorisi PA'yı yorumluyor. Ama, Pudlac sonucundan tarafından, Pensilvanya olamaz (sadece söylediği gibi) Gentzen teorisine beri, Gentzen teorisini yorumlamak Q + Con (PA) olarak yorumlar ve yorumlanabilir geçişlidir. Yani: PA, Gentzen'in teorisini yorumlasaydı, Q + Con (PA) 'yı da yorumlayacak ve Pudlák'ın sonucuna göre tutarsız olacaktır. Dolayısıyla, yorumlanabilirlikle karakterize edilen tutarlılık gücü anlamında, Gentzen'in teorisi Peano aritmetiğinden daha güçlüdür.

Hermann Weyl , Gödel'in 1931 eksiklik sonucunun Hilbert'in matematiğin tutarlılığını kanıtlama planı üzerindeki yıkıcı etkisinin ardından Gentzen'in tutarlılık sonucunun önemi hakkında 1946'da aşağıdaki yorumu yaptı.

Başarılı bir şekilde uygulayabilseydi, tüm matematikçiler sonunda Hilbert'in yaklaşımını kabul edeceklerdi. İlk adımlar ilham verici ve umut vericiydi. Ama sonra Gödel, henüz iyileşemediği müthiş bir darbe indirdi (1931). Gödel, Hilbert'in biçimciliğindeki sembolleri, formülleri ve formül dizilerini belirli bir şekilde sıraladı ve böylece tutarlılık iddiasını aritmetik bir önermeye dönüştürdü. Bu önermenin biçimcilik içinde ne kanıtlanabileceğini ne de çürütülemeyeceğini gösterebilirdi. Bu sadece iki anlama gelebilir: Ya tutarlılık kanıtının verildiği mantık, sistem içinde resmi karşılığı olmayan bir argüman içermelidir, yani matematiksel tümevarım prosedürünü tamamen resmileştirmeyi başaramadık; ya da kesinlikle "sonlu" bir tutarlılık kanıtı ümidinden tamamen vazgeçilmelidir. G. Gentzen nihayet aritmetiğin tutarlılığını kanıtlamayı başardığında, gerçekten de Cantor'un "ikinci sınıf sıra sayıları" na giren bir akıl yürütme türünün açık olduğunu iddia ederek bu sınırları aştı.

Kleene (2009 , s. 479) 1952'de Gentzen'in sonucunun önemi üzerine, özellikle Hilbert tarafından başlatılan biçimci program bağlamında aşağıdaki yorumu yapmıştır.

Biçimcilerin klasik matematiği bir tutarlılık ispatıyla güvenli hale getirmeye yönelik orijinal önerileri, ε 0'a kadar sonlu tümevarım gibi bir yöntemin kullanılması gerekeceğini düşünmüyordu . Gentzen kanıtı, klasik sayı teorisini güvence altına almak olarak ne ölçüde kabul edilebilir ki, bu problem formülasyonu mevcut durumda bireysel yargı meselesidir, kişinin one 0'a kadar sonlu bir kanıt olarak kabul etmeye ne kadar hazır olduğuna bağlı olarak, bireysel yargı meselesidir. yöntem.

Aritmetiğin diğer tutarlılık kanıtları

Gentzen'in tutarlılık kanıtının ilk versiyonu yaşamı boyunca yayınlanmadı çünkü Paul Bernays , ispatta zımnen kullanılan bir yönteme itiraz etmişti. Yukarıda açıklanan değiştirilmiş kanıt, 1936'da Annals'da yayınlandı . Gentzen, biri 1938'de diğeri 1943'te olmak üzere iki tutarlılık kanıtı daha yayınlamaya devam etti. Bunların tümü ( Gentzen & Szabo 1969 ) 'da yer almaktadır.

1940 yılında Wilhelm Ackermann da sıralı £ değenni kullanarak, Peano aritmetik için başka tutarlılık kanıtı yayınlanan 0 .

Gentzen'in kanıtıyla başlatılan çalışma

Gentzen'in kanıtı, kanıt-teorik sıra analizi denen şeyin ilk örneğidir . Sıralı analizde, teorilerin gücü, iyi düzenlenmiş olduğu kanıtlanabilen (yapıcı) sıra sayılarının ne kadar büyük olduğunu veya eşdeğer bir (yapıcı) ordinalin ne kadar büyük bir (yapıcı) sıralı tümevarımın sonlandırılabileceğini kanıtlayabildiğini ölçerek ölçülür. Yapıcı bir sıra, doğal sayıların özyinelemeli iyi sıralanmasının sıra türüdür .

Laurence Kirby ve Jeff Paris , 1982'de Goodstein'in teoreminin Peano aritmetiğinde kanıtlanamayacağını kanıtladılar. Kanıtları Gentzen'in teoremine dayanıyordu.

Notlar

Referanslar