Введение

В математической логике интерпретация Брауэра — Хейтинга — Колмогорова, или БХК-интерпретация, интуиционистской логики была предложена Л. Э. Ж. Брауэром и Арендом Хейтингом, а также независимо Андреем Колмогоровым. Она также иногда называется интерпретацией реализуемости из-за связи с теорией реализуемости Стивена Клини. Это стандартное толкование интуиционистской логики.

Интерпретация

В интерпретации указывается, что должно быть доказательством данной формулы. Это определяется индукцией по структуре этой формулы:

Доказательство ¬A – это пара <B, C>, где B – доказательство A, а C – доказательство ⊥.
Доказательство A ∧ B – это либо <A, C>, где C – доказательство B, либо <B, C>, где C – доказательство A.
Доказательство A ∨ B – это функция, преобразующая доказательство A в доказательство B.
Доказательство A → B – это пара <A, C>, где A – элемент домена, а C – доказательство B.
Доказательство ∀x.A – это функция, преобразующая элемент x из домена в доказательство A.
Формулу ⊥ определяют как ¬¬A, поэтому доказательство ⊥ – это функция, преобразующая доказательство A в доказательство ¬A.
Доказательства ⊥ не существует, это абсурд или нижний тип (неокончание в некоторых языках программирования).
Интерпретация примитивного высказывания предполагается известной из контекста. В контексте арифметики доказательство формулы a = b – это вычисление, приводящее оба терма к одному и тому же числу. Колмогоров придерживался тех же принципов, но формулировал свою интерпретацию в терминах задач и решений. Утверждать формулу – значит заявлять, что известно решение задачи, представленной этой формулой. Например, a = b – это задача сведения a к b; для её решения требуется метод решения задачи a, при условии решения задачи b.

Определение абсурда

В общем случае, логическая система не может иметь формального оператора отрицания, при котором существовало бы доказательство "не" ровно тогда, когда не существует доказательства ; см. теоремы о неполноте Гёделя. Интерпретация BHK вместо этого понимает "не" как приведение к абсурду, обозначаемому , так что доказательство является функцией, преобразующей доказательство в доказательство абсурда. Классический пример абсурда встречается при работе с арифметикой. Предположим, что 0 = 1, и применим математическую индукцию: 0 = 0 по аксиоме равенства. Теперь (по гипотезе индукции), если 0 было бы равно некоторому натуральному числу n, то 1 было бы равно n + 1 (аксиома Пеано: Sm = Sn тогда и только тогда, когда m = n), но поскольку 0 = 1, то 0 также было бы равно n + 1. Следовательно, по индукции, 0 равно любому числу, и, как следствие, любые два натуральных числа становятся равными. Таким образом, существует способ перейти от доказательства 0 = 1 к доказательству любого базового арифметического равенства и, следовательно, к доказательству любого сложного арифметического утверждения. Более того, для получения этого результата не требовалось апеллировать к аксиоме Пеано, утверждающей, что 0 "не" является преемником какого-либо натурального числа. Это делает 0 = 1 подходящим в качестве в арифметике Хейтинга (а аксиома Пеано переписывается как 0 = Sn → 0 = S0). Такое использование 0 = 1 подтверждает принцип взрыва.

Определение функции

Интерпретация БХК будет зависеть от того, как понимать функцию, преобразующую одно доказательство в другое, или преобразующую элемент области определения в доказательство. Различные версии конструктивизма расходятся во мнениях по этому вопросу. Теория реализуемости Клини отождествляет функции с вычислимыми функциями. Она рассматривает арифметику Гейтинга, где область квантификации – натуральные числа, а примитивные высказывания имеют вид x = y. Доказательство x = y – это просто тривиальный алгоритм, если x вычисляется в то же число, что и y (что всегда разрешимо для натуральных чисел), иначе доказательства не существует. Затем из них, посредством индукции, строятся более сложные алгоритмы. Если исходить из того, что лямбда-исчисление определяет понятие функции, то интерпретация БХК описывает соответствие между натуральной дедукцией и функциями.