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

Формальная система логики

В математике и логике логика высшего порядка (сокращенно HOL ) — это форма логики, которая отличается от логики первого порядка дополнительными квантификаторами и, иногда, более сильной семантикой . Логики высшего порядка с их стандартной семантикой более выразительны, но их модельно-теоретические свойства менее хорошо себя ведут, чем свойства логики первого порядка.

Термин «логика высшего порядка» обычно используется для обозначения простой предикатной логики высшего порядка . Здесь «простой» указывает на то, что базовая теория типов — это теория простых типов , также называемая простой теорией типов . Леон Хвистек и Фрэнк П. Рэмси предложили это как упрощение сложной и неуклюжей разветвленной теории типов, указанной в Principia Mathematica Альфреда Норта Уайтхеда и Бертрана Рассела . Простые типы иногда также подразумевают исключение полиморфных и зависимых типов. ^[1]

Объем количественной оценки

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

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

Семантика

Существуют две возможные семантики логики высшего порядка.

В стандартной или полной семантике квантификаторы по объектам более высокого типа охватывают все возможные объекты этого типа. Например, квантификатор по множествам индивидов охватывает весь powerset множества индивидов. Таким образом, в стандартной семантике, как только множество индивидов определено, этого достаточно, чтобы задать все квантификаторы. HOL со стандартной семантикой более выразительна, чем логика первого порядка. Например, HOL допускает категориальные аксиоматизации натуральных чисел и действительных чисел , которые невозможны в логике первого порядка. Однако, согласно результату Курта Гёделя , HOL со стандартной семантикой не допускает эффективного , обоснованного и полного исчисления доказательств . ^[2] Теоретико-модельные свойства HOL со стандартной семантикой также более сложны, чем свойства логики первого порядка. Например, число Лёвенгейма логики второго порядка уже больше, чем первый измеримый кардинал , если такой кардинал существует. ^[3] Число Лёвенгейма логики первого порядка, напротив, равно ℵ 0 , наименьшему бесконечному кардиналу.

В семантике Хенкина в каждую интерпретацию для каждого типа более высокого порядка включен отдельный домен. Таким образом, например, квантификаторы по множествам индивидов могут охватывать только подмножество powerset множества индивидов. HOL с этой семантикой эквивалентна многосортной логике первого порядка , а не сильнее логики первого порядка. В частности, HOL с семантикой Хенкина обладает всеми модельно-теоретическими свойствами логики первого порядка и имеет полную, надежную, эффективную систему доказательств, унаследованную от логики первого порядка.

Характеристики

Логики более высокого порядка включают ответвления простой теории типов Чёрча [ ^4] и различные формы интуиционистской теории типов . Жерар Юэ показал, что унифицируемость неразрешима в теоретико-типовом варианте логики третьего порядка, ^{[5] [6] [7] [8]} то есть не может быть алгоритма для определения того, имеет ли решение произвольное уравнение между членами второго порядка (не говоря уже о произвольных членах более высокого порядка).

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

Термин «логика высшего порядка» в некотором контексте предполагается относящимся к классической логике высшего порядка. Однако модальная логика высшего порядка также изучалась. По мнению нескольких логиков, онтологическое доказательство Гёделя лучше всего изучать (с технической точки зрения) в таком контексте. ^[10]

Смотрите также

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

Примечания

1. Джейкобс, 1999, глава 5
2. Шапиро 1991, стр. 87.
3. Менахем Магидор и Йоуко Вяэнянен . «О числах Левенхайма-Сколема-Тарского для расширений логики первого порядка», Отчет № 15 (2009/2010) Института Миттаг-Леффлера.
4. Алонзо Чёрч , Формулировка простой теории типов, Журнал символической логики 5(2):56–68 (1940)
5. Huet, Gérard P. (1973). «Неразрешимость объединения в логике третьего порядка». Информация и управление . 22 (3): 257–267. doi :10.1016/s0019-9958(73)90301-x.
6. Юэ, Жерар (сентябрь 1976 г.). Резолюция d'Equations dans des Langages d'Ordre 1,2,...ω (доктор философии) (на французском языке). Парижский университет VII.
7. Уоррен Д. Голдфарб (1981). «Неразрешимость проблемы объединения второго порядка» (PDF) . Теоретическая информатика . 13 : 225–230.
8. Huet, Gérard (2002). «Высшее объединение порядка 30 лет спустя» (PDF) . В Carreño, V.; Muñoz, C.; Tahar, S. (ред.). Труды 15-й международной конференции TPHOL . LNCS. Том 2410. Springer. стр. 3–12.
9. запись на HOL
10. Fitting, Melvin (2002). Типы, Tableaus и Бог Гёделя . Springer Science & Business Media. стр. 139. ISBN 978-1-4020-0604-3. Аргумент Гёделя является модальным и, по крайней мере, второго порядка, поскольку в его определении Бога присутствует явная квантификация свойств. [...] [AG96] показал, что можно рассматривать часть аргумента не как второго порядка, а как третьего порядка.

Ссылки

• Эндрюс, Питер Б. (2002). Введение в математическую логику и теорию типов: к истине через доказательство , 2-е изд., Kluwer Academic Publishers, ISBN 1-4020-0763-9 
• Стюарт Шапиро , 1991, «Основания без фундаментализма: случай в пользу логики второго порядка». Oxford University Press., ISBN 0-19-825029-0 
• Стюарт Шапиро , 2001, «Классическая логика II: Логика высшего порядка», в книге Лу Гобла, ред., « Руководство Блэквелла по философской логике ». Блэквелл, ISBN 0-631-20693-0 
• Ламбек, Дж. и Скотт, П.Дж., 1986. Введение в категориальную логику высшего порядка , Cambridge University Press, ISBN 0-521-35653-9 
• Jacobs, Bart (1999). Категориальная логика и теория типов. Исследования по логике и основаниям математики 141. North Holland, Elsevier. ISBN 0-444-50170-3.
• Benzmüller, Christoph; Miller, Dale (2014). «Автоматизация логики высшего порядка». В Gabbay, Dov M.; Siekmann, Jörg H.; Woods, John (ред.). Справочник по истории логики, том 9: Вычислительная логика . Elsevier. ISBN 978-0-08-093067-1.

Внешние ссылки

• Эндрюс, Питер Б., Теория типов Чёрча в Стэнфордской энциклопедии философии .
• Миллер, Дейл, 1991, «Логика: Высший порядок», Энциклопедия искусственного интеллекта , 2-е изд.
• Герберт Б. Эндертон, Логика второго и высшего порядка в Стэнфордской энциклопедии философии , опубликовано 20 декабря 2007 г.; существенная переработка 4 марта 2009 г.