Kanıt Kuramı
Kanıt kuramı, biçimsel kanıtları kendi başlarına matematiksel nesneler olarak inceler; yapılarını, dönüşümlerini ve bu kanıtları üreten kuramların gücünü analiz etmektedir.
Tanım
Kanıt kuramı, matematiksel mantığın, biçimsel sistemlerdeki kanıtları sonlu kombinatoryal nesneler olarak ele alan, bunların nasıl dönüştürülebileceğini ve normalleştirilebileceğini, ayrıca varlıklarının temel kuramların tutarlılığı ve gücü hakkında neyi ortaya koyduğunu inceleyen bir dalıdır.
Kapsam
Bu alan, doğal çıkarım ve sekant hesabı gibi biçimsel hesaplamaları, kesme-eleme ve normalleştirme teoremlerini, Gödel'in eksiklik teoremlerini, kuramların gücünün sıra sayısal analiz (ordinal analysis) ile ölçülmesini ve kanıtlar ile programlar arasındaki yazışma (correspondence) aracılığıyla ortaya çıkan kanıtların yapıcı ve hesaplamalı içeriğini kapsamaktadır.
Alt konular
Temel sorular
- Biçimsel kanıtlar kombinatoryal nesneler olarak nasıl temsil edilebilir ve manipüle edilebilir?
- Kanıtlardaki hangi dolambaçlı yollar sistematik olarak ortadan kaldırılabilir ve bu neyi ortaya koyar?
- Biçimsel bir kuramın kendisi hakkında kanıtlayabileceği şeylere ilişkin doğal sınırlar nelerdir?
- Bir kuramın gücü hassas bir şekilde nasıl ölçülebilir?
Temel kuramlar
- Kesme-Eleme Teoremi
- Gentzen, sekant hesabındaki herhangi bir kanıtın kesme kuralı olmadan bir kanıta dönüştürülebileceğini, böylece alt formül özelliğine sahip kanıtlar ve doğrudan tutarlılık sonuçları elde edildiğini göstermiştir.
- Gödel Eksiklik Teoremleri
- Aritmetiği ifade edebilecek kadar güçlü herhangi bir tutarlı biçimsel kuram, kanıtlayamayacağı doğru önermeler içerir ve kendi tutarlılığını kanıtlayamaz; bu da biçimselleştirmeye temel sınırlar getirmektedir.
- Curry-Howard Yazışması
- Doğal çıkarımdaki kanıtlar, tipli lambda hesabının terimlerine karşılık gelir ve kanıt normalleştirmesi hesaplamaya karşılık gelir; bu da kanıt kuramını programlama dilleri kuramına bağlar.
Klinik önem
Kanıt kuramı, matematikte tutarlılık ve yapıcı içeriğin analizinin temelini oluşturmakta; tip kuramı, fonksiyonel programlama ve otomatik kanıt yardımcıları için teorik temel sağlamaktadır. Bu bağlamda kanıtlar, doğrulanabilir programlar olarak da işlev görmektedir.
Tarihçe
Kanıt kuramı, Hilbert tarafından, matematiği sonlu tutarlılık kanıtlarıyla güvence altına alma programının bir parçası olarak kurulmuştur. Gödel'in 1931 tarihli eksiklik teoremleri, orijinal programın tam olarak başarılı olamayacağını göstermiş; Gentzen'in aritmetik için transfinite tümevarım yoluyla kesme-eleme ve tutarlılık kanıtı ise alanı sıra sayısal analize (ordinal analysis) ve daha sonra kanıtlar-programlar paradigmasına yönlendirmiştir.
Öne çıkan isimler
- David Hilbert
- Gerhard Gentzen
- Kurt Goedel
- Jean-Yves Girard
İlgili konular
Temel eserler
- troelstra2000
- takeuti1987
- girard1989
Sıkça sorulan sorular
- Kanıt kuramı model kuramından nasıl farklılaşır?
- Model kuramı, yapıları ve içlerindeki önermelerin doğruluğunu, yani semantik bir bakış açısını incelerken; kanıt kuramı, biçimsel türetmeleri ve bunların sentaktik dönüşümlerini inceler. Gödel'in tamlık teoremi ikisini birbirine bağlasa da, yöntemleri ve soruları farklıdır.
- Hilbert'in programı nedir?
- Bu, matematiğin tamamının tutarlılığını yalnızca sonlu, tartışmasız akıl yürütme kullanarak kanıtlama önerisiydi. Gödel'in ikinci eksiklik teoremi, yeterince güçlü hiçbir kuramın kendi tutarlılığını kanıtlayamayacağını göstermiştir; bu nedenle program orijinal haliyle yürütülemese de, değiştirilmiş versiyonları etkisini sürdürmektedir.