Meta-Mantık (Meta-Logic) ispatlar neden alt seviyeden (Sentetik mantık, Nicelemeler mantığı vs. ) mantık kurallarını kullanır ?

Question

Meta-mantığın ispatlarında karşılaştığım ispat adımlarında alt seviyeden mantığın çıkarım kurallarını kullanmakta. Hatta matematiksel indüksiyon prensibide sıklıkla karşılaştığım türden ispat metodlarından biri. Bu bir bakıma makul görünüyor. Mesela Gödel numaralandırmasında olduğu gibi bir  meta-teori yine sistemin bir başka teoremine haritalanarak sistemin kendi hakkında konuşturulması gibi bir durumu hayal ettiriyor. Diyelimki meta mantık mantığın kurallarını değilde kendine has kurallar kullansaydı bu seferde bu kuralların geçerliliğinin soruşturması şüpheli görünecekti. Ama bu seferde sıfırıncı derece ve birinci derece mantığın tamlık ve tutarlılığı yine kendilerinden menkul gibi görünüp dögüsellik hissi yaratıyor. 

Answer 1

Çünkü işe bir yerden başlamak zorudasınız!

Sorunuzun cevabı sorunun içerisindeki bir kelimede gizli: "Metamantığın ispatları..."

Günün sonunda teoremler kanıtlamak istiyorsunuz ve bunu yapabilmeniz için de bir biçimsel sisteme ihtiyaç duyuyorsunuz. Yani metamatematik yapmaya başladığınızda arka planda çalıştığınız objeleri içerisinde formalize edeceğiniz bir biçimsel sistemi varsayarak başlıyorsunuz. Örneğin Gödel, eksiklik teoremlerinin orijinal kanıtını aritmetiğin dilinde ve Peano belitlerinin biraz daha güçsüz bir hali içerisinde yapıyor (ve bu teori içerisinde aritmetiği "sayılaştırıyor"). Herhangi bir model teori kitabı açtığınızda hakkında konuşulan tüm kavramların arka planda olduğu varsayılan bir kümeler kuramı içerisinde biçimselleştirildiğini görürsünüz.

Ortada teknik olarak döngüsel bir şey yok. Sadece içerisinde kavramlarınızı biçimselleştirilebileceğiniz bir sistemi kabul ederek işe başlamanız lazım. Son cümlenizde bir anlamda haklısınız, sıfırıncı derece mantığı ve birinci derece mantığı bir nevi olduğu gibi kabul ediyoruz. Öte yandan bu, birincil derece mantığı kendi içerisinde biçimselleştirip, lafın gelişi, tamlık teoremini bir teorem olarak kanıtlamanız için engel değil.

Bunun dışında, mesela, birincil derece mantığın çıkarım kurallarının bir çelişkiye yol açmadığını görmek istiyorsanız formüller üzerinde tümevarımla tek elemanlı modelin imzası boş olan birincil derece dildeki tüm cümleleri sağladığını informal olarak gösterebilirsiniz. Ama bunu bir teorem olarak kanıtlamak istediğinizde gene arka planda başka bir sistem içerisinde çalışmak zorundasınız ki bu sistem içerisinde formül, model ve küme kavramlarını formalize ettikten sonra bahsedilen tümevarımı gerçekleştirebilin.

Comments

Son paragraf benim icin biraz daha aciklamaya muhtac. Anlamamis olabilirim fakat benim kastim su . Bir bicimsel sistem tamam fakat bicimsel sistem dedigimiz zaman alfabesi ve olusum kurallari demek degilmidir? Boylece neyin wffs oldugunu anlaya biliriz. Bir deduktif sistem dedigimizdede bunlaea ilaveten bir kurallar ve hatta aksiyomlar eklemiyormuyuz. Benim anlayamadigim mesela sifirinci derece nantigin tamliginin( semantik gecerli ise deduktif gecerlidir)  ispatinda modus tollens kullanarak basliyor. Bu kural sentetik mantigin bir cikarimi yada digerlerinden meydana gelen bir teoremi. Simdi klasik sentetik mantigin tamligini ispatlarken neden gene onun bir cikarim kurali yada teoremini kullanalim. Belkide yukarda anlattiniz ama benim icin daha aciklayici olmanizi rica etsem.

---

Yukarıda da dediğim gibi hiçbir şey kabul etmeden bir şeyler kanıtlayamazsınız.

Dolayısıyla (ihtiyaçlarınıza göre) sıfırıncı derece mantığı, yani önermeler mantığını, ya da birinci derece mantığı zaten kabul ederek işe başlıyoruz. Atmanız gereken bu ilk adımı başka bir şekilde temellendirmenin yolu yok. (Çünkü bunu yapmaya çalışırsanız "infinite regression" denen duruma girersiniz.)

Sezgisel olarak neden sıfırıncı derece mantığın tam olması gerektiğini görebiliyoruz. Diyelim ki bu sezgimizi formalize ederek bir "teorem" olarak kanıtlamak istiyoruz. Bu durumda "tam olmak" kavramını ilk başta kabul ettiğimiz biçimsel sistem içinde formalize etmemiz lazım zira yapmaya çalıştığımız şey bir teoremi kanıtlamak.

Örnek üzerinden gitmeliyim belki de. İçerisinde çalışacağımız sistem olarak ZFC kümeler kuramını seçelim. Bu durumda ilk adım olarak dilinin imzası $\in$ sembolünden oluşan birincil derece mantık sistemini standart çıkarım kuralları, standart aksiyomları ve ZFC aksiyomlarıyla kabul ediyoruz.

Daha sonra bu kuram içerisinde dil, model, teori vs. gibi kavramları objelerle (yani kümelerle) eşleyerek formalize ediyoruz. Daha sonra formalize ettiğimiz sıfırıncı derece mantığın tam olduğunu standart argümanlarla kanıtlıyoruz.

Sormak istediğiniz şey lisansta matematiksel mantık öğrenirken çok kafamı karıştıran bir şey olduğundan çok iyi anlıyorum takıldığınız noktayı, o yüzden şöyle özetleyeyim: Teori ile meta-teori arasındaki ayrıma dikkat edin.

Yukarıdaki örnekte içerisinde çalıştığımız meta-teori ZFC, hakkında matematiksel teoremler kanıtladığımız teori de (ZFC içerisinde formalize edilmiş) sıfırıncı derece mantık. Aynı şekilde birincil derece mantığı ZFC içerisinde formalize edip tam olduğunu kanıtlayabiliriz. Bu durumda meta-teorimiz ZFC, teorimiz birincil derece mantık.

Sizin sormak istediğiniz şey şu: E birincil derece mantığın tamlığını kanıtlamak için ZFC'nin dilindeki birincil derece mantığı kullandık, bu döngüsel değil mi?

Hayır, değil. İlk başta içerisinde çalışmak istediğimiz yeterince güçlü bir biçimsel sistemi olduğu gibi kabul ediyoruz. Daha sonra matematiksel objeler olarak formalize ettğimiz biçimsel sistemin tam olduğunu kanıtlıyoruz.

Dediğim gibi hiçbir şey kabul etmeden bir şeyler kanıtlayamazsınız. Dolayısıyla içerisinde çalışacağınız "arka plandaki" biçimsel sistem ne ise o sistemin kurallarını kabul ederek işe başlamanız lazım. Aksi halde birisine, lafın gelişi, birincil derece mantığın tamlığının kanıtından bahsetmek istediğinizde size şu soru gelecektir: Nere içerisindeki kanıtı?

---

Şimdi sonsuz geri gidişe düşmemek için bir yerde durmamız gerektiği tamamdır. (Gerçi Bu kuralda metadile ait bir durum olsa gerek ki metateorem olarak kabul ettik).

Özellikle metateorem ve teorem kavramları her kaynakta titizlikle belirtilen bir durum buda tamam. 

Cevap bir yerden başlamak durumunda yatıyor belli ki. Yani sezgisel olarak yeterince güçlü bir mantık sistemi kabul etmekle durum anlaşılıyor. 

Ama her nasılsa bu mantığın yeterince güçlü olduğunu düşünmemiz (Frege den bu yana ) ve onların tamlığını ispatlamamız (1918-1930) gibi 70-80 yıl almış. Kümeler kuramının aksiyomlarını ve tanımsız terimlerini temel aldığımız bu sistemler acaba kümeler kuramının bir model kaldığı daha temelde ne tür kavramlara yol açacak çok merak ediyorum.

Burak Bey bu arada teşekkür ederim bu ve daha öğrendikçe nice sorularımın cevabı sizde gibi gözüküyor. Amatör olarak ilgilendiğim bu konularda ne kadar yalnızım bir bilseniz :) Saygılar.

---

Bu arada yanlış anlaşılmamak için söylüyorum. İlla kümeler kuramları içerisinde çalışmak zorunda değilsiniz. Mesela sadece "kanıtlanabilirlik" ile ilgili konuşmak istiyorsanız ve hakkında konuşmak istediğiniz dilin sembolleri sayılabilirse, bunu aritmetikte (Peano aritmetiğinde, primitive recursive aritmetikte vs.) yapmak da mümkün ki Gödel'in orijinal olarak yaptığı tam olarak bu.

Ama genel olarak vardığınız noktada sorunuzun cevabını yakalamışsınız, bir yerden başlamak zorundayız ve sezgisel olarak bize anlamlı gelen bir biçimsel sistemi kabul ederek işe girişiyoruz. (Daha sonra da bize sezgisel olarak anlamlı gelen bu biçimsel sistemleri formalize edip bunların hakkında teoremler kanıtlıyoruz.)