Decidability (logic)
In
Decidability of a logical system
Each
A logical system is decidable if there is an effective method for determining whether arbitrary formulas are theorems of the logical system. For example,
First-order logic is not decidable in general; in particular, the set of logical validities in any signature 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 as second-order logic and type theory, are also undecidable.
The validities of monadic 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,
Decidability of a theory
A theory is a set of formulas, often assumed to be closed under logical 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-
A consistent theory that has the property that every consistent extension is undecidable is said to be essentially 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 of real closed fields, and Presburger arithmetic, while the theory of groups and Robinson arithmetic are examples of undecidable theories.
Some decidable theories
Some decidable theories include (Monk 1976, p. 234):[2]
- The set of first-order logical validities in the signature with only equality, established by Leopold Löwenheim in 1915.
- The set of first-order logical validities in a signature with equality and one unary function, established by Ehrenfeucht in 1959.
- The first-order theory of the natural numbers in the signature with equality and addition, also called Presburger arithmetic. The completeness was established by Mojżesz Presburger in 1929.
- The first-order theory of the natural numbers in the signature with equality and multiplication, also called Skolem arithmetic.
- The first-order theory of Boolean algebras, established by Alfred Tarski in 1940 (found in 1940 but announced in 1949).
- The first-order theory of algebraically closed fields of a given characteristic, established by Tarski in 1949.
- The first-order theory of real-closed ordered fields, established by Tarski in 1949 (see also Tarski's exponential function problem).
- The first-order theory of Euclidean geometry, established by Tarski in 1949.
- The first-order theory of Abelian groups, established by Szmielew in 1955.
- The first-order theory of hyperbolic geometry, established by Schwabhäuser in 1959.
- Specific decidable sublanguages of set theory investigated in the 1980s through today.(Cantone et al., 2001)
- The monadic second-order theory of trees (see S2S).
Methods used to establish decidability include
Some undecidable theories
Some undecidable theories include (Monk 1976, p. 279):[2]
- The set of logical validities in any first-order signature with equality and either: a relation symbol of arity no less than 2, or two unary function symbols, or one function symbol of arity no less than 2, established by Trakhtenbrot in 1953.
- The first-order theory of the natural numbers with addition, multiplication, and equality, established by Tarski and Andrzej Mostowski in 1949.
- The first-order theory of the rational numbers with addition, multiplication, and equality, established by Julia Robinson in 1949.
- The first-order theory of groups, established by Alfred Tarski in 1953.[3] Remarkably, not only the general theory of groups is undecidable, but also several more specific theories, for example (as established by Mal'cev 1961) the theory of finite groups. Mal'cev also established that the theory of semigroups and the theory of rings are undecidable. Robinson established in 1949 that the theory of fields is undecidable.
- Raphael Robinsonin 1950.
- The first-order theory with equality and two function symbols[4]
The interpretability method is often used to establish undecidability of theories. If an essentially undecidable theory T is interpretable in a consistent theory S, then S is also essentially undecidable. This is closely related to the concept of a many-one reduction in computability theory.
Semidecidability
A property of a theory or logical system weaker than decidability is semidecidability. 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 is not 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 validities V 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 formula A whether A is not in V. Similarly, the set of logical consequences of any
Relationship with completeness
Decidability should not be confused with completeness. 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. Unfortunately, as a terminological ambiguity, the term "undecidable statement" is sometimes used as a synonym for independent statement.
Relationship to computability
As with the concept of a
In context of games
Some
- Chess is decidable.[5][6] The same holds for all other finite two-player games with perfect information.
- Mate in n in infinite chess (with limitations on rules and gamepieces) is decidable.[7][8] However, there are positions (with finitely many pieces) that are forced wins, but not mate in n for any finite n.[9]
- Some team games with imperfect information on a finite board (but with unlimited time) are undecidable.[10]
See also
References
Notes
- ^ Trakhtenbrot, 1953 .
- ^ ISBN 9780387901701.
- ISBN 9780444533784
- S2CID 798307. Retrieved 5 August 2014.
- ^ Stack Exchange Computer Science. "Is chess game movement TM decidable?"
- ^ Undecidable Chess Problem?
- ^ Mathoverflow.net/Decidability-of-chess-on-an-infinite-board Decidability-of-chess-on-an-infinite-board
- S2CID 8998263.
- ^ "Lo.logic – Checkmate in $\omega$ moves?".
- ISBN 9781107002661.}
Bibliography
- ISBN 978-0-444-86388-1
- Cantone, D.; Omodeo, E. G.; Policriti, A. (2013) [2001], Set Theory for Computing. From Decision Procedures to Logic Programming with Sets, Monographs in Computer Science, Springer, ISBN 9781475734522
- Chagrov, Alexander; Zakharyaschev, Michael (1997), Modal logic, Oxford Logic Guides, vol. 35, Oxford University Press, MR 1464942
- ISBN 9780486151069
- Enderton, Herbert (2001), A mathematical introduction to logic (2nd ed.), ISBN 978-0-12-238452-3
- ISBN 978-0-444-86388-1
- Monk, J. Donald (2012) [1976], Mathematical Logic, ISBN 9781468494525