Existenzielle Definitionen in ZFC

In der formalen Mengenlehre (speziell ZFC) gibt es einige Arten von Definitionen: zum Beispiel Prädikatdefinitionen A ⊂ B ist eine Abkürzung für ∀ X ( X ∈ A ⇒ X ∈ B ) , Verständnisdefinitionen, zum Beispiel A ∩ B ist eine Abkürzung für { X ∈ A : X ∈ B }

Die Prädikatdefinitionen sind Abkürzungen von Formeln und Verständnisdefinitionen sind Abkürzungen von Mengen (Begriffen oder Objekten in ZFC).

Das Problem sind die Definitionen der existentiellen Eindeutigkeit, bei denen wir einem Objekt einen Namen geben, dessen existenzielle Eindeutigkeit durch ein Theorem der existenziellen Eindeutigkeit gegeben ist. Sei der Satz der existentiellen Eindeutigkeit ∀ X ∃ ! j ( ∀ z ( z ∈ j ⟺ z ⊂ X ) ) . Es ist eine direkte Folge des Power-Set-Axioms.

In diesem Fall ist bei gegebener Menge A die Potenzmenge Pow(A) keine Abkürzung, Sie können Pow(A) nicht durch ersetzen ∀ X ∃ ! j ( ∀ z ( z ∈ j ⟺ z ⊂ X ) ) weil das eine eine Menge (ein Begriff oder Objekt) und das andere eine Formel ist. Wie kann diese Art von Definitionen formal ausgedrückt werden?

Schlimmer noch, in vielen Büchern das Power-Set-Axiom ∀ X ∃ j ( ∀ z ( z ∈ j ⟺ z ⊂ X ) ) wird direkt verwendet, um Pow(A) zu benennen, ohne zu erwähnen, dass die Eindeutigkeit bewiesen werden muss, um Pow(A) definieren zu können.

Ich habe Pow (A) als Beispiel verwendet, aber meine Frage bezieht sich auf existenzielle Definitionen (Ist dies der richtige Name für diese Art von Definitionen?) im Allgemeinen für ZFC. Wo finde ich eine angemessene Behandlung dieses Themas?

Kurz gesagt, „existentielle Definitionen“ unterscheiden sich wesentlich von solchen Definitionen, dass:

A ⊂ B ≡ D e F ∀ X ( X ∈ A ⇒ X ∈ B )

A ∩ B ≡ D e F { X ∈ A : X ∈ B }

Wie kann eine Existenzdefinition geschrieben werden? Es ist unvermeidlich die Verwendung von Metasprache?

Wie kann man ein Objekt benennen, das dank eines existentiellen Eindeutigkeitssatzes existiert?

Als Fußnote zu Asafs Antwort, wenn wir "das Einzigartige" bezeichnen X so dass φ " als ich X φ , können wir dies nicht auf hilfreiche Weise als Abkürzung behandeln, ohne der Sprache neue Begriffe hinzuzufügen. Aber Terme kommen nie alleine vor, sondern nur als Teile von Formeln, also denkt man statt wie man auspackt ich X φ ∈ A oder A ∈ ich X φ , ist es einfacher, diese nur als Abkürzungen von Formeln in der Sprache der Mengenlehre zu behandeln A frei.

Antworten (5)

Sobald Sie eine Bedingung angeben, folgt auf die Eindeutigkeit die Extensionalität. Und da wir das beweisen können , macht es wenig Sinn, es zu verwenden ∃ ! j in der Aussage des Axioms, weil ∃ ! ist kein Standardquantifizierer, sondern eine Kurzformulierung für eine viel kompliziertere Formel.

Jetzt möchten Sie über Klassenfunktionen wie sprechen P ( ⋅ ) oder Konstanten wie ∅ oder ω . Und das ist ein berechtigtes Anliegen, da die Sprache der Mengenlehre nur die hat ∈ Symbol.

Geben Sie den Begriff einer konservativen Erweiterung ein. In Logik, wenn Sie eine Sprache haben L und eine Theorie T , und Sie haben eine Formel φ ( X ) so dass T beweist das φ ( X ) definiert eine eindeutige Menge, dann können wir die Sprache erweitern L + durch Hinzufügen eines konstanten Symbols C φ und das Axiom φ ( C φ ) .

Wir können jetzt beweisen, dass jedes Modell von T kann natürlich als Vorbild für interpretiert werden T + φ ( C φ ) als Interpretation für die Sprache L + . Ähnlich können wir das mit definierbaren Funktionen oder Relationen machen. Und darüber hinaus jeder Beweis aus T + φ ( C φ ) In L + kann in einen Beweis aus übersetzt werden T in der Sprache L .

Und darum geht es eigentlich. Tatsächlich erweitern wir die Sprache der Mengenlehre so, dass sie viele "bequeme Symbole" enthält, und wir wissen, dass wir alle Aussagen und Beweise aus der erweiterten Sprache mit just rekursiv zurück in die ursprüngliche Sprache der Mengenlehre übersetzen können ∈ .

Vielen Dank, Asaf, aber ich hatte eine Lösung erwartet, die syntaktischer ist als die semantische Methode unter Verwendung der in Ihrer Antwort verwendeten Modelltheorie. Es ist schwer für mich zu verstehen. Ich hatte mehr in Richtung des Kommentars von Malice erwartet.
Dies ist ein syntaktischer Weg, ich habe ihn nur als semantischen Weg verkleidet, da ich lieber über Semantik nachdenke als über Syntax. Der Punkt ist, dass Sie die erweiterten Definitionen rekursiv entpacken können, sodass jeder Beweis (syntaktisches Objekt) in der erweiterten Sprache in einen Beweis in der Originalsprache übersetzt wird.
Richtig, ich muss mehr syntaktisch denken, weil in der ZFC-Version, an der ich arbeite, die Modelltheorie nicht verwendet werden kann. Jeder Quantor hat sein eigenes und explizites Universum, das jedes Mal anders sein kann, wenn Sie einen Quantor schreiben.
Der Punkt ist, dass dies wirklich genau das ist, was Sie erwarten würden. Hier gibt es keine "klugen Tricks". Sie ersetzen einfach jede Formel, in der die "erweiterte Funktion" erscheint, indem Sie behaupten, dass es ein Objekt gibt, das dies und das erfüllt; die Einzigartigkeit wiederum ist nicht notwendig, da wir bereits wissen, dass ZFC die Einzigartigkeit dieser Dinge beweist.
Was meinst du mit "erweiterte Funktion"? Kann eine Formel in der Art sein, wie sie im Ersetzungsaxiom erscheint, wo das Wort Funktion nicht erwähnt wird, aber die funktionale Beziehung in der Formel vorhanden ist.
Sie haben die erweiterte Sprache der Mengenlehre ∈ Und P , Wo P ist der Potenzmengenoperator. Nehmen Sie ZFC, wie es in dieser Sprache definiert wäre (dh fügen Sie auch die notwendigen Axiome zu Replacement hinzu), dann kann jeder Beweis rekursiv in einen Beweis von ZFC in der Sprache von übersetzt werden ∈ . Und bei dieser Übersetzung müssen wir auch nicht jedes Mal verlangen, dass die j die als Potenzmenge von instanziiert wird X ist einzigartig, da ZFC das bereits beweist.
Ok Asaf, Sie haben klar erklärt, dass die Einführung eines neuen Symbols die Sprache überhaupt nicht beeinflusst, indem Sie beginnen: "Sie haben die erweiterte Sprache der Mengenlehre ∈ und P, wobei P der Potenzmengenoperator ist. Nehmen Sie ZFC so, wie es wäre in dieser Sprache definiert werden". Der Kern meiner Frage ist jedoch: Wie kann es in der Sprache definiert werden? (Ich würde jetzt syntaktisch hinzufügen).
Dann verstehe ich den "Kern deiner Frage" nicht. Der Potenzmengenoperator ist definiert als φ P ( X , j ) ist die Formel ∀ z ( z ∈ j ↔ ∀ u ( u ∈ z → u ∈ X ) ) (beachten Sie, dass ⊆ gehört nicht zur Sprache der Mengenlehre, ist also formal auch eine Abkürzung). Wenn Sie jetzt etwas über Machtsätze sagen wollen, dann sagen Sie das ∃ j ( φ P ( X , j ) ∧ ψ ( j ) ) . Abgesehen davon könnte es eine gute Idee sein, die Initiative zu ergreifen und ein vernünftiges Logikbuch zu finden, das den Begriff "konservative Erweiterungen" behandelt, und mehr darüber zu lesen.
Ich betone in meiner Frage diese Definition wie:
Zum Beispiel was? Wenn der Power-Set-Operator nur ein Beispiel ist, verstehe ich nicht, warum meine Antwort nicht allgemein genug ist, "nur" um dasselbe Beispiel zu verwenden. Wir beginnen uns im Kreis zu drehen, und ich fürchte, dass ich ohne eine angemessene Klärung Ihrerseits keinen Sinn darin sehe, dies fortzusetzen.
Woher wissen Sie, dass Sie existieren, damit Ihr Operator Sinn macht? Die Antwort ist das Machtaxiom. Meine Frage ist, wie man das Objekt y nennt, das für jede Menge x existiert, dank des Potenzaxioms? In vielen Lehrbüchern geschieht dies locker. Wie kann man ein Objekt benennen, das dank eines existentiellen Eindeutigkeitssatzes existiert?
@CarlosFreites: Ich bin mir nicht sicher, was du mit "Name" meinst. Jedes Mal, wenn Sie auf ein solches Objekt verweisen möchten, verwenden Sie dafür eine gebundene Variable, die Sie benötigen, um die definierende Bedingung zu erfüllen.
Ich meine Namen außerhalb der Formel. Angenommen, ich habe eine Existenzformel für Einzigartigkeit ∃ ! j ( φ ( j , X ) ) (Theorem XYZ) Jetzt möchte ich mich auf die Menge beziehen, die die Formel besagt, dass sie eindeutig ist. In Lehrbüchern wird dies mehr oder weniger so gemacht: "Sei NEU (x) die Menge, der Satz XYZ sagt, dass sie bei gegebener Menge x eindeutig ist." Dann, von diesem Moment an, φ ( N E W ( X ) , X ) es wird als wahr angenommen.
Der letzte Kommentar war an @EricWofsey.
@CarlosFreites: aber es ist eigentlich dasselbe wie für A ∩ B : Der Satz ∀ A ∀ B ∃ C ( ∀ X , X ∈ C ⟺ ( X ∈ A ∧ X ∈ B ) ) ist ein Satz, und von diesem können Sie verwenden A ∩ B als seiend C . Da ist es nicht anders { X ∈ A : X ∈ B } wird auch nur in der Metasprache verwendet: Es kann kein Begriff sein, da Formeln darin enthalten sind
@ Max: { X ∈ A : X ∈ B } ist dank des Verstehensaxioms eine Menge (also ein Begriff). Das Problem, mit dem wir es hier zu tun haben, ist genau, wie man Symbole wie \{x\in A : x\in B\} und POW(x) mit existentiellen Eindeutigkeitssätzen verbindet.
@ Carlos: Formal gesehen, { X ∈ A : X ∈ B } ist kein Begriff. Es verwendet den informellen Operator mit geschweiften Klammern, der – wenn nichts anderes – ein Operator zweiter Ordnung ist. Mit dem Verstehensaxiom können Sie das für alle beweisen A und für alle B es existiert C so dass X ∈ C ↔ X ∈ A ∧ X ∈ B ; und die Extensionalität ermöglicht es Ihnen, dies zu beweisen C ist eigentlich einzigartig. Nun, wann immer Sie darauf verweisen möchten C Sie müssen damit beginnen, dass "es existiert C so dass C ist die so und so Menge ..." und dann, wann immer Sie schreiben C was meinen Sie A ∩ B für den Rest des Beweises.
@Carlos: Wenn Sie keine sehr seltsame Begriffsdefinition verwenden, kann ein Begriff keine Formel in seiner Bildung verwenden. In der (üblichen) Theorie erster Ordnung ZF gibt es außer Variablen keine Terme
@ Max Das stimmt! Danke, dass Sie mir klar gemacht haben, dass es in ZFC keine Begriffe gibt. Ich bin implizit davon ausgegangen, dass fast Dinge wie z ∅ wo Bedingungen von ZFC. Sehr interessant und hilfreich für mich.
Hm. Ich war mir sicher, dass mein zweiter Absatz das ansprach. Anscheinend nicht deutlich genug.

Es scheint eine gewisse Unsicherheit darüber zu bestehen, was Sie genau fragen, aber vielleicht ist dies eine Antwort auf Ihre Frage.

Wenn Sie nur Abkürzungen der Art verwenden möchten, die für verwendet werden A ⊂ B , lautet die Antwort, dass Sie nicht versuchen, Begriffe isoliert zu übersetzen; Sie versuchen, Formeln zu übersetzen, in denen sie vorkommen. Denn die wohlgeformten Formeln der Mengenlehre werden induktiv aus Atomformeln der Form gebildet a ∈ β Und a = β , das heißt, wenn wir "übersetzen wollen { X : φ } "man muss nur herausfinden was" { X : φ } ∈ a ," " a ∈ { X : φ } ," Und " a = { X : φ } " sollten Abkürzungen für sein. Hier ist eine Version, die in ZF angemessen funktioniert:

  • Für a ∈ { X : φ } , wir können einfach sagen, dass es ein Synonym für ist ∃ j ( a ∈ j ∧ ∀ z ( z ∈ j ↔ ϕ ) ) .
  • Für { X : φ } ∈ a , sagen wir, dass dies nur kurz für ist ∃ j ( j ∈ a ∧ j = { X : φ } ) .
  • und für a = { X : φ } Wir beziehen uns auf den ersten Aufzählungspunkt und die Extensionalität und übersetzen es als ∀ j ( j ∈ a ↔ j ∈ { X : φ } ) .

Wenn wir auf diese Weise weiterhin Formeln entpacken, die Mengenabstrakte enthalten, werden wir sie schließlich auf Formeln reduzieren, in denen die einzigen Terme Variablen sind und die atomare Formel diejenigen sind, die beteiligt sind ∈ Und = . Diese Formeln werden jedoch sehr lang und hässlich; Glücklicherweise müssen wir aus Gründen, die Asaf angibt, nicht wirklich aufpassen, solange unsere Axiome die Existenz einer Menge aller Dinge garantieren, die die Eigenschaft erfüllen φ – wir können sie einfach als atomare Begriffe behandeln und weitermachen.

Das in der ersten Kugel ist das einzige echte, weil es das einzige ist, das es ermöglicht, das Symbol loszuwerden { X : φ } . Die anderen beiden Kugeln benötigen die erste, wie Sie bemerkt haben. Das ist eine gute Beschreibung, wie man ein Symbol wie loswird { X : φ } . Die Frage ist: Wie das Symbol { X : φ } ist vorgestellt? Dieser Fall ist besonders schwierig, weil er nicht von einem Axiom, sondern von einem Axiomenschema herrührt.

In der Sprache von ZFC gibt es keine Konstanten oder Funktionssymbole, daher sind die einzigen Begriffe Variablen. Eine Möglichkeit, mit Definitionen umzugehen, besteht darin, die Möglichkeit zu ignorieren, neue Symbole einzuführen, und sich einfach vorzustellen, dass jede Formel, die Definitionen verwendet, eine Abkürzung einer Formel in der Sprache von ZFC ist. Definitionen können als informeller, aber präziser Weg angesehen werden, kürzere und besser lesbare Formeln anstelle sehr langer Formeln zu schreiben. Es sollte klar sein, wie man eine Formel, die definierte Symbole enthält, in eine Formel in der reinen ZFC-Sprache übersetzt.

Zum Beispiel, A ⊂ B übersetzen kann ( ∀ X ) ( X ∈ A ⇒ X ∈ B ) , und eine Formel mit ⊂ irgendwo innerhalb wird übersetzt, indem jede Unterformel des Formulars entsprechend ersetzt wird A ⊂ B . Ähnlich für jedes definierte Prädikatsymbol P ( X 1 , … , X N ) .

Was definierte Funktionssymbole betrifft, müssen wir nur wissen, wie man eine Formel der Form übersetzt j = F ( X 1 , … , X N ) , diese wird durch die Formel ersetzt φ ( j , X 1 , … , X N ) als Definition verwendet F . Dann können wir auch übersetzen j ∈ F ( X 1 , … , X N ) : wir ersetzen es durch ( ∃ z ) ( j ∈ z ∧ φ ( z , X 1 , … , X N ) ) . Ebenso können wir übersetzen F ( X 1 , … , X N ) ∈ j . Die Tatsache, dass für alle X 1 , … , X N es gibt genau einen j befriedigend φ ( j , X 1 , … , X N ) als „Hintergrundwissen“ betrachtet werden kann, muss es nicht direkt in die Übersetzung kodiert werden.

Übrigens, { X ∈ A : X ∈ B } ist auch eine Abkürzung, die in eine reine ZFC-Sprache übersetzt werden muss; Formel j = { X ∈ A : X ∈ B } wird natürlich ersetzt durch ( ∀ X ) ( X ∈ j ⇔ ( X ∈ A ∧ X ∈ B ) ) .

Nein, das ist ungenau. Es gibt einen formalisierten Weg, neue Symbole einzuführen. Es ist genau das, wovon ich in meiner Antwort gesprochen habe, konservative Erweiterungen; speziell en.wikipedia.org/wiki/Conservativity_theorem ist in diesem Fall relevant.
Was ich vielleicht sagen wollte, war: "Ein Weg, wie man mit Definitionen umgeht, besteht darin, die Möglichkeit zu ignorieren, neue Symbole einzuführen, und sich einfach vorzustellen, dass jede Formel, die Definitionen verwendet, eine Abkürzung einer Formel in der Sprache von ZFC ist". Trotzdem danke für den Kommentar.
Ja, das machen wir oft, wir betrachten all diese Dinge als Abkürzungen. Aber das geht einfacher mit Relationen (zB A ⊆ B ) als bei Begriffen (z ∅ oder A × B ).
@PeterElias Wäre schön, wenn Sie den Satz in Ihrer Antwort ändern "Außerdem gibt es keinen formalisierten Weg, um neue Symbole einzuführen." von dem in deinem letzten Kommentar. Ihre Antwort ist der Typ, den ich suche.
@Asaf Zu deinem letzten Kommentar. Exakt!
@Carlos: Wie ich immer wieder sage, konservative Erweiterungen durch Hinzufügen neuer Funktionssymbole.
@CarlosFreites Fertig... Freut mich, dass dir meine Antwort gefällt!

Wenn ich Ihre Kommentare zu Asafs Antwort sehe, denke ich, dass eine andere Möglichkeit, Ihr Problem zu lösen, eine andere Sichtweise wäre: Denken Sie in Bezug auf die (klassische) Folgerechnung.

Angenommen, Sie möchten den Satz „Für jede Menge A , es existiert B so dass es eine Injektion gibt A → B , und keine Surjektion A → B ". Die übliche Wahl, um diesen Satz zu beweisen, ist die Verwendung B = P ( A ) . Aber wie schreibt man das formal?

Wenn Sie Ihre Folgenrechnung machen, kommen Sie irgendwann an Z F ⊢ ∃ B , ϕ P ( A , B ) Wo ϕ P ( X , j ) ist eine Abkürzung für die Formel " j ist die Potenzmenge von X ".

An diesem Punkt denkst du „Lass es B sei die Potenzmenge von A “, und Ihr natürlicher Abzugsbeweis fährt fort mit Z F , ϕ P ( A , B ) ⊢ . . . „wobei „...“ alles ist, was es sein muss.

Wenn Sie bei " Z F , ϕ P ( A , B ) ⊢ es gibt eine Spritze A → B und keine Surjektion A → B ", können Sie eine der Inferenzregeln des Folgenkalküls verwenden:

Aus Γ , ϕ ( T ) ⊢ ψ ( T nicht frei rein Γ ) Und Γ ⊢ ∃ X , ϕ ( X ) , schließen Γ ⊢ ψ .

Wenden Sie dies an ϕ ( X ) = ϕ P ( A , X ) , Und ψ = ∃ j , Ω ( j ) Wo ∃ B , Ω ( B ) ist die Formel, die wir zu beweisen versuchen, die Sie endlich bekommen Z F ⊢ ∃ B , Ω ( B ) . Verallgemeinerung verwenden, Z F ⊢ ∀ A , ∃ B , B l A B l A .

Also haben wir das Powerset von verwendet A in einem formalen Beweis, aber die Sache ist die, dass Sie sie als nicht verwendete Variable benennen (in gewissem Sinne speichern) können, indem Sie ihre Definition auf die Seite der Hypothesen stellen und die (jetzt verwendete) Variable im Beweis verwenden, indem Sie ihre verwenden Definition an verschiedenen Stellen im Beweis.

Das ist der Fall, wenn Sie das definierte Objekt verwenden möchten, um etwas anderes zu beweisen. Wenn Sie einige Eigenschaften des definierten Objekts beweisen möchten, können Sie ähnliche Dinge tun, z. B. anstatt zu beweisen ∀ A , | P ( A ) | > | A | kannst du beweisen ∀ A , ∀ B , ϕ P ( A , B ) ⟹ | B | > | A | usw. Da es nur einen gibt B so dass ϕ P ( A , B ) , dieser letzte Satz ist dasselbe wie das, was Sie zu beweisen versuchen.

Ich habe dies auf rein syntaktische Weise getan, aber natürlich ist es meiner Meinung nach wichtig, den semantischen Aspekt der Dinge im Auge zu behalten, und in dieser Hinsicht ist Asafs Antwort, in der konservative Erweiterungen erwähnt werden, sehr interessant. Beachten Sie, dass er auch den syntaktischen Aspekt erwähnt hat ("Übersetzen eines Beweises in L + in einen Proof in L rekursiv"), das einzige, was ich "mehr" getan habe, ist, Hinweise zu geben, wie diese Übersetzung erreicht werden kann.

Wenn jemand meine Antwort verbessern kann, indem er einige Fehler korrigiert, die ich wahrscheinlich gemacht habe, sind solche Änderungen natürlich sehr willkommen

Ich habe die korrigiert L A T E X :)

Ein Ansatz, den fx Bourbaki verwendet, ist die Einführung des Hilbert-Operators . Auf diese Weise benötigen Sie keine weiteren Primitive, da die Quantoren in Thermen des Hilbert-Operators ausgedrückt werden können.

Der Vorteil dieser Verwendung besteht darin, dass die Sprache es einem Konstrukt ermöglicht, ein Prädikat in ein Objekt zu verwandeln (wobei das Prädikat nach Möglichkeit erfüllt wird).

Dies ähnelt der Ad-hoc-Lösung, um einfach die Definition eines Symbols durch ein Prädikat mit eindeutiger Gültigkeit zu ermöglichen.

Existenzielle Definitionen in ZFC
AntwortenHierDatenschutz-Bestimmungen1y, 0v