De Wikipedia, la enciclopedia libre
Ir a navegaciónSaltar a buscar

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 .

Definición

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

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

Los cuantificadores acotados son los de la forma ∀ (x <y) y ∃ (x <y) que son abreviaturas de ∀ x (x <y) → ... y ∃x (x <y) ∧ ... en la forma habitual manera.

Los axiomas de EFA son

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

La gran conjetura de Friedman

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.

El enunciado original de la conjetura de Friedman (1999) es:

"Cada teorema publicado en Annals of Mathematics cuyo enunciado involucra solo objetos matemáticos finitarios (es decir, lo que los lógicos llaman un enunciado aritmético) se puede probar en EFA. EFA es el fragmento débil de Peano Arithmetic basado en los axiomas habituales sin cuantificadores para 0 , 1, +, ×, exp, junto con el esquema de inducción para todas las fórmulas en el lenguaje cuyos cuantificadores están acotados ".

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 .

Sistemas relacionados

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

  • Se puede omitir el símbolo de la 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 indique aproximadamente que la exponenciación es una función definida en todas partes. Esto es similar a EFA y tiene la misma fuerza teórica de prueba, pero es más complicado trabajar con él.
  • Hay fragmentos débiles de aritmética de segundo orden llamados RCA*
    0     y WKL*
    0     que tienen la misma fuerza de consistencia que EFA y son conservadores al respecto durante Π0
    2    oraciones [ se necesitan más explicaciones ] , que a veces se estudian en matemáticas inversas ( Simpson 2009 ).
  • La aritmética recursiva elemental ( ERA ) es un subsistema de aritmética recursiva primitiva (PRA) en el que la recursividad está restringida a sumas y productos acotados . Esto también tiene lo mismo Π0
    2    oraciones como EFA, en el sentido de que siempre que EFA demuestra ∀x∃y P ( x , y ), con P libre de cuantificador, ERA demuestra la fórmula abierta P ( x , T ( x )), con T un término definible en ERA . Al igual que PRA, ERA se puede definir de una manera totalmente libre de lógica [se necesita aclaración ] , 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 se pueden caracterizar por el cierre bajo composición y proyección de un finito número de funciones básicas y, por lo tanto, sólo se necesita un número finito de ecuaciones definitorias.

Ver también

Referencias