Çıkarım kuralı - Rule of inference

Gelen mantık felsefesi , bir çıkarım üstünlüğü , kesmesi kuralı veya bağlanma kuralıyla a, mantıksal bir şekilde , bina alır bunların analiz bir fonksiyonu kapsayan sözdizimini bir sonuç (veya eden ve sonuçlar ). Örneğin, modus ponens adı verilen çıkarım kuralı , biri "Eğer p ise q ise" ve diğeri "p" biçiminde olmak üzere iki öncül alır ve "q" sonucunu döndürür. Kural, klasik mantığın semantiğine (ve ayrıca klasik olmayan birçok mantığın semantiğine ) göre geçerlidir, şu anlamda, eğer öncüller doğruysa (bir yorum altında), o zaman sonuç da doğrudur.

Tipik olarak, bir çıkarım kuralı, anlamsal bir özellik olan gerçeği korur. Çok değerli mantıkta , genel bir atamayı korur. Ancak bir çıkarım kuralının eylemi tamamen sözdizimseldir ve herhangi bir anlamsal özelliği koruması gerekmez: formül kümelerinden formüllere kadar herhangi bir işlev, bir çıkarım kuralı olarak sayılır. Genellikle yalnızca özyinelemeli kurallar önemlidir; yani, verilen herhangi bir formülün, kurala göre belirli bir formüller dizisinin sonucu olup olmadığını belirlemek için etkili bir prosedür olacak şekilde kurallar. Bu anlamda etkili olmayan bir kural örneği, sonsuz ω kuralıdır .

Önerme mantığındaki popüler çıkarım kuralları arasında modus ponens , modus tollens ve kontrapozisyon bulunur . Birinci dereceden yüklem mantığı , mantıksal niceleyicilerle başa çıkmak için çıkarım kurallarını kullanır .

Standart biçim

In biçimsel mantık (ve birçok ilgili alanlarda), çıkarsama kuralları genellikle aşağıdaki standart formda verilmiştir:

  Öncül#1
  Öncül #2
        ...
  Öncül#n   
  Sonuç

Bu ifade, herhangi bir mantıksal türetme sırasında verilen öncüller elde edildiğinde, belirtilen sonucun da kesin olarak alınabileceğini belirtir. Hem öncülleri hem de sonuçları tanımlamak için kullanılan kesin biçimsel dil, türetmelerin gerçek bağlamına bağlıdır. Basit bir durumda, aşağıdaki gibi mantıksal formüller kullanılabilir:

${\ Displaystyle A\'dan B'ye}$

${\displaystyle {\altı çizili {A\dörtlü \dörtlü }}\,\!}$

${\görüntüleme stili B\!}$

Bu, önermeler mantığının modus ponens kuralıdır . Çıkarım kuralları genellikle formüle edilir şema kullanılarak metavariables . Yukarıdaki kuralda (şemada), A ve B meta değişkenleri, sonsuz bir çıkarım kuralları kümesi oluşturmak için evrenin herhangi bir öğesine (veya bazen, geleneksel olarak, önermeler gibi sınırlı bir alt kümeye ) örneklenebilir .

Bir ispat sistemi, türetme olarak da adlandırılan ispatları oluşturmak için birbirine zincirlenmiş bir dizi kuraldan oluşur . Herhangi bir türetmenin yalnızca bir nihai sonucu vardır, bu da kanıtlanan veya türetilen ifadedir. Tesislerinde türetmedeki tatminsiz bırakılırsa, o zaman türetme bir bir kanıtıdır varsayımsal açıklamada: " eğer tesislerinde, tutun sonra sonuca tutar."

Örnek: İki önerme mantığı için Hilbert sistemleri

Bir de Hilbert sisteminde , bina ve çıkarım kurallarının sonucu genellikle metavariables kullanan bazı dilin formülleri, basitçe bulunmaktadır. Sunumun grafiksel kompaktlığı ve aksiyomlar ile çıkarsama kuralları arasındaki ayrımı vurgulamak için, bu bölüm , kuralların dikey bir sunumu yerine sıralı gösterimi ( ) kullanır. Bu notasyonda, ${\görüntüleme stili \vdash }$

${\displaystyle {\begin{array}{c}{\text{Öncül }}1\\{\text{Öncül }}2\\\hline {\text{Sonuç}}\end{dizi}}}$

olarak yazılır . ${\displaystyle ({\text{Öncül }}1),({\text{Öncül }}2)\vdash ({\text{Sonuç}})}$

Klasik önerme mantığı için biçimsel dil, sadece olumsuzlama (¬), ima (→) ve önerme sembolleri kullanılarak ifade edilebilir. Üç aksiyom şeması ve bir çıkarım kuralı ( modus ponens ) içeren iyi bilinen bir aksiyomlaştırma şöyledir:

(CA1) ⊢ A → (B → A)

(CA2) ⊢ (A → (B → C)) → ((A → B) → (A → C))

(CA3) ⊢ (¬A → ¬B) → (B → A)

(MP)  A, A → B ⊢ B

Bu durumda iki çıkarım kavramına sahip olmak gereksiz görünebilir, ⊢ ve →. Klasik önerme mantığında bunlar gerçekten de örtüşürler; kesinti teoremi devletler o A ⊢ B ancak ve ancak ⊢ eğer bir → B . Bununla birlikte, bu durumda bile vurgulanmaya değer bir ayrım vardır: ilk gösterim, bir tümdengelimi , yani tümcelerden cümlelere geçme etkinliğini tanımlar , oysa A → B , bu durumda mantıksal bir bağlaçla yapılmış bir formüldür , ima. Bir çıkarım kuralı olmadan ( bu durumda modus ponens gibi ), hiçbir kesinti veya çıkarım yoktur. Bu nokta, Lewis Carroll'un " Kaplumbağa Akhilleus'a Ne Dedi " adlı diyaloğunda ve daha sonra Bertrand Russell ve Peter Winch'in diyalogda ortaya çıkan paradoksu çözme girişimlerinde gösterilmektedir .

Bazı klasik olmayan mantıklar için tümdengelim teoremi geçerli değildir. Örneğin, üç değerli mantık ait Lukasiewicz olarak axiomatized edilebilir:

(CA1) ⊢ A → (B → A)

(LA2) ⊢ (A → B) → ((B → C) → (A → C))

(CA3) ⊢ (¬A → ¬B) → (B → A)

(LA4) ⊢ ((A → ¬A) → A) → A

(MP)  A, A → B ⊢ B

Bu dizi, aksiyom 2'deki değişiklik ve aksiyom 4'ün eklenmesiyle klasik mantıktan farklıdır. Klasik tümdengelim teoremi bu mantık için geçerli değildir, ancak değiştirilmiş bir form geçerlidir, yani A ⊢ B eğer ve ancak ve ancak ⊢ A → ( A ise) → B ).

Kabul edilebilirlik ve türetilebilirlik

Bir dizi kuralda, bir çıkarım kuralı, kabul edilebilir veya türetilebilir olması anlamında gereksiz olabilir . Türetilebilir bir kural, sonucu diğer kurallar kullanılarak öncüllerinden çıkarılabilen bir kuraldır. Kabul edilebilir bir kural, öncüllerin geçerli olduğu her durumda sonucu geçerli olan kuraldır. Tüm türetilebilir kurallar kabul edilebilir. Farkı anlamak için, doğal sayıları tanımlamak için aşağıdaki kurallar dizisini göz önünde bulundurun ( yargı , bunun doğal bir sayı olduğu gerçeğini ortaya koymaktadır ): ${\displaystyle n\,\,{\mathsf {nat}}}$${\görüntüleme stili n}$

${\displaystyle {\begin{matrix}{\begin{array}{c}\\\hline {\mathbf {0} \,\,{\mathsf {nat}}}\end{array}}&{\begin {array}{c}{n\,\,{\mathsf {nat}}}\\\hline {\mathbf {s(} n\mathbf {)} \,\,{\mathsf {nat}}}\ bitiş{dizi}}\bitiş{matris}}}$

İlk kural 0'ın bir doğal sayı olduğunu, ikinci kural ise n ise s( n )' nin bir doğal sayı olduğunu belirtir . Bu ispat sisteminde, bir doğal sayının ikinci ardılının da bir doğal sayı olduğunu gösteren aşağıdaki kural türetilebilirdir:

${\displaystyle {\begin{array}{c}{n\,\,{\mathsf {nat}}}\\\hline {\mathbf {s(s(} n\mathbf {))} \,\, {\mathsf {nat}}}\end{dizi}}}$

Türetilmesi, yukarıdaki ardıl kuralın iki kullanımının bileşimidir. Sıfırdan farklı herhangi bir sayı için bir öncünün varlığını iddia etmek için aşağıdaki kural yalnızca kabul edilebilir:

${\displaystyle {\begin{array}{c}{\mathbf {s(} n\mathbf {)} \,\,{\mathsf {nat}}}\\\hline {n\,\,{\mathsf {nat}}}\end{dizi}}}$

Bu, tümevarımla kanıtlanabileceği gibi, doğal sayıların gerçek bir gerçeğidir . (Bu kuralın kabul edilebilir olduğunu kanıtlamak için, öncülün bir türevini varsayın ve onun üzerinde bir türev üretmek için tümevarım yapın .) Bununla birlikte, türetilebilir değildir, çünkü öncülün türetilmesinin yapısına bağlıdır. Bu nedenle, ispat sistemine yapılan eklemelerde türetilebilirlik sabittir, kabul edilebilirlik ise sabit değildir. Farkı görmek için, ispat sistemine aşağıdaki saçma kuralın eklendiğini varsayalım: ${\displaystyle n\,\,{\mathsf {nat}}}$

${\displaystyle {\begin{array}{c}\\\hline {\mathbf {s(-3)} \,\,{\mathsf {nat}}}\end{dizi}}}$

Bu yeni sistemde, çift ardıl kuralı hala türetilebilir. Bununla birlikte, selefi bulma kuralı artık kabul edilemez, çünkü türetmenin bir yolu yoktur . Kabul edilebilirliğin kırılganlığı, kanıtlanma biçiminden gelir: kanıt, öncüllerin türevlerinin yapısı üzerinde tümevarım yapabildiğinden, sistemdeki uzantılar, bu kanıta artık geçerli olmayabilecek yeni durumlar ekler. ${\displaystyle \mathbf {-3} \,\,{\mathsf {nat}}}$

Kabul edilebilir kurallar, bir ispat sisteminin teoremleri olarak düşünülebilir . Örneğin, kesme eliminasyonunun geçerli olduğu ardışık bir hesapta , kesme kuralı kabul edilebilir.

Ayrıca bakınız

• Argümantasyon şeması
• anında çıkarım
• çıkarım itirazı
• düşünce yasası
• Çıkarım kurallarının listesi
• mantıksal gerçek
• yapısal kural

Referanslar