Gödel'in böyle bir kanıtı mevcut ve kendi bağlamında geçerli bir kanıt. Öte yandan, matematik belitsel olduğu için kanıtladığınız şeylerin ne kadar anlamlı olduğu yaptığınız tanımlara, belitlere ve mantık sisteminize ne kadar anlam yüklediğinize bağlı. Dolayısıyla bu kanıtın "pratik" sonuçları olup olmadığı ya da "gerçekten" bir şey söyleyip söylemediği tartışılabilir.
Gödel'in kanıtındaki fikrin özü "ontolojik kanıt" olarak geçer. Ontolojik kanıt Gödel'den önce bilinen bir şey aslında. St. Anselmus, Descartes ve Leibniz gibi insanlar tarafından kullanılıyor. Ontolojik kanıtlardaki genel yaklaşım Tanrı'nin belirli özellikleri olduğunu varsaymak, öyle ki bu özellikler Tanrı'yı "var olmak zorunda" bıraksın. St. Anselmus'un kanıtında bu özellik "kendisinden daha üstününün tasavvur edilememesi", Descartes'ınkinde de "tüm mükemmelliklere sahip olmak" şeklinde. Tabii St. Anselmus'un ve Descartes'ın argümanları "günlük dil" içerisinde yapıldıkları için kullandıkları kavramlar ve yaptıkları çıkarımların mekanizmaları açısından çok muğlak kalıyorlar. Dolayısıyla pek ikna edici değiller.
Gödel'in yaptığı şeyin farkı ise kafasındaki ontolojik argümanı bir modern mantık sistemi içerisinde biçimselleştirip belitselleştirmesi.
Kanıt, tanımsız terim olarak bırakılan pozitif özellikler üzerinden yürüyor. Tanrı'yı tüm pozitif özelliklere sahip şey olarak tanımlıyoruz. Pozitif özelliklerin sağladığını belit olarak varsaydığımız bazı özellikler var. Daha sonra da modal mantık içerisinde tüm pozitif özelliklere sahip bir şeyin, yani Tanrı'nın, var olduğunu kanıtlıyoruz.
Gödel'in kanıtı matematiksel olarak doğrudur ve biçimselleştirilip doğruluğu kontrol edilmiştir. Bu konuda yapılmış bir çalışma için şu makaleyi okuyabilirsiniz. Bu makaleye ek olarak da kanıtın hangi basamaklarının hangi modal mantık sistemi içerisinde yapılabildiğini açıklayan bir özet için şu bağlantıya bakınız.
Şimdi de Gödel'in kanıtını genel hatlarıyla özetleyeyim, daha doğrusu Türkçeye çevireyim. Yüksek mertebeli mantık içerisinde çalışacağız çünkü sadece objeler üzerinde değil özellikler üzerinde de niceleme (quantification) yapmak istiyoruz. Ayrıca modal mantık kullanacağız, yani "zorunlu" ve "olası" şeklinde iki operatörümüz var. Bağlantısını verdiğim Wikipedia sayfasından modal mantık için çeşitli belit sistemleri ve modal operatörlerin nasıl tanımlandığı okunabilir.
"Pozitif özellik" dediğimiz şeyin ne olduğunu tanımlamayacağız. Öte yandan pozitif özelliklerle ilgili belitler sunacağız. $P$ pozitiflik yüklemi olmak üzere,
Belit 1: Her özellik için o özellik pozitif değildir ancak ve ancak o özelliğin değili pozitifse.
$\forall \phi (\neg P(\phi) \leftrightarrow P(\neg \phi))$
Belit 2: Pozitif bir özellik tarafından zorunlu olarak gerektirilen her özellik pozitiftir.
$\forall \phi \forall \psi ([P(\phi) \wedge \square \forall x (\phi(x) \rightarrow \psi(x))] \rightarrow P(\psi))$
Teorem 1: Pozitif özellikler olası olarak örneklenir.
$\forall \phi [P(\phi) \rightarrow \lozenge \exists x \phi(x)]$
Tanım 1: Tüm pozitif özelliklere sahip şeye Tanrısal-varlık diyelim ve G ile gösterelim. (God ya da Gödel'in G'si olsun bu.)
$G(x) \leftrightarrow \forall \phi [P(\phi) \rightarrow \phi(x)]$
Belit 3: Tanrısal-varlık olmak pozitif bir özelliktir.
$P(G)$
Ara sonuç: Olası olarak, bir Tanrısal-varlık vardır.
$\lozenge \exists x G(x)$
Belit 4: Pozitif özellikler zorunlu olarak pozitiftir.
$\forall \phi (P(\phi) \rightarrow \square P(\phi))$
Tanım 2: Bir objenin sahip olduğu ve o objenin tüm özelliklerini zorunlu olarak gerektiren her özelliğe o objenin bir özü (essence) diyelim.
$\phi\ ess\ x \leftrightarrow \phi(x) \wedge (\forall \psi (\psi(x) \rightarrow \square \forall y (\phi(y) \rightarrow \psi(y))))$
Teorem 2: Tanrısal-varlık olmak özelliği her Tanrısal-varlığın özüdür.
$\forall x (G(x) \rightarrow G\ ess\ x)$
Tanım 4: Tüm özleri zorunlu olarak örneklenen bir varlığa zorunlu olarak vardır diyelim ve zorunlu olarak var olmak özelliğini NE ile gösterelim (necessary existence).
$NE(x) \leftrightarrow \forall \phi (\phi\ ess\ x \rightarrow \square \exists y \phi(y))$
Belit 5: Zorunlu olarak var olmak pozitif bir özelliktir.
$P(NE)$
Teorem 3: Zorunlu olarak, bir Tanrısal-varlık vardır.
$\square \exists x G(x)$
Bu kanıtın her basamağı öncekilerden ilgili mantık sistemi içerisinde çıkarsanabiliyor, ki attığım ilk makalenin tek yaptığı da bunu bilgisayar yardımı ile kontrol etmek. Bağlantısını verdiğim ikinci yazıdan da hangi mantık sisteminin ve çıkarım kurallarının gerektiği okunabilir.
Dolayısıyla, eğer yapılan tanımları, bu beş beliti, modal mantığı ve çıkarım kurallarını kabul etmeye hazırsanız, Tanrı vardır.