¿Qué es?
No se ha añadido ninguna twiki todavía.
Propiedad de los sistemas formales que disponen de un procedimiento de decisión efectivo, o un algoritmo, que permite determinar si toda expresión bien formada del sistema es o no es deducible dentro del sistema. A los sistemas formales que gozan de esta propiedad para todas sus fórmulas o expresiones se les llama decidibles. Una expresión bien formada es deducible si es un teorema del sistema. A su vez, una fómulaes decidible dentro de un sistema si ella o su negación son teoremas del sistema.
Según el teorema de Church, la lógica de predicados de primer orden no dispone de tal procedimiento de decisión. Lo posee, en cambio, la lógica de enunciados: las tablas de verdad (y las expresiones monádicas de la lógica de predicados, reducibles a expresiones de lógica de enunciados)