Matematikte, Alman matematikçi David Hilbert tarafından 1920'lerin başında formüle edilen Hilbert'in programı, matematiğin temellerini açıklığa kavuşturmaya yönelik ilk girişimlerin tutarsız olduğu bulunduğunda, matematiğin temel krizine önerilen bir çözümdü. Çözüm olarak Hilbert, mevcut tüm teorileri sonlu, sonlu bir aksiyom dizisine dayandırmayı ve bu aksiyomların tutarlı olduğuna dair bir kanıt sunmayı önerdi. Hilbert, gerçek analiz gibi daha karmaşık sistemlerin tutarlılığının daha basit sistemleri kullanarak kanıtlayabileceğini gösterdi. Sonuçta matematiğin tamamının tutarlılığı temel aritmetiğe indirgenebilir.
Gödel'in 1931'de yayınlanan eksiklik teoremleri, Hilbert'in programının matematiğin kilit alanlarında uygulanamaz olduğunu gösterdi. Gödel, ilk teoreminde, aritmetiği ifade edebilen, hesaplanabilir aksiyomlar dizisine sahip herhangi bir tutarlı sistemin asla sonlu olamayacağını gösterdi: Doğru olduğu kanıtlanabilen, bir ifade oluşturmak mümkündür ancak mevcut formel sistemler kullanılarak türetilemez. İkinci teoreminde ise böyle bir sistemin kendi tutarlılığını kanıtlayamayacağını, dolayısıyla daha güçlü bir şeyin tutarlılığını kesinlikle kanıtlamak için kullanılamayacağını gösterdi. Bu, Hilbert'in sonlu bir sistemin kendi tutarlılığını kanıtlamak için kullanılabileceği ve dolayısıyla geri kalan her şeyi kanıtlayabileceği yönündeki varsayımını çürüttü.
Hilbert Programı'nın Önermeleri
Hilbert'in programının temel amacı tüm matematik alanlarını kapsayacak, sağlam bir temel bulmaktı. Bu temeli, aşağıdaki ilkeler üzerine kuracaktı:
Tüm matematiğin formel dille yazılmalı ve iyi tanımlanmış kurallara göre işlemler yapılmalıdır.
Bütünlük: Tüm doğru matematiksel ifadelerin formalizmde kanıtlanabileceğinin kanıtı.
Tutarlılık: Matematiğin formalizminde hiçbir çelişkinin elde edilemeyeceğinin kanıtı. Bu tutarlılık kanıtı tercihen sonlu matematiksel nesneler hakkında yalnızca "sonlu" akıl yürütmeyi kullanmalıdır.
Korunum: "İdeal nesneler" (sayılamayan kümeler gibi) hakkında akıl yürütme kullanılarak elde edilen "gerçek nesneler" hakkında herhangi bir sonucun, ideal nesneler kullanılmadan kanıtlanabileceğinin kanıtı.
Değerlendirilebirlik: Herhangi bir matematiksel ifadenin doğruluğuna veya yanlışlığına karar verecek bir algoritma olmalıdır.
Gödel'in Eksiklik Teoremleri
Kurt Gödel, Hilbert'in programının hedeflerinin çoğuna ulaşmanın, kabaca, imkansız olduğunu gösterdi. Gödel'in ikinci eksiklik teoremi, tamsayıların toplama ve çarpma işlemlerini kodlayacak kadar güçlü herhangi bir tutarlı teorinin kendi tutarlılığını kanıtlayamayacağını göstermektedir. Bu Hilbert'in programı için bir zorluk teşkil ediyor:
Tüm matematiksel doğru ifadeleri formel bir sistem içinde formelize etmek mümkün değildir, çünkü böyle bir formalizme yönelik herhangi bir girişim bazı doğru matematiksel ifadeleri kapsayamayacaktır.. Peano aritmetiğinin bile yinelemeli olarak numaralandırılabilir aksiyomlar dizisine dayanan tam ve tutarlı bir uzantısı yoktur.
Peano aritmetiği gibi bir teori kendi tutarlılığını bile kanıtlayamaz; bu nedenle onun "sonlu" bir alt kümesi, küme teorisi gibi daha geniş teorilerin tutarlılığını kesinlikle kanıtlayamaz.
Peano aritmetiğinin herhangi bir tutarlı uzantısında ifadelerin doğruluğuna kanıtlayabilecek bir algoritma yoktur. Açıkça konuşursak, Entscheidungsproblem'e yönelik bu olumsuz çözüm, Gödel teoreminden birkaç yıl sonra ortaya çıktı, çünkü o zamanlar algoritma kavramı kesin olarak tanımlanmamıştı.
Gödel'den sonra Hilbert Programı
Kanıt teorisi, ters matematik ve matematiksel mantık gibi birçok güncel ar aştırma kolu Hilbert'in orijinal programının doğal devamı olarak görülebilir. Hedeflerini biraz değiştirerek çoğu işlevli hale gelebilir (Zach 2005) ve aşağıdaki değişikliklerle bir kısmı başarıyla tamamlanmıştır:
Matematiğin tamamını formelize etmek mümkün olmasa da, umumi olarak kullanılan matematiğin tamamını formelize etmek mümkündür. Özellikle Zermelo-Fraenkel küme teorisi, birinci dereceden mantıkla birleştiğinde, neredeyse tüm güncel umumimatematik için tatmin edici ve genel kabul görmüş bir biçimcilik sağlar.
Peano aritmetiğini ifade edebilen (veya daha genel konuşmak gerekirse, hesaplanabilir bir aksiyom dizisine sahip) sistemler için tamamlanmışlığığı kanıtlamak mümkün olmasa da, diğer birçok ilginç sistem için bütünlük biçimlerini kanıtlamak mümkündür.Bütünlüğü kanıtlanmış önemsiz olmayan bir teorinin bir örneği, belirli bir karakteristiğe sahip cebirsel olarak kapalı alanlar teorisidir.
Güçlü teorilerin sonlu tutarlılık kanıtları olup olmadığı sorusunun yanıtlanması zordur; bunun temel nedeni, "sonlu kanıt"ın genel kabul görmüş bir tanımının olmamasıdır. Kanıt teorisindeki çoğu matematikçi, sonlu matematiğin Peano aritmetiğinin içinde olduğunu düşünüyor ve bu durumda oldukça güçlü teorilerin sonlu kanıtlarını vermek mümkün değil. Öte yandan Gödel, Peano aritmetiğinde formelize edilemeyen sonlu yöntemler kullanılarak sonlu tutarlılık kanıtları bulma olasılığını gördü, bu nedenle hangi sonlu yöntemlerin yürüyeceği konusunda daha açık görüşlü görünüyor. Birkaç yıl sonra Gentzen, Peano aritmetiği için bir tutarlılık kanıtı verdi. Bu ispatın açıkça sonlu olmayan tek kısmı ε 0ordinaline kadar belirli bir sonlu ötesi tümevarımdı. Eğer bu sonlu ötesi tümevarım sonlu bir yöntem olarak kabul edilirse Peano aritmetiğinin tutarlılığının sonlu bir kanıtı olduğu ileri sürülebilir. Gaisi Takeuti ve diğerleri tarafından ikinci dereceden aritmetiğin daha güçlü alt kümelerine tutarlılık kanıtları verilmiştir ve bu kanıtların tam olarak ne kadar sonlu veya yapıcı olduğu yine tartışılabilir. (Bu yöntemlerle tutarlılığı kanıtlanmış teoriler oldukça güçlüdür ve "sıradan" matematiğin çoğunu içerir.)
Peano aritmetiğinde ifadelerin doğruluğuna karar verecek bir algoritma olmamasına rağmen, bu tür algoritmaların bulunduğu pek çok ilginç ve önemsiz olmayan teori vardır. Örneğin Tarski, analitik geometrideki herhangi bir ifadenin doğruluğuna karar verebilecek bir algoritma buldu (daha doğrusu, gerçek kapalı alanlar teorisinin çıkarım yapılabilir olduğunu kanıtladı). Cantor-Dedekind aksiyomu göz önüne alındığında, bu algoritma Öklid geometrisindeki herhangi bir ifadenin doğruluğuna karar veren bir algoritma olarak kabul edilebilir.
↑Zalta, Edward N.; Nodelman, Uri, (Ed.) (2023), "Hilbert's Program", The Stanford Encyclopedia of Philosophy, Spring 2023, Metaphysics Research Lab, Stanford University5 Temmuz 2023Birden fazla yazar-name-list parameters kullanıldı (yardım); |ad= ve |soyadı= eksik (yardım)
G. Gentzen, 1936/1969. Die Widerspruchfreiheit der reinen Zahlentheorie. Matheatische Annalen 112:493–565. Gerhard Gentzen'in toplanan makaleleri, ME Szabo (ed.), 1969'da 'Aritmetiğin tutarlılığı' olarak tercüme edilmiştir.
D.Hilbert. 'Die Grundlegung der elementaren Zahlenlehre'. Matheatische Annalen 104:485–94. W. Ewald tarafından 'Temel Sayılar Teorisinin Temellendirilmesi' olarak çevrilmiştir, s.266–273, Mancosu (ed., 1998) Brouwer'dan Hilbert'e: 1920'lerde matematiğin temelleri üzerine tartışma, Oxford University Press. New York.
