Ja, herzlich willkommen zur letzten Sitzung des Semesters.

Ja, wir haben ein bisschen was vor heute.

Die endgültigen Resultate, das Eingemachte gewissermaßen, das kommt alles heute.

Jawohl.

Ja, wir hatten das letzte Mal schon angefangen.

Das war Quantoren-Elimination in der Theorie der dichten Ordnung.

Ich schreibe jetzt die Axiome nicht nochmal von vorne an, sondern erinnere nur nochmal,

wie das intuitiv aussah.

Es ging genauer gesagt um lineare Ordnungen, also wo man sich genau das vorstellen darf,

was man sich sonst unberechtigterweise vorstellt, nämlich dass also in einer geordneten Menge

die Elemente tatsächlich so auf einer Linie liegen, insbesondere also immer von zwei Elementen

immer entweder eins größer ist oder das andere, wenn sie nicht zufällig gerade gleich sind.

Und die Dichte der Ordnung, genauer gesagt sind es dichte Ordnungen ohne Endpunkte, die

kann man sich folgendermaßen visualisieren, wenn ich jetzt zwei Punkte habe auf meiner

Ordnung, die nicht gleich sind, sprich der eine muss dann größer sein als der andere,

so rum oder so rum, dann finde ich einen dazwischen.

Das ist das eine, das ist die Dichte und die Ordnung ist endpunktfrei, das heißt ich finde

nicht nur dazwischen noch einen, sondern ich finde auch hier rechts noch einen und ich

finde hier links immer noch einen.

So, das sind also dichte endpunktfreie Ordnungen.

Zum Beispiel Q mit der üblichen dichten Ordnung, mit der üblichen strikten Ordnung ist eine

dichte endpunktfreie Ordnung oder genauso die reellen Zahlen mit der üblichen strikten

Ordnung, nicht aber zum Beispiel die ganzen Zahlen mit der üblichen strikten Ordnung,

nicht denn bei den ganzen Zahlen, da hätte ich hier eins und hier zwei und ich kann nichts

dazwischen quetschen an ganzen Zahlen, da wäre also die Dichte verletzt.

Ebenso kein Beispiel sind die nicht negativen reellen Zahlen, die wären auch zwar eine dichte

Ordnung, aber sie haben eben offensichtlich einen Endpunkt, das fängt hier bei Null an

und geht nach rechts, das ist verboten, da gibt es also so ein Element Null links, von

dem es nichts gibt, das wollen wir nicht haben.

Wohl aber die positiven, echt positiven reellen Zahlen, die wären auch ein Beispiel einer

dichten linearen Ordnung ohne Endpunkte, in diesem Falle ist eben der Endpunkt, die Null

gerade rausgenommen und jede Zahl, die echt positiv ist und wenn es auch nur ein Millionstel

ist oder so, ja die ist dann immer noch kein Endpunkt, weil ich links davon immer noch

etwas kleineres finde, zum Beispiel eben die Hälfte der Zahlen.

Ja und wir interessieren uns jetzt eben für Quantoren-Elimination, das hatte ich letztes

Mal formal definiert, will ich jetzt hier nicht wiederholen, es bedeutet das, was man

denkt, was es bedeutet, nämlich ich möchte eine Prozedur haben, die mir eine beliebige

Formel überführt in eine, die keine Quantoren mehr enthält, natürlich nicht äquivalent,

das kann man nicht hoffen, ja aber erfüllbarkeitsäquivalent.

So, es gibt da in der Quantoren-Elimination wenig allgemeine Resultate, was damit korreliert,

dass die meisten Theorien keine Quantoren-Elimination zulassen, aber einige wichtige tun es eben

doch, die tun es aber generell aus ziemlich verschiedenen Gründen, aber ein allgemeines

Kriterium, mit dem man sich ein bisschen Arbeit in den konkreten Beispielen sparen kann,

macht es doch und zwar, stellen wir uns mal vor, wir hätten eine Formel dieser Form hier,

die ist quantifiziert am Anfang und dann eine Konjunktion von α1 bis αn, wobei diese

αi alle literale sein sollen, das heißt, sie sind Gleichungen oder Prädikaten, Anwendungen

oder Negationen von solchen Dingen, also wenn ich für solche sehr einfachen Formeln, so

ich sage das jetzt mal salopp, wenn für solche einfachen Formeln der eine Quantor, den sie

halt enthalten, eliminierbar ist, unter meiner Theorie T, also nicht schlechthin, sondern

nur unter der Annahme meiner Aktion, meiner Theorie, zum Beispiel unter der Annahme der