Magasabb rendű logika

A magasabb rendű logika a matematikában és a logikában a predikátumlogikának egy olyan formája, amely az elsőrendű logikától a predikátumok feletti további predikátumokban, a felettük lévő kvantorokban és ennek megfelelően gazdagabb szemantikában különbözik . A magasabb rendű logikák szabványos szemantikájukkal kifejezőbbek, de modellelméleti tulajdonságaik sokkal nehezebben tanulmányozhatók és alkalmazhatók az elsőrendű logikához képest.

Az elsőrendű logika csak a változókat számszerűsíti; a másodrendű logika lehetővé teszi predikátumok és függvényszimbólumok számszerűsítését is (halmazok felett); a harmadrendű logika a predikátumokat használja és számszerűsíti a predikátumokkal (halmazok halmazaival) szemben, és így tovább. Például egy másodrendű mondat

a matematikai indukció elvét fejezi ki . A magasabb rendű logika magában foglalja az összes alacsonyabb rendű logikát; más szóval, a magasabb rendű logika lehetővé teszi az alacsonyabb beágyazási mélységű predikátumokkal (halmazok feletti) szóló utasításokat.

Példák és tulajdonságok

A magasabb rendű logika magában foglalja Church egyszerű típuselméletének [1] hajtásait és az intuicionista típuselmélet különféle formáit. Gerard Huet kimutatta, hogy az egyesítési probléma a harmadrendű logika intuicionista változatában algoritmikusan megoldhatatlan [2] [3] [4] , vagyis nincs olyan algoritmus, amely meghatározná, hogy egy tetszőleges egyenletnek van-e megoldása harmadrendűvel szemben. kifejezésekkel (és még inkább a harmadik feletti tetszőleges sorrendben).

Figyelembe véve az izomorfizmus fogalmát, a Boole -művelet másodrendű logikában van definiálva. Ezt a megfigyelést felhasználva Hintikka 1955-ben megállapította, hogy a magasabb rendű logikák másodrendű logikával is reprezentálhatók abban az értelemben, hogy a magasabb rendű logika minden képletéhez találhatunk megfelelő, egyformán érvényes másodrendű logikai formulát [5] .

Egyes összefüggésekben a magasabb rendű logika fogalma a klasszikus magasabb rendű logikára utal. Ugyanakkor a magasabb rendű modális logikát is tanulmányozták. Egyes logikusok szerint Gödel ontológiai bizonyítása ( technikai szempontból) ] .

Lásd még

• Elsőrendű logika
• Másodrendű logika
• Felsőfokú nyelvtan
• Intuicionista típuselmélet
• Többféle logika
• Gépelt lambda kalkulus
• modális logika

Jegyzetek

1. ↑ Church, Alonzo , A típusok egyszerű elméletének megfogalmazása Archivált : 2018. november 15., a Wayback Machine , The Journal of Symbolic Logic 5(2):56–68 (1940)
2. ↑ Huet, Gérard P.  Az egységesítés eldönthetetlensége a harmadrendű logikában  // Információ és vezérlés : folyóirat. - 1973. - 1. évf. 22 , sz. 3 . - P. 257-267 . - doi : 10.1016/s0019-9958(73)90301-x .
3. ↑ Huet, Gerard (1976. szept.). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (Ph.D.). Université de Paris VII.
4. ↑ Huet, Gerard. Higher Order Unification 30 years later // Proceedings, 15th International Conference TPHOL  (angol) / Carreño, V.; Muñoz, C.; Tahar, S. - Springer, 2002. - 20. évf. 2410. - P. 3-12. — (LNCS).
5. ↑ A Stanford Encyclopedia of Philosophy cikke a magasabb rendű logikáról . Letöltve: 2016. augusztus 9. Az eredetiből archiválva : 2016. június 17. (határozatlan)
6. ↑ Illesztés, MelvinTípusok, Tableau és Gödel Istene. - Springer Science & Business Media , 2002. - P. 139. - ISBN 978-1-4020-0604-3 . . – „Godel érvelése modális és legalább másodrendű, mivel Isten definíciójában a tulajdonságok kifejezett kvantifikálása szerepel. [...] [AG96] megmutatta, hogy az érvelés egy részét nem másodrendűnek, hanem harmadrendűnek tekinthetjük."

Irodalom

• Andrews, Peter B. (2002). Bevezetés a matematikai logikába és a típuselméletbe: A bizonyításon keresztül az igazsághoz , 2. kiadás, Kluwer Academic Publishers, ISBN 1-4020-0763-9
• Stewart Shapiro, 1991, "Alapok alapítványok nélkül: A másodrendű logika esete". Oxford University Press. ISBN 0-19-825029-0
• Stewart Shapiro, 2001, "Classical Logic II: Higher Order Logic", Lou Goble, szerk., The Blackwell Guide to Philosophical Logic . Blackwell, ISBN 0-631-20693-0
• Lambek, J. és Scott, PJ, 1986. Bevezetés a magasabb rendű kategorikus logikába , Cambridge University Press, ISBN 0-521-35653-9
• Jacobs, Bart. Kategorikus logika és típuselmélet . - North Holland, Elsevier, 1999. - (Studies in Logic and the Foundations of Mathematics 141). - ISBN 0-444-50170-3 .
• Benzmuller, Christoph; Miller, Dale. A magasabb rendű logika automatizálása // Handbook of the History of Logic, 9. kötet: Computational Logic  (angol) / Gabbay, Dov M.; Siekmann, George H.; Woods, John. - Elsevier , 2014. - ISBN 978-0-08-093067-1 .

Linkek

• Andrews, Peter B, Church's Type Theory in Stanford Encyclopedia of Philosophy .
• Miller, Dale, 1991, Logic: Higher-order, Encyclopedia of Artificial Intelligence , 2. kiadás.
• Herbert B. Enderton, Másodrendű és magasabb rendű logika in Stanford Encyclopedia of Philosophy , 2007. december 20-án; lényegesen felülvizsgálva 2009. március 4-én.