Elimination der Quantoren - Detailseite

Sei T eine Theorie in der (quantorenlogischen) Sprache L; T erlaubt Quantorenelimination gdw
für jede Formel A aus L gibt es eine quantorenfreie
Formel B aus L so daß T |- A B.

Quantoren sind irgendwie schwieriger als Junktoren; deshalb hat man es beim Beweisen am liebsten nicht mit jenen zu tun. Beim axiomatischen Beweisen sind sie schwer zu eliminieren; aber ihre Eliminierbarkeit bringt häufig erwünschte Eigenschaften für T mit sich: wie die Entscheidbarkeit und Vollständigkeit von T. Diese sollten gerade auch für empirische Theorien Desiderata sein.

Dieses HS ist eine Einführung in das Thema Quantorenelimination. Ich möchte die klassischen Beispiele -- wie Theorien nur mit "=", Presburger Arithmetik, Theorien der reellen Zahlen -- behandeln. Es wäre schön, wenn uns am Ende des HS Eliminationsbeweise für diese Theorien bekannt wären, die so elegant sind, daß man sie ohne große Lücken hinschreiben und doch verstehen kann.