Арифметика второго порядка

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

Предшественник арифметики второго порядка, включающий параметры третьего порядка, был представлен Дэвидом Гильбертом и Полем Бернейсом в их книге «Основы математики» . Стандартная аксиоматизация арифметики второго порядка обозначается Z ₂ .

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

Арифметику второго порядка также можно рассматривать как слабую версию теории множеств , в которой каждый элемент является либо натуральным числом, либо набором натуральных чисел. Хотя арифметика второго порядка намного слабее, чем теория множеств Цермело–Френкеля , она может доказать по существу все результаты классической математики , выражаемые на ее языке.

Подсистема арифметики второго порядка — это теория на языке арифметики второго порядка, каждая аксиома которой является теоремой полной арифметики второго порядка (Z ₂ ). Такие подсистемы необходимы для обратной математики — исследовательской программы, изучающей, какая часть классической математики может быть получена в определенных слабых подсистемах различной силы. Большая часть базовой математики может быть формализована в этих слабых подсистемах, некоторые из которых определены ниже. Обратная математика также проясняет степень и способ неконструктивности классической математики .

Определение

Синтаксис

Язык арифметики второго порядка двусортен . первого типа Термины и, в частности, переменные , обычно обозначаемые строчными буквами, состоят из отдельных лиц , предполагаемая интерпретация которых — это натуральные числа. Переменные другого типа, называемые по-разному «переменными набора», «переменными класса» или даже «предикатами», обычно обозначаются заглавными буквами. Они относятся к классам/предикатам/свойствам индивидуумов, поэтому их можно рассматривать как наборы натуральных чисел. И индивидуумы, и набор переменных могут быть определены количественно универсально или экзистенциально . Формула без связанных переменных множества (то есть без кванторов над переменными множества) называется арифметической . Арифметическая формула может иметь свободные наборы переменных и связанные отдельные переменные.

Отдельные термы формируются из константы 0, унарной функции S ( функции-последователя ) и бинарных операций + и $\cdot$(сложение и умножение). Функция-преемник добавляет 1 к своему входу. Отношения = (равенство) и < (сравнение натуральных чисел) связывают двух индивидов, тогда как отношение ∈ (принадлежность) связывает индивидуума и множество (или класс). Таким образом, в обозначениях язык арифметики второго порядка задается сигнатурой ${\mathcal {L}}=\{0,S,+,\cdot ,=,<,\in \}$.

Например, $\forall n(n\in X\rightarrow Sn\in X)$, представляет собой правильно сформированную формулу арифметики второго порядка, которая является арифметической, имеет одну свободную переменную множества X и одну связанную индивидуальную переменную n (но не имеет связанных переменных множества, как того требует арифметическая формула), тогда как $\exists X\forall n(n\in X\leftrightarrow n<SSSSSS0\cdot SSSSSSS0)$ — это правильно составленная формула, не являющаяся арифметической, имеющая одну связанную заданную переменную X и одну связанную индивидуальную переменную n .

Семантика

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

Аксиомы

Базовый

Следующие аксиомы известны как основные аксиомы или иногда аксиомы Робинсона. Полученная в результате теория первого порядка , известная как арифметика Робинсона , по существу представляет собой арифметику Пеано без индукции. Областью обсуждения количественных переменных являются натуральные числа , совокупно обозначаемые N и включающие выделенный член $0$, называемый « ноль ».

Примитивные функции — это унарная функция-преемник , обозначаемая префиксом $S$и две двоичные операции , сложение и умножение , обозначаемые инфиксным оператором «+» и « $\cdot$", соответственно. Существует также примитивное бинарное отношение , называемое порядком , обозначаемое инфиксным оператором "<".

Аксиомы, управляющие функцией-преемником и нулем :

1. $\forall m[Sm=0\rightarrow \bot ].$ («Последователь натурального числа никогда не равен нулю»)

2. $\forall m\forall n[Sm=Sn\rightarrow m=n].$ («функция-преемник инъективна »)

3. $\forall n[0=n\lor \exists m[Sm=n]].$ («каждое натуральное число равно нулю или является его преемником»)

Сложение определяется рекурсивно :

4. $\forall m[m+0=m].$

5. $\forall m\forall n[m+Sn=S(m+n)].$

Умножение определено рекурсивно:

6. $\forall m[m\cdot 0=0].$

7. $\forall m\forall n[m\cdot Sn=(m\cdot n)+m].$

Аксиомы, управляющие отношением порядка «<»:

8. $\forall m[m<0\rightarrow \bot ].$ («ни одно натуральное число не меньше нуля»)

9. $\forall n\forall m[m<Sn\leftrightarrow (m<n\lor m=n)].$

10. $\forall n[0=n\lor 0<n].$ («каждое натуральное число равно нулю или больше нуля»)

11. $\forall m\forall n[(Sm<n\lor Sm=n)\leftrightarrow m<n].$

Все эти аксиомы являются утверждениями первого порядка . То есть все переменные варьируются в пределах натуральных чисел , а не их наборов , и это факт даже более сильный, чем их арифметический характер. Более того, в Аксиоме 3 есть только один квантор существования . Аксиомы 1 и 2 вместе со схемой аксиом индукции составляют обычное Пеано-Дедекинда определение N . Добавление к этим аксиомам какой-либо схемы аксиом индукции делает излишними аксиомы 3, 10 и 11.

Схема индукции и понимания

Если φ ( n ) является формулой арифметики второго порядка со свободной индивидуальной переменной n другими свободными индивидуальными или наборными переменными (записанными m1 _, ..., mk _{и, возможно} и X1 _, ..., Xl _, ), аксиомой индукции для φ является аксиома:

$\forall m_{1}\dots m_{k}\forall X_{1}\dots X_{l}((\varphi (0)\land \forall n(\varphi (n)\rightarrow \varphi (Sn)))\rightarrow \forall n\varphi (n))$

( Полная ) схема индукции второго порядка состоит из всех экземпляров этой аксиомы по всем формулам второго порядка.

Один особенно важный пример схемы индукции — это случай, когда φ представляет собой формулу « $n\in X$«выражающее тот факт, что n является членом X ( X — свободная переменная множества): в этом случае аксиома индукции для φ равна

$\forall X((0\in X\land \forall n(n\in X\rightarrow Sn\in X))\rightarrow \forall n(n\in X))$

Это предложение называется аксиомой индукции второго порядка .

Если φ ( n ) — формула со свободной переменной n и, возможно, другими свободными переменными, но не с переменной Z , аксиомой понимания для φ является формула

$\exists Z\forall n(n\in Z\leftrightarrow \varphi (n))$

Эта аксиома позволяет сформировать множество $Z=\{n|\varphi (n)\}$натуральных чисел, удовлетворяющих φ ( n ). Существует техническое ограничение: формула φ не может содержать переменную Z , иначе формула $n\not \in Z$ приведет к аксиоме понимания

$\exists Z\forall n(n\in Z\leftrightarrow n\not \in Z)$,

что противоречиво. Это соглашение предполагается в оставшейся части этой статьи.

Полная система

Формальная теория арифметики второго порядка (на языке арифметики второго порядка) состоит из основных аксиом, аксиомы понимания для каждой формулы φ (арифметической или иной) и аксиомы индукции второго порядка. Эту теорию иногда называют полной арифметикой второго порядка, чтобы отличить ее от ее подсистем, определенных ниже. Поскольку полная семантика второго порядка подразумевает, что существует каждое возможное множество, аксиомы понимания можно рассматривать как часть дедуктивной системы, когда используется полная семантика второго порядка.

Модели

В этом разделе описывается арифметика второго порядка с семантикой первого порядка. Таким образом, модель ${\mathcal {M}}$языка арифметики второго порядка состоит из множества M (образующего диапазон отдельных переменных) вместе с константой 0 (элементом M ), функцией S от M до M , двумя двоичными операциями + и · над M. , бинарное отношение < на M и набор D подмножеств M , который является диапазоном заданных переменных. Если опустить D, получится модель языка арифметики первого порядка.

Когда D — полный набор мощности M , модель ${\mathcal {M}}$называется полной моделью . Использование полной семантики второго порядка эквивалентно ограничению моделей арифметики второго порядка полными моделями. Фактически аксиомы арифметики второго порядка имеют только одну полную модель. Это следует из того, что аксиомы Пеано с аксиомой индукции второго порядка имеют только одну модель при семантике второго порядка.

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

Функции первого порядка, которые доказуемо полны в арифметике второго порядка, в точности такие же, как и функции, представимые в системе F . Почти то же самое, что система F представляет собой теорию функционалов, соответствующую арифметике второго порядка, аналогично тому, как система Гёделя T соответствует арифметике первого порядка в интерпретации «Диалектики» .

Больше типов моделей

Когда модель языка арифметики второго порядка обладает определенными свойствами, ее можно называть и другими именами:

• Когда M — обычный набор натуральных чисел с обычными операциями, ${\mathcal {M}}$называется ω-моделью . В этом случае модель можно отождествить с D , ее совокупностью наборов натуральных чисел, поскольку этого набора достаточно для полного определения ω-модели. Уникальный полный $\omega$-модель, представляющая собой обычный набор натуральных чисел с его обычной структурой и всеми его подмножествами, называется предполагаемой или стандартной моделью арифметики второго порядка.
• Модель ${\mathcal {M}}$ языка арифметики второго порядка называется β-моделью , если ${\mathcal {M}}\prec _{1}^{1}{\mathcal {P}}(\omega )$, то есть Σ ¹ _{1 -} операторы с параметрами из ${\mathcal {M}}$ которые удовлетворены ${\mathcal {M}}$ такие же, как и те, которые удовлетворяются полной моделью. Некоторые понятия, абсолютные по отношению к β-моделям, включают: $A\subseteq \omega \times \omega$ кодирует порядок » и " $A\subseteq \omega \times \omega$ это дерево ».
• Приведенный выше результат был распространен на концепцию β _n -модели для $n\in \mathbb {N}$, который имеет то же определение, что и выше, за исключением $\prec _{1}^{1}$ заменяется на $\prec _{n}^{1}$, то есть $\Sigma _{1}^{1}$ заменяется на $\Sigma _{n}^{1}$. Используя это определение, β0 _- модели — это то же самое, что и ω-модели.

Подсистемы

Основная статья: Обратная математика

Существует множество названных подсистем арифметики второго порядка.

Индекс 0 в названии подсистемы означает, что она включает в себя только ограниченная часть полной схемы индукции второго порядка. Такое ограничение существенно снижает теоретико-доказательную силу системы. Например, _{система ACA 0} описанная ниже эквисовместима с арифметикой Пеано . Соответствующая теория ACA, состоящая из ACA ₀ плюс полная схема индукции второго порядка, сильнее арифметики Пеано.

Арифметическое понимание

Многие из хорошо изученных подсистем связаны со свойствами замыкания моделей. Например, можно показать, что каждая ω-модель полной арифметики второго порядка замкнута относительно скачка Тьюринга , но не каждая ω-модель, замкнутая относительно скачка Тьюринга, является моделью полной арифметики второго порядка. Подсистема ACA ₀ включает в себя ровно столько аксиом, чтобы уловить понятие замыкания при скачке Тьюринга.

ACA ₀ определяется как теория, состоящая из основных аксиом, схемы аксиом арифметического понимания (другими словами, аксиомы понимания для каждой арифметической формулы φ ) и обычной аксиомы индукции второго порядка. Было бы эквивалентно также включить всю схему аксиом арифметической индукции, другими словами, включить аксиому индукции для каждой арифметической формулы φ .

Можно показать, что набор S подмножеств ω определяет ω-модель ACA ₀ тогда и только тогда, когда S замкнуто относительно скачка Тьюринга, сводимости по Тьюрингу и соединения Тьюринга.

Индекс 0 в ACA ₀ указывает на то, что не каждый экземпляр схемы аксиом индукции включает эту подсистему. Это не имеет значения для ω-моделей, которые автоматически удовлетворяют каждому случаю аксиомы индукции. Однако это важно при изучении не-ω-моделей. Систему, состоящую из ACA ₀ плюс индукция для всех формул, иногда называют ACA без индекса.

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

Арифметическая иерархия формул

Основная статья: Арифметическая иерархия

Формула называется ограниченной арифметической , или ∆ ⁰ ₀ , когда все его кванторы имеют вид ∀ n < t или ∃ n < t (где n — индивидуальная переменная, подлежащая количественному определению, а t — отдельный термин), где

$\forall n<t(\cdots )$

означает

$\forall n(n<t\rightarrow \cdots )$

и

$\exists n<t(\cdots )$

означает

$\exists n(n<t\land \cdots )$.

Формула называется Σ ⁰ ₁ (или иногда Σ ₁ ), соответственно Π ⁰ ₁ (или иногда Π ₁ ), когда он имеет вид ∃ m φ , соответственно ∀ m φ , где φ — ограниченная арифметическая формула, а m — индивидуальная переменная (свободная в φ ). В более общем смысле формула называется Σ ⁰ _n соответственно Π ⁰ _n, когда оно получается добавлением экзистенциальных, соответственно универсальных, индивидуальных кванторов к Π ⁰ _{n −1} соответственно Σ ⁰ _{формула n −1} (и S ⁰ ₀ и Π ⁰ ₀ оба равны Δ ⁰ ₀ ). По построению все эти формулы являются арифметическими (никакие переменные класса никогда не связаны), и фактически, поставив формулу в пренексную форму Сколема, можно увидеть, что каждая арифметическая формула логически эквивалентна Σ ⁰ _п или Π ⁰ _{формула n} для всех достаточно больших n .

Рекурсивное понимание

Подсистема RCA ₀ является более слабой системой, чем ACA _0, и часто используется в качестве базовой системы в обратной математике . Он состоит из: основных аксиом, Σ ⁰ ₁ индукционная схема, а ∆ ⁰ ₁ схема понимания. Первый термин ясен: Σ ⁰ ₁ схема индукции является аксиомой индукции для каждого Σ ⁰ ₁ формула φ . Термин «Δ ⁰ ₁ понимание» является более сложным, потому что не существует такой вещи, как Δ ⁰ ₁ формула. Δ ⁰ ₁ схема понимания вместо этого утверждает аксиому понимания для каждого Σ ⁰ ₁ формула, которая логически эквивалентна Π ⁰ ₁ формула. Эта схема включает в себя для каждого Σ ⁰ ₁ формула φ и каждое Π ⁰ ₁ формула ψ , аксиома:

$\forall m\forall X((\forall n(\varphi (n)\leftrightarrow \psi (n)))\rightarrow \exists Z\forall n(n\in Z\leftrightarrow \varphi (n)))$

Набор следствий первого порядка RCA ₀ такой же, как и у подсистемы IΣ ₁ арифметики Пеано, в которой индукция ограничена Σ ⁰ ₁ формулы. В свою очередь, IΣ ₁ консервативен по отношению к примитивно-рекурсивной арифметике (PRA) для $\Pi _{2}^{0}$предложения. Более того, теоретико-доказательный ординал $\mathrm {RCA} _{0}$ это ω ^ой , то же, что и у ПРА.

Можно видеть, что набор S подмножеств ω определяет ω-модель RCA ₀ тогда и только тогда, когда S замкнуто относительно сводимости по Тьюрингу и соединения по Тьюрингу. В частности, совокупность всех вычислимых подмножеств ω дает ω-модель RCA ₀ . Это мотивация названия этой системы: если существование набора можно доказать с помощью RCA ₀ , то этот набор является рекурсивным (т. е. вычислимым).

системы

даже более слабая система, чем RCA ₀ Иногда желательна . Одна из таких систем определяется следующим образом: сначала необходимо дополнить язык арифметики символом экспоненциальной функции (в более сильных системах экспоненту можно определить в терминах сложения и умножения обычным приемом, но когда система становится слишком слабой, это уже невозможно) и основные аксиомы очевидными аксиомами, определяющими возведение в степень индуктивно из умножения; тогда система состоит из (обогащенных) основных аксиом плюс ∆ ⁰ ₁ понимание плюс Δ ⁰ ₀ индукция.

системы

Над ACA ₀ каждая формула арифметики второго порядка эквивалентна Σ ¹ _п или Π ¹ _{формула n} для всех достаточно больших n . Система Π ¹ ₁ -понимание – это система, состоящая из основных аксиом, плюс обычная аксиома индукции второго порядка и аксиома понимания для каждого ( жирный шрифт ) ПИ ¹ ₁ формула φ . Это эквивалентно Σ ¹ ₁ -понимание (с другой стороны, ∆ ¹ ₁ -понимание, определяемое аналогично ∆ ⁰ ₁ – понимание, слабее).

Проективная детерминированность

Основная статья: Аксиома проективной определенности

Проективная детерминированность — это утверждение, что каждая игра с совершенной информацией для двух игроков, ходы которой являются натуральными числами, длина игры ω и проективное множество выигрышей определена, то есть один из игроков имеет выигрышную стратегию. (Первый игрок выигрывает игру, если игра принадлежит выигрышному множеству; в противном случае выигрывает второй игрок.) Множество является проективным тогда и только тогда, когда (как предикат) оно выражается формулой на языке второго порядка. арифметика, допускающая действительные числа в качестве параметров, поэтому проективная определенность выражается в виде схемы на языке Z ₂ .

Многие естественные предложения, выражаемые на языке арифметики второго порядка, не зависят от Z ₂ и даже от ZFC , но доказуемы с точки зрения проективной определенности. Примеры включают свойство коаналитического совершенного подмножества , измеримость и свойство Бэра для $\Sigma _{2}^{1}$ наборы, $\Pi _{3}^{1}$ униформизация и т. д. В рамках слабой базовой теории (такой как RCA ₀ ) проективная определенность подразумевает понимание и обеспечивает по существу полную теорию арифметики второго порядка — естественные утверждения на языке Z ₂ , независимые от Z ₂ с проективной определенностью, трудно найти.

ZFC + {существует n кардиналов Вудина : n — натуральное число} консервативен над Z ₂ с проективной определенностью. , то есть утверждение на языке арифметики второго порядка доказуемо в Z ₂ с проективной определенностью тогда и только тогда, когда его перевод на язык теории множеств доказуем в ZFC + {существует n кардиналов Вудина: n ∈N}.

Кодирование математики

Арифметика второго порядка непосредственно формализует натуральные числа и множества натуральных чисел. Однако он способен формализовать другие математические объекты косвенно, с помощью методов кодирования, и этот факт впервые заметил Вейль . Целые числа , рациональные числа и действительные числа могут быть формализованы в подсистеме RCA ₀ вместе с полными сепарабельными метрическими пространствами и непрерывными функциями между ними.

Исследовательская программа обратной математики использует эти формализации математики в арифметике второго порядка для изучения аксиом существования множеств, необходимых для доказательства математических теорем. Например, теорема о промежуточном значении для функций от вещественных чисел до вещественных чисел доказуема в RCA ₀ , в то время как теорема Больцано – Вейерштрасса эквивалентна ACA ₀ над RCA ₀ .

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

См. также

• Теорема Пэрис – Харрингтона
• Арифметика Пресбургера
• Истинная арифметика

Дальнейшее чтение

• Берджесс, JP (2005). Исправление Фреге . Издательство Принстонского университета.
• Басс, СР (1998). Справочник по теории доказательств . Эльзевир. ISBN  0-444-89840-9 .
• Такеути, Г. (1975). Теория доказательств . ISBN  0-444-10492-5 .