Формальная арифметика

Форма́льная арифме́тика, арифметическое исчисление, логико-математическое исчисление, формализующее элементарную теорию чисел. Язык наиболее употребительного варианта формальной арифметики содержит константу ${\displaystyle 0}$, числовые переменные, символ равенства, функциональные символы ${\displaystyle +}$, ${\displaystyle \cdot }$, ${\displaystyle '}$ (прибавление ${\displaystyle 1}$) и логические связки. Термы строятся из константы ${\displaystyle 0}$ и переменных с помощью функциональных символов; в частности, натуральные числа изображаются термами вида ${\displaystyle 0'\ldots '}$. Атомарные формулы – это равенства термов; остальные формулы строятся из атомарных с помощью логических связок ${\displaystyle \&amp}$;, ${\displaystyle \lor }$, ${\displaystyle \to }$, ${\displaystyle \neg }$, ${\displaystyle \forall }$, ${\displaystyle \exists }$. Формулы в языке формальной арифметики называются арифметическими формулами. Постулатами формальной арифметики являются постулаты исчисления предикатов (классического или интуиционистского в зависимости от того, какая формальная арифметика рассматривается), аксиомы Пеано

${\displaystyle }$
${\displaystyle a'=b'\to a=b,\quad \neg (a'=0),\quad (a=b\&a=c)\to b=c,}$
${\displaystyle a=b\to a'=b',\quad a+0=a,\quad a+b'=(a+b)',}$
${\displaystyle a\cdot 0=0,\quad a\cdot b'=(a\cdot b)+a}$
${\displaystyle }$

и схема аксиом индукции

${\displaystyle A(0)\&\forall x(A(x)\to A(x'))\to A(x)}$,

где ${\displaystyle A}$ – произвольная формула, называемая индукционной формулой.

Средства формальной арифметики оказываются достаточными для вывода теорем, устанавливаемых в стандартных курсах элементарной теории чисел. В настоящее время (1970-е годы), по-видимому, неизвестно ни одной содержательной теоретико-числовой теоремы, доказанной без привлечения средств анализа, которая не была бы выводима в формальной арифметике. Запись и доказательство таких теорем в формальной арифметике требует выявления её выразительных возможностей. Особенно существенна выразимость в формальной арифметике многих теоретикочисловых функций. В частности, в формальной арифметике можно записывать суждения о примитивно (и даже частично) рекурсивных функциях. При этом оказываются выводимыми формулы, выражающие важные свойства частично рекурсивных функций, в частности их определяющие равенства. Так, равенство ${\displaystyle f(x')=g(x,f(x))}$ выражается формулой

${\displaystyle \forall a\forall b\forall c\,(F(x',a)\&F(x,b)\&G(x,b,c)\to a=c)}$,

где ${\displaystyle F}$ и ${\displaystyle G}$ – формулы, изображающие графики функций ${\displaystyle f}$ и ${\displaystyle g}$, соответственно. В формальной арифметике можно формулировать суждения о конечных множествах. Более того, классическая формальная арифметика эквивалентна аксиоматической теории множеств Цермело – Френкеля без аксиомы бесконечности: в каждой из этих систем может быть построена модель другой.

Дедуктивная сила системы формальной арифметики характеризуется ординалом ${\displaystyle \varepsilon _{0}}$ (наименьшее решение уравнения ${\displaystyle \omega ^{\varepsilon }=\varepsilon }$): в формальной арифметике выводима схема трансфинитной индукции до любого ординала ${\displaystyle \alpha <\varepsilon _{0}}$, но не выводима схема индукции до ${\displaystyle \varepsilon _{0}}$. Класс доказуемо рекурсивных функций системы формальной арифметики (то есть частично рекурсивных функций, общерекурсивность которых может быть установлена средствами формальной арифметики) совпадает с классом ординально рекурсивных функций с ординалами ${\displaystyle <\varepsilon _{0}}$. Это позволяет погружать в формальную арифметику некоторые её расширения, например формальную арифметику с символами для всех примитивно рекурсивных функций и соответствующими дополнительными постулатами. Формальная арифметика удовлетворяет условиям обеих теорем Гёделя о неполноте. В частности, имеются такие полиномы ${\displaystyle P}$, ${\displaystyle Q}$ от нескольких переменных, что формула ${\displaystyle \forall X(P(X)\neq Q(X))}$ невыводима, хотя и выражает истинное утверждение, а именно непротиворечивость системы формальной арифметики.

При исследовании структуры формальной арифметики (в частности, вопросов непротиворечивости) используется её формулировка без кванторов, но с гильбертовским ${\displaystyle \varepsilon }$-символом. При построении формул этой системы не допускается употребление кванторов, но разрешается использование термов вида ${\displaystyle \varepsilon _{x}A(x)}$ (некоторое ${\displaystyle x}$, удовлетворяющее условию ${\displaystyle A}$, если такие ${\displaystyle x}$ существуют, и ${\displaystyle 0}$ в противном случае). Постулаты ${\displaystyle \varepsilon }$-системы – это постулаты исчисления высказываний, правила для равенства, правило подстановки вместо свободной числовой переменной, аксиомы для функций ${\displaystyle +}$, ${\displaystyle \cdot }$, ${\displaystyle '}$, ${\displaystyle pd}$ (вычитание ${\displaystyle 1}$ из положительных чисел) и следующие ${\displaystyle \varepsilon }$-аксиомы:

${\displaystyle }$
${\displaystyle A(a)\to A(\varepsilon _{x}A(x));\quad A(a)\to \varepsilon _{x}A(x)\neq a';}$
${\displaystyle \neg A(\varepsilon _{x}A(x))\to \varepsilon _{x}A(x)=0.}$
${\displaystyle }$

Кванторы вводятся как сокращения:

${\displaystyle \exists xA(x)\leftrightharpoons A(\varepsilon _{x}A(x));\quad \forall xa\leftrightharpoons \neg \exists x\,\neg A}$;

аксиома индукции оказывается выводимой.

Формулы формальной арифметики, содержащие свободные переменные, задают теоретико-числовые предикаты. Формулы, не содержащие свободных переменных (замкнутые формулы), выражают суждения. ${\displaystyle k}$-местный предикат ${\displaystyle {\mathcal {P}}}$ от натуральных чисел называется арифметическим, если найдётся такая арифметическая формула ${\displaystyle P(x_{1},\dots ,x_{k})}$, что для любых натуральных чисел ${\displaystyle n_{1},\dots ,n_{k}}$ имеет место

${\displaystyle P(n_{1},\dots ,n_{k})\leftrightarrow \langle n_{1},\dots ,n_{k}\rangle \in {\mathcal {P}}}$.

Это определяет классификацию арифметических предикатов по типу префикса в предваренной форме соответствующей формулы. Класс ${\displaystyle \Sigma _{n}}$ (класс ${\displaystyle \Pi _{n}}$) состоит из предикатов ${\displaystyle P(\alpha )}$, изобразимых формулой вида

${\displaystyle Q_{1}x_{1}Q_{2}x_{2}\dots Q_{n}x_{n}(f(x_{1},\dots ,x_{n},\alpha )=0)}$,

где ${\displaystyle f}$ – примитивно рекурсивная функция, ${\displaystyle Q_{1}}$ есть ${\displaystyle \exists }$ (соответственно ${\displaystyle \forall }$) и ${\displaystyle Q_{i}}$ – чередующиеся кванторы (то есть ${\displaystyle Q_{i+1}}$ есть ${\displaystyle {\overline {Q}}_{i}}$, где ${\displaystyle {\overline {\forall }}}$ есть ${\displaystyle \exists }$, а ${\displaystyle {\overline {\exists }}}$ есть ${\displaystyle \forall }$). Каждый из этих классов содержит универсальный предикат, то есть такой предикат ${\displaystyle T(e,a)}$, что для всякого одноместного предиката ${\displaystyle P}$ из того же класса имеется число ${\displaystyle e_{p}}$, для которого верно ${\displaystyle \forall x(T(e_{p},x)\equiv P(x))}$. Многоместные предикаты сводятся к одноместным с помощью функций, нумерующих системы натуральных чисел. При каждом ${\displaystyle n>0}$ справедливо неравенство ${\displaystyle \Sigma _{n}\neq \Pi _{n}}$, и класс с меньшим индексом есть собственная часть любого класса с большим индексом. Классификация предикатов порождает классификацию арифметических функций на основе классификации соответствующих графиков. Не все теоретико-числовые предикаты арифметические: примером неарифметического предиката является такой предикат ${\displaystyle T(x)}$, что для любой замкнутой арифметической формулы ${\displaystyle A}$ имеет место ${\displaystyle T({\overset {\lceil }{}}A{\overset {\rceil }{}})\equiv A}$, где ${\displaystyle {\overset {\lceil }{}}A{\overset {\rceil }{}}}$ – номер формулы ${\displaystyle A}$ в некоторой фиксированной нумерации, удовлетворяющей естественным условиям. Предикат ${\displaystyle T}$ играет существенную роль в исследованиях структуры формальной арифметики, в частности вопроса о независимости её аксиом.

Присоединение к формальной арифметике символа ${\displaystyle T}$ с аксиомами типа ${\displaystyle T({\overset {\lceil }{}}A\&B{\overset {\rceil }{}})\equiv T({\overset {\lceil }{}}A{\overset {\rceil }{}})\&T({\overset {\lceil }{}}B{\overset {\rceil }{}})}$, выражающими его перестановочность с логическими связками, позволяет доказать непротиворечивость формальной арифметики. Та же конструкция (но уже внутри формальной арифметики) проходит для подсистемы ${\displaystyle A_{[n]}}$ системы формальной арифметики, в которой схема индукции ограничена условием: индукционная формула имеет сложность ${\displaystyle \leq n}$, то есть принадлежит ${\displaystyle \Pi _{n}\bigcup \Sigma _{n}}$. Роль ${\displaystyle T}$ здесь успешно исполняет, например, универсальный предикат для ${\displaystyle \Sigma _{[n+1]}}$, и соответствующее доказательство проводится в системе ${\displaystyle A_{[n+1]}}$. В силу второй теоремы Гёделя о неполноте отсюда следует, что ${\displaystyle A_{[n+1]}}$ сильнее ${\displaystyle A_{[n]}}$, так что формальная арифметика не совпадает ни с одной из систем ${\displaystyle A_{[n]}}$ и схему индукции нельзя заменить никаким конечным множеством аксиом. Формальная арифметика оказывается полной относительно формул из класса ${\displaystyle \Sigma _{1}}$: замкнутая формула из этого класса выводима в формальной арифметике тогда и только тогда, когда она истинна. Так как класс ${\displaystyle \Sigma _{1}}$ содержит алгоритмически неразрешимый предикат, отсюда следует, что проблема выводимости в формальной арифметике алгоритмически неразрешима.

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

${\displaystyle {\frac {A(0)A(1)\dots A(N)\dots }{\forall x\,A(x)}}}$.

На этом пути было получено одно из первых доказательств непротиворечивости формальной арифметики. При фактическом построении системы с ${\displaystyle \omega }$-правилом основным оказывается предикат «число ${\displaystyle e}$ есть номер общерекурсивной функции, описывающей вывод длины ${\displaystyle <\varepsilon _{0}}$ с ${\displaystyle \omega }$-правилом (${\displaystyle \omega }$-вывод)». Этот предикат принадлежит классу ${\displaystyle \Pi _{2}}$, и получающаяся система оказывается не формальной, а лишь полуформальной. Каждому выводу формулы ${\displaystyle A}$ в формальной арифметике удаётся сопоставить такое число ${\displaystyle e}$, что суждение «${\displaystyle e}$ есть ${\displaystyle \omega }$-вывод формулы ${\displaystyle A}$ без сечения» истинно (и даже доказуемо в формальной арифметике). Так как ${\displaystyle \omega }$-вывод без сечения замкнутой бескванторной формулы не содержит кванторов, отсюда следует непротиворечивость формальной арифметики. Применение второй теоремы Гёделя о неполноте позволяет получить отсюда, что теорема об устранении сечения из любого вывода в формальной арифметике не может быть доказана средствами формальной арифметики; тем не менее это может быть доказано в формальной арифметике при любом фиксированном ${\displaystyle N}$ для любого вывода с индукциями сложности ${\displaystyle \leq N}$. Переход к ${\displaystyle \omega }$-выводам позволяет устанавливать многие метаматематические теоремы о системе формальной арифметики, в частности полноту относительно формул из ${\displaystyle \Sigma _{1}}$ и ординальную характеристику доказуемо рекурсивных функций.