He leído en algunos libros que el cálculo proposicional es decidible (por ejemplo, con tablas de verdad), y que el cálculo de predicados no es decidible (como demostraron Church y Turing). Por desgracia, no entiendo exactamente el alcance de esta última afirmación. Permítanme explicar lo que sé sobre el cálculo de predicados (por favor, corríjanme si me equivoco):
En su forma mínima, el cálculo de predicados es el cálculo de predicados puro con igualdad: su lenguaje tiene un conjunto completo de conectivas lógicas, un suministro ilimitado de variables individuales, cuantificadores $\forall,\exists$ y un símbolo de predicado binario especial $=$ por la igualdad. También tiene los axiomas lógicos habituales y las reglas de inferencia, incluidos los axiomas de igualdad.
En una forma más rica, el cálculo de predicados puede tener además un conjunto finito de constantes individuales, un conjunto finito de símbolos funcionales n-arios, un conjunto finito de símbolos de predicado n-arios, y axiomas adicionales para manipular esos símbolos (suponemos que los axiomas se generan efectivamente, y "ser un axioma" es una propiedad decidible de una fórmula).
¿El resultado de indecidibilidad se aplica a la forma mínima (el cálculo de predicados puro con igualdad), o es un resultado más débil que dice que no existe ningún procedimiento de decisión que pueda manejar todas las formas generales del cálculo de predicados?
Gracias.
