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

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

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

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

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

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

Семантика

Есть две возможные семантики логики высшего порядка.

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

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

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

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

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

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

См. также

Примечания

^ Джейкобс, 1999, глава 5.
^ Шапиро 1991, с. 87.
^ Менахем Магидор и Йоуко Вяэнянен . « О числах Левенхайма-Сколема-Тарского для расширений логики первого порядка », Отчет № 15 (2009/2010) Института Миттаг-Леффлера.
^ Алонсо Черч , Формулировка простой теории типов , Журнал символической логики 5 (2): 56–68 (1940).
^ Юэ, Жерар П. (1973). «Неразрешимость объединения в логике третьего порядка». Информация и контроль . 22 (3): 257–267. дои : 10.1016/s0019-9958(73)90301-x .
^ Юэ, Жерар (сентябрь 1976 г.). Решение уравнений на языках порядка 1,2,...ω (доктор философии) (на французском языке). Парижский университет VII.
^ Уоррен Д. Гольдфарб (1981). «Неразрешимость проблемы объединения второго порядка» (PDF) . Теоретическая информатика . 13 : 225–230.
^ Юэ, Жерар (2002). «Объединение высшего порядка 30 лет спустя» (PDF) . Ин Карреньо, В.; Муньос, К.; Тахар, С. (ред.). Материалы 15-й Международной конференции ТФОЛ . ЛНКС. Том. 2410. Спрингер. стр. 3–12.
^ запись на HOL
^ Фиттинг, Мелвин (2002). Типы, таблицы и Бог Гёделя . Springer Science & Business Media. п. 139. ИСБН 978-1-4020-0604-3 . Аргумент Гёделя является модальным и, по крайней мере, второго порядка, поскольку в его определении Бога имеется явная количественная оценка свойств. [...] [AG96] показал, что можно рассматривать часть аргумента не как аргумент второго, а как третьего порядка.

Ссылки

Эндрюс, Питер Б. (2002). Введение в математическую логику и теорию типов: к истине через доказательство , 2-е изд., Kluwer Academic Publishers, ISBN 1-4020-0763-9
Стюарт Шапиро , 1991, «Основы без фундаментализма: аргументы в пользу логики второго порядка». Издательство Оксфордского университета, ISBN 0-19-825029-0
Стюарт Шапиро , 2001, «Классическая логика II: логика высшего порядка», в издании Лу Гобла, « Руководство Блэквелла по философской логике ». Блэквелл, ISBN 0-631-20693-0
Ламбек Дж. и Скотт П.Дж., 1986. высшего порядка Введение в категориальную логику , издательство Кембриджского университета, ISBN 0-521-35653-9
Джейкобс, Барт (1999). Категориальная логика и теория типов . Исследования по логике и основам математики 141. Северная Голландия, Elsevier. ISBN 0-444-50170-3 .
Бенцмюллер, Кристоф; Миллер, Дейл (2014). «Автоматизация логики высшего порядка». В Габбае, Дов М.; Зикманн, Йорг Х.; Вудс, Джон (ред.). Справочник по истории логики, том 9: Вычислительная логика . Эльзевир. ISBN 978-0-08-093067-1 .

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

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

[1] Джейкобс, 1999, глава 5.

[2] Шапиро 1991, с. 87.

[3] Менахем Магидор и Йоуко Вяэнянен . « О числах Левенхайма-Сколема-Тарского для расширений логики первого порядка », Отчет № 15 (2009/2010) Института Миттаг-Леффлера.

[church-4] Алонсо Черч , Формулировка простой теории типов , Журнал символической логики 5 (2): 56–68 (1940).

[5] Юэ, Жерар П. (1973). «Неразрешимость объединения в логике третьего порядка». Информация и контроль . 22 (3): 257–267. дои : 10.1016/s0019-9958(73)90301-x .

[6] Юэ, Жерар (сентябрь 1976 г.). Решение уравнений на языках порядка 1,2,...ω (доктор философии) (на французском языке). Парижский университет VII.

[7] Уоррен Д. Гольдфарб (1981). «Неразрешимость проблемы объединения второго порядка» (PDF) . Теоретическая информатика . 13 : 225–230.

[8] Юэ, Жерар (2002). «Объединение высшего порядка 30 лет спустя» (PDF) . Ин Карреньо, В.; Муньос, К.; Тахар, С. (ред.). Материалы 15-й Международной конференции ТФОЛ . ЛНКС. Том. 2410. Спрингер. стр. 3–12.

[9] запись на HOL

[Fitting2002-10] Фиттинг, Мелвин (2002). Типы, таблицы и Бог Гёделя . Springer Science & Business Media. п. 139. ИСБН 978-1-4020-0604-3 . Аргумент Гёделя является модальным и, по крайней мере, второго порядка, поскольку в его определении Бога имеется явная количественная оценка свойств. [...] [AG96] показал, что можно рассматривать часть аргумента не как аргумент второго, а как третьего порядка.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]