Quantoreneliminierung

Quantoreneliminierung ist eine Eigenschaft einer formalen Theorie T in einer Sprache L: Jedes L-Formel φ(x1,...,xn) ist in T äquivalent zu einer quantifierfreien Formel ψ(x1,...,xn). Genauer: T ⊨ ∀x1,...,xn (φ ↔ ψ). Ist diese Eigenschaft vorhanden, spricht man davon, dass T Quantorenelimination besitzt. QE erleichtert die Beschreibung definierbarer Mengen und führt oft zu Entscheidbarkeit, sofern der quantifierfreie Teil der Sprache algorithmisch beherrschbar ist.

Bekannte Beispiele: Die Theorie der reell abgeschlossenen Körper hat Quantoreneliminierung in der Sprache der geordneten Ringe (Tarski-Seidenberg). Damit ist jede Aussage über reelle Zahlen, definierbar mit +, ·, < und Konstanten, äquivalent zu einer Booleschen Kombination von Polynomgleichungen und -ungleichungen. Die Theorie algebraisch abgeschlossener Körper besitzt QE in der Sprache der Körper (mit +, ·, 0, 1); daraus folgt Entscheidbarkeit der Theorie. Die Presburger-Arithmetik (N mit Addition, Ordnung, null und eins) besitzt QE in einer geeigneten Sprache und ist decidierbar.

Folgen und Anwendungen: QE erleichtert die geometrische Interpretation definierbarer Mengen, führt zu Modellvollständigkeit in vielen Fällen und ermöglicht Entscheidungsverfahren für Theorien der Real- und Algebra-Geometrie. In der Praxis wird QE in Real Algebraic Geometry durch CAD-Algorithmen umgesetzt.

Nicht alle Theorien besitzen QE; der Nachweis oder Gegenbeispiele hängt stark von der Sprache ab.