Decidibilidad

En lógica, el término decidible se refiere a la existencia de un método efectivo para determinar si un objeto es miembro de un conjunto de fórmulas.Un sistema lógico o teoría 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.Por otra parte, una teoría decidible semánticamente, es un sistema axiomático donde existe un método lógico y finito para evidenciar que el axioma, proposición, fórmula etc. es un teorema. Ejemplo: La Lógica proposicional es decidible, porque existe para ella un algoritmo; la tabla de verdad tal que para cada fórmula que combina M formulas atómicas, hay un número máximo N = 2M de pasos tal que tras completar estos N pasos el algoritmo siempre decidirá si la fórmula es válida o no. Cada ""paso"" del algoritmo ha sido definido como una línea de la tabla de verdad.La lógica de primer orden es sintácticamente decidible si se limita a predicados con un solo argumento (ver cálculo de predicados monódicos). Si se incluyen predicados con dos o más argumentos, no es decidible.Toda teoría completa recursivamente enumerable es decidible sintácticamente. Por otro lado, toda teoría que incluya aritmética básica es no decidible sintácticamente.