Prädikatenlogik: Unentscheidbarkeit trotz vollständigem Kalkül?

Neue Frage »

auxilium Auf diesen Beitrag antworten »
Prädikatenlogik: Unentscheidbarkeit trotz vollständigem Kalkül?
Hallo zusammen,

Ich bin im Skript meines Profs auf folgende Aussage gestoßen, die ich nicht ganz nachvollziehen kann:

Auf der einen Seite heißt es:

Dass es für die Prädikatenlogik einen vollständigen und korrekten Kalkül gibt, d.h.

vollständig: wenn etwas semantisch aus einer Formelmenge folgt, dan folgt es auch syntaktisch durch das Kalkül.
korrekt: wenn etwas syntaktisch folgt, dann folgt es auch semantisch.

Wobei semantische Folgerung bedeutet, dass für jede Interpretation die Folgerung erfüllt ist.

Vgl auch den Gödelschen VollständigkeitssatzWikipedia

Gleichzeitig heißt es dann auch:
Für die Prädikatenlogik gibt es kein berechenbares Entscheidungsverfahren, das entscheidet, ob eine Formel eine Folgerung aus einer Formelmenge ist oder nicht.


Jetzt frage ich mich, wie kann ich das vereinen?

Also was ich gesehen habe, ist dass das Resolutionskalkül in der Prädikatenlogik unendlich abgeleitet werden kann, man kann also dann keine klare Aussage machen.

Ich kann daher durchaus die Korrektheit und die Unentscheidbarkeit vereinen: Also wenn was gefunden wird, dann ist es korrekt.

Aber wie die Vollständigkeit und die Unentscheidbarkeit vereinen:
Wenn etwas semantisch folgt, muss es doch dann auch durch die Resolution syntaktisch gefolgert werden können.
Wenn aber doch ein Beweis unendlich lange dauert, dann ist das doch nicht mehr gewährleistet?

Oder aus welchem Grund darf man unendlich lange nicht mit unvollständigkeit gleichsetzen?


Wäre cool, wenn da jemand eine Idee hätte
Neue Frage »
Antworten »



Verwandte Themen

Die Beliebtesten »
Die Größten »
Die Neuesten »