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

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

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

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

Пример: реализуемость Клини 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] Таким образом, реализуемость не совсем отражает интуиционистские рассуждения.

Дальнейший анализ метода может быть использован для доказательства того, что ГА обладает « свойствами дизъюнкции и существования »: ^[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] — это интуиционистский анализ рекурсивных или рекурсивно перечислимых элементов структур данных, которые не обязательно вычислимы, например, вычислимые операции со всеми действительными числами, когда действительные числа могут быть только аппроксимированы в цифровых компьютерных системах.

Приложения

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

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

• Переписка Карри-Ховарда
• Диалектическая интерпретация
• Формула Харропа

Примечания

1. ван Остен 2000
2. А. Щедров, «Интуиционистская теория множеств» (стр. 263–264). Из исследования Харви Фридмана по основам математики (1985), « Исследования по логике и основам математики», том. 117.
3. ван Остен 2000, стр. 7
4. Роза 1953 г.
5. ван Остен 2000, стр. 6
6. Биркедал 2000

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

• Биркедал, Ларс; Яап ван Остен (2000). Относительная и модифицированная относительная реализуемость.
• Крейзель Г. (1959). «Интерпретация анализа с помощью конструктивных функционалов конечных типов», в: Конструктивность в математике под редакцией А. Хейтинга, Северная Голландия, стр. 101–128.
• Клини, Южная Каролина (1945). «Об интерпретации интуиционистской теории чисел». Журнал символической логики . 10 (4): 109–124. дои : 10.2307/2269016. JSTOR  2269016.
• Клини, Южная Каролина (1973). «Реализуемость: ретроспективный обзор» от Матиаса, ARD; Хартли Роджерс (1973). Кембриджская летняя школа по математической логике: проводилась в Кембридже, Англия, 1–21 августа 1971 г. Берлин: Шпрингер. ISBN 3-540-05569-Х., стр. 95–112.
• ван Остен, Яап (2000). Реализуемость: исторический очерк.
• Роуз, ГФ (1953). «Исчисление высказываний и реализуемость». Труды Американского математического общества . 75 (1): 1–19. дои : 10.2307/1990776 . JSTOR  1990776.

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

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