Teorema establecido en 1936 por el lógico americano Alonzo Church, según el cual la lógica de predicados (superior a la de predicados monádicos) no posee un procedimiento de decisión, o un algoritmo que permita demostrar que una fórmula cualquiera sea un teorema de dicha lógica. Esta lógica se considera, por tanto, indecidible (ver cita).