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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до навігації Перейти до пошуку
Підручник з арифметики Леонтія Магницького, 1703 рік
Ганс Себальд Бехам. Арифметика. XVI век

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

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

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

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

Означення[ред. | ред. код]

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

  1. Предметна константа .
  2. Двомісні функціональні символи та , одномісний функціональний символ .
  3. Двомісний предикат ( позначатимемо через ).
  4. Власні схеми аксіом:
    • .

Тут – довільна формула, а , , – довільні терми теорії . Схема аксіом виражає принцип математичної індукції.

Класифікація[ред. | ред. код]

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

Джерела[ред. | ред. код]

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

Список літератури[ред. | ред. код]

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

Див. також[ред. | ред. код]