Karar verilebilirlik

Açılış sahnesi

Tolga, katalog programına yeni bir görev veriyor: bir formül verildiğinde, onun geçerli olup olmadığını bulmak. Program, bütün olası kanıtları kısa olandan uzun olana doğru sırayla üretiyor ve her birinin verilen formülle bitip bitmediğini denetliyor. İlk formül için, birkaç saniye sonra bir kanıt buluyor ve duruyor: formül geçerliydi. İkinci formül için program saatlerce çalışıyor. Hiçbir kanıt bulamıyor, ama durmuyor da.

Tolga, ekrana bakarak ne düşünmesi gerektiğini bilmiyor. Formül geçersiz miydi, yoksa kanıtı henüz sıraya gelmemiş miydi? Selin, önermeler mantığında böyle bir belirsizlik olmadığını hatırlatıyor: doğruluk tablosu her formül için sonlu sayıda satırdan sonra bir cevap veriyordu. Kerem, yüklemler mantığı için de böyle bir tablonun neden bulunmadığını soruyor. Lina, katalogdaki bazı cümlelerin yalnızca nüshaların özelliklerinden, bazılarının ise nüshalar arasındaki ilişkilerden söz ettiğini ve bunun bir fark yaratıp yaratmadığını merak ediyor. Barış, bir işlemin hukuka uygun olup olmadığını her durumda mekanik olarak belirleyen bir yöntemin mümkün olup olmadığını düşünüyor. Defne ise kurallarının hepsi basit koşullardan oluşan bir tanı kılavuzunun, bu bakımdan yüklemler mantığından farklı olup olmadığını soruyor. Bu ders, Mantık ve Akıl Yürütme programının Metalojik ve Hesaplanabilirlik kursunda, bir formülün geçerli olup olmadığını sonlu sayıda adımda her zaman belirleyen mekanik bir yöntemin var olup olmadığını, önermeler mantığı ile yüklemler mantığının bu bakımdan neden ayrıldığını ve tamlığın bu soruya neden tek başına bir cevap vermediğini soruyor.

Bu derste ne olacak

Önce bu dersin yerini belirleyelim. Tamlık dersi, yüklemler mantığında geçerli olan her formülün bir kanıtı bulunduğunu ve bu teoremin nasıl kanıtlandığını inceledi. Programın Yüklemler Mantığı kursunda ise Church'ün yüklemler mantığının karar problemini olumsuz cevaplayan 1936 tarihli notu ve karar verilemezlik kavramı, Klasik Olmayan Mantıklar kursunda da sezgici mantıktaki karar verilebilir önerme kavramı tanıtılmıştı. Bu ders, Metateori modülünü kapatıyor: karar verilebilirliği, seslilik ve tamlıkla birlikte bir sistemin üçüncü temel özelliği olarak ele alıyor ve tamlıktan neden ayrı olduğunu gösteriyor.

Sonra üç kaynağa bakacağız. Heinrich Behmann, 1922'de yayımladığı Mantık Cebirine, Özellikle Karar Problemine Katkılar makalesinde, yalnızca tek yerli yüklemler içeren yüklemler mantığı için bir karar yöntemi verir. Alan Turing, 1936'da yayımladığı Hesaplanabilir Sayılar ve Karar Problemine Bir Uygulama makalesinde, mekanik bir yöntemin ne olduğunu kesin biçimde tanımlar ve bazı soruların hiçbir mekanik yöntemle karara bağlanamayacağını gösterir. Alfred Tarski ise 1951'de yayımladığı Temel Cebir ve Geometri İçin Bir Karar Yöntemi kitabında, gerçek sayılar hakkındaki temel cebir cümlelerinin karar verilebilir olduğunu kanıtlar.

Ardından üç itirazı tartacağız: karar verilemezlik sonuçlarının, mekanik yöntemin kanıtlanmamış bir tanımına dayandığı, pratikte işe yarayan kanıt programlarının bu sonuçları önemsiz kıldığı ve karar verilemezliğin yüklemler mantığını kullanışsız hâle getirdiği itirazları.

Sonda, bir sorular sınıfının karar verilebilirliğini değerlendirmenin dört adımını göstereceğiz: sorular sınıfını açıkça tanımlamak, bir karar yöntemi aramak, yöntem yoksa bir yarı karar yöntemi bulunup bulunmadığını sormak ve karar verilebilirliğin pratikte uygulanabilirlik anlamına gelip gelmediğini ayırmak.

Merkez soru

Sorumuz şu: bir formülün geçerli olup olmadığını sonlu sayıda adımda her zaman belirleyen mekanik bir yöntem var mıdır ve tamlık bu soruya neden tek başına bir cevap vermez?

Ölçülü iddiam şu: bir sorular sınıfı, her soruya sonlu sayıda adımda doğru cevabı veren mekanik bir yöntem varsa karar verilebilirdir. Önermeler mantığı karar verilebilirdir. Doğruluk tablosu, bir formülün bütün olası değerlemelerini sonlu bir listede sınar. Yüklemler mantığı ise, Church'ün ve Turing'in 1936'da birbirinden bağımsız olarak gösterdiği gibi, karar verilebilir değildir. Tamlık bu sonuçla çelişmez, ama yalnızca daha zayıf bir şey verir. Geçerli her formülün bir kanıtı olduğu için, bütün kanıtları sırayla üreten bir program, geçerli bir formüle eninde sonunda bir "evet" cevabı verir. Ama geçersiz bir formül için hiçbir zaman "hayır" demez; yalnızca aramaya devam eder. Bu özelliğe yarı karar verilebilirlik denir. Turing'in katkısı, mekanik yöntemin kesin bir tanımını vermesi ve bu tanımla, bazı soruların hiçbir yöntemle karara bağlanamayacağını, bir yöntemin kendi davranışı hakkındaki sorulara uygulanmasından doğan bir çelişkiyle göstermesiydi. Karar verilemezlik yüklemler mantığının bütününe aittir, her parçasına değil. Behmann'ın gösterdiği gibi, yalnızca tek yerli yüklemler içeren parça karar verilebilirdir. Tarski'nin gösterdiği gibi, bazı zengin matematik kuramları da karar verilebilirdir. Karar verilebilirlik, bir sorunun ilke olarak mekanik biçimde cevaplanabildiğini söyler. Bu cevabın makul bir sürede bulunabildiğini söylemez.

Sıfır noktası

Bir öğrenci doğruluk tablosunu öğrendiğinde, mantığın mekanik olduğunu düşünür. Bir formül verilir, tablosu kurulur, satırlar doldurulur ve cevap okunur. Hiçbir yaratıcılık, hiçbir sezgi gerekmez. Bu, önermeler mantığı için doğrudur. Bir formül sonlu sayıda yalın önerme içerir ve bu önermelerin doğruluk değerlerinin bütün birleşimleri sonlu bir listede yazılabilir.

Yüklemler mantığında bu yöntem çöker. Bir formülün her modelde doğru olup olmadığını sormak, sonsuz sayıda modele, hatta sonsuz büyüklükte modellere bakmayı gerektirir. Bu modellerin bir listesi yapılamaz. Tamlık teoremi başka bir yol açar gibi görünür: modellere bakmak yerine kanıtları aramak. Kanıtlar sonlu dizilerdir ve sırayla üretilebilir.

Ama bu yol yalnızca bir yöne işler. Formül geçerliyse, kanıtı bir gün bulunur. Formül geçersizse, arama sonsuza kadar sürer ve hiçbir an, aramayı bırakıp "geçersiz" demenin güvenli olduğunu göstermez. Karar verilebilirlik, iki yönde de sonlu bir cevap ister. Tamlık yalnızca bir yönü güvence altına alır.

Görüşler ve pozisyonlar

Karar verilemezlik sonuçlarının anlamı konusunda üç görüş var.

Birinci görüş, sınır görüşüdür. Buna göre karar verilemezlik, mekanik akıl yürütmenin aşılamaz bir sınırını gösterir. Bazı mantık soruları, hiçbir algoritma tarafından her durumda cevaplanamaz ve bu, mantığın mekanikleştirilmesi projesinin ilke düzeyinde bir sınırıdır.

İkinci görüş, zihin görüşüdür. Buna göre karar verilemezlik, makinelerin yapamadığını insan zihninin yapabildiğini gösterir. Matematikçiler, hiçbir makinenin karara bağlayamadığı soruları sezgiyle cevaplar. Bu yüzden insan akıl yürütmesi mekanik değildir.

Üçüncü görüş, harita görüşüdür. Buna göre karar verilemezlik sonuçları, mantığın hangi bölgelerinin mekanik olarak işlenebildiğini gösteren bir haritadır. Yüklemler mantığının bütünü karar verilemezdir, ama geniş ve önemli parçaları karar verilebilirdir. Soru, bir problemin hangi bölgeye düştüğünü belirlemektir.

Bu ders üçüncü görüşü temel alır ve birinci görüşün, karar verilemezliğin ilke düzeyinde bir sınır olduğu gözlemini kabul eder. Birinci görüş, bu sınırın gerçek olduğunu doğru görür. Ama Behmann'ın ve Tarski'nin sonuçlarında görüldüğü gibi, sınırın mantığın bütün bölgelerini kapsamadığını hesaba katmaz. İkinci görüş, karar verilemezliğin insan zihni hakkında bir şey söylediğini varsayar. Ama bir matematikçinin bazı karar verilemez sorulara cevap bulması, her soruya cevap bulabildiğini göstermez. Üçüncü görüş, sınırı kabul eder ve onun nereden geçtiğini sorar.

Argümanın yapısı

Bir sorular sınıfının karar verilebilirliğini değerlendirmek için dört adım izlenebilir.

Birinci adım, sorular sınıfını açıkça tanımlamaktır. Değerlendiren, hangi formüllerin ya da soruların sınıfa girdiğini ve her soruya hangi cevabın doğru sayılacağını kesin olarak yazar.

İkinci adım, bir karar yöntemi aramaktır. Değerlendiren, sınıftaki her soruya sonlu sayıda adımda doğru cevabı veren mekanik bir yöntem arar. Doğruluk tablosu ya da niceleyicileri ortadan kaldırma gibi bilinen yöntemlerin uygulanıp uygulanamayacağını sorar.

Üçüncü adım, yöntem yoksa bir yarı karar yöntemi bulunup bulunmadığını sormaktır. Değerlendiren, en azından "evet" cevaplarını her zaman sonlu bir sürede veren, ama "hayır" cevaplarında durmayabilen bir yöntemin var olup olmadığını belirler.

Dördüncü adım, karar verilebilirliğin pratikte uygulanabilirlik anlamına gelip gelmediğini ayırmaktır. Değerlendiren, bir karar yöntemi varsa, onun makul bir sürede sonuç verip vermediğini ayrıca sorar.

En güçlü itiraz

Bu yaklaşıma üç yönden ciddi itiraz yapılabilir.

Karar verilebilirliği ciddiye alan düşünce şu cevabı verebilir. Bir sorular sınıfı, her soruya sonlu sayıda adımda doğru cevabı veren mekanik bir yöntem varsa karar verilebilirdir. Selin'in sekiz satırında görüldüğü gibi, önermeler mantığı doğruluk tablosuyla karar verilebilirdir. Yüklemler mantığı ise, Church'ün ve Turing'in gösterdiği gibi, karar verilebilir değildir. Turing, mekanik yöntemin kesin bir tanımını verdi ve Kerem'in denetçi programında görüldüğü gibi, bir yöntemi kendi üzerine uygulayan bir çelişki argümanıyla bazı soruların hiçbir yöntemle karara bağlanamayacağını gösterdi. Tolga'nın durmayan programında görüldüğü gibi, tamlık yalnızca yarı karar verilebilirliği verir: geçerli formüllere "evet" denir, geçersiz olanlarda arama durmayabilir. Karar verilemezlik yüklemler mantığının bütününe aittir. Behmann'ın gösterdiği ve Lina'nın özellik cümlelerinde görülen tek yerli parça ile Tarski'nin gösterdiği temel cebir karar verilebilirdir. Barış'ın süre hesabında görüldüğü gibi, karar verilemezlik kesin olarak tanımlanmış soru sınıflarının bir özelliğidir. Selin'in ve Defne'nin durumlarında görüldüğü gibi, karar verilebilirlik de pratikte uygulanabilirlik anlamına gelmez.

Açık kalan sorular

Kerem'in denetçi programı, karar verilemezliğin, bir yöntemin kendi davranışı hakkındaki bir soruya uygulanmasından doğduğunu gösterdi. Bu yapı yalancı paradoksuna benziyordu. Kendi kendine gönderim, mantıktaki bütün sınır sonuçlarının ortak kaynağı mıdır? Kendi kendine gönderimi dışarıda bırakan bir sistem, bu sınırlardan kurtulabilir mi?

Lina'nın özellik cümleleri, karar verilebilirliğin ilişkilerle birlikte kaybolduğunu düşündürdü. Karar verilebilir parça ile karar verilemez bütün arasındaki sınır tam olarak nereden geçer? Hangi tür ilişkiler karar verilebilirliği bozar, hangileri bozmaz?

Selin'in sekiz satırı, karar verilebilir bir sorunun bile pratikte çözülemeyecek kadar uzun sürebileceğini gösterdi. Bir sorunun ilke olarak çözülebilmesi ile makul bir sürede çözülebilmesi arasındaki fark, mantığın bir konusu mudur, yoksa yalnızca bilgisayar biliminin mi?

Yaygın hatalar

Kendin dene

Aklında kalsın

Beş cümlede dersin iskeleti.

Bir sorular sınıfı, her soruya sonlu sayıda adımda doğru cevabı veren mekanik bir yöntem varsa karar verilebilirdir; önermeler mantığı doğruluk tablosuyla karar verilebilirdir, yüklemler mantığı ise Church'ün ve Turing'in gösterdiği gibi karar verilebilir değildir.

Behmann'ın 1922 tarihli makalesi tek yerli yüklemlerle sınırlı parçanın karar verilebilir olduğunu, Turing'in 1936 tarihli makalesi mekanik yöntemin kesin tanımını verip bazı soruların hiçbir yöntemle karara bağlanamayacağını, Tarski'nin 1951 tarihli kitabı ise gerçek sayıların temel cebirinin karar verilebilir olduğunu gösterdi.

Bir sorular sınıfının karar verilebilirliği dört adımla değerlendirilir: sınıfı açıkça tanımlamak, bir karar yöntemi aramak, yöntem yoksa bir yarı karar yöntemi bulunup bulunmadığını sormak ve karar verilebilirliğin pratikte uygulanabilirlik anlamına gelip gelmediğini ayırmak.

Karar verilemezliğin kanıtlanmamış bir tanıma dayandığı, pratikteki kanıt programlarının onu önemsiz kıldığı ve yüklemler mantığını kullanışsız hâle getirdiği itirazları, bağımsız tanımların örtüşmesinin tezi desteklediğini, karar verilemezliğin bir başarısızlığı değil bir güvencenin yokluğunu bildirdiğini ve karar verilebilir parçaların ile yarı karar verilebilirliğin mantığı kullanışlı tuttuğunu gördüğümüzde cevaplanabilir.

Bu yüzden tamlık geçerli her formülün bir kanıtı olduğunu söyler, ama geçersiz bir formülün geçersiz olduğunu her zaman bildiren bir yöntem vermez; karar verilebilirlik, seslilik ve tamlıktan ayrı, üçüncü bir soru olarak kalır.

Sonraki derse köprü

Bu modül, bir sistemi bir nesne olarak incelemenin temel kavramlarını kurdu: nesne dili ve üst dil, biçimsel sistem, seslilik, tamlık ve karar verilebilirlik. Tamlık teoremi, bu kavramların merkezinde duruyordu. Ama Kerem, teoremi şimdiye kadar hep sonuçlarıyla, yani neyi güvence altına aldığıyla konuştuklarını fark ediyor. Teoremin yüklemler mantığına özgü olan içeriğine, bu mantığın niceleyicilerinin ve modellerinin teoremde nasıl bir rol oynadığına henüz bakmamışlardı.

Tolga, Henkin'in kanıtının, dile tanık sabitleri eklediğini ve bunun tam da niceleyicilerden kaynaklandığını hatırlatıyor: "bir nesne vardır" diyen bir cümle, bir tanık adı istiyordu. Selin, Gödel'in kendi kanıtının Henkin'inkinden farklı bir yol izlediğini duyduğunu söylüyor. Lina, teoremin sonsuz modeller hakkında ne söylediğini, bir cümlenin yalnızca sonsuz bir modelde doğru olabilmesinin teoremle nasıl bir ilişkisi olduğunu soruyor.

Bir sonraki ders bu soruya dönüyor. Tamlık teoremi dersi, birinci derece mantığın tamlık teoreminin bu mantığın niceleyicilerine ve modellerine özgü içeriğini, Gödel'in kanıtının izlediği yolu ve teoremin birinci derece mantığın modelleri hakkında, özellikle sonsuz modeller hakkında, hangi sonuçlar doğurduğunu soruyor.