En la teoría de la prueba , 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 , es el sistema de aritmética con las propiedades elementales habituales de 0, 1, +, ×, x y , junto con inducción para fórmulas con cuantificadores acotados .
EFA es un sistema lógico muy débil, cuyo ordinal teórico de la demostración es ω 3 , pero todavía parece capaz de probar gran parte de las matemáticas ordinarias que se pueden enunciar en el lenguaje de la aritmética de primer orden .
Los cuantificadores acotados son aquellos de la forma ∀ (x <y) y ∃ (x <y) que son abreviaturas de ∀ x (x <y) → ... y ∃x (x <y) ∧ ... en la forma habitual camino.
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.
Si bien es fácil construir enunciados aritméticos artificiales que sean verdaderos pero no probables en EFA [se necesita un ejemplo ] , el punto de la conjetura de Friedman es que los ejemplos naturales de tales enunciados en matemáticas parecen ser raros. Algunos ejemplos naturales incluyen declaraciones de coherencia de la lógica, varias declaraciones relacionadas con la teoría de Ramsey , como el lema de regularidad de Szemerédi y el teorema de grafos menores .