Логика высшего порядка в математике и логике — форма предикатной логики, которая отличается от логики первого порядка дополнительными предикатами над предикатами, кванторами над ними, и, соответственно, более богатой семантикой. Логики высшего порядка с их стандартными семантиками более выразительны, но их модельно-теоретические свойства значительно более сложны для изучения и применения по сравнению с логикой первого порядка.
Логика первого порядка квантифицирует только переменные; логика второго порядка допускает также квантификацию предикатов и функциональных символов (над множествами); логика третьего порядка использует и квантифицирует предикаты над предикатами (множества множеств), и так далее. Например, предложение второго порядка
выражает принцип математической индукции. Логика высшего порядка включает все логики более низкого порядка; иначе говоря, логика высшего порядка допускает высказывания с предикатами (над множествами) более низкой глубины вложенности.
Примеры и свойства править
Логика высшего порядка включает ответвления простой теории типов[1] Чёрча и различные формы интуиционистской теории типов. Жерар Юэ показал, что задача унификации алгоритмически неразрешима в интуиционистской разновидности логики третьего порядка[2][3][4], то есть не существует алгоритма, который определял бы, есть ли решение у произвольного уравнения над термами третьего порядка (и тем более термами произвольного порядка выше третьего).
С учётом понятия изоморфизма операция булеана определяется в логике второго порядка. Используя это наблюдение, Хинтикка установил в 1955 году, что логики высшего порядка могут быть представлены логикой второго порядка в том смысле, что для каждой формулы логики высшего порядка можно найти соответствующую равновыполнимую формулу логики второго порядка[5].
В некоторых контекстах предполагается, что понятие логики высшего порядка относится к классической логике высшего порядка. Однако модальная логика высшего порядка также изучалась. Согласно некоторым учёным-логикам онтологическое доказательство Гёделя лучше всего изучено (с технической точки зрения) именно в таком контексте[6].
См. также править
Примечания править
- ↑ Чёрч, Алонзо, A formulation of the simple theory of types Архивная копия от 15 ноября 2018 на Wayback Machine, The Journal of Symbolic Logic 5(2):56–68 (1940)
- ↑ Huet, Gérard P. The Undecidability of Unification in Third Order Logic (англ.) // Information and Control : journal. — 1973. — Vol. 22, no. 3. — P. 257—267. — doi:10.1016/s0019-9958(73)90301-x. Архивировано 21 января 2022 года.
- ↑ Huet, Gérard (Sep 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (Ph.D.). Universite de Paris VII.
- ↑ Huet, Gérard. Higher Order Unification 30 years later // Proceedings, 15th International Conference TPHOL (англ.) / Carreño, V.; Muñoz, C.; Tahar, S.. — Springer, 2002. — Vol. 2410. — P. 3—12. — (LNCS). Архивировано 4 марта 2016 года.
- ↑ статья в Стэнфордской философской энциклопедии о логике высшего порядка. Дата обращения: 9 августа 2016. Архивировано 17 июня 2016 года.
- ↑ Fitting, Melvin Types, Tableaus, and Gödel's God. — Springer Science & Business Media, 2002. — С. 139. — ISBN 978-1-4020-0604-3.. — «Godel's argument is modal and at least second-order, since in his definition of God there is an explicit quantification over properties. [...] [AG96] showed that one could view a part of the argument not as second-order, but as third-order.».
Литература править
- Andrews, Peter B. (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed, Kluwer Academic Publishers, ISBN 1-4020-0763-9
- Stewart Shapiro, 1991, "Foundations Without Foundationalism: A Case for Second-Order Logic". Oxford University Press., ISBN 0-19-825029-0
- Stewart Shapiro, 2001, "Classical Logic II: Higher Order Logic," in Lou Goble, ed., The Blackwell Guide to Philosophical Logic. Blackwell, ISBN 0-631-20693-0
- Lambek, J. and Scott, P. J., 1986. Introduction to Higher Order Categorical Logic, Cambridge University Press, ISBN 0-521-35653-9
- Jacobs, Bart. Categorical Logic and Type Theory. — North Holland, Elsevier, 1999. — (Studies in Logic and the Foundations of Mathematics 141). — ISBN 0-444-50170-3.
- Benzmuller, Christoph; Miller, Dale. Automation of Higher-Order Logic // Handbook of the History of Logic, Volume 9: Computational Logic (англ.) / Gabbay, Dov M.; Siekmann, Jörg H.; Woods, John. — Elsevier, 2014. — ISBN 978-0-08-093067-1.
Ссылки править
- Andrews, Peter B, Church's Type Theory в Стэнфордской философской энциклопедии.
- Miller, Dale, 1991, "Logic: Higher-order," Encyclopedia of Artificial Intelligence, 2nd ed.
- Herbert B. Enderton, Second-order and Higher-order Logic в Стэнфордской философской энциклопедии, опубликовано 20 декабря 2007 года; существенно переработано 4 марта 2009 года.