Decidability (logic)

You don't need to be Editor-In-Chief to add or edit content to WikiDoc. You can begin to add to or edit text on this WikiDoc page by clicking on the edit button at the top of this page. Next enter or edit the information that you would like to appear here. Once you are done editing, scroll down and click the Save page button at the bottom of the page.

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 effective method such that for every formula in the system the method is capable of deciding whether the formula is valid (is a theorem) 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 = 2^M 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.

See also

• effective method
• completeness
• László Kalmár (1936)
• Leopold Löwenheim (1915)
• Alonzo Church (1956)
• W.V.O. Quine (1953)
• Meyer and Lambert (1967)

Template:Logiccs:Rozhodnutelnost fr:décidabilité he:כריעותsl:Odločljivost