Логика высшего порядка - Higher-order logic

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

Термин «логика высшего порядка», сокращенно HOL , обычно используется для обозначения простой логики предикатов более высокого порядка . Здесь «простой» означает, что лежащая в основе теория типов - это теория простых типов , также называемая простой теорией типов (см. Теория типов ). Леон Чвистек и Фрэнк П. Рэмси предложили это как упрощение сложной и неуклюжей разветвленной теории типов, описанной в « Основах математики » Альфреда Норта Уайтхеда и Бертрана Рассела . В наши дни простые типы иногда также предназначены для исключения полиморфных и зависимых типов.

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

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

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

Семантика

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

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

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

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

Высшие логики порядка включают отпрыск Церковь «s простой теории типов и различные формы теории интуиционистского типа . Жерара Huet показал , что unifiability является неразрешимым в типа теоретико- привкусе логики третьего порядка, то есть, не может быть никакого алгоритма , чтобы решить , произвольное уравнение между третьим порядком ( не говоря уже произвольный более высокий порядок) ли условие имеет решение .

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

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

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

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

Заметки

Рекомендации

• Эндрюс, Питер Б. (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
• Джейкобс, Барт (1999). Категориальная логика и теория типов . Исследования по логике и основам математики 141. Северная Голландия, Эльзевир. ISBN   0-444-50170-3 .
• Бенцмюллер, Кристоф; Миллер, Дейл (2014). «Автоматизация логики высшего порядка». В Габбае, Дов М .; Siekmann, Jörg H .; Вудс, Джон (ред.). Справочник по истории логики, Том 9: Вычислительная логика . Эльзевир. ISBN   978-0-08-093067-1 .

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

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