Aritmética recursiva primitiva

Formalización de los números naturales

La aritmética recursiva primitiva ( PRA ) es una formalización sin cuantificadores de los números naturales . Fue propuesta por primera vez por el matemático noruego Skolem (1923), ^[1] como una formalización de su concepción finitista de los fundamentos de la aritmética , y se acepta ampliamente que todo el razonamiento de PRA es finitista. Muchos también creen que todo el finitismo está capturado por PRA, ^[2] pero otros creen que el finitismo puede extenderse a formas de recursión más allá de la recursión primitiva, hasta ε 0 , ^[3] que es el ordinal de prueba teórica de la aritmética de Peano . El ordinal de prueba teórica de PRA es ω ^ω , donde ω es el ordinal transfinito más pequeño . PRA a veces se llama aritmética de Skolem , aunque eso tiene otro significado, consulte aritmética de Skolem .

El lenguaje de PRA puede expresar proposiciones aritméticas que involucran números naturales y cualquier función recursiva primitiva , incluidas las operaciones de adición , multiplicación y exponenciación . PRA no puede cuantificar explícitamente sobre el dominio de los números naturales. PRA se toma a menudo como el sistema formal metamatemático básico para la teoría de pruebas , en particular para pruebas de consistencia como la prueba de consistencia de Gentzen de la aritmética de primer orden .

Lenguaje y axiomas

El lenguaje del PRA consta de:

• Un número infinito contable de variables x , y , z ,....
• Los conectivos proposicionales ;
• El símbolo de igualdad = , el símbolo constante 0 y el símbolo sucesor S (que significa agregar uno );
• Un símbolo para cada función recursiva primitiva .

Los axiomas lógicos del PRA son:

• Tautologías del cálculo proposicional ;
• Axiomatización usual de la igualdad como relación de equivalencia .

Las reglas lógicas del PRA son el modus ponens y la sustitución de variables .
Los axiomas no lógicos son, en primer lugar:

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

donde siempre denota la negación de modo que, por ejemplo, es una proposición negada. ${\displaystyle x\neq y}$ ${\displaystyle x=y}$ ${\displaystyle S(0)=0}$

Además, las ecuaciones de definición recursivas para cada función recursiva primitiva pueden adoptarse como axiomas según se desee. Por ejemplo, la caracterización más común de las funciones recursivas primitivas es como la función constante 0 y sucesora cerrada bajo proyección, composición y recursión primitiva. Por lo tanto, para una función f de ( n + 1) lugares definida por recursión primitiva sobre una función base g de n lugares y una función de iteración h de ( n + 2) lugares, habría las ecuaciones de definición:

• ${\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})}$

Especialmente:

• ${\displaystyle x+0=x\ }$
• ${\displaystyle x+S(y)=S(x+y)\ }$
• ${\displaystyle x\cdot 0=0\ }$
• ${\displaystyle x\cdot S(y)=x\cdot y+x\ }$
• ... etcétera.

PRA reemplaza el esquema axiomático de inducción para la aritmética de primer orden con la regla de inducción (sin cuantificadores):

• De y , deduzca , para cualquier predicado ${\displaystyle \varphi (0)}$ ${\displaystyle \varphi (x)\to \varphi (S(x))}$ ${\displaystyle \varphi (y)}$ ${\displaystyle \varphi .}$

En aritmética de primer orden , las únicas funciones recursivas primitivas que necesitan ser axiomatizadas explícitamente son la suma y la multiplicación . Todos los demás predicados recursivos primitivos pueden definirse utilizando estas dos funciones recursivas primitivas y la cuantificación sobre todos los números naturales . Definir funciones recursivas primitivas de esta manera no es posible en PRA, porque carece de cuantificadores.

Cálculo sin lógica

Es posible formalizar un PRA de tal manera que no tenga ningún conector lógico: una oración de PRA es simplemente una ecuación entre dos términos. En este contexto, un término es una función recursiva primitiva de cero o más variables. Curry (1941) proporcionó el primer sistema de este tipo. La regla de inducción en el sistema de Curry era inusual. Goodstein (1954) proporcionó un refinamiento posterior. La regla de inducción en el sistema de Goodstein es:

${\displaystyle {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)}.}$

Aquí x es una variable, S es la operación sucesora y F , G y H son funciones recursivas primitivas que pueden tener parámetros distintos de los que se muestran. Las únicas otras reglas de inferencia del sistema de Goodstein son las reglas de sustitución, como se indica a continuación:

${\displaystyle {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}.}$

Aquí A , B y C son términos cualesquiera (funciones recursivas primitivas de cero o más variables). Finalmente, hay símbolos para cualquier función recursiva primitiva con ecuaciones de definición correspondientes, como en el sistema de Skolem anterior.

De esta manera, el cálculo proposicional puede descartarse por completo. Los operadores lógicos pueden expresarse completamente de forma aritmética; por ejemplo, el valor absoluto de la diferencia de dos números puede definirse mediante recursión primitiva:

${\displaystyle {\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}}}$

Por lo tanto, las ecuaciones x = y y son equivalentes. Por lo tanto, las ecuaciones y expresan la conjunción y disyunción lógicas , respectivamente, de las ecuaciones x = y y u = v . La negación se puede expresar como . ${\displaystyle |x-y|=0}$ ${\displaystyle |x-y|+|u-v|=0}$ ${\displaystyle |x-y|\cdot |u-v|=0}$ ${\displaystyle 1{\dot {-}}|x-y|=0}$

Véase también

• Aritmética recursiva elemental
• Lógica de valores finitos
• Aritmética de Heyting
• Aritmética de Peano
• Función recursiva primitiva
• Aritmética de Robinson
• Aritmética de segundo orden
• Aritmética de Skolem

Notas

1. reimpreso traducido en van Heijenoort (1967)
2. Tait 1981.
3. Kreisel 1960.

Referencias

• Curry, Haskell B. (1941). "Una formalización de la aritmética recursiva". American Journal of Mathematics . 63 (2): 263–282. doi :10.2307/2371522. JSTOR  2371522. MR  0004207.

• Goodstein, RL (1954). "Formalizaciones libres de lógica de aritmética recursiva". Mathematica Scandinavica . 2 : 247–261. doi : 10.7146/math.scand.a-10412 . MR  0087614.

• van Heijenoort, Jean (1967). De Frege a Gödel. Un libro de consulta sobre lógica matemática, 1879-1931 . Cambridge, Mass.: Harvard University Press. pp. 302-333. MR  0209111.

• Kreisel, Georg (1960). "Lógica ordinal y caracterización de conceptos informales de prueba" (PDF) . Actas del Congreso Internacional de Matemáticos, 1958. Nueva York: Cambridge University Press. pp. 289–299. MR  0124194.

• Skolem, Thoralf (1923). "Begründung der elementaren Arithmetik durch die rekurrierende Denkweise ohne Anwendung scheinbarer Veränderlichen mit unendlichem Ausdehnungsbereich" [Los fundamentos de la aritmética elemental establecidos mediante el modo de pensamiento recursivo sin el uso de variables aparentes que abarcan dominios infinitos] (PDF) . Skrifter Utgit av Videnskapsselskapet I Kristiania. Yo, Matematisk-naturvidenskabelig Klasse (en alemán). 6 : 1–38.

• Tait, William W. (1981). "Finitismo". Revista de Filosofía . 78 (9): 524–546. doi :10.2307/2026089. JSTOR  2026089.

• Tait, William W. (junio de 2012). "Aritmética recursiva primitiva y su papel en los fundamentos de la aritmética: reflexiones históricas y filosóficas" (PDF) . Epistemología versus ontología . págs. 161–180. doi :10.1007/978-94-007-4435-6_8.

Lectura adicional

• Feferman, Solomon (1993). "¿Qué se apoya en qué? El análisis teórico de la demostración de las matemáticas" (PDF) . Filosofía de las matemáticas . J. Czermak (ed.): 1–147.

• Rosa, ÉL (1961). "Sobre la coherencia y la indecidibilidad de la aritmética recursiva". Zeitschrift für Mathematische Logik und Grundlagen der Mathematik . 7 (7–10): 124–135. doi :10.1002/malq.19610070707. SEÑOR  0140413.