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

Файл:Magnitsky.djvu

Джузеппе Пеано в 1889 році сформулював аксіоми натуральних чисел

Ганс Себальд Бехам. Арифметика. XVI век

Формальна арифметика — це формулювання арифметики у вигляді формальної (аксіоматичної) системи.

Мова формальної арифметики містить константу $\text{0}$, числові змінні, символ рівності, функціональні символи $\text{+}$, $\times$, (збільшення 1) і логічні зв'язки. Постулатами формальної арифметики є аксіоми і правила виводу числення предикатів, що визначають рівність для арифметичних операцій. Засоби формальної арифметики достатні для виведення теорем елементарної теорії чисел. На даний момент невідомо жодної змістовної теоретико-числової теореми, доведеної без залучення засобів аналізу, яка не виводилася б у формальну арифметику. У формальній арифметиці змальовані рекурсивні функції і їх визначена рівність. Це дозволяє формулювати думки про скінченну множину. Більш того, формальна арифметика еквівалентна аксіоматичній теорії множин Цермела – Френкеля. Без аксіоми нескінченності у кожній з цих систем може бути побудована інша модель.

Формальна арифметика задовольняє умовам обох теорем Геделя про неповноту. Зокрема, є такі поліноми $\text{P}$ , $\text{Q}$ від 9 змінних, що формула " $\text{x1...x9}$ " $\text{(P1Q)}$ не виводиться, хоча і виражає дійсну думку, а саме несуперечність формальної арифметики. Тому нерозв'зність діофантового рівняння Р-Q=0 недоказова у формальній арифметиці. Несуперечність формальної арифметики доведена за допомогою трансфінітної індукції до ординала е0 (найменший розв'язок рівняння $\text{we=e}$). Тому схема індукції до е0 недоказова у формальній арифметиці, хоча там доказова схема індукції до будь-якого ординала а<e0. Класу доказово рекурсивних функцій формальної арифметики (тобто частково рекурсивних функцій, загальна рекурсивність яких може бути встановлена засобами формальної арифметики) збігається з класом ординально-рекурсивних функцій з ординалами <e0.

Не всі теоретико-числові предикати виражаються у формальній арифметиці: прикладом є такий предикат $\text{T}$, що для будь-якої замкнутої арифметичної формули $\text{A}$ має місце Т (é А ù) , де é А ù – номер формули $\text{A}$ в деякій фіксованій нумерації, що задовольняє природним умовам. Приєднання до формальної арифметики символу $\text{T}$, що виражають його перестановку з логічними зв'язками, що дозволяє довести не суперечність формально арифметики. Схожа конструкція доводить, що схему індукції не можна замінити жодною кінцевою безліччю аксіом. Формальна арифметика коректна і повна відносно формул вигляду "$\text{x 1 ... x}$" до $\text{( P=Q )}$; замкнута формула з цього класу доказова тоді і лише тоді, коли вона достеменна. Оскільки цей клас містить алгоритмічно нерозв'язний предикат, звідси випливає, що проблема вивідності у формальній арифметиці алгоритмічно нерозв'язна.

При заданні формальної арифметики у вигляді гензенівської системи реалізована нормалізація виводу, причому нормальне виведення числової рівності складається лише з числової рівності. На цьому шляху було отримано перший доказ несуперечності формальної арифметики. Нормальне виведення формули з кванторами може містити скільки завгодно складних формул. Повна підформульність досягається після заміни схеми індукції на со-правило. Поняття $\text{w}$-виведення (тобто виводу з $\text{w}$-правилом) висоти <e0 виражається у формальній арифметиці, тому перехід до $\text{w}$-виводів дозволяє встановлювати у Ф. а. багато метаматематичних теорем, зокрема повноту і ординальну характеристику рекурсивних функцій.

Означення

Формальна арифметика $\text{A}$ – це числення предикатів, в якому є:

1. Предметна константа $\text{0}$.
2. Двомісні функціональні символи $\text{+}$ та $\times$, одномісний функціональний символ $\text{´}$.
3. Двомісний предикат $\text{=}$ ($⌝\text{=}$ позначатимемо через $\ne$).
4. Власні схеми аксіом:
   • $\text{(P(0)}\wedge \mathrm{\forall }\text{x(P(x)}\to \text{ P(x´)))}\to \mathrm{\forall }\text{xP(x)}$.
   • $\text{t1´=t2´}\to \text{t1=t2}$
   • $\text{t´}\ne \text{0}$
   • $\text{t1=t2}\to \text{(t1=t3}\to \text{t2=t3)}$
   • $\text{t1=t2}\to \text{t1´=t2´}$
   • $\text{t+0=t}$
   • $\text{t1+t2´=(t1 + t2)´}$
   • $\text{t}\times \text{0=0}$
   • $\text{t1}\times \text{t2´=t1}\times \text{t2+t1}$

Тут $\text{P}$ – довільна формула, а $\text{t}$, $\text{t1}$, $\text{t2}$ – довільні терми теорії $\text{A}$. Схема аксіом виражає принцип математичної індукції.

Класифікація

Формальна арифметика поділяється на такі види:

• класична формальна арифметика з D-оператором;
• класична формальна арифметика з P-опера тором;
• конструктивна формальна арифметика.

Див. також

• Теоретична арифметика
• Числення висловлень
• Квантор
• Правило резолюцій
• Числення секвенцій
• Логіка другого порядку
• Теорема Льовенгейма—Сколема
• Нормальна форма Сколема

Джерела

• Формальна арифметика
• Основи математичної логіки
• Класична формальна арифметика з P-оператором
• формальна арифметика з D-оператором Шаблон:Недоступне посилання
• Конструктивна формальна арифметика
• Числення предикатів

Список літератури

• Шаблон:УРЕ
• Арнольд І. В. Теоретична арифметика. К., 1939;
• Шаблон:Погребиський.Арифметика
• Беллюстин В. К. Как постепенно дошли люди до настоящей арифметики. М., 1940;
• Гильберт Д., Аккерман В. Основы теоретической логики. М., 1947
• Клини С. К. Введение в метаматематику. М., 1957
• Мендельсон Э. Введение в математическую логику. М., 1976
• Новиков П. С. Элементы математической логики. М., 1959
• Черч А. Введение в математическую логику, т. I. М. 1960
• Шаблон:ФС