Indecibilitat

Un sistema formal és indecidible si no disposa d'un algorisme o procediment de decisió per a determinar, en un nombre finit de passos, si un enunciat o fórmula d'aquest sistema és un teorema seu. La lògica d'enunciats és decidible, atès que disposa d'un medi mecànic, les taules de veritat, per a poder determinar, per a qualsevol fórmula donada, si és o no una veritat lògica, una contradicció o una contingència. La lògica de predicats de primer ordre, en canvi, no ho és, segons el teorema de Church (1936).