WikiSort.ru - Не сортированное

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

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

${\displaystyle \forall P((0\in P\land \forall i(i\in P\to i+1\in P))\to \forall n(n\in P))}$

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

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

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

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

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

См. также

• Логика первого порядка
• Логика второго порядка
• Грамматика высшего порядка (англ.)
• Интуиционистская теория типов (англ.)
• Многосортная логика (англ.)
• Типизированное лямбда-исчисление
• Модальная логика

Примечания

Литература

• 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. — ISBN 0-444-50170-3.
• Benzmuller, Christoph. Automation of Higher-Order Logic // Handbook of the History of Logic, Volume 9: Computational Logic / Christoph Benzmuller, Miller. — 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 года.