Aritmética recursiva primitiva

Formalización de los números naturales.

La aritmética recursiva primitiva ( PRA ) es una formalización de los números naturales sin cuantificadores . Fue propuesto 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 existe un amplio consenso en que todo razonamiento de PRA es finitista. Muchos también creen que PRA captura todo el finitismo, ^[2] pero otros creen que el finitismo puede extenderse a formas de recursividad más allá de la recursividad primitiva, hasta ε , ^[3] que es el ordinal de la teoría de prueba de la aritmética de Peano . El ordinal teórico de prueba de PRA es ω ^ω , donde ω es el ordinal transfinito más pequeño . PRA a veces se denomina aritmética de Skolem , aunque eso tiene otro significado, véase 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 suma , multiplicación y exponenciación . PRA no puede cuantificar explícitamente el dominio de los números naturales. PRA se considera a menudo como el sistema formal metamatemático básico para la teoría de la prueba , en particular para las pruebas de consistencia como la prueba de consistencia de la aritmética de primer orden de Gentzen .

Lenguaje y axiomas

El lenguaje de PRA consiste en:

• Un número contablemente infinito 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 de PRA son:

• Tautologías del cálculo proposicional ;
• Axiomatización habitual 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 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 recursivas que definen 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 constante 0 y la función sucesora cerrada bajo proyección, composición y recursividad primitiva. Entonces, para una función de lugar ( n +1) f definida por recursividad primitiva sobre una función base de n -lugar g y una función de iteración de ( n +2)-lugar h , existirían las ecuaciones definitorias:

• ${\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 de axioma de inducción para la aritmética de primer orden con la regla de inducción (sin cuantificadores):

• De y , deducir , 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 se pueden definir utilizando estas dos funciones recursivas primitivas y la cuantificación de 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 PRA de tal manera que no tenga ningún conectivo 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) presentó el primer sistema de este tipo. La regla de inducción en el sistema de Curry era inusual. Goodstein (1954) dio 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 a los que se muestran. Las únicas otras reglas de inferencia del sistema de Goodstein son las reglas de sustitución, como sigue:

${\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 sus correspondientes ecuaciones definitorias, como en el sistema de Skolem anterior.

De esta manera se puede descartar por completo el cálculo proposicional. Los operadores lógicos se pueden expresar enteramente aritméticamente; por ejemplo, el valor absoluto de la diferencia de dos números se puede definir mediante recursividad 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 tanto, las ecuaciones x = y y son equivalentes. Por lo tanto, las ecuaciones y expresan la conjunción y disyunción lógica , 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}$

Ver también

• Aritmética recursiva elemental
• Lógica de valores finitos
• Heyting aritmética
• 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". Revista Estadounidense de Matemáticas . 63 (2): 263–282. doi :10.2307/2371522. JSTOR  2371522. SEÑOR  0004207.

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

• van Heijenoort, Jean (1967). De Frege a Gödel. Un libro de consulta sobre lógica matemática, 1879-1931 . Cambridge, Massachusetts: Harvard University Press. págs. 302–333. SEÑOR  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. págs. 289–299. SEÑOR  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". La 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, Salomón (1993). "¿Qué se basa en qué? El análisis de la teoría de la prueba 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.