Для установки нажмите кнопочку Установить расширение. И это всё.

Исходный код расширения WIKI 2 регулярно проверяется специалистами Mozilla Foundation, Google и Apple. Вы также можете это сделать в любой момент.

4,5
Келли Слэйтон
Мои поздравления с отличным проектом... что за великолепная идея!
Александр Григорьевский
Я использую WIKI 2 каждый день
и почти забыл как выглядит оригинальная Википедия.
Статистика
На русском, статей
Улучшено за 24 ч.
Добавлено за 24 ч.
Альтернативы
Недавние
Show all languages
Что мы делаем. Каждая страница проходит через несколько сотен совершенствующих техник. Совершенно та же Википедия. Только лучше.
.
Лео
Ньютон
Яркие
Мягкие

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

Из Википедии — свободной энциклопедии

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

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

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

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

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

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

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

См. также

Примечания

  1. Чёрч, Алонзо, A formulation of the simple theory of types, 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.
  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).
  5. статья в Стэнфордской философской энциклопедии о логике высшего порядка
  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.

Ссылки

Эта страница в последний раз была отредактирована 3 марта 2021 в 19:43.
Основа этой страницы находится в Википедии. Текст доступен по лицензии CC BY-SA 3.0 Unported License. Нетекстовые медиаданные доступны под собственными лицензиями. Wikipedia® — зарегистрированный товарный знак организации Wikimedia Foundation, Inc. WIKI 2 является независимой компанией и не аффилирована с Фондом Викимедиа (Wikimedia Foundation).