“ rasyonel olacak şekilde a ve b irrasyonel sayıları vardır.” İspatı oldukça kolay görünüyor. sayısını düşünelim. Elimizde iki ihtimal var:

(1) rasyoneldir. Bu durumda olarak seçebiliriz.
(2) irrasyoneldir. Bu durumda ise, , seçeriz ve böylece rasyonel olur.

Aynı problemi şu şekilde de çözebiliriz: olmak üzere, bir rasyonel sayıdır. (Burada, b bir irrayonel sayıdır. Tersine, b bir rasyonel sayı olsaydı, olacak şekilde p ve q tamsayıları olurdu. Buradan, ve böylece olur. Fakat bu bir çelişkidir, çünkü bir çift sayı iken, bir tek sayıdır.)

Yukarıdaki ilk ispat yapıcı olmayan ispat (non-constructive proof) tekniğine bir örnektir. Burada ispatı yaparken elimizde iki ihtimal olduğunu söyleyip, hangisinin doğru olduğu hakkında bir bilgi sunmadan sonuca ulaştık. Bu ispat tekniği karşımıza oldukça sık çıkmıştır. Matematik bölümlerinde, daha ayağımızın tozuyla öğrendiğimiz Ara Değer, Rolle, Ortalama Değer ve Monoton Yakınsaklık Teoremleri bunun en güzel örnekleridir. Örneğin bir polinomun ‘de bir kökü olduğunu gösterirken, belli koşulları kontrol edip, Ara Değer Teoreminden bu koşullar altında bir kök bulmanın mümkün olduğu sonucuna ulaşırız fakat bu kökün ne olduğu açıkça ifade etmeyiz.

İkincisi ispat ise yapıcı ispat (constructive proof) tekniğine bir örnektir. Bunun diğerinden farkı, kabaca, çözümü inşa etmemizdir. Yapıcı ispat, var olduğunu iddia ettiğimiz nesneyi nasıl bulacağımızı bize tarif eder.

Yapıcı olmayan ispatlar seçme prensibinden ve daha da önemlisi ara değeri dışlama (Law of excluded middle-kısaca LEM) kanunundan kaynaklanır. Klasik mantığın temel kurallarından biri olan LEM, bir önermenin ya kendisinin ya da değilinin doğru olduğunu (yani üçüncü bir ihtimalin olmadığını) ifade eder.

Şimdi buradan, Bertrand Russell’ın 1901 yılında keşfettiği meşhur Russell paradoksuna bir geçiş yapıyoruz. , “kendisini içermeyen kümelerin” kümesi olsun. Bu noktada biraz daha açıklama gerekiyor sanırım. Örneğin, 3’ten fazla elemanı olan kümelerin kümesi, (kendisi de 3’ten fazla elemana sahip olacağı için) kendisini içerir. Fakat doğal sayılar kümesi, (kendisi bir doğal sayı olmadığından) kendisini içermez. Aynı şekilde, tüm karelerin kümesi de kendisini içermeyen bir kümedir. Burada paradoksa neden olan soru şudur: Acaba kümesi kendini içerir mi, yoksa içermez mi? Elimizde iki olasılık var:

(1) kendini içerir, yani ‘dir. Bu durumda kümenin tanımı gereği olmalıdır, ki bu bir çelişkidir.
(2) kendini içermez, yani ‘dir. Yine tanım gereği, çelişkisini elde ederiz.

(Matematik sevmeyenler için, bu paradoksun diğer bir versiyonu şöyledir: Diyelim ki, bir berber, yalnızca kendini tıraş etmeyenleri tıraş ediyor, kendini tıraş edenleri tıraş etmiyor. Peki bu berber kendini tıraş eder mi? Soruyu cevaplarken, aynı yukarıda olduğu gibi, önce kendini tıraş eder, daha sonra da etmez deyip, her iki durumda da çelişkiye varıyoruz.)

Burada aslında, “ kümesi kendisini içerir” önermesini ele alıp, “bu önerme ya doğrudur ya da değili doğrudur” yaklaşımıyla ispata başlayıp, sonrasında işin içinden çıkamıyoruz. Belli ki bu önerme, bu yasayı ihlal ediyor. Demek ki LEM aslında vazgeçilemez bir kanun değildir, yani bu yasanın (ya da genel olarak klasik mantık yasalarının) geçerli olmadığı mantık türleri tanımlamak da mümkündür. Bu örnek için, bu kuralı kaldırmak paradoksun ortadan kalkmasına yetmiyor maalesef. Çünkü bu kez de, birbirini olumsuzlayan iki önermenin aynı anda doğru olamayacağını söyleyen çelişki yasası (law of non-contradiction) yolumuza taş koyuyor. Russell bu paradoksu ortadan kaldırmak için, Principia Mathematica‘da tipler kuramını (theory of types) ortaya atmıştır. Burada birkaç kelime ile özetlendiği gibi;

“Tipler kuramı kümeleri derecelendirir. Örneğin, dördüncü dereceden bir kümeyi tanımlamak için ancak birinci, ikinci ve üçüncü dereceden kümeler kullanılabilir. Böylece “tüm kümeler kümesi” diye bir küme matematikte yasaklanmış olur ve Russell’ın paradoksu paradoks olmaktan çıkar. Yani Russell akla gelen her nesnenin küme olmasını yasaklayarak, matematiği değiştirmiş, (şimdilik) çelişkisiz bir matematik yaratmıştır. Ünlü Fransız matematikçisi Poincaré’nin de dediği gibi, kurtlardan korumak için sürünün çevresine bir çit çekilmiştir.”

Konudan konuya atlama uzmanı olarak, Cem Say’ın (şiddetle tavsiye ettiğim) 50 Soruda Yapay Zeka isimli kitabında Principia Mathematica ile ilgili yazdıklarını da eklemeden edemeyeceğim.

Bertrand Russell, matematiğin mantık temeline oturtulması bayrağını Frege’den devraldıktan sonra bu konuda insanüstü bir çaba gösterdi. Russell’ın meslektaşı Alfred North Whitehead’le birlikte bu amaçla yazmaya giriştiği Principia Mathematica, tarihin en zor kitaplarından biridir. Her kavramı, en ama en temel par­çacıklarına ayırıp, hiçbir kuşkuya, Frege’nin düş kırıklığına yol açandaki gibi hiçbir paradoksa meydan vermeyecek şekilde yazma çabası, Whitehead’le Russell’ın yıllarına, neredeyse akıl sağlıklarına ve Russell’ın evliliklerinden birine mal oldu. Çok çetrefilli bir notasyonla yazılan kitabın 1912’de basılan ikinci cildinin 86. sayfasında nihayet 1+1’in 2’ye eşit olduğunun kanıtı tamamlanıyor ve hemen ardından “Yukarıdaki önerme bazen yararlı olur” cümlesi yer alıyordu! Üçüncü ciltten sonra halleri kalmayan ikili, geometrinin temellerini işlemesini öngördükleri dördüncü cildi yazmaktan vazgeçtiler. (Eski bir mantıkçı bilmecesi: “Principia Mathematica’yı kaç kişi okumuştur? Cevap: İki. Russell’ın yazdığı yerleri Russell, Whitehead’inkileri de Whitehead”)

Şimdi asıl meseleye dönüp, yukarıda bahsettiğimiz ara değeri dışlama kanununa ek olarak çifte olumsuzlama elemesi () de çıkarılarak elde edilen sezgisel mantık (Intuitionistic Logic), ya da diğer adıyla Yapıcı Mantığa (Constructive Logic) bir bakalım.

Sezgiselciler, matematiksel bir nesnenin var kabul edilebilmesi için bu nesnenin nasıl inşa edildiğine dair bir kural ya da işlemin ortaya konması gerektiğini savunurlar. Bu görüşü ortaya atan Luitzen Egbertus Jan Brouwer, formalize eden ise Arend Heyting olmuştur. Tabi her yenilikte olduğu gibi bunun da kabul görmesi öyle kolay olmamıştır. Bunu, Brouwer ile David Hilbert arasındaki tartışmada Hilbert’in

“Matematikçiden ara değeri dışlama kanununu almak, astronoma teleskopu ya da boksöre yumruklarını kullanmayı yasaklamakla aynıdır. Varlık ifadelerini ve ara değeri dışlama kanununu yasaklamak, matematik bilimden vazgeçmekle aynı şeydir”

sözlerinden anlamak mümkün. Sezgisel mantık ile, oldukça işe yarayan iki aracı kaybetmiş oluruz; fakat uygulanabilirliğinin fazla olması onu değerli kılar. Elde ettiğimiz yapıcı ispatları birer algoritma olarak kullanmamız mümkündür ve böylece bunları doğrulamak ve belki de daha kapsamlı çözümler üretmek için “kanıt asistanları” kullanma şansımız olur. Mizar, Isabelle, Coq gibi kanıt asistanları sayesinde bizler için oldukça karmaşık olan ya da belki de mümkün görünmeyen durumları yazılım temelli ispatlar ile elde edebiliriz. Örneğin buradan Mizar kullanılarak yazılmış birçok makaleye ulaşabilirsiniz. Bir yazılım yardımıyla ispatlanan en önemli problemlerden biri, Dört Renk Problemidir:

Bir harita, komşu ülkelerin farklı renklerde olması koşuluyla, dört renk kullanılarak boyanabilir.

1852 yılında ortaya atılan ve uzun yıllar ispatlanamayan problem, en sonunda, 1976 yılında bilgisayarların yardımıyla çözüme kavuşmuştur. (Günümüzde bilgisayarlara olan güvenimiz sonsuz, ama o zamanlar bu ispat büyük kuşku ile karşılanmış olmalı.)

Sezgisel mantığı anlatırken, Arend Heyting’in tanımladığı Heyting cebirlerinden bahsetmemek olmaz. Nasıl Boole cebirleri klasik mantığın cebirsel modelleri ise, Heyting cebirleri de sezgisel mantığın modelleridir.

sınırlı bir latis olmak üzere, eğer her için

koşulunu sağlayan bir ikili işlemi varsa, ‘ye bir Heyting Cebiri (ya da Brouwer Latis ya da Frame) denir.

Son olarak, Heyting Cebirleri ile topoloji arasındaki ilişkiye bir bakalım:

bir topolojik uzay olsun (En sevdiğim başlangıç cümlesi 🙂 ). açık kümeler olmak üzere, supremum, infimum, Heyting operatörü ve tümleyen işlemini, sırasıyla, aşağıdaki gibi tanımlayalım:

, ,
, .
(Burada iç operatörünü, ise tümleyeni gösterir.)

Bu durumda ‘in tüm açık kümelerinin ailesi bir Heyting cebiridir. İşte bize açılan bu pencereden nokta-bağımsız topoloji olarak da bilinen Frame ve Lokal Teorisine bir geçiş yaparız. Frame’ler topolojik uzaylar teorisine cebirsel bir bakış açısı sunar. Topolojik uzaylar teorisinde bilinen (Stone-Čech kompaktlaştırma gibi) bazı yapılar için yapıcı ispatlar elde edilmesine olanak sağlar. Ayrıca, kompakt uzayların çarpımının kompakt olması gibi, seçme aksiyomuna bağlı ispatların yapıcı versiyonlarına sahip olmamızı sağlar. Konu hakkında daha fazla bilgi sahibi olmak isteyenler için, bu teori üzerine yazılmış en kapsamlı kaynağı buraya bırakıyorum.

Bu yazıda sadece sezgisel mantıktan kısaca bahsetmiş olduk. Tabii mantık türleri bununla sınırlı değil ve hepsinden biraz bahsetmek bile sayfalar sürer. Daha sonraki yazılar ve daha derin konularda görüşmek üzere.

Kaynaklar
1)https://web.stanford.edu/~bobonich/glances%20ahead/IV.excluded.middle.html
2) https://en.wikipedia.org/wiki/Heyting_algebra
3) https://plato.stanford.edu/entries/logic-intuitionistic/
4) https://plato.stanford.edu/entries/russell-paradox/