Inlogic, a true/falsedecision problem isdecidable if there exists aneffective method for deriving the correct answer.Zeroth-order logic (propositional logic) is decidable, whereasfirst-order andhigher-order logic are not.Logical systems are decidable if membership in their set oflogically valid formulas (or theorems) can be effectively determined. Atheory (set of sentencesclosed underlogical 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 areundecidable, 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.
Eachlogical system comes with both asyntactic component, which among other things determines the notion ofprovability, and asemantic component, which determines the notion oflogical validity. The logically valid formulas of a system are sometimes called thetheorems of the system, especially in the context of first-order logic whereGödel's completeness theorem establishes the equivalence of semantic and syntactic consequence. In other settings, such aslinear logic, the syntactic consequence (provability) relation may be used to define the theorems of a system.
A logical system is decidable if there is an effective method for determining whether arbitrary formulas are theorems of the logical system. For example,propositional logic is decidable, because thetruth-table method can be used to determine whether an arbitrarypropositional formula is logically valid.
First-order logic is not decidable in general; in particular, the set of logical validities in anysignature that includes equality and at least one other predicate with two or more arguments is not decidable.[1] Logical systems extending first-order logic, such assecond-order logic andtype theory, are also undecidable.
The validities ofmonadic predicate calculus with identity are decidable, however. This system is first-order logic restricted to those signatures that have no function symbols and whose relation symbols other than equality never take more than one argument.
Some logical systems are not adequately represented by the set of theorems alone. (For example,Kleene's logic has no theorems at all.) 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 ofsequents, or theconsequence relation {(Г,A) | Г ⊧A} of the logic.
Atheory is a set of formulas, often assumed to beclosed underlogical consequence. Decidability for a theory concerns whether there is an effective procedure that decides whether the formula is a member of the theory or not, given an arbitrary formula in the signature of the theory. The problem of decidability arises naturally when a theory is defined as the set of logical consequences of a fixed set of axioms.
There are several basic results about decidability of theories. Every (non-paraconsistent) inconsistent theory is decidable, as every formula in the signature of the theory will be a logical consequence of, and thus a member of, the theory. Everycompleterecursively enumerable first-order theory is decidable. An extension of a decidable theory may not be decidable. For example, there are undecidable theories in propositional logic, although the set of validities (the smallest theory) is decidable.
A consistent theory that has the property that every consistent extension is undecidable is said to beessentially undecidable. In fact, every consistent extension will be essentially undecidable. The theory of fields is undecidable but not essentially undecidable.Robinson arithmetic is known to be essentially undecidable, and thus every consistent theory that includes or interprets Robinson arithmetic is also (essentially) undecidable.
Examples of decidable first-order theories include the theory ofreal closed fields, andPresburger arithmetic, while the theory ofgroups andRobinson arithmetic are examples of undecidable theories.
Some decidable theories include (Monk 1976, p. 234):[2]
Methods used to establish decidability includequantifier elimination,model completeness, and theŁoś-Vaught test.
Some undecidable theories include:[2]
Theinterpretability method is often used to establish undecidability of theories. If an essentially undecidable theoryT is interpretable in a consistent theoryS, thenS is also essentially undecidable. This is closely related to the concept of amany-one reduction incomputability theory.
A property of a theory or logical system weaker than decidability issemidecidability. A theory is semidecidable if there is a well-defined method whose result, given an arbitrary formula, arrives as positive, if the formula is in the theory; otherwise, may never arrive at all; otherwise, arrives as negative. A logical system is semidecidable if there is a well-defined method for generating a sequence of theorems such that each theorem will eventually be generated. This is different from decidability because in a semidecidable system there may be no effective procedure for checking that a formula isnot a theorem.
Every decidable theory or logical system is semidecidable, but in general the converse is not true; a theory is decidable if and only if both it and its complement are semi-decidable. For example, the set of logical validitiesV of first-order logic is semi-decidable, but not decidable. In this case, it is because there is no effective method for determining for an arbitrary formulaA whetherA is not inV. Similarly, the set of logical consequences of anyrecursively enumerable set of first-order axioms is semidecidable. Many of the examples of undecidable first-order theories given above are of this form.
Decidability should not be confused withcompleteness. For example, the theory ofalgebraically 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. Unfortunately, as a terminological ambiguity, the term "undecidable statement" is sometimes used as a synonym forindependent statement.
As with the concept of adecidable set, the definition of a decidable theory or logical system can be given either in terms ofeffective methods or in terms ofcomputable functions. These are generally considered equivalent perChurch's thesis. 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.).
Somegames have been classified as to their decidability:
{{citation}}:ISBN / Date incompatibility (help)| General | |||||||||
|---|---|---|---|---|---|---|---|---|---|
| Theorems (list) and paradoxes | |||||||||
| Logics |
| ||||||||
| Set theory |
| ||||||||
| Formal systems (list), language and syntax |
| ||||||||
| Proof theory | |||||||||
| Model theory | |||||||||
| Computability theory | |||||||||
| Related | |||||||||
| International | |
|---|---|
| National | |
| Other | |
