# Decidability (logic)

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Decidability_(logic)
> Markdown URL: https://mediated.wiki/source/Decidability_(logic).md
> Source: https://en.wikipedia.org/wiki/Decidability_(logic)
> Source revision: 1325540591
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

Whether a decision problem has an effective method to derive the answer

In [logic](/source/Logic), a true/false [decision problem](/source/Decision_problem) is **decidable** if there exists an [effective method](/source/Effective_method) for deriving the correct answer. [Logical systems](/source/Formal_system) are decidable if membership in their set of [logically valid](/source/Validity_(logic)) formulas (or theorems) can be effectively determined. [Zeroth-order logic](/source/Zeroth-order_logic) (propositional logic) is decidable, whereas [first-order](/source/First-order_logic) and [higher-order](/source/Higher-order_logic) logic are not. A [theory](/source/Theory_(mathematical_logic)) (set of sentences [closed](/source/Deductive_closure) under [logical consequence](/source/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](/source/Undecidable_problem), 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.

## Decidability of a logical system

Each [logical system](/source/Logical_system) comes with both a [syntactic component](/source/Syntax_(logic)), which among other things determines the notion of [provability](/source/Formal_proof), and a [semantic component](/source/Formal_semantics_(logic)), which determines the notion of [logical validity](/source/Logical_validity). 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](/source/G%C3%B6del's_completeness_theorem) establishes the equivalence of semantic and syntactic consequence. In other settings, such as [linear logic](/source/Linear_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](/source/Propositional_logic) is decidable, because the [truth-table](/source/Truth_table) method can be used to determine whether an arbitrary [propositional formula](/source/Propositional_formula) is logically valid.

[First-order logic](/source/First-order_logic) is not decidable in general; in particular, the set of logical validities in any [signature](/source/Signature_(logic)) that includes equality and at least one other [predicate symbol](/source/Predicate_(logic)) with two or more arguments is not decidable.[1] Logical systems extending first-order logic, such as [second-order logic](/source/Second-order_logic) and [type theory](/source/Type_theory), are also undecidable.

The validities of [monadic predicate calculus](/source/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 predicate 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](/source/Ternary_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 of [sequents](/source/Sequent), or the [consequence relation](/source/Logical_consequence) {(Г, *A*) | Г ⊧ *A*} of the logic.

## Decidability of a theory

A [theory](/source/Theory_(mathematical_logic)) is a set of formulas, often assumed to be [closed](/source/Deductively_closed) under [logical consequence](/source/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](/source/Axiom).

There are several basic results about decidability of theories. Every (non-[paraconsistent](/source/Paraconsistent_logic)) 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. Every [complete](/source/Complete_theory) [computably enumerable](/source/Computably_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 be **essentially undecidable**. In fact, every consistent extension will be essentially undecidable. The theory of [fields](/source/Field_(mathematics)) is undecidable but not essentially undecidable. [Robinson arithmetic](/source/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](/source/Real_closed_field), and [Presburger arithmetic](/source/Presburger_arithmetic), while the theory of [groups](/source/Group_(mathematics)) and [Robinson arithmetic](/source/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](/source/Leopold_L%C3%B6wenheim) in 1915.

- The set of first-order logical validities in a signature with equality and one unary function, established by [Ehrenfeucht](/source/Ehrenfeucht) in 1959.

- The first-order theory of the [natural numbers](/source/Natural_number) in the signature with equality and addition, also called [Presburger arithmetic](/source/Presburger_arithmetic). The completeness was established by [Mojżesz Presburger](/source/Moj%C5%BCesz_Presburger) in 1929.

- The first-order theory of the natural numbers in the signature with equality and multiplication, also called [Skolem arithmetic](/source/Skolem_arithmetic).

- The first-order theory of [Boolean algebras](/source/Boolean_algebras_canonically_defined), established by [Alfred Tarski](/source/Alfred_Tarski) in 1940 (found in 1940 but announced in 1949).

- The first-order theory of [algebraically closed fields](/source/Algebraically_closed_field) of a given [characteristic](/source/Characteristic_(algebra)), established by Tarski in 1949.

- The [first-order theory of real-closed ordered fields](/source/Decidability_of_First-order_Theory_of_Real_Numbers), [established by Tarski in 1949](/source/Tarski%E2%80%93Seidenberg_theorem) (see also [Tarski's exponential function problem](/source/Tarski's_exponential_function_problem)).

- The first-order theory of [Euclidean geometry](/source/Euclidean_geometry), established by Tarski in 1949.

- The first-order theory of [abelian groups](/source/Abelian_group), established by [Szmielew](/source/Wanda_Szmielew) in 1955.

- The first-order theory of [hyperbolic geometry](/source/Hyperbolic_geometry), established by Schwabhäuser in 1959.

- Specific [decidable sublanguages of set theory](/source/Decidable_sublanguages_of_set_theory) investigated in the 1980s through today. (Cantone *et al.*, 2001)

- The [monadic second-order](/source/Monadic_second-order_logic) theory of [trees](/source/Tree_(graph_theory)) (see [S2S](/source/S2S_(mathematics))).

Methods used to establish decidability include [quantifier elimination](/source/Quantifier_elimination), [model completeness](/source/Model_completeness), and the [Łoś–Vaught test](/source/%C5%81o%C5%9B%E2%80%93Vaught_test).

## Some undecidable theories

Some undecidable theories include:[2]

- The set of logical validities in any first-order signature with equality and either: a predicate symbol of [arity](/source/Arity) no less than 2, or two unary function symbols, or one function symbol of arity no less than 2, established by [Trakhtenbrot](/source/Boris_Trakhtenbrot) in 1953.

- The first-order theory of the natural numbers with addition, multiplication, and equality, established by Tarski and [Andrzej Mostowski](/source/Andrzej_Mostowski) in 1949.

- The first-order theory of the [rational numbers](/source/Rational_number) with addition, multiplication, and equality, established by [Julia Robinson](/source/Julia_Robinson) in 1949.

- The first-order theory of [groups](/source/Group_(mathematics)), established by [Alfred Tarski](/source/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](/source/Anatoly_Maltsev) 1961) the theory of [finite groups](/source/Finite_group). Mal'cev also established that the theory of [semigroups](/source/Semigroup) and the theory of [rings](/source/Ring_(mathematics)) are undecidable. Robinson established in 1949 that the theory of [fields](/source/Field_(mathematics)) is undecidable.

- [Robinson arithmetic](/source/Robinson_arithmetic) (and therefore any consistent extension, such as [Peano arithmetic](/source/Peano_arithmetic)) is essentially undecidable, as established by [Raphael Robinson](/source/Raphael_Robinson) in 1950.

- The first-order theory with equality and two function symbols.[4]

The [interpretability](/source/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](/source/Many-one_reduction) in [computability theory](/source/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 or arrives as negative. Equivalently, 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 semidecidable. For example, the set of logical validities *V* of first-order logic is semidecidable, 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 [computably enumerable set](/source/Computably_enumerable_set) of first-order axioms is semidecidable. Many of the examples of undecidable first-order theories given above are of this form.

## Relationship with completeness

Decidability should not be confused with [completeness](/source/Complete_theory). For example, the theory of [algebraically closed fields](/source/Algebraically_closed_field) is decidable but incomplete, whereas the set of all true first-order statements about the natural numbers 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](/source/Independence_(mathematical_logic)).

## Relationship to computability

As with the concept of a [decidable set](/source/Decidable_set), the definition of a decidable theory or logical system can be given either in terms of *[effective methods](/source/Effective_method)* or in terms of *[computable functions](/source/Computable_function)*. These are generally considered equivalent per [Church's thesis](/source/Church'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. 206*ff.*).

## In context of games

Some [games](/source/Games) have been classified as to their decidability:

- Mate in *n* in [infinite chess](/source/Infinite_chess) (with limitations on rules and gamepieces) is decidable.[5][6] However, there are positions (with finitely many pieces) that are forced wins, but not mate in *n* for any finite *n*.[7]

- Some team games with [imperfect information](/source/Imperfect_information) on a finite board (but with unlimited time) are undecidable.[8]

## See also

- [Philosophy portal](https://en.wikipedia.org/wiki/Portal:Philosophy)

- [Entscheidungsproblem](/source/Entscheidungsproblem)

- [Existential quantification](/source/Existential_quantification)

## References

### Notes

1. **[^](#cite_ref-1)** [Boris Trakhtenbrot](/source/Boris_Trakhtenbrot) (1953). "On recursive separability". *[Doklady Akademii Nauk SSSR](/source/Doklady_Akademii_Nauk_SSSR)* (in Russian). **88**: 935–956.

1. ^ [***a***](#cite_ref-Monk1976_2-0) [***b***](#cite_ref-Monk1976_2-1) Monk, Donald (1976). [*Mathematical Logic*](https://archive.org/details/mathematicallogi00jdon). Springer. p. 279. [ISBN](/source/ISBN_(identifier)) [9780387901701](https://en.wikipedia.org/wiki/Special:BookSources/9780387901701).

1. **[^](#cite_ref-3)** Tarski, A.; Mostovski, A.; Robinson, R. (1953), [*Undecidable Theories*](https://books.google.com/books?id=XtLbjZjB1B8C&pg=PP1), Studies in Logic and the Foundation of Mathematics, North-Holland, Amsterdam, [ISBN](/source/ISBN_(identifier)) [9780444533784](https://en.wikipedia.org/wiki/Special:BookSources/9780444533784) {{[citation](https://en.wikipedia.org/wiki/Template:Citation)}}: ISBN / Date incompatibility ([help](https://en.wikipedia.org/wiki/Help:CS1_errors#invalid_isbn_date))

1. **[^](#cite_ref-4)** [Gurevich, Yuri](/source/Yuri_Gurevich) (1976). ["The Decision Problem for Standard Classes"](http://dblp.uni-trier.de/rec/bib/journals/jsyml/Gurevich76). *[J. Symb. Log.](/source/J._Symb._Log.)* **41** (2): 460–464. [CiteSeerX](/source/CiteSeerX_(identifier)) [10.1.1.360.1517](https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.360.1517). [doi](/source/Doi_(identifier)):[10.1017/S0022481200051513](https://doi.org/10.1017%2FS0022481200051513). [S2CID](/source/S2CID_(identifier)) [798307](https://api.semanticscholar.org/CorpusID:798307). Retrieved 5 August 2014.

1. **[^](#cite_ref-Decidability_5-0)** [Mathoverflow.net/Decidability-of-chess-on-an-infinite-board Decidability-of-chess-on-an-infinite-board](https://mathoverflow.net/q/27967)

1. **[^](#cite_ref-Mate_in_N_6-0)** Brumleve, Dan; [Hamkins, Joel David](/source/Joel_David_Hamkins); Schlicht, Philipp (2012). ["The Mate-in-n Problem of Infinite Chess Is Decidable"](https://link.springer.com/chapter/10.1007%2F978-3-642-30870-3_9). *Conference on [Computability in Europe](/source/Computability_in_Europe)*. Lecture Notes in Computer Science. Vol. 7318. Springer. pp. 78–88. [arXiv](/source/ArXiv_(identifier)):[1201.5597](https://arxiv.org/abs/1201.5597). [doi](/source/Doi_(identifier)):[10.1007/978-3-642-30870-3_9](https://doi.org/10.1007%2F978-3-642-30870-3_9). [ISBN](/source/ISBN_(identifier)) [978-3-642-30870-3](https://en.wikipedia.org/wiki/Special:BookSources/978-3-642-30870-3). [S2CID](/source/S2CID_(identifier)) [8998263](https://api.semanticscholar.org/CorpusID:8998263).

1. **[^](#cite_ref-7)** ["Lo.logic – Checkmate in $\omega$ moves?"](https://mathoverflow.net/q/63423).

1. **[^](#cite_ref-8)** [Poonen, Bjorn](/source/Bjorn_Poonen) (2014). ["10. Undecidable Problems: A Sampler: §14.1 Abstract Games"](https://books.google.com/books?id=ulw3BAAAQBAJ&pg=PA211). In Kennedy, Juliette (ed.). *Interpreting Gödel: Critical Essays*. Cambridge University Press. pp. 211–241 See p. 239. [arXiv](/source/ArXiv_(identifier)):[1204.0299](https://arxiv.org/abs/1204.0299). [CiteSeerX](/source/CiteSeerX_(identifier)) [10.1.1.679.3322](https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.679.3322). [ISBN](/source/ISBN_(identifier)) [9781107002661](https://en.wikipedia.org/wiki/Special:BookSources/9781107002661).

### Bibliography

- [Barwise, Jon](/source/Jon_Barwise) (1982), "Introduction to first-order logic", in Barwise, Jon (ed.), *Handbook of Mathematical Logic*, Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, [ISBN](/source/ISBN_(identifier)) [978-0-444-86388-1](https://en.wikipedia.org/wiki/Special:BookSources/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*](https://books.google.com/books?id=KWvlBwAAQBAJ&pg=PR2), Monographs in Computer Science, Springer, [ISBN](/source/ISBN_(identifier)) [9781475734522](https://en.wikipedia.org/wiki/Special:BookSources/9781475734522)

- Chagrov, Alexander; Zakharyaschev, Michael (1997), *Modal logic*, Oxford Logic Guides, vol. 35, Oxford University Press, [ISBN](/source/ISBN_(identifier)) [978-0-19-853779-3](https://en.wikipedia.org/wiki/Special:BookSources/978-0-19-853779-3), [MR](/source/MR_(identifier)) [1464942](https://mathscinet.ams.org/mathscinet-getitem?mr=1464942)

- [Davis, Martin](/source/Martin_Davis_(mathematician)) (2013) [1958], [*Computability and Unsolvability*](https://books.google.com/books?id=nbOqAAAAQBAJ&pg=PP1), Dover, [ISBN](/source/ISBN_(identifier)) [9780486151069](https://en.wikipedia.org/wiki/Special:BookSources/9780486151069)

- Enderton, Herbert (2001), *A mathematical introduction to logic* (2nd ed.), [Academic Press](/source/Academic_Press), [ISBN](/source/ISBN_(identifier)) [978-0-12-238452-3](https://en.wikipedia.org/wiki/Special:BookSources/978-0-12-238452-3)

- [Keisler, H. J.](/source/H._J._Keisler) (1982), "Fundamentals of model theory", in Barwise, Jon (ed.), *Handbook of Mathematical Logic*, Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, [ISBN](/source/ISBN_(identifier)) [978-0-444-86388-1](https://en.wikipedia.org/wiki/Special:BookSources/978-0-444-86388-1)

- Monk, J. Donald (2012) [1976], *Mathematical Logic*, [Springer-Verlag](/source/Springer-Verlag), [ISBN](/source/ISBN_(identifier)) [9781468494525](https://en.wikipedia.org/wiki/Special:BookSources/9781468494525)

v t e Mathematical logic General Axiom list Cardinality First-order logic Formal proof Formal semantics Foundations of mathematics Information theory Lemma Logical consequence Model Theorem Theory Type theory Theorems (list), paradoxes Gödel's completeness – incompleteness theorems Tarski's undefinability Banach–Tarski paradox Cantor's theorem – paradox – diagonal argument Compactness Halting problem Lindström's Löwenheim–Skolem Russell's paradox Logics Traditional Classical logic Logical truth Tautology Proposition Inference Logical equivalence Consistency Equiconsistency Argument Soundness Validity Syllogism Square of opposition Venn diagram Propositional Boolean algebra Boolean functions Logical connectives Propositional calculus Propositional formula Truth tables Many-valued logic 3 finite ∞ Predicate First-order list Second-order Monadic Higher-order Fixed-point Free Quantifiers Predicate Monadic predicate calculus Set theory Set hereditary Class (Ur-)Element Ordinal number Extensionality Forcing Relation equivalence partition Set operations: intersection union complement Cartesian product power set identities Types of sets Countable Uncountable Empty Inhabited Singleton Finite Infinite Transitive Ultrafilter Recursive Fuzzy Universal Universe constructible Grothendieck Von Neumann Maps, cardinality Function/Map domain codomain image In/Sur/Bi-jection Schröder–Bernstein theorem Isomorphism Gödel numbering Enumeration Large cardinal inaccessible Aleph number Operation binary Theories Zermelo–Fraenkel axiom of choice continuum hypothesis General Kripke–Platek Morse–Kelley Naive New Foundations Tarski–Grothendieck Von Neumann–Bernays–Gödel Ackermann Constructive Formal systems (list), language, syntax Alphabet Arity Automata Axiom schema Expression ground Extension by definition conservative Relation Formation rule Grammar Formula atomic closed ground open Free/bound variable Language Metalanguage Logical connective ¬ ∨ ∧ → ↔ = Predicate functional variable propositional variable Proof Quantifier ∃ ! ∀ rank Sentence atomic spectrum Signature String Substitution Symbol function logical/constant non-logical variable Term Theory list Example axiomatic systems (list) of true arithmetic Peano second-order elementary function primitive recursive Robinson Skolem of the real numbers Tarski's axiomatization of Boolean algebras canonical minimal axioms of geometry Euclidean Elements Hilbert's Tarski's non-Euclidean Principia Mathematica Proof theory Formal proof Natural deduction Logical consequence Rule of inference Sequent calculus Theorem Systems axiomatic deductive Hilbert list Complete theory Independence (from ZFC) Proof of impossibility Ordinal analysis Reverse mathematics Self-verifying theories Model theory Interpretation function of models Model atomic equivalence finite prime saturated spectrum submodel Non-standard model of non-standard arithmetic Diagram elementary Categorical theory Model complete theory Satisfiability Semantics of logic Strength Theories of truth semantic Tarski's Kripke's T-schema Transfer principle Truth predicate Truth value Type Ultraproduct Validity Computability theory Church encoding Church–Turing thesis Computably enumerable Computable function Computable set Decision problem decidable undecidable P NP P versus NP problem Kolmogorov complexity Lambda calculus Primitive recursive function Recursion Recursive set Turing machine Type theory Related Abstract logic Algebraic logic Automated theorem proving Category theory Concrete/Abstract category Category of sets History of logic History of mathematical logic timeline Logicism Mathematical object Philosophy of mathematics Supertask Mathematics portal

v t e Metalogic and metamathematics Cantor's theorem Entscheidungsproblem Church–Turing thesis Consistency Effective method Foundations of mathematics of geometry Gödel's completeness theorem Gödel's incompleteness theorems Soundness Completeness Decidability Interpretation Löwenheim–Skolem theorem Metatheorem Satisfiability Independence Type–token distinction Use–mention distinction

Authority control databases International FAST National United States France BnF data Czech Republic Israel Other IdRef Yale LUX

---
Adapted from the Wikipedia article [Decidability (logic)](https://en.wikipedia.org/wiki/Decidability_(logic)) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Decidability_(logic)?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.