В математике и логике , А логика высшего порядка является формой логики предикатов , которая отличается от логики первого порядка дополнительных кванторами , а иногда и более сильными семантики . Логики более высокого порядка с их стандартной семантикой более выразительны, но их теоретико-модельные свойства хуже, чем свойства логики первого порядка.
Термин «логика более высокого порядка», сокращенно HOL , обычно используется для обозначения простой логики предикатов более высокого порядка . Здесь «простой» означает, что лежащая в основе теория типов - это теория простых типов , также называемая простой теорией типов (см. Теория типов ). Леон Чвистек и Фрэнк П. Рэмси предложили это как упрощение сложной и неуклюжей разветвленной теории типов, указанной в « Основах математики » Альфреда Норта Уайтхеда и Бертрана Рассела . Простые типыв настоящее время иногда также означает исключение полиморфных и зависимых типов. [1]
Объем количественной оценки
Логика первого порядка определяет количественно только переменные, которые варьируются от отдельных лиц; логика второго порядка , кроме того, также дает количественную оценку по множествам; логика третьего порядка также дает количественную оценку по наборам множеств и так далее.
Логика высшего порядка - это объединение логики первого, второго, третьего, ..., n- го порядка; то есть логика более высокого порядка допускает количественную оценку по множествам, которые вложены сколь угодно глубоко.
Семантика
Есть две возможные семантики для логики более высокого порядка.
В стандартной или полной семантике квантификаторы для объектов более высокого типа располагаются для всех возможных объектов этого типа. Например, количественный показатель для наборов индивидуумов распространяется на всю мощь набора индивидуумов. Таким образом, в стандартной семантике после определения набора индивидов этого достаточно, чтобы указать все квантификаторы. HOL со стандартной семантикой более выразителен, чем логика первого порядка. Например, HOL допускает категориальную аксиоматизацию натуральных и действительных чисел , что невозможно с логикой первого порядка. Однако, согласно результату Курта Гёделя , HOL со стандартной семантикой не допускает эффективного , надежного и полного исчисления доказательств . [2] Теоретико-модельные свойства HOL со стандартной семантикой также более сложны, чем свойства логики первого порядка. Например, номер Левенгейм из логики второго порядка уже больше первого измеримый кардинала , если такие кардинальные существует. [3] Левенгейма количество логики первого порядка, напротив, ℵ 0 , наименьший бесконечный кардинал.
В семантике Хенкина в каждую интерпретацию для каждого типа более высокого порядка включается отдельный домен. Таким образом, например, кванторы по множеству индивидов могут варьироваться только по подмножеству мощного множества индивидов. HOL с такой семантикой скорее эквивалентен многосортированной логике первого порядка , чем более сильной, чем логика первого порядка. В частности, HOL с семантикой Хенкина обладает всеми теоретико-модельными свойствами логики первого порядка и имеет полную, надежную и эффективную систему доказательств, унаследованную от логики первого порядка.
Примеры и свойства
Высшие логики порядка включают отпрыск Церковь «s простой теории типов [4] , а также различных формы теории интуиционистского типа . Жерара Huet показал , что unifiability является неразрешимым в типа теоретико- привкусе логики третьего порядка, [5] [6] [7] , то есть не может быть никакого алгоритма , чтобы решить , следует ли произвольное уравнение между третьим порядком ( не говоря уже произвольные члены высшего порядка) имеет решение.
С точностью до определенного понятия изоморфизма операция powerset определима в логике второго порядка. Используя это наблюдение, Яакко Хинтикка в 1955 году установил, что логика второго порядка может моделировать логики более высокого порядка в том смысле, что для каждой формулы логики более высокого порядка можно найти равно удовлетворяемую формулу в логике второго порядка. [8]
Термин «логика высшего порядка» предполагается в некотором контексте для обозначения классической логики высшего порядка. Однако модальная логика высшего порядка также изучалась. По мнению некоторых логиков, онтологическое доказательство Гёделя лучше всего изучать (с технической точки зрения) в таком контексте. [9]
Смотрите также
- Логика первого порядка
- Логика второго порядка
- Теория типов
- Грамматика высшего порядка
- Логическое программирование высшего порядка
- HOL (помощник проверки)
- Многосортная логика
- Типизированное лямбда-исчисление
- Модальная логика
Заметки
- ↑ Джейкобс, 1999, глава 5
- ^ Шапиро 1991, стр. 87.
- ^ Менахем Магидор и Йоуко Вяэнянен. « О числах Левенхайма-Сколема-Тарского для расширений логики первого порядка », Отчет № 15 (2009/2010) Института Миттаг-Леффлера.
- ↑ Алонзо Чёрч , Формулировка простой теории типов , Журнал символической логики 5 (2): 56–68 (1940)
- ^ Хуэ, Жерар П. (1973). «Неразрешимость объединения в логике третьего порядка» . Информация и контроль . 22 (3): 257–267. DOI : 10.1016 / s0019-9958 (73) 90301-х .
- ^ Юэ, Жерар (сентябрь 1976 г.). Resolution d'Equations dans des Langages d'Ordre 1,2, ... ω (доктор философии) (на французском языке). Парижский университет VII.
- ^ Юэ, Жерар (2002). «Объединение высшего порядка 30 лет спустя» (PDF) . In Carreño, V .; Muñoz, C .; Тахар, С. (ред.). Материалы 15-й Международной конференции TPHOL . LNCS. 2410 . Springer. С. 3–12.
- ^ запись на HOL
- ^ Фиттинг, Мелвин (2002). Типы, Таблицы и Бог Гёделя . 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
- Джейкобс, Барт (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 г.