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 ε₀,​ 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$.

Véase también

• Aritmética recursiva elemental
• Lógica de valores finitos
• Heyting aritmética
• aritmética peano
• función recursiva primitiva
• Aritmética de Robinson
• aritmética de segundo orden
• aritmética de Skolem

Referencias

• Curry, Haskell B. (1941). «A formalization of recursive arithmetic». American Journal of Mathematics 63: 263-282. doi:10.2307/2371522. 

• Goodstein, R. L. (1954). «Logic-free formalisations of recursive arithmetic». Mathematica Scandinavica 2: 247-261. 

• van Heijenoort, Jean (1967). From Frege to Gödel. A source book in mathematical logic, 1879–1931. Cambridge, Mass.: Harvard University Press. pp. 302–333. 

• Kreisel, Georg (1960). Proceedings of the International Congress of Mathematicians, 1958. Ordinal logics and the characterization of informal concepts of proof. Cambridge University Press. pp. 289-299. 

• Skolem, Thoralf (1923). «Begründung der elementaren Arithmetik durch die rekurrierende Denkweise ohne Anwendung scheinbarer Veränderlichen mit unendlichem Ausdehnungsbereich» [The foundations of elementary arithmetic established by means of the recursive mode of thought without the use of apparent variables ranging over infinite domains]. Skrifter utgit av Videnskapsselskapet i Kristiania. I, Matematisk-naturvidenskabelig klasse (en alemán) 6: 1-38. 

• Tait, W.W. (1981). «Finitism». The Journal of Philosophy 78: 524-546. doi:10.2307/2026089. 

Lecturas adicionales

• Feferman, Solomon (1993). «What rests on what? The proof-theoretic analysis of mathematics». Philosophy of Mathematics (J. Czermak (ed.)): 1-147. 

• Rose, H. E. (1961). «On the consistency and undecidability of recursive arithmetic». Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 7: 124-135. doi:10.1002/malq.19610070707.