Doğal Çıkarım ve Sekant Hesabı
Doğal çıkarım ve sekant hesabı, mantıksal bağlaçlar için giriş ve eleme kuralları aracılığıyla kanıtları temsil eden, yapısal kanıt kuramının temel mekanizmasını oluşturan iki Gentzen tarzı biçimsel sistemdir.
Tanım
Doğal çıkarım, gayri resmi akıl yürütmeyi yansıtan giriş ve eleme kurallarını kullanarak varsayımlardan formülleri türetirken; sekant hesabı, bir formül listesinin diğerini gerektirdiğini iddia eden sekantları, bir gerektirme ifadesinin solunda ve sağında etkili olan kurallar aracılığıyla manipüle etmektedir.
Kapsam
Bu konu, doğal çıkarım kurallarını giriş ve eleme çiftleriyle birlikte, sekant hesabının sol ve sağ kuralları ile yapısal kurallarını, doğal çıkarım için normalleştirmeyi, iki sistem arasındaki ilişkiyi ve bunların sezgisel ve klasik varyantlarını kapsamaktadır.
Temel sorular
- Giriş ve eleme kuralları, mantıksal bağlaçlara nasıl anlam kazandırmaktadır?
- Sekant nedir ve kuralları doğal çıkarımın kurallarından nasıl farklılık göstermektedir?
- Normalleştirme, doğal çıkarım kanıtlarını nasıl basitleştirmektedir?
- Bu hesapların klasik ve sezgisel versiyonları birbiriyle nasıl ilişkilidir?
Temel kuramlar
- Giriş ve eleme kuralları
- Her bağlaç, onu tanıtan kurallar ve onu kullanan kurallar tarafından yönetilir; ve bunların uyumu, yani elemenin girişin tam olarak neyi koyduğunu geri kazanması, bağlacın anlamını ifade etmektedir.
- Normalleştirme teoremi
- Prawitz, doğal çıkarım kanıtlarının, bir girişin bir eleme ile hemen geri alındığı dolambaçlardan arınmış normal bir forma indirgenebileceğini, yani kesim-elemesinin doğal çıkarım analoğu olduğunu göstermiştir.
- İki hesabın yazışması
- Doğal çıkarım ve sekant hesabı aynı teoremleri kanıtlar ve sekant sol kurallarının doğal çıkarım eleme kurallarına karşılık gelmesiyle birbirine çevrilebilir.
Klinik önem
Bu hesaplar, kanıtları yapısal olarak incelemek için standart formatlardır: doğal çıkarım, kanıtlar-programlar yazışması aracılığıyla tip kuramının ve kanıt asistanlarının temelini oluştururken; sekant hesabı, kesim-elemesi sonrası alt formül özelliğine sahip olarak, otomatik kanıt arama ve analitik tabloların temelini oluşturmaktadır.
Tarihçe
Gentzen, hem doğal çıkarımı hem de sekant hesabını 1934 ve 1935 yıllarında tanıtmış, doğal çıkarımı analiz etmenin daha zor olduğunu gördükten sonra kesim-elemesi teoremini elde etmek için sekant hesabını geliştirmiştir. Prawitz, 1965 yılında kapsamlı bir normalleştirme çalışmasıyla doğal çıkarımı yeniden canlandırmış ve bu sistemler, daha sonraki kanıtlar-programlar gelişmelerinin merkezine yerleşmiştir.
Öne çıkan isimler
- Gerhard Gentzen
- Dag Prawitz
- Stanislaw Jaskowski
- Jan von Plato
İlgili konular
Temel eserler
- troelstra2000
- prawitz1965
- negri2001
Sıkça sorulan sorular
- Doğal çıkarım ile sekant hesabı arasındaki fark nedir?
- Doğal çıkarım, varsayımlar bağlamındaki formüllerle çalışır ve gayri resmi kanıta yakından uyan eleme kurallarını kullanır. Sekant hesabı ise açık gerektirmelerle çalışır ve eleme kurallarını sol-giriş kurallarıyla değiştirir; bu format, kesim-elemesini ve alt formül özelliğini şeffaf hale getirmektedir.
- Normalleştirme neden önemlidir?
- Normal bir kanıt, dolambaç içermez ve alt formül özelliğine sahiptir; bu nedenle içindeki her formül, sonucun veya öncüllerin bir alt formülüdür. Bu durum, kanıtların şeklini kısıtlar, tutarlılık sonuçları verir ve kanıtlar-programlar yazışması aracılığıyla bir programı bir değere değerlendirmeye karşılık gelmektedir.