Axiomschema der Spezifikation (Formelargumente)

Sie benötigen keine Parameter.

Ralf Schindler hat eine kurze Notiz geschrieben , wo Sie die Details sehen können (und Ralf und ich haben letztes Jahr im Mai darüber gesprochen). Schließlich fanden wir eine frühe Referenz, die ein noch stärkeres Theorem beweist. Sehen

Azriel Levy, Parameters in the Comprehension Axiom Schemas of Set Theory , in Proceedings of the Tarski symposium , Proceedings of Symposia in Pure Mathematics, vol. 25, American Mathematical Society, Providence, RI, S. 309–324.

(Siehe auch Akihiro Kanamoris In Lob des Ersatzes für weitere Diskussionen und zusätzliche Referenzen.)

Das Theorem in Ralfs Notiz ist stärker als Sie fragen: Wir können formulieren$\mathsf{ZFC}$ohne dass Parameter entweder zum Verständnis (Spezifikation) oder zum Ersetzen erforderlich sind.

Wie Sie sehen können, ist das Argument weniger als eine Seite lang. Lassen Sie mich eine kurze Zusammenfassung geben: Beachten Sie zuerst, dass wir die Existenz von beweisen können$0$Und$1$, und daher von geordneten Paaren der Form$(a,0)$oder$(a,1)$für alle$a$. Aus (einer Instanz von parameterfreier) Ersetzung erhalten wir das$a\times\{0\}$Und$a\times\{1\}$existieren für alle$a$. Auch für alle$a$Und$b$,$(a\times\{0\})\cup\{(b,1)\}$existiert. Daraus können wir das beweisen

$$\{((u,0),(b,1))\mid u\in a\}$$ existiert für alle $a$Und $b$: Erste, $d=\mathcal P(\mathcal P((a\times\{0\})\cup\{(b,1)\}))$existiert, und die gewünschte Menge ist $$\{x\in d\mid \exists u\,\exists v\,(x=((u,0),(b,1)))\},$$ die durch Anwenden einer Instanz einer parameterfreien Spezifikation existiert.

Wir können jetzt die Spezifikation mit Parametern beweisen. Beachten Sie dazu, dass wir mit Pairing endlich viele Parameter in einem einzigen codieren können, sodass es beispielsweise ausreicht, das Ergebnis für Formeln mit einem Parameter anzuzeigen$\phi(x,v)$. Das heißt, gegeben$a,b$, das müssen wir zeigen

$$\{x\in a\mid \phi(x,b)\}$$ existiert.

Wir verwenden die von der Klassenfunktion gegebene parameterfreie Ersetzungsinstanz$F$definiert von$F(x)=0$es sei denn$x$hat die Form$((u,0),(c,1))$für einige$u,c$, in diesem Fall setzen wir$F(x)=u$. Wir sehen das

$$F''\{((u,0),(b,1))\mid u\in a\}= \{x\in a\mid \phi(x,b)\}\cup\{0\},$$ und daraus folgt Ihre Frage (indem Sie eine parameterfreie Instanz der Spezifikation zum Entfernen anwenden $0$ggf. aus dem Set).

Abschließend beweisen wir die Ersetzung von Formeln mit einem Parameter (was wiederum durch Paarung ausreicht). Dementsprechend lassen$\phi(x,y,v)$eine Formel sein, lassen Sie$b$sei eine Menge, und nehme an, dass für jeden$x$es gibt ein Unikat$y$so dass$\phi(x,y,b)$. Das müssen wir jedem zeigen$a$,

$$\{y\mid\exists x\in a\,(\phi(x,y,b))\}$$ existiert.

Wir verwenden die von der Klassenfunktion gegebene parameterfreie Ersetzungsinstanz$F$definiert von$F(z)=0$es sei denn, es gibt$x,c$mit$z=((x,0),(c,1))$, und es ist ein Unikat$y$so dass$\phi(x,y,c)$gilt, in diesem Fall setzen wir$F(z)=y$. Das sehen wir dann

$$F''\{((x,0),(b,1))\mid x\in a\}=\{y\mid\exists x\in a\,(\phi(x,y,b))\}\cup\{0\}$$ und wie zuvor sind wir durch einen letzten Appell an eine (parameterfreie) Instanz der Spezifikation erledigt, wenn entfernt wird $0$aus dem Set benötigt.

Die Notwendigkeit der universellen Quantoren ist ein Artefakt der Tatsache, dass in den klassischen Formulierungen der Logik die Betonung auf Aussagen fällt, denen Wahrheitswerte zugeordnet werden könnten, und diese Aussagen daher notwendigerweise durch Formeln ohne freie Variablen dargestellt werden. In diesem Aufbau sind Axiome, Theoreme usw. alle notwendigerweise Sätze und werden daher durch Formeln ohne freie Variablen dargestellt. Um also die Axiome im Axiomenschema als Aussagen zu formulieren, benötigt man die universellen Quantoren.

Bei weniger klassischen Ansätzen (die sich mehr mit dem Beweiskalkül wie der Typentheorie oder der Kategorientheorie befassen) liegt der Schwerpunkt auf hypothetischen Behauptungen, dass etwas wahr ist. Bei der Formulierung der klassischen Logik kann eine solche Behauptung mit bezeichnet werden$\phi\vdash_{\vec x}\psi$, wo zum Beispiel$\phi$Und$\psi$sind beliebige Formeln, und$\vec x$ist eine Liste aller in vorkommenden freien Variablen$\phi$Und$\psi$. Diese Behauptung ist zu lesen als: im Zusammenhang mit den Symbolen in der Liste$\vec x$sind Elemente des Universums, so dass$\phi$ist befriedigt,$\psi$ist auch zufrieden.

Diese Formulierung ist für die klassische Logik unnötig (obwohl ich sie bequem finde), da die Behauptung$\phi\vdash_{\vec x}\psi$ist nach der Folgerungsregel der Implikation gleichbedeutend mit$\vdash_{\vec x}\phi\rightarrow\psi$(im Kontext$\vec x$, die Formel$\phi$impliziert$\psi$erfüllt ist), was aus der Definition des Universalquantors äquivalent ist$\vdash\forall\vec x(\phi\rightarrow\psi)$(Wo$\forall\vec x$ist eine Abkürzung für$\forall x_1\forall x_2\forall\dots\forall x_n$Wenn$\vec x=[x_1,\dots,x_n]$). Diese Behauptung besagt, dass im leeren Kontext und ohne Hypothesen die (freie variable freie) Formel$\forall\vec x(\phi\rightarrow\psi)$ist befriedigt.

(Beachten Sie jedoch, dass für nichtklassische Logiken oder Fragmente der klassischen Logik, für die uns nur eingeschränkter Zugriff auf Quantoren und Konnektoren gewährt wird, die obige Äquivalenz möglicherweise einfach nicht verfügbar ist, daher diese alternative Formulierung).

So insbesondere in dieser alternativen Formulierung der klassischen Logik die Behauptung

$$\vdash_{\vec w}\forall A \, \exists B \, \forall x \, ( x \in B \leftrightarrow [ x \in A \wedge \varphi] )$$ kann als Axiom genommen werden und ist per Definition von $\forall$Äquivalent zur Behauptung $$\vdash\forall\vec w(\forall A \, \exists B \, \forall x \, ( x \in B \leftrightarrow [ x \in A \wedge \varphi]$$

Beachten Sie, dass wir immer noch die freien Variablen verfolgen. Soweit ich weiß, können Sie die freien Variablen nicht nachverfolgen, und ein Teil des nicht-klassischen Ansatzes besteht darin, dass die Nachverfolgung eingebaut ist (denn wenn Sie sich mit mehrfach sortierter Logik oder Typentheorie befassen möchten, müssen Sie müssen nicht nur nachverfolgen, welche Symbole Variablen sind, sondern auch welche Art oder Typen diese Variablen sind).

---

Um die geklärte Frage zu beantworten, ist es im Allgemeinen einfach nicht wahr, dass jede Formel mit zwei Variablen durch eine unendliche Familie von Formeln mit einer Variablen ersetzt werden kann. Der Grund dafür ist, dass Elemente der Domäne einfach nicht Teil des Alphabets sind, über dem die Formeln als Zeichenketten definiert sind. Insbesondere für die Mengenlehre sind Formeln Zeichenketten aus Variablen ($x,y,z,\dots$), die logischen Verknüpfungen ($\wedge,\vee,\neg,\rightarrow$), die beiden Quantoren ($\exists,\forall$), Klammern ($(,)$), das Gleichheitszeichen ($=$) und das nicht-logische Beziehungssymbol$\in$.

Beachten Sie, dass nicht einmal die leere Menge, die wir informell als bezeichnen$\{\}$, kommt als Ausdruck in den obigen Symbolen vor. Eher, wenn wir eine Formel haben$\phi(u)$, und wir wollen es mit instanziieren$\{\}$, was wir erhalten, ist$\phi_{\{\}}\equiv\left(\forall x\neg(x\in u)\right)\wedge\phi(u)$. Folglich sind die nur Formeln$\phi_z$für$z$Ein Element des Bereichs sind diejenigen, die definierbar sind , dh solche, die durch die Ableitbarkeit (aus den Axiomen) der Wahrheit einer Formel definiert sind$\exists z\left(x\in z\leftrightarrow\phi(x)\right)$stimmt wo$\phi$verwendet nur die oben definierten Symbole.

Da es jedoch abzählbar viele Formeln und unabzählbar viele Mengen gibt (dies ist ein metatheoretisches Ergebnis), wird ersetzt$\phi(x,z)$mit$\phi_z(x)$, was Sie nur für definierbar tun können$z$, führt nicht zu demselben Axiomschema: Es führt zu dem schwächeren Schema, das nur definierbare Mengen betrifft.

Der$w_i$sind notwendig. Die Auswahlkriterien$\varphi$kann sich auf zuvor eingeführte freie Variablen beziehen (die$w_i$) zusätzlich zu$A$.

Beispiel:

Lassen$A$ein Satz sein.

Vermuten$P(w_1,w_2,w_3)$(Einführung freier Variablen$w_1,w_2, w_3$Prädikat verwenden$P$)

Dann gibt es$B\subset A$so dass$\forall x [x\in B \iff x\in A \land\varphi(x,w_1,w_2,w_3,A)]$.

Beachten Sie, dass die ausgewählte Teilmenge von den freien Variablen abhängt$w_1,w_2,w_3$.