La indecidibilidad de la lógica de primer orden y el método de árboles

Abstract

El teorema de Church demuestra que la cuestión de la validez o no de fórmulas de primer orden no es resoluble por máquinas de Turing ni procedimientos equivalentes, lo que a partir de la tesis de Church-Turing significa la inexistencia de métodos efectivos de decisión para determinar si una fórmula de primer orden es válida o no. El método deductivo de árboles para la lógica proposicional sí que es un método de decisión para esta lógica, porque el árbol siempre se termina tanto si se cierran todas las ramas del árbol como si no. Por el contrario, en lógica de primer orden el método de árboles no es un método efectivo, puesto que en algunos casos no se acaban nunca. A tenor de lo dicho más arriba, tampoco podría nunca serlo, aun cuando intentásemos complementarlo de alguna manera. A partir de ahí intentaremos desmenuzar las razones que hacen que los árboles de primer orden no sean ni puedan ser un método de decisión y las implicaciones que eso tiene.