Skip to main content

Modern Logic: Since Gödel: Decidable and Undecidable Theories

MODERN LOGIC: SINCE GÖDEL: DECIDABLE AND UNDECIDABLE THEORIES

Suppose T is a theory (i.e., a set of sentences) in a formal language L of logic. A decision procedure for T is a mechanical procedure for calculating whether any given sentence of L is a logical consequence of T. We say that T is decidable if it has a decision procedure and undecidable if not. The decision problem for T is to determine whether or not T is decidable. (One can avoid the slightly vague notion of a mechanical procedure by noting that a theory T is decidable if and only if the set of its logical consequences is computable.)

Quantifier elimination and related model-theoretic techniques have yielded proofs that many important first-order theories are decidable. Examples are the theory of addition of integers (Presburger 1930), the theories of real-closed fields and algebraically closed fields (Tarski 1951), the theory of abelian groups (Szmielew 1955), andif a number-theoretic conjecture of Schanuel is truethe theory of the field of real numbers with exponentiation (Macintyre and Wilkie 1996). The first theory shown to be undecidable was first-order Peano arithmetic; Kurt Gödel proved its undecidability in 1931. Many other undecidable theories are known, but the proofs of undecidability are all based directly or indirectly on Gödel's ideas. In 1970 Yuri V. Matiyasevich (1993) improved Gödel's result by showing that the set of diophantine sentences true in the natural numbers is not computable (a diophantine sentence is one of the form "There are natural numbers m, n, and so on such that E is true," where E is an arithmetical equation using m, n, and so on). Part 3 of "Decidable and Undecidable Theories" of J. Donald Monk (1976) gives many examples.

We say that a formal language L of logic is decidable if the empty theory in L is decidablein other words, if there is a mechanical test to determine which sentences of L are valid. Gödel's ideas led to a proof that if L is a nontrivial first-order language, for example, with at least one binary relation symbol besides equality, then L is undecidable (Church 1936). Later research extended this result to various important sublanguages of first-order languages. But there are also decidable languages, for example, languages of propositional logic and a number of languages with monadic predicate symbols (e.g., the language of syllogisms). See Egon Börger, Erich Grädel, and Yuri Gurevich (1997) for full information on decidable and undecidable languages. After their book appeared, a new family of decidable languages was discovered, the guarded languages, whose decidability implies the decidability of various modal logics (see Grädel, Hirsch, and Otto 2002).

The decision problem for logical languages is also known as the Entscheidungsproblem. See Paulo Mancosu (1999, §8) on the place of this problem in early twentieth-century thinking about the foundations of mathematics, particularly within the school of David Hilbert.

See also Computability Theory; First-Order Logic; Gödel's Theorem; Model Theory.

Bibliography

Börger, Egon, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Berlin: Springer, 1997.

Church, Alonzo. "A Note on the Entscheidungsproblem." Journal of Symbolic Logic 1 (1936): 4041. Correction ibid : 101102.

Gödel, Kurt. "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I." Monatshefte für Mathematik und Physik 38 (1931): 173198. Edited and translated in Kurt Gödel. Collected Works Volume I: Publications 19291936, ed. Solomon Feferman, et al, pp. 144195. New York: Oxford University Press, 1986.

Grädel, Erich, Colin Hirsch, and Martin Otto. "Back and Forth between Guarded and Modal Logics." ACM Transactions on Computational Logics 3 (2002): 418463.

Macintyre, Angus, and Alex Wilkie. "On the Decidability of the Real Exponential Field." Kreiseliana, edited by P. Odifreddi, pp. 441467. Wellesley, MA: A.K. Peters, 1996.

Mancosu, Paolo. "Between Russell and Hilbert: Behmann on the Foundations of Mathematics." Bulletin of Symbolic Logic 5 (1999): 303330.

Matiyasevich, Yuri V. Hilbert's Tenth Problem. Cambridge, MA: MIT Press, 1993.

Monk, J. Donald. Mathematical Logic. New York: Springer, 1976.

Presburger, Mojżesz. "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt." Comptes Rendus du Premier Congrès des Mathématiciens des Pays Slaves, Warszawa 1929. Warsaw (1930): 92101; supplementarty note ibid : 395.

Szmielew, Wanda. "Elementary Properties of Abelian Groups." Fundamenta Mathematicae 41 (1955): 203271.

Tarski, Alfred. A Decision Method for Elementary Algebra and Geometry. Berkeley: University of California Press, 1951.

Tarski, Alfred, Andrzej Mostowski, and Raphael M. Robinson. Undecidable Theories. Amsterdam: North-Holland, 1953.

Wilfrid Hodges (2005)

Cite this article
Pick a style below, and copy the text for your bibliography.

  • MLA
  • Chicago
  • APA

"Modern Logic: Since Gödel: Decidable and Undecidable Theories." Encyclopedia of Philosophy. . Encyclopedia.com. 17 Oct. 2018 <http://www.encyclopedia.com>.

"Modern Logic: Since Gödel: Decidable and Undecidable Theories." Encyclopedia of Philosophy. . Encyclopedia.com. (October 17, 2018). http://www.encyclopedia.com/humanities/encyclopedias-almanacs-transcripts-and-maps/modern-logic-godel-decidable-and-undecidable-theories

"Modern Logic: Since Gödel: Decidable and Undecidable Theories." Encyclopedia of Philosophy. . Retrieved October 17, 2018 from Encyclopedia.com: http://www.encyclopedia.com/humanities/encyclopedias-almanacs-transcripts-and-maps/modern-logic-godel-decidable-and-undecidable-theories

Learn more about citation styles

Citation styles

Encyclopedia.com gives you the ability to cite reference entries and articles according to common styles from the Modern Language Association (MLA), The Chicago Manual of Style, and the American Psychological Association (APA).

Within the “Cite this article” tool, pick a style to see how all available information looks when formatted according to that style. Then, copy and paste the text into your bibliography or works cited list.

Because each style has its own formatting nuances that evolve over time and not all information is available for every reference entry or article, Encyclopedia.com cannot guarantee each citation it generates. Therefore, it’s best to use Encyclopedia.com citations as a starting point before checking the style against your school or publication’s requirements and the most-recent information available at these sites:

Modern Language Association

http://www.mla.org/style

The Chicago Manual of Style

http://www.chicagomanualofstyle.org/tools_citationguide.html

American Psychological Association

http://apastyle.apa.org/

Notes:
  • Most online reference entries and articles do not have page numbers. Therefore, that information is unavailable for most Encyclopedia.com content. However, the date of retrieval is often important. Refer to each style’s convention regarding the best way to format page numbers and retrieval dates.
  • In addition to the MLA, Chicago, and APA styles, your school, university, publication, or institution may have its own requirements for citations. Therefore, be sure to refer to those guidelines when editing your bibliography or works cited list.