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

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

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

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

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

Предполагается, что интерпретация примитивного предложения известна из контекста. В контексте арифметики доказательство формулы $x=y$ представляет собой вычисление, сводящее два термина к одному и тому же числу.

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

Примеры

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

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

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

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

Действительно, тот же ход мыслей обеспечивает доказательство modus ponens . правила $(P\wedge (P\to Q))\to Q$ а также, где $Q$ это любое предложение.

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

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

не может В общем, логическая система иметь формальный оператор отрицания, обеспечивающий доказательство «нет». $P$ именно тогда, когда нет доказательств $P$; см. теоремы Гёделя о неполноте . Интерпретация BHK вместо этого принимает «не». $P$ иметь в виду, что $P$ приводит к абсурду, обозначенному $\bot$, так что доказательство $\lnot P$ это функция, преобразующая доказательство $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 подходящим в качестве $\bot$ в арифметике Гейтинга переписана 0 = Sn (а аксиома Пеано → 0 = S 0). Такое использование 0 = 1 подтверждает принцип взрыва .

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

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

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

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

См. также

• Переписка Карри-Ховарда

Ссылки

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

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

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