Logik erster Ordnung Arity definiert die Dekidabilität?

Question

Ich habe gelesen, dass die Logik erster Ordnung im Allgemeinen unentscheidbar ist, und das könnte nur bei der Arbeit mit unären Operatoren entscheidbar sein. (Ich denke, das ist die Propositionslogik, korrigieren Sie mich, wenn ich falsch liege)

Die Frage ist Warum führt Arity zu unentscheidbaren Problemen?

Ich würde gerne ein Referenzmaterial oder zumindest etwas einfach sehen Beispiel davon, um in dieser Passage von Unary nach Nary zu denken und warum es zu unentschlossenen Problemen führt.

Answer 1

Logik mit Unary Prädikate (nicht Operatoren), heißt monadisch. Das, was genannt wird Aussagen Logik hat nur Nullary Prädikate, dh Konstanten true und false, und keine Quantifizierer.

Das Unentschlossenheit der Prädikatlogik folgt, weil die Prädikatlogik (mit mindestens einem binären Prädikat) stark genug ist, um Beschreiben Sie, wie eine Turing -Maschine funktioniert, und so können wir in der Logik ausreichend komplizierte Aussagen über Turing -Maschinen ausdrücken, um Unentschieden zu erhalten. Im Gegensatz dazu können wir in der monadischen Logik, in der wir nur unäre Prädikate haben, die Arbeit einer Turing -Maschine nicht beschreiben. Ich bin hier absichtlich vage, um eine Idee zu geben, ohne mich in technischen Weise festzuhalten.

Answer 2

Wie Raphael in einem Kommentar betonte, fragen Sie wahrscheinlich nach der Dekidabilität des klassischen Entscheidungsproblems für Fragmente der Logik erster Ordnung mit unären Prädikaten.

Die Suche nach syntaktisch eingeschränkten Fragmenten der Logik erster Ordnung, bei denen die Validität von Formeln entscheidbar ist, war seit über 100 Jahren ein aktives Forschungsfeld. Es wurde sehr früh verstanden, dass es die Abhängigkeiten zwischen Variablen sind, die das Entscheidungsproblem erschweren. Und Abhängigkeiten werden am besten ausgedrückt, wenn zwei Variablen innerhalb der Argumente eines Prädikats auftreten. Daher sind binäre Prädikate oder funktionelle Symbole (falls Sie funktionelle Symbole zulassen) für die Unentschlossenheit von wesentlicher Bedeutung.

Es war Löwenheim, der 1915 ein Entscheidungsverfahren für Logik erster Ordnung mit unären Prädikaten gab. Wenn Sie interessiert sind, finden Sie möglicherweise faszinierende Expositionspapier mit dem Titel "Über das klassische Entscheidungsproblem"Geschrieben von Yuri Gurevich in Form eines Dialogs von zwei fiktiven Charakteren. Das Papier wurde erstmals im Bulletin of Eatcs veröffentlicht.

Das Papier stellt nicht nur das Problem ein, sondern erklärt, wie sich die Suche entwickelt hat, um eine vollständige Klassifizierung von lichtbaren und unentscheidbaren Fragmenten hinsichtlich der Quantifiziererpräfixe zu finden.