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

В математической логике реализуемость — это набор методов в теории доказательств, используемых для изучения конструктивных доказательств и извлечения из них дополнительной информации. [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.
  • Реализуемость Коллекция ссылок на последние статьи по реализуемости и смежным темам.
Retrieved from "https://en.wikipedia.org/w/index.php?title=Realizability&oldid=1266223236"