Bir ispattaki kesim nedir?

Kesim kuralı, bir yardımcı önermeyi (lemma) ispatlamaya ve sonra onu kullanmaya olanak tanır: bir formülü oluşturan bir türetimden ve o formülü bir öncül olarak kullanan başka bir türetimden, birleşik sonucu çıkarmaktadır. Kesim-eliminasyonu, bu tür ara yardımcı önermelerin prensipte her zaman kaldırılabileceğini göstermektedir.

Kesimleri ortadan kaldırmak ispatları neden çok daha uzun hale getirebilir?

Bir kesimi kaldırmak, bir türetimin büyük kısımlarının kopyalanmasını gerektirebilir ve bunun tekrarlanması, ispat boyutunu üstel bir kule kadar artırabilir. Bu nedenle, kesimsiz ispatlar kavramsal olarak daha basit olmakla birlikte, kesimli orijinal ispatlardan çok daha büyük olabilmektedir.

Kesim-Eliminasyonu

Kesim-eliminasyonu, Gentzen'in, yardımcı önermelerin (lemma) kullanımını formüle eden kesim kuralının, herhangi bir sekant kalkülüsü ispatından çıkarılabileceğini ve böylece ispatın sadece ilgili formüllerden oluşacak şekilde yeniden yapılandırılabileceğini belirten teoremidir.

PaperMind ile konu bulYakındaMakale ve konu bul

Tools & resources

Slaytları indir

Learn & explore

VideoYakında

Tanım

Kesim-eliminasyonu, kesim kuralını kullanan herhangi bir sekant kalkülüsü türetiminin, bu kuralı kullanmayan bir türetime dönüştürülebileceğini gösteren bir teorem ve yapıcı bir prosedürdür; bu sayede ispatlanabilir her sekant, sadece nihai sekantın altformüllerini içeren bir ispata sahip olmaktadır.

Kapsam

Bu konu, kesim kuralını ve sekant kalkülüsündeki rolünü, kesim-eliminasyonu prosedürünü ve sonlanmasını, kesimsiz ispatların altformül özelliğini, bunun sonucunda ortaya çıkan tutarlılık ve karar verilebilirlik sonuçlarını ve eliminasyonun ispat boyutunda yol açabileceği sınırları kapsamaktadır.

Temel sorular

Kesim kuralı neyi ifade etmektedir ve kaldırılması neden önemlidir?
Kesim-eliminasyonu prosedürü nasıl sonlanmaktadır?
Altformül özelliği nedir ve ispat arayışı için ne anlama gelmektedir?
Kesimleri ortadan kaldırmanın hesaplama maliyeti nedir?

Temel kuramlar

Gentzen Hauptsatzı: Gentzen'in ana teoremi, kesim kuralının sekant kalkülüsünde kabul edilebilir olduğunu, bu nedenle kesimler kullanan herhangi bir ispatın, aynı nihai sekantın kesimsiz bir ispatına dönüştürülebileceğini belirtmektedir.
Altformül özelliği: Kesimsiz bir ispatta yer alan her formül, nihai sekantın bir altformülüdür; bu durum ispatın şeklini kısıtlamakta ve karar prosedürleri ile tutarlılık argümanlarının temelini oluşturmaktadır.
Kesim-eliminasyonu yoluyla tutarlılık: Boş sekantın kesimsiz bir ispatı imkansız olduğundan, kesim-eliminasyonu, kalkülüsün ve dolayısıyla formüle ettiği teorinin tutarlı olduğuna dair doğrudan bir ispat sağlamaktadır.

Klinik önem

Kesim-eliminasyonu, geniş sonuçları olan temel bir sonuçtur: tutarlılık ispatları, otomatik teorem ispatı ve tablo yöntemleri için temel olan altformül özelliği, interpolasyon teoremleri ve ispatlar-programlar yazışması aracılığıyla tipli programların normalizasyonunu sağlamaktadır.

Tarihçe

Gentzen, 1934 yılında birinci dereceden mantık için kesim-eliminasyonunu (Hauptsatz'ı) ispatlamış ve bu yöntem yapısal ispat teorisinin temel taşı haline gelmiştir. Tait ve Girard, bu tekniği daha güçlü sistemlere ve yüksek dereceden mantığa genişletmişler ve kesim-eliminasyonu altında ispat boyutundaki büyümenin sınırları başlı başına bir çalışma konusu haline gelmiştir.

Öne çıkan isimler

Gerhard Gentzen
William Tait
Jean-Yves Girard
Gaisi Takeuti

İlgili konular

Temel eserler

takeuti1987
troelstra2000
negri2001

Sıkça sorulan sorular

Bir ispattaki kesim nedir?: Kesim kuralı, bir yardımcı önermeyi (lemma) ispatlamaya ve sonra onu kullanmaya olanak tanır: bir formülü oluşturan bir türetimden ve o formülü bir öncül olarak kullanan başka bir türetimden, birleşik sonucu çıkarmaktadır. Kesim-eliminasyonu, bu tür ara yardımcı önermelerin prensipte her zaman kaldırılabileceğini göstermektedir.
Kesimleri ortadan kaldırmak ispatları neden çok daha uzun hale getirebilir?: Bir kesimi kaldırmak, bir türetimin büyük kısımlarının kopyalanmasını gerektirebilir ve bunun tekrarlanması, ispat boyutunu üstel bir kule kadar artırabilir. Bu nedenle, kesimsiz ispatlar kavramsal olarak daha basit olmakla birlikte, kesimli orijinal ispatlardan çok daha büyük olabilmektedir.