Comience con un conjunto $S$ que es su axioma como conjunto de teoremas.
Construir un nuevo conjunto de teoremas $U$ como:
- para cada par de teoremas en $S$ como $s_1$ y $s_2$ (o cuantas reglas de inferencia exija tu lógica)
- para cada regla de inferencia $I$ en su lógica
- dejar $T = I(s_1, s_2)$ y añadir $T$ a $U$
entonces $U$ son todos los teoremas que se pueden deducir en $1$ "paso" de $S$ . Añadir $U$ a $S$ y repetir. Esta es una simple búsqueda de la lógica de la amplitud. Este define qué teoremas son demostrables y es completamente constructivo.
Si se utiliza este procedimiento para buscar un teorema que sea demostrable o refutable, obviamente terminará. Si se utiliza para buscar un teorema indecidible (ni demostrable ni refutable), entonces no terminará.
Esto plantea dos preguntas: (1) ¿Existen tales teoremas indecidibles y (2) Si existen, podemos simplemente ejecutar otro y determinar si un teorema es indecidible?
La respuesta a (1) es "más o menos". Si el conjunto de axiomas de una lógica es consistente y no trivial, entonces la "Sentencia de Godel" da un ejemplo de teorema que debe ser indecidible; así que en ese caso la respuesta a (1) es "sí".
La respuesta a (2) es que si tal algoritmo existiera, el propio algoritmo podría usarse como axioma para (de forma bastante artificiosa) asignar "verdadero" y "falso" a teoremas indecidibles y añadir esas asignaciones al axioma manteniendo la consistencia del mismo. Tal algoritmo permitiría construir una lógica completa y consistente, lo que contradiría (1) y la existencia demostrable de la Sentencia de Godel.
