Логика высшего порядка

(перенаправлено с «Логики высшего порядка»)

Логика высшего порядка в математике и логике — форма предикатной логики, которая отличается от логики первого порядка дополнительными предикатами над предикатами, кванторами над ними, и, соответственно, более богатой семантикой. Логики высшего порядка с их стандартными семантиками более выразительны, но их модельно-теоретические свойства значительно более сложны для изучения и применения по сравнению с логикой первого порядка.

Логика первого порядка квантифицирует только переменные; логика второго порядка допускает также квантификацию предикатов и функциональных символов (над множествами); логика третьего порядка использует и квантифицирует предикаты над предикатами (множества множеств), и так далее. Например, предложение второго порядка

выражает принцип математической индукции. Логика высшего порядка включает все логики более низкого порядка; иначе говоря, логика высшего порядка допускает высказывания с предикатами (над множествами) более низкой глубины вложенности.

Примеры и свойства

править

Логика высшего порядка включает ответвления простой теории типов[1] Чёрча и различные формы интуиционистской теории типов. Жерар Юэ показал, что задача унификации алгоритмически неразрешима в интуиционистской разновидности логики третьего порядка[2][3][4], то есть не существует алгоритма, который определял бы, есть ли решение у произвольного уравнения над термами третьего порядка (и тем более термами произвольного порядка выше третьего).

С учётом понятия изоморфизма операция булеана определяется в логике второго порядка. Используя это наблюдение, Хинтикка установил в 1955 году, что логики высшего порядка могут быть представлены логикой второго порядка в том смысле, что для каждой формулы логики высшего порядка можно найти соответствующую равновыполнимую формулу логики второго порядка[5].

В некоторых контекстах предполагается, что понятие логики высшего порядка относится к классической логике высшего порядка. Однако модальная логика высшего порядка также изучалась. Согласно некоторым учёным-логикам онтологическое доказательство[англ.] Гёделя лучше всего изучено (с технической точки зрения) именно в таком контексте[6].

См. также

править

Примечания

править
  1. Чёрч, Алонзо, A formulation of the simple theory of types Архивная копия от 15 ноября 2018 на Wayback Machine, The Journal of Symbolic Logic 5(2):56–68 (1940)
  2. 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 года.
  3. Huet, Gérard (Sep 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (Ph.D.). Universite de Paris VII.
  4. 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 года.
  5. статья в Стэнфордской философской энциклопедии о логике высшего порядка. Дата обращения: 9 августа 2016. Архивировано 17 июня 2016 года.
  6. 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.

Ссылки

править