Интерпретация Брауэра-Гейтинга-Колмогорова

В математической логике интерпретация Брауэра –Гейтинга–Колмогорова , или интерпретация BHK , интуиционистской логики была предложена Л. Э. Дж. Брауэром и Арендом Гейтингом , и независимо Андреем Колмогоровым . Иногда её также называют интерпретацией реализуемости из-за связи с теорией реализуемости Стивена Клини . Это стандартное объяснение интуиционистской логики. ^[1]

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

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

• Доказательство — это пара, где — доказательство и — доказательство . ${\displaystyle P\wedge Q}$ ${\displaystyle \langle a,b\rangle }$ ${\displaystyle a}$ ${\displaystyle P}$ ${\displaystyle b}$ ${\displaystyle Q}$
• Доказательство чего-либо — это либо где есть доказательство чего-либо , либо где есть доказательство чего-либо . ${\displaystyle P\vee Q}$ ${\displaystyle \langle 0,a\rangle }$ ${\displaystyle a}$ ${\displaystyle P}$ ${\displaystyle \langle 1,b\rangle }$ ${\displaystyle b}$ ${\displaystyle Q}$
• Доказательство — это функция ^{[ Explain ]} , которая преобразует доказательство в доказательство . ${\displaystyle P\to Q}$ ${\displaystyle f}$ ${\displaystyle P}$ ${\displaystyle Q}$
• Доказательством является пара , где является элементом и является доказательством . ${\displaystyle (\exists x{\in }S)(Px)}$ ${\displaystyle \langle x,a\rangle }$ ${\displaystyle x}$ ${\displaystyle S}$ ${\displaystyle a}$ ${\displaystyle Px}$
• Доказательство — это функция , которая преобразует элемент в доказательство . ${\displaystyle (\forall x{\in }S)(Px)}$ ${\displaystyle f}$ ${\displaystyle x}$ ${\displaystyle S}$ ${\displaystyle Px}$
• Формула определена как , поэтому ее доказательство — это функция , которая преобразует доказательство в доказательство . ${\displaystyle \neg P}$ ${\displaystyle P\to \bot }$ ${\displaystyle f}$ ${\displaystyle P}$ ${\displaystyle \bot }$
• Нет никаких доказательств , абсурдности или нижнего типа (незавершенности в некоторых языках программирования). ${\displaystyle \bot }$

Интерпретация примитивного предложения должна быть известна из контекста. В контексте арифметики доказательство формулы — это вычисление, сводящее два термина к одному и тому же числу. ${\displaystyle x=y}$

Колмогоров следовал тем же направлениям, но сформулировал свою интерпретацию в терминах проблем и решений. Утверждать формулу — значит утверждать, что знаешь решение проблемы, представленной этой формулой. Например, проблема сведения к ; для ее решения требуется метод решения проблемы при заданном решении проблемы . ${\displaystyle P\to Q}$ ${\displaystyle Q}$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle P}$

Примеры

Функция тождества является доказательством формулы , независимо от того, чему равно P. ${\displaystyle P\to P}$

Закон непротиворечия расширяется до : ${\displaystyle \neg (P\wedge \neg P)}$ ${\displaystyle (P\wedge (P\to \bot ))\to \bot }$

• Доказательство — это функция , которая преобразует доказательство в доказательство . ${\displaystyle (P\wedge (P\to \bot ))\to \bot }$ ${\displaystyle f}$ ${\displaystyle (P\wedge (P\to \bot ))}$ ${\displaystyle \bot }$
• Доказательство — это пара доказательств < a ,  b >, где — доказательство P , а — доказательство . ${\displaystyle (P\wedge (P\to \bot ))}$ ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle P\to \bot }$
• Доказательство — это функция, которая преобразует доказательство P в доказательство . ${\displaystyle P\to \bot }$ ${\displaystyle \bot }$

Собирая все вместе, доказательство — это функция , которая преобразует пару < a ,  b > — где — доказательство , а — функция, которая преобразует доказательство в доказательство — в доказательство . Есть функция , которая это делает, где , доказывая закон непротиворечивости, независимо от того, что такое P. ${\displaystyle (P\wedge (P\to \bot ))\to \bot }$ ${\displaystyle f}$ ${\displaystyle a}$ ${\displaystyle P}$ ${\displaystyle b}$ ${\displaystyle P}$ ${\displaystyle \bot }$ ${\displaystyle \bot }$ ${\displaystyle f}$ ${\displaystyle f(\langle a,b\rangle )=b(a)}$

На самом деле, тот же ход мыслей дает доказательство и правила modus ponens , где бы ни было какое-либо предложение. ${\displaystyle (P\wedge (P\to Q))\to Q}$ ${\displaystyle Q}$

С другой стороны, закон исключенного третьего расширяется до , и в общем случае не имеет доказательства. Согласно интерпретации, доказательство — это пара < a ,  b >, где a равно 0, а b — доказательство P , или a равно 1, а b — доказательство . Таким образом, если ни P , ни не доказуемы, то ни . ${\displaystyle P\vee (\neg P)}$ ${\displaystyle P\vee (P\to \bot )}$ ${\displaystyle P\vee (\neg P)}$ ${\displaystyle P\to \bot }$ ${\displaystyle P\to \bot }$ ${\displaystyle P\vee (\neg P)}$

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

В общем случае невозможно, чтобы логическая система имела формальный оператор отрицания, такой, что существует доказательство «не» в точности тогда, когда нет доказательства ; см. теоремы Гёделя о неполноте . Интерпретация BHK вместо этого трактует «не» как , что приводит к абсурду, обозначенному , так что доказательство является функцией, преобразующей доказательство в доказательство абсурда. ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle \bot }$ ${\displaystyle \lnot P}$ ${\displaystyle P}$

Стандартный пример абсурда можно найти в арифметике. Предположим, что 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 подтверждает принцип взрыва . ${\displaystyle \bot }$

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

Интерпретация BHK будет зависеть от точки зрения на то, что представляет собой функция , преобразующая одно доказательство в другое или преобразующая элемент домена в доказательство. Различные версии конструктивизма будут расходиться по этому вопросу.

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

Если взять лямбда-исчисление как определение понятия функции, то интерпретация BHK описывает соответствие между естественной дедукцией и функциями.

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

• Переписка Карри–Говарда

Примечания

1. Ван Аттен 2022.

Ссылки

• Троэльстра, А. (1991). «История конструктивизма в двадцатом веке» (PDF) .
• Троелстра, А. (2003). «Конструктивизм и теория доказательств (черновик)». CiteSeerX  10.1.1.10.6972 .

Внешняя ссылка

• Ван Аттен, Марк (4 мая 2022 г.). «Развитие интуиционистской логики». В Zalta, Edward N. (ред.). Стэнфордская энциклопедия философии .