Biçimsel sistem

Açılış sahnesi

Kerem, katalog programını bir nesne olarak incelemeye karar vermişti. Ama incelemeye başlayınca, programın neden oluştuğunu hiç yazmadığını fark ediyor. Program hangi işaretleri tanıyordu? Hangi işaret dizileri bir kayıt sayılıyordu, hangileri anlamsız bir karalamaydı? Hangi kayıtlar başlangıçta programa elle girilmişti, hangileri programın kurallarıyla türetilmişti? Kerem, bu soruların cevapları olmadan, programın tutarlı olup olmadığını sormanın bile anlamsız olduğunu görüyor.

Tolga, bir defterin arkasına üç harfle oynanan küçük bir oyun yazıyor. Oyunun bir başlangıç dizisi ve dört dönüştürme kuralı var; hiçbir harf bir şey anlatmıyor. Tolga, bu oyunun bir mantık sisteminden ne farkı olduğunu soruyor. Selin, anlamı olmayan işaretlerle oynanan bir oyunun hiçbir şeyi kanıtlayamayacağını düşünüyor. Lina, bir dilin dilbilgisinin de, hangi dizilerin cümle olduğunu anlamlarına bakmadan söyleyebildiğini hatırlıyor. Barış, bir vasiyetnamenin içeriği ne olursa olsun, biçim şartlarını karşılamıyorsa geçersiz sayıldığını söylüyor. Defne ise bir tanı kılavuzunun, hekimin yargısından bağımsız olarak, yalnızca kayıtların biçimine bakarak işletilip işletilemeyeceğini merak ediyor. Bu ders, Mantık ve Akıl Yürütme programının Metalojik ve Hesaplanabilirlik kursunda, bir mantığı bir nesne olarak inceleyebilmek için onun hangi parçalardan oluşan bir biçimsel sistem olarak tanımlanması gerektiğini, alfabenin, kuruluş kurallarının, aksiyomların ve çıkarım kurallarının her birinin ne iş gördüğünü ve bir sistemin anlamından soyutlanarak yalnızca biçimiyle ele alınmasının ne kazandırıp ne kaybettirdiğini soruyor.

Bu derste ne olacak

Önce bu dersin yerini belirleyelim. Nesne dil/üstdil dersi, bir sistemin içinde kanıtlanan önermeler ile sistem hakkında kanıtlanan metateoremler arasındaki ayrımı kurdu ve Hilbert'in, kanıtları sonlu işaret dizileri olarak inceleyen programını tanıttı. Programın önceki kurslarında çıkarım kuralı ve biçimselleştirme kavramları tanımlanmış, Post'un önermeler mantığı için doğruluk tablosu yöntemini veren 1921 tarihli çalışması ve Frege'nin Aritmetiğin Temel Yasaları'nın iki kesimi de ele alınmıştı. Bu ders, metateorinin nesnesini tanımlıyor: bir biçimsel sistemin tam olarak ne olduğunu ve onu anlamından ayırmanın neyi mümkün kıldığını inceliyor.

Sonra üç kaynağa bakacağız. Emil Post, 1943'te yayımladığı Genel Birleşimsel Karar Probleminin Biçimsel İndirgenmeleri makalesinde, her biçimsel sistemin, işaret dizilerini yeniden yazan basit kurallardan oluşan bir sisteme indirgenebileceğini gösterir. Douglas Hofstadter, 1979'da yayımladığı Gödel, Escher, Bach kitabında, anlamı olmayan dört işaretle kurulmuş küçük bir sistem aracılığıyla, bir sistemin içinde çalışmak ile onun hakkında düşünmek arasındaki farkı gösterir. Gottlob Frege ise 1903'te yayımlanan Aritmetiğin Temel Yasaları'nın ikinci cildinde, aritmetiği anlamsız işaretlerle oynanan bir oyun sayan biçimci görüşü eleştirir.

Ardından üç itirazı tartacağız: anlamsız bir işaret oyununun hiçbir doğruyu kanıtlayamayacağı, biçimsel sistemlerin keyfi olduğu ve bir kuralın uygulanmasının bile anlamı gerektirdiği itirazları.

Sonda, bir akıl yürütme alanını bir biçimsel sistem olarak tanımlamanın dört adımını göstereceğiz: alfabeyi belirlemek, iyi kurulmuş dizileri tanımlayan kuralları yazmak, aksiyomları seçmek ve çıkarım kurallarını yalnızca dizilerin biçimine başvurarak ifade etmek.

Merkez soru

Sorumuz şu: bir mantığı bir biçimsel sistem olarak tanımlamak ne demektir ve onu anlamından soyutlayarak yalnızca biçimiyle ele almak ne kazandırıp ne kaybettirir?

Ölçülü iddiam şu: bir biçimsel sistem dört parçadan oluşur. Birincisi, sistemin kullandığı işaretlerin sonlu bir listesi olan alfabedir. İkincisi, bu işaretlerin hangi dizilerinin iyi kurulmuş formül sayıldığını belirleyen kuruluş kurallarıdır. Üçüncüsü, başlangıçta verilen formüller olan aksiyomlardır. Dördüncüsü, bazı formüllerden başka bir formüle geçmeye izin veren çıkarım kurallarıdır. Bu parçaların her biri, formüllerin anlamına değil, yalnızca biçimine başvurarak tanımlanır. Bir formülün iyi kurulmuş olup olmadığı, bir dizinin bir kanıt olup olmadığı, işaretlerin ne anlattığı bilinmeden, mekanik olarak denetlenebilir. Kazanç budur. Bir kanıtın doğruluğu, bir yorumun inandırıcılığına değil, sonlu bir denetime bağlanır. Sistemin kendisi de, Hofstadter'in küçük sisteminde görüldüğü gibi, bir matematik nesnesi olarak incelenebilir. Post, bu yapının son derece genel olduğunu, her biçimsel sistemin dizileri yeniden yazan basit kurallara indirgenebileceğini gösterdi. Kayıp ise, Frege'nin vurguladığı gibi, biçimsel bir sistemin kendi başına hiçbir şeyi doğru olarak ileri sürmemesidir. Bir teorem yalnızca türetilebilir bir dizidir. Onun bir şeyi doğru olarak söylemesi için bir yoruma, çıkarım kurallarının doğruluğu koruması içinse ayrıca kanıtlanması gereken bir özelliğe ihtiyaç vardır.

Sıfır noktası

Bir öğrenci bir mantık kitabında kanıt yazmayı öğrendiğinde, çoğu zaman her adımı anlamıyla denetler: bu öncül doğruysa, bu sonuç da doğru olmalı. Bu, önceki kurslarda tanımlanan çıkarım kuralı kavramına uygundur. Orada bir çıkarım kuralı, öncüller doğruysa sonucu da doğru kılan bir geçiş olarak tanımlanmıştı.

Biçimsel sistem kavramı bu tanımı ikiye ayırır. Bir yanda, kuralın biçimi vardır: belirli biçimdeki dizilerden belirli biçimdeki bir diziye geçmek. Öbür yanda, kuralın doğruluğu koruyup korumadığı sorusu vardır. Biçimsel sistem yalnızca birinci yanla tanımlanır. Kural, "şu biçimdeki iki diziden sonra şu biçimdeki diziyi yazabilirsin" der; neden yazabileceğini söylemez. Doğruluğun korunup korunmadığı, sistemin içinde değil, sistem hakkında, üst dilde sorulan bir sorudur.

Bu ayrım ilk bakışta yapay görünür. Ama Hilbert'in programı tam olarak buna ihtiyaç duyuyordu. Bir kanıtın geçerliliği, anlam hakkındaki tartışmalı yargılara bağlı kalırsa, kanıtların güvenilirliği de tartışmalı kalırdı. Kanıtın geçerliliği yalnızca biçime bağlanırsa, herkes aynı sonlu denetimi yaparak aynı sonuca varabilirdi.

Görüşler ve pozisyonlar

Biçimsel sistemlerin matematik ve mantıkla ilişkisi konusunda üç görüş var.

Birinci görüş, oyun biçimciliğidir. Buna göre matematik, anlamsız işaretlerle belirli kurallara göre oynanan bir oyundur. Bir teorem, bir satranç konumu gibi, kurallara uygun hamlelerle ulaşılan bir dizidir ve hiçbir şey hakkında doğru değildir.

İkinci görüş, anlambilimsel görüştür. Buna göre bir biçimsel sistem, önceden anlamı olan bir akıl yürütme pratiğinin biçimsel bir kaydıdır. Sistemin değeri, işaretlerinin bir şeyi göstermesinden ve kurallarının doğruluğu korumasından gelir. Frege'nin görüşü budur.

Üçüncü görüş, metamatematik görüşüdür. Buna göre bir biçimsel sistem, anlamından soyutlanarak incelenebilir, ama bu soyutlama bir araçtır, bir öğreti değil. Sistem biçim olarak incelenir, sonra bir yorumla ilişkilendirilir ve iki düzey arasındaki bağ ayrıca kanıtlanır. Hilbert'in ve Kleene'nin yaklaşımı budur.

Bu ders üçüncü görüşü temel alır ve ikinci görüşün, bir biçimsel sistemin değerinin bir yorumdan geldiği gözlemini kabul eder. Birinci görüş, bir kanıtın geçerliliğinin biçime bağlanabildiğini doğru görür. Ama Haskell Curry gibi biçimcilerin de sonradan kabul ettiği gibi, sistemin neden bu kurallarla kurulduğunu ve neden işe yaradığını açıklamakta güçlük çeker. İkinci görüş, bu açıklamayı verir. Üçüncü görüş, iki görüşün de haklı olduğu yerleri ayırır: biçim, denetim için; yorum, doğruluk için.

Argümanın yapısı

Bir akıl yürütme alanını bir biçimsel sistem olarak tanımlamak için dört adım izlenebilir.

Birinci adım, alfabeyi belirlemektir. Tanımlayan, sistemin kullanacağı bütün işaretleri sonlu bir liste olarak yazar ve bu listenin dışındaki hiçbir işaretin sistemde yer almayacağını belirtir.

İkinci adım, iyi kurulmuş dizileri tanımlayan kuralları yazmaktır. Tanımlayan, alfabenin hangi dizilerinin sistemin formülleri sayılacağını, anlamlarına değil, işaretlerin sırasına ve düzenine bakarak belirleyen kuralları yazar.

Üçüncü adım, aksiyomları seçmektir. Tanımlayan, sistemin başlangıçta kabul edeceği formülleri listeler ya da aksiyomların hangi biçimde olacağını gösteren kalıplar verir.

Dördüncü adım, çıkarım kurallarını yalnızca dizilerin biçimine başvurarak ifade etmektir. Tanımlayan, her kuralın hangi biçimdeki formüllerden hangi biçimdeki bir formüle geçmeye izin verdiğini yazar ve kuralın uygulanıp uygulanmadığının mekanik olarak denetlenebildiğini gösterir.

En güçlü itiraz

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

Biçimsel sistem kavramını ciddiye alan düşünce şu cevabı verebilir. Bir biçimsel sistem, bir alfabeden, iyi kurulmuş dizileri belirleyen kuruluş kurallarından, aksiyomlardan ve çıkarım kurallarından oluşur. Bütün bu parçalar yalnızca işaretlerin biçimine başvurarak tanımlanır. Kerem'in dört listesinde görüldüğü gibi, bir dizinin bir kanıt olup olmadığı bu yüzden işaretlerin ne anlattığı bilinmeden mekanik olarak denetlenebilir. Post, bu yapının her biçimsel sistemi kapsayacak kadar genel olduğunu gösterdi. Hofstadter'in küçük sisteminde ve Tolga'nın üç harfinde görüldüğü gibi, anlamı olmayan bir sistem de bir matematik nesnesi olarak incelenebilir ve bir dizinin türetilemezliği, kuralların koruduğu bir değişmez özellik bulunarak üst düzeyde kanıtlanabilir. Kazanç, kanıtın geçerliliğinin sonlu ve herkesin aynı biçimde yapabileceği bir denetime bağlanmasıdır. Kayıp ise Frege'nin vurguladığı gibi, bir teoremin kendi başına hiçbir şeyi doğru olarak ileri sürmemesidir. Barış'ın vasiyetnamesinde ve Defne'nin kılavuzunda görüldüğü gibi, biçim bir amaca hizmet ettiğinde anlam kazanır. Bu yüzden bir biçimsel sistemin değeri, ancak onun bir yorumla ilişkisi ayrıca incelendiğinde tam olarak ortaya çıkar.

Açık kalan sorular

Tolga'nın üç harfi, MU'nun türetilemezliğinin bir değişmez özellik bulunarak kanıtlanabildiğini gösterdi. Her türetilemez dizi için böyle bir özellik bulunabilir mi? Bir dizinin türetilip türetilemeyeceğine her zaman karar verilebilir mi?

Lina'nın dizileri, bir dilin kuruluş kurallarının kullanımdan çıkarıldığını ve istisnalar taşıdığını gösterdi. Bir doğal dilin cümleleri, istisnasız kuruluş kurallarıyla tam olarak tanımlanabilir mi? Tanımlanamıyorsa, doğal dildeki akıl yürütme bir biçimsel sistemle tam olarak kaydedilebilir mi?

Defne'nin tanı kılavuzu, biçimsel sistemin denetlenebilirlik kazandırıp yargının esnekliğini kaybettirdiğini gösterdi. Bu iki değer arasında bir denge kurulabilir mi? Bir biçimsel sistem, kendi kurallarının istisnalarını da biçimsel olarak içerebilir mi?

Yaygın hatalar

Kendin dene

Aklında kalsın

Beş cümlede dersin iskeleti.

Bir biçimsel sistem bir alfabeden, iyi kurulmuş dizileri belirleyen kuruluş kurallarından, aksiyomlardan ve çıkarım kurallarından oluşur ve bütün bu parçalar yalnızca işaretlerin biçimine başvurarak tanımlanır, bu yüzden bir dizinin kanıt olup olmadığı mekanik olarak denetlenebilir.

Post'un 1943 tarihli makalesi her biçimsel sistemin dizileri yeniden yazan basit kurallara indirgenebileceğini, Hofstadter'in Gödel, Escher, Bach kitabı anlamı olmayan bir sistemin de bir değişmez özellikle üst düzeyde incelenebileceğini, Frege'nin Aritmetiğin Temel Yasaları'ndaki eleştirisi ise anlamından soyutlanmış bir sistemin doğruluğu ve uygulanabilirliği açıklayamayacağını gösterdi.

Bir alan dört adımla biçimsel bir sistem olarak tanımlanır: alfabeyi belirlemek, iyi kurulmuş dizileri tanımlayan kuralları yazmak, aksiyomları seçmek ve çıkarım kurallarını yalnızca dizilerin biçimine başvurarak ifade etmek.

Anlamsız bir oyunun doğruyu kanıtlayamayacağı, biçimsel sistemlerin keyfi olduğu ve kuralı uygulamanın bile anlam gerektirdiği itirazları, biçimin doğruluğu dışlamadığını ama onunla bağını ayrıca kanıtlanabilir kıldığını, bir sistemin keyfi olmamasının bir amaca hizmet etmesinden geldiğini ve kuralların yorum anlaşmazlıklarının en az olduğu bir düzeyde seçildiğini gördüğümüzde cevaplanabilir.

Bu yüzden bir mantığı bir biçimsel sistem olarak tanımlamak, kanıtın geçerliliğini sonlu bir denetime bağlar ve sistemi bir matematik nesnesi hâline getirir, ama sistemin değerini onun bir yorumla ilişkisi incelendiğinde ortaya çıkan bir soruya bırakır.

Sonraki derse köprü

Tolga'nın üç harfli oyunu hiçbir şey anlatmıyordu. Ama katalog programı anlatıyordu. Programın türettiği her kayıt, bir nüsha hakkında bir şey söylüyordu. Kerem, programın kurallarının biçimsel olarak doğru uygulanmasının, türetilen kayıtların nüshalar hakkında doğru olmasını güvence altına alıp almadığını soruyor.

Selin, önceki kurslarda bir çıkarım kuralının, öncüller doğruysa sonucu da doğru kılan bir geçiş olarak tanımlandığını hatırlatıyor. Biçimsel sistemde ise kural yalnızca bir biçim geçişiydi. Doğruluğun korunması, kuralın tanımından çıkarılmış, ayrıca kanıtlanması gereken bir özelliğe dönüşmüştü. Defne, tanı kılavuzunun bir kuralı yanlış kurulmuşsa, sistemin kusursuz işleyip yanlış tanılar üretebileceğini söylüyor.

Bir sonraki ders bu soruya dönüyor. Seslilik dersi, bir biçimsel sistemin türettiği her sonucun, öncüllerinin doğru olduğu her yorumda doğru olmasının ne demek olduğunu, bu özelliğin bir sistem için nasıl kanıtlandığını ve bir sistemin sesli olmasının, onun bütün doğruları türetebilmesinden neden farklı bir şey olduğunu soruyor.