Logica de ordin superior

Logica de ordin superior în matematică și logică este o formă de logică a predicatelor care diferă de logica de ordinul întâi prin predicate suplimentare față de predicate, cuantificatori asupra acestora și, în consecință, semantică mai bogată . Logica de ordin superior cu semantica lor standard sunt mai expresive, dar proprietățile lor teoretice model sunt mult mai dificil de studiat și aplicat în comparație cu logica de ordinul întâi.

Logica de ordinul întâi cuantifică doar variabile; logica de ordinul doi permite, de asemenea, cuantificarea predicatelor și simbolurilor de funcție (peste mulțimi); logica de ordinul trei folosește și cuantifică predicate peste predicate (seturi de mulțimi) și așa mai departe. De exemplu, o propoziție de ordinul doi

exprimă principiul inducţiei matematice . Logica de ordin superior include toate logicile de ordin inferior; cu alte cuvinte, logica de ordin superior permite declarații cu predicate (peste seturi) de adâncime de imbricare mai mică.

Exemple și proprietăți

Logica de ordin superior include ramuri ale teoriei simple a tipurilor a lui Church [1] și diverse forme de teorie a tipurilor intuiționiste. Gerard Huet a arătat că problema unificării este de nerezolvat din punct de vedere algoritmic în varietatea intuiționistă a logicii de ordinul trei [2] [3] [4] , adică nu există un algoritm care să determine dacă o ecuație arbitrară are o soluție față de ordinul al treilea. termeni (și cu atât mai mult prin ordinea arbitrară a termenilor deasupra celui de-al treilea).

Ținând cont de conceptul de izomorfism, operația booleană este definită în logica de ordinul doi. Folosind această observație, Hintikka a stabilit în 1955 că logicile de ordinul superior pot fi reprezentate prin logica de ordinul doi în sensul că pentru fiecare formulă a logicii de ordinul superior se poate găsi o formulă logică de ordinul doi corespunzătoare la fel de validă [5] .

În unele contexte, se presupune că conceptul de logică de ordin superior se referă la logica clasică de ordin superior. Cu toate acestea, a fost studiată și logica modală de ordin superior . Potrivit unor logicieni, demonstrația ontologică a lui Gödel cel mai bine studiată (din punct de vedere tehnic) în acest context ] .

Vezi și

• Logica de ordinul întâi
• Logica de ordinul doi
• Gramatică superioară
• Teoria tipului intuitivistă
• Logica
• Calcul lambda tipizat
• logica modală

Note

1. ↑ Church, Alonzo , A formulation of the simple theory of types Arhivat la 15 noiembrie 2018 la Wayback Machine , The Journal of Symbolic Logic 5(2):56–68 (1940)
2. ↑ Huet, Gérard P.  The Indecidibility of Unification in Third Order Logic  // Information and Control : jurnal. - 1973. - Vol. 22 , nr. 3 . - P. 257-267 . - doi : 10.1016/s0019-9958(73)90301-x .
3. ↑ Huet, Gerard (sept. 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (Ph.D.). Universitatea din Paris VII.
4. ↑ Huet, Gerard. Higher Order Unification 30 years later // Proceedings, a 15th International Conference TPHOL  (engleză) / Carreño, V.; Muñoz, C.; Tahar, S. - Springer, 2002. - Vol. 2410. - P. 3-12. — (LNCS).
5. ↑ Articol de la Stanford Encyclopedia of Philosophy despre Higher Order Logic . Preluat la 9 august 2016. Arhivat din original la 17 iunie 2016. (nedefinit)
6. ↑ Fitting, MelvinTipuri, tablouri și Dumnezeul lui Gödel. - Springer Science & Business Media , 2002. - P. 139. - ISBN 978-1-4020-0604-3 . . — „Argumentul lui Godel este modal și cel puțin de ordinul doi, deoarece în definiția lui Dumnezeu există o cuantificare explicită asupra proprietăților. [...] [AG96] a arătat că se poate vedea o parte a argumentului nu ca de ordinul doi, ci de ordinul al treilea.”

Literatură

• Andrews, Peter B. (2002). O introducere în logica matematică și teoria tipurilor: la adevăr prin dovezi , ed. a doua, Kluwer Academic Publishers, ISBN 1-4020-0763-9
• Stewart Shapiro, 1991, „Fundații fără fundalism: un caz pentru logica de ordin al doilea”. Oxford University Press. ISBN 0-19-825029-0
• Stewart Shapiro, 2001, „Classical Logic II: Higher Order Logic”, în Lou Goble, ed., The Blackwell Guide to Philosophical Logic . Blackwell, ISBN 0-631-20693-0
• Lambek, J. și Scott, PJ, 1986. Introducere în logica categorială de ordin superior , Cambridge University Press, ISBN 0-521-35653-9
• Jacobs, Bart. Logica categorială și teoria tipurilor . - North Holland, Elsevier, 1999. - (Studies in Logic and the Foundations of Mathematics 141). - ISBN 0-444-50170-3 .
• Benzmuller, Christoph; Miller, Dale. Automatizarea logicii de ordin superior // Handbook of the History of Logic, volumul 9: Computational Logic  (english) / Gabbay, Dov M.; Siekmann, George H.; Woods, John. - Elsevier , 2014. - ISBN 978-0-08-093067-1 .

Link -uri

• Andrews, Peter B, Teoria tipului bisericii în Stanford Encyclopedia of Philosophy .
• Miller, Dale, 1991, " Logic: Higher-order " , Encyclopedia of Artificial Intelligence , a 2-a ed.
• Herbert B. Enderton, Logica de ordin al doilea și de ordin superior în Stanford Encyclopedia of Philosophy , publicat pe 20 decembrie 2007; revizuită substanțial la 4 martie 2009.