Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Ontos Web: r.e. von Gültigkeit und Erfülbarkeit in FOL
In der Vorlesung wurde ja behandelt, dass FOL nicht entscheidbar ist.
Mir sind ein paar Sachen noch nicht klar geworden.
z.B. wurde gesagt, Gültigkeit ist co r.e. Da man alle bekannten Beweise
nehmen kann und sich dann die letzt Formel ausgeben lassen kann.
Also hat man doch eine Menge von gültigen Formeln, die in jedem Modell
gelten. Bedeutet das co. r.e. dass alle ungültigen Formeln rekursiv aufzählbar sind?
Aber wie wird das gemacht? Was ist der Algorithmus?
Dasselbe bei Erfüllbarkeit in FOL. Heißt das, wenn ich eine erfüllbare Formel habe, finde
ich eine Belegung die mir diese Formel erfüllen wird? Oder kann ich alle Formeln aufzählen, die
mir dieses Modell erfüllen?
Und ein paar Kommentare — teils Übersetzungen aus dem Wikipedia-Artikel:
- Ich bin mir nie sicher, was mit Gültigkeit gemeint ist (Allgemeingültigkeit oder Erfüllbarkeit?)
- Allgemeingültigkeit ist rekursiv aufzählbar, da man alle Beweise aufzählen kann (Nicht nur die “bekannten” — was auch immer “bekannt” bedeuten mag). Allgemeingültigkeit heißt: eine Konsequenz aus den Axiomen. Der Algorithmus hat keinen Namen, da er nur besteht aus: Beginne bei den Axiomen und liste alle darauf aufbauenden Beweise (und deren letzte Formel) auf. Das ist effektiv eine Breitensuche, wobei die Knoten die Formeln sind und die ausgehenden Kanten die auf die Formel passenden Schlüsse (= logische Umformungen) sind. (Es wird nur komplizierter, wenn ein Knoten unendlich viele ausgehende Kanten hat, d.h. wenn ich auf eine Formel unendlich viele Schlüsse passen. Das kann man aber durch geschicktes Parallelisieren auch hinbekommen. Das nackte FOL an sich ist jedoch “finitely axiomatizable” ).
- Dem zu Folge muss die Erfüllbarkeit Co-Rekursiv aufzählbar sein, d.h. das negierte Problem (“Unerfüllbarkeit”) rekursiv aufzählbar: eine Formel φ ist nämlich genau dann Unerfüllbar (es gibt kein Model in dem φ gilt), wenn in allen Modellen ¬φ gilt. Mit anderen Worten: ¬φ ist allgemeingültig. Und Allgemeingültigkeit ist ja rekursiv-aufzählbar. D.h. wenn du den Erfüllbarkeits-Co-R.E.-Algorithmus anwirst, dann bekommst du im Falle der Unerfüllbarkeit nach endlicher einen Gegenbeweis (einen Beweis von ¬φ) und im Falle der Erfüllbarkeit wartest du ewig auf eine Antwort.
Ich habe das jetzt so verstanden.
Eine Formel ist gültig, wenn sie unabhängig vom Modell, also für alle Modelle gilt.
Diese Menge an Formeln kann man durch Beweise (formale Deduktion) ermitteln. Damit sind diese Formeln
r.e. das Komplement aber nicht.
Bei Erfüllbarkeit von FOL geht es darum, dass eine Formel für mindestens ein Modell erfüllt ist. Man kann diese nicht
rekursiv aufzählen, da es aber unendliche Modelle gibt, muss man ewig warten. Daher ist das nicht r.e. sondern nur ko-rekursiv-aufzählbar.
Heißt: Nimm alle endlichen Modelle und setze ein, solange bis ein Modell nicht erfüllt ist.
Ist das korrekt?
edit:
Danke für deine Erklärung errnosys.
Genau. (bzw. genauer: „Damit sind diese Formeln r.e., das Komplement aber erstmal nicht zwingend“.)
Ich verstehe hier den zweiten Satz von dir grammatikalisch nicht ganz. Also man kann sich jetzt streiten, was das „man muss ewig warten“ genau bedeutet. Ein „für eine Antwort muss man garantiert immer ewig warten“ kann man direkter sagen: „es gibt kein Programm, das die richtige Antwort liefert“.
Achtung: „nicht r.e. sondern nur ko-rekursiv-aufzählbar“ klingt so als wäre „ko-rekursiv-aufzählbar“ eine Abschwächung von „r.e.“ — das ist es aber nicht! R.e. impliziert nämlich nicht ko-r.e.!
Was soll das tun? Das ist auf jeden Fall nicht der Algorithmus der zur co-r.e.-Eigenschaft von Erfüllbarkeit gehört.
Wenn ich dich richtig verstehe, geht es hier allgemein um „Erfüllbarkeit“ und „Allgemeingültigkeit“ und nicht um die Abwandlungen um die es auf der Aufgabe auf dem 1. Übungsblatt geht.
Ja ich habe da teilweise was durcheinander gebracht. Danke nochmal für deine Erläuterungen 