Decidability (logic) - Some Undecidable Theories

Some Undecidable Theories

Some undecidable theories include (Monk 1976, p. 279):

• 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 Mal'cev in 1961. 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.
• Peano arithmetic is essentially undecidable. Gödel's incompleteness theorems show that many other sufficiently strong theories of arithmetic share this property.

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.