Хейтинговая арифметика

В математической логике — арифметика Гейтинга. ${\mathsf {HA}}$ представляет собой аксиоматизацию арифметики в соответствии с философией интуиционизма . Он назван в честь Аренда Хейтинга , который первым его предложил.

Аксиоматизация

Арифметику Гейтинга можно охарактеризовать так же, как порядка . теорию первого арифметики Пеано ${\mathsf {PA}}$, за исключением того, что он использует интуиционистское исчисление предикатов ${\mathsf {IQC}}$ для вывода. В частности, это означает, что принцип исключения двойного отрицания, а также принцип исключенного третьего ${\mathrm {PEM} }$, не держи. Обратите внимание, что сказать ${\mathrm {PEM} }$ не выполняется в точности, означает, что исключенное среднее утверждение не является автоматически доказуемым для всех предложений — на самом деле многие такие утверждения все еще доказуемы в ${\mathsf {HA}}$ и отрицание любого такого дизъюнкция непоследовательно. ${\mathsf {PA}}$ строго сильнее, чем ${\mathsf {HA}}$ в том смысле, что все ${\mathsf {HA}}$- теоремы тоже ${\mathsf {PA}}$-теоремы.

Арифметика Хейтинга включает аксиомы арифметики Пеано, а предполагаемая модель представляет собой набор натуральных чисел. ${\mathbb {N} }$. В подписи указан ноль" $0$"и преемник" $S$", а теории характеризуют сложение и умножение. Это влияет на логику: при $1:=S0$, это метатеорема, которая $\bot$ может быть определен как $0=1$ и так что $\neg P$ является $P\to \bot$ на каждое предложение $P$. Отрицание $\bot$ имеет форму $P\to P$ и, таким образом, тривиальное предложение.

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

Теоремы

Двойные отрицания

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

Двойное отрицание $\neg \neg P$ влечет за собой $(\alpha \to \neg P)\to (\alpha \to 0=1)$. Итак, теорема вида $\neg \neg P$ также всегда дает новые средства для окончательного отклонения (также положительных) утверждений. $\alpha$.

Доказательства классически эквивалентных утверждений

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

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

Действующие принципы и правила

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

И $\Sigma _{1}^{0}$-результаты также ведут себя хорошо: правило Маркова на самом низком уровне арифметической иерархии является допустимым правилом вывода , т. е. для $\varphi$ с $n$ бесплатно,

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

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

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

Исключено среднее

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

${\mathsf {HA}}\vdash \forall n.\cdots \forall m.\,\phi (n,\dots ,m)\lor \neg \phi (n,\dots ,m)$

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

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

Консервативность

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

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

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

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

Обсуждение здесь ни в коем случае не является исчерпывающим. Существуют различные результаты, когда классическая теорема уже вытекает из конструктивной теории. Также обратите внимание, что может иметь значение, какая логика использовалась для получения металогических результатов. Например, многие результаты о реализуемости действительно были получены в конструктивной металогике. Но когда не указан конкретный контекст, заявленные результаты следует считать классическими.

Недоказуемые утверждения

Результаты независимости касаются таких предложений, что ни они, ни их отрицания не могут быть доказаны в теории. Если классическая теория непротиворечива (т.е. не доказывает $\bot$) и конструктивный аналог не доказывает ни одной из своих классических теорем $P$, тогда это $P$ не зависит от последнего. Учитывая некоторые независимые предложения, из них легко определить больше, особенно в конструктивной структуре.

Гейтинговая арифметика обладает свойством дизъюнкции. ${\mathrm {DP} }$: По всем предложениям $\alpha$ и $\beta$,

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

Действительно, это и его численное обобщение также демонстрируются в конструктивной арифметике второго порядка и теориях общих множеств, таких как ${\mathsf {CZF}}$ и ${\mathsf {IZF}}$. Это общее стремление к неформальному понятию конструктивной теории. Теперь в теории с ${\mathrm {DP} }$, если предложение $P$ независима , то классически тривиальная $P\lor \neg P$ — другое независимое суждение, и наоборот. Схема недействительна, если существует хотя бы один экземпляр, который невозможно доказать. ${\mathrm {PEM} }$ приходит неудача. Можно сломать ${\mathrm {DP} }$ путем аксиоматического принятия исключенного среднего утверждения без проверки любого из дизъюнктов, как это имеет место в случае ${\mathsf {PA}}$.

Можно сказать больше: если $P$ даже классически независимо, то и отрицание $\neg P$ независима — это справедливо независимо от того, $\neg \neg P$ эквивалентно $P$. Тогда конструктивно слабый исключил среднего. ${\mathrm {WPEM} }$ не соблюдается, т.е. принцип, согласно которому $\neg \alpha \lor \neg \neg \alpha$ справедливо для всех предложений, недействительно. Если такой $P$ является $\Sigma _{1}^{0}$, недоказуемость дизъюнкции свидетельствует о нарушении $\Pi _{1}^{0}$- ${\mathrm {PEM} }$, или что представляет собой экземпляр ${\mathrm {WLPO} }$ для примитивно-рекурсивной функции.

Классически независимые предложения

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

Решение десятой проблемы Гильберта дало некоторые конкретные полиномы. $f$ и соответствующие полиномиальные уравнения , такие, что утверждение о том, что последние имеют решение, алгоритмически неразрешимо . Предложение может быть выражено как

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

Некоторые такие утверждения о существовании нулевой ценности имеют более конкретную интерпретацию: такие теории, как ${\mathsf {PA}}$ или ${\mathsf {ZFC}}$ докажите, что эти утверждения эквивалентны арифметизированному утверждению о собственной противоречивости теорий. Таким образом, подобные предложения можно записать даже для сильных классических теорий множеств.

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

ПА нарушает ДП

Нижеследующее проясняет смысл таких независимых утверждений. Учитывая индекс в перечислении всех доказательств теории, можно проверить, доказательством какого утверждения она является. ${\mathsf {PA}}$ адекватен в том смысле, что может правильно представить эту процедуру: существует примитивный рекурсивный предикат $\mathrm {F} (w):=\mathrm {Prf} (w,\ulcorner 0=1\urcorner )$ выражая, что доказательство является одним из абсурдных предложений $0=1$. Это относится к более явному арифметическому предикату, приведенному выше, о том, что возвращаемое значение полинома равно нулю. Можно металогически рассуждать, что если ${\mathsf {PA}}$ непротиворечиво, то это действительно доказывает $\neg \mathrm {F} ({\underline {\mathrm {w} }})$ для каждого отдельного индекса ${\mathrm {w} }$.

В эффективно аксиоматизированной теории можно последовательно проверять каждое доказательство. Если теория действительно непротиворечива, то не существует доказательства абсурда, что соответствует утверждению, что упомянутый «поиск абсурда» никогда не прекратится. Формально в теории первое выражается предложением $\neg \exists w.\mathrm {F} (w)$, отрицая утверждение арифметизированной несогласованности. Эквивалент $\Pi _{1}^{0}$-предложение $\forall w.\neg \mathrm {F} (w)$ формализует непрерывность поиска, заявляя, что не все доказательства являются доказательством абсурда. И действительно, в омега-непротиворечивой теории, которая точно представляет доказуемость, нет никаких доказательств того, что поиск абсурдности когда-либо завершится остановкой (явная непротиворечивость не выводится), и, как показал Гёдель, не может быть доказательства того, что поиск абсурдности когда-либо завершится остановкой. никогда не остановится (последовательность не выводима). В переформулированной форме не существует доказательств того, что поиск абсурда никогда не прекращается (непротиворечивость не выводится), а также нет доказательств того, что поиск абсурдности никогда не прекращается (непротиворечивость не может быть отвергнута).Еще раз повторю: ни одно из этих двух дизъюнктов не является ${\mathsf {PA}}$-доказуемы, а их дизъюнкция тривиально ${\mathsf {PA}}$-доказуемый. Действительно, если ${\mathsf {PA}}$ согласовано, то оно нарушает ${\mathrm {DP} }$.

The $\Sigma _{1}^{0}$-предложение, выражающее существование доказательства $0=1$ является логически позитивным утверждением. Тем не менее, исторически оно обозначается $\neg {\mathrm {Con} }_{\mathsf {PA}}$, а его отрицание есть $\Pi _{1}^{0}$-предложение, обозначаемое ${\mathrm {Con} }_{\mathsf {PA}}$. В конструктивном контексте такое использование знака отрицания может вводить в заблуждение номенклатуру.

Фридман установил еще одно интересное недоказуемое утверждение, а именно, что непротиворечивая и адекватная теория никогда не доказывает свое арифметическое свойство дизъюнкции.

Недоказуемые классические принципы

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

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

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

Действительное значение $\neg \neg (\alpha \to \beta )\to (\alpha \to \neg \neg \beta )$ Можно доказать, что это утверждение справедливо и в его обратной форме, используя дизъюнктивный силлогизм. Однако сдвиг двойного отрицания ${\mathrm {DNS} }$ не является интуиционистски доказуемой, т. е. схема коммутативности " $\neg \neg$" с универсальной количественной оценкой по всем числам. Это интересная разбивка, которая объясняется согласованностью $\neg {\mathrm {Dec} _{M}}$ для некоторых $M$, как обсуждалось в разделе, посвященном диссертации Чёрча.

Принцип наименьшего числа

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

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

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

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

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

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

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

Бинарное отношение» $<$", которая подтверждает сильную схему индукции в приведенной выше форме, всегда также иррефлексивна: учитывая $\phi _{c}(n):=(n\neq c)$ или эквивалентно

$Q_{c}(n):=(n=c)$

за какое-то фиксированное число $c$, сказанное выше упрощается до утверждения, что ни один член $k$ из $B=\{c\}$ проверяет $k<c$, то есть $\neg (c<c)$. (И этот логический вывод даже не использовал никаких других свойств бинарного отношения.)В более общем смысле, если $B$ непусто, и связанный с ним (классический) принцип наименьшего числа можно использовать для доказательства некоторого утверждения отрицательной формы (например, $\neg (c<c)$), то это можно распространить до вполне конструктивного доказательства. Это потому, что последствия $\alpha \to \neg \beta$ всегда интуиционистски эквивалентны формально более сильным $(\neg \neg \alpha )\to \neg \beta$.

Но в целом над конструктивной логикой ослабление принципа наименьшего числа поднять невозможно. Следующий пример демонстрирует это: для некоторого предложения $P$ (сказать ${\mathrm {C} _{f}}$ как указано выше), рассмотрим предикат

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

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

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

Антиклассические расширения

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

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

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

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

Диссертация Чёрча

Правило Церкви является допустимым правилом в ${\mathsf {HA}}$. Принцип тезиса Чёрча ${\mathrm {CT} _{0}}$ может быть принят в ${\mathsf {HA}}$, пока ${\mathsf {PA}}$ отвергает его: оно подразумевает отрицания, подобные только что описанным.

Рассмотрим принцип в форме, утверждающий, что все предикаты, разрешимые в приведенном выше логическом смысле, также разрешимы полной вычислимой функцией . Чтобы увидеть, как он противоречит исключенному третьему, нужно просто определить предикат, который не является вычислимо разрешимым.Для этого напишите $\Delta _{e}(w):=T_{1}(e,e,w)$ для предикатов, определенных из предиката T Клини . Индексы $e$ всех вычислимых функций удовлетворяют $\forall x.\exists w.T_{1}(e,x,w)$. Пока $T_{1}$ может быть реализован примитивно-рекурсивным способом, предикат $\exists w.\Delta _{e}(w)$ в $e$, то есть класс $H:=\{e\mid \exists w.\Delta _{e}(w)\}$ индексов частично вычислимых функций со свидетелем, описывающим, как они останавливаются на диагонали, является вычислимо перечислимым, но невычислимым . Классический комплимент $M$ определяется с помощью $\neg \exists w.\Delta _{e}(w)$ даже не является вычислимо перечислимым, см. проблему остановки. Эта заведомо неразрешимая проблема $e\in M$ приводит пример нарушения. Для любого индекса $e$, эквивалентная форма $\forall w.\neg \Delta _{e}(w)$ выражает, что когда соответствующая функция вычисляется (при $e$), то все мыслимые описания историй оценок ( $w$) не описывайте имеющуюся оценку. В частности, неразрешимость этого для функций устанавливает отрицание того, что сводится к ${\mathrm {WLPO} }$.

Формальные принципы Церкви, естественно, связаны с рекурсивной школой. Принцип Маркова ${\mathrm {MP} _{\mathrm {Dec} }}$ обычно принимается этой школой и конструктивной математикой в ​​более широком смысле. В присутствии принципа Чёрча, ${\mathrm {MP} _{\mathrm {Dec} }}$ эквивалентно его более слабой форме ${\mathrm {MP} _{\mathrm {PR} }}$. Последнее обычно может быть выражено в виде одной аксиомы, а именно исключения двойного отрицания для любого $\neg \neg \exists w.T_{1}(e,x,w)$. Выполняем арифметику вместе с обоими ${\mathrm {MP} _{\mathrm {Dec} }}$+ ${\mathrm {ECT} _{0}}$ доказать независимость посылок разрешимых предикатов, ${\mathrm {IP} }_{0}$. Но они не идут рука об руку, последовательно, с ${\mathrm {IP} }$. ${\mathrm {CT} _{0}}$ также отрицает ${\mathrm {DNS} }$. Интуиционистская школа Л.Я. Брауэра расширяет арифметику Гейтинга путем совокупность принципов, которые отрицают оба ${\mathrm {PEM} }$ а также ${\mathrm {CT} _{0}}$.

Модели

Последовательность

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

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

Теория множеств

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

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

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

Эту небольшую вселенную множеств можно понимать как упорядоченную совокупность конечных двоичных последовательностей , кодирующих их взаимную принадлежность. Например, $100_{2}$'й набор содержит еще один набор и $110101_{2}$'-й набор содержит четыре других набора. См. предикат BIT .

Реализуемость

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

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

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

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

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

Типизированные версии реализуемости были представлены Георгом Крайзелем . Этим он продемонстрировал независимость классически справедливого принципа Маркова для интуиционистских теорий.

См. также интерпретацию BHK и интерпретацию диалектики .

В эффективном топосе уже конечно аксиомизируемая подсистема арифметики Гейтинга с индукцией, ограниченной $\Sigma _{1}$ является категоричным . Категоричность здесь напоминает теорему Тенненбаума . Модель подтверждает ${\mathsf {HA}}$ но не ${\mathsf {PA}}$ и поэтому полнота в этом контексте терпит неудачу.

Теория типов

Теоретические реализации типов, отражающие формализации логики, основанные на правилах вывода, были реализованы на различных языках .

Расширения

Арифметика Хейтинга обсуждалась с добавлением потенциальных функциональных символов для примитивно-рекурсивных функций. Эта теория доказывает сумму функции Аккермана .

Помимо этого, выбор аксиом и формализма всегда был предметом дискуссий даже в кругах конструктивистов. Многие типизированные расширения ${\mathsf {HA}}$ были широко изучены в теории доказательств , например, с типами функций между числами, функций между ними и т. д. Формальности, естественно, усложняются, поскольку применение функций регулируется различными возможными аксиомами. Таким образом можно расширить класс функций, являющихся тотальными. Теория с конечными типами ${\mathsf {HA}}^{\omega }$ в сочетании с экстенсиональностью функции и аксиомой выбора в ${\mathbb {N} }^{\mathbb {N} }$ по-прежнему доказывает те же арифметические формулы, что и только что ${\mathsf {HA}}$ и имеет теоретико-типовую интерпретацию. Однако эта теория отвергает тезис Чёрча о ${\mathbb {N} }^{\mathbb {N} }$ а также то, что все функции в ${\mathbb {N} }^{\mathbb {N} }\to {\mathbb {N} }$ было бы непрерывным. Но приняв, скажем, различные правила экстенсиональности, аксиомы выбора, принципы Маркова и независимости и даже лемму Кенига — все вместе, но каждый на определенной силе или уровнях — можно определить довольно «наполненную» арифметику, которая, возможно, все еще не сможет доказать исключенное среднее на уровне уровень $\Pi _{1}^{0}$-формулы. Ранее также варианты с интенсиональным равенством и брауэровской последовательностью выбора исследовались .

обратные математические исследования конструктивной арифметики второго порядка. Проведены

История

Формальная аксиоматизация теории восходит к Хейтингу (1930), Эрбрану и Клин . Гёдель доказал непротиворечивость относительно ${\mathsf {PA}}$ в 1933 году.

Связанные понятия

Гейтинговую арифметику не следует путать с алгебрами Гейтинга , которые являются интуиционистским аналогом булевых алгебр .

См. также

• Интерпретация БХК
• Конструктивный анализ
• Конструктивная теория множеств
• Формула Харропа
• Реализуемость

Ссылки

• Ульрих Коленбах (2008), Прикладная теория доказательств , Springer.
• Энн С. Трулстра , изд. (1973), Метаматематическое исследование интуиционистской арифметики и анализа , Springer, 1973.

Внешние ссылки

• Стэнфордская энциклопедия философии : « Интуиционистская теория чисел » Джоан Мошовакис .
• Фрагменты «Арифметики Гейтинга» Вольфганга Бёрра