Decidibilidad

En metalógica, la decidibilidad es una propiedad de los sistemas formales cuando, para cualquier fórmula en el lenguaje del sistema, existe un método efectivo para determinar si esa fórmula pertenece o no al conjunto de las verdades del sistema. Por ejemplo, la lógica proposicional es decidible, porque existe un algoritmo (la tabla de verdad) que en un número finito de pasos puede decidir si la fórmula es válida o no.

Cuando una fórmula no puede ser probada verdadera ni falsa, se dice que la fórmula es independiente, y que por lo tanto el sistema es no decidible. La única manera de incorporar una fórmula independiente a las verdades del sistema es postulándola como axioma. Dos ejemplos muy importantes de fórmulas independientes son el axioma de elección en la teoría de conjuntos, y el quinto postulado de la geometría euclidiana.

Un sistema formal es decidible sintácticamente si el conjunto de todas las fórmulas válidas en el sistema es decidible. Es decir, existe un algoritmo tal que para cada fórmula del sistema es capaz de decidir en un número finito de pasos si la fórmula es válida o no en el sistema.

La lógica de primer orden es sintácticamente decidible si se limita a predicados con un solo argumento (monádica). Si se incluyen predicados con dos o más argumentos, no es decidible.

Toda teoría completa y recursivamente enumerable es decidible sintácticamente. Por otro lado, toda teoría que incluya aritmética básica no es decidible sintácticamente.

Un sistema formal es decidible semánticamente si existe un método lógico y finito para evidenciar que el axioma, proposición, fórmula etc. es un teorema.