aritmética de funciones elementales

En la teoría de la demostración , una rama de la lógica matemática , la aritmética de funciones elementales ( EFA ), también llamada aritmética elemental y aritmética de funciones exponenciales , ^{[ 1 ]} es el sistema de aritmética con las propiedades elementales usuales de 0,  1,  +,  ×, ${\displaystyle x^{y}}$, junto con la inducción para fórmulas con cuantificadores acotados .

EFA es un sistema lógico muy débil, cuyo ordinal de teoría de la demostración es${\displaystyle \omega ^{3}}$pero aún parece capaz de demostrar gran parte de las matemáticas ordinarias que pueden expresarse en el lenguaje de la aritmética de primer orden .

EFA es un sistema de lógica de primer orden (con igualdad). Su lenguaje contiene:

• dos constantes${\displaystyle 0}$,${\displaystyle 1}$,
• tres operaciones binarias${\displaystyle +}$,${\displaystyle \times }$,${\displaystyle {\textrm {exp}}}$, con${\displaystyle {\textrm {exp}}(x,y)}$generalmente se escribe como${\displaystyle x^{y}}$,
• un símbolo de relación binaria${\displaystyle <}$(Esto no es realmente necesario, ya que puede escribirse en términos de las otras operaciones y a veces se omite, pero es conveniente para definir cuantificadores acotados).

Los cuantificadores acotados son aquellos de la forma${\displaystyle \forall (x<y)}$y${\displaystyle \exists (x<y)}$que son abreviaturas de${\displaystyle \forall x(x<y)\rightarrow \ldots }$y${\displaystyle \exists x(x<y)\land \ldots }$De la forma habitual.

Los axiomas del EFA son

• Los axiomas de la aritmética de Robinson para${\displaystyle 0}$,${\displaystyle 1}$,${\displaystyle +}$,${\displaystyle \times }$,${\displaystyle <}$
• Los axiomas para la exponenciación:${\displaystyle x^{0}=1}$,${\displaystyle x^{y+1}=x^{y}\times x}$.
• Inducción para fórmulas cuyos cuantificadores están todos acotados (pero que pueden contener variables libres ).

La gran conjetura de Harvey Friedman implica que muchos teoremas matemáticos, como el Último Teorema de Fermat , pueden demostrarse en sistemas muy débiles como EFA.

La formulación original de la conjetura de Friedman (1999) es:

Todo teorema publicado en los Anales de Matemáticas cuya formulación involucre únicamente objetos matemáticos finitos (es decir, lo que los lógicos denominan una formulación aritmética) puede demostrarse en EFA. EFA es el fragmento débil de la aritmética de Peano, basado en los axiomas usuales sin cuantificadores para 0,  1,  +,  ×,  exp, junto con el esquema de inducción para todas las fórmulas del lenguaje cuyos cuantificadores están acotados.

Si bien es fácil construir enunciados aritméticos artificiales que son verdaderos pero no demostrables en EFA, la conjetura de Friedman apunta a que los ejemplos naturales de tales enunciados en matemáticas parecen ser escasos. Algunos ejemplos naturales incluyen enunciados de consistencia de la lógica, varios enunciados relacionados con la teoría de Ramsey, como el lema de regularidad de Szemerédi , y el teorema del menor de grafos .

Varias clases de complejidad computacional relacionadas tienen propiedades similares a EFA:

• Se puede omitir el símbolo de función binaria exp del lenguaje, tomando la aritmética de Robinson junto con la inducción para todas las fórmulas con cuantificadores acotados y un axioma que establece, a grandes rasgos, que la exponenciación es una función definida en todas partes. Esto es similar a EFA y tiene la misma solidez teórica de la demostración, pero es más engorroso de manejar.
• Existen fragmentos débiles de aritmética de segundo orden llamados${\displaystyle {\mathsf {RCA}}_{0}^{*}}$y${\displaystyle {\mathsf {WKL}}_{0}^{*}}$que son conservadores sobre la EFA para${\displaystyle \Pi _{2}^{0}}$oraciones (es decir, cualquier${\displaystyle \Pi _{2}^{0}}$sentencias probadas por${\displaystyle {\mathsf {RCA}}_{0}^{*}}$o${\displaystyle {\mathsf {WKL}}_{0}^{*}}$ya han sido probados por EFA.) ^{[ 2 ]} En particular, son conservadores para las declaraciones de consistencia. Estos fragmentos a veces se estudian en matemáticas inversas ( Simpson 2009 ) .
• La aritmética recursiva elemental ( ERA ) es un subsistema de la aritmética recursiva primitiva (PRA) en el que la recursión se restringe a sumas y productos acotados . Esto también tiene la misma${\displaystyle \Pi _{2}^{0}}$Las oraciones como EFA, en el sentido de que siempre que EFA prueba ∀x∃y P ( x , y ), con P sin cuantificadores, ERA prueba la fórmula abierta P ( x , T ( x )), con T un término definible en ERA. Al igual que PRA, ERA puede definirse de una manera completamente libre de lógica, con solo las reglas de sustitución e inducción, y definiendo ecuaciones para todas las funciones recursivas elementales. Sin embargo, a diferencia de PRA, las funciones recursivas elementales pueden caracterizarse por el cierre bajo composición y proyección de un número finito de funciones base, y por lo tanto solo se necesita un número finito de ecuaciones definitorias.

• Función elemental – Tipo de función matemática 
• Jerarquía de Grzegorczyk : funciones en la teoría de la computabilidad. 
• Matemáticas inversas : rama de la lógica matemática. 
• Análisis ordinal : técnica matemática utilizada en la teoría de la demostración. 
• Problema de álgebra de la escuela secundaria de Tarski - Problema matemático 

• Avigad, Jeremy (2003), "Teoría de números y aritmética elemental", Philosophia Mathematica , Serie III, 11 (3): 257– 284, doi : 10.1093/philmat/11.3.257 , ISSN 0031-8019 , MR 2006194  
• Friedman, Harvey (16 de abril de 1999), "Grandes conjeturas" , lista de correo FOM , archivado del original el 29 de noviembre de 2019.
• Simpson, Stephen G. (2009), Subsistemas de aritmética de segundo orden , Perspectivas en lógica (2.ª  ed.), Cambridge University Press , ISBN 978-0-521-88439-6, MR 1723993