Введение

Аксиоматизация арифметики
В математической логике, арифметика Хейтинга — это аксиоматизация арифметики, соответствующая философии интуиционизма. Она названа в честь Аренда Хейтинга, который впервые её предложил.

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

Арифметика Хейтинга может быть охарактеризована так же, как теория первого порядка арифметики Пеано, за исключением того, что она использует интуиционистское предикатное исчисление для вывода. В частности, это означает, что принцип устранения двойного отрицания, а также принцип исключённого третьего, не выполняются. Следует отметить, что "не выполняются" означает, что утверждение об исключённом третьем не является автоматически доказуемым для всех высказываний — действительно, многие такие высказывания всё ещё доказуемы в арифметике Хейтинга, и отрицание любого такого дизъюнкта является противоречивым. Арифметика Хейтинга строго сильнее арифметики Пеано в том смысле, что все теоремы арифметики Пеано также являются теоремами арифметики Хейтинга. Арифметика Хейтинга включает в себя аксиомы арифметики Пеано, а её предполагаемая модель — это множество натуральных чисел. Сигнатура включает ноль "0" и функцию следования "S", а теории характеризуют сложение и умножение. Это влияет на логику: в арифметике Хейтинга как метатеорема доказывается, что ложь можно определить как ¬Истина, и, следовательно, отрицание любого высказывания A имеет вид ¬A, и, таким образом, является тривиальным высказыванием. Для термов будем писать t для обозначения терма. Для фиксированного терма t равенство t = t истинно по рефлексивности, и высказывание P(t) эквивалентно ∃x P(x). Можно показать, что тогда ¬∃x P(x) может быть определено как ∀x ¬P(x). Такое формальное устранение дизъюнкций было невозможно в примитивно рекурсивной арифметике без кванторов. Теорию можно расширить символами функций для любой примитивно рекурсивной функции, что делает арифметику Хейтинга также фрагментом этой теории. Для тотальной функции f часто рассматриваются предикаты вида P(x₁, ..., xₙ) ≡ f(x₁, ..., xₙ) = 0.

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

С взрывом, действующим в любой интуиционистской теории, если является теоремой для некоторой , то по определению доказуемо тогда и только тогда, когда теория противоречива. Действительно, в арифметике Хейтинга двойное отрицание явно выражает . Для предиката , теорема вида выражает, что противоречиво исключать возможность того, что может быть истинным для некоторого . Конструктивно, это слабее, чем утверждение о существовании такого . Значительная часть метатеоретической дискуссии будет посвящена классически доказуемым утверждениям о существовании. Двойное отрицание влечет за собой . Таким образом, теорема вида также всегда предоставляет новые средства для окончательного опровержения (в том числе и положительных) утверждений .

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

Напомним, что импликация в классическом случае может быть обращена, и вместе с ней – и импликация в Здесь различие заключается в том, что речь идет о существовании численных контрпримеров, а не об абсурдных заключениях при предположении истинности для всех чисел. Вставка двойных отрицаний превращает теоремы в теоремы. Более точно, для любой формулы, доказуемой в , классически эквивалентный отрицательный перевод Гёделя — Гентцена этой формулы уже доказуем в . В одной из формулировок процедура перевода включает замену на . Результат означает, что все теоремы арифметики Пеано имеют доказательство, состоящее из конструктивного доказательства, за которым следует классическая логическая перепись. Грубо говоря, последний шаг сводится к применению устранения двойного отрицания. В частности, при отсутствии неразрешимых атомарных высказываний, для любого высказывания, не содержащего экзистенциальных кванторов или дизъюнкций, выполняется .

Валидные принципы и правила

Минимальная логика доказывает устранение двойного отрицания для отрицательных формул. В более общем виде, арифметика Хейтинга доказывает эту классическую эквивалентность для любой формулы Харропа. И результаты также хорошо себя ведут: правило Маркова на самом низком уровне арифметической иерархии является допустимым правилом вывода, то есть для с переменной, свободной. Вместо того чтобы говорить о предикатах без кванторов, можно эквивалентно сформулировать это для примитивно рекурсивных предикатов или предиката Т Клини, называемых , соответственно. Даже связанное с этим правило допустимо, в котором аспект вычислимости не основан, например, на синтаксическом условии, но левая часть также требует . Следует помнить, что при классификации высказывания на основе его синтаксической формы нельзя ошибочно присваивать ему более низкую сложность, основываясь лишь на какой-либо классически верной эквивалентности.

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

Как и в случае с другими теориями над интуиционистской логикой, в этой конструктивной арифметике можно доказать различные экземпляры . При введении дизъюнкции, если доказано либо предложение , либо , то доказано и . Таким образом, например, имея в аксиомах и , можно обосновать предпосылки для индукции закона исключённого среднего для предиката "Один", а затем утверждать, что равенство нулю является разрешимым. Действительно, доказывает разрешимость равенства "" для всех чисел, то есть, более того, поскольку равенство – единственный символ предиката в арифметике Хейтинга, то следует, что для любой формулы без кванторов , где – свободные переменные, теория замкнута относительно правила .

Любая теория над минимальной логикой доказывает для всех предложений. Следовательно, если теория непротиворечива, она никогда не доказывает отрицание утверждения закона исключённого среднего. На практике, в достаточно консервативных конструктивных системах, таких как , когда понятно, какие типы утверждений алгоритмически разрешимы, результат недоказуемости дизъюнкции закона исключённого среднего выражает алгоритмическую неразрешимость .

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

Для простых утверждений теория не просто подтверждает такие классически обоснованные бинарные дихотомии. Перевод Фридмана может быть использован для установления того, что все теоремы доказываются следующим образом: для любого и без кванторов, .

Этот результат, конечно, также может быть выражен с помощью явного универсального замыкания. Грубо говоря, простые утверждения о вычислимых отношениях, доказуемые классически, уже доказуемы конструктивно. Хотя в задачах об остановке важную роль играют не только пропозиции без кванторов, но и пропозиции с кванторами, и, как будет показано, они могут быть даже классически независимыми. Аналогично, уже само уникальное существование в бесконечной области, то есть , формально не является особенно простым. Таким образом, является консервативным расширением для . В отличие от этого, классическая теория арифметики Робинсона доказывает все теоремы, но некоторые простые теоремы независимы от неё. Индукция также играет решающую роль в результате Фридмана: например, более работоспособная теория, полученная путем усиления аксиомами об упорядочении и, опционально, разрешимым равенством, доказывает больше утверждений, чем её интуиционистский аналог. Данное обсуждение отнюдь не является исчерпывающим. Существуют различные результаты, определяющие, когда классическая теорема уже следует из конструктивной теории. Также следует отметить, что может иметь значение, какая логика использовалась для получения металогических результатов. Например, многие результаты по реализуемости были получены в конструктивной металогике. Но если конкретный контекст не указан, следует предполагать, что заявленные результаты относятся к классической логике.

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

Знание теорем неполноты Гёделя помогает понять, какие типы утверждений доказуемы, но невыводимы. Решение десятой проблемы Гильберта предоставило конкретные полиномы и соответствующие полиномиальные уравнения, для которых утверждение о существовании решения алгоритмически неразрешимо. Это утверждение можно выразить следующим образом:

Некоторые из таких утверждений о существовании нуля имеют более специфическую интерпретацию: теории, такие как или , доказывают, что эти утверждения эквивалентны арифметическому утверждению о собственной противоречивости этих теорий. Таким образом, подобные утверждения можно сформулировать даже для сильных классических теорий множеств. В непротиворечивой и корректной арифметической теории подобное утверждение о существовании является независимым утверждением. Затем, перенося отрицание через квантор, можно увидеть, что это независимое утверждение типа Гольдбаха или . Чтобы быть точным, двойное отрицание (или ) также является независимым. И любое тройное отрицание, в любом случае, уже интуиционистски эквивалентно одинарному отрицанию.

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

Следующее проливает свет на смысл таких независимых утверждений. Для заданного индекса в перечислении всех доказательств теории можно проверить, какое утверждение этим доказательством доказывается. Это адекватно, поскольку может корректно представлять эту процедуру: существует примитивно рекурсивный предикат, выражающий, что доказательство является доказательством абсурдного утверждения. Это связано с более явно арифметическим предикатом, упомянутым выше, относительно нулевого значения, возвращаемого полиномом. Металогически можно рассуждать, что если теория согласована, то она действительно доказывает для каждого отдельного индекса.

В эффективно аксиоматизированной теории можно последовательно проверять каждое доказательство. Если теория действительно согласована, то не существует доказательства абсурда, что соответствует утверждению о том, что указанный "поиск абсурда" никогда не завершится. Формально в теории это выражается предложением , отрицающим арифметическое выражение несогласованности. Эквивалентное предложение формализует бесконечность поиска, утверждая, что ни одно доказательство не является доказательством абсурда. И действительно, в омега-согласованной теории, точно представляющей доказуемость, нет доказательства того, что поиск абсурда когда-либо завершится (явная несогласованность не выводима), и, как показал Гёдель, не может быть доказательства того, что поиск абсурда никогда не завершится (согласованность не выводима). Перефразируя, нет доказательства того, что поиск абсурда никогда не завершается (согласованность не выводима), и нет доказательства того, что поиск абсурда не никогда не завершается (согласованность не опровержима). Повторюсь, ни один из этих двух дизъюнктов не доказуем, в то время как их дизъюнкция тривиально доказуема. Действительно, если согласована, то она противоречит . Утверждение, выражающее существование доказательства , является логически положительным утверждением. Тем не менее, исторически оно обозначается как , а его отрицание – предложением, обозначаемым как . В конструктивном контексте такое использование знака отрицания может быть вводящей в заблуждение номенклатурой. Фридман установил другое интересное недоказуемое утверждение, а именно, что согласованная и адекватная теория никогда не доказывает свое арифметическое свойство дизъюнкции.

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

Уже минимальная логика логически доказывает все утверждения о непротиворечивости, и в частности, и . Поскольку также , теорему можно интерпретировать как доказуемое дизъюнктивное утверждение двойного отрицания исключённого среднего (или утверждение о существовании). Однако, в свете свойства дизъюнкции, или поскольку один из соответствующих законов Де Моргана не выполняется интуиционистски, простое исключённое среднее не может быть доказано. Разрушение принципов и было объяснено. Теперь в , принцип наименьшего числа – это лишь одно из многих утверждений, эквивалентных принципу индукции. Приведенное ниже доказательство показывает, как из следует , и, следовательно, почему этот принцип также не может быть общепринятым в . Однако схема, гарантирующая существование наименьшего числа с двойным отрицанием для любого нетривиального предиката, обозначаемая , в целом является валидной. В свете доказательства Гёделя, разрушение этих трёх принципов можно понимать как согласованность арифметики Гейтинга с интерпретацией конструктивной логики как доказуемости. Принцип Маркова для примитивно рекурсивных предикатов уже не выполняется как схема импликации для , не говоря уже о строго более сильных . Хотя в форме соответствующих правил они допустимы, как упоминалось. Аналогично, теория не доказывает принцип независимости посылки для отрицательных предикатов, хотя она замкнута относительно правила для всех отрицательных высказываний, то есть можно вынести экзистенциальный квантор в . То же самое верно и для варианта, где экзистенциальное утверждение заменено простой дизъюнкцией. Валидное следствие можно доказать и в обратной форме, используя дизъюнктивный силлогизм. Однако двойное отрицание не является интуиционистски доказуемым, то есть схема коммутативности "" с универсальной квантификацией по всем числам не выполняется. Это интересное разрушение, которое объясняется согласованностью для некоторого , как обсуждалось в разделе о тезисе Черча.

Теза церкви

Правило Черча является допустимым правилом в принципе тезиса Черча, и может быть принято в , в то время как отвергает его: это подразумевает отрицания, подобные тем, что были только что описаны. Рассмотрим принцип в форме, утверждающей, что все предикаты, которые являются разрешимыми в логическом смысле, указанном выше, также разрешимы тотальной вычислимой функцией. Чтобы увидеть, как это противоречит закону исключённого третьего, достаточно определить предикат, который не является вычислимо разрешимым. Для этого обозначим через предикаты, определённые из предиката Т Клини. Индексы тотальных вычислимых функций удовлетворяют условию , при этом может быть реализован примитивно рекурсивно, а предикат в , то есть класс индексов частично вычислимых функций с доказательством остановки на диагонали, является вычислимо перечислимым, но не вычислимым. Классическое дополнение, определённое с помощью , даже не является вычислимо перечислимым, см. проблему остановки. Эта доказанно неразрешимая проблема служит контрпримером. Для любого индекса , эквивалентная формулировка выражает, что когда соответствующая функция вычисляется (в точке ), то все возможные описания истории вычислений не описывают данное вычисление. В частности, неразрешимость этого для функций устанавливает отрицание того, что составляет . Формальные принципы Черча естественным образом связаны с рекурсивной школой. Принцип Маркова обычно принимается этой школой и конструктивной математикой в целом. В присутствии принципа Черча, эквивалентно его более слабой форме. Последняя может быть выражена как единая аксиома, а именно устранение двойного отрицания для любой арифметики Хейтинга вместе с доказательством независимости посылки для разрешимых предикатов, но они несовместимы, в силу последовательности, с , которое также отрицает . Интуиционистская школа Л. Э. Й. Брауэра расширяет арифметику Хейтинга набором принципов, которые отрицают как , так и .

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

Если теория непротиворечива, то никакое доказательство не может привести к абсурду. Курт Гёдель ввёл отрицательный перевод и доказал, что если арифметика Хейтинга непротиворечива, то и арифметика Пеано тоже. Иными словами, он свёл задачу доказательства непротиворечивости к задаче доказательства непротиворечивости . Однако, теоремы о неполноте Гёделя, касающиеся неспособности определенных теорий доказать собственную непротиворечивость, применимы и к самой арифметике Хейтинга. Стандартная модель классической теории первого порядка, а также любая из её нестандартных моделей, является также моделью для арифметики Хейтинга.

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

Существуют также конструктивные модели теории множеств для полной и её предполагаемой семантики. Достаточно относительно слабых теорий множеств: они должны принимать аксиому бесконечности, аксиоматическую схему предикативного разделения для доказательства индукции арифметических формул в , а также существование функциональных пространств на конечных областях определения для рекурсивных определений. В частности, эти теории не требуют , полной аксиомы разделения или индукции по множествам (не говоря уже об аксиоме регулярности), ни общих функциональных пространств (не говоря уже о полной аксиоме множества мощностей). Более того, она биинтерпретируема со слабой конструктивной теорией множеств, в которой класс ординалов составляет , так что коллекция натуральных чисел фон Неймана не существует как множество в этой теории. Метатеоретически, область этой теории столь же велика, как класс её ординалов и по существу задаётся классом всех множеств, находящихся в биекции с натуральным числом. Как аксиома это называется , а остальные аксиомы относятся к алгебре множеств и порядку: объединение и бинарное пересечение, тесно связанные со схемой предикативного разделения, аксиомой экстенсиональности, аксиомой пар и схемой индукции по множествам. Эта теория уже идентична теории, заданной без сильной бесконечности и с добавленной аксиомой конечности. Обсуждение в этой теории множеств происходит так же, как в теории моделей. И в обратном направлении, аксиомы теории множеств доказываются относительно примитивно рекурсивного отношения.

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

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

Для некоторого числа в метатеории, число в изучаемой объектной теории обозначается как . В интуиционистской арифметике свойство дизъюнкции обычно справедливо. И это теорема, что любое c.e.-расширение арифметики, для которого оно выполняется, также обладает свойством численного существования.

Таким образом, эти свойства металогически эквивалентны в арифметике Хейтинга. Свойство существования и дизъюнкции фактически сохраняется при релятивизации утверждения о существовании формулой Харропа, то есть для доказуемого . Клин, ученик Черча, ввёл важные модели реализуемости арифметики Хейтинга. В свою очередь, его ученик Нельс Дэвид Нельсон установил (в расширении ), что все замкнутые теоремы (то есть все переменные связаны) могут быть реализованы. Дедукция в арифметике Хейтинга сохраняет реализуемость. Более того, если , то существует частично рекурсивная функция, реализующая в том смысле, что всякий раз, когда функция, вычисленная в , завершается со значением , то . Это можно обобщить на любое конечное число аргументов функции.

Существуют также классические теоремы, которые не доказуемы, но имеют реализацию. Георг Крайзель ввёл типизированные версии реализуемости. С её помощью он продемонстрировал независимость классически верного принципа Маркова для интуиционистских теорий. См. также интерпретацию BHK и интерпретацию Dialectica. В эффективном топосе уже конечно аксиоматизируемая подсистема арифметики Хейтинга с индукцией, ограниченной , является категоричной. Категоричность здесь напоминает теорему Тенненбаума. Модель подтверждает , но не подтверждает , и поэтому полнота не выполняется в этом контексте.

Теория типов

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

Расширения

Обсуждалась арифметика Хейтинга с добавлением потенциальных функциональных символов для примитивно рекурсивных функций. Эта теория доказывает тотализацию функции Аккермана. Более того, выбор аксиом и формализма всегда был предметом дебатов даже внутри конструктивистского сообщества. Многие типизированные расширения интенсионально изучались в теории доказательств, например, с типами функций между числами и функциями между этими типами и так далее. Формализмы, естественно, становятся сложнее, с различными возможными аксиомами, регулирующими применение функций. Таким образом можно обогатить класс тотальных функций. Теория с конечными типами, будучи дополнительно объединенной с экстенсиональностью функций и аксиомой выбора, все еще доказывает те же арифметические формулы, что и просто арифметика Хейтинга, и имеет типо-теоретическую интерпретацию. Однако эта теория отвергает тезис Черча для и также утверждает, что не все функции в будут непрерывными. Но, приняв, скажем, различные правила экстенсиональности, аксиомы выбора, принципы Маркова и независимости, и даже лемму Кёнига – все вместе, но каждый с определенной силой или на определенном уровне – можно определить довольно "насыщенные" арифметики, которые все равно могут не доказать исключенное среднее на уровне формул. Ранее также исследовались варианты с иннтенциональным равенством и последовательностью выбора Брауэра. Проводились исследования обратной математики конструктивной арифметики второго порядка.

История

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

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

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