In logic, a true/false decision problem is decidable if there exists an effective method for deriving the correct answer.
A theory (set of sentences closed under logical consequence) in a fixed logical system is decidable if there is an effective method for determining whether arbitrary formulas are included in the theory.
Many important problems are undecidable, that is, it has been proven that no effective method for determining membership (returning a correct answer after finite, though possibly very long, time in all cases) can exist for them.
The logically valid formulas of a system are sometimes called the theorems of the system, especially in the context of first-order logic where Gödel's completeness theorem establishes the equivalence of semantic and syntactic consequence.
In other settings, such as linear logic, the syntactic consequence (provability) relation may be used to define the theorems of a system.
In such cases, alternative definitions of decidability of a logical system are often used, which ask for an effective method for determining something more general than just validity of formulas; for instance, validity of sequents, or the consequence relation {(Г, A) | Г ⊧ A} of the logic.
This is different from decidability because in a semidecidable system there may be no effective procedure for checking that a formula is not a theorem.
For example, the theory of algebraically closed fields is decidable but incomplete, whereas the set of all true first-order statements about nonnegative integers in the language with + and × is complete but undecidable.
Indeed, the proof that a logical system or theory is undecidable will use the formal definition of computability to show that an appropriate set is not a decidable set, and then invoke Church's thesis to show that the theory or logical system is not decidable by any effective method (Enderton 2001, pp. 206ff.).