Арифметика второго порядка - Second-order arithmetic

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

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

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

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

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

Определение

Синтаксис

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

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

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

Семантика

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

Аксиомы

Базовый

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

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

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

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

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

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

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

4. ${\ displaystyle \ forall m [m + 0 = m].}$

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

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

6. ${\ displaystyle \ forall m [m \ cdot 0 = 0].}$

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

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

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

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

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

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

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

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

Если φ ( n ) является формулой арифметики второго порядка со свободной числовой переменной n и возможными другими свободными числовыми или заданными переменными (записываются m _• и X _• ), аксиома индукции для φ является аксиомой:

${\ displaystyle \ forall m \ forall X ((\ varphi (0) \ land \ forall n (\ varphi (n) \ rightarrow \ varphi (Sn))) \ rightarrow \ forall n \ varphi (n))}$

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

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

${\ Displaystyle \ forall X ((0 \ in X \ land \ forall п (п \ in X \ rightarrow Sn \ in X)) \ rightarrow \ forall п (п \ in X))}$

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

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

${\ Displaystyle \ существует Z \ forall п (п \ в Z \ leftrightarrow \ varphi (п))}$

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

${\ Displaystyle \ существует Z \ forall п (п \ в Z \ leftrightarrow п \ не \ в Z)}$,

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

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

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

Модели

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

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

Когда M - обычный набор натуральных чисел с его обычными операциями, он называется ω-моделью . В этом случае модель может быть отождествлена ​​с D , ее набором наборов натуральных чисел, потому что этого набора достаточно, чтобы полностью определить ω-модель. ${\ Displaystyle {\ mathcal {M}}}$

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

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

Функции первого порядка, которые доказуемо являются тотальными в арифметике второго порядка, в точности такие же, как функции, представимые в системе F (Girard and Taylor, 1987, стр. 122–123). Почти эквивалентно, система F является теорией функционалов, соответствующей арифметике второго порядка, аналогично тому, как система Гёделя T соответствует арифметике первого порядка в интерпретации диалектики .

Подсистемы

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

Нижний индекс 0 в названии подсистемы указывает, что она включает только ограниченную часть полной схемы индукции второго порядка (Friedman 1976). Такое ограничение значительно снижает теоретико-доказательную стойкость системы. Например, система АС ₀ , описанная ниже , equiconsistent с арифметикой Пеаны . Соответствующая теория ACA, состоящая из ACA ₀ плюс полная схема индукции второго порядка, сильнее арифметики Пеано.

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

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

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

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

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

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

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

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

${\ Displaystyle \ forall п <т (\ cdots)}$

означает

${\ Displaystyle \ forall п (п <т \ rightarrow \ cdots)}$

а также

${\ Displaystyle \ существует п <т (\ cdots)}$

означает

${\ Displaystyle \ существует п (п <т \ земля \ cdots)}$.

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

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

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

${\ displaystyle \ forall m \ forall X ((\ forall n (\ varphi (n) \ leftrightarrow \ psi (n))) \ rightarrow \ существует Z \ forall n (п \ in Z \ leftrightarrow \ varphi (n)) )}$

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

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

Более слабые системы

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

Более сильные системы

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

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

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

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

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

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

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

Программа исследований обратной математики использует эти формализации математики в арифметике второго порядка для изучения аксиом существования множеств, необходимых для доказательства математических теорем (Simpson 2009, p. 32). Например, теорема о промежуточном значении для функций от действительных чисел до действительных чисел доказуема в RCA ₀ (Simpson 2009, стр. 87), в то время как теорема Больцано - Вейерштрасса эквивалентна ACA ₀ над RCA ₀ (Simpson 2009, стр. 34). ).

Вышеупомянутое кодирование хорошо работает для непрерывных и полных функций, как показано в (Kohlenbach 2002, Section 4), при условии, что базовая теория более высокого порядка плюс слабая лемма Кенига . Как, возможно, и ожидалось, в случае топологии или теории меры, кодирование сопряжено с проблемами, о чем говорится, например, в (Hunter, 2008) или (Normann-Sanders, 2019). Однако даже кодирование интегрируемых функций Римана приводит к проблемам: как показано в (Normann-Sanders, 2020), минимальные (понятные) аксиомы, необходимые для доказательства теоремы сходимости Арзелы для интеграла Римана, * очень * различны в зависимости от того, используется ли второй - коды заказа или функции третьего порядка.

Смотрите также

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

использованная литература

• Берджесс, JP (2005), Fixing Frege , Princeton University Press.
• Buss, SR (1998), Справочник по теории доказательств , Elsevier. ISBN  0-444-89840-9
• Фридман, Х. (1976), "Системы арифметики второго порядка с ограниченной индукцией", I, II (Тезисы). Журнал символической логики , т. 41, стр. 557–559. JStor
• Жирар Л. и Тейлор (1987), Доказательства и типы , Издательство Кембриджского университета.
• Гильберт Д. и Бернейс П. (1934), Grundlagen der Mathematik , Springer-Verlag. Руководство по ремонту 0237246
• Хантер, Джеймс, Обратная топология высшего порядка , Диссертация, Университет Мэдисона-Висконсина [1] .
• Коленбах, У. , Основы и математическое использование высших типов , Размышления об основах математики, Lect. Журнал заметок., Т. 15, ASL, 2002, стр. 92–116.
• Даг Норманн и Сэм Сандерс, Представления в теории меры , arXiv: 1902.02756 , (2019).
• Даг Норманн и Сэм Сандерс, О несчетности $ \ mathbb {R} $ , arxiv: [2] , (2020), стр. 37.
• Зиг, В. (2013), Программы Гильберта и не только , Oxford University Press.
• Шапиро, С. (1991), Фонды без фундаментализма , Oxford University Press. ISBN  0-19-825029-0
• Симпсон, С.Г. (2009), Подсистемы арифметики второго порядка , 2-е издание, Перспективы в логике, Cambridge University Press. ISBN  978-0-521-88439-6 MR 2517689
• Такеути, Г. (1975) ISBN теории доказательства 0-444-10492-5 
• Вудин, WH (2001), "Гипотеза континуума, часть I", Уведомления Американского математического общества , т. 48, стр. 6.