Реализуемость

В математической логике реализуемость — это набор методов в теории доказательств, используемых для изучения конструктивных доказательств и извлечения из них дополнительной информации. ^[1] Формулы из формальной теории «реализуются» объектами, известными как «реализаторы», таким образом, что знание реализатора дает знание об истинности формулы. Существует много вариаций реализуемости; какой именно класс формул изучается и какие объекты являются реализаторами, отличается от одной вариации к другой.

Реализуемость можно рассматривать как формализацию интерпретации Брауэра–Гейтинга–Колмогорова (BHK) интуиционистской логики . В реализуемости понятие «доказательство» (которое остается неопределенным в интерпретации BHK) заменяется формальным понятием «реализатора». Большинство вариантов реализуемости начинаются с теоремы о том, что любое утверждение, которое доказуемо в изучаемой формальной системе, реализуемо. Однако реализатор обычно дает больше информации о формуле, чем формальное доказательство могло бы предоставить напрямую.

Помимо понимания интуиционистской доказуемости, реализуемость может применяться для доказательства свойств дизъюнкции и существования для интуиционистских теорий и для извлечения программ из доказательств, как в добыче доказательств . Она также связана с теорией топосов через реализуемость топосов .

Пример: реализуемость Клини 1945 года

Оригинальная версия реализуемости Клини использует натуральные числа в качестве реализаторов для формул в арифметике Гейтинга . Требуется несколько частей записи: во-первых, упорядоченная пара ( n , m ) рассматривается как одно число с использованием фиксированной примитивной рекурсивной функции спаривания ; во-вторых, для каждого натурального числа n , φ _n является вычислимой функцией с индексом n . Следующие предложения используются для определения отношения « n реализует A » между натуральными числами n и формулами A на языке арифметики Гейтинга, известного как отношение реализуемости Клини 1945 года: ^[2]

• Любое число n реализует атомарную формулу s = t тогда и только тогда, когда s = t истинно. Таким образом, каждое число реализует истинное уравнение, и ни одно число не реализует ложное уравнение.
• Пара ( n , m ) реализует формулу A ∧ B тогда и только тогда, когда n реализует A , а m реализует B. Таким образом, реализатор для конъюнкции — это пара реализаторов для конъюнктов.
• Пара ( n , m ) реализует формулу A ∨ B тогда и только тогда, когда выполняются следующие условия: n равно 0 или 1; и если n равно 0, то m реализует A ; и если n равно 1, то m реализует B. Таким образом, реализатор для дизъюнкции явно выбирает один из дизъюнктов (с n ) и предоставляет реализатор для него (с m ).
• Число n реализует формулу A → B тогда и только тогда, когда для каждого m , реализующего A , φ _n ( m ) реализует B. Таким образом, реализатор для импликации соответствует вычислимой функции, которая берет любой реализатор для гипотезы и создает реализатор для заключения.
• Пара ( n , m ) реализует формулу (∃ x ) A ( x ) тогда и только тогда, когда m является реализатором для A ( n ). Таким образом, реализатор для экзистенциальной формулы производит явного свидетеля для квантификатора вместе с реализатором для формулы, инстанцированной с этим свидетелем.
• Число n реализует формулу (∀ x ) A ( x ) тогда и только тогда, когда для всех m определено φ _n ( m ) и реализует A ( m ). Таким образом, реализатор для универсального утверждения — это вычислимая функция, которая для каждого m создает реализатор для формулы, инстанцированной с помощью m .

При таком определении получается следующая теорема: ^[3]

Пусть A — предложение арифметики Гейтинга (HA). Если HA доказывает A, то существует n, такое что n реализует A.

С другой стороны, существуют классические теоремы (даже схемы пропозициональных формул), которые реализуются, но не доказуемы в HA, факт, впервые установленный Роузом. ^[4] Таким образом, реализуемость не совсем отражает интуиционистские рассуждения.

Дальнейший анализ метода может быть использован для доказательства того, что HA обладает « свойствами дизъюнкции и существования »: ^[5]

• Если HA доказывает предложение (∃ x ) A ( x ), то существует n такое , что HA доказывает A ( n )
• Если HA доказывает предложение A ∨ B , то HA доказывает A или HA доказывает B.

Больше подобных свойств получено с использованием формул Харропа .

Дальнейшие события

Крайзель ввел модифицированную реализуемость , которая использует типизированное лямбда-исчисление как язык реализаторов. Модифицированная реализуемость — один из способов показать, что принцип Маркова невыводим в интуиционистской логике. Напротив, она позволяет конструктивно обосновать принцип независимости посылок :

${\displaystyle (A\rightarrow \exists x\;P(x))\rightarrow \exists x\;(A\rightarrow P(x))}$.

Относительная реализуемость ^[6] представляет собой интуиционистский анализ вычислимых или вычислимо перечислимых элементов структур данных, которые не обязательно вычислимы, например, вычислимые операции над всеми действительными числами, когда действительные числа могут быть только приближены в цифровых компьютерных системах.

Классическая реализуемость была введена Кривином ^[7] и расширяет реализуемость на классическую логику. Кроме того, она реализует аксиомы теории множеств Цермело–Френкеля . Понимаемая как обобщение форсинга Коэна , она использовалась для предоставления новых моделей теории множеств. ^[8]

Линейная реализуемость расширяет методы реализуемости до линейной логики . Термин был придуман Сейллером ^[9] для охвата нескольких конструкций, таких как геометрия моделей взаимодействия, ^[10] лудика , ^[11] модели графов взаимодействия. ^[12]

Приложения

Реализуемость — один из методов, используемых в добыче доказательств для извлечения конкретных «программ» из, казалось бы, неконструктивных математических доказательств. Извлечение программ с использованием реализуемости реализовано в некоторых помощниках по доказательству, таких как Coq .

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

• Переписка Карри–Говарда
• Диалектика интерпретация
• формула Харропа

Примечания

1. ван Оостен 2000
2. А. Щедров, «Интуиционистская теория множеств» (стр. 263--264). Из книги Харви Фридмана «Исследования оснований математики» (1985), «Исследования по логике и основаниям математики», т. 117.
3. ван Оостен 2000, стр. 7
4. Роуз 1953
5. ван Оостен 2000, стр. 6
6. Биркедал 2000
7. Кривин, Жан-Луи (2001). «Типизированное лямбда-исчисление в классической теории множеств Цермело-Френкеля». Архив для Mathematical Logic . 40 (2): 189–205.
8. Кривин, Жан-Луи (2011). «Алгебры реализуемости: программа для хорошего упорядочивания R». Логические методы в информатике . 7 .
9. Зайллер, Томас (2024). Математическая информатика (кандидатская диссертация). Университет Сорбонны Париж-Норд.
10. Жирар, Жан-Ив (1989). «Геометрия взаимодействия 1: Интерпретация системы F». Исследования по логике и основаниям математики . 127 : 221–260.
11. Жирар, Жан-Ив (2001). «Locus Solum: от правил логики к логике правил». Математические структуры в информатике . 11 : 301–506.
12. Seiller, Thomas (2016). «Графы взаимодействия: Полная линейная логика». Труды 31-го ежегодного симпозиума ACM/IEEE по логике в компьютерных науках .

Ссылки

• Биркедал, Ларс; Яап ван Остен (2000). Относительная и модифицированная относительная реализуемость.
• Крайзель Г. (1959). «Интерпретация анализа с помощью конструктивных функционалов конечных типов», в: Конструктивность в математике, под редакцией А. Гейтинга, Северная Голландия, стр. 101–128.
• Клини, СК (1945). «Об интерпретации интуиционистской теории чисел». Журнал символической логики . 10 (4): 109–124. doi :10.2307/2269016. JSTOR  2269016.
• Kleene, SC (1973). "Realizability: a retrospective survey" от Mathias, ARD; Hartley Rogers (1973). Летняя школа Кембриджа по математической логике: проводилась в Кембридже/Англия, 1–21 августа 1971 г. Берлин: Springer. ISBN 3-540-05569-X., стр. 95–112.
• ван Остен, Яап (2000). Реализуемость: исторический очерк.
• Rose, GF (1953). «Пропозициональное исчисление и реализуемость». Труды Американского математического общества . 75 (1): 1–19. doi : 10.2307/1990776 . JSTOR  1990776.

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

• Реализуемость Коллекция ссылок на последние статьи по реализуемости и смежным темам.