Las teorías autoverificables son sistemas consistentes de aritmética 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 describió 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 de la aritmética de Robinson ; no obstante, pueden contener teoremas sólidos.
En resumen, la clave para la construcción de su sistema por parte 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 suma). La suma y la multiplicación no son símbolos funcionales del lenguaje de Willard; en cambio, la resta y la división lo son, y los predicados de suma y multiplicación se definen en términos de estos. Aquí no se puede probar la oración que expresa la totalidad de la multiplicación:
Además, se puede agregar cualquier oración aritmética verdadera a la teoría manteniendo la coherencia de la teoría.
