Большая Советская Энциклопедия (ФО)

•b’ = (а •b ) + а ,

аксиомы Пеано:

ù(а’ = 0), a’ = b’ ® а = b ,

(a = b & а = с ) ® b = с , а = b ®a ' = b '

и схема аксиом индукции:

А (0) & ' x (А (х ) ® А (x ')) ® ' xa (x ).

  Средства Ф. а. достаточны для вывода теорем элементарной теории чисел. В настоящее время, по- видимому, неизвестно ни одной содержательной теоретико-числовой теоремы, доказанной без привлечения средств анализа, которая не была бы выводима в Ф. а. В Ф. а. изобразимы рекурсивные функции и доказуемы их определяющие равенства. Это позволяет, в частности, формулировать суждения о конечных множествах. Более того, Ф. а. эквивалентна аксиоматической теории множеств Цермело – Френкеля без аксиомы бесконечности: в каждой из этих систем может быть построена модель другой.

  Ф. а. удовлетворяет условиям обеих теорем Гёделя о неполноте. В частности, имеются такие полиномы Р , Q от 9 переменных, что формула ' x ₁ ... 'x ₉ (P &sup1; Q ) невыводима, хотя и выражает истинное суждение, а именно непротиворечивость Ф. а. Поэтому неразрешимость диофантова уравнения Р - Q = 0 недоказуема в Ф. а. Непротиворечивость Ф. а. доказана с помощью трасфинитной индукции до ординала e₀ (наименьшее решение уравнения w^e = e). Поэтому схема индукции до e₀ недоказуема в Ф. а., хотя там доказуема схема индукции до любого ординала a < e₀ . Класс доказуемо рекурсивных функций Ф. а. (т. е. частично рекурсивных функций, общерекурсивность которых может быть установлена средствами Ф. а.) совпадает с классом ординально рекурсивных функций с ординалами < e₀ .

  Не все теоретико-числовые предикаты выразимы в Ф. а.: примером является такой предикат T, что для любой замкнутой арифметической формулы А имеет место Т (éА ù) « А, где éА ù – номер формулы А в некоторой фиксированной нумерации, удовлетворяющей естественным условиям. Присоединение к Ф. а. символа Т с аксиомами типа

Т (éА & B ù) « Т (éА ù) & Т (éB ù),

выражающими его перестановочность с логическими связками, позволяет доказать непротиворечивость Ф. а. Похожая конструкция (но уже внутри Ф. а.) доказывает, что схему индукции нельзя заменить никаким конечным множеством аксиом. Ф. а. корректна и полна относительно формул вида $x ₁ ... $x_k (P = Q ); замкнутая формула из этого класса доказуема тогда и только тогда, когда она истинна. Так как этот класс содержит алгоритмически неразрешимый предикат, отсюда следует, что проблема выводимости в Ф. а. алгоритмически неразрешима.