Логика высшего порядка
В математике и логике ( логика высшего порядка сокращенно HOL ) — это форма логики, которая отличается от логики первого порядка дополнительными кванторами и, иногда, более сильной семантикой . Логики высшего порядка с их стандартной семантикой более выразительны, но их теоретико-модельные свойства менее эффективны, чем свойства логики первого порядка.
Термин «логика высшего порядка» обычно используется для обозначения простой логики предикатов высшего порядка . Здесь «простой» указывает на то, что в основе теории типов лежит теория простых типов , также называемая простой теорией типов . Леон Чвистек и Фрэнк П. Рэмси предложили это как упрощение сложной и неуклюжей разветвленной теории типов в Principia Mathematica , изложенной Альфреда Норта Уайтхеда и Бертрана Рассела . Простые типы иногда также предназначены для исключения полиморфных и зависимых типов. [1]
Объем количественной оценки [ править ]
Логика первого порядка количественно определяет только переменные, которые варьируются в пределах отдельных людей; логика второго порядка , также дает количественную оценку множествам; логика третьего порядка также дает количественную оценку множествам множеств и так далее.
Логика высшего порядка представляет собой объединение логики первого, второго, третьего, ..., n -го порядка; т. е. логика высшего порядка допускает количественную оценку множеств, которые вложены сколь угодно глубоко.
Семантика [ править ]
Есть две возможные семантики логики высшего порядка.
В стандартной или полной семантике кванторы объектов более высокого типа варьируются по всем возможным объектам этого типа. Например, квантор множества индивидуумов распространяется на весь набор мощности множества индивидуумов. Таким образом, в стандартной семантике, как только набор индивидуумов указан, этого достаточно, чтобы указать все кванторы. HOL со стандартной семантикой более выразителен, чем логика первого порядка. Например, HOL допускает категориальную аксиоматизацию натуральных , и действительных чисел что невозможно с логикой первого порядка. Однако, по мнению Курта Гёделя , HOL со стандартной семантикой не допускает эффективного , надежного и полного исчисления доказательств . [2] Теоретико-модельные свойства HOL со стандартной семантикой также более сложны, чем свойства логики первого порядка. Например, число Левенгейма логики второго порядка уже больше первого измеримого кардинала , если такой кардинал существует. [3] Число Левенгейма логики первого порядка, напротив, равно ℵ 0 , наименьшему бесконечному кардиналу.
В семантике Хенкина в каждую интерпретацию для каждого типа высшего порядка включается отдельный домен. Таким образом, например, кванторы множества индивидуумов могут распространяться только на подмножество множества индивидов. HOL с этой семантикой эквивалентен многосортной логике первого порядка , а не более силен, чем логика первого порядка. В частности, HOL с семантикой Хенкина обладает всеми теоретико-модельными свойствами логики первого порядка и имеет полную, надежную и эффективную систему доказательств, унаследованную от логики первого порядка.
Свойства [ править ]
Логика высшего порядка включает в себя ответвления Чёрча . простой теории типов [4] и различные формы интуиционистской теории типов . Жерар Юэ показал, что в теоретико унификация неразрешима - типовой разновидности логики третьего порядка: [5] [6] [7] [8] то есть не может быть алгоритма, позволяющего решить, имеет ли произвольное уравнение между членами второго порядка (не говоря уже о произвольных членах более высокого порядка) решение.
С точностью до определенного понятия изоморфизма операция над набором степеней определима в логике второго порядка. Используя это наблюдение, Яакко Хинтикка установил в 1955 году, что логика второго порядка может моделировать логику высшего порядка в том смысле, что для каждой формулы логики высшего порядка можно найти для нее эквивалентную формулу в логике второго порядка. [9]
Предполагается, что в некотором контексте термин «логика высшего порядка» относится к классической логике высшего порядка. Однако модальная логика высшего порядка также изучалась. По мнению некоторых логиков, онтологическое доказательство Гёделя лучше всего изучать (с технической точки зрения) в таком контексте. [10]
См. также [ править ]
- Логика нулевого порядка (логика высказываний)
- Логика первого порядка
- Логика второго порядка
- Теория типов
- Грамматика высшего порядка
- Логическое программирование высшего порядка
- HOL (помощник по проверке)
- Многосортная логика
- Типизированное лямбда-исчисление
- Модальная логика
Примечания [ править ]
- ^ Джейкобс, 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 г.
