В математической логике реализуемость — это совокупность методов теории доказательств, используемых для изучения конструктивных доказательств и извлечения из них дополнительной информации. [1] Формулы из формальной теории «реализуются» объектами, известными как «реализаторы», таким образом, что знание реализатора дает знание об истинности формулы. Есть много вариантов реализуемости; какой именно класс формул изучается и какие объекты являются реализаторами, различаются от одной вариации к другой.
Реализуемость можно рассматривать как формализацию интерпретации интуиционистской логики БХК; в реализуемости понятие «доказательство» (оставленное неопределенным в интерпретации БХК) заменяется формальным понятием «реализатор». Большинство вариантов реализуемости начинаются с теоремы о том, что любое утверждение, доказуемое в изучаемой формальной системе, реализуемо. Однако реализатор обычно дает больше информации о формуле, чем прямое формальное доказательство.
Помимо понимания интуиционистской доказуемости, реализуемость может быть применена для доказательства свойств дизъюнкции и существования для интуиционистских теорий и для извлечения программ из доказательств, как при добыче доказательств . Это также связано с теорией топоса через топос реализуемости .
Первоначальная версия реализуемости Клини использует натуральные числа в качестве реализаторов для формул в арифметике Гейтинга . Требуется несколько элементов записи: во-первых, упорядоченная пара ( n , m ) обрабатывается как одно число с использованием фиксированной примитивно-рекурсивной функции сопряжения ; во- вторых, для каждого натурального числа n φ n является вычислимой функцией с индексом n . Следующие пункты используются для определения отношения « n реализует A » между натуральными числами n и формулами A.на языке арифметики Гейтинга, известной как отношение реализуемости Клини 1945 года: [2]
С другой стороны, есть формулы, которые реализуются, но недоказуемы в HA, факт, впервые установленный Роузом. [4]
Дальнейший анализ метода может быть использован для доказательства того, что HA обладает « свойствами дизъюнкции и существования »: [5]