La utilidad de pruebas supone implícitamente que el sistema formal es consistente (con excepción de aquellos extraños paraconsistent lógicas). La prueba por contradicción, y, más generalmente, de la resolución de las pruebas, son explícitamente la lógica proposicional, lo cual es consistente y completa. Incompletitud es introducido por medio de reglas de inferencia para la manipulación de los cuantificadores lo suficientemente potente como para representar a la aritmética, que está más allá de la mera prueba por contradicción.
Los teoremas de incompletitud nos dice que los sistemas formales que son lo suficientemente potente como para representar Robinson aritmética (o de sus más fuertes, más ortodoxo, primo de la aritmética de Peano) han indecidible declaraciones, pero proposicional cálculo no es muy poderoso y es totalmente decidable. Incluso la aritmética de Presburger y extensiones que involucran multiplicaciones por constantes son SMT decidable, y seguramente son completos. Así que, en resumen, la resolución de las pruebas en sí mismo no son impedidas por la incompletitud.
La incompletitud significa que su posible hay algunos nuevos Russel de la paradoja de ahí que las fuerzas de todos para reconstruir los fundamentos de los sistemas lo suficientemente fuerte como para representar Robinson aritmética. Las consecuencias de tal oculto inconsistencia es catastrófico, porque entonces todas las declaraciones que se puede probar (por contradicción, como se demostró) y el sistema se vuelve inútil, Pero no necesariamente irreparables, como hicimos recuperarse de Russel paradoja. Sin embargo, podemos tomar consuelo de que para muchos útil más débil de los sistemas, son perfectamente estables, decidable, toda la planta.
