Реализуемость
В математической логике реализуемость — это совокупность методов теории доказательств, используемых для изучения конструктивных доказательств и извлечения из них дополнительной информации. [1] Формулы формальной теории «реализуются» объектами, известными как «реализаторы», таким образом, что знание реализующего дает знание об истинности формулы. Существует множество вариантов реализуемости; какой именно класс формул изучается и какие объекты являются реализаторами, различаются от одной вариации к другой.
Реализуемость можно рассматривать как формализацию БГК-интерпретации интуиционистской логики ; в реализуемости понятие «доказательство» (которое в интерпретации БГК остается неопределенным) заменяется формальным понятием «реализатор». Большинство вариантов реализуемости начинается с теоремы о том, что любое утверждение, доказуемое в изучаемой формальной системе, реализуемо. Однако реализатор обычно дает больше информации о формуле, чем могло бы дать непосредственно формальное доказательство.
Помимо понимания интуиционистской доказуемости, реализуемость может применяться для доказательства свойств дизъюнкции и существования интуиционистских теорий, а также для извлечения программ из доказательств, как при интеллектуальном анализе доказательств . Это также связано с теорией топоса через топосы реализуемости .
: реализуемость Клини в 1945 году . Пример
арифметике Первоначальная версия реализуемости Клини использует натуральные числа в качестве реализаторов формул в Хейтинга . Требуется несколько обозначений: во-первых, упорядоченная пара ( n , m ) рассматривается как одно число с использованием фиксированной примитивно-рекурсивной функции спаривания ; во-вторых, для каждого натурального числа n φ n — вычислимая функция с индексом n . Следующие предложения используются для определения отношения « n реализует A » между натуральными числами n и формулами A на языке арифметики Хейтинга, известного как отношение реализуемости Клини 1945 года: [2]
- Любое число n реализует атомарную формулу s = t тогда и только тогда, когда s = t истинно. Таким образом, каждое число реализует истинное уравнение, и ни одно число не реализует ложное уравнение.
- Пара ( n , m ) реализует формулу A ∧ B тогда и только тогда, когда реализует A , а m реализует B. n Таким образом, реализатор конъюнкта — это пара реализаторов конъюнктов.
- Пара ( 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. или
Другие подобные свойства можно получить с помощью формул Харропа .
Дальнейшие события [ править ]
Крейзель представил модифицированную реализуемость , которая использует типизированное лямбда-исчисление в качестве языка реализаций. Модифицированная реализуемость — один из способов показать, что принцип Маркова не выводится в интуиционистской логике. Напротив, это позволяет конструктивно обосновать принцип независимости посылок :
- .
Относительная реализуемость [6] - это интуиционистский анализ рекурсивных или рекурсивно перечислимых элементов структур данных, которые не обязательно вычислимы, например, вычислимые операции над всеми действительными числами, когда действительные числа могут быть только аппроксимированы в цифровых компьютерных системах.
Приложения [ править ]
Реализуемость — это один из методов, используемых при поиске доказательств для извлечения конкретных «программ» из, казалось бы, неконструктивных математических доказательств. Извлечение программы с использованием реализуемости реализовано в некоторых помощниках по доказательству, таких как Coq .
См. также [ править ]
Примечания [ править ]
Ссылки [ править ]
- Биркедал, Ларс; Яап ван Остен (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 .
Внешние ссылки [ править ]
- Реализуемость Коллекция ссылок на недавние статьи по реализуемости и смежным темам.