Procediment de decisió

Algorisme o mètode efectiu per a 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.