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