Procediment de decisió

Algorisme o mètode efectiu per poder decidir si una fórmula ben formada d'un sistema de lògica és un teorema d'aquest sistema, això és, 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.