Примитивно-рекурсивная арифметика ( PRA ) — это формализация натуральных чисел без кванторов . Впервые она была предложена норвежским математиком Скулемом (1923) [1] как формализация его финитной концепции основ арифметики , и широко распространено мнение, что все рассуждения PRA являются финитными. Многие также считают, что весь финитизм охватывается PRA [2], но другие полагают, что финитизм может быть расширен до форм рекурсии за пределами примитивной рекурсии, вплоть до ε [3], что является теоретическим ординалом доказательства арифметики Пеано . Теоретический ординал доказательства PRA — это ω ω , где ω — наименьший трансфинитный ординал . PRA иногда называют арифметикой Скулема , хотя это имеет и другое значение, см. Арифметика Скулема .
Язык PRA может выражать арифметические предложения, включающие натуральные числа и любую примитивную рекурсивную функцию , включая операции сложения , умножения и возведения в степень . PRA не может явно квантифицировать область натуральных чисел. PRA часто принимается за основную метаматематическую формальную систему для теории доказательств , в частности, для доказательств непротиворечивости, таких как доказательство непротиворечивости арифметики первого порядка Генцена .
Язык PRA состоит из:
Логическими аксиомами PRA являются:
Логические правила PRA — это modus ponens и подстановка переменных .
Нелогические аксиомы, во-первых:
где всегда обозначает отрицание , так что, например, является отрицаемым предложением.
Далее, рекурсивные определяющие уравнения для каждой примитивной рекурсивной функции могут быть приняты в качестве аксиом по желанию. Например, наиболее распространенной характеристикой примитивных рекурсивных функций является как константа 0 и функция-последователь, замкнутая относительно проекции, композиции и примитивной рекурсии. Так, для ( n +1)-местной функции f, определенной примитивной рекурсией над n -местной базовой функцией g и ( n +2)-местной итерационной функцией h, будут определяющие уравнения:
Особенно:
PRA заменяет схему аксиом индукции для арифметики первого порядка правилом индукции (без кванторов):
В арифметике первого порядка единственными примитивно-рекурсивными функциями , которые необходимо явно аксиоматизировать, являются сложение и умножение . Все остальные примитивно-рекурсивные предикаты можно определить с помощью этих двух примитивно-рекурсивных функций и квантификации по всем натуральным числам . Определение примитивно-рекурсивных функций таким образом невозможно в PRA, поскольку в ней отсутствуют квантификаторы.
Можно формализовать PRA таким образом, что в нем вообще не будет логических связок — предложение PRA — это просто уравнение между двумя терминами. В этой постановке термин — это примитивная рекурсивная функция нуля или более переменных. Карри (1941) дал первую такую систему. Правило индукции в системе Карри было необычным. Более позднее уточнение было дано Гудштейном (1954). Правило индукции в системе Гудштейна следующее:
Здесь x — переменная, S — операция-последователь, а F , G и H — любые примитивные рекурсивные функции, которые могут иметь параметры, отличные от показанных. Единственными другими правилами вывода системы Гудстейна являются правила подстановки, как показано ниже:
Здесь A , B , и C — любые термины (примитивно-рекурсивные функции от нуля или более переменных). Наконец, существуют символы для любых примитивно-рекурсивных функций с соответствующими определяющими уравнениями, как в системе Сколема выше.
Таким образом, исчисление высказываний может быть полностью отброшено. Логические операторы могут быть выражены полностью арифметически, например, абсолютное значение разности двух чисел может быть определено примитивной рекурсией:
Таким образом, уравнения x = y и эквивалентны. Следовательно, уравнения и выражают логическую конъюнкцию и дизъюнкцию соответственно уравнений x = y и u = v . Отрицание можно выразить как .