Перегляд вихідного коду сторінки Формальна арифметика

{{Переписати|дата=серпень 2018}}
{{Автопереклад|дата=січень 2014}}

[[Файл:Magnitsky.djvu|page=3|thumb|Підручник з арифметики [[Магницький Леонтій Пилипович|Леонтія Магницького]], 1703 рік]]
[[Файл:Giuseppe Peano.jpg|200px|thumb|right|[[Джузеппе Пеано]] в 1889 році сформулював [[Аксіоми Пеано|аксіоми натуральних чисел]]]]
[[Файл:Arithmetria.jpg|thumb|right|200px|[[Бехам Ганс Себальд|Ганс Себальд Бехам]]. Арифметика. XVI век]]
'''Формальна арифметика'''&nbsp;— це формулювання [[Арифметика|арифметики]] у вигляді [[Формальна система|формальної (аксіоматичної) системи]].

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

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

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

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

== Означення ==
Формальна арифметика <math>\mbox{A}</math> – це числення предикатів, в якому є:
# Предметна константа <math>\mbox{0}</math>.
# Двомісні функціональні символи <math>\mbox{+}</math> та <math>\times</math>, одномісний функціональний символ <math>\mbox{´}</math>.
# Двомісний предикат <math>\mbox{=}</math> (<math>\urcorner\mbox{=}</math> позначатимемо через <math>\ne</math>).
# Власні схеми аксіом:
#* <math>\mbox{(P(0)}\wedge\forall\mbox{x(P(x)}\rightarrow\mbox{ P(x´)))}\rightarrow\forall\mbox{xP(x)}</math>.
#* <math>\mbox{t1´=t2´}\rightarrow\mbox{t1=t2}</math>
#*<math>\mbox{t´}\ne\mbox{0}</math>
#*<math>\mbox{t1=t2}\rightarrow\mbox{(t1=t3}\rightarrow\mbox{t2=t3)}</math>
#*<math>\mbox{t1=t2}\rightarrow\mbox{t1´=t2´}</math>
#*<math>\mbox{t+0=t}</math>
#*<math>\mbox{t1+t2´=(t1 + t2)´}</math>
#*<math>\mbox{t}\times\mbox{0=0}</math>
#*<math>\mbox{t1}\times\mbox{t2´=t1}\times\mbox{t2+t1}</math>
Тут <math>\mbox{P}</math> – довільна формула, а <math>\mbox{t}</math>, <math>\mbox{t1}</math>, <math>\mbox{t2}</math> – довільні терми теорії <math>\mbox{A}</math>. Схема аксіом виражає
принцип математичної індукції.

== Класифікація ==
Формальна арифметика поділяється на такі види:
* [[класична формальна арифметика з D-оператором]];
* [[класична формальна арифметика з P-опера тором]];
* [[конструктивна формальна арифметика]].

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

== Джерела ==
* [http://vseslova.com.ua/word/Формальна_арифметика-114685u/ Формальна арифметика]
* [https://web.archive.org/web/20150117033631/http://www.imath.kiev.ua/~drozd/Logic.pdf Основи математичної логіки]
* [https://web.archive.org/web/20141129050336/http://www.vuzllib.su/books/7619-Констуктивная_математическая_логика_с_точки_зрения_классической/31-%C2%A7_2._Классическая_формальная_арифметика_с_р-опера_тором/ Класична формальна арифметика з P-оператором]
* [http://www.vuzllib.su/books/7619-Констуктивная_математическая_логика_с_точки_зрения_классической/30-%C2%A7_1._Классическая_формальная_арифметика_с_D-оператором/Класична формальна арифметика з D-оператором ]{{Недоступне посилання|date=липень 2019 |bot=InternetArchiveBot }}
* [https://web.archive.org/web/20141129050339/http://www.vuzllib.su/books/7619-Констуктивная_математическая_логика_с_точки_зрения_классической/33-%C2%A7_4._Конструктивная_формальная_арифметика/ Конструктивна формальна арифметика]
* [https://web.archive.org/web/20161130183009/http://oim.asu.kpi.ua/files/DM/17_Predicate_calculus.pdf Числення предикатів]

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

[[Категорія:Математична логіка]]
[[Категорія:Теоретична інформатика]]