Wie ist die Logik erster Ordnung vollständig, aber nicht entscheidbar?

NEIN , Vollständigkeit der Logik erster Ordnung impliziert keine Entscheidbarkeit.

Sie mischen zwei Verwendungen der Vollständigkeit .

Die erste Verwendung betrifft die Vollständigkeit von "Standard"-Beweissystemen für die Logik erster Ordnung .

Dies ist der Vollständigkeitssatz von Gödel , der besagt:

Der Vollständigkeitssatz besagt, dass wenn eine Formel logisch gültig ist, es eine endliche Deduktion (einen formalen Beweis) der Formel gibt.

Der Vollständigkeitssatz von Gödel besagt, dass ein deduktives System des Prädikatenkalküls erster Ordnung "vollständig" in dem Sinne ist, dass keine zusätzlichen Inferenzregeln erforderlich sind, um alle logisch gültigen Formeln zu beweisen. Ein Gegenteil von Vollständigkeit ist Korrektheit, die Tatsache, dass nur logisch gültige Formeln im deduktiven System beweisbar sind. Zusammen mit der Solidität (deren Überprüfung leicht ist) impliziert dieser Satz, dass eine Formel genau dann logisch gültig ist, wenn sie die Schlussfolgerung einer formalen Deduktion ist.

Es lässt sich leicht auf die Beziehung logischer Konsequenz zwischen einer Menge Γ von Formeln erster Ordnung und einer Formel φ in Symbolen verallgemeinern:

Γ ⊨ φ .

In diesem Fall haben wir das:

Γ ⊨ φ genau dann, wenn Γ ⊢ φ (dh φ ist aus Γ beweisbar ).

Der Einfachheit halber betrachten wir den Fall, dass Γ die leere Menge ist; In diesem Fall haben wir die vorherige Version:

⊨ φ (dh φ ist gültig ) gdw ⊢ φ (dh φ ist beweisbar ).

Ihr Irrtum betrifft die "Grundeigenschaft" der Gültigkeit :

es ist nicht wahr, dass wenn φ nicht gültig ist , dann ¬φ gültig ist .

Betrachten Sie die Formel:

∃x∃y ¬(x = y).

Es bedeutet: „Es gibt mindestens zwei Dinge x und y, so dass sie nicht gleich sind“. Diese Formel gilt nicht in einem Universum mit nur einem einzigen Element. Daher ist es nicht gültig (Gültigkeit bedeutet: wahr in jedem Universum).

Seine Negation ist:

¬∃x∃y ¬(x = y)

was beläuft sich auf:

∀x∀y (x = y).

Es bedeutet „alle Dinge sind gleich“. Auch diese Formel ist nicht gültig, da sie in einem Universum mit mehr als einem Element nicht zutrifft.

Vergleichen Sie mit der Aussagenlogik , wo eine gültige Formel als Tautologie bezeichnet wird (die Negation einer Tautologie wird als Widerspruch bezeichnet : eine Formel, die immer falsch ist).

In diesem Fall haben wir ein Entscheidungsverfahren : den Wahrheitstabellen- Algorithmus (er ist höchst "ineffizient", aber er funktioniert ...).

Wenden Sie es auf eine Formel A an : Wenn Sie in ihrer Spalte alle "T" haben, dann ist die Formel eine Tautologie .

Auch in diesem Fall gibt es einen Vollständigkeitssatz: Wenn A eine Tautologie ist, finden wir einen Beweis dafür in den "üblichen" Beweissystemen, wie der natürlichen Deduktion .

Aber beachten Sie, dass es auch in diesem Fall nicht gilt, dass für eine Formel A , wie auch immer, A eine Tautologie oder ¬A ist.

Die Formel :

p V q

ist weder eine Tautologie noch ein Widerspruch.

Die zweite Bedeutung von Vollständigkeit bezieht sich auf Theorien und ist der Schlüssel zu den berühmten Gödelschen Unvollständigkeitssätzen , die Folgendes besagen:

Der erste Unvollständigkeitssatz besagt, dass kein konsistentes System von Axiomen, dessen Sätze durch ein "effektives Verfahren" (z. B. ein Computerprogramm, aber es könnte jede Art von Algorithmus sein können) aufgelistet werden kann, alle Wahrheiten über die Beziehungen des Natürlichen beweisen kann Zahlen (Arithmetik). Für ein solches System wird es immer Aussagen über die natürlichen Zahlen geben, die wahr, aber innerhalb des Systems nicht beweisbar sind.

Dieses (negative) Ergebnis betrifft einen weiteren Aspekt der intuitiven "Vollständigkeit" (im Sinne von Angemessenheit): Für eine mathematische Theorie wie Arithmetik oder Mengenlehre ist es eine vernünftige Erwartung, dass die Axiome (formalisiert mit Logik erster Ordnung) in der Lage sind um die ganze mathematische Wahrheit zu "erfassen", die in dieser Theorie ausgedrückt werden kann.

Für die meisten "wenig komplexen" mathematischen Theorien ist dies nicht möglich.

Hinzugefügt

Entscheidbarkeit ist mit der zweiten Bedeutung von Vollständigkeit verbunden .

Wenn eine Theorie T vollständig ist (im zweiten Sinne plus eine zweite "technische" Bedingung : effektiv axiomatisiert), dh T ist in der Lage, alle wahren Sätze φ zu beweisen, die in der Sprache der Theorie ausdrückbar sind, aufgrund der Tatsache, dass entweder φ ist wahr in T oder ¬φ in T wahr ist , dann ist T entscheidbar .

[ Anmerkung . Wenn wir die beiden obigen Formeln betrachten und ihre Bedeutung in Bezug auf die einzelne arithmetische Interpretation betrachten, haben wir jetzt, dass eine von ihnen wahr und die andere falsch ist. Aufgrund der Tatsache, dass es unendlich viele natürliche Zahlen gibt (also mehr als eine), haben wir, dass die Formel : ∃x∃y ¬(x = y) in der arithmetischen Interpretation (betrachte zB 1 und 2 ) wahr ist, während seine Verneinung ∀x∀y (x = y) ist offensichtlich falsch (nicht alle Zahlen sind gleich)].

Um auf die Entscheidbarkeit zurückzukommen, warum ist eine vollständige Theorie so?

Genau weil das in Ihrer Frage beschriebene "Verfahren" funktioniert: Beginnen Sie mit dem Beweis von Theoremen in T . Wenn φ nach einer endlichen Zeit wahr ist, werden Sie den Beweis dafür finden; wenn nicht, dann ist ¬φ wahr und Sie werden einen Beweis dafür finden.

Wie bereits gesagt, funktioniert dieses "Verfahren" nicht für die Gültigkeit , da es nicht wahr ist, dass entweder eine Formel oder ihre Verneinung gültig sind.

Gödels Unvollständigkeitssatz beweist, dass formalisierte Theorien, die genügend "Fähigkeit" zum Ausdrücken arithmetischer Tatsachen haben, im zweiten Sinne nicht vollständig sind: Sie sind nicht in der Lage, alle wahren arithmetischen Tatsachen "zu erfassen".

Somit sind die obigen Theorien nicht entscheidbar.

Was ist die "Verbindung" zwischen den beiden Verwendungen von Vollständigkeit ?

Betrachten Sie eine Theorie erster Ordnung T , die die Sprache der Arithmetik enthält.

Die "zugrundeliegende" Logik ist vollständig (erster Sinn): dh sie ist in der Lage, alle logischen Konsequenzen der Axiome der Theorie T zu beweisen .

Aber die Theorie T ist unvollständig (nach Gödels Unvollständigkeitssatz), dh es gibt einen wahren arithmetischen Satz φ , der nicht aus den Axiomen von T beweisbar ist .

Na und ?

Es ist kein Widerspruch. Betrachten Sie die Def der logischen Konsequenz, die auf T angewendet wird :

T ⊨ φ genau dann , wenn φ in jedem Modell von T wahr ist .

Da φ im „beabsichtigten Modell“ der Arithmetik (den „üblichen“ Zahlen) wahr ist, schließen wir daraus, dass es in einigen anderen Modellen nicht wahr ist [siehe Kommentar von Francis Davey]: Es gibt Nicht-Standard-Modelle der Arithmetik .

Insofern ist es keine logische Konsequenz der Axiome von T und das ist der Grund, warum seine Unbeweisbarkeit in T nicht mit der Vollständigkeit der zugrunde liegenden Logik kollidiert.

Da Taylor Hornby die Definition von Vollständigkeit bereits selbst korrigiert hat (dank Mauro ALLEGRANZAs erster Definition), möchte ich nur darauf hinweisen, wo genau seine Argumentation in die Irre geht.

Warum impliziert Vollständigkeit keine Entscheidbarkeit für die Logik erster Ordnung? Taylor Hornby begründet dies wie folgt:

Warum geht das nicht: Alle Strings x aufzählen. Wenn x die gültige Ableitung von B von A kodiert, akzeptiere. Wenn x die gültige Ableitung von ~B von A kodiert, verwerfe.

Der Vollständigkeit halber stolpert dieser Prozess schließlich über ein x, das entweder ein Beweis von B oder ~B von A ist. Wenn B, dann impliziert A B in allen Interpretationen. Wenn ~B, dann ist es nicht so, dass A in allen Interpretationen B impliziert. Also ist FOL entscheidbar.

Was hier falsch ist, ist der Satz:

Der Vollständigkeit halber stolpert dieser Prozess schließlich über ein x, das entweder ein Beweis von B oder ~B von A ist.

Vollständigkeit bedeutet per Definition: „Wenn B logisch involviert ist, dann ist B beweisbar.“ Es ist eine bedingte Aussage. Nun wissen wir im Allgemeinen im Voraus nicht, ob ein gegebenes B logisch impliziert ist oder nicht. Wir wissen also nicht, ob es einen Beweis von B gibt oder nicht. Was also wirklich passiert, ist Folgendes:

Irgendwann wird dieser Prozess über ein x stolpern, das entweder ein Beweis für B oder ~B von A ist, ODER dieser Prozess wird für immer weiterlaufen.

Das heißt, dieser Algorithmus bestimmt nicht immer, ob B logisch impliziert ist (oder äquivalent, ob B dank der Eigenschaften der Korrektheit und Vollständigkeit von FOL beweisbar ist). Wenn entweder B oder ~B beweisbar ist, werden wir schließlich seinen Beweis finden. Aber wenn weder B noch ~B beweisbar ist, können wir nie sagen, ob es keinen Beweis gibt oder ob wir einfach weiter suchen müssen. Dieser Algorithmus gibt uns also keine Antwort für jedes B, aber wir können fragen, ob es einen besseren Algorithmus gibt, der uns eine Antwort für jedes B gibt. Turings Halteproblem wird verwendet, um zu zeigen, dass es keinen Algorithmus gibt, um zu bestimmen, ob B eine ist logisch dazugehört.

Die Logik erster Ordnung ist vollständig, weil alle Folgerungen beweisbar sind, aber unentscheidbar, weil es keinen Algorithmus gibt, um zu entscheiden, ob ein gegebener Satz logisch Folgerungen hat oder nicht.

Den Maschinen sind, egal wie clever sie konstruiert sind, höchste Grenzen gesetzt. 1936 bewies Turing mathematisch, dass es niemals einen allgemeinen Algorithmus zur Lösung des Problems für alle möglichen Programm-Eingabe-Paare geben kann. Das heißt, kein Algorithmus kann so geschrieben werden, dass er für ein gegebenes Programm-Eingabe-Paar immer korrekt entscheidet, ob das Programm anhält oder nicht. In der Informatik wird dies als Halteproblem bezeichnet. Turing hat bewiesen, dass jeder Algorithmus dazu gebracht werden kann, sich selbst zu widersprechen und daher nicht richtig entscheiden kann. Zur Veranschaulichung können wir ein „pathologisches“ Programm-Eingabe-Paar verwenden, das darauf ausgelegt ist, das Gegenteil von dem zu tun, was der Algorithmus vorhersagt.

Turings Beweis impliziert, dass es unmöglich ist vorherzusagen, ob die Turing-Maschine, die programmiert wurde, bestimmte mathematische Probleme anzugehen, jemals erfolgreich sein und zum Stillstand kommen oder für immer weiterlaufen wird. Eigentlich gilt für den Menschen eine äquivalente Endgrenze: Es ist auch unmöglich vorherzusagen, ob es Mathematikern jemals gelingen wird, dieselben Probleme zu lösen.

Die entscheidende Frage betrifft Vollständigkeit und Entscheidbarkeit (ob ein Theorem entweder wahr oder falsch ist, aber nicht beides), was dem Halteproblem in der Informatik entspricht. Unvollständigkeit öffnet die Tür zur Möglichkeit der Unentscheidbarkeit. Ein erfolgreicher Beweis eines bestimmten Problems impliziert, dass es in der Theorie (oder dem System), in dem es formuliert wird, nicht unentscheidbar ist. Aber ein solcher Beweis impliziert nicht, dass die Theorie selbst vollständig oder entscheidbar ist. Es kann andere Probleme in der Theorie geben, die unentscheidbar sind, in diesem Fall gibt es keine Lösung. In einer unvollständigen Theorie gibt es zum Beispiel Theoreme oder Gleichungen, die intuitiv wahr erscheinen, aber nicht beweisbar sind. Daher ist es unmöglich vorherzusagen, ob ein bestimmtes Problem, das in einer unvollständigen Theorie formuliert ist, jemals gelöst werden kann.

Ich bin mir ziemlich sicher, dass das richtig ist, aber nicht 100% sicher:

Eine mögliche Verwirrung besteht darin, dass wir denken, wir sprächen über ein einziges Modell, wenn wir in Wirklichkeit über alle möglichen Modelle sprechen, die einen bestimmten Satz von Axiomen erfüllen. Wenn wir also über ein Modell sprechen, dann ist P oder NOT P wahr, aber wenn wir über mehrere sprechen, dann kann P gültig sein, NOT P kann gültig sein oder es kann gemischt sein (hier gültig = immer wahr).

Vollständigkeit bedeutet, dass wir es schließlich beweisen werden, wenn P gültig ist, und da NICHT P nur eine andere Aussage ist, gilt es auch dafür. Dies garantiert jedoch nichts über die gemischten Vorschläge. Wir können nie wissen, dass wir keinen Beweis für P oder für NOT P finden würden, wenn wir nicht einfach länger suchen würden.

Oder um noch mehr zu verdeutlichen, die folgenden beiden Behauptungen sind unterschiedlich:

• "NICHT P" ist gültig
• NICHT "P ist gültig"

Letzteres beinhaltet auch das Mischen von P

Logik erster Ordnung ist nur getarnte Algebra, während Logik höherer Ordnung Analyse ist. Theorien, die in Logik erster Ordnung formuliert sind, können als algebraische Systeme ausgedrückt werden: ein System, das eine Menge von Operationen, eine Menge ausgezeichneter Objekte und eine Menge gleicher Identitäten enthält; während Theorien, die in Logik höherer Ordnung formuliert sind und nicht gleichwertig ausdrückbar oder auf Theorien erster Ordnung reduzierbar sind, zu Recht als Kalküle angesehen werden können.

Beispielsweise kann eine abelsche Gruppe als Algebra ausgedrückt werden, die eine einzelne Operation ("-" für Subtraktion), ein ausgezeichnetes Objekt ("0") und die folgenden Identitäten enthält: 0 - 0 = 0, x - (x - y ) = y und x - (y - z) = z - (y - x).

Auch kann beispielsweise eine affine Geometrie A über einem bestimmten Körper F als zweisortige Algebra ausgedrückt werden, die die ternären Operatoren a,f,b ∈ A×F×A ↦ [a,f,b] ∈ A und a enthält ,b,c ∈ A×A×A ↦ abc ∈ A, das die Operationen [a,f,b] = (1 - f)a + fb und abc = a - b + c verkörpert. Ein Beispiel für Axiome (geeignet, außer für die beiden Körper F = GF(2) der Größe 2 und F = GF(3) der Größe 3) ist: [a,0,b] = a, [a,1,b ] = b, [a,rt(1-t),[b,s,c]] = [[a,rt(1-s),b],t,[a,rs(1-t),c ]], abc = [[b,1/(1-t),a],t,[b,1/t,c]], wobei t willkürlich als irgendein Element des Feldes F außer 0 oder 1 gewählt wird .

Für algebraische Theorien ist die "freie Algebra" diejenige, die nur die ausgezeichneten Objekte und alle anderen Objekte enthält, die mit den Operationen der Algebra daraus gemacht werden können. Man kann auch von der "aus einer Menge X generierten freien Algebra" sprechen, bei der die Mitglieder der Menge X zur Liste ausgezeichneter Objekte hinzugefügt werden. Zum Beispiel ist die obige Subtraktionsalgebra, frei erzeugt aus der Menge {1}, ein und dieselbe wie die Algebra der ganzzahligen Subtraktion und enthält auch die Algebra der ganzzahligen Addition durch die Definitionen -x = (x - x ) - x und x + y = x - (-y). (x - x = 0 kann man mit den Axiomen beweisen, und zwar durch: x = 0 - (0 - x) = x - (0 - 0) = x - 0, und x - x = x - (x - 0) = 0, also ist -x = 0 - x eine äquivalente Definition, aber weniger in sich geschlossen.)

Theorien erster Ordnung können also immer durch Modelle realisiert werden, womit die Logik erster Ordnung komplett ist. Genauer gesagt wird dies in der nachstehenden Zusammenfassung zu "First-Order Theories as Many-Sorted Algebras" (Notre Dame Journal Of Formal Logic 25(1), Januar 1984 https://www.researchgate.net/publication/ 38355700_Theorien erster Ordnung_als_viele-sortierte_Algebren )

Vollständigkeit stellt sicher, dass ein Beweis für jede gültige Aussage durch eine endliche Suche gefunden werden kann. Das Scheitern eines Beweises, wenn eine Aussage ungültig ist, tritt erst auf, nachdem die endlose Suche durch alle möglichen Beweise niemals endet. Sie müssten also zunächst eine Ewigkeit warten, um niemals zu enden, bevor Sie eine „Nein“-Antwort auf die Frage „Ist es gültig?“ sehen. Um entscheidbar zu sein, muss die „Nein“-Antwort einige Zeit bevorstehen, bevor die Ewigkeit niemals zu Ende ist.

Der wichtigste Auszug aus dem Abstract:

„In diesem Aufsatz zeigen wir, indem wir das Studium der Logik erster Ordnung durch vielsortierte Algebren entwickeln, dass jede Theorie erster Ordnung eine bestimmte Algebra ist, die Axiome in Gleichungsform verifiziert (siehe Abschnitt 2); daher sind wir in der Lage, die von Birkhoff anzuwenden Sätze über die Varietäten (siehe Abschnitt 1 [und zwei in der Arbeit enthaltene Referenzen]) und um die Henkin-Modelle algebraisch zu erhalten, woraus der Vollständigkeitssatz der Logik erster Ordnung (siehe Abschnitt 3) resultiert.

Pointe: „Many-sorted“ ist der Schlüsselbegriff – fügen Sie also einen booleschen Typ hinzu und erstellen Sie Prädikate als boolesche Operatoren neu.