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

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

История

Предпосылки возникновения

Идея формализации арифметики восходит к работам Готфрида Вильгельма Лейбница, который в XVII веке предложил создать универсальный язык науки (characteristica universalis) и исчисление рассуждений (calculus ratiocinator). Однако практическая реализация этой идеи стала возможной лишь в конце XIX — начале XX века благодаря развитию математической логики.

Аксиоматизация Пеано

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

Формализация Гильберта

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

Теоремы Гёделя

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

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

Формальная арифметика строится как формальная система, включающая:

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

Язык формальной арифметики

Язык формальной арифметики первого порядка (часто обозначаемый как \(L_{PA}\)) включает:

• Индивидуальные переменные: \(x, y, z, \dots\) (счётное множество), обозначающие натуральные числа.
• Индивидуальную константу: \(0\) (нуль).
• Функциональные символы: \(S\) (одноместный — функция следования, \(S(x)\) означает \(x+1\)), \(+\) (двухместный — сложение), \(\times\) (двухместный — умножение).
• Предикатный символ: \(=\) (двухместный — равенство).
• Логические связки: \(\neg\) (отрицание), \(\land\) (конъюнкция), \(\lor\) (дизъюнкция), \(\rightarrow\) (импликация), \(\leftrightarrow\) (эквиваленция).
• Кванторы: \(\forall\) (квантор всеобщности), \(\exists\) (квантор существования).

Аксиомы формальной арифметики

Аксиомы формальной арифметики (аксиомы Пеано, записанные на формальном языке) делятся на две группы:

Аксиомы равенства (определяют свойства отношения равенства):

1. \(\forall x (x = x)\) (рефлексивность).
2. \(\forall x \forall y (x = y \rightarrow y = x)\) (симметричность).
3. \(\forall x \forall y \forall z ((x = y \land y = z) \rightarrow x = z)\) (транзитивность).
4. \(\forall x \forall y (x = y \rightarrow S(x) = S(y))\) (замена в функции следования).
5. \(\forall x \forall y \forall z (x = y \rightarrow x + z = y + z)\) и \(\forall x \forall y \forall z (x = y \rightarrow z + x = z + y)\) (замена в сложении).
6. \(\forall x \forall y \forall z (x = y \rightarrow x \times z = y \times z)\) и \(\forall x \forall y \forall z (x = y \rightarrow z \times x = z \times y)\) (замена в умножении).

Собственно арифметические аксиомы:

1. \(\forall x \neg (S(x) = 0)\) (нуль не является последователем никакого числа).
2. \(\forall x \forall y (S(x) = S(y) \rightarrow x = y)\) (функция следования инъективна).
3. \(\forall x (x + 0 = x)\) (определение сложения с нулём).
4. \(\forall x \forall y (x + S(y) = S(x + y))\) (рекурсивное определение сложения).
5. \(\forall x (x \times 0 = 0)\) (определение умножения на нуль).
6. \(\forall x \forall y (x \times S(y) = (x \times y) + x)\) (рекурсивное определение умножения).
7. Схема аксиом индукции: для любой формулы \(\phi(x)\) с одной свободной переменной \(x\) аксиомой является формула:

\[ (\phi(0) \land \forall x (\phi(x) \rightarrow \phi(S(x)))) \rightarrow \forall x \phi(x). \] Эта схема бесконечна, так как включает отдельную аксиому для каждой формулы \(\phi\).

Правила вывода

Основным правилом вывода является modus ponens: если выведены формулы \(A\) и \(A \rightarrow B\), то выводима \(B\). Также используются правила работы с кванторами (обобщение и конкретизация).

Свойства формальной арифметики

Непротиворечивость

Формальная арифметика непротиворечива, если в ней нельзя вывести одновременно формулу \(A\) и её отрицание \(\neg A\). Непротиворечивость формальной арифметики была доказана Герхардом Генценом в 1936 году с использованием трансфинитной индукции до ординала \(\varepsilon_0\). Это доказательство выходит за рамки самой формальной арифметики, что согласуется со второй теоремой Гёделя.

Полнота

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

Разрешимость

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

Модели формальной арифметики

Стандартная модель

Стандартной моделью формальной арифметики является множество натуральных чисел \(\mathbb{N} = \{0, 1, 2, \dots\}\) с обычными операциями сложения и умножения. В этой модели все аксиомы истинны, а множество теорем совпадает с множеством формул, истинных в \(\mathbb{N}\).

Нестандартные модели

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

Применение

Формальная арифметика является фундаментом для многих разделов математической логики и теории доказательств:

• Теория доказательств: изучение структуры доказательств, их нормализации и силы.
• Теория рекурсии: связь с вычислимыми функциями и алгоритмами.
• Теория моделей: исследование моделей арифметики и их свойств.
• Основания математики: анализ аксиоматических систем и их ограничений.

Критика и ограничения

Формальная арифметика подвергалась критике со стороны интуиционистов (Лёйтзен Брауэр, Аренд Гейтинг), которые отрицали закон исключённого третьего и требовали конструктивных доказательств. В ответ были разработаны интуиционистские версии арифметики (арифметика Гейтинга), где не используется закон исключённого третьего.

Теоремы Гёделя показали, что формальная арифметика не может быть одновременно полной и непротиворечивой, что ограничивает её возможности как инструмента для обоснования всей математики. Тем не менее, она остаётся центральным объектом изучения в математической логике.

Источники

• Гильберт Д., Бернайс П. Основания математики. Том 1. — М.: Наука, 1979.
• Гёдель К. О формально неразрешимых предложениях Principia Mathematica и родственных систем I. — 1931.
• Мендельсон Э. Введение в математическую логику. — М.: Наука, 1984.
• Булос Дж., Джеффри Р. Вычислимость и логика. — М.: Мир, 1994.