SAT(FO) nicht aufzählbar, aber FINSAT(FO)?

pinanta
Neuling
Neuling
Beiträge: 4
Registriert: 30. Jul 2017 10:37

SAT(FO) nicht aufzählbar, aber FINSAT(FO)?

Beitrag von pinanta » 13. Aug 2017 21:14

Hey, ich stehe gerade etwas auf dem Schlauch...

Weshalb das Erfüllbarkeitsproblem der Logik erster Stufe unentscheidbar ist, leuchtet mit denke ein:
Es gibt grundsätzlich unendlich viele S-Strukturen, weshalb es nicht möglich ist systematisch für beliebige AL-Formeln zu bestimmen, ob diese erfüllbar sind oder nicht. Man müsste nämlich eventuell unendlich viele Strukturen als Modell testen, was algorithmisch nicht umsetzbar ist. Allerdings besteht die Möglichkeit durch die Reduktion des Problems auf SAT(FO) via Satz von Herbrand bzw. dem Beweis das die Herbrandexpansion (die Menge aller Grundinstanzen der jeweiligen Formel) unerfüllbar ist. Falls die Formel unerfüllbar ist, hält dieses Verfahren an, wenn nicht, dann nicht. Somit ist UNSAT(FO) rekursiv aufzählbar, aber SAT(FO) unentscheidbar.
Nun steht im Skript von M.Otto unter Abschnitt 7.2 'Die Sätze von Traktenbrot und Tarski' das FINSAT(FO) rekursiv aufzählbar ist. Als Begründung wird geliefert, dass man systematisch alle endlichen S-Strukturen A der Reihe nach (mit wachsender Größe) generieren kann und jeweils 'A ist Modell von phi' testen kann, bis man ggf. Erfolg hat, was einleuchtend klingt.
Allerdings stell ich mir dann die Frage, weshalb UNFINSAT(FO), also die Frage ob eine beliebige FO-Formel nicht durch ein endliches Modell erfüllbar ist, nicht rekursiv aufzählbar ist?

Liegt es daran, dass wir hier den Satz von Herbrand nicht anwenden können, da jedes (mir bekannte) Herbrand-Modell unendlich ist, und somit nicht als Modell infrage kommt?

Zurück zu „Archiv“