eine logische Theorie, die, als Menge von Formeln aufgefaßt, entscheidbar ist.

Intuitiv heißt dies, daß es es einen Algorithmus gibt, der bei Eingabe einer Formel in endlich vielen Schritten entscheidet, ob die Formel zur betreffenden Theorie gehört oder nicht.

Ein Beispiel für eine entscheidbare Theorie ist Th(ℕ, +), die sog. Presburger-Arithmetik.

Unentscheidbar ist dagegen Th(ℕ, +, *), die elementare Zahlentheorie, oder PL₁, die Menge aller wahren Formeln der Prädikatenlogik erster Stufe.