An effective algorithm or method that determines whether some element $S$ is a member of a set $S$. Frequently, this amounts to determining whether some natural number is a member of some set of natural numbers, e.g., the set of Gödel numbers encoding true sentences of arithmetic. In the case of formal logic, decision procedures are often invoked when asking whether there is a decision procedure for determining whether a formula $\phi$ is a logical consequence of a theory $T$, i.e., asking whether $T$ is decidable.