Las teorías de autoverificación son sistemas aritméticos consistentes de primer orden mucho más débiles que la aritmética de Peano que son capaces de demostrar su propia consistencia . Dan Willard fue el primero en investigar sus propiedades y ha descrito una familia de tales sistemas. Según el teorema de incompletitud de Gödel , estos sistemas no pueden contener la teoría de la aritmética de Peano ni su aritmética de fragmentos débiles de Robinson ; no obstante, pueden contener fuertes teoremas.
En resumen, la clave para la construcción de Willard de su sistema es formalizar lo suficiente de la maquinaria de Gödel para hablar de demostrabilidad internamente sin poder formalizar la diagonalización . La diagonalización depende de poder demostrar que la multiplicación es una función total (y en las versiones anteriores del resultado, la suma también). La suma y la multiplicación no son símbolos funcionales del lenguaje de Willard; en cambio, la resta y la división son, y los predicados de suma y multiplicación se definen en términos de estos. Aquí, uno no puede probar eloración que expresa la totalidad de la multiplicación:
dónde es el predicado de tres lugares que significa . Cuando las operaciones se expresan de esta manera, la demostrabilidad de una oración dada se puede codificar como una oración aritmética que describe la terminación de un cuadro analítico . La demostrabilidad de la coherencia se puede agregar simplemente como un axioma. El sistema resultante puede probarse consistente por medio de un argumento de consistencia relativa con respecto a la aritmética ordinaria.
Además, se puede agregar cualquier frase de la aritmética a la teoría sin dejar de mantener la coherencia de la teoría.
Referencias
- Solovay, Robert M. (9 de octubre de 1989). "Inyección de inconsistencias en modelos de PA" . Anales de lógica pura y aplicada . 44 (1–2): 101-132. doi : 10.1016 / 0168-0072 (89) 90048-1 .
- Willard, Dan E. (junio de 2001). "Sistemas de axiomas de autoverificación, el teorema de la incompletitud y principios de reflexión relacionados" . El diario de la lógica simbólica . 66 (2): 536–596. doi : 10.2307 / 2695030 .
- Willard, Dan E. (marzo de 2002). "Cómo extender los cuadros semánticos y versiones sin cortes del segundo teorema de incompletitud casi a la aritmética Q de Robinson" . El diario de la lógica simbólica . 67 (1): 465–496. doi : 10.2178 / jsl / 1190150055 .