Eine Theorie ist entscheidbar, wenn es einen Algorithmus gibt, der für jede Formel in der Sprache der Theorie in endlicher Zeit entscheidet, ob diese Formel eine Folgerung der Theorie ist (also zur Menge der Theoreme der Theorie gehört).

Prinzip

Wirksamkeit der Theoremhaftigkeit: Entscheidbarkeit verlangt, dass die Menge der aus der Theorie beweisbaren Formeln eine entscheidbare (berechenbare) Menge ist, sodass Theoremhaftigkeit mechanisch prüfbar ist und nicht nur rekursiv aufzählbar oder semientscheidbar.

Demonstration

Beispiel: Presburger-Arithmetik (die Theorie der ganzen Zahlen mit Addition) ist entscheidbar; die Theorie reell abgeschlossener Körper ist entscheidbar, weil Quantorenelimination Sätze auf quantorenfreie Aussagen reduziert, die algorithmisch überprüfbar sind; viele Theorien mit Quantorenkontrolle sind entscheidbar.

Fehlanwendung

Zu glauben, Entscheidbarkeit impliziere praktische Durchführbarkeit: Eine entscheidbare Theorie kann eine extrem hohe Komplexität aufweisen, sodass die Beweissuche unpraktisch wird; oder anzunehmen, Entscheidbarkeit bleibe bei Erweiterungen der Sprache oder Axiome ohne Prüfung erhalten.

Konsequenz

Entscheidbarkeit liefert ein effektives Verfahren zur Bestimmung der Theoremhaftigkeit, ermöglicht automatisches Schließen, algorithmische Klassifikation von Formeln und reproduzierbare Verifikation von Eigenschaften; sie steht zudem in Beziehung zur Komplexitätstheorie bezüglich praktischer Durchführbarkeit.

Umkehrung

Eine unentscheidbare Theorie besitzt keinen Algorithmus, der Theoremhaftigkeit entscheidet: Beispiele sind hinreichend ausdrucksstarke arithmetische Systeme, was fundamentale Grenzen für Automatisierung setzt.

Abgrenzung

Entscheidbarkeit hängt von der Wahl von Sprache, Signatur und Axiomen ab; eine Theorie kann in einer Sprache entscheidbar, nach Hinzufügen von Symbolen oder Axiomen jedoch unentscheidbar sein. Zu unterscheiden sind Entscheidbarkeit, semientscheidbare (rekursiv aufzählbare) Mengen und Vollständigkeit als eigenständige Begriffe.

Semantische Spannung

Spannung zwischen Entscheidbarkeit, Vollständigkeit und Axiomatisierbarkeit: Vollständigkeit betrifft Wahrheitswerte, Axiomatisierbarkeit rekursive Aufzählbarkeit der Axiome; Entscheidbarkeit verlangt ein effektives Verfahren für die vollständige Folgerungsmenge und liegt damit an der Schnittstelle von logischer Ausdruckskraft und Berechenbarkeitsbeschränkungen.

Synthese

Eine entscheidbare Theorie ist eine, deren logische Konsequenzen mechanisch und zuverlässig bestimmbar sind: Sie macht Theoremhaftigkeit zu einer algorithmischen Tatsache statt zu einer theoretischen Möglichkeit und ermöglicht automatische Verifikation und konkrete Berechnung in modeltheoretischen und algebraischen Anwendungen.