Gentzen argumentó que su demostración evitaba los modos cuestionables de inferencia contenidos en la aritmética de Peano y que, por lo tanto, su consistencia es menos controvertida.
Esta es una teoría de "primer orden": los cuantificadores se extiende sobre números naturales, pero no sobre conjuntos o funciones de números naturales.
La teoría es lo suficientemente fuerte como para describir funciones de enteros definidas recursivamente como la exponenciación, los factoriales o los números de Fibonacci.
Esta creciente simplicidad se formaliza adjuntando un < ordinal ε0 a cada demostración, y mostrando que, a medida que uno se mueve hacia abajo en el árbol, estos ordinales se hacen más pequeños a cada paso.
Por ejemplo, no demuestra la inducción matemática ordinaria para todas las fórmulas, mientras que PA sí lo hace (ya que todas las instancias de inducción son axiomas de PA).
Y, suponiendo que T no es extremadamente débil, T mismo será capaz de demostrar esto condicionalmente: Si B es consistente, entonces también lo es T. Por lo tanto, T no puede probar que B es consistente, por el segundo teorema de incompletitud, mientras que B bien puede ser capaz de probar que T es consistente.
Así que Q+Con(T) es siempre más lógicamente fuerte que T. Pero la teoría de Gentzen interpreta trivialmente Q+Con(PA), ya que contiene Q y demuestra Con(PA), y así la teoría de Gentzen interpreta PA.
Es decir: si PA interpretara la teoría de Gentzen, entonces también interpretaría Q+Con(PA) y por lo tanto sería inconsistente, según el resultado de Pudlák.
[4] Es probable que todos los matemáticos hubieran aceptado finalmente el enfoque de Hilbert si hubiera sido capaz de llevarlo a cabo con éxito.
Pero luego Gödel le asestó un golpe terrible (1931), del que aún no se ha recuperado.
Pudo demostrar que esta proposición no puede ser probada ni refutada dentro del formalismo.
Esto puede significar sólo dos cosas: o bien el razonamiento por el cual se da una demostración de consistencia debe contener algún argumento que no tenga contrapartida formal dentro del sistema, es decir, no hemos logrado formalizar completamente el procedimiento de inducción matemática; o la esperanza de una demostración estrictamente "finitista" de consistencia debe ser abandonada por completo.
Kleene (2009, p. 479) hizo el siguiente comentario en 1952 sobre la importancia del resultado de Gentzen, particularmente en el contexto del programa formalista iniciado por Hilbert.
Las propuestas originales de los formalistas para asegurar las matemáticas clásicas mediante una demostración de consistencia no contemplaban que un método como la inducción transfinita hasta ε0 tendría que ser utilizado.
Gentzen publicó dos demostraciones de consistencia adicionales, una en 1938 y otra en 1943.
Todos estos están contenidos en (Gentzen y Szabo, 1969).
Laurence Kirby y Jeff Paris demostró en 1982 que el teorema de Goodstein no puede ser probado en la aritmética de Peano.