Decidability (logic) - Some Decidable Theories

Some Decidable Theories

Some decidable theories include (Monk 1976, p. 234):

• 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 integers 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 Boolean algebras, established by Alfred Tarski 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.
• The first-order theory of Euclidean geometry, established by Tarski in 1949.
• 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)

Methods used to establish decidability include quantifier elimination, model completeness, and Vaught's test.