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

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

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

• 1 Язык и аксиомы
• 2 Исчисление без логики
• 3 См. также
• 4 Ссылки

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

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

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

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

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

• $S\; (x)\; \ne \; 0\; \{\backslash \; displaystyle\; S\; (x)\; \backslash \; neq\; 0\}$;
• $S\; (x)\; =\; S\; (y)\; \to \; x\; =\; y,\; \{\backslash \; displaystyle\; S\; (x)\; =\; S\; (y)\; ~\; \backslash \; to\; ~\; x\; =\; y,\}$

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

• $f\; (0,\; y\; 1,\dots ,\; yn)\; =\; g\; (y\; 1,\dots ,\; yn)\; \{\backslash \; displaystyle\; f\; (0,\; y\_\; \{1\},\; \backslash \; ldots,\; y\_\; \{n\})\; =\; g\; (y\_\; \{1\},\; \backslash \; ldots,\; y\_\; \{n\; \})\}$
• $f\; (S\; (x),\; y\; 1,\dots ,\; yn)\; =\; h\; (x,\; f\; (x,\; y\; 1,\dots ,\; yn),\; y\; 1,\dots ,\; yn)\; \{\backslash \; displaystyle\; f\; (S\; (x),\; y\_\; \{1\},\; \backslash \; ldots,\; y\_\; \{n\})\; =\; h\; (x,\; f\; (x,\; y\_\; \{1\},\; \backslash \; ldots,\; y\_\; \{n\}),\; y\_\; \{1\},\; \backslash \; ldots,\; y\_\; \{\; n\})\}$

В частности:

• $x\; +\; 0\; =\; x\; \{\backslash \; displaystyle\; x\; +\; 0\; =\; x\; \backslash \}$
• $x\; +\; S\; (y)\; =\; S\; (x\; +\; y)\; \{\backslash \; displaystyle\; x\; +\; S\; (\; у)\; знак\; равно\; S\; (Икс\; +\; Y)\; \backslash \}$
• $Икс\; \cdot \; 0\; знак\; равно\; 0\; \{\backslash \; Displaystyle\; х\; \backslash \; cdot\; 0\; =\; 0\; \backslash \}$
• $Икс\; \cdot \; S\; (Y)\; =\; Икс\; \cdot \; Y\; +\; х\; \{\backslash \; Displaystyle\; х\; \backslash \; cdot\; S\; (y)\; =\; x\; \backslash \; cdot\; y\; +\; x\; \backslash \}$
• ... и т. д.

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

• From $\phi \; (0)\; \{\backslash \; displaystyle\; \backslash \; varphi\; (0)\}$и $\phi \; (x)\; \to \; \phi \; (S\; (х))\; \{\backslash \; displaystyle\; \backslash \; varphi\; (x)\; \backslash \; to\; \backslash \; varphi\; (S\; (x))\}$, выведите $\phi \; (y)\; \{\backslash \; displaystyle\; \backslash \; varphi\; (y)\}$для любого предиката $\phi .\; \{\backslash \; displaystyle\; \backslash \; varphi.\}$

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

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

$F\; (0)\; =\; G\; (0)\; F\; (S\; (x))\; =\; H\; (x,\; F\; (x))\; G\; (S\; (x))\; =\; H\; (x,\; G\; (x))\; F\; (x)\; =\; G\; (x).\; \{\backslash \; Displaystyle\; \{F\; (0)\; =\; G\; (0)\; \backslash \; четырехъядерный\; F\; (S\; (x))\; =\; H\; (x,\; F\; (x))\; \backslash \; четырехъядерный\; G\; (S\; (x))\; =\; H\; (x,\; G\; (x))\; \backslash \; over\; F\; (x)\; =\; G\; (x)\}.\}$

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

$F\; (x)\; =\; G\; (x)\; F\; (A)\; =\; G\; (A)\; A\; =\; BF\; (A)\; =\; F\; (В)\; А\; =\; ВА\; =\; СВ\; =\; С.\; \{\backslash \; Displaystyle\; \{F\; (x)\; =\; G\; (x)\; \backslash \; над\; F\; (A)\; =\; G\; (A)\}\; \backslash \; qquad\; \{A\; =\; B\; \backslash \; над\; F\; (A)\; =\; F\; (B)\}\; \backslash \; qquad\; \{A\; =\; B\; \backslash \; quad\; A\; =\; C\; \backslash \; over\; B\; =\; C\}.\}$

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

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

$P\; (0)\; =\; 0\; P\; (S\; (x))\; =\; xx\; -\; \dot{}\; 0\; =\; xx\; -\; \dot{}\; S\; (y)\; =\; P\; (x\; -\; \dot{}\; y)\; |\; х\; -\; у\; |\; =\; (х\; -\; \dot{}\; у)\; +\; (у\; -\; х).\; \{\backslash \; Displaystyle\; \{\backslash \; begin\; \{align\}\; P\; (0)\; =\; 0\; \backslash \; quad\; \backslash \; quad\; P\; (S\; (x))\; =\; x\; \backslash \backslash \; x\; \{\backslash \; dot\; \{-\}\}\; 0\; =\; x\; \backslash \; quad\; \backslash \; quad\; x\; \{\backslash \; mathrel\; \{\backslash \; dot\; \{-\}\}\}\; S\; (y)\; =\; P\; (x\; \{\backslash \; mathrel\; \{\backslash \; dot\; \{-\}\}\}\; y)\; \backslash \backslash \; |\; xy\; |\; =\; (x\; \{\backslash \; mathrel\; \{\backslash \; dot\; \{-\}\}\})\; y)\; +\; (y\; \{\backslash \; mathrel\; \{\backslash \; dot\; \{-\}\}\}\; x).\; \backslash \backslash \backslash \; end\; \{align\}\}\}$

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

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

1. ^Skolem, Thoralf (1923), "Begründung der elementaren Arithmetik durch die rekurrierende Denkweise ohne Anwendung scheinbarer Veränderlichen mit UNENDLICHEME" [Основы элементарной арифметики, установленные с помощью рекурсивного мышления без использования видимых переменных в бесконечных областях] (PDF), Skrifter utgit av Videnskapsselskapet i Kristiania. I, Matematisk-naturvidenskabelig klasse (на немецком языке), 6 : 1–38. Перепечатано в переводе в van Heijenoort, Jean (1967), From Frege to Gödel. Справочник по математической логике, 1879–1931, Кембридж, Массачусетс: Harvard University Press, стр. 302–333, MR 0209111.
2. ^Tait, WW (1981), «Finitism», The Journal of Philosophy, 78: 524–546, doi : 10.2307 / 2026089.
3. ^Kreisel, G. (1960), «Порядковая логика и характеристика неформальные концепции доказательства » (PDF), Proceedings of the International Congress of Mathematicians, 1958, New York: Cambridge University Press, pp. 289–299, MR 0124194.
4. ^Curry, Haskell B. (1941), «Формализация рекурсивной арифметики», Американский журнал математики, 63: 263–282, doi : 10.2307 / 2371522, MR 0004207.
5. ^Гудштейн, 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-й международный симпозиум Витгенштейна.