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

Средства формальной арифметики оказываются достаточными для вывода теорем, устанавливаемых в стандартных курсах элементарной теории чисел. В настоящее время (1970-е годы), по-видимому, неизвестно ни одной содержательной теоретико-числовой теоремы, доказанной без привлечения средств анализа, которая не была бы выводима в формальной арифметике. Запись и доказательство таких теорем в формальной арифметике требует выявления её выразительных возможностей. Особенно существенна выразимость в формальной арифметике многих теоретикочисловых функций. В частности, в формальной арифметике можно записывать суждения о примитивно (и даже частично) рекурсивных функциях. При этом оказываются выводимыми формулы, выражающие важные свойства частично рекурсивных функций, в частности их определяющие равенства. Так, равенство $f(x')=g(x,f(x))$ выражается формулой$$\forall a \forall b \forall c\, (F(x',a)\& F(x,b)\& G(x,b,c)\to a=c),$$где $F$ и $G$ – формулы, изображающие графики функций $f$ и $g$, соответственно. В формальной арифметике можно формулировать суждения о конечных множествах. Более того, классическая формальная арифметика эквивалентна аксиоматической теории множеств Цермело – Френкеля без аксиомы бесконечности: в каждой из этих систем может быть построена модель другой.

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

При исследовании структуры формальной арифметики (в частности, вопросов непротиворечивости) используется её формулировка без кванторов, но с гильбертовским $\varepsilon$-символом. При построении формул этой системы не допускается употребление кванторов, но разрешается использование термов вида $\varepsilon_x A(x)$ (некоторое $x$, удовлетворяющее условию $A$, если такие $x$ существуют, и $0$ в противном случае). Постулаты $\varepsilon$-системы – это постулаты исчисления высказываний, правила для равенства, правило подстановки вместо свободной числовой переменной, аксиомы для функций $+$, $\cdot$, $'$, $pd$ (вычитание $1$ из положительных чисел) и следующие $\varepsilon$-аксиомы:$$\begin{gathered} A(a)\to A(\varepsilon_x A(x));\quad A(a)\to \varepsilon_x A(x)\ne a';\\ \neg A(\varepsilon_x A(x)) \to \varepsilon_x A(x)=0. \end{gathered}$$Кванторы вводятся как сокращения:$$\exists x A(x) \leftrightharpoons A(\varepsilon_x A(x)); \quad \forall x a\leftrightharpoons \neg\exists x \,\neg A;$$аксиома индукции оказывается выводимой.

Формулы формальной арифметики, содержащие свободные переменные, задают теоретико-числовые предикаты. Формулы, не содержащие свободных переменных (замкнутые формулы), выражают суждения. $k$-местный предикат $\mathscr P$ от натуральных чисел называется арифметическим, если найдётся такая арифметическая формула $P(x_1,\dots,x_k)$, что для любых натуральных чисел $n_1,\dots,n_k$ имеет место$$P(n_1,\dots,n_k)\leftrightarrow \langle n_1,\dots,n_k\rangle \in\mathscr P.$$Это определяет классификацию арифметических предикатов по типу префикса в предваренной форме соответствующей формулы. Класс $\Sigma_n$ (класс $\Pi_n$) состоит из предикатов $P(\alpha)$, изобразимых формулой вида$$Q_1x_1Q_2x_2\dots Q_n x_n (f(x_1,\dots,x_n,\alpha)=0),$$где $f$ – примитивно рекурсивная функция, $Q_1$ есть $\exists$ (соответственно $\forall$) и $Q_i$ – чередующиеся кванторы (то есть $Q_{i+1}$ есть $\overline Q_i$, где $\overline{\forall}$ есть $\exists$, а $\overline{\exists}$ есть $\forall$). Каждый из этих классов содержит универсальный предикат, то есть такой предикат $T(e,a)$, что для всякого одноместного предиката $P$ из того же класса имеется число $e_p$, для которого верно $\forall x( T(e_p,x)\equiv P(x))$. Многоместные предикаты сводятся к одноместным с помощью функций, нумерующих системы натуральных чисел. При каждом $n>0$ справедливо неравенство $\Sigma_n\ne \Pi_n$, и класс с меньшим индексом есть собственная часть любого класса с большим индексом. Классификация предикатов порождает классификацию арифметических функций на основе классификации соответствующих графиков. Не все теоретико-числовые предикаты арифметические: примером неарифметического предиката является такой предикат $T(x)$, что для любой замкнутой арифметической формулы $A$ имеет место $T(\overset{\lceil}{} A \overset{\rceil}{}) \equiv A$, где $\overset{\lceil}{} A \overset{\rceil}{}$ – номер формулы $A$ в некоторой фиксированной нумерации, удовлетворяющей естественным условиям. Предикат $T$ играет существенную роль в исследованиях структуры формальной арифметики, в частности вопроса о независимости её аксиом.

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

При задании формальной арифметики в виде формальной системы Генцена обычного типа сечение оказывается неустранимым. Устранение сечения становится возможным, если заменить схему индукции правилом бесконечной индукции ($\omega$-правило):$$\frac{A(0) A(1)\dots A(N)\dots}{\forall x\, A(x)}.$$На этом пути было получено одно из первых доказательств непротиворечивости формальной арифметики. При фактическом построении системы с $\omega$-правилом основным оказывается предикат «число $e$ есть номер общерекурсивной функции, описывающей вывод длины $<\varepsilon_0$ с $\omega$-правилом ($\omega$-вывод)». Этот предикат принадлежит классу $\Pi_2$, и получающаяся система оказывается не формальной, а лишь полуформальной. Каждому выводу формулы $A$ в формальной арифметике удаётся сопоставить такое число $e$, что суждение «$e$ есть $\omega$-вывод формулы $A$ без сечения» истинно (и даже доказуемо в формальной арифметике). Так как $\omega$-вывод без сечения замкнутой бескванторной формулы не содержит кванторов, отсюда следует непротиворечивость формальной арифметики. Применение второй теоремы Гёделя о неполноте позволяет получить отсюда, что теорема об устранении сечения из любого вывода в формальной арифметике не может быть доказана средствами формальной арифметики; тем не менее это может быть доказано в формальной арифметике при любом фиксированном $N$ для любого вывода с индукциями сложности $\le N$. Переход к $\omega$-выводам позволяет устанавливать многие метаматематические теоремы о системе формальной арифметики, в частности полноту относительно формул из $\Sigma_1$ и ординальную характеристику доказуемо рекурсивных функций.