Resumen
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.
Palabras clave: máquinas de Turing, halting problem, método de decisión, método deductivo de árboles.

The undecidability of first-order logic and the method of analytic tableaux
Summary
Church's theorem proves that the question of validity or not of first-order formulas cannot be resolved by Turing machines or equivalent procedures; Which, on the basis of Church-Turing thesis, means the inexistence of effective decision methods in order to determine whether a first-order formula is valid or not.
The method of analytic tableaux for propositional logic is indeed a decision method for this logic, due to the tableaux always being terminated whether all tableaux branches are closed or not. On the contrary, in first-order logic tableaux method is not an effective one, since in some cases they never close. Taking into consideration the aforementioned, it could never be effective, even if we try to supplement it in some way. Henceforth, we will try to analyse the reasons why first-order tableaux are not and cannot be a decision method and the implications that this entails.
Key words: Turing machines, halting problem, decision problem, method of tableaux.