Kanıtlar ve anlamsal tablolar

1. Kanıt nedir

Bir argüman, bir sonucun birtakım öncüllerden çıktığı iddiasıdır. Kanıt ise bu iddiayı karara bağlayan şeydir: herkesin satır satır okuyup onaylayabileceği, sizin sözünüze güvenmeyi gerektirmeyen sonlu ve denetlenebilir bir nesne. Kanıtın değeri ikna etmesinde değildir - iyi bir konuşma da ikna eder - her adımının başka türlü olamayacak olmasındadır.

Bu, kulağa geldiğinden daha katı bir taleptir. «Yağmur yağıyor, öyleyse yer ıslaktır» demek makuldür, ama bu, yağmur ve yer hakkında bildiklerinize yaslanır. Biçimsel mantık bunu bir kenara koyar ve daha dar bir soru sorar: yalnızca cümlelerin biçimine bakıldığında, öncüllerin doğru ve sonucun yanlış olmasının herhangi bir yolu var mıdır? Yoksa argüman geçerlidir ve kanıt, neden böyle bir yol bulunmadığının kaydıdır.

Bu rehber, o kaydı üretmenin bir yolunu anlatır: doğruluk ağaçları da denen anlamsal tablolar yöntemini. Hesap makinesine bir argüman yazdığınızda bu sitenin kullandığı yöntem budur; bir kez izledikten sonra bir argümanı kâğıt üzerinde yalnızca bir kalemle denetleyebilirsiniz.

2. Geçerli - ve bunu nereden bilirsiniz

Bir argümanı gerektirme işaretiyle yazın: öncüller solda, sonuç sağda. p → q, ¬q ⊨ ¬p iddiası, bir koşullu önerme ile ardbileşeninin değillemesinden önbileşeninin değillemesinin çıktığını söyler. Gerektirme işareti bir bağlaç daha değildir. İki yanındaki formüller hakkında bir iddiadır ve ya doğrudur ya da yanlış.

Geçerliliğin tanımı, onu sınamanın bir yolunu doğrudan gösterir: değişkenlere doğru ve yanlış atamalarının hepsini gözden geçirin ve içlerinden birinin tüm öncülleri doğru, sonucu yanlış yapıp yapmadığına bakın. Doğruluk tablosunun yaptığı budur ve iki ya da üç değişken için gayet iyi iş görür. Sorun şu ki tablo 2ⁿ ile büyür. On değişken bin satır ister, yirmi değişken bir milyon; üstelik tablo hangi satırların önemli olduğu konusunda hiçbir şey söylemez.

Bir tablo aynı soruya öbür uçtan saldırır. Her olasılığı sıralayıp içlerinden kötü olanı aramak yerine, kötü bir olasılığın var olduğunu varsayar ve onu kurmaya çalışır. Girişim izleyebileceği her yolda çelişkiyle çöküyorsa böyle bir atama yoktur ve argüman geçerlidir. Girişim başarıya ulaşırsa kurulan şey, doğrudan okuyabileceğiniz bir karşı örnektir.

3. Tablo yöntemi

Bir tablo, işaretli formüllerden oluşan bir ağaçtır. Her satır, önünde bir T ya da bir F bulunan bir formüldür ve işaret, dalın o formül hakkında ne varsaydığını söyler: doğruluk değerinin ne olduğunu değil, argümanın çökmesi için ne olması gerektiğini. Yöntemin tamamı dört adımdır:

1. Her öncülü bir T ile yazın. Argümanın bütün öncüllerinin geçerli olduğunu varsayıyorsunuz.
2. Sonucu bir F ile yazın. Buna rağmen çöktüğünü varsayıyorsunuz - çürütmeye çalıştığınız varsayım budur.
3. Henüz atom olmayan herhangi bir satırı alın ve ana bağlacı ile işareti için geçerli kuralı uygulayın; kuralın ürettiğini, o satırdan geçen her dalın sonuna ekleyin.
4. Bir dal, aynı A formülü için hem T A hem de F A taşır taşımaz onu kapatın. Bütün dallar kapandığında ya da ayrıştırılacak satır kalmadığında durun.

Bu döngüde ne beceri ne de bir strateji seçimi gerekir. Her satırın tam olarak bir kuralı vardır ve kuralları hangi sırayla uygularsanız uygulayın sonuç aynıdır - bu yüzden işi bir makine yapabilir ve bu yüzden yaptığında sonucuna güvenebilirsiniz.

4. Kurallar

Her bağlaç için her işaret altında bir kural vardır - toplam on. İki türe ayrılırlar ve bu türler arasındaki fark, bir tablonun neden liste değil de ağaç olduğunun bütün nedenidir. Bir α kuralı birkaç şeyin birlikte geçerli olması gerektiğini söyler, dolayısıyla sonuçlarını dal boyunca alt alta yığar. Bir β kuralı iki şeyden birinin geçerli olması gerektiğini söyler, dolayısıyla dalı ikiye ayırır ve her durumun kendi yolundan gitmesine izin verir.

Her kural, bağlacının doğruluk koşulunun tersten okunmasından ibarettir. Bir tümel evetleme ancak iki yanı da doğruysa doğrudur, bu yüzden T (A ∧ B) hem T A hem T B'yi yığar. Bir tümel evetleme en az bir yanı yanlışsa yanlıştır, ama formül hangisi olduğunu söylemez, bu yüzden F (A ∧ B) ikisini de denemek zorundadır: dallanır. Aynı asimetri tikel evetlemede ters yönde işler ve yanlış bir koşullu önerme, önbileşenin geçerli olup ardbileşenin çöktüğü anlamına gelir - bir gerektirmenin kırıldığı tek durum.

Kuralların asla yapmadığı şeye dikkat edin: asla formül uydurmazlar. Bir kuralın ürettiği her şey, geldiği satırın bir parçasıdır. Bu özellik - altformül özelliği - yöntemi sonlu kılan şeydir ve aşağıda ona geri döneceğiz.

5. Bir dalı kapatmak

Bir dal tek bir akıl yürütme çizgisidir: kökten bir yaprağa kadar okuyun, elinizde eksiksiz bir varsayımlar kümesi olur. Bir dal, bu varsayımlar açıkça birbiriyle çeliştiğinde, yani aynı formül için hem T A hem F A taşıdığında kapanır. A'nın ne kadar karmaşık olduğu ya da iki satırın birbirinden ne kadar uzak olduğu fark etmez - bir dal bir formülün hem doğru hem yanlış olmasını gerektiriyorsa onu hiçbir şey karşılamaz.

Kapanan dalı × ile işaretleyin, onu kapatan iki satırı yazın ve üzerinde çalışmayı bırakın. Zaten olanaksız olan bir varsayımdan öğrenilecek başka bir şey yoktur.

Bütün dallar kapandığında tablo kapanmıştır ve kanıt budur. Başladığınız varsayımın - bütün öncüller doğru, sonuç yanlış - izleyebileceği her yolda çelişkiye vardığını gösterir. Geriye yol kalmadığına göre böyle bir atama yoktur ve argüman geçerlidir. Bu, hiçbir durumun gözden kaçırılamayacağı biçimde serilmiş bir olmayana ergi kanıtıdır.

6. Satır satır bir kanıt

Modus tollens'i ele alalım: p → q, ¬q ⊨ ¬p. 1. ve 2. satırlar, doğru varsayılan öncüllerdir. 3. satır, yanlış varsayılan sonuçtur; sonuç ¬p olduğuna göre onu yanlış varsaymak p'yi doğru varsaymaktır ve bunu 5. satır kaydeder. 4. satır, 2. satıra uygulanan değilleme kuralından gelir: ¬q doğruysa q yanlıştır. 1. satırdaki koşullu önerme, bağlacı kalan tek satırdır ve bir β kuralıdır, dolayısıyla ağaç ikiye ayrılır:

Soldaki dal, koşullu önermenin önbileşeni çöktüğü için geçerli olduğunu varsayar - ama 5. satırda p zaten doğrudur, dolayısıyla dal kendisiyle çelişir ve kapanır. Sağdaki dal, ardbileşeni doğru olduğu için geçerli olduğunu varsayar - ama 4. satırda q zaten yanlıştır, dolayısıyla o da kapanır.

Her iki dal da kapandı, öyleyse ¬p yanlışken p → q ve ¬q'yu doğru yapmanın hiçbir yolu yok. Argüman geçerlidir ve gerekçesi ağacın kendisidir. Kanıtın yağmurdan, yerden ya da p ile q'nun neyi temsil ettiğinden hiç söz etmediğine dikkat edin. Buna gereği yoktu.

7. Bir dal açık kaldığında

Her argüman geçerli değildir ve yöntem asıl burada değerini gösterir. Bir dalı, üzerinde ayrıştırılabilecek hiçbir şey kalmayana dek - yalnızca atomlar ve değillenmiş atomlar kalana dek - işlerseniz ve dal yine de kapanmamışsa, o dal doymuş ve açıktır. Erken bıraktığınız için kapanmamış değildir; denenecek başka bir şey yoktur.

Açık bir dal, «geçersiz» hükmünden fazlasıdır. Atomlarının işaretlerini okuyun ve elinizde bir atama olur: T ile işaretli her atom doğru, F ile işaretli her atom yanlıştır. Bu atama bütün öncülleri doğru, sonucu yanlış yapar; karşı örnek dediğimiz tam olarak budur. Mantıkçılar buna karşı model der ve bu, «neden olmasın?» sorusuna somut bir yanıttır, bir ret değil.

Ardbileşeni olumlama, p → q, q ⊨ p, ders kitabı örneğidir. Tablosu, p yanlış ve q doğruyken bir dalı açık bırakır - koşullu önermenin geçerli olduğu, ardbileşeninin de geçerli olduğu, buna karşın önbileşenin geçerli olmadığı bir durum. Bu tek atama argümanı kendi başına çürütür.

8. Neden her zaman biter

Her kural bir formülü kendi altformülleriyle değiştirir ve her altformül, geldiği formülden kesinlikle daha kısadır. Dolayısıyla hiçbir dal sonsuza dek büyüyemez: her adım, özgün argümanın parçalarından oluşan sonlu bir merdivenden aşağı iner ve merdivenin bir dibi vardır. Eninde sonunda bir daldaki her satır bir atom ya da bir atomun değillemesi olur ve yapılacak başka bir şey kalmaz.

Bu gerçek bir güvencedir, bir umut değil. Yöntemin önermeler mantığı için bir karar yordamı olduğu anlamına gelir: hangi argümana uygularsanız uygulayın duracaktır - ya kapalı bir ağaçla ya da açık bir dalla, asla omuz silkerek değil. Bu sitedeki kanıtlayıcı bunun üstüne bir düğüm bütçesi uygular, ama yalnızca patolojik bir formülün tarayıcı sekmesini tüketmesine karşı bir önlem olarak; matematiğin böyle bir sınıra ihtiyacı yoktur.

9. Diğer kanıt sistemleri

Tablolar birkaç kanıt sisteminden biridir ve çürütme biçiminde olanıdır: başarısızlığı eleyerek çalışırlar. Doğal çıkarım tersini yapar ve sonucu öncüllerden ileriye doğru kurar; modus ponens ve koşullu kanıt gibi kurallarla ilerler ve bir matematikçinin düzyazıyla nasıl akıl yürüttüğüne çok daha çok benzer. Doğal çıkarımla yazılmış bir kanıt genellikle daha kısadır; onu bulmak genellikle daha çok buluş gerektirir.

Ardışım hesabı gerektirme işaretinin kendisini biçimselleştirir ve gerektirme iddialarını birer nesne olarak ele alır; bu da onu kanıtlar hakkında bir şey kanıtlamak istendiğinde tercih edilen araç yapar. Çözümleme her şeyi tümcelere ve tek bir kurala indirger; okuması gösterişsiz, çalıştırması son derece hızlıdır - otomatik kanıtlayıcıların ve SAT çözücülerin çoğu bunun üzerine kuruludur.

Hepsi hangi önermesel argümanların geçerli olduğunda anlaşır; bir kanıtın neye benzediğinde ve neyin kolay bulunduğunda ayrışırlar. Öğrenmek için en dostane olanı tablolardır, çünkü başarısız bir kanıt burada çıkmaz sokak değildir - size karşı örneği verir.

10. Alıştırma

Yöntemi öğrenmenin en hızlı yolu onu çalıştırmaktır. Hesap makinesine ⊨, ⊢ ya da |= ile bir argüman yazın; tablo doğruluk tablosunun yanında çizilir, böylece ağacı satırlarla karşılaştırabilirsiniz. Sonra bakmadan önce birkaç kanıtı kâğıt üzerinde çalışın.