Herzlich willkommen!

Thema der heutigen Sitzung, Quantoren-Elimination.

Ich hatte schon mal angedeutet, Gültigkeit in logikerster Stufe ist zunächst einmal unentscheidbar.

Das machen wir hier nicht, aber es ist nicht fürchterlich schwer zu zeigen.

Mit anderen Worten, vollständiges automatisches Schließen ist im Allgemeinen nicht möglich.

Nun ist das aber auch im Allgemeinen gar nicht unbedingt das, was einen interessiert, sondern im Allgemeinen hat man eigentlich eine feste Theorie im Kopf, über der man arbeitet.

90% der Zeit ist das die klassische Mengentheorie.

Und solche Theorien können, wenn man Glück hat, durchaus entscheidbar sein.

Gut, was das überhaupt heißt, das halten wir mal kurz fest.

Also zunächst mal kurz der Begriff der Theorie. Was ist eine Theorie?

Typischer Buchstabe T.

Also es soll irgendwie kalografisch sein, deswegen mache ich so einen Schnörkel dran.

Das ist ein Paar.

Sigma, Phi.

Bei ist Sigma eine Signatur.

Und Groß Phi ist eine Menge von Sigmasetzen, also von Formeln ohne freie Variablen, wo also im Zweifel für alles vorne in Allquantum steht zum Beispiel.

Das ist eine Theorie, davon kennen wir mittlerweile schon etliche Beispiele. Wir haben den Begriff auch zumindest auf den Zettel vielleicht schon mal verwendet.

Also die Piano-Axiome der natürlichen Zahlen bilden eine Theorie, wo eben die Signatur eigentlich nur aus Nullsuccessor und zwei arithmetischen Operationen besteht typischerweise.

Und die Sätze, das sind halt die Piano-Axiome, die also besagen Null ist kein Nachfolger und die Nachfolgerfunktion ist injektiv und für jede mögliche Instanzformel habe ich ein Induktionsschema.

Also in dem Falle eine unendliche Menge von Sätzen sogar oder eben die übliche ZF-Mengenlehre. Auch das wäre im Übrigen eine unendliche Menge von Aktionen, wenn man genau hinschaut.

So, das wäre die Theorie.

Dann haben wir einen Begriff vom Modell dieser Theorie, das ist auch nicht weiter schwer.

So ein Ding soll natürlich ein Sigma-Modell sein, also die Symbole in der Signatur auch tatsächlich interpretieren.

Sagen wir Minden ist M.

Und es soll natürlich alle Aktionen der Theorie erfüllen. Also ein Modell der Signatur, das alle Aktionen erfüllt ist ein Modell der Theorie.

Und die entscheidende Frage, die wir uns dann stellen ist folgt irgendein Satz, den wir uns ausdenken aus dieser Theorie oder nicht.

Wenn das entscheidbar ist, dann sagen wir T sei entscheidbar.

Gut, das ist also jetzt das formale Grundgerüst. Wir fragen uns jetzt also, für welche Theorien bekommen wir es womöglich hin, Folgerungen aus der Theorie eben doch noch zu entscheiden.

So, es gibt nur wenige Theorien, für die das möglich ist.

Zum Beispiel die Peano-Rithmetik ist nicht entscheidbar.

Und für die meisten Signaturen, gut, da muss man sich auf den Detail angucken, ist auch die Lehretheorie nicht entscheidbar, also keine Aktionen sind nur auch zu wenige.

Ein berühmtes Beispiel einer entscheidbaren Theorie ist nun ausgerechnet die Theorie der reellen Zahlen.

Also die Theorie der reellen Zahlen hat einen Entscheidungsalgorithmus, der ist fürchterlich komplex, also er läuft in nicht elementarer Zeit, wie man so schön sagt.

Das heißt, seine Laufzeit wächst schneller als jeder exponentielle Turm.

Aber immerhin entscheidbar ist es und das ist auch ein berühmtes Resultat von berühmten, nicht von berühmten Leuten, sondern nur von einem berühmten Leute, das ist von Tarski.

Das ist jetzt ein Resultat, das verwendet auch das gleiche Schema, wie das, was wir jetzt in unserem Beispiel in der heutigen Sitzung verwenden, das heißt, es verwendet Quantoren-Elimination.

Das ist aber ein Papier mit 50 Seiten, das schaffe ich also nicht in einer Sitzung.

Ich will auch nicht behaupten, ich hätte es zu irgendeinem Zeitpunkt mal vollständig verstanden.

Aber das ist andererseits ein implementierter Algorithmus. Trotz dieser katastrophalen Komplexität gibt es also implementierte Systeme, die also Aussagen über reelle Zahlen per Quantoren-Elimination entscheiden.

Es mag einen so ein bisschen überraschen, irgendwie das ausgerechnet, sowas, was man so als schwierig im Kopf hat, wie die reellen Zahlenentscheidbare Theorie hat.

Der Punkt dabei ist zum Teil der, dass das eben wohlgemerkt die erststufige Theorie der reellen Zahlen ist. Wenn man über die reellen Zahlen spricht, spricht man ja normalerweise in einer höherstufigen Sprache über die reellen Zahlen.

Zum Beispiel schon das Vollständigkeitsaktion der reellen Zahlen. Jede beschränkte nicht leere Teilmenge hat ein Supremum.

Schon das ist ja in logikerster Stufe gar nicht ausdrückbar. Das heißt, man kann nur vergleichsweise langweilige Aussagen über reelle Zahlen überhaupt kodieren.

Zum Beispiel, wenn ich mal die Quantoren mir ganz wegdenke oder nur Existenzquantoren zulasse, kann ich sowas entscheiden wie Lösbarkeit von Polynomengleichungen.

Eine Polynomengleichung ist einfach sofort hingeschrieben, eine existenzielle Formel in logikerster Stufe über den reellen Zahlen.

Also, Lösbarkeit von solchen Sachen kann ich entscheiden, wohlgemerkt egal, wie schlimm der Grad des Polynoms ist.

Was dann auch wieder so überraschend ist, wie entscheide ich, ob ein Polynom im dritten Grad eine Nullstelle hat oder nicht.

Naja, ich gucke, ob es an einer Stelle über Null ist und an einer unter Null und wenn es an einer über Null und an einer unter Null ist, dann ist es wohl lösbar, weil es irgendwann zwischendurch die Null überqueren muss.

Also, das ist alles nicht so geheimnisvoll, wie es erstmal klingt, aber es ist trotzdem relativ kompliziert tatsächlich zu zeigen.

Schreiben wir den Namen mal dazu.