¿Qué es?
No se ha añadido ninguna twiki todavía.
(El llamado Entscheidungsproblem) El de si se dispone o no, para un enunciado o fórmula cualquiera de un sistema formal, de un procedimiento de decisión efectivo, o de un algoritmo, para determinar si la fórmula o el enunciado en cuestión constituyen una verdad universalmente válida (o un teorema) del sistema. Hay procedimiento de decisión para la lógica de enunciados y la lógica de predicados (monádicos) pero, no lo hay, según el teorema de Church, de 1936, para la lógica de predicados de primer orden.