Una pequeña demostración basada en el Segundo Teorema de Gödel
Vamos a demostrar que el problema de determinar si un enunciado P es decidible con respecto a una teoría T no es resoluble algorítmicamente.
Hagamos la demostración por el absurdo. Supongamos que sí hubiera un algoritmo A que resuelve ese problema y lleguemos a una contradicción.
Sea T una teoría "que contiene suficiente aritmética" y CON un enunciado que expresa (en cierto nivel de lectura) que T es consistente. Recordemos que el Segundo Teorema de Gödel dice que si T es consistente entonces CON es indecicible con respecto a T.
Apliquemos el algoritmo A para determinar si CON es decidible con respecto a T. Si la respuesta de A es que CON es decidible, entonces T es inconsistente (por el Segundo Teorema). Si la respuesta de A es que CON es indecidible entonces T es consistente (porque sólo las teorías consistentes admiten enunciados indecidibles).
Por lo tanto, si A existiera tendríamos un algoritmo que permite determinar si una teoría es consistente, o no. Pero una consecuencia del Segundo Teorema de Gödel es que tal algoritmo no puede existir. Llegamos a un absurdo. Por lo tanto A no existe.
