Las teorías autoverificables son sistemas aritméticos consistentes de primer orden , mucho más débiles que la aritmética de Peano , que son capaces de probar 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 fragmento débil , la aritmética de Robinson ; no obstante, pueden contener teoremas fuertes.
En líneas generales, la clave de la construcción del sistema de Willard es formalizar lo suficiente 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, también la adición). La adición y la multiplicación no son símbolos de función del lenguaje de Willard; en cambio, lo son la resta y la división, y los predicados de adición y multiplicación se definen en términos de estos. Aquí, no se puede demostrar la oración que expresa la totalidad de la multiplicación: donde es el predicado de tres lugares que representa 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 una tabla analítica . La demostrabilidad de la consistencia se puede agregar simplemente como un axioma. El sistema resultante se puede demostrar consistente por medio de un argumento de consistencia relativa con respecto a la aritmética ordinaria.
Se puede añadir además cualquier oración aritmética verdadera a la teoría manteniendo al mismo tiempo la consistencia de la teoría.
