Yapıcı ispat

Açılış sahnesi

Kerem, raporun en eski argümanlarından birine dönüyor. Grup, bir zamanlar şunu göstermişti: katalogda kaynağa yakın iki aday vardı, kütüphanedeki el yazması ve müzedeki el yazması; ikisinin de kaynak olmadığını varsaymak, üç tanığın ortak okumalarıyla çelişiyordu; öyleyse ikisinden biri kaynaktı. Argüman geçerliydi ve grup onu hâlâ kabul ediyordu. Ama Kerem, argümanın hangisinin kaynak olduğunu hiç söylemediğini fark ediyor. Grup, "ya kütüphanedeki ya müzedeki el yazması kaynaktır" cümlesini kanıtlamıştı, ama iki seçenekten hangisinin doğru olduğunu bilmiyordu. Bu kanıt, bir kaynak bulmuş muydu, yoksa yalnızca bir kaynağın bulunmaması gerektiğini mi göstermişti?

Selin, matematikte de benzer bir kanıtın bilindiğini, iki sayı arasında belirli bir ilişki bulunduğunu, hangi iki sayı olduğunu söylemeden kanıtlayan bir kanıt olduğunu hatırlatıyor. Tolga, raporun "ya da" ile kurulan cümlelerinin hangilerinin gerçekten bir seçeneği gösterdiğini, hangilerinin yalnızca bir çelişkiden kaçındığını ayırmak istiyor. Barış, bir mahkemenin "iki sanıktan biri suçludur" sonucuna vardığında, ikisinden hiçbirini mahkûm edemeyeceğini söylüyor. Defne, bir hekimin bir hastanın iki hastalıktan birini taşıdığını bildiği hâlde hangisini bilmediğinde, bazen yine de tedaviye başlayabildiğini anlatıyor. Lina ise bir kanıtın, bir şeyin var olduğunu göstermekle kalmayıp onu bulmanın bir yolunu da verip veremeyeceğini soruyor. Bu ders, Mantık ve Akıl Yürütme programının Klasik Olmayan Mantıklar kursunda, üçüncü hâlin olmazlığını genel bir yasa olarak kabul etmeyen sezgici mantığın temel düşüncesini, bir cümlenin doğru olmasının onun kanıtlanabilmesi anlamına geldiği görüşünü ve bu görüşün hangi klasik çıkarımları geçersiz kıldığını soruyor.

Bu derste ne olacak

Önce bu dersin yerini belirleyelim. Çok değerli ve bulanık mantık modülü, klasik mantığı yeni değerler ekleyerek genişleten mantıkları inceledi ve Felsefi yorum dersi, bu mantıkların iki değerli durumlarda klasik mantığa indirgendiğini gösterdi. Bu ders, farklı türden bir klasik olmayan mantığı, sezgici mantığı, açıyor: yeni değerler eklemeyen, ama bazı klasik yasaları geçersiz sayan bir mantığı. Programın önceki kurslarında Brouwer'in, Kolmogorov'un, Glivenko'nun ve Heyting'in sezgici mantık üzerine çalışmaları ile reductio yöntemi tanıtılmıştı. Bu ders, bunları yeniden anlatmadan, yapıcı ispatın ne olduğunu, bir kanıtın bir şeyi kurmasının ne anlama geldiğini ve bu düşüncenin çağdaş matematik ve bilgisayar biliminde nasıl bir biçim aldığını inceliyor.

Sonra üç kaynağa bakacağız. Dov Jarden, 1953'te Scripta Mathematica'da yayımladığı kısa bir notta, iki irrasyonel sayının, birinin ötekine göre kuvvetinin rasyonel olabileceğini, hangi iki sayının bu özelliği taşıdığını belirlemeden kanıtlar; bu kanıt, yapıcı olmayan kanıtların en çok anılan örneklerinden biri olmuştur. Errett Bishop, 1967'de yayımladığı Yapıcı Analizin Temelleri kitabında, matematiğin bütün önermelerinin sayısal bir anlam taşıması gerektiğini savunur ve klasik analizin büyük bir kısmını yapıcı biçimde yeniden kurar. Per Martin-Löf ise 1984'te yayımlanan Sezgici Tür Kuramı derslerinde, bir önermeyi onun kanıtlarının türü, bir kanıtı ise bir tür içindeki bir nesne olarak ele alan bir çerçeve kurar ve bu çerçevede kanıtların programlar gibi işlediğini gösterir.

Ardından üç itirazı tartacağız: yapıcı olmayan kanıtların da gerçek bilgi verdiği, yapıcılık gereğinin matematiği gereksiz yere daralttığı ve kanıtın doğrulukla özdeşleştirilmesinin doğruluğu insan bilgisine bağladığı itirazları.

Sonda, bir kanıtın yapıcı olup olmadığını değerlendirmenin dört adımını göstereceğiz: kanıtın bir "ya da" ya da bir varlık önermesi taşıyıp taşımadığını belirlemek, kanıtın hangi seçeneğin ya da hangi nesnenin söz konusu olduğunu gösterip göstermediğini sormak, kanıtın üçüncü hâlin olmazlığına ya da çifte olumsuzlamanın elenmesine dayanıp dayanmadığını denetlemek ve kanıttan bir yöntem çıkarılıp çıkarılamayacağını sınamak.

Merkez soru

Sorumuz şu: bir kanıtın yapıcı olması ne demektir ve bir cümlenin doğru olmasını onun kanıtlanabilmesiyle özdeşleştirmek hangi klasik çıkarımları geçersiz kılar?

Ölçülü iddiam şu: bir kanıt, bir varlık önermesi için belirli bir nesneyi ve onun istenen özelliği taşıdığının kanıtını, bir "ya da" önermesi için ise seçeneklerden birini ve onun kanıtını verdiğinde yapıcıdır; sezgici mantığın kanıt yorumuna göre, bağlaçların anlamı, onları içeren önermelerin nasıl kanıtlanacağıyla verilir: "ya A ya B" önermesinin bir kanıtı, A'nın ya da B'nin bir kanıtı ve hangisinin kanıtlandığının bir göstergesidir; "A ise B" önermesinin bir kanıtı, A'nın her kanıtını B'nin bir kanıtına dönüştüren bir yöntemdir. Bu yorumda, üçüncü hâlin olmazlığı genel bir yasa olamaz, çünkü "ya A ya A değil" önermesini kanıtlamak, A'yı ya da onun olumsuzlamasını kanıtlamayı gerektirir ve bu her A için yapılamaz. Jarden'in kanıtının gösterdiği gibi, klasik mantık, hangi seçeneğin doğru olduğunu göstermeden bir "ya da" önermesini kanıtlamaya izin verir, sezgici mantık ise vermez. Bishop'ın gösterdiği gibi, yapıcılık gereği matematiğin büyük bir kısmını dışarıda bırakmaz, onu sayısal anlamı olan bir biçimde yeniden kurar. Martin-Löf'ün çerçevesinde, yapıcı bir kanıt, istenen nesneyi hesaplayan bir program gibi işler. Bu yüzden yapıcı ispat, yalnızca bir şeyin var olduğunu değil, onun nasıl bulunacağını da gösteren bir ispattır.

Sıfır noktası

Bir öğrenci bir şeyin var olduğunu kanıtlamanın iki yolu olduğunu çoğu zaman fark etmez. Birinci yol, o şeyi göstermektir: bir denklemin bir çözümü olduğunu, o çözümü bulup denklemi sağladığını göstererek kanıtlamak. İkinci yol, o şeyin var olmamasının bir çelişkiye yol açtığını göstermektir: bir denklemin çözümü olmadığını varsayıp bu varsayımdan bir çelişki türeterek, bir çözümün var olduğu sonucuna varmak. Klasik mantıkta iki yol da geçerlidir ve aynı sonucu verir.

Ama iki yol, farklı şeyler verir. Birinci yol, çözümün kendisini verir; ikinci yol, yalnızca bir çözümün bulunmaması gerektiğini. Önermeler mantığı kursunda görülen reductio yöntemi, ikinci yolun temel aracıdır: bir önermenin olumsuzlamasından bir çelişki türetmek, o önermenin olumsuzlamasının olumsuzlamasını kanıtlar; klasik mantıkta çifte olumsuzlama elenerek önermenin kendisine geçilir. Sezgici mantık, bu son adımı genel olarak kabul etmez: bir şeyin olmamasının olanaksız olduğunu göstermek, onun olduğunu göstermek değildir.

Bu fark, "ya da" önermeleri için de geçerlidir. Klasik mantıkta "ya A ya A değil" her zaman doğrudur ve bu yasa, iki seçenekten hangisinin doğru olduğunu bilmeden bir "ya da" önermesini kanıtlamaya izin verir. Sezgici mantıkta ise "ya A ya B" önermesini kanıtlamak, A'yı ya da B'yi kanıtlamak ve hangisini kanıtladığını bilmek demektir.

Görüşler ve pozisyonlar

Yapıcı ispatın matematik ve mantık için önemi konusunda üç görüş var.

Birinci görüş, sezgici görüştür. Buna göre bir matematik önermesinin doğru olması, onun kanıtlanabilmesidir ve matematiksel nesneler, onları kuran zihinsel etkinlikten bağımsız olarak var olmaz. Yapıcı olmayan kanıtlar, bir nesnenin var olduğunu değil, yalnızca var olmamasının olanaksız olduğunu gösterir ve bu yüzden gerçek bir varlık kanıtı değildir.

İkinci görüş, yapıcı pratik görüşüdür. Buna göre yapıcı ispat, bir felsefi öğretiye bağlanmadan, matematiğin sayısal içerik taşıyan bir biçimde yapılmasının bir yoludur. Bir önermenin yapıcı bir kanıtı, onun klasik bir kanıtından daha fazla bilgi verir ve bu yüzden tercih edilir, ama klasik kanıtlar da geçerlidir.

Üçüncü görüş, klasik görüştür. Buna göre bir matematik önermesi, kanıtlanıp kanıtlanamayacağından bağımsız olarak ya doğru ya yanlıştır ve yapıcı olmayan kanıtlar, yapıcı kanıtlar kadar geçerlidir. Yapıcı ispat, bazı durumlarda daha fazla bilgi verir, ama bu, bir mantık meselesi değil, bir kullanım meselesidir.

Bu ders ikinci görüşü temel alır ve birinci görüşün kanıt yorumunu, bağlaçların anlamını açıklamanın güçlü bir yolu olarak kabul eder. Birinci görüş, bir "ya da" önermesinin bir seçim bilgisi taşıması gerektiği sezgisini doğru yakalar, ama matematiksel nesnelerin zihinsel etkinliğe bağlı olduğu yönündeki felsefi iddiası tartışmalıdır. Üçüncü görüş, klasik kanıtların geçerliliğini korur, ama Kerem'in iki adayında görüldüğü gibi, yapıcı olmayan bir kanıtın bir karar için neden yetersiz kalabileceğini açıklamakta güçlük çeker. İkinci görüş, iki kanıt türü arasındaki farkı bir felsefi öğretiye bağlamadan, bir bilgi farkı olarak açıklar.

Argümanın yapısı

Bir kanıtın yapıcı olup olmadığını değerlendirmek için dört adım izlenebilir.

Birinci adım, kanıtın bir "ya da" ya da bir varlık önermesi taşıyıp taşımadığını belirlemektir. Değerlendiren, kanıtın sonucunun bir seçimi ya da bir nesnenin varlığını ileri sürüp sürmediğini sorar; yapıcılık sorunu, bu tür sonuçlarda ortaya çıkar.

İkinci adım, kanıtın hangi seçeneğin ya da hangi nesnenin söz konusu olduğunu gösterip göstermediğini sormaktır. Değerlendiren, kanıtın sonunda, istenen nesnenin ya da doğru seçeneğin ne olduğunu söyleyip söyleyemediğine bakar.

Üçüncü adım, kanıtın üçüncü hâlin olmazlığına ya da çifte olumsuzlamanın elenmesine dayanıp dayanmadığını denetlemektir. Değerlendiren, kanıtın bir adımında "ya A ya A değil" önermesinin ya da "A değil değil ise A" çıkarımının kullanılıp kullanılmadığını belirler.

Dördüncü adım, kanıttan bir yöntem çıkarılıp çıkarılamayacağını sınamaktır. Değerlendiren, kanıtın, istenen nesneyi bulmanın ya da doğru seçeneği belirlemenin adım adım bir yolunu verip vermediğini sorar.

En güçlü itiraz

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

Yapıcı ispatı ciddiye alan düşünce şu cevabı verebilir. Bir kanıt, bir varlık önermesi için belirli bir nesneyi, bir "ya da" önermesi için ise seçeneklerden birini ve onun kanıtını verdiğinde yapıcıdır; sezgici mantığın kanıt yorumuna göre bağlaçların anlamı, onları içeren önermelerin nasıl kanıtlanacağıyla verilir ve bu yorumda üçüncü hâlin olmazlığı genel bir yasa olamaz. Jarden'in kanıtı, klasik mantığın, hangi nesnenin istenen özelliği taşıdığını göstermeden bir varlık önermesini kanıtlamaya izin verdiğini gösterir. Bishop'ın gösterdiği gibi, yapıcılık gereği, bir felsefi öğretiye bağlanmadan, matematiğin geniş bir kısmını sayısal anlamı olan bir biçimde yeniden kurar ve kaybettiği, çoğu zaman sayısal içeriği olmayan teoremlerdir. Martin-Löf'ün çerçevesinde, yapıcı bir kanıt, istenen nesneyi hesaplayan bir program gibi işler. Yapıcı olmayan kanıtlar da bir bilgi verir, ama bu bilgi, bir şeyin var olmamasının olanaksız olduğu bilgisidir; yapıcı kanıtlar ise o şeyin ne olduğunu ve nasıl bulunacağını da gösterir ve bir karar ya da bir eylem için çoğu zaman bu ikinci bilgi gerekir.

Açık kalan sorular

Kerem'in iki adayı, grubun yapıcı olmayan bir "ya da" bilgisine sahip olduğunu, filigran kaydının ise bu bilgiyi yapıcı bir bilgiye çevirdiğini gösterdi. Yapıcı olmayan bir bilgiyi yapıcı bir bilgiye çevirmenin genel bir yöntemi var mıdır, yoksa her durumda yeni bir kanıt mı gerekir?

Selin'in iki sayısı, Jarden'in kanıtındaki doğru kutunun, çok daha derin bir teoremle belirlendiğini gösterdi. Bir yapıcı olmayan kanıtın ardından, doğru seçeneği belirlemenin olanaksız olduğu durumlar olabilir mi? Olabilirse, o durumlarda "ya da" önermesi doğru mudur?

Barış'ın iki sanığı, ceza hukukunun yapıcı bir kanıt gereğine benzer bir ilke taşıdığını gösterdi. Hukukun başka alanlarında, örneğin medeni hukukta, yapıcı olmayan bir sorumluluk bilgisi, iki kişiden birinin bir zararı karşılaması gerektiği bilgisi, bir karar için yeterli olabilir mi?

Yaygın hatalar

Kendin dene

Aklında kalsın

Beş cümlede dersin iskeleti.

Bir kanıt, bir varlık önermesi için belirli bir nesneyi, bir "ya da" önermesi için ise seçeneklerden birini ve onun kanıtını verdiğinde yapıcıdır; sezgici mantığın kanıt yorumunda bağlaçların anlamı, onları içeren önermelerin nasıl kanıtlanacağıyla verilir.

Jarden'in notu klasik mantığın hangi nesnenin istenen özelliği taşıdığını göstermeden bir varlık önermesini kanıtlamaya izin verdiğini, Bishop'ın Yapıcı Analizin Temelleri kitabı yapıcılık gereğinin matematiğin geniş bir kısmını sayısal anlamı olan bir biçimde yeniden kurduğunu, Martin-Löf'ün Sezgici Tür Kuramı dersleri ise yapıcı bir kanıtın istenen nesneyi hesaplayan bir program gibi işlediğini gösterdi.

Bir kanıtın yapıcı olup olmadığı dört adımla değerlendirilir: kanıtın bir "ya da" ya da varlık önermesi taşıyıp taşımadığını belirlemek, hangi seçeneği ya da nesneyi gösterdiğini sormak, üçüncü hâlin olmazlığına ya da çifte olumsuzlamanın elenmesine dayanıp dayanmadığını denetlemek ve kanıttan bir yöntem çıkarılıp çıkarılamayacağını sınamak.

Yapıcı olmayan kanıtların da bilgi verdiği, yapıcılığın matematiği daralttığı ve doğruluğu kanıta bağlamanın onu insana bağladığı itirazları, iki kanıt türünün farklı bilgiler verdiğini, kaybedilen teoremlerin çoğu zaman sayısal içeriği olmayan teoremler olduğunu ve yapıcı ispatın değerinin doğruluğun ne olduğu tartışmasından bağımsız olduğunu gördüğümüzde cevaplanabilir.

Bu yüzden bir şeyin var olduğunu kanıtlamak, onun olmamasının olanaksız olduğunu göstermekle yetinmek değil, bir karar ya da bir eylem gerektiğinde, onun ne olduğunu ve nasıl bulunacağını da gösterip göstermediğini sormaktır.

Sonraki derse köprü

Kerem'in iki adayı ve Selin'in iki sayısı, yapıcı olmayan kanıtların hep aynı noktaya, üçüncü hâlin olmazlığına, dayandığını göstermişti. Kerem, sezgici mantığın bu yasayı neden genel bir yasa olarak kabul etmediğini daha açık görmek istiyor: bir önerme ya doğru ya yanlış değil miydi? Sezgici mantık, bu yasanın hiçbir zaman doğru olmadığını mı, yoksa her zaman doğru olmadığını mı söylüyordu?

Tolga, kolofondaki okunaksız tarihin, "ya bu yıl ya sonraki yıl" cümlesinin yapıcı olarak kanıtlanamamasının nedeni olduğunu, ama sözcük okunabilirse cümlenin yapıcı hâle geleceğini hatırlatıyor. Selin, bazı matematik önermelerinin, hiç kimsenin kanıtlayamadığı ve çürütemediği önermelerin, sezgici mantıkta ne durumda olduğunu soruyor. Lina, bir sonlu kümede, örneğin bir kataloğun nüshaları arasında, üçüncü hâlin olmazlığının her zaman geçerli olup olmadığını merak ediyor.

Bir sonraki ders bu soruya dönüyor. Dışlanmış üçüncü dersi, sezgici mantığın üçüncü hâlin olmazlığını neden genel bir yasa olarak kabul etmediğini, bu yasanın hangi durumlarda sezgici olarak da geçerli olduğunu ve Brouwer'in bu yasaya karşı kurduğu zayıf karşı örneklerin neyi gösterdiğini soruyor.