Einige Definitionsdetails in der Modelltheorie – Gleichheit & QE

Fordern wir, dass jede Sprache (zumindest im Kontext der Modelltheorie) ein Gleichheitszeichen enthalten muss? Und muss dieses Gleichheitszeichen als die „wirkliche“ Gleichheit (die Gleichheit in der Metasprache) interpretiert werden?

Ja und ja. Standardmäßig enthält die Syntax der Logik erster Ordnung ein primitives Symbol$=$, und die Semantik der Logik erster Ordnung behandelt dieses Symbol als Hinweis auf wahre Gleichheit in Modellen. Die Logik ohne primitive Gleichheit wird "Logik erster Ordnung ohne Gleichheit" genannt. Vorbehalt: Meiner Erfahrung nach ist dies die übliche moderne Verwendung von Terminologie. Aber man muss ein bisschen vorsichtig sein, besonders wenn man ältere Quellen liest, da es nicht immer eine universelle Konvention war, dass die Logik erster Ordnung primitive Gleichheit beinhaltet.

Um unsere Modelltheorie allgemeiner zu machen, wollen wir definitiv keine zusätzliche Annahme aufzwingen.

Aber die Logik erster Ordnung ohne Gleichheit befindet sich in der Logik erster Ordnung mit Gleichheit, sodass Sie keine Allgemeingültigkeit verlieren. Wenn Sie Logik erster Ordnung ohne Gleichheit ausführen möchten, können Sie sich einfach auf Sätze und Formeln konzentrieren, die das Gleichheitszeichen nicht verwenden. Und wenn Sie ein Symbol für Gleichheit wollen, das nicht unbedingt als wahre Gleichheit interpretiert wird, können Sie ein neues binäres Beziehungssymbol einführen$\hat{=}$.

Wenn wir andererseits verlangen, dass jede Sprache gleich ist, was ist dann mit der Mengenlehre selbst, die verwendet wird?$\in$als einzige primitive Beziehung und betrachtet$=$als eine Art abgeleitete Relation?

Das ist nicht das, was die (Standard-)Mengentheorie tut. ZFC ist eine Theorie in Logik erster Ordnung mit Gleichheit. Das Extensionalitätsaxiom$\forall x\forall y(\forall z(z\in x\leftrightarrow z\in y)\leftrightarrow (x=y))$enthält das Gleichheitszeichen, und wenn wir über ZFC-Modelle sprechen, wird dieses Gleichheitszeichen als echte Gleichheit interpretiert.

Außerdem müssen wir Theoreme wie den Vollständigkeitssatz sorgfältig neu formulieren, da Formeln wie "$\forall x\ (x = x)$" wurde (implizit) von jeder Struktur erfüllt, ist aber syntaktisch gesehen keine Tautologie (und kann daher nicht aus einem leeren Axiom abgeleitet werden).

NEIN,$\forall x\ (x = x)$ ist eine syntaktische Tautologie und kann aus keinen Hypothesen in irgendeinem Standard-Beweissystem für Logik erster Ordnung abgeleitet werden. Natürlich kann dieser Satz in einem Beweissystem für Logik erster Ordnung nicht ohne Gleichheit hergeleitet werden, da ein solches Beweissystem keine Regeln hat, die das Symbol erwähnen$=$! Aber der Punkt ist, dass ein Beweissystem für die Logik erster Ordnung ohne Gleichheit nicht vollständig für die Logik erster Ordnung (mit Gleichheit) ist.

Müssen wir bei der Definition der Quantorenelimination (QE) verlangen, dass die eliminierte Formel dieselben freien Variablen wie die ursprüngliche Formel hat?

Ja.

Gibt es eine Theorie$T$, ohne konstantes Symbol und nicht vollständig, aber hat QE?

Nun, einige Formulierungen der Logik erster Ordnung erlauben dies auch$0$-äre Beziehungssymbole ("Satzsymbole"). Ein propositionales Symbol$P$ist ein eigener Satz. Also zum Beispiel in der Sprache$L = \{P\}$Wo$P$ist ein propositionales Symbol, die Theorie$T = \{(\exists x\top)\land \forall x\forall y(x = y)\}$hat QE, ist aber nicht vollständig, da es nicht über den Wahrheitswert entscheidet$P$.

Aber auf der anderen Seite haben wir:

Vorschlag Wenn$L$ist eine Sprache mit Nr$0$-ary-Symbole (keine Konstanten oder Aussagensymbole), dann every$L$-Theorie$T$mit QE ist abgeschlossen.

Beweis: Let$\varphi$Bohne$L$-Satz. Dann gibt es einen quantorenfreien$L$-Satz$\psi$so dass$T\models \varphi\leftrightarrow \psi$. Aber der einzige Quantifizierer-frei$L$-Sätze sind$\top$Und$\bot$. Daher$T\models \varphi$oder$T\models \lnot \varphi$, So$T$ist komplett.$\square$

Selbst für Sprachen mit konstanten Symbolen ist der Beweis von QE eine gängige Strategie, um zu beweisen, dass eine Theorie vollständig ist. Wenn eine Theorie$T$QE hat, dann ist es genau dann vollständig, wenn es die Wahrheit aller quantifiziererfreien Sätze entscheidet, was darauf hinausläuft, das zu sagen$T$bestimmt den Isomorphietyp der "durch die Konstanten erzeugten Struktur". Genauer gesagt, bei jedem Modell$M\models T$,$M$hat eine kleinste Unterstruktur$M_\emptyset$, die Unterstruktur von$M$von den Konstanten erzeugt. Wenn$T$hat QE, dann$T$ist vollständig, wenn und nur wenn für alle$M\models T$Und$N\models T$, die Strukturen$M_\emptyset$Und$N_\emptyset$sind isomorph. Im Fall wann$T$hat keine Konstanten,$M_\emptyset$ist immer die leere Struktur, und wann$T$hat auch keine Satzsymbole, zwei beliebige leere Strukturen sind isomorph.