Algorismeo mètode efectiu per poder decidir si una fórmula ben formada
d’un sistema de lògica és un teorema
d'aquest sistema, és a dir, si pot ser objecte de deducció en una sèrie finita de passos sotmesos a regles. La
lògica
d’enunciats disposa de tals procediments(les
taules de veritat;) però no la
lògica de predicats de primer ordre, o la lògica elemental en general, segons determina el teorema de Church.
