В математической логике , в интерпретации Браувер-гейтингова-Колмогорова или интерпретации ВНК , из интуиционистской логики была предложена LEJ Brouwer и Гейтинг , и независимо друг от друга Андрея Колмогорова . Ее также иногда называют интерпретацией реализуемости из-за связи с теорией реализуемости Стивена Клини .
Интерпретация
Интерпретация заявляет, что должно быть доказательством данной формулы . Это определяется индукцией по структуре этой формулы:
- Доказательство пара < a , b >, где a - доказательствои b является доказательством.
- Доказательство - пара < a , b >, где a равно 0, а b - доказательство, или a равно 1 и b является доказательством.
- Доказательство это функция что превращает доказательство в доказательство .
- Доказательство - пара < a , b >, где a - элемент S , а b - доказательство.
- Доказательство это функция который превращает элемент a из S в доказательство.
- Формула определяется как , поэтому доказательством этого является функция f, которая преобразует доказательство в доказательство .
- Нет доказательств (абсурд, или нижний тип (в некоторых языках программирования не прекращение)).
Предполагается, что интерпретация примитивного предложения известна из контекста. В контексте арифметики доказательство формулы s = t - это вычисление, сводящее два члена к одной и той же цифре.
Колмогоров придерживался той же линии, но сформулировал свою интерпретацию в терминах проблем и решений. Утверждать формулу - значит утверждать, что вы знаете решение проблемы, представленной этой формулой. Напримерпроблема сведения Q к P ; решить это требует способ , чтобы решить проблему Q дано решение задачи Р .
Примеры
Функция идентичности является доказательством формулы , Независимо от того , что P есть.
Закон непротиворечия расширяется до :
- Доказательство это функция что превращает доказательство в доказательство .
- Доказательство - пара доказательств < a , b >, гдеявляется доказательством P , и является доказательством .
- Доказательство - функция, которая превращает доказательство P в доказательство.
Собирая все вместе, доказательство это функция который преобразует пару < a , b > - гдеявляется доказательством P , и- функция, которая превращает доказательство P в доказательство - в доказательство . Есть функция что делает это, где , Не доказывает закон непротиворечия, независимо от того , что P есть.
В самом деле, тот же образ мыслей дает доказательство того, что а также где это любое предложение.
С другой стороны, закон исключенного среднего расширяется до , и вообще не имеет доказательств. Согласно интерпретации, доказательство- это пара < a , b >, где a равно 0, а b - доказательство P , или a равно 1, а b - доказательство. Таким образом, если ни P, ни доказуемо, то и .
Что такое абсурд?
Для логической системы , как правило, невозможно иметь формальный оператор отрицания, такой, что существует доказательство «не». именно тогда, когда нет доказательства ; см. теоремы Гёделя о неполноте . Интерпретация BHK вместо этого принимает "не" иметь в виду, что приводит к абсурду, обозначенному , так что доказательство - функция, преобразующая доказательство в доказательство абсурда.
Стандартный пример абсурда - это арифметика. Предположим, что 0 = 1, и действуем по математической индукции : 0 = 0 по аксиоме равенства. Теперь (предположение индукции), если бы 0 был равен некоторому натуральному числу n , то 1 был бы равен n + 1 ( аксиома Пеано : S m = S n тогда и только тогда, когда m = n ), но поскольку 0 = 1 , поэтому 0 также был бы равен n + 1. По индукции 0 равен всем числам, и поэтому любые два натуральных числа становятся равными.
Следовательно, есть способ перейти от доказательства 0 = 1 к доказательству любого основного арифметического равенства и, следовательно, к доказательству любого сложного арифметического предложения. Более того, чтобы получить этот результат, не нужно было использовать аксиому Пеано, которая утверждает, что 0 «не» является преемником любого натурального числа. Это делает 0 = 1 подходящим в качествев арифметике Гейтинга (и аксиома Пеано переписывается 0 = S n → 0 = S 0). Использование 0 = 1 подтверждает принцип взрыва .
Что такое функция?
Интерпретация BHK будет зависеть от мнения о том, что составляет функцию, которая преобразует одно доказательство в другое или преобразует элемент области в доказательство. По этому поводу разные версии конструктивизма расходятся.
Теория реализуемости Клини отождествляет функции с вычислимыми функциями . Он имеет дело с арифметикой Гейтинга, где область количественной оценки - натуральные числа, а примитивные предложения имеют форму x = y . Доказательство x = y - это просто тривиальный алгоритм, если x вычисляет то же число, что и y (которое всегда разрешимо для натуральных чисел), в противном случае доказательства нет. Затем они вводятся в более сложные алгоритмы.
Если принять лямбда-исчисление как определение понятия функции, то интерпретация BHK описывает соответствие между естественным выводом и функциями.
Рекомендации
- Троэльстра, А. (1991). «История конструктивизма в двадцатом веке» (PDF) . Цитировать журнал требует
|journal=
( помощь ) - Троэльстра, А. (2003). «Конструктивизм и теория доказательств (проект)». CiteSeerX 10.1.1.10.6972 . Цитировать журнал требует
|journal=
( помощь )