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

views updated

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), and—if a number-theoretic conjecture of Schanuel is true—the 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 decidable—in 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.

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): 40–41. Correction ibid : 101–102.

Gödel, Kurt. "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I." Monatshefte für Mathematik und Physik 38 (1931): 173–198. Edited and translated in Kurt Gödel. Collected Works Volume I: Publications 1929–1936, ed. Solomon Feferman, et al, pp. 144–195. 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): 418–463.

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

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

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): 92–101; supplementarty note ibid : 395.