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

Примитивная рекурсивная арифметика ( PRA ) представляет собой кванторов без формализацию натуральных чисел . Впервые его предложил норвежский математик Сколем (1923) . как формализация его финитистской концепции основ арифметики , и широко распространено мнение, что все рассуждения PRA являются финитистскими. Многие также считают, что весь финитизм захвачен PRA, но другие полагают, что финитизм можно распространить на формы рекурсии, выходящие за рамки примитивной рекурсии, вплоть до ε ₀ , который является теоретико-доказательным ординалом арифметики Пеано . Теоретический ординал доказательства PRA равен ω. ^ой , где ω — наименьший трансфинитный ординал . PRA иногда называют скулемской арифметикой , хотя это имеет и другое значение, см. Скулемскую арифметику .

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

Язык и аксиомы

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

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

Логическими аксиомами PRA являются:

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

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

• $S(x)\neq 0$;
• $S(x)=S(y)\to x=y,$

где $x\neq y$ всегда означает отрицание $x=y$ так что, например, $S(0)=0$ является отрицательным предложением.

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

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

Особенно:

• $x+0=x\$
• $x+S(y)=S(x+y)\$
• $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) предложил первую такую ​​систему. Правило индукции в системе Карри было необычным. Более позднее уточнение было дано Гудштейном (1954) . Правило : индукции в системе Гудстейна

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

См. также

• Элементарная рекурсивная арифметика
• Конечнозначная логика
• Хейтинговая арифметика
• Арифметика Пеано
• Примитивная рекурсивная функция
• арифметика Робинсона
• Арифметика второго порядка
• Скулемская арифметика

Ссылки

• Карри, Хаскелл Б. (1941). «Формализация рекурсивной арифметики». Американский журнал математики . 63 (2): 263–282. дои : 10.2307/2371522 . JSTOR   2371522 . МР   0004207 .

• Гудштейн, Р.Л. (1954). «Безлогические формализации рекурсивной арифметики» . Математика Скандинавия . 2 : 247–261. дои : 10.7146/math.scand.a-10412 . МР   0087614 .

• ван Хейеноорт, Жан (1967). От Фреге до Гёделя. Справочник по математической логике, 1879–1931 гг . Кембридж, Массачусетс: Издательство Гарвардского университета. стр. 302–333. МР   0209111 .

• Крайзель, Георг (1960). «Ординальная логика и характеристика неформальных концепций доказательства» (PDF) . Материалы Международного конгресса математиков, 1958 г. Нью-Йорк: Издательство Кембриджского университета. стр. 289–299. МР   0124194 .

• Сколем, Торальф (1923). « Основы элементарной арифметики, установленные посредством рекурсивного способа мышления без использования очевидных переменных, охватывающих бесконечные области » (PDF) . Skrifter Utgit av Videnskapsselskapet I Kristiania. I класс математики-естествознания (на немецком языке). 6 :1–38.

• Тейт, Уильям В. (1981). «Финитизм». Журнал философии . 78 (9): 524–546. дои : 10.2307/2026089 . JSTOR   2026089 .

• Тейт, Уильям В. (июнь 2012 г.). «Примитивная рекурсивная арифметика и ее роль в основах арифметики: исторические и философские размышления» (PDF) . Эпистемология против онтологии . стр. 161–180. дои : 10.1007/978-94-007-4435-6_8 .

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

• Феферман, Соломон (1993). «Что на чем опирается? Теоретико-доказательный анализ математики» (PDF) . Философия математики . Дж. Чермак (ред.): 1–147.

• Роуз, HE (1961). «О непротиворечивости и неразрешимости рекурсивной арифметики». Журнал математической логики и основ математики . 7 (7-10): 124-135. дои : 10.1002/malq.19610070707 . MR0140413   .