Арифметика Гейтинга

В 1930 г. А. Гейтинг предложил формализованные исчисления: интуиционистской логики высказываний IL, интуиционистской логики предикатов и интуиционистской арифметики НА. Такая формализация противоречила основному принципу интуиционизма, выдвинутого Л. Я. Брауэром и утверждающему интуитивную ясность математических доказательств. Но возник ряд вопросов метаматематического характера, решить которые без точного очерчивания границ соответствующих теорий не представлялось возможным. Работа над этими вопросами привела к созданию аксиоматической системы теории множеств, основанной на интуиционистской логике. Формализованные теории решали эти задачи успешно^[2]. Получались эти теории из соответствующих классических исчислений в результате отказа от законов исключённого третьего, (снятия) двойного отрицания, косвенного доказательства (доказательства от противного).

НА характеризуется точно так же, как логика первого порядка арифметики Пеано (в дальнейшем ${\displaystyle {\mathsf {PA}}}$ — Peano Arithmetic), получаемая заменой аксиомы индукции системой аксиом на языке логики первого порядка и добавлением символов операций сложения и умножения, за исключением того, что НА использует интуиционистское исчисление предикатов. В частности, это означает, что закон двойного отрицания, а также закон исключённого третьего отсутствуют. ${\displaystyle {\mathsf {PA}}}$ строго сильнее, чем НА в том смысле, что все НА-теоремы являются также и РА-теоремами^[3].

Интуиционистская арифметика Гейтинга HA задаётся теми же аксиомами, что и арифметика Пеано PA, но над FO-Int вместо FO-CL. Сигнатура та же: =, 𝑆, +, ⋅.

НА охватывает аксиомы ${\displaystyle {\mathsf {PA}}}$, в случае, если предполагаемой моделью является множество натуральных чисел ${\displaystyle {\mathbb {N} }}$. Источник включает «${\displaystyle 0}$», а преемник «${\displaystyle S}$», и теории характеризуют сложение и умножение. Это влияет на логику: c ${\displaystyle 1:=S0}$, это метатеорема, в которой ${\displaystyle \bot }$ может быть определено как ${\displaystyle 0=1}$ и тогда ${\displaystyle \neg P}$ такое, что ${\displaystyle P\to \bot }$ для каждого утверждения ${\displaystyle P}$. Отрицание ${\displaystyle \bot }$ означает ${\displaystyle P\to P}$ и, таким образом, является тривиальным утверждением.

Для терминов запись ${\displaystyle s\neq t}$ означает ${\displaystyle \neg (s=t)}$. На определённый срок ${\displaystyle t}$, равенство ${\displaystyle t=t}$ верно в силу рефлексивности и утверждение ${\displaystyle P}$эквивалентно ${\displaystyle (t=t)\to P}$. Можно показать, что ${\displaystyle P\lor Q}$ может быть определён как ${\displaystyle \exists n.(n=0\to P)\land (n\neq 0\to Q)}$. Это формальное исключение дизъюнкций было невозможно в примитивно рекурсивной арифметике ${\displaystyle {\mathsf {PRA}}}$ без кванторов. Теория может быть расширена функциональными символами для любой примитивной рекурсивной функции, делая ${\displaystyle {\mathsf {PRA}}}$ частью этой теории. Для общей функции ${\displaystyle f}$, часто рассматривают предикаты ${\displaystyle f(n)=0}$.

аксиомы равенства EqAr;

определяющие аксиомы для функциональных символов:

¬ 0 = 𝑆𝑥; 𝑆𝑥 = 𝑆𝑦 → 𝑥 = 𝑦; 𝑥 + 0 = 𝑥; 𝑥 + 𝑆𝑦 = 𝑆(𝑥 + 𝑦); 𝑥 ⋅ 0 = 0; 𝑥 ⋅ (𝑆𝑦) = (𝑥 ⋅ 𝑦) + 𝑥;

индукция: (𝜑(0, ⃗𝑦) ∧ ∀𝑥 (𝜑(𝑥, ⃗𝑦) → 𝜑(𝑆𝑥, ⃗𝑦))) → ∀𝑧 𝜑(𝑧, ⃗𝑦).

Аксиоматика HA не включает разрешимость равенства, но она доказуема по индукции.

Согласно правилу взрыва, действующего в любой интуиционистской теории, если ${\displaystyle \neg \neg P}$ является теоремой для некоторых ${\displaystyle P}$, то по определению ${\displaystyle \neg P}$ доказуема тогда и только тогда, когда теория непоследовательна. Действительно, в арифметике Гейтинга двойное отрицание явно выражает ${\displaystyle \neg P\to 0=1}$. Для предиката ${\displaystyle Q}$, теорема вида ${\displaystyle \neg \neg \exists n.Q(n)}$ выражает несовместимость, чтобы в исключении того, что ${\displaystyle Q(t)}$ могло бы быть действительным для некоторых ${\displaystyle t}$. Конструктивно это слабее, чем утверждение о существовании такого ${\displaystyle t}$. Большая часть метатеоретической дискуссии будет посвящена классически доказуемым утверждениям о существовании. Двойное отрицание ${\displaystyle \neg \neg P}$ влечёт за собой ${\displaystyle (\alpha \to \neg P)\to (\alpha \to 0=1)}$. Тогда теорема вида ${\displaystyle \neg \neg P}$ приводит новые доказательства для окончательного опровержения (в том числе позитивных) утверждений ${\displaystyle \alpha }$.

В ${\displaystyle {\mathsf {HA}}\vdash \alpha \to \neg \neg \alpha }$ может быть классически обратным и в ${\displaystyle {\mathsf {HA}}\vdash {\big (}\exists n.\neg \psi (n){\big )}\to \neg \forall n.\psi (n)}$. В этом отличие между существованием числовых контрпримеров и абсурдными выводами при допущении справедливости для всех чисел. Вставка витков с двойным отрицанием ${\displaystyle {\mathsf {PA}}}$-теорем в ${\displaystyle {\mathsf {HA}}}$-теоремы. Точнее, для любой формулы, доказуемой в ${\displaystyle {\mathsf {PA}}}$, классически эквивалентный отрицательный перевод формулы Гёделя — Генцена уже доказан в ${\displaystyle {\mathsf {HA}}}$. В одной из формулировок процедура перевода включает в себя переписывание ${\displaystyle {\big (}\exists n.Q(n){\big )}^{N}}$в ${\displaystyle \neg \forall n.\neg Q^{N}(n).}$ В результате все арифметические теоремы Пеано имеют доказательство, состоящее из конструктивного доказательства, за которым следует классическое логическое переписывание. Грубо говоря, последний шаг сводится к применению устранения двойного отрицания.

В частности, при отсутствии неразрешимых атомарных предложений для любого предложения ${\displaystyle \psi }$ не включая экзистенциальные квантификации или дизъюнкции вообще, имеем ${\displaystyle {\mathsf {PA}}\vdash \psi \iff {\mathsf {HA}}\vdash \psi }$.

Минимальная логика доказывает устранение двойного отрицания для отрицаемых формул ${\displaystyle \neg \neg (\neg \alpha )\leftrightarrow (\neg \alpha )}$. Арифметика Гейтинга доказывает эту классическую эквивалентность для любой формулы Харропа.

И результаты ${\displaystyle \Sigma _{1}^{0}}$ показывают следующее: принцип Маркова на самом низком уровне арифметической иерархии является допустимым правилом вывода, в том числе для ${\displaystyle \varphi }$ с ${\displaystyle n}$: ${\displaystyle {\mathsf {HA}}\vdash \neg \neg \exists m.\varphi (n,m)\iff {\mathsf {HA}}\vdash \exists m.\varphi (n,m)}$.

Не упоминая о предикатах без кванторов, можно эквивалентно сформулировать для примитивного рекурсивного предиката или Т-предиката Клини, называемого ${\displaystyle {\mathrm {MR} }_{\mathrm {QF} }}$, соотв. ${\displaystyle {\mathrm {MR} _{\mathrm {PR} }}}$ и ${\displaystyle {\mathrm {MR} _{0}}}$. Даже связанное правило ${\displaystyle {\mathrm {MR} }_{\mathrm {Dec} }}$ допустимо, в котором аспект управляемости ${\displaystyle \varphi }$ без основания, например, на синтаксическом условии, но где левая часть также требует ${\displaystyle \vdash \forall m.\varphi (n,m)\lor \neg \varphi (n,m)}$.

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

Как и в случае с другими теориями интуиционистской логики, различные примеры ${\displaystyle {\mathrm {PEM} }}$ может быть доказано в этой конструктивной арифметике. С помощью принципа дизъюнкции, всякий раз, когда высказывание ${\displaystyle P}$, либо ${\displaystyle \neg P}$ доказано, то доказано и ${\displaystyle P\lor \neg P}$ . Например, для ${\displaystyle 0=0}$ и ${\displaystyle \forall n.Sn\neq 0}$ из аксиом, можно подтвердить возможность индукции исключённого третьего для предиката ${\displaystyle n=0}$. Тогда равенство нулю разрешимо. Действительно, ${\displaystyle {\mathsf {HA}}}$ доказывает равенство «${\displaystyle =}$» разрешимо для всех чисел, то есть ${\displaystyle \forall n.\forall m.(n=m\lor n\neq m)}$. Более строго, поскольку равенство является единственным предикатным символом в арифметике Гейтинга, отсюда следует, что для любой формулы ${\displaystyle \phi }$ без кванторов, где ${\displaystyle n,\dots ,m}$являются свободными переменными, теория замкнута по правилу ${\displaystyle {\mathsf {HA}}\vdash \forall n.\cdots \forall m.\,\phi (n,\dots ,m)\lor \neg \phi (n,\dots ,m)}$.

Любая теория, основанная на минимальной логике, доказывает ${\displaystyle \neg \neg (P\lor \neg P)}$ для всех высказываний. Так что если теория непротиворечива, она никогда не доказывает отрицание исключённого третьего утверждения.

На практике, в довольно консервативных конструктивных рамках, таких как ${\displaystyle {\mathsf {HA}}}$, когда понятно, какой тип утверждений алгоритмически разрешим, то результат недоказуемости исключённого третьего дизъюнкции выражает алгоритмическую неразрешимость ${\displaystyle P}$.

Для простых утверждений, эта теория не просто подтверждает такие классически допустимые бинарные дихотомии как ${\displaystyle \phi (n,\dots )\lor \neg \phi (n,\dots )}$. Можно использовать перевод Фридмана для подтверждения того, что теоремы ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle \Pi _{2}^{0}}$ — доказаны ${\displaystyle {\mathsf {HA}}}$: для любого ${\displaystyle n}$ и ${\displaystyle \varphi }$ без квантификаторов

${\displaystyle {\mathsf {PA}}\vdash \exists m.\varphi (n,m)\iff {\mathsf {HA}}\vdash \exists m.\varphi (n,m)}$.

Этот результат может быть выражен и с помощью явных универсальных замыканий ${\displaystyle \forall n}$. Простые утверждения о вычислимых отношениях, доказуемые классически, уже доказуемы конструктивно. Хотя в проблемах остановки не только утверждения без кванторов, но и ${\displaystyle \Pi _{1}^{0}}$-утверждения играют важную роль и могут быть даже классически независимыми. Аналогично, уже уникальное существование ${\displaystyle \exists !n.Q(n)}$ в бесконечной области, то есть ${\displaystyle \exists n.\forall w.{\big (}n=w\leftrightarrow Q(w){\big )}}$, формально не является особенно простым.

Итак, ${\displaystyle {\mathsf {PA}}}$ является ${\displaystyle \Pi _{2}^{0}}$ — консервативен как ${\displaystyle {\mathsf {HA}}}$. Для контраста, в то время как классическая теория арифметики Робинсона ${\displaystyle {\mathsf {Q}}}$ доказывает все ${\displaystyle \Sigma _{1}^{0}}$-${\displaystyle {\mathsf {PA}}}$-теоремы, некоторые простые some simple ${\displaystyle \Pi _{1}^{0}}$-${\displaystyle {\mathsf {PA}}}$-теоремы независимы от него. Индукция также играет решающую роль в результате Фридмана: например, более работоспособная теория, полученная путём усиления ${\displaystyle {\mathsf {Q}}}$ с аксиомами о порядке и опционально разрешимым равенством, доказывает больше ${\displaystyle \Pi _{2}^{0}}$-утверждений, чем его интуиционистский аналог.

Независимые результаты касаются таких высказываний, что ни они, ни их отрицания не могут быть доказаны в теории. Если классическая теория непротиворечива (то есть не доказывает ${\displaystyle \bot }$) и конструктивный аналог не доказывает ни одну из классических теорем ${\displaystyle P}$, то не зависит от последующего ${\displaystyle P}$. При наличии некоторых независимых высказываний легко определить бо́льшее из них, особенно в конструктивной структуре.

Арифметика Гейтинга имеет свойство дизъюнкции ${\displaystyle {\mathrm {DP} }}$ — для всех выражений ${\displaystyle \alpha }$ и ${\displaystyle \beta }$^[4]:

${\displaystyle {\mathsf {HA}}\vdash \alpha \lor \beta \iff {\mathsf {HA}}\vdash \alpha {\text{ or }}{\mathsf {HA}}\vdash \beta }$.

Данное утверждение и его численное обобщение также подтверждаются конструктивной арифметикой второго порядка и общими теориями множеств. Следуя принципам дизъюнкции, если высказывание ${\displaystyle P}$ независимо, то классически тривиально ${\displaystyle P\lor \neg P}$ — другое независимое высказывание, и наоборот. Схема не действует, если существует хотя бы один случай, который не может быть доказан, тогда закон ${\displaystyle {\mathrm {PEM} }}$ не действует.

Для определения типа высказыаний как ${\displaystyle {\mathsf {PA}}}$-доказуемо, но не ${\displaystyle {\mathsf {HA}}}$-доказуемо используют теоремы Гёделя о неполноте.

Решение десятой проблемы Гильберта дало некоторые конкретные многочлены ${\displaystyle f}$ и соответствующие Диафантовы уравнения, такие, что утверждение о том, что последние имеют решение, алгоритмически неразрешимо. Высказывание можно выразить:

${\displaystyle \exists w_{1}.\cdots \exists w_{n}.f(w_{1},\dots ,w_{n})=0}$.

В последовательной и обоснованной арифметической теории высказывание о существовании ${\displaystyle {\mathrm {I} _{f}}}$ является независимым ${\displaystyle \Sigma _{1}^{0}}$-утверждение. Тогда, ${\displaystyle {\mathrm {C} _{f}}:=\neg {\mathrm {I} _{f}}}$ проводя отрицание через квантификатор, получим независимую проблему Гольдбаха или ${\displaystyle \Pi _{1}^{0}}$-предложение. Точнее, двойное отрицание${\displaystyle \neg \neg {\mathrm {I} _{f}}}$ (или ${\displaystyle \neg {\mathrm {C} _{f}}}$) также независимо. И любое тройное отрицание, в любом случае, уже интуиционистски эквивалентно одинарному отрицанию.

Используя принципы минимальной логики, можно доказать все утверждения о непротиворечивости, и в частности: ${\displaystyle \neg ({\mathrm {I} _{f}}\land \neg {\mathrm {I} _{f}})}$ и ${\displaystyle \neg ({\mathrm {C} _{f}}\land \neg {\mathrm {C} _{f}})}$. Поскольку также ${\displaystyle ({\mathrm {C} _{f}}\land \neg {\mathrm {C} _{f}})\leftrightarrow \neg ({\mathrm {I} _{f}}\lor \neg {\mathrm {I} _{f}})}$, теорема ${\displaystyle \neg ({\mathrm {C} _{f}}\land \neg {\mathrm {C} _{f}})}$ может быть прочитана как доказуемая двойного отрицания, исключения третьего и (утверждение о существовании). Но по свойству дизъюнкции, простой принцип исключённая третьего ${\displaystyle {\mathrm {C} _{f}}\lor \neg {\mathrm {C} _{f}}}$ не может быть ${\displaystyle {\mathsf {HA}}}$-доказуем. Таким образом, один из законов Де Моргана также не может быть интуиционистски справедлив в общем случае.

Расхождение принципов ${\displaystyle {\mathrm {WPEM} }}$ и ${\displaystyle {\mathrm {WLPO} }}$ было объяснено. Теперь в ${\displaystyle {\mathsf {PA}}}$, принцип наименьшего числа является лишь одним из многих утверждений, эквивалентных принципу индукции. В свете доказательства Гёделя, нарушение этих трёх принципов можно понимать как соответствие арифметики Гейтинга доказуемому прочтению конструктивной логики.

Принцип Маркова для примитивно-рекурсивных предикатов ${\displaystyle {\mathrm {MP} _{\mathrm {PR} }}}$ уже не имеет места как схема импликации для ${\displaystyle {\mathsf {HA}}}$, не говоря уже о строго более сильном ${\displaystyle {\mathrm {MP} _{\mathrm {Dec} }}}$, хотя в форме соответствующих правил они допустимы. Аналогично, теория не доказывает принцип независимости предпосылок ${\displaystyle {\mathrm {IP} }}$ для отрицаемых предикатов, хотя он замкнут по правилу для всех отрицаемых высказываний, то есть можно выдвинуть квантор существования в ${\displaystyle \neg P\to \exists n.Q(n)}$. То же самое относится и к версии, где экзистенциальное утверждение заменено простой дизъюнкцией.

Действующий смысл выражения ${\displaystyle \neg \neg (\alpha \to \beta )\to (\alpha \to \neg \neg \beta )}$ может быть доказан и в обратной форме, используя дизъюнктивный силлогизм. Однако с заменой двойного отрицания ${\displaystyle DNS}$ выражение не является интуиционистски доказуемым.

Используя зависимость порядка следования натуральных чисел, принцип полной индукции гласит:

${\displaystyle \forall n.{\Big (}{\big (}\forall (k<n).\phi (k){\big )}\,\to \,\phi (n){\Big )}\,\to \,\forall m.\phi (m)}$

В нотации классов, известной из теории множеств, арифметическое выражение ${\displaystyle Q(n)}$ записывается как ${\displaystyle n\in B}$, где ${\displaystyle B:=\{m\in {\mathbb {N} }\mid Q(m)\}}$. Для любого данного предиката отрицательной формы ${\displaystyle \phi (n):=\neg (n\in B)}$, логическим эквивалентом индукции является:

${\displaystyle \neg \exists (n\in B).\neg \exists (k\in B).k<n\,\,\,\leftrightarrow \,\,\,B=\{\}}$.

Идея заключается в том, что среди подклассов ${\displaystyle B\subseteq {\mathbb {N} }}$, свойство (доказуемо) не иметь наименьшего члена эквивалентно необитаемости, то есть пустому классу. Принимая противоположные результаты, получаем теорему, выражающую, что для любого непустого подкласса нельзя последовательно исключить, что существует член ${\displaystyle n\in B}$ такой, что нет ни одного члена ${\displaystyle k\in B}$ меньше, чем ${\displaystyle n}$:

${\displaystyle B\neq \{\}\,\to \,\neg \neg \exists (n\in B).\neg \exists (k\in B).k<n}$.

В арифметике Пеано, где устранение двойного отрицания всегда допустимо, действует принцип наименьшего числа в его общей формулировке. В классическом прочтении быть непустым эквивалентно (доказуемо) быть населённым некоторым наименьшим членом.

Бинарное отношение «${\displaystyle <}$», которое подтверждает схему полной индукции, всегда является нерефлексивным: рассматривая ${\displaystyle \phi _{c}(n):=(n\neq c)}$ или эквивалентное ему ${\displaystyle Q_{c}(n):=(n=c)}$ для некоторого фиксированного числа ${\displaystyle c}$, вышеизложенное упрощается до утверждения, что нет ни одного члена ${\displaystyle k}$ из ${\displaystyle B=\{c\}}$, который ${\displaystyle k<c}$ , то есть ${\displaystyle \neg (c<c)}$. В более общем смысле, если ${\displaystyle B}$ не пустое множество, и связанный с ним (классический) принцип наименьшего числа может быть использован для доказательства некоторого утверждения отрицательной формы (например ${\displaystyle \neg (c<c)}$), то можно расширить это до полностью конструктивного доказательства. И это благодаря тому, что импликации ${\displaystyle \alpha \to \neg \beta }$ всегда интуиционистски эквивалентны формально более сильным ${\displaystyle (\neg \neg \alpha )\to \neg \beta }$.

Но в целом, по конструктивной логике, ослабление принципа наименьшего числа не может быть снято. Например: для некоторого высказывания ${\displaystyle P}$рассмотрим предикат

${\displaystyle Q_{P}(n):=(n=0\land P)\lor (n=1)}$

${\displaystyle Q_{P}}$ относится к подклассу натуральных чисел ${\displaystyle b_{P}:=\{z\in \{0\}\mid P\}\cup \{1\}}$. Каким же будет наименьший член этого класса? Любое число, доказано или предполагается, что оно принадлежит этому классу, либо равно ${\displaystyle 0}$, либо ${\displaystyle 1}$, то есть ${\displaystyle b_{P}\subseteq \{0,1\}}$. Используя разрешимость равенства и разделительный силлогизм, доказывает эквивалентность ${\displaystyle P\leftrightarrow Q_{P}(0)}$. Если основное высказывание ${\displaystyle P}$ независимо, то предикат теоретически неразрешим. Поскольку ${\displaystyle 1=1}$, высказывание ${\displaystyle Q_{P}(1)}$ тривиально верно, следовательно класс населён:${\displaystyle 1\in b_{P}}$. В частности, существование наименьшего числа для этого класса не может быть отклонено. Учитывая конъюнкцию с тривиальным ${\displaystyle Q_{P}(1)}$, утверждение о существовании наименьшего числа ${\displaystyle Q_{P}}$ подтверждает само себя и переводится, как исключённое третье для ${\displaystyle P}$. Значение такого числа фактически определяет, содержит ли его ${\displaystyle P}$ или нет. Для независимого ${\displaystyle P}$, по принципу наименьшего числа, член с ${\displaystyle Q_{P}}$ также не зависим и по ${\displaystyle {\mathsf {HA}}}$.

В нотации теории множеств, ${\displaystyle P}$ эквивалентно ${\displaystyle 0\in b_{P}}$ и тогда ${\displaystyle b_{P}=\{0,1\}}$, в то время как его отрицание также эквивалентно ${\displaystyle b_{P}=\{1\}}$. Это показывает, что неуловимые предикаты могут определять неуловимые подмножества. И также в конструктивной теории множеств, хотя стандартный порядок в классе натуральных чисел разрешим, натуральные числа не являются вполне упорядоченными . Но также действуют и сильные принципы индукции, которые конструктивно не подразумевают нереализуемых утверждений о существовании.

В вычислимом контексте для предиката ${\displaystyle M}$, классически тривиальная бесконечная дизъюнкция:

${\displaystyle \forall n.{\big (}M(n)\lor \neg M(n){\big )}}$,

также записывается ${\displaystyle {\mathrm {Dec} }_{M}}$ и читается как подтверждение разрешимости проблемы принятия решения. В нотации классов ${\displaystyle M(n)}$ также записывается как ${\displaystyle n\in M}$.

${\displaystyle {\mathsf {HA}}}$ не доказывает никаких высказываний, которые нельзя доказать с помощью ${\displaystyle {\mathsf {PA}}}$ и поэтому, в частности, она не отвергает никаких теорем классической теории. Но существуют такие предикаты ${\displaystyle M}$, что аксиомы ${\displaystyle {\mathsf {HA}}+\neg {\mathrm {Dec} }_{M}}$ являются последовательными. Такое отрицание не эквивалентно существованию конкретного числового примера ${\displaystyle t}$ к исключённому третьему для ${\displaystyle M(t)}$. Действительно, уже минимальная логика доказывает двойное отрицание и исключённое третье для всех высказываний, и поэтому ${\displaystyle \forall n.\neg \neg {\big (}Q(n)\lor \neg Q(n){\big )}}$, что эквивалентно для любого предиката ${\displaystyle Q}$.

Если теория последовательна, то нет доказательство её абсурдности. Курт Гёдель, используя отрицание, доказал, что если арифметика Гейтинга последовательна, то последовательна и арифметика Пеано. Он сократил задачу непротиворечивости ${\displaystyle {\mathsf {PA}}}$ для ${\displaystyle {\mathsf {HA}}}$. Однако теоремы Гёделя о неполноте, свидетельствующие о неспособности некоторых теорий доказать свою собственную последовательность, применимы и к самой арифметике Гейтинга.

Стандартная модель классической теории первого порядка ${\displaystyle {\mathsf {PA}}}$, а также любая из её нестандартных моделей также является моделью для арифметики Гейтинга.

Существуют конструктивные модели теории множеств для полногоl ${\displaystyle {\mathsf {HA}}}$ и его предполагаемая семантика. Относительно достаточно слабых теорий множеств: они должны принять аксиому бесконечности, аксиоматическую схему предикативного разделения, чтобы доказать индукцию арифметических формул в ${\displaystyle \omega }$, а также существование функциональных пространств на конечных областях для рекурсивных определений.

В частности, эти теории не требуют ${\displaystyle {\mathrm {PEM} }}$, ни полной аксиомы выбора или индукции множеств (не говоря уже об аксиоме регулярности), ни общих функциональных пространств (не говоря уже о полной аксиоме степени).

${\displaystyle {\mathsf {HA}}}$ — дву-интерпретируема со слабой конструктивной теорией множеств, в которой класс ординалов ${\displaystyle \omega }$ такой, что набор натуральных чисел фон Неймана не существует в теории множеств^[5]. Область этой теории так же велика, как класс её ординалов и по существу она задана через класс ${\displaystyle {\mathrm {Fin} }}$ всех множеств, которые находятся во взаимно однозначном соответствии с естественным ${\displaystyle n\in \omega }$. Аксиома названа ${\displaystyle V={\mathrm {Fin} }}$, а другие аксиомы связаны с алгеброй множеств и порядком: объединение и бинарное пересечение, которые тесно связаны со схемой предикативного разделения, экстенсиональностью, парностью и схемой индукции множеств. Эта теория идентична теории, заданной ${\displaystyle {\mathsf {CZF}}}$ без Строгой Бесконечности и с добавлением аксиомы конечности. Обсуждение ${\displaystyle {\mathsf {HA}}}$ в этой теории множеств как в теории моделей. И в другом направлении аксиомы теории множеств доказываются относительно примитивно-рекурсивного отношения:

${\displaystyle x\in y\iff \exists (r<2^{x}).\exists (s<y).{\big (}2^{x}(2s+1)+r=y{\big )}}$.

Для некоторого числа ${\displaystyle \mathrm {n} }$ в метатеории, число в изучаемой теории объекта обозначается ${\displaystyle {\underline {\mathrm {n} }}}$.

В интуиционистской арифметике свойство дизъюнкции ${\displaystyle {\mathrm {DP} }}$ является допустимым. Существует теорема, что любое расширение арифметики, для которого она выполняется, также имеет числовое свойство существования ${\displaystyle {\mathrm {NEP} }}$:

${\displaystyle {\mathsf {HA}}\vdash \exists n.\psi (n)\iff {\text{ exists }}{\mathrm {n} }{\text{ }}{\mathsf {HA}}\vdash \psi ({\underline {\mathrm {n} }})}$

Эти свойства металогически эквивалентны в арифметике Гейтинга. Свойство существования и дизъюнкции сохраняется при релятивизации утверждения о существовании с помощью формулы Харропа ${\displaystyle \alpha }$, то есть для доказуемого ${\displaystyle \alpha \to \exists n.\psi (n)}$.

С. К. Клини представил важные модели реализуемости арифметики Гейтинга. Вывод в арифметике Гейтинга сохраняет реализуемость: если ${\displaystyle {\mathsf {HA}}\vdash \forall n.\exists m.\varphi (n,m)}$ — частично рекурсивная функция, реализующая ${\displaystyle \varphi }$, то всякий раз, когда функция оценивается в ${\displaystyle {\mathrm {n} }}$ заканчивается на ${\displaystyle {\mathrm {m} }}$, следует ${\displaystyle {\mathsf {HA}}\vdash \varphi ({\underline {\mathrm {n} }},{\underline {\mathrm {m} }})}$. Это можно распространить на любое конечное число ${\displaystyle {\mathrm {n} }}$ аргументов функции. Существуют также классические теоремы, которые не доказуемы в ${\displaystyle {\mathsf {HA}}}$, но имеют реализацию.

Реализации теории типов, отражающие логические формализации на основе правил вывода, нашли своё применение в системе интерактивного доказательства теорем.

Дальнейшие исследования в области формализованной интуиционистской математики сосредоточились в первую очередь вокруг арифметики НА, которая рассматривалась как базисная. Различные расширения НА — такие, как арифметика Пеано, традиционный конструктивизм A.A. Маркова-младшего, антитрадиционный конструктивизм, арифметика реализуемости и ряд других, оказались непротиворечивыми относительно базисной системы арифметики НА.

Одной из наиболее популярных трактовок интуиционистской логики является BHK — от английского написания фамилий Л.Э.Я. Брауэра, А. Гейтинга и А. Н. Колмогорова. В рамках данной неформальной семантики истинность формулы ${\displaystyle A}$ понимается как наличие доказательства данной формулы ${\displaystyle A}$. В свою очередь, ложность формулы понимается следующим образом: допущение о наличии доказательства формулы ${\displaystyle A}$ вед`ёт к противоречию. Можно заключить, что формула ложная, только лишь исходя из того, что не найдено её доказательство. Ложность формулы требует отдельного доказательства путём сведения к абсурду. Таким образом, получают дизъюнктивное свойство: чтобы построить доказательство дизъюнкции ${\displaystyle A\lor B}$, нужно иметь доказательство хотя бы одного из дизъюнктов (или ${\displaystyle A}$, или ${\displaystyle B}$). В связи с этим пониманием дизъюнкции перестаёт быть аксиомой, действует закон исключённого третьего.

Колмогоров следовал тем же путём, но сформулировал свою интерпретацию в терминах проблем и решений. Утверждать формулу — значит утверждать, что знаешь решение проблемы, представленной этой формулой.