Kann man die Set-Builder-Notation offiziell in ZFC einführen?

Wenn man ganz formal ist, dann kann man ZFC als Satz von Formeln erster Ordnung über die Signatur formulieren L = { ∈ } bestehend nur aus einer binären Relation ∈ . Dann kann man in dieser Formensprache die üblichen ZFC-Axiome aufstellen.

Ich habe kürzlich etwas über das Konzept der Erweiterung per Definition erfahren . Die Grundidee ist folgende: In der Praxis arbeiten wir nicht in einer Sprache, die nur aus besteht ∈ , aber wir führen ständig neue Symbole ein! Zum Beispiel beobachten wir zuerst, dass es eine einzigartige Menge gibt, die überhaupt keine Elemente hat, und dies rechtfertigt, dass wir dieser einzigartigen Menge ein spezielles Symbol geben können – wir wählen ∅ dafür. Ebenso kann man ein Symbol einführen N für die natürlichen Zahlen. Aber das gleiche Konzept funktioniert auch, wenn wir neue Funktions- und Beziehungssymbole einführen: Wir können zum Beispiel die Operation definieren ∪ durch den Beweis, dass es für jedes A, B eine eindeutige Menge gibt A ∪ B mit dem Eigentum ∀ X ( X ∈ A ∪ B ⟺ X ∈ A ∨ X ∈ B ) (nachdem bewiesen wurde, dass dies eindeutig ist, wenn zwei Sätze A, B gegeben sind ); man kann auch eine Relation definieren ⊆ indem man es einstellt A ⊆ B :⇔ ∀ X ( X ∈ A ⟹ X ∈ B ) .

Für eine formale Definition dieses Konzepts der "Erweiterung per Definition" siehe den verlinkten Wikipedia-Artikel. Ich wundere mich:

Kann man in ähnlicher Weise eine Set-Builder-Notation in die formale Sprache der Mengenlehre einführen? Ich habe so etwas im Sinn: ein Mengensymbol gegeben A und eine Formel ϕ ( X ) mit einer freien Variablen kann man die Menge definieren { X ∈ A : ϕ ( X ) } die eindeutige Menge aller Elemente von A zu sein, die die Eigenschaft erfüllen ϕ . Ist dies nur eine menschliche Notation oder kann dies ähnlich wie das Konzept der Erweiterung per Definition präzisiert werden?

Anscheinend nicht gut genug. Verzeihung.
@Arthur: Ich frage, ob es möglich ist, einen Ausdruck wie hinzuzufügen { X ∈ A ∣ ϕ ( X ) } zur formalen Syntax von ZFC, wie man hinzufügen kann ⊆ Und ∪ Und ∅ zur formalen Syntax. Meine Frage ist ein bisschen dumm und naiv, aber im besten Fall gibt es etwas zu lernen :-)
Ich habe nie wirklich viel von der Intuition in der strengsten mathematischen Logik verstanden, aber es scheint mir so ϕ ist eine Hürde. Aus diesem Grund sind Verstehen und Ersetzen keine Axiome, sondern Axiomenschemata. Sie könnten ein Schema für die Set-Builder-Notation erstellen, denke ich. Oder ich bin überfordert.
Für alle anderen, die auf diesen Beitrag stoßen, führt der formelle Weg dazu über die definitoriale Erweiterung . Dies ist die rigorose Methode zur Unterstützung der sogenannten Set-Builder-Notation (die im Wesentlichen ein konstantes Symbol ist, das existentielle Aussagen bezeugt) sowie ∪ (ein binäres Funktionssymbol) und ⊆ (ein binäres Prädikat-Symbol). Beachten Sie, dass die beiden letzteren in ZFC nicht durch Objekte (Sets) repräsentiert werden.
@ user21820: Ich habe unten eine Antwort auf Ihre Frage im Sinne der definitorialen Erweiterung gegeben, aber bevor ich Ihren Kommentar gelesen habe. Sie haben Recht. Die Set-Builder-Notation, die auf eine gegebene Formel mit einer freien Variablen angewendet wird, kann als neues unäres Funktionssymbol interpretiert werden, das der Sprache der Mengenlehre hinzugefügt werden soll.
@Transcendental: Ja, und Sie haben eine alternative Denkweise, nämlich dass das Spezifikationsaxiom eine definierbare Funktion für Mengen für jede Formel angibt, die die durch die Formel angegebene Teilmenge ausschneidet. Meine war einfach die allgemeinere Vorstellung, dass jedes existentielle Axiom mechanisch in eine definierbare Konstante umgewandelt werden kann. =)

Antworten (3)

Hier ist ein Ansatz, der Russells Beschreibungsoperator nicht verwendet ι .

Gegeben sei eine Formel erster Ordnung φ mit einer freien Variablen z in der Sprache der Mengenlehre ( L Ö S T ), können Sie (i) ein neues unäres Funktionssymbol hinzufügen F φ Zu L Ö S T und (ii) das folgende neue Axiom to Z F :

( ∀ X ) ( ∀ j ) ( j = F φ ( X ) ⟺ ( ∀ z ) ( z ∈ j ⟺ ( z ∈ X ∧ φ ) ) ) . ( ⋆ )
Durch die wohlbekannte Technik der Erweiterung durch Definitionen in der Logik erster Ordnung ergeben diese Additionen eine konservative Erweiterung von Z F denn einerseits stellt das Axiom-Schema der Spezifikation dies sicher
( ∀ X ) ( ∃ j ) ( ∀ z ) ( z ∈ j ⟺ ( z ∈ X ∧ φ ) ) ,
und andererseits stellt das Axiom der Extensionalität dies sicher
( ∀ X ) ( ∃ ! j ) ( ∀ z ) ( z ∈ j ⟺ ( z ∈ X ∧ φ ) ) .
Sie können daher denken F φ als formalisierte Version der Set-Builder-Notation angewendet auf φ .

Die Set-Builder-Notation ist ein „termbildender“ Operator, dh ein Symbol, das mit „input“ eine Formel als „output“ einen Term erzeugt , wie bei Russell ι für konkrete Beschreibungen .

Um die Sprache mit zu "vergrößern". ι , wir müssen :

1) beweisen: ( ∃ ! z ) Q ( z , X 1 , … , X N )

2) füge das Axiom hinzu: j = ( ι z ) Q ( z , X 1 , … , X N ) ↔ Q ( j , X 1 , … , X N ) .

Ebenso müssen wir in der Mengenlehre beweisen:

( ∃ ! z ) ( ∀ X ) ( X ∈ z ↔ φ ( X ) )

und füge dann das Axiom hinzu:

{ X : φ ( X ) } = ( ι z ) ( ∀ X ) ( X ∈ z ↔ φ ( X ) ) .

Danke. Scheint, als wären eindeutige Beschreibungen die perfekte Antwort, um die Set-Builder-Notation in ZFC zu formalisieren.

Ja, die Namen in der Entwicklung des Forcierens können so gesehen werden, und die Definition des konstruierbaren Universums L kann man auch so formulieren.

Ich erinnere mich, dass ich ein Rückwärts-K-Symbol gesehen habe, das verwendet wurde, um formale Terme zu bezeichnen, die im Wesentlichen unterschiedliche Set-Builder-Terme waren.

Kann man die Set-Builder-Notation offiziell in ZFC einführen?
AntwortenHierDatenschutz-Bestimmungen1y, 0v