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

Примитивная рекурсивная арифметика ( PRA ) - это бескванторная формализация натуральных чисел . Впервые это было предложено Сколемом ^[1] как формализация его финитистской концепции основ арифметики , и широко признано, что все рассуждения PRA являются финитистскими. Многие также считают , что все финитизма захватывается ОРА, ^[2] , но другие считают , что Финитизм может быть продлен до форм рекурсии за пределы примитивной рекурсии, вплоть до epsi ; ₀ , ^[3] , который является доказательством теоретико-порядковое из арифметики Пеано. Теоретический ординал доказательства PRA - это ω ^ω , где ω - наименьший трансфинитный ординал . PRA иногда называют сколемской арифметикой .

Язык PRA может выражать арифметические предложения с использованием натуральных чисел и любых примитивных рекурсивных функций , включая операции сложения , умножения и возведения в степень . PRA не может явным образом определять количество в области натуральных чисел. PRA часто принимаются в качестве основного метаматематическома формальной системы для доказательства теории , в частности , для доказательства непротиворечивости , таких как доказательство непротиворечивости Генцена из арифметики первого порядка .

Язык и аксиомы [ править ]

Язык PRA состоит из:

Счетно бесконечное число переменных х , у , г , ....
В пропозициональных связках;
Символ равенства = , постоянный символ 0 и последующий символ S (означающий добавление единицы );
Символ для каждой примитивной рекурсивной функции .

Логические аксиомы PRA:

Тавтологии о исчислении ;
Обычная аксиоматизация равенства как отношения эквивалентности .

Логические правила PRA - это modus ponens и подстановка переменных .
Нелогические аксиомы:

${\ Displaystyle S (х) \ neq 0}$ ;
${\ Displaystyle S (х) = S (у) ~ \ к ~ х = у,}$

и рекурсивные определяющие уравнения для каждой примитивной рекурсивной функции по желанию. Например, наиболее распространенная характеристика примитивных рекурсивных функций - это константа 0 и функция-преемник, закрытая для проекции, композиции и примитивной рекурсии. Таким образом, для ( n + 1) -разрядной функции f, определенной посредством примитивной рекурсии по n- разрядной базовой функции g и ( n +2) -разрядной итерационной функции h , будут определяющие уравнения:

${\ displaystyle f (0, y_ {1}, \ ldots, y_ {n}) = g (y_ {1}, \ ldots, y_ {n})}$
${\ displaystyle f (S (x), y_ {1}, \ ldots, y_ {n}) = h (x, f (x, y_ {1}, \ ldots, y_ {n}), y_ {1}) , \ ldots, y_ {n})}$

Особенно:

${\ Displaystyle х + 0 = х \}$
${\ Displaystyle х + S (у) = S (х + у) \}$
$x\cdot 0=0\$
$x\cdot S(y)=x\cdot y+x\$
... и так далее.

PRA заменяет схему аксиом индукции для арифметики первого порядка правилом (бескванторной) индукции:

Из и , вывести , для любого предиката $\varphi (0)$ $\varphi (x)\to \varphi (S(x))$ $\varphi (y)$ $\varphi .$

В арифметике первого порядка единственные примитивные рекурсивные функции, которые необходимо аксиоматизировать явно, - это сложение и умножение . Все другие примитивно-рекурсивные предикаты могут быть определены с использованием этих двух примитивно-рекурсивных функций и количественной оценки всех натуральных чисел . Такое определение примитивных рекурсивных функций невозможно в PRA, поскольку в нем отсутствуют кванторы.

Исчисление без логики [ править ]

Можно формализовать PRA таким образом, чтобы в нем вообще не было логических связок - предложение PRA - это просто уравнение между двумя терминами. В этой настройке терм - это примитивная рекурсивная функция от нуля или более переменных. В 1941 году Хаскелл Карри представил первую такую систему. ^[4] Правило индукции в системе Карри было необычным. Более позднее уточнение было дано Рубеном Гудстайном . ^[5] правило индукции в системе Гудстейна является:

{F(0)=G(0)\quad F(S(x))=H(x,F(x))\quad G(S(x))=H(x,G(x)) \over F(x)=G(x)}.

Здесь x - переменная, S - последующая операция, а F , G и H - любые примитивные рекурсивные функции, которые могут иметь параметры, отличные от показанных. Единственными другими правилами вывода системы Гудстейна являются следующие правила замены:

{F(x)=G(x) \over F(A)=G(A)}\qquad {A=B \over F(A)=F(B)}\qquad {A=B\quad A=C \over B=C}.

Здесь A , B и C - любые термины (примитивно рекурсивные функции от нуля или более переменных). Наконец, есть символы для любых примитивных рекурсивных функций с соответствующими определяющими уравнениями, как в системе Сколема выше.

Таким образом можно полностью отказаться от исчисления высказываний. Логические операторы могут быть выражены полностью арифметически, например, абсолютное значение разности двух чисел может быть определено с помощью примитивной рекурсии:

{\begin{aligned}P(0)=0\quad &\quad P(S(x))=x\\x{\dot {-}}0=x\quad &\quad x{\mathrel {\dot {-}}}S(y)=P(x{\mathrel {\dot {-}}}y)\\|x-y|=&(x{\mathrel {\dot {-}}}y)+(y{\mathrel {\dot {-}}}x).\\\end{aligned}}

Таким образом, уравнения x = y и эквивалентны. Следовательно, уравнения и выражают логическое соединение и дизъюнкцию , соответственно, уравнений x = y и u = v . Отрицание можно выразить как . $|x-y|=0$ $|x-y|+|u-v|=0$ $|x-y|\cdot |u-v|=0$ $1{\dot {-}}|x-y|=0$

См. Также [ править ]

Элементарная рекурсивная арифметика
Арифметика Гейтинга
Арифметика Пеано
Арифметика второго порядка
Примитивная рекурсивная функция
Конечная логика

Ссылки [ править ]

^ Сколем, Торальф (1923), "Begründung der elementaren Arithmetik durch die rekurrierende Denkweise ohne Anwendung scheinbarer Veränderlichen mit unendlichem Ausdehnungsbereich" [Основы элементарной арифметики, установленные с помощью очевидных средств рекурсивного способа определения значений переменных без ] (PDF) , Skrifter utgit av Videnskapsselskapet i Kristiania. I, Matematisk-naturvidenskabelig klasse (на немецком языке), 6 : 1–38. CS1 maint: discouraged parameter (link). Перепечатано в переводе в van Heijenoort, Jean (1967), From Frege to Gödel. Справочник по математической логике, 1879–1931 , Кембридж, Массачусетс: издательство Гарвардского университета, стр. 302–333, MR 0209111 .
^ Тэйт, WW (1981), "Финитизм", Журнал философии , 78 : 524-546, DOI : 10,2307 / 2026089 CS1 maint: discouraged parameter (link).
^ Kreisel, Г. (1960), "порядковые логики и характеристика неформальных понятий доказательства" (PDF) , Труды Международного конгресса математиков, 1958 , Нью - Йорк:. Cambridge University Press, стр 289-299, MR 0124194 .
^ Карри, Хаскелл Б. (1941), "Формализация рекурсивной арифметики", Американский журнал математики , 63 : 263-282, DOI : 10,2307 / 2371522 , МР 0004207 .
^ Гудстейн, RL (1954), "Свободные от логики формализации рекурсивной арифметики", Mathematica Scandinavica , 2 : 247–261, MR 0087614 .

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

Rose, HE (1961), "О непротиворечивости и неразрешимости рекурсивной арифметики", Zeitschrift für Mathematische Logik und Grundlagen der Mathematik , 7 : 124–135, MR 0140413.

Феферман, S (1992) Что на чем опирается? Теоретико-доказательный анализ математики . Приглашенная лекция, 15-й международный симпозиум Витгенштейна.

[1] Сколем, Торальф (1923), "Begründung der elementaren Arithmetik durch die rekurrierende Denkweise ohne Anwendung scheinbarer Veränderlichen mit unendlichem Ausdehnungsbereich" [Основы элементарной арифметики, установленные с помощью очевидных средств рекурсивного способа определения значений переменных без ] (PDF) , Skrifter utgit av Videnskapsselskapet i Kristiania. I, Matematisk-naturvidenskabelig klasse (на немецком языке), 6 : 1–38. CS1 maint: discouraged parameter (link). Перепечатано в переводе в van Heijenoort, Jean (1967), From Frege to Gödel. Справочник по математической логике, 1879–1931 , Кембридж, Массачусетс: издательство Гарвардского университета, стр. 302–333, MR 0209111 .

[2] Тэйт, WW (1981), "Финитизм", Журнал философии , 78 : 524-546, DOI : 10,2307 / 2026089 CS1 maint: discouraged parameter (link).

[3] Kreisel, Г. (1960), "порядковые логики и характеристика неформальных понятий доказательства" (PDF) , Труды Международного конгресса математиков, 1958 , Нью - Йорк:. Cambridge University Press, стр 289-299, MR 0124194 .

[4] Карри, Хаскелл Б. (1941), "Формализация рекурсивной арифметики", Американский журнал математики , 63 : 263-282, DOI : 10,2307 / 2371522 , МР 0004207 .

[5] Гудстейн, RL (1954), "Свободные от логики формализации рекурсивной арифметики", Mathematica Scandinavica , 2 : 247–261, MR 0087614 .

[1]