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

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

Підручник з арифметики Леонтія Магницького, 1703 рік

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

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

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

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

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

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

Означення

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

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

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

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

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

• ;
• ;
• .

Див. також

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

Джерела

• Формальна арифметика
• формальна арифметика з D-оператором ^{[недоступне посилання з липня 2019]}

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

• Українська радянська енциклопедія : у 12 т. / гол. ред. М. П. Бажан ; редкол.: О. К. Антонов та ін. — 2-ге вид. — К. : Головна редакція УРЕ, 1974–1985.
• Арнольд І. В. Теоретична арифметика. К., 1939;
• Погребиський Й. Б. Арифметика. — Київ : Освіта, 1953.(укр.)
• Беллюстин В. К. Как постепенно дошли люди до настоящей арифметики. М., 1940;
• Гильберт Д., Аккерман В. Основы теоретической логики. М., 1947
• Клини С. К. Введение в метаматематику. М., 1957
• Мендельсон Э. Введение в математическую логику. М., 1976
• Новиков П. С. Элементы математической логики. М., 1959
• Черч А. Введение в математическую логику, т. I. М. 1960
• Філософський словник / за ред. В. І. Шинкарука. — 2-ге вид., перероб. і доп. — К. : Головна ред. УРЕ, 1986.