# Aritmética recursiva primitiva

La aritmética recursiva primitiva (PRA por sus siglas en inglés) es una formalización libre de cuantificadores de los números naturales. Fue introducida por el matemático noruego Skolem (1923), como una formalización de su concepción finitista de los fundamentos de la aritmética. Es ampliamente aceptado que todo razonamiento de PRA es finitista. Para muchos, el PRA captura todo el finitismo, pero otros creen que el finitismo puede extenderse a formas de recursión más allá de la recursividad primitiva, hasta ε$_0$, que es el poder de demostración de la aritmética de Peano. El poder de demostración de PRA es ω$^ω$, donde ω es el primer ordinal transfinito. No ha de confundirse con la aritmética de Skolem, aunque a veces se la llama así.
El lenguaje de PRA puede expresar proposiciones aritméticas que involucren números naturales y cualquier función recursiva primitiva, incluidas las operaciones de suma, multiplicación y exponenciación. PRA no permite cuantificar explícitamente sobre el dominio de los números naturales. A menudo se toma como sistema formal metamatemático básico en teoría de la demostración, sobre todo en demostraciones de consistencia como la demostración de Gentzen sobre la consistencia de la aritmética de primer orden.

## Lenguaje y axiomas

El lenguaje de PRA consiste en:
* Una cantidad infinita numerable de variables x, y, z ,. . . .
* Los conectores proposicionales ;
* El símbolo de igualdad '=', el símbolo constante 0 y el símbolo sucesor S (que significa sumar uno);
* Un símbolo para cada función recursiva primitiva .
Los axiomas lógicos de PRA son los siguientes:
* Las tautologías del cálculo proposicional
* La axiomatización habitual de la igualdad como relación de equivalencia.
Las reglas lógicas de PRA son el modus ponens y la sustitución de variables. El resto de axiomas de la teoría son:
* $S(x)\neq 0$ ;
* $S(x)=S(y)~\to ~x=y,$
junto con, para cada función recursiva primitiva, una ecuación que la define recursivamente. Por ejemplo, la caracterización más común de las funciones recursivas primitivas consiste en la clase que se obtiene al cerrar bajo la proyección, la sustitución y la recursión primitiva el conjunto de las funciones constante 0 y sucesor. Entonces, para una función f (n+1)-aria definida por recursividad primitiva a partir de una función base g n-aria y una función de iteración de (n+2)-aria h, se tendrían las ecuaciones definitorias:
* $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})$
Como caso especial:
* $x+0=x\$
* $x+S(y)=S(x+y)\$
* $x\cdot 0=0\$
* $x\cdot S(y)=x\cdot y+x\$
* ... etcétera.
PRA reemplaza el esquema de axiomas de inducción que existe en la aritmética de primer orden con la siguiente regla de inducción (sin cuantificador):
* De $\varphi (0)$ y $\varphi (x)\to \varphi (S(x))$, deducir $\varphi (y)$, para cualquier predicado $\varphi .$
En aritmética de primer orden, las únicas funciones recursivas primitivas que hace falta axiomatizar explícitamente son la suma y la multiplicación. Todos los demás predicados recursivos primitivos se pueden definir a partir de estas dos funciones y de la cuantificación sobre 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 conector lógico: una oración de PRA sería solo 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) dio el primer sistema de este tipo. La regla de inducción en el sistema de Curry era inusual;Goodstein (1954) la refinó. La regla de inducción en el sistema de Goodstein es:
    ${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 sucesor y F, G y H son funciones recursivas primitivas que pueden tener parámetros adicionales a los que se muestran. Las únicas otras reglas de inferencia del sistema de Goodstein son las reglas de sustitución, como sigue:
    ${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 cada función recursiva primitiva con ecuaciones definitorias correspondientes, como en el sistema anterior de Skolem.
De esta manera, el cálculo proposicional puede descartarse por completo. Los operadores lógicos se pueden expresar aritméticamente: por ejemplo, el valor absoluto de la diferencia de dos números se puede definir mediante recursividad primitiva:
    ${\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}}$
Así, las ecuaciones x = y y $|x-y|=0$ son equivalentes. Por lo tanto las ecuaciones $|x-y|+|u-v|=0$ y $|x-y|\cdot |u-v|=0$ expresan la conjunción y la disyunción lógicas, respectivamente, de las ecuaciones x = y y u = v. La negación se puede expresar como $1{\dot {-}}|x-y|=0$.