Gödel'in Eksiklik Teoremleri

Gödel'in Eksiklik Teoremleri, modern mantığın en temel sonuçları arasında yer alan ve biçimsel aksiyomatik sistemlerde ispatlanabilirliğin sınırlarıyla ilgili olan iki teoremdir. Avusturyalı mantıkçı ve felsefeci Kurt Gödel tarafından 1931 yılında yayımlanan bu teoremler, matematiğin temelleri, biçimselcilik ve hesaplanabilirlik kuramı gibi alanlarda etkiler bırakmıştır.

Birinci eksiklik teoremi, belirli bir miktar aritmetiği içerebilen herhangi bir tutarlı biçimsel sistemin içerisinde, ne ispatlanabilen ne de çürütülebilen ifadelerin (önermelerin) var olduğunu belirtir. İkinci eksiklik teoremi ise, böyle bir biçimsel sistemin, kendi tutarlılığını yine kendi içinde ispatlayamayacağını ifade eder. Bu sonuçlar, matematik ve mantık felsefesinde değişikliklere yol açmıştır.

Biçimsel Mantığın Aşılmaz Ve Eksik Sınırları (Yapay Zeka İle Oluşturulmuştur.)

Tanım ve Temel Kavramlar

Gödel'in teoremlerini anlamak için bazı temel kavramların açıklanması gereklidir:

• Biçimsel Sistem (Formal System): Yeni teoremlerin üretilmesine olanak tanıyan çıkarım kuralları ile donatılmış bir aksiyomlar sistemidir. Bir biçimsel sistemin aksiyom kümesinin sonlu veya en azından karar verilebilir olması, yani belirli bir ifadenin aksiyom olup olmadığına mekanik olarak karar veren bir algoritmanın bulunması gerekir. Çıkarım kuralları da etkili işlemlerdir, bu sayede belirli bir formül dizisinin sistem içinde geçerli bir ispat olup olmadığına mekanik olarak karar verilebilir.

• Tutarlılık (Consistency): Bir biçimsel sistemde, hem bir ifadenin hem de o ifadenin değilinin (çelişiğinin) aynı anda ispatlanamaması durumudur. Tutarsız bir sistemde her ifade ispatlanabilir olduğu için, bu tür sistemler anlamsız kabul edilir.

• Tamlık (Completeness): Bir biçimsel sistemin dilindeki her ifade için, ya ifadenin kendisinin ya da değilinin sistem içinde ispatlanabilmesi (türetilebilmesi) durumudur. Gödel'in teoremleri, belirli koşulları sağlayan sistemlerin bu anlamda tam olamayacağını göstermektedir.

Teoremlerin geçerli olduğu sistemler, genellikle en azından Robinson Aritmetiği (Q) olarak bilinen zayıf bir aritmetik sistemini veya daha yaygın olarak Peano Aritmetiği'ni (PA) içerebilen sistemlerdir.

Tarihsel Gelişim ve Bağlam

20. yüzyılın başlarında, matematiğin temellerinde bir kriz yaşanmaktaydı. Georg Cantor'un sonsuz kümeler kuramı ve Bertrand Russell gibi düşünürlerin bu kuramda keşfettiği paradokslar (örneğin Russell Paradoksu), matematiğin değişmez temellerine olan güveni zedelemişti.

Bu krize bir yanıt olarak, Alman matematikçi David Hilbert, biçimselcilik (formalism) olarak bilinen bir program başlattı. Hilbert'in programının temel amacı, tüm matematiği çelişkilerden arındırmak, sağlam bir temel üzerine oturtmak ve bunu yaparken sonlu (finitary) yöntemler kullanmaktı. Hilbert programı şu hedefleri içeriyordu:

1. Tutarlılık: Sistemin çelişki içermediğinin ispatlanması.
2. Tamlık: Sistemdeki her doğru önermenin ispatlanabilir olması.
3. Karar Verilebilirlik (Decidability): Herhangi bir önermenin doğruluğuna veya yanlışlığına karar verecek bir algoritmanın varlığı.

Hilbert, matematiğin bu şekilde mekanikleştirilebileceğini ve "bilinemeyecek hiçbir şeyin olmadığını" savunuyordu. Gödel'in 1930'da Viyana'da açıkladığı ve 1931'de yayımladığı teoremleri, Hilbert'in bu programının, özellikle tamlık ve kendi içinde tutarlılık ispatı hedeflerinin, planlandığı şekilde gerçekleştirilemeyeceğini gösterdi.

Birinci Eksiklik Teoremi ve Kanıt Süreci

Teorem: Aritmetiği ifade edebilen her tutarlı biçimsel T teorisinde, doğruluğuna veya yanlışlığına karar verilemeyen, yani T içinde ne kanıtlanabilen ne de çürütülebilen önermeler vardır. Gödel'in bu teoremi ispatlama süreci birkaç temel adımdan oluşur:

Aritmetikleştirme (Gödel Numaralandırması)

Gödel, ilk olarak biçimsel sistemin dilindeki her sembol, formül ve ispat dizisine benzersiz bir doğal sayı atayan bir yöntem geliştirdi. Bu sayıya "Gödel numarası" denir. Bu yöntem sayesinde, bir sistemin sözdizimi (sentaks) hakkındaki iddialar, sayılar ve onlar arasındaki aritmetik ilişkiler hakkındaki iddialara dönüştürülebilir. Örneğin, bir formülün "ispatlanabilir" olması gibi sözdizimsel bir özellik, o formülün Gödel numarasına sahip olan bir sayısal özelliğe karşılık gelir.

İspatlanabilirlik Yükleminin Temsili

"x Gödel sayılı formülün, y Gödel sayılı bir ispatı vardır" şeklindeki ilişki <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mopen">(</span><span class="mord mathnormal" style="margin-right:0.13889em;">P</span><span class="mord mathnormal" style="margin-right:0.02778em;">r</span><span class="mord"><span class="mord mathnormal" style="margin-right:0.10764em;">f</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:-0.1076em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span><span class="mopen">(</span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.1667em;"></span><span class="mord mathnormal">x</span><span class="mclose">))</span></span></span></span>, sistemin kendi içinde bir aritmetik formülle temsil edilebilir. Buradan hareketle, bir formülün ispatlanabilirliği <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mopen">(</span><span class="mord mathnormal" style="margin-right:0.13889em;">P</span><span class="mord mathnormal">ro</span><span class="mord"><span class="mord mathnormal" style="margin-right:0.03588em;">v</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:-0.0359em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mclose">))</span></span></span></span>, "o formülün bir ispatı vardır" <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mopen">(</span><span class="mord">∃</span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mord mathnormal" style="margin-right:0.13889em;">P</span><span class="mord mathnormal" style="margin-right:0.02778em;">r</span><span class="mord"><span class="mord mathnormal" style="margin-right:0.10764em;">f</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:-0.1076em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span><span class="mopen">(</span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.1667em;"></span><span class="mord mathnormal">x</span><span class="mclose">))</span></span></span></span>şeklinde ifade edilebilir. Bu ispatlanabilirlik yüklemi, sistem içinde zayıf olarak temsil edilebilir (weakly representable).

Köşegenleştirme (Diyagonalizasyon) ve "Kendine Gönderme"

Gödel, bir formülün kendi Gödel numarası hakkında bir iddiada bulunmasını sağlayan bir teknik kullandı. Bu teknik, Köşegenleştirme Lemması olarak bilinir ve biçimsel olarak şunu ifade eder: Herhangi bir <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord mathnormal">A</span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mclose">)</span></span></span></span>formülü için, <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.6944em;"></span><span class="mord mathnormal" style="margin-right:0.13889em;">F</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">⊢</span><span class="mspace" style="margin-right:0.2778em;"></span></span><span class="base"><span class="strut" style="height:0.6833em;"></span><span class="mord mathnormal" style="margin-right:0.02778em;">D</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">↔</span><span class="mspace" style="margin-right:0.2778em;"></span></span><span class="base"><span class="strut" style="height:1.138em;vertical-align:-0.25em;"></span><span class="mord mathnormal">A</span><span class="mopen"><span class="mopen">(</span><span class="msupsub"><span class="vlist-t"><span class="vlist-r"><span class="vlist" style="height:0.888em;"><span style="top:-3.063em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mtight"><span class="mopen mtight">⌈</span></span></span></span></span></span></span></span></span><span class="mord"><span class="mord mathnormal" style="margin-right:0.02778em;">D</span><span class="msupsub"><span class="vlist-t"><span class="vlist-r"><span class="vlist" style="height:0.888em;"><span style="top:-3.063em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mtight"><span class="mclose mtight">⌉</span></span></span></span></span></span></span></span></span><span class="mclose">)</span></span></span></span> olacak şekilde bir <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.6833em;"></span><span class="mord mathnormal" style="margin-right:0.02778em;">D</span></span></span></span> cümlesi inşa edilebilir. Bu <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.6833em;"></span><span class="mord mathnormal" style="margin-right:0.02778em;">D</span></span></span></span> cümlesi, kendisinin <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.6833em;"></span><span class="mord mathnormal">A</span></span></span></span> özelliğine sahip olduğunu "iddia eder".

Gödel Cümlesinin (G) İnşası

Gödel, Köşegenleştirme Lemması'nı "ispatlanamaz" özelliğine, yani <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord">¬</span><span class="mord mathnormal" style="margin-right:0.13889em;">P</span><span class="mord mathnormal">ro</span><span class="mord"><span class="mord mathnormal" style="margin-right:0.03588em;">v</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:-0.0359em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mclose">)</span></span></span></span>formülüne uyguladı. Bunun sonucunda şu özelliğe sahip bir Gödel cümlesi (<span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.8333em;vertical-align:-0.15em;"></span><span class="mord"><span class="mord mathnormal">G</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span></span></span></span>) elde etti: <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.6944em;"></span><span class="mord mathnormal" style="margin-right:0.13889em;">F</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">⊢</span><span class="mspace" style="margin-right:0.2778em;"></span></span><span class="base"><span class="strut" style="height:0.8333em;vertical-align:-0.15em;"></span><span class="mord"><span class="mord mathnormal">G</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">↔</span><span class="mspace" style="margin-right:0.2778em;"></span></span><span class="base"><span class="strut" style="height:1.3383em;vertical-align:-0.2935em;"></span><span class="mord">¬</span><span class="mord mathnormal" style="margin-right:0.13889em;">P</span><span class="mord mathnormal">ro</span><span class="mord"><span class="mord mathnormal" style="margin-right:0.03588em;">v</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:-0.0359em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span><span class="mopen"><span class="mopen">(</span><span class="msupsub"><span class="vlist-t"><span class="vlist-r"><span class="vlist" style="height:0.888em;"><span style="top:-3.063em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mtight"><span class="mopen mtight">⌈</span></span></span></span></span></span></span></span></span><span class="mord"><span class="mord mathnormal">G</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:1.0448em;"><span style="top:-2.4065em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span><span style="top:-3.2198em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mtight"><span class="mclose mtight">⌉</span></span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.2935em;"><span></span></span></span></span></span></span><span class="mclose">)</span></span></span></span> Bu cümle, sezgisel olarak "Ben bu sistemde ispatlanamam" anlamına gelir.

Bu cümlenin ne ispatlanabilir ne de çürütülebilir olduğu gösterilebilir:

• Eğer <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.8333em;vertical-align:-0.15em;"></span><span class="mord"><span class="mord mathnormal">G</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span></span></span></span>ispatlanabilir olsaydı, o zaman<span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1.3383em;vertical-align:-0.2935em;"></span><span class="mord mathnormal" style="margin-right:0.13889em;">P</span><span class="mord mathnormal">ro</span><span class="mord"><span class="mord mathnormal" style="margin-right:0.03588em;">v</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:-0.0359em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span><span class="mopen"><span class="mopen">(</span><span class="msupsub"><span class="vlist-t"><span class="vlist-r"><span class="vlist" style="height:0.888em;"><span style="top:-3.063em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mtight"><span class="mopen mtight">⌈</span></span></span></span></span></span></span></span></span><span class="mord"><span class="mord mathnormal">G</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:1.0448em;"><span style="top:-2.4065em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span><span style="top:-3.2198em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mtight"><span class="mclose mtight">⌉</span></span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.2935em;"><span></span></span></span></span></span></span><span class="mclose">)</span></span></span></span>ifadesi de doğru ve sistemde ispatlanabilir olurdu. Ancak bu durum, yukarıdaki denklik gereği <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.8333em;vertical-align:-0.15em;"></span><span class="mord">¬</span><span class="mord"><span class="mord mathnormal">G</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span></span></span></span>'nin de ispatlanabilir olması anlamına gelirdi ki bu, sistemin tutarsız olması demektir.

• Eğer <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.8333em;vertical-align:-0.15em;"></span><span class="mord">¬</span><span class="mord"><span class="mord mathnormal">G</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span></span></span></span>ispatlanabilir olsaydı, denklik gereği <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1.3383em;vertical-align:-0.2935em;"></span><span class="mord mathnormal" style="margin-right:0.13889em;">P</span><span class="mord mathnormal">ro</span><span class="mord"><span class="mord mathnormal" style="margin-right:0.03588em;">v</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:-0.0359em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span><span class="mopen"><span class="mopen">(</span><span class="msupsub"><span class="vlist-t"><span class="vlist-r"><span class="vlist" style="height:0.888em;"><span style="top:-3.063em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mtight"><span class="mopen mtight">⌈</span></span></span></span></span></span></span></span></span><span class="mord"><span class="mord mathnormal">G</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:1.0448em;"><span style="top:-2.4065em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span><span style="top:-3.2198em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mtight"><span class="mclose mtight">⌉</span></span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.2935em;"><span></span></span></span></span></span></span><span class="mclose">)</span></span></span></span>'nin de ispatlanabilir olması gerekirdi. Bu ise " <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.8333em;vertical-align:-0.15em;"></span><span class="mord"><span class="mord mathnormal">G</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span></span></span></span>ispatlanabilir" anlamına gelir. Ancak sistemin 1-tutarlı (1-consistent) olduğu varsayımı altında, eğer <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.8333em;vertical-align:-0.15em;"></span><span class="mord"><span class="mord mathnormal">G</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span></span></span></span>ispatlanamazsa sistem bunu bilir ve <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1.3383em;vertical-align:-0.2935em;"></span><span class="mord mathnormal" style="margin-right:0.13889em;">P</span><span class="mord mathnormal">ro</span><span class="mord"><span class="mord mathnormal" style="margin-right:0.03588em;">v</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:-0.0359em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span><span class="mopen"><span class="mopen">(</span><span class="msupsub"><span class="vlist-t"><span class="vlist-r"><span class="vlist" style="height:0.888em;"><span style="top:-3.063em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mtight"><span class="mopen mtight">⌈</span></span></span></span></span></span></span></span></span><span class="mord"><span class="mord mathnormal">G</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:1.0448em;"><span style="top:-2.4065em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span><span style="top:-3.2198em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mtight"><span class="mclose mtight">⌉</span></span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.2935em;"><span></span></span></span></span></span></span><span class="mclose">)</span></span></span></span>'yi ispatlayamaz. Bu durum bir çelişki yaratır.

Dolayısıyla, eğer sistem tutarlı ise <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.8333em;vertical-align:-0.15em;"></span><span class="mord"><span class="mord mathnormal">G</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span></span></span></span> ne ispatlanabilir ne de çürütülebilir; sistem zorunlu olarak eksiktir. Dahası, <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.8333em;vertical-align:-0.15em;"></span><span class="mord"><span class="mord mathnormal">G</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span></span></span></span> cümlesi genellikle "doğru ama ispatlanamaz" olarak nitelendirilir, çünkü tutarlı bir sistemde ispatlanamadığı için, söylediği şey (yani ispatlanamaz olduğu) doğrudur.

İkinci Eksiklik Teoremi

Teorem: Aritmetiği içerebilen herhangi bir tutarlı biçimsel <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.6833em;"></span><span class="mord mathnormal" style="margin-right:0.13889em;">F</span></span></span></span>sistemi, kendi tutarlılığını <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord mathnormal" style="margin-right:0.07153em;">C</span><span class="mord mathnormal">o</span><span class="mord mathnormal">n</span><span class="mord mathnormal">s</span><span class="mopen">(</span><span class="mord mathnormal" style="margin-right:0.13889em;">F</span><span class="mclose">)</span></span></span></span>içinde ispatlayamaz.

Bu teoremin ispatı, birinci teoremin ispat sürecinin sistemin kendisi içinde biçimselleştirilmesine dayanır.

1. Sistemin tutarlılığı, "çelişkinin (örneğin <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.6444em;"></span><span class="mord">0</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">=</span><span class="mspace" style="margin-right:0.2778em;"></span></span><span class="base"><span class="strut" style="height:0.6444em;"></span><span class="mord">1</span></span></span></span>) ispatlanamaz olması" şeklinde biçimsel bir formülle ifade edilebilir: <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord mathnormal" style="margin-right:0.07153em;">C</span><span class="mord mathnormal">o</span><span class="mord mathnormal">n</span><span class="mord mathnormal">s</span><span class="mopen">(</span><span class="mord mathnormal" style="margin-right:0.13889em;">F</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">≡</span><span class="mspace" style="margin-right:0.2778em;"></span></span><span class="base"><span class="strut" style="height:1.138em;vertical-align:-0.25em;"></span><span class="mord">¬</span><span class="mord mathnormal" style="margin-right:0.13889em;">P</span><span class="mord mathnormal">ro</span><span class="mord"><span class="mord mathnormal" style="margin-right:0.03588em;">v</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:-0.0359em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span><span class="mopen"><span class="mopen">(</span><span class="msupsub"><span class="vlist-t"><span class="vlist-r"><span class="vlist" style="height:0.888em;"><span style="top:-3.063em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mtight"><span class="mopen mtight">⌈</span></span></span></span></span></span></span></span></span><span class="mord">0</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">=</span><span class="mspace" style="margin-right:0.2778em;"></span></span><span class="base"><span class="strut" style="height:1.138em;vertical-align:-0.25em;"></span><span class="mord"><span class="mord">1</span><span class="msupsub"><span class="vlist-t"><span class="vlist-r"><span class="vlist" style="height:0.888em;"><span style="top:-3.063em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mtight"><span class="mclose mtight">⌉</span></span></span></span></span></span></span></span></span><span class="mclose">)</span></span></span></span>.
2. Birinci teoremin ilk kısmının ispatı ("Eğer F tutarlıysa, <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.8333em;vertical-align:-0.15em;"></span><span class="mord"><span class="mord mathnormal">G</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span></span></span></span> ispatlanamaz") F'nin kendi içinde biçimselleştirilebilir. Bu, şu formüle karşılık gelir: <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.6944em;"></span><span class="mord mathnormal" style="margin-right:0.13889em;">F</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">⊢</span><span class="mspace" style="margin-right:0.2778em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord mathnormal" style="margin-right:0.07153em;">C</span><span class="mord mathnormal">o</span><span class="mord mathnormal">n</span><span class="mord mathnormal">s</span><span class="mopen">(</span><span class="mord mathnormal" style="margin-right:0.13889em;">F</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2778em;"></span><span class="mrel">→</span><span class="mspace" style="margin-right:0.2778em;"></span></span><span class="base"><span class="strut" style="height:0.8333em;vertical-align:-0.15em;"></span><span class="mord"><span class="mord mathnormal">G</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span></span></span></span>
3. Eğer F sistemi kendi tutarlılığını, yani Cons(F)'yi ispatlayabilseydi, o zaman modus ponens çıkarım kuralı ile <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.8333em;vertical-align:-0.15em;"></span><span class="mord"><span class="mord mathnormal">G</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span></span></span></span>'yi de ispatlayabilirdi.
4. Ancak <span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.8333em;vertical-align:-0.15em;"></span><span class="mord"><span class="mord mathnormal">G</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3283em;"><span style="top:-2.55em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.13889em;">F</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span></span></span></span>​'nin F içinde ispatlanması, birinci eksiklik teoremine göre sistemin tutarsız olması anlamına gelir.
5. Dolayısıyla, eğer F tutarlıysa, kendi tutarlılığını ispatlayamaz.

Bu sonuç, Hilbert'in, matematiğin tutarlılığının sonlu ve "güvenli" metotlarla (ki bu metotların aritmetik içinde biçimselleştirilebileceği düşünülüyordu) ispatlanabileceği yönündeki umuduna büyük bir darbe vurdu. Bir sistemin tutarlılığı ancak ondan daha güçlü bir sistem kullanılarak ispatlanabilir, bu da tutarlılık ispatlarını mutlak değil, göreceli hale getirir.

İlgili Sonuçlar ve Teoremler

Gödel'in teoremlerinde kullanılan teknikler, mantık ve hesaplanabilirlik kuramında başka önemli sonuçlara da yol açmıştır:

Tarski'nin Doğrunun Tanımlanamazlığı Teoremi

Yeterli miktarda aritmetik içeren tutarlı bir F sisteminin dilinde, o dilin "doğru" cümleler kümesini tanımlayan bir formül (Tr(x)) bulunamaz. Eğer bulunsaydı, "Bu cümle doğru değildir" diyen bir "Yalancı Paradoksu" cümlesi inşa edilebilir ve bu da sistemde bir çelişkiye yol açardı.

Karar Verilemezlik (Undecidability)

Aritmetiği içeren teorilerin çoğu aynı zamanda karar verilemezdir, yani herhangi bir cümlenin teorem olup olmadığına karar verecek mekanik bir prosedür (algoritma) yoktur. Bu sonuç, Alan Turing ve Alonzo Church'ün çalışmalarıyla yakından ilişkilidir ve Church-Turing Tezi ile sağlam bir temele oturtulmuştur.

Hilbert'in Onuncu Problemi

1970'te Yuri Matiyasevich, Julia Robinson, Martin Davis ve Hilary Putnam'ın çalışmalarını tamamlayarak, verilen bir Diophantine denkleminin (tam sayı katsayılı polinom denklemi) tam sayı çözümleri olup olmadığına karar verecek genel bir algoritmanın olmadığını ispatlamıştır. Bu, Gödel'in teoremleriyle ilişkili bir karar verilemezlik sonucudur.

Felsefi Etkileri

Gödel'in teoremleri, matematik felsefesinin seyrini kalıcı olarak değiştirmiştir:

Hilbert'in Programı

Teoremler, Hilbert'in biçimselci programının temel hedeflerinin (özellikle tutarlılık ve tamlık ilkelerinin) biçimsel sistemler içerisinde sağlanamayacağını ortaya koyarak, söz konusu programın uygulanabilirliğini sınırlamıştır.

İspat ve Doğruluk Ayrımı

Teoremler, biçimsel bir sistemde "ispatlanabilirlik" ile (genellikle Tarski'nin tanımına göre anlaşılan) "doğruluk" kavramlarının özdeş olmadığını göstermiştir. Doğru olduğu halde ispatlanamayan aritmetik önermelerin varlığı, matematiksel doğruluğun biçimsel sistemler tarafından tam olarak kuşatılamayacağını ortaya koymuştur.

Platonculuk ve Sezgicilik

Gödel, teoremlerin matematiksel nesnelerin ve gerçeklerin insan zihninden bağımsız olarak var olduğu şeklindeki Platoncu görüşü desteklediğini düşünmüştür. Ona göre, eğer matematik sadece kendi yaratımımız olsaydı, çözemeyeceğimiz problemler olmamalıydı. Gödel, aksiyomların doğruluğuna bir tür "matematiksel görü" (mathematical intuition) yoluyla ulaştığımızı öne sürmüştür.

Mekanizma Karşıtı Argümanlar

Filozoflar J.R. Lucas ve Roger Penrose, Gödel'in teoremlerini insan zihninin herhangi bir sonlu makineyi veya biçimsel sistemi aştığını savunmak için kullanmışlardır. Argümanlarına göre, herhangi bir makine için onun ispatlayamayacağı bir Gödel cümlesi vardır, ancak insan zihni bu cümlenin doğru olduğunu "görebilir". Bu argümanlar, Gödel cümlesinin doğruluğunun sistemin tutarlılığına bağlı olduğu ve insanın bir sistemin tutarlılığını her zaman sezgisel olarak bilemeyeceği gerekçesiyle eleştirilmiştir.