Decidability (logic)
From Wikipedia, the free encyclopedia
A logical system or theory is decidable if the set of all well-formed formulas valid in the system is decidable. That is, there exists an algorithm such that for every formula in the system the algorithm is capable of deciding in finitely many steps whether the formula is valid in the system or not.
Example: Propositional logic is decidable, because there exists for it an algorithm—truth-table construction—such that for every formula which combines M atomic formulas there is a maximum number N = 2M of steps such that after completing those N steps the algorithm will always decide whether the formula is valid or not. Here, a "step" of the algorithm has been (arbitrarily) defined as completion of a row of the truth-table.
First-order logic is decidable if confined to predicates with only one argument (see monadic predicate calculus). If it includes predicates with two or more arguments, then it is not decidable. Famous examples of decidable first-order theories include the theory of real closed fields, and Presburger arithmetic.
Every complete recursively enumerable theory is decidable. On the other hand, every consistent theory which includes some basic arithmetic is undecidable.
Decidability should not be confused with completeness. For example, the theory of algebraically closed fields is decidable but incomplete, whereas true arithmetic (the set of all true first-order statements about nonnegative integers in the language with + and ×) is complete but undecidable. Unfortunately, as a terminological ambiguity, the term "undecidable statement" is sometimes used as a synonym for independent statement.
