stringtranslate.com

Примитивная рекурсивная арифметика

Примитивно-рекурсивная арифметика ( 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 . Отрицание можно выразить как .

Смотрите также

Примечания

  1. ^ перепечатано в переводе ван Хейеноорта (1967).
  2. ^ Тейт 1981.
  3. ^ Крайзель 1960.

Ссылки

Дополнительное чтение