4.7.1. Compleción y decidibilidad

• es completo porque si ₀C existen algoritmos que demuestran C, y
• es decidible porque existen algoritmos que responden «sí» en el caso de que ₀C y «no» en el caso de que ₀ /C

Kurt Gödel demostró en 1930 el teorema de compleción para la lógica de predicados de primer orden (otra cosa es su teorema de incompleción para los sistemas axiomáticos de la aritmética). El teorema establece que si un conjunto de sentencias ₀ = {₁,₂,..._n} implica lógicamente una sentencia C (₀C) entonces existe una demostración de C, es decir (Apartado 4.6.3), una secuencia finita, R, de aplicación de reglas de inferencia que conduce de ₀ a C ({₁,₂,..._n}_RC).

Sin embargo, Alonzo Church demostró en 1936 que si no es el caso que ₀C entonces no existe un procedimiento finito que permita demostrarlo (es decir, demostrar que C no está implicada por ₀). Por esto se dice que la lógica de predicados de primer orden, en su forma general, es semidecidible (aunque hay formas particulares que sí son decidibles, por ejemplo, aquella en la que los predicados sólo tienen uno o dos argumentos).

 DIT-ETSIT-UPM