Notizen SAT, UNSAT, etc. (Update 2)

[eintopf]

Hallo,

da letztes Jahr eine wie ich finde ziemlich miese Aufgabe zu SAT, UNSAT, etc. kam (Diagramm in dem man die Inklusionen etc. einzeichnen musste), habe ich angefangen mir aufzuschreiben, was die Mengen bedeuten und was deren Komplemente und Inklusionen etc. sind.

Bin noch nicht fertig, aber wäre schön wenn ihr daran mitwirken könntet, werde es dann immer aktualisieren.

Viele Grüße!

EDIT:
19:21 - Datei aktuallisiert, Boolesche Algebra Regeln eingefügt, Distributivgesetz etc.

[Matthias Senker]

Hi,

im Prinzip finde ich die Liste praktisch. Gute Idee.
Aber meiner Meinung nach müssten FINSAT(FO) und FINUNSAT(FO) Komplemente voneinander sein. Demzufolge dürfte FINUNSAT(FO) dann auch nicht aufzählbar sein, weil ja FINSAT(FO) schon aufzählbar ist. Und wenn FINUNSAT(FO) nicht aufzählbar ist, dann ist auch FINVAL(FO) nicht aufzählbar. (steht auch im Skript: Seite 37 Über Satz 7.3 (Traktenbrot): "Die Menge der in endlichen Strukturen allgemeingültigen FO-Sätze ist nicht rekursiv aufzählbar.")

Und ich würde die Beschreibung von FINUNSAT(FO) ändern zu:
"Die Menge aller Formeln in FO, die in endlichen Strukturen unerfüllbar sind." oder aber "Die Menge aller Formeln in FO, die kein endliches Modell haben."
Wenn eine Formel nämlich ein Modell hat, ist sie auch erfüllbar! Die bisherige Beschreibung "Alle unerfüllbaren Formeln in FO mit endlichem Modell" ist also ein Widerspruch!

Und auch bei FINVAL(FO) würde ich schreiben:
"Die Menge aller Formeln in FO, die in endlichen Strukturen allgemeingültig sind."

[fscheepy]

Wie kommst du denn auf deine Aussagen über INF0, INF1 und INF2? Und was ist mit INFVAL(FO) - alle Formeln, die im Unendlichen allgemeingültig sind? Dazu habe ich bisher noch nirgends etwas gefunden

[eintopf]

Aber meiner Meinung nach müssten FINSAT(FO) und FINUNSAT(FO) Komplemente voneinander sein.

Das ist die zunächst "intuitive" Überlegung, aber ich habe mir folgendes überlegt:
Das Komplement von FINSAT(FO) enthält FINUNSAT, aber auch viel mehr, es enthält z.B. auch alle Formeln die in unendlichen Modellen erfüllbar sind etc. (allein schon weil FINSAT(FO) eine Teilmenge von SAT(FO))

Demzufolge dürfte FINUNSAT(FO) dann auch nicht aufzählbar sein, weil ja FINSAT(FO) schon aufzählbar ist.
Und wenn FINUNSAT(FO) nicht aufzählbar ist, dann ist auch FINVAL(FO) nicht aufzählbar. (steht auch im Skript: Seite 37 Über Satz 7.3 (Traktenbrot): "Die Menge der in endlichen Strukturen allgemeingültigen FO-Sätze ist nicht rekursiv aufzählbar.")

Bin mir grad nicht ganz sicher mit FINUNSAT, aber glaube du hast Recht. FINVAL ist auf keinen Fall rek. aufzählbar, da geb ich dir absolut Recht!

Und ich würde die Beschreibung von FINUNSAT(FO) ändern zu:
"Die Menge aller Formeln in FO, die in endlichen Strukturen unerfüllbar sind." oder aber "Die Menge aller Formeln in FO, die kein endliches Modell haben."
Wenn eine Formel nämlich ein Modell hat, ist sie auch erfüllbar! Die bisherige Beschreibung "Alle unerfüllbaren Formeln in FO mit endlichem Modell" ist also ein Widerspruch!

Und auch bei FINVAL(FO) würde ich schreiben:
"Die Menge aller Formeln in FO, die in endlichen Strukturen allgemeingültig sind."

Done, danke!

Wie kommst du denn auf deine Aussagen über INF0, INF1 und INF2? Und was ist mit INFVAL(FO) - alle Formeln, die im Unendlichen allgemeingültig sind? Dazu habe ich bisher noch nirgends etwas gefunden

Folie 112 (letzter Foliensatz, Seite 4)

[Ankou]

Das ist die zunächst "intuitive" Überlegung, aber ich habe mir folgendes überlegt:
Das Komplement von FINSAT(FO) enthält FINUNSAT, aber auch viel mehr, es enthält z.B. auch alle Formeln die in unendlichen Modellen erfüllbar sind etc. (allein schon weil FINSAT(FO) eine Teilmenge von SAT(FO))

mMn ist FINUNSAT(FO) die Menge aller Formeln ohne endliches Modell, wie Matthias es auch geschrieben hat, eine genaue Definition hab ich nicht gefunden.
Die Menge aller Formeln ohne endlichem Modell ist natürlich das Komplement zur Menge aller Formeln mit einem endlichen Modell, ich wüsste nicht wieso die Formeln, die nur im unendlichen erfüllbar sind nicht in FINUNSAT sein sollten?

[Matthias Senker]

Das Komplement von FINSAT(FO) enthält FINUNSAT, aber auch viel mehr, es enthält z.B. auch alle Formeln die in unendlichen Modellen erfüllbar sind etc. (allein schon weil FINSAT(FO) eine Teilmenge von SAT(FO))

Mir scheint, du hast FINSAT nicht ganz verstanden. Wenn eine Formel in FINSAT ist, dann hat sie ein endliches Modell, aber das heißt NICHT, dass sie keine unendlichen Modelle besitzen darf. Ebenso darf eine Formel in FINUNSAT sehr wohl unendliche Modelle besitzen, nur halt keine endlichen.
Daher kann eine Formel, wenn sie ein unendliches Modell besitzt, trotzdem in FINUNSAT sein! Daher bin ich mir eigentlich ziemlich sicher, dass FINSAT und FINUNSAT Komplemente voneinander sind (Eine 3. Meinung wäre vielleicht ganz hilfreich.) EDIT: Danke an Ankou für seine Meinung.

Bin mir grad nicht ganz sicher mit FINUNSAT, aber glaube du hast Recht. FINVAL ist auf keinen Fall rek. aufzählbar, da geb ich dir absolut Recht!

Wenn FINUNSAT rekursiv aufzählbar wäre, dann könnte man auch FINVAL aufzählen, indem man eine Formel, für die man wissen möchte, ob sie in FINVAL ist, einfach negiert und dann das Aufzählverfahren für FINUNSAT anwendet, denn eine Formel ist in endlichen Strukturen allgemeingültig, gdw. wenn ihre Negation in endlichen Strukturen unerfüllbar ist.

[eintopf]

Das Komplement von FINSAT(FO) enthält FINUNSAT, aber auch viel mehr, es enthält z.B. auch alle Formeln die in unendlichen Modellen erfüllbar sind etc. (allein schon weil FINSAT(FO) eine Teilmenge von SAT(FO))

Mir scheint, du hast FINSAT nicht ganz verstanden. Wenn eine Formel in FINSAT ist, dann hat sie ein endliches Modell, aber das heißt NICHT, dass sie keine unendlichen Modelle besitzen darf. Ebenso darf eine Formel in FINUNSAT sehr wohl unendliche Modelle besitzen, nur halt keine endlichen.
Daher kann eine Formel, wenn sie ein unendliches Modell besitzt, trotzdem in FINUNSAT sein! Daher bin ich mir eigentlich ziemlich sicher, dass FINSAT und FINUNSAT Komplemente voneinander sind (Eine 3. Meinung wäre vielleicht ganz hilfreich.) EDIT: Danke an Ankou für seine Meinung.

Bin mir grad nicht ganz sicher mit FINUNSAT, aber glaube du hast Recht. FINVAL ist auf keinen Fall rek. aufzählbar, da geb ich dir absolut Recht!

Wenn FINUNSAT rekursiv aufzählbar wäre, dann könnte man auch FINVAL aufzählen, indem man eine Formel, für die man wissen möchte, ob sie in FINVAL ist, einfach negiert und dann das Aufzählverfahren für FINUNSAT anwendet, denn eine Formel ist in endlichen Strukturen allgemeingültig, gdw. wenn ihre Negation in endlichen Strukturen unerfüllbar ist.

Ok, denke ich habe es nun verstanden, dazu stell ich gleich ein Update ein.
Man könnte doch sagen, dass FINUNSAT INF0(FO) enthällt oder?

[Matthias Senker]

Man könnte doch sagen, dass FINUNSAT INF0(FO) enthällt oder?

Nein, denn INF0 enthält zwar alle Formeln, die unendliche Modelle besitzen, verbietet den Formeln aber nicht, ebenso auch endliche Modelle zu besitzen. Und eine Formel mit endlichen Modellen ist ja nicht in FINUNSAT.
Aber wich würde sagen, dass FINUNSAT INF1 enthält. Denn jede Formel in INF1 ist nur in unendlichen Strukturen erfüllbar, besitzt also kein endliches Modell und ist daher in FINUNSAT.
Ich würde sogar sagen (korrigiert mich, wenn ich mich irre), dass FINUNSAT die Vereinigung von UNSAT und INF1 ist!

[eintopf]

Man könnte doch sagen, dass FINUNSAT INF0(FO) enthällt oder?

Nein, denn INF0 enthält zwar alle Formeln, die unendliche Modelle besitzen, verbietet den Formeln aber nicht, ebenso auch endliche Modelle zu besitzen. Und eine Formel mit endlichen Modellen ist ja nicht in FINUNSAT.
Aber wich würde sagen, dass FINUNSAT INF1 enthält. Denn jede Formel in INF1 ist nur in unendlichen Strukturen erfüllbar, besitzt also kein endliches Modell und ist daher in FINUNSAT.
Ich würde sogar sagen (korrigiert mich, wenn ich mich irre), dass FINUNSAT die Vereinigung von UNSAT und INF1 ist!

Das hört sich gut an.

[fscheepy]

Wie kommst du denn auf deine Aussagen über INF0, INF1 und INF2? Und was ist mit INFVAL(FO) - alle Formeln, die im Unendlichen allgemeingültig sind? Dazu habe ich bisher noch nirgends etwas gefunden

Folie 112 (letzter Foliensatz, Seite 4)

Vielleicht habe ich mich ungenau ausgedrückt: Ich frage mich, mit welcher Begründung du diese Teilmengen als unentscheidbar bezeichnet hast.

[kain]

Was noch nützlich wäre:

Zu jeder Menge eine Bsp. - Formel und desen Negat und in welcher Menge diese liegen würde...

[eintopf]

Was noch nützlich wäre:

Zu jeder Menge eine Bsp. - Formel und desen Negat und in welcher Menge diese liegen würde...

dafür hatte ich leider keine Zeit mehr, bzw. die Inklusionen hab ich so weit hingeschrieben wie ich mir sicher bin.