Daha yüksek mertebeden mantık - Higher-order logic

Gelen matematik ve mantık , bir yüksek dereceden mantık şeklidir yüklem mantık ayırt edilir birinci dereceden mantık ilave tarafından Nicelik ve bazen daha güçlü anlam . Standart anlambilimlerine sahip yüksek dereceli mantık daha açıklayıcıdır, ancak model-teorik özellikleri birinci dereceden mantığa göre daha az iyi davranır.

HOL olarak kısaltılan "yüksek dereceli mantık" terimi, genellikle yüksek dereceli basit yüklem mantığını ifade etmek için kullanılır . İşte "basit" altında yatan gösterir tip teori olan basit türleri teorisi olarak da adlandırılan türde basit teorisi (bkz Tip teorisi ). Leon Chwistek ve Frank P. Ramsey , Alfred North Whitehead ve Bertrand Russell tarafından Principia Mathematica'da belirtilen karmaşık ve beceriksiz tipler teorisinin basitleştirilmesi olarak önerdiler . Basit türler günümüzde bazen polimorfik ve bağımlı türleri dışlamak anlamına da gelmektedir .

Miktar belirleme kapsamı

Birinci dereceden mantık, yalnızca bireyler arasında değişen değişkenleri nicelleştirir; ikinci dereceden mantık , ek olarak, kümeler üzerinden nicelemeyi de belirler; üçüncü dereceden mantık aynı zamanda kümeler kümeleri üzerindeki nicelikleri de belirler ve bu böyle devam eder.

Yüksek mertebeden mantık , birinci, ikinci, üçüncü, ..., n inci mertebe mantığının birleşimidir ; diğer bir deyişle, yüksek dereceli mantık, keyfi olarak derinlemesine iç içe geçmiş kümeler üzerinde nicelleştirmeye izin verir.

Anlambilim

Daha yüksek mertebeden mantık için iki olası anlambilim vardır.

Olarak standart ya da tam anlam , nesneler üzerinde aralığı içinde daha yüksek tipi miktar bildiren tüm bu tür muhtemel nesneleri. Örneğin, birey kümeleri üzerindeki bir nicelik belirteci, bireyler kümesinin tüm güç kümesine yayılır . Bu nedenle, standart anlambilimde, bireyler kümesi belirtildikten sonra, bu, tüm niceleyicileri belirtmek için yeterlidir. Standart semantiğe sahip HOL, birinci dereceden mantıktan daha etkileyici. Örneğin, HOL doğal sayıların ve birinci dereceden mantıkla imkansız olan gerçek sayıların kategorik aksiyomatizasyonlarını kabul eder . Ancak, Kurt Gödel'in bir sonucu olarak , standart semantiğe sahip HOL, etkili , sağlam ve tam bir ispat hesabı kabul etmez . Standart semantiğe sahip HOL'ün model-teorik özellikleri de birinci dereceden mantığınkinden daha karmaşıktır. Örneğin , eğer böyle bir kardinal varsa , ikinci dereceden mantığın Löwenheim sayısı zaten birinci ölçülebilir kardinalden daha büyüktür . Buna karşılık, birinci dereceden mantığın Löwenheim sayısı , en küçük sonsuz kardinal olan ℵ _0'dır .

Gelen Henkin anlam , ayrı bir alan her yüksek dereceden türü için her bir yorumlama dahildir. Bu nedenle, örneğin, birey kümeleri üzerindeki niceleyiciler, bireyler kümesinin güç kümesinin yalnızca bir alt kümesini kapsayabilir . Bu semantiğe sahip HOL, birinci dereceden mantıktan daha güçlü olmaktan çok, çok sıralı birinci dereceden mantığa eşdeğerdir . Özellikle, Henkin semantiği ile HOL, birinci dereceden mantığın tüm model-teorik özelliklerine sahiptir ve birinci dereceden mantıktan miras alınan eksiksiz, sağlam, etkili bir ispat sistemine sahiptir.

Örnekler ve özellikler

Yüksek mertebeden mantıkları arasında dalları dahil Kilisesi 'nin tiplerinin basit teori ve çeşitli formları intuitionistic tip teorisi . Gerard Huet göstermiştir unifiability olan undecidable bir de tip-teorik üçüncü dereceden mantık lezzet olduğunu terimleri, bir çözümü vardır üçüncü düzen arasında rasgele bir denklem (tek başına rasgele yüksek sıralı izin) olmadığına karar vermek için bir algoritma olabilir .

Belirli bir izomorfizm kavramına kadar, güç kümesi işlemi ikinci derece mantıkta tanımlanabilir. Jaakko Hintikka , bu gözlemi kullanarak , 1955 yılında, ikinci dereceden mantığın, daha yüksek mertebeden mantığın her formülü için, ikinci mertebe mantıkta denkleştirilebilir bir formül bulabileceği anlamında, daha yüksek mertebeden mantığı simüle edebileceğini ortaya koydu .

"Yüksek dereceli mantık" teriminin bazı bağlamlarda klasik yüksek dereceli mantığa atıfta bulunduğu varsayılır . Bununla birlikte, modal yüksek mertebe mantığı da incelenmiştir. Birkaç mantıkçıya göre, Gödel'in ontolojik kanıtı en iyi şekilde (teknik açıdan) böyle bir bağlamda incelenir.

Ayrıca bakınız

• Birinci dereceden mantık
• İkinci dereceden mantık
• Tip teorisi
• Üst düzey dilbilgisi
• Üst düzey mantık programlama
• HOL (prova asistanı)
• Çok sıralı mantık
• Yazılı lambda hesabı
• Modal mantık

Notlar

Referanslar

• Andrews, Peter B. (2002). Matematiksel Mantık ve Tip Teorisine Giriş: Kanıtla Gerçeğe , 2. baskı, Kluwer Academic Publishers, ISBN   1-4020-0763-9
• Stewart Shapiro , 1991, "Temelsiz Temeller: İkinci Derece Mantık için Bir Örnek". Oxford University Press., ISBN   0-19-825029-0
• Stewart Shapiro , 2001, "Classical Logic II: Higher Order Logic", Lou Goble, editör, The Blackwell Guide to Philosophical Logic . Blackwell, ISBN   0-631-20693-0
• Lambek, J. ve Scott, PJ, 1986. Yüksek Dereceli Kategorik Mantığına Giriş , Cambridge University Press, ISBN   0-521-35653-9
• Jacobs, Bart (1999). Kategorik Mantık ve Tip Teorisi . Mantık Çalışmaları ve Matematiğin Temelleri 141. Kuzey Hollanda, Elsevier. ISBN   0-444-50170-3 .
• Benzmüller, Christoph; Miller, Dale (2014). "Yüksek Dereceli Mantığın Otomasyonu". Gabbay, Dov M .; Siekmann, Jörg H .; Woods, John (editörler). Handbook of the History of Logic, Cilt 9: Hesaplamalı Mantık . Elsevier. ISBN   978-0-08-093067-1 .

Dış bağlantılar

• Andrews, Peter B, Kilise'nin Tipi Teorisi içinde Felsefe Stanford Encyclopedia .
• Miller, Dale, 1991, " Logic: Higher-order ," Encyclopedia of Artificial Intelligence , 2. baskı.
• Herbert B. Enderton, Second-order and Higher-order Logic in Stanford Encyclopedia of Philosophy , 20 Aralık 2007; önemli revizyon 4 Mart 2009.