Sistema de aritmética en la teoría de la demostración
En teoría de la prueba , una rama de la lógica matemática , la aritmética de funciones elementales ( AFE ), también llamada aritmética elemental y aritmética de funciones exponenciales , [1] es el sistema de aritmética con las propiedades elementales habituales de 0, 1, +, ×, , junto con la inducción para fórmulas con cuantificadores acotados .
EFA es un sistema lógico muy débil, cuyo ordinal teórico de prueba es , pero aún parece capaz de demostrar gran parte de las matemáticas ordinarias que pueden enunciarse en el lenguaje de la aritmética de primer orden .
Definición
EFA es un sistema de lógica de primer orden (con igualdad). Su lenguaje contiene:
- dos constantes , ,
- tres operaciones binarias , , , que generalmente se escriben como ,
- un símbolo de relación binaria (esto no es realmente necesario ya que se puede escribir en términos de otras operaciones y a veces se omite, pero es conveniente para definir cuantificadores acotados).
Los cuantificadores acotados son aquellos de la forma y que son abreviaturas de y en el sentido habitual.
Los axiomas del EFA son
- Los axiomas de la aritmética de Robinson para , , , ,
- Los axiomas para la exponenciación: , .
- Inducción para fórmulas cuyos cuantificadores están todos 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 el EFA.
El enunciado original de la conjetura de Friedman (1999) es:
- "Todo teorema publicado en los Anales de Matemáticas cuyo enunciado involucra sólo objetos matemáticos finitos (es decir, lo que los lógicos llaman un enunciado aritmético) puede ser demostrado en EFA. EFA es el fragmento débil de la Aritmética de Peano basada en los axiomas libres de cuantificadores habituales para 0, 1, +, ×, exp, junto con el esquema de inducción para todas las fórmulas en el lenguaje cuyos cuantificadores están todos acotados".
Si bien es fácil construir enunciados aritméticos artificiales que sean verdaderos pero no demostrables en el AFE, 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 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 grafo menor .
Sistemas relacionados
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 establezca aproximadamente que la exponenciación es una función definida en todas partes. Esto es similar al EFA y tiene la misma fuerza teórica de prueba, pero es más complicado trabajar con él.
- Existen fragmentos débiles de aritmética de segundo orden llamados y que son conservadores respecto del AFE para oraciones (es decir, cualquier oración probada o ya probada por el AFE). [2] En particular, son conservadores para enunciados consistentes. 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 está restringida a sumas y productos acotados . Esto también tiene las mismas oraciones que EFA, en el sentido de que siempre que EFA prueba ∀x∃y P ( x , y ), con P libre de cuantificadores, ERA prueba 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 completamente libre de lógica [ aclaración necesaria ] , con solo las reglas de sustitución e inducción, y ecuaciones definitorias 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 número finito de funciones base y, por lo tanto, solo se necesita un número finito de ecuaciones definitorias.
Véase también
Referencias
- ^ C. Smoryński, "Modelos no estándar y desarrollos relacionados" (p. 217). De la obra de Harvey Friedman, Research on the Foundations of Mathematics (1985), Studies in Logic and the Foundations of Mathematics, vol. 117.
- ^ SG Simpson, RL Smith, "Factorización de polinomios y Σ 1 0 {\displaystyle \Sigma _{1}^{0}} -inducción" (1986). Anales de lógica pura y aplicada, vol. 31 (p.305)
- 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 (1999), grandes conjeturas
- 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, Sr. 1723993