Die Mathe-Redaktion - 22.02.2017 13:54 - Registrieren/Login
Auswahl
Schwarzes Brett
Aktion im Forum
Suche
Stichwortsuche in Artikeln und Links von Matheplanet
Suchen im Forum
Suchtipps

Bücher
Englische Bücher
Software
Suchbegriffe:
Mathematik bei amazon
Naturwissenschaft & Technik
In Partnerschaft mit Amazon.de
Kontakt
Mail an Matroid
[Keine Übungsaufgaben!]
Impressum

Bitte beachten Sie unsere Nutzungsbedingungen, die Distanzierung, unsere Datenschutzerklärung und
die Forumregeln.

Sie können Mitglied werden oder den Newsletter bestellen.

Der Newsletter Dez. 2016

Für Mitglieder
Mathematisch für Anfänger
Wer ist Online
Aktuell sind 697 Gäste und 27 Mitglieder online.

Sie können Mitglied werden:
Klick hier.

Über Matheplanet
 
Mathematik: SEAR: Mengen, Elemente und Relationen
Freigegeben von matroid am Do. 22. September 2016 15:52:18
Verfasst von Triceratops -   1247 x gelesen [Gliederung] [Statistik] Druckbare Version Druckerfreundliche Version
Mathematik

SEAR: Mengen, Elemente und Relationen

Eine strukturelle Mengenlehre


Die Mathematik wird üblicherweise mithilfe der Mengenlehre fundiert, und die Mengenlehre wird üblicherweise als die Theorie des Axiomensystems <math>\mathsf{ZF}</math> von Zermelo und Fraenkel bzw. seiner Varianten angesehen. Es gibt allerdings noch andere Axiomensysteme, welche zu einer äquivalenten Mengenlehre führen. Ich stelle in diesem Artikel eines dieser Axiomensysteme vor. Es heißt <math>\mathsf{SEAR}</math>, was eine Abkürzung für sets, elements and relations ist. Es wurde vor einigen Jahren von Michael Shulman entwickelt und bisher nur im nLab veröffentlicht. Das Axiomensystem verdient aber eine größere Aufmerksamkeit, weil es im Gegensatz zu <math>\mathsf{ZF}</math> eine typisierte und strukturelle Mengenlehre ist.


1. Einleitung

Wie der Name bereits sagt, gibt es in <math>\mathsf{SEAR}</math> drei, voneinander abhängige, Typen von Objekten: Mengen, Elemente und Relationen. Funktionen werden darauf aufbauend wie üblich als spezielle Relationen definiert. Eine zumindest informelle Typisierung ist im mathematischen Alltag sehr üblich. Entsprechend sinnvoll ist es, für die Mathematik eine typisierte Fundierung zu verwenden. So erkennen wir zum Beispiel an, dass die Wurzelfunktion <math>\sqrt{-} : \mathds{R}^+ \to \mathds{R}^+</math> einem anderem Typ als die Menge der rationalen Zahlen <math>\mathds{Q}</math> angehört und es daher nicht sinnvoll ist, zum Beispiel die Menge <math>\sqrt{-} \cap \mathds{Q}</math> zu bilden. Genau das ist in <math>\mathsf{ZF}</math> allerdings möglich, weil dort jedes Objekt, also auch Elemente und Funktionen als Mengen angesehen werden. Auch <math>\pi</math> ist demnach eine Menge - was sind ihre Elemente? Ist <math>\pi</math> eine Teilmenge von <math>\mathds{R}</math>? Die Typisierung in <math>\mathsf{SEAR}</math> sorgt dafür, dass solche nicht besonders sinnvollen Fragen gar nicht erst gestellt werden können. In <math>\mathsf{SEAR}</math> sind Elemente keine Mengen und können daher auch keine weiteren Elemente enthalten. Sie sind atomar. Elemente können aber mithilfe von Relationen und Funktionen mit Elementen anderer Mengen in Beziehung gesetzt werden.
 
Neben der Typisierung weist <math>\mathsf{SEAR}</math> einen weiteren Vorteil gegenüber <math>\mathsf{ZF}</math> auf: Es handelt sich um eine strukturelle Mengenlehre. Das bedeutet, dass mathematische Objekte durch ihre strukturellen Eigenschaften definiert bzw. charakterisiert werden. In <math>\mathsf{ZF}</math>, einer materiellen Mengenlehre, werden Mengen hingegen üblicherweise durch ihre Elemente definiert bzw. regelrecht kodiert. Ein typisches Beispiel ist die Konstruktion der natürlichen Zahlen in <math>\mathsf{ZF}</math> nach von Neumann:
 
<math>\displaystyle 0 := \emptyset, \quad  1 := \{0\}, \quad  2 := \{0,1\}, \quad 3 := \{0,1,2\}, \quad \dotsc</math>
 
Diese Konstruktion entspricht nicht wirklich unserer strukturellen Vorstellung von natürlichen Zahlen oder dem alltäglichen Umgang mit ihnen. Die aus ihr resultierenden Eigenschaften wie etwa <math>2 \in 5</math> sind unbrauchbar. Normalerweise wird <math>5</math> nicht einmal als Menge angesehen, sondern als ein Element von <math>\mathds{N}</math>; das ist wieder ein Beispiel für Typisierung. Wenn überhaupt, dann benutzen wir <math>2<5</math> für eine geeignete durch strukturelle Eigenschaften charakterisierte Ordnungsrelation <math><</math> auf <math>\mathds{N}</math>. Die strukturelle Definition von <math>\mathds{N}</math> bzw. genauer gesagt von <math>(\mathds{N},0,S)</math>, wobei <math>0 \in \mathds{N}</math> die kleinste natürliche Zahl und <math>S : \mathds{N} \to \mathds{N}</math> die Nachfolgerfunktion ist, geht auf Peano zurück und wird sich auch in <math>\mathsf{SEAR}</math> wiederfinden. Sie beinhaltet nicht, was natürliche Zahlen sind, sondern was man mit ihnen machen kann bzw. auch machen möchte, nämlich Folgen und darauf aufbauend die gesamte Arithmetik rekursiv zu definieren.
 
Eine weitere Eigenschaft von <math>\mathsf{SEAR}</math> ist, dass die Gleichheit von zwei Mengen nicht definiert ist. Einen Ersatz liefern dafür bijektive Funktionen bzw. Isomorphismen. In <math>\mathsf{ZF}</math> können wir uns etwa die Frage stellen, ob die Gleichung <math>\mathds{R}=P(\mathds{N})</math> gilt. Dies ist in <math>\mathsf{SEAR}</math> nicht möglich. Wir können uns aber die sinnvollere Frage stellen, ob es eine bijektive Funktion <math>\mathds{R} \to P(\mathds{N})</math> gibt. Darauf kommt es letztlich auch an. Tatsächlich gibt es in <math>\mathsf{SEAR}</math> nicht einmal die Potenzmenge einer Menge. Potenzmengen werden implizit durch universelle Eigenschaften charakterisiert und sind daher nur bis auf Isomorphie eindeutig bestimmt. Dasselbe gilt für alle anderen Konstruktionen von Mengen.
 
Das System <math>\mathsf{SEAR}</math> ist also typisiert, strukturell und implizit kategoriell. In dieser Hinsicht ist es viel weniger mit <math>\mathsf{ZF}</math> als mit dem kategorientheoretischen Axiomensystem der Mengenlehre <math>\mathsf{ETCS}</math> von Lawvere verwandt, in dem Mengen und Funktionen die Basistypen sind. Abgesehen von der Prädikatenlogik sind zum Verständnis von <math>\mathsf{SEAR}</math> aber naturgemäß keine Vorkenntnisse aus anderen Gebieten der Mathematik nötig.

2. Das Typensystem

Wir beginnen nun mit der Beschreibung des Typensystems von <math>\mathsf{SEAR}</math>. Der Begriff Typ kann hier informell als Synonym für Art oder Sorte angesehen werden.

In <math>\mathsf{SEAR}</math> beginnen wir mit dem Typ
 
<math>\displaystyle \texttt{Set}</math>
 
der Mengen. Aus diesem werden gleich noch weitere Typen gebildet. Wie auch bei anderen Axiomensystemen spielt es keine Rolle, was Mengen sind, sondern wie sie sich zueinander verhalten. Dass <math>A</math> eine Menge ist, notieren wir mit

<math>\displaystyle A : \texttt{Set}.</math>

Hierbei handelt es sich streng genommen um keine Aussage im Sinne der Logik, die wahr oder falsch sein kann. Vielmehr handelt es sich bei <math>A : \texttt{Set}</math> um eine Zuweisung eines im Kontext neuen Objektes <math>A</math> zum Typ <math>\texttt{Set}</math>. Der Fachbegriff heißt Typdeklaration. Weil Typdeklarationen keine Aussagen sind, ist erst Recht die Aussage <math>A : \texttt{Set} \,\wedge\, B : \texttt{Set}</math> nicht formbar, aber man kann natürlich trotzdem mehrere Typdeklarationen hintereinander ausführen.
 
Für jede Menge <math>A : \texttt{Set}</math> soll es einen neuen, ebenfalls mit <math>A</math> bezeichneten Typ der Elemente von <math>A</math> geben. Unter der Typdeklaration

<math>\displaystyle x : A</math>

verstehen wir, dass <math>x</math> als Element der Menge <math>A</math> deklariert werden soll. Wir sagen auch, dass <math>x</math> zu <math>A</math> gehöre, etc. Auch <math>x:A</math> ist keine Aussage, die wahr oder falsch ist, sondern vielmehr eine Beschreibung, was für eine Sorte Element <math>x</math> eigentlich ist, nämlich vom Typ <math>A</math>. Daher schreiben wir auch nicht <math>x \in A</math> (wie in Michael Shulmans Artikel), weil wir <math>x \in A</math> in der Regel als Aussage verinnerlicht haben und es daher zu Verwirrungen kommen könnte. Stattdessen verwenden wir konsequent die aus der Typentheorie übliche Notation <math>x : A</math>. (Wir werden später noch Aussagen der Form <math>x \in T</math> verwenden, wenn <math>T</math> eine Teilmenge einer Menge <math>A</math> ist.)

Es gibt keinen Typ für alle Elemente, also unabhängig von der Menge <math>A</math>. Daher sind auch Aussagen wie "Für alle Elemente <math>x</math> gilt <math>\phi(x)</math>" nicht formbar, sondern wir müssen stets dazusagen, die Elemente welcher Menge wir meinen. Die Aussage "Für alle <math>x:A</math> gilt <math>\phi(x)</math>" bzw. formal <math>\forall x : A.\, \phi(x)</math> ist also formbar, sofern im Kontext <math>A:\texttt{Set}</math> deklariert worden ist.

Zu je zwei Mengen <math>A : \texttt{Set}</math> und <math>B : \texttt{Set}</math> soll es einen neuen mit <math>A \looparrowright B</math> bezeichneten Typ der Relationen von <math>A</math> nach <math>B</math> geben. Unter der Typdeklaration

<math>\displaystyle R : A \looparrowright B</math>

verstehen wir, dass <math>R</math> eine Relation von <math>A</math> nach <math>B</math> ist. Auch hier ist <math>R : A \looparrowright B</math> keine Aussage. Es gibt keinen Typ für alle Relationen, also unabhängig von den zwei Mengen <math>A,B</math>. Bei Aussagen über Relationen muss daher ein Typ der Form <math>A \looparrowright B</math> stets mitgeliefert werden.
 
Man beachte, dass für zwei Mengen <math>A : \texttt{Set}</math> und <math>B : \texttt{Set}</math> keine Elementrelation <math>A \in B</math> definiert ist. Elemente können auch keine Elemente oder Mengen enthalten. Das ist der wesentliche Unterschied zu <math>\mathsf{ZF}</math>.
 
Eine allgemeine Regel der Typentheorie lautet, dass zwei Objekte nur dann miteinander verglichen werden können, wenn sie demselben Typ angehören. So können wir also etwa die Aussage

<math>\displaystyle x=y</math>

für Elemente <math>x,y</math> nur dann formulieren, wenn vorab <math>x,y</math> als Elemente derselben Menge <math>A</math> deklariert worden sind. Wenn <math>x,y</math> verschiedenen Mengen angehören, ist die Aussage <math>x=y</math> nicht definiert, man könnte sogar sagen verboten. Für Relationen <math>R,S</math> können wir entsprechend die Aussage

<math>\displaystyle R=S</math>

nur dann formulieren, wenn <math>A,B</math> Mengen sind und <math>R,S</math> vorab als Relationen desselben Typs <math>A \looparrowright B</math> deklariert worden sind. Die Gleichheit <math>x=A</math> für Elemente <math>x:B</math> und Mengen <math>A</math> ist nicht definiert bzw. verboten. Entsprechendes gilt für <math>x=R</math> und <math>A=R</math>, wobei <math>x:B</math>, <math>A:\texttt{Set}</math> und <math>R:C \looparrowright D</math>. Obwohl je zwei Mengen <math>A,B</math> demselben Typ <math>\texttt{Set}</math> angehören, vereinbaren wir trotzdem, dass die Aussage <math>A=B</math> nicht formbar ist. (Ansonsten würden wir sinnlose Aussagen wie <math>\mathds{R}=P(\mathds{N})</math> erlauben.) Um Mengen miteinander zu vergleichen, werden wir stattdessen Relationen benutzen.
 
Schließlich soll es für jede Relation <math>R : A \looparrowright B</math> und Elemente <math>a:A</math>, <math>b:B</math> eine mit

<math>\displaystyle R(a,b)</math>

notierte Aussage geben, die so interpretiert wird, dass <math>R</math> für <math>(a,b)</math> gilt.

Wir können damit definieren, wann eine Relation <math>f : A \looparrowright B</math> eine Funktion von <math>A</math> nach <math>B</math> ist und schreiben dann

<math>\displaystyle f: A \to B,</math>

nämlich wenn es für alle <math>a: A</math> genau ein <math>b:B</math> gibt mit <math>f(a,b)</math>. Wir schreiben dafür wie üblich <math>b = f(a)</math> und <math>f(a) : B</math>.

3. Die ersten Axiome und deren Konsequenzen

Wir werden nun die 5 Axiome von <math>\mathsf{SEAR}</math> formulieren. Wir werden immer wieder kleine Anwendungen und Erklärungen der bisherigen Axiome einstreuen. Damit wir überhaupt ein bewohntes Universum von Mengen haben, fordern wir nun zunächst:

Axiom 0. Es gibt eine Menge <math>A</math> mit einem Element <math>a:A</math>.<math>\blacktriangleleft</math>

Dieses Axiom wird später durch Axiom 4 redundant. Um Relationen zu konstruieren, brauchen wir:

Axiom 1. Seien <math>A,B</math> zwei Mengen. Für jede in der Prädikatenlogik erster Stufe gebildete Aussage <math>\phi(a,b)</math> über Elemente <math>a:A</math> und <math>b:B</math> gibt es genau eine Relation <math>R : A \looparrowright B</math> mit der Eigenschaft, dass für alle Elemente <math>a:A</math> und <math>b:B</math> gilt:

<math>\displaystyle \phi(a,b) \Longleftrightarrow R(a,b)</math><math>\blacktriangleleft</math>

Die Eindeutigkeit besagt hier: Sind <math>R,S : A \looparrowright B</math> Relationen mit <math>R(a,b) \Leftrightarrow S(a,b)</math> für alle <math>a:A</math> und <math>b:B</math>, so gilt <math>R=S</math>. Für Funktionen <math>f,g : A \to B</math> bedeutet das insbesondere: Wenn <math>f(a)=g(a)</math> für alle <math>a : A</math> gilt, folgt <math>f=g</math>.
 
Für jede Relation <math>R : A \looparrowright B</math> gibt es die duale Relation <math>R^{\mathrm{op}} : B \looparrowright A</math>, die mithilfe von Axiom 1 durch <math>R^{\mathrm{op}}(b,a) \Leftrightarrow R(a,b)</math> definiert ist.
 
Das nächste Axiom bewirkt, dass wir jeder Relation eine Menge von geordneten Paaren zuordnen können, für welche die Relation gilt.
 
Axiom 2. Seien <math>A,B</math> zwei Mengen und <math>R : A \looparrowright B</math> eine Relation. Dann gibt es eine Menge <math>|R|</math> und zwei Funktionen

<math>\displaystyle p_1 : |R| \to A,\quad p_2 : |R| \to B,</math>

sodass gilt: Für Elemente <math>a:A</math> und <math>b:B</math> gilt <math>R(a,b)</math> genau dann, wenn es ein Element <math>x : |R|</math> gibt mit <math>p_1(x)=a</math> und <math>p_2(x)=b</math>.

Ferner ist <math>x</math> eindeutig durch <math>a</math> und <math>b</math> bestimmt.<math>\blacktriangleleft</math>

Wir nennen <math>|R|</math> eine Realisierung von <math>R</math> (Michael Shulman wählt den Begriff Tabulation). Für das eindeutig bestimmte Element <math>x : |R|</math> mit <math>p_1(x)=a</math> und <math>p_2(x)=b</math> schreiben wir

<math>\displaystyle x=(a,b)</math>

und nennen es das geordnete Paar von <math>a</math> und <math>b</math>. Die Elemente von <math>|R|</math> sind also die geordneten Paare <math>(a,b)</math> mit <math>a:A</math> und <math>b:B</math>, für die <math>R(a,b)</math> gilt.
 
Als Anwendung der Axiome 0,1,2 zeigen wir die Existenz einer leeren Menge:
 
Nach Axiom 0 gibt es eine Menge <math>A</math> mit einem Element <math>a:A</math>. Betrachte die Aussage <math>\bot</math>, die stets falsch ist. Nach Axiom 1 gibt es eine Relation <math>R : A \looparrowright A</math>, sodass <math>R(a,b)</math> stets falsch ist. Nach Axiom 2 existiert nun eine Menge <math>|R|</math>, die keine Elemente besitzt. Wir bezeichnen eine solche Menge mit

<math>\displaystyle 0 : \texttt{Set}</math>

und nennen sie eine leere Menge. Wir erinnern daran, dass wir die Gleichheit von Mengen nicht formulieren können, sodass insbesondere die Frage nach der Eindeutigkeit von <math>0</math> keinen Sinn ergibt. Wir können aber festhalten, dass es für je zwei Mengen <math>0</math> und <math>0'</math>, die keine Elemente haben, nach Axiom 1 genau eine Funktion <math>0 \to 0'</math> und analog genau eine Funktion <math>0' \to 0</math> gibt. Diese sind in einem gleich zu definierenden Sinne notwendigerweise zueinander invers, sodass also <math>0</math> und <math>0'</math> problemlos miteinander identifiziert werden können. Wir nennen eine leere Menge <math>0</math> auch eine initiale Menge, weil es für jede Menge <math>A</math> genau eine Funktion <math>0 \to A</math> gibt. Es gibt aber nur dann eine Funktion <math>A \to 0</math>, wenn <math>A</math> ebenfalls leer ist.

Wir definieren nun einfache Operationen mit Relationen und Funktionen: Für jede Menge <math>A</math> haben wir die Relation

<math>\displaystyle \mathrm{id}_A : A \looparrowright A,</math>

die sogar eine Funktion ist und dadurch definiert ist, dass <math>\mathrm{id}_A(a,a')</math> für <math>a:A</math> und <math>a':A</math> genau dann gilt, <math>a=a'</math>. Die Existenz ist durch Axiom 1 gesichert. Es gilt also <math>\mathrm{id}_A(a)=a</math> für alle <math>a:A</math>. Wir nennen <math>\mathrm{id}_A</math> die Identität von <math>A</math>.

Sind <math>R : A \looparrowright  B</math> und <math>S : B \looparrowright C</math> zwei Relationen, so ist ihre Komposition oder auch Verkettung die Relation

<math>\displaystyle S \circ R : A \looparrowright C,</math>

die mithilfe von Axiom 1 durch

<math>\displaystyle (S \circ R)(a,c) \Longleftrightarrow \exists b : B.\, R(a,b) \wedge S(b,c)</math>

für Elemente <math>a:A</math>, <math>c:C</math> definiert ist. Man überlegt sich: Die Komposition von zwei Funktionen ist wieder eine Funktion. Die Komposition von Relationen ist assoziativ und die Identitäten sind beidseitig neutral bezüglich der Komposition.

Wir nennen eine Funktion <math>g : B \to A</math> zu einer gegebenen Funktion <math>f : A \to B</math> invers, wenn die Gleichungen

<math>\displaystyle f \circ g = \mathrm{id}_B, \quad g \circ f = \mathrm{id}_A</math>

gelten. In diesem Fall ist <math>g</math> eindeutig bestimmt, denn es folgt <math>g=f^{\mathrm{op}}</math>. Man schreibt in diesem Fall <math>g=f^{-1}</math> und nennt <math>f^{-1}</math> die zu <math>f</math> inverse Funktion. Wenn eine Funktion <math>f : A \to B</math> eine inverse Funktion besitzt, nennen wir sie invertierbar oder auch bijektiv oder auch Isomorphismus. Dies ist genau dann der Fall, wenn <math>f</math> injektiv und surjektiv ist. Dabei heißt <math>f : A \to B</math> injektiv, wenn

<math>\displaystyle f(a)=f(a') \Longrightarrow a=a'</math>

für alle <math>a:A</math> und <math>a':A</math> gilt, und <math>f : A \to B</math> heißt surjektiv, wenn es für alle <math>b:B</math> ein <math>a:A</math> gibt mit <math>b=f(a)</math>. Wenn es eine bijektive Funktion <math>f : A \to B</math> gibt, nennen wir <math>A</math> und <math>B</math> zueinander isomorph und schreiben:

<math>\displaystyle A \cong B</math>

Wir haben also oben gezeigt, dass die leere Menge bis auf Isomorphie eindeutig bestimmt ist. Isomorphie ist für uns ein struktureller Ersatz für die nicht formulierbare Gleichheit von Mengen. Man kann übrigens zeigen, dass jede im System <math>\mathsf{SEAR}</math> gebildete Aussage über eine Menge auch für jede dazu isomorphe Menge gilt.
 
Die Realisierung <math>|R|</math> einer Relation <math>R : A \looparrowright B</math> ist, zusammen mit den Funktionen <math>p_1 : |R| \to A</math> und <math>p_2 : |R| \to B</math>, ebenfalls bis auf Isomorphie eindeutig bestimmt: Ist <math>|R|'</math> eine weitere Realisierung zusammen mit Funktionen <math>p'_1 : |R| \to A</math> und <math>p'_2 : |R|' \to B</math>, so definieren wir die Relation <math>S : |R| \looparrowright |R|'</math> durch

<math>\displaystyle S(x,x') \Longleftrightarrow p_1(x)=p'_1(x') \wedge p_2(x)=p'_2(x')</math>

und beobachten, dass <math>S</math> eine bijektive Funktion ist.

Wir können mit den Axiomen 0,1,2 auch die Existenz einer Menge mit genau einem Element beweisen: Wählen wir mit Axiom 0 eine Menge <math>A</math> mit einem Element <math>a:A</math>. Nach Axiom 1 gibt es eine Relation <math>R : A \looparrowright A</math>, sodass <math>R(x,y)</math> genau dann gilt, wenn <math>x=y</math> und <math>x=a</math> gilt. Die Realisierung <math>|R|</math> aus Axiom 2 besitzt dann das Element <math>(a,a)</math> und kein weiteres Element. Jede Menge, die genau ein Element besitzt, bezeichnen wir mit

<math>\displaystyle 1:\texttt{Set}</math>

und nennen sie eine terminale Menge. Sie ist bis auf Isomorphie eindeutig bestimmt. Beachte, dass es für jede Menge <math>A</math> genau eine Funktion <math>A \to 1</math> gibt.

Sind <math>A : \texttt{Set}</math> und <math>B:\texttt{Set}</math> zwei Mengen, so definieren wir das Produkt von <math>A</math> und <math>B</math>

<math>\displaystyle A \times B : \texttt{Set}</math>

als eine Realisierung der Relation <math>\top : A \looparrowright B</math>, die immer wahr ist. Das Produkt kommt also zusammen mit zwei Funktionen

<math>\displaystyle p_1 : A \times B \to A, \quad p_2 : A \times B \to B,</math>

sodass es für <math>a:A</math> und <math>b:B</math> genau ein <math>x : A \times B</math> gibt mit <math>p_1(x)=a</math> und <math>p_2(x)=b</math>; man schreibt dann <math>x=(a,b)</math>. Das Produkt von <math>A</math> und <math>B</math> ist bis auf Isomorphie eindeutig bestimmt. Für je drei Mengen <math>A,B,C</math> gibt es einen eindeutigen Isomorphismus

<math>\displaystyle A \times (B \times C) \cong (A \times B) \times C</math>

mit <math>(a,(b,c)) \mapsto ((a,b),c)</math>. Wir können also <math>A \times B \times C</math> als irgendeine dieser Mengen definieren zusammen mit den Funktionen nach <math>A</math>, <math>B</math> und <math>C</math>; die Elemente heißen dann geordnete Tripel.

Eine wichtige Eigenschaft, ja sogar alternative Charakterisierung des Produktes lautet: Ist <math>C</math> eine Menge und sind <math>f : C \to A</math>, <math>g : C \to B</math> zwei Funktionen, so gibt es genau eine Funktion <math>h : C \to A \times B</math> mit <math>p_1 \circ h = f</math> und <math>p_2 \circ h = g</math>. Man kann bzw. muss <math>h</math> durch <math>h(c):=(f(c),g(c))</math> definieren.

4. Das Potenzmengenaxiom und Anwendungen

Wir definieren eine Teilmenge einer Menge <math>A</math> als eine Relation

<math>\displaystyle T : 1 \looparrowright A.</math>

Das eindeutig bestimmte Element einer terminalen Menge <math>1</math> bezeichnen wir <math>\star</math>. Anstelle von <math>T(\star,a)</math> für <math>a:A</math> schreiben wir auch

<math>\displaystyle a \in T.</math>

Hierbei handelt es sich um eine Aussage. Beachte, dass die Typdeklaration <math>a:T</math> keinen Sinn ergeben würde, weil <math>T</math> nicht vom Typ <math>\texttt{Set}</math> ist. Den Typ <math>1 \looparrowright A</math> bezeichnen wir ebenfalls mit

<math>\displaystyle \subseteq A.</math>

Aus Axiom 1 folgt, dass es für jede in der Prädikatenlogik erster Stufe formulierte Aussage <math>\phi(a)</math> über Elemente <math>a:A</math> genau eine Teilmenge <math>T:\, \subseteq A</math> gibt mit

<math>\displaystyle \forall a : A. \, \phi(a) \Longleftrightarrow a \in T.</math>

Aus Axiom 2 folgt außerdem, dass es für jede Teilmenge <math>T :\, \subseteq A</math> eine Menge <math>|T|</math> zusammen mit einer injektiven Funktion

<math>\displaystyle \iota : |T| \to A</math>

gibt, sodass <math>a:A</math> genau dann gleich <math>\iota(t)</math> für ein <math>t : |T|</math> ist, wenn <math>a \in T</math> gilt. Diese Menge <math>|T|</math> ist zusammen mit der Funktion <math>|T| \to A</math> bis auf Isomorphie eindeutig durch <math>T</math> bestimmt. Das Komplement von <math>T:\, \subseteq A</math> ist die Teilmenge <math>T^c : \, \subseteq A</math>, die aus den Elementen <math>a:A</math> besteht mit <math>a \notin T</math>. Zwei Teilmengen <math>T</math> und <math>T'</math> einer Menge <math>A</math> heißen disjunkt, wenn für kein <math>a:A</math> sowohl <math>a \in T</math> als auch <math>a \in T'</math> gilt.

Als Anwendung können wir jede Funktion <math>f : A \to B</math> schreiben als die Komposition einer surjektiven Funktion <math>p : A \to C</math> mit einer injektiven Funktion <math>i : C \to B</math>: Sei nämlich die Teilmenge <math>T</math> von <math>B</math> dadurch definiert, dass <math>b \in T</math> genau dann gilt, wenn es ein <math>a:A</math> gibt mit <math>f(a)=b</math>, und sei <math>C=|T|</math> zusammen mit der zugehörigen injektiven Funktion <math>i : C \to B</math>. Die Funktion <math>p : A \to C</math> sei definiert durch <math>p(a,c) \Leftrightarrow f(a)=i(c)</math>. Man kann sich überlegen, dass die Menge <math>C</math> zusammen mit den Funktionen <math>p</math> und <math>i</math> bis auf Isomorphie eindeutig bestimmt ist. Sie heißt das Bild von <math>f</math> und wird mit <math>\Bild(f)</math> bezeichnet.

Das nächste Axiom besagt grob besagt, dass wir die Teilmengen einer Menge zu einer neuen Menge zusammenfassen können.

Axiom 3. Für jede Menge <math>A:\texttt{Set}</math> gibt es eine Menge

<math>\displaystyle P(A) : \texttt{Set},</math>

genannte eine Potenzmenge von <math>A</math>, und eine Relation

<math>\displaystyle \varepsilon : A \looparrowright P(A),</math>

sodass es für jede Teilmenge <math>T: \,  \subseteq A</math> genau ein Element <math>t : P(A)</math> gibt, sodass für alle <math>a:A</math> gilt:

<math>\displaystyle a \in T \Longleftrightarrow \varepsilon(a,t)</math><math>\blacktriangleleft</math>

Eine Potenzmenge <math>P(A)</math> ist zusammen mit der Relation <math>\varepsilon : A \looparrowright P(A)</math> bis auf Isomorphie eindeutig bestimmt. Das Axiom besagt, dass es eine 1:1 Beziehung zwischen Elementen von <math>P(A)</math> und Teilmengen von <math>A</math> gibt, also zwischen Funktionen <math>1 \to P(A)</math> und Relationen <math>1 \looparrowright A</math>. Allgemeiner können wir daraus für jede Menge <math>B</math> eine 1:1 Beziehung zwischen Funktionen <math>B \to P(A)</math> und Relationen <math>A \looparrowright B</math> ableiten: Ist <math>f : B \to P(A)</math> eine Funktion, so sei die Relation <math>R : A \looparrowright B</math> mithilfe von Axiom 1 definiert durch

<math>\displaystyle R(a,b) \Longleftrightarrow \varepsilon(a,f(b)).</math>

Ist umgekehrt <math>R : A \looparrowright B</math> eine Relation und <math>b:B</math> ein Element, so erhalten wir mit Axiom 1 die Teilmenge von <math>A</math>, bestehend aus den <math>a : A</math> mit <math>R(a,b)</math>, und wählen dann mit Axiom 3 das eindeutige Element <math>t : P(A)</math>, sodass <math>R(a,b) \Leftrightarrow \varepsilon(a,t)</math> für alle <math>a:A</math> gilt. Es erklärt also <math>f(b) := t</math> eine Funktion <math>f : B \to P(A)</math> mit <math>R(a,b) \Leftrightarrow \varepsilon(a,f(b))</math>.

Als Anwendung konstruieren wir für je zwei Mengen <math>A:\texttt{Set}</math> und <math>B:\texttt{Set}</math> die Menge der Funktionen

<math>\displaystyle \mathrm{Fun}(A,B) : \texttt{Set}</math>

von <math>A</math> nach <math>B</math>. Wir definieren dazu mit Axiom 1 die Teilmenge <math>F : \, \subseteq P(A \times B)</math> dadurch, dass <math>f \in F</math> genau dann gilt, wenn es für alle <math>a:A</math> genau ein <math>b:B</math> gibt mit <math>\varepsilon((a,b),f)</math>. Es sei <math>\mathrm{Fun}(A,B):=|F|</math> die Realisierung und <math>|F| \to P(A \times B)</math> die zugehörige injektive Funktion. Wir sehen, dass es eine 1:1 Beziehung zwischen den Elementen der Menge <math>\mathrm{Fun}(A,B)</math> und den Funktionen <math>A \to B</math> gibt: Wenn <math>f : A \to B</math> eine Funktion ist, so definieren wir ihren Graphen <math>\Gamma_f</math> als die Teilmenge von <math>A \times B</math>, bestehend aus den Paaren <math>(a,b)</math> mit <math>b=f(a)</math>. Dazu korrespondiert ein Element von <math>P(A \times B)</math>, welches offenbar zu <math>|F|</math> gehört, das heißt im Bild von <math>|F| \to P(A \times B)</math> liegt. Diese Zuordnung lässt sich auch umkehren.
 
Sind <math>A:\texttt{Set}</math> und <math>B:\texttt{Set}</math> zwei Mengen, so definieren wir ihr Koprodukt oder auch ihre disjunkte Vereinigung

<math>\displaystyle A \sqcup B : \texttt{Set}</math>

als eine Realisierung der Teilmenge von <math>P(A) \times P(B)</math>, die aus den <math>(\{a\},0)</math> mit <math>a : A</math> und den <math>(0,\{b\})</math> mit <math>b : B</math> besteht. Hierbei sei das Element <math>\{a\}:P(A)</math> definiert durch die Teilmenge von <math>A</math>, die nur <math>a</math> enthält, und <math>0 : P(B)</math> sei definiert durch die Teilmenge von <math>B</math>, die aus keinem Element besteht. Es gibt zwei injektive Funktionen

<math>\iota_1 : A \to A \sqcup B,\, a \mapsto (\{a\},0),\medskip\\\iota_2 : B \to A \sqcup B,\, b \mapsto (0,\{b\}).</math>
 
Jedes Element von <math>A \sqcup B</math> ist von der Form <math>\iota_1(a)</math> für ein Element <math>a:A</math> oder von der Form <math>\iota_2(b)</math> für ein Element <math>b:B</math>, aber beides gleichzeitig kann nicht auftreten: Es gilt <math>\iota_1(a) \neq \iota_2(b)</math> für alle <math>a:A</math> und <math>b:B</math> wegen <math>a \in p_1(\iota_1(a))</math> und <math>a \notin p_1(\iota_2(b))</math>. Daraus folgt leicht die folgende Eigenschaft: Ist <math>C</math> eine Menge und sind <math>f : A \to C</math>, <math>g : B \to C</math> zwei Funktionen, so gibt es genau eine Funktion <math>h : A \sqcup B \to C</math> mit <math>h \circ \iota_1 = f</math> und <math>h \circ \iota_2 = g</math>. Durch diese Eigenschaft ist das Koprodukt bis auf Isomorphie eindeutig festgelegt.
 
Eine Relation <math>R : A \looparrowright A</math> heißt Äquivalenzrelation, wenn sie die folgenden Eigenschaften erfüllt:

<math>R</math> ist reflexiv: Für alle <math>a:A</math> gilt <math>R(a,a)</math>.
<math>R</math> ist symmetrisch: Für alle <math>a:A</math>, <math>b:A</math> gilt <math>R(a,b) \Longleftrightarrow R(b,a)</math>.
<math>R</math> ist transitiv: Für alle <math>a:A</math>, <math>b:A</math>, <math>c:A</math> gilt: <math>R(a,b) \wedge R(b,c) \Longrightarrow R(a,c)</math>.
 
Wir definieren die Quotientenmenge <math>A/R</math> wie folgt: Zu <math>R</math> gehört die Funktion <math>A \to P(A)</math>, die <math>a:A</math> auf die (als Element von <math>P(A)</math> aufgefasste) Teilmenge der <math>b:A</math> mit <math>R(a,b)</math> schickt. Diese Teilmenge heißt die Äquivalenzklasse von <math>a</math>. Es sei

<math>\displaystyle A \xrightarrow{~p~} A/R \xrightarrow{~i~} P(A)</math>

eine Bildzerlegung dieser Funktion. Wir nennen <math>p</math> die kanonische Projektion. Es ist also <math>p</math> surjektiv, und man überlegt sich

<math>\displaystyle p(a)=p(b) \Longleftrightarrow R(a,b)</math>

für alle <math>a:A</math>, <math>b:A</math>. Ist umgekehrt <math>f : A \to Y</math> eine Funktion mit der Eigenschaft <math>R(a,b) \Rightarrow f(a)=f(b)</math> für alle <math>a:A</math>, <math>b:A</math>, so gibt es genau eine Funktion

<math>\displaystyle \overline{f} : A/R \to Y</math>

mit <math>\overline{f} \circ p = f</math>. Die Eindeutigkeit folgt aus der Surjektivität von <math>p</math>, zur Existenz definiere man für <math>u : A/R</math> und <math>y : Y</math>

<math>\displaystyle \overline{f}(u,y) \Longleftrightarrow \exists a : A.\, u = p(a) \wedge f(a) = y.</math>

Durch diese Eigenschaft ist <math>A/R</math> zusammen mit der kanonischen Projektion <math>p : A \to A/R</math> bis auf Isomorphie eindeutig festgelegt.

5. Axiome zur Unendlichkeit

Mit den bisherigen Axiomen kann man bereits einige Grundlagen der Mengenlehre und der Mathematik entwickeln. Um aber auch über unendliche Objekte zu sprechen, insbesondere unendliche Folgen, brauchen wir die Menge der natürlichen Zahlen, die durch das folgende Axiom postuliert wird (welches Axiom 0 redundant macht):  

Axiom 4. Es gibt eine Menge <math>N</math> zusammen mit einem Element <math>0 : N</math> und einer injektiven Funktion <math>S : N \to N</math>, sodass <math>S(n) \neq 0</math> für alle <math>n:N</math> gilt.<math>\blacktriangleleft</math>

Die Elemente

<math>\displaystyle 0, \quad 1:=S(0), \quad 2:=S(S(0)), \quad 3:=S(S(S(0))), \quad \dotsc</math>

von <math>N</math> sind dann paarweise verschieden. Wenn wir ein solches Tripel <math>(N,0,S)</math> haben, definieren wir die Menge der natürlichen Zahlen

<math>\displaystyle \mathds{N} : \texttt{Set}</math>

als eine Realisierung der kleinsten Teilmenge von <math>N</math>, die <math>0</math> enthält und unter <math>S</math> abgeschlossen ist. Die Elemente von <math>\mathds{N}</math> heißen entsprechend natürliche Zahlen. Die Existenz von <math>\mathds{N}</math> können wir so begründen: Es sei <math>\mathds{N}</math> die Realisierung der Teilmenge <math>\hat{\mathds{N}} :\, \subseteq N</math>, bestehend aus den <math>n : N</math>, für die gilt: Ist <math>T</math> eine Teilmenge von <math>N</math> mit <math>0 \in T</math> und <math>\forall m : N. \, m \in T \Rightarrow S(m) \in T</math>, so gilt <math>n \in T</math>.
 
Aus der Definition von <math>\mathds{N}</math> folgt das Induktionsprinzip: Ist <math>T : \, \subseteq \mathds{N}</math> mit <math>0 \in T</math> und

<math>\displaystyle n \in T \Longrightarrow S(n) \in T</math>

für alle <math>n : \mathds{N}</math>, so folgt bereits <math>n \in T</math> für alle <math>n : \mathds{N}</math>, d.h. <math>|T| \to \mathds{N}</math> ist ein Isomorphismus. Dazu betrachten wir einfach die Teilmenge <math>T' : \, \subseteq N</math>, die aus den <math>n : N</math> besteht, für die gilt: Wenn <math>m : \mathds{N}</math> ein Urbild von <math>n</math> unter der injektiven Funktion <math>\mathds{N} \to N</math> ist, so gilt <math>m \in T</math>. Wenn <math>n</math> kein Urbild hat, fordern wir nichts. Nun wenden wir die obige Definition an.
 
Eine zentrale Eigenschaft des Tripels <math>(\mathds{N},0,S)</math> ist der folgende Rekursionssatz: Ist <math>A:\texttt{Set}</math> eine Menge, <math>a_0 : A</math> ein Element und <math>R : A \to A</math> eine Funktion, so existiert genau eine Funktion <math>f : \mathds{N} \to A</math> mit <math>f(0)=a_0</math> und

<math>\displaystyle f(S(n))=R(f(n))</math>

für alle <math>n : \mathds{N}</math>. Wir skizzieren den Beweis: Die Eindeutigkeit folgt leicht aus dem Induktionsprinzip. Zur Konstruktion nennen wir eine Relation <math>F : \mathds{N} \looparrowright A</math> gut, wenn <math>F(0,a_0)</math> gilt und <math>F(n,a) \Rightarrow F(S(n),R(a))</math> für alle <math>n : \mathds{N}</math> und <math>a : A</math> gilt. Wir definieren dann die Relation <math>f : \mathds{N} \looparrowright A</math> wiefolgt: Für <math>n : \mathds{N}</math> und <math>a : A</math> gelte <math>f(n,a)</math>, wenn für jede gute Relation <math>F : \mathds{N} \looparrowright A</math> die Aussage <math>F(n,a)</math> gilt. Dann sieht man, dass <math>f</math> ebenfalls gut ist. Es bleibt zu zeigen, dass <math>f</math> eine Funktion ist. Sei dazu <math>T</math> die Teilmenge von <math>\mathds{N}</math>, die aus den <math>n : \mathds{N}</math> besteht, für die es genau ein <math>a : A</math> gibt mit <math>f(n,a)</math>. Es sei nun dem Leser überlassen, zu prüfen, dass <math>0 \in T</math> gilt und dass <math>n \in T \Rightarrow S(n) \in T</math> für alle <math>n : \mathds{N}</math> gilt. Aus dem Induktionsprinzip folgt daher die Behauptung.
 
Aus dem Rekursionssatz folgt, dass das Tripel <math>(\mathds{N},0,S)</math> bis auf Isomorphie eindeutig bestimmt ist. Außerdem lassen sich damit die üblichen Rechenoperationen (Addition, Multiplikation, Potenzierung) auf <math>\mathds{N}</math> definieren. Ihre Eigenschaften lassen sich mithilfe des Induktionsprinzips beweisen. Es gilt insbesondere <math>S(n)=n+1</math> für <math>n:\mathds{N}</math>.
 
Es bezeichne <math>\mathds{N}^+</math> die Realisierung der Teilmenge der <math>n : \mathds{N}</math> mit <math>n \neq 0</math>. Diese kommt mit einer injektiven Funktion <math>\iota : \mathds{N}^+ \to \mathds{N}</math>. Die Menge der ganzen Zahlen <math>\mathds{Z}</math> lässt sich als die Quotientenmenge von <math>\mathds{N} \times \mathds{N}^+</math> nach der durch

<math>\displaystyle R\bigl((a,b),(c,d)\bigr) \Longleftrightarrow a+\iota(d)=b+\iota(c)</math>

definierten Äquivalenzrelation <math>R</math> definieren. (Sie lässt sich auch strukturell charakterisieren mithilfe der ganzen Zahl <math>0 : \mathds{Z}</math> und einer bijektiven Nachfolgerfunktion <math>S : \mathds{Z} \to \mathds{Z}</math>.) Ganz ähnlich lässt sich die Menge der rationalen Zahlen <math>\mathds{Q}</math> als Quotientenmenge von <math>\mathds{Z} \times \mathds{N}^+</math> konstruieren. Schließlich lässt sich die Menge der reellen Zahlen <math>\mathds{R}</math> zum Beispiel als die Menge der Dedekindschnitte in <math>\mathds{Q}</math>, also als Realisierung einer Teilmenge von <math>P(\mathds{Q})</math> konstruieren. Wenn man möchte, kann man hier noch mit den komplexen Zahlen und den Quaternionen fortfahren. Für diese Zahlenmengen gibt es jeweils injektive Funktionen

<math>\displaystyle \mathds{N} \to \mathds{Z} \to \mathds{Q} \to \mathds{R} \to \mathds{C} \to \mathds{H}.</math>

Weil ein Element immer nur einer Menge angehört, ist die natürliche Zahl <math>2 : \mathds{N}</math> nicht identisch mit der ganzen Zahl <math>2 : \mathds{Z}</math> ist (bzw. diese Aussage wäre in unserem System nicht wohldefiniert). Vielmehr meinen wir mit der ganzen Zahl <math>2 : \mathds{Z}</math> eigentlich das Bild von <math>2 : \mathds{N}</math> unter der injektiven Funktion <math>\mathds{N} \to \mathds{Z}</math>, welche in der obigen Konstruktion <math>n : \mathds{N}</math> auf die Äquivalenzklasse von <math>(n,0)</math> schickt. Wenn man <math>\mathds{C}</math> durch <math>\mathds{R} \times \mathds{R}</math> mit den üblichen Rechenoperationen definiert, ist die injektive Funktion <math>\mathds{R} \to \mathds{C}</math> durch <math>a \mapsto (a,0)</math> gegeben, wobei <math>0:\mathds{R}</math>. Hier wird besonders klar, warum man zwischen <math>a : \mathds{R}</math> und <math>(a,0) : \mathds{C}</math> unterscheiden sollte, auch wenn man letzteres Element üblicherweise einfach als <math>a : \mathds{C}</math> schreibt.

Für <math>n:\mathds{N}</math>, <math>m:\mathds{N}</math> sei <math>n < m</math> rekursiv durch

<math>\displaystyle \neg(n < 0),\quad n<m+1 \Longleftrightarrow n=m \vee n<m</math>

definiert. Was wir hier eigentlich rekursiv definieren, ist die Funktion <math>\mathds{N} \to P(\mathds{N})</math>, die <math>m:\mathds{N}</math> auf die Menge der <math>n : \mathds{N}</math> mit <math>n < m</math> schickt. Diese bezeichnen wir mit <math>\{0,\dotsc,m\}</math> bzw. ihre Realisierung mit <math>\mathds{N}_{<m}</math>. Wenn wir die Null noch herausnehmen, erhalten wir die Teilmenge

<math>\displaystyle [m] := \{1,\dotsc,m\}</math>

von <math>\mathds{N}</math>. Eine Menge <math>X</math> heißt endlich, wenn es eine natürliche Zahl <math>n:\mathds{N}</math> und eine bijektive Funktion <math>|[n]| \to X</math> gibt. Man kann zeigen, dass <math>n</math> eindeutig bestimmt ist und nennt <math>\# X := n</math> die Kardinalität von <math>X</math>. Mengen, die nicht endlich sind, heißen unendlich.
 
Das nächste Axiom ermöglicht es uns grob gesagt, Konstruktionen von sehr großen Mengen durchzuführen. (Die Formulierung ist etwas anders als bei Michael Shulman, aber die Äquivalenz ist leicht zu sehen.)
 
Axiom 5. Sei <math>A</math> eine Menge. Sei <math>\psi(a,B)</math> eine Aussage in der Prädikatenlogik erster Stufe über Elemente <math>a:A</math> und Mengen <math>B</math>. Für alle Elemente <math>a:A</math> gebe es eine Menge <math>B</math> mit <math>\psi(a,B)</math>. Dann gibt es Mengen <math>I</math> und <math>U</math> sowie Funktionen <math>p : I \to A</math> und <math>X : I \to P(U)</math>, sodass gilt:

• Für alle <math>i : I</math> gilt <math>\psi(p(i),|X(i)|)</math>.

<math>p</math> ist surjektiv.<math>\blacktriangleleft</math>

Die Vorstellung ist folgende: Sagen wir, dass einem Element <math>a:A</math> die Menge <math>B</math> zugeordnet wird, wenn <math>\psi(a,B)</math> gilt. Einem Element von <math>A</math> können durchaus mehrere Mengen zugeordnet werden, aber jedem Element wird mindestens eine Menge zugeordnet. Das Axiom sagt nun, dass wir eine Parametrisierung von <math>A</math> finden, also eine surjektive Funktion <math>p : I \to A</math>, sodass für jeden Index <math>i : I</math> eine ausgewählte Menge <math>|X(i)|</math> dem Element <math>p(i):A</math> zugeordnet wird. Diese Mengen <math>|X(i)|</math> sind die Realisierungen von Teilmengen <math>X(i)</math> einer groß genug gewählten Menge <math>U</math>. Das Axiom kann für endliche Mengen <math>A</math> aus den vorherigen Axiomen abgeleitet werden, macht also nur für unendliche Mengen <math>A</math> eine wirkliche Aussage.

Damit sind bereits alle Axiome von <math>\mathsf{SEAR}</math> beschrieben.
 
Die Bedeutung von Axiom 5 bzw. des dazu analogen, sogenannten Ersetzungsaxioms in <math>\mathsf{ZF}</math> wird kontrovers diskutiert. Das liegt daran, dass ein sehr großer Prozentteil der Mathematik auch ohne das Ersetzungsaxiom entwickelt werden kann. Der Mengentheoretiker Kenneth Kunen fordert die Leser seines Buches Set theory in der Aufgabe IV.9 sogar dazu auf, zu überprüfen, dass mehr als 99 Prozent der Mathematik ohne das Ersetzungsaxiom auskommt. Das könnte auch erklären, warum das kategorientheoretische Axiomensystem <math>\mathsf{ETCS}</math> von Lawvere in seiner ursprünglichen Fassung kein zum Ersetzungsaxiom analoges Axiom beinhaltet.

Als Anwendung von Axiom 5 konstruieren wir, für jede Menge <math>S</math>, eine Folge von Mengen

<math>\displaystyle S, \quad P(S), \quad P(P(S)), \quad \dotsc .</math>

Hier sollte, von <math>S</math> abgesehen, jede Menge eine Potenzmenge der vorherigen Menge sein. Beachte, dass hier der Rekursionssatz nicht anwendbar ist, weil a priori die genannten Mengen in keiner Menge enthalten sind bzw. dies auch nicht gehen würde, weil Mengen keine Mengen enthalten. Wenn überhaupt, dann können wir erwarten, dass die Mengen isomorph sind zu Realisierungen von Teilmengen einer festen, genügend großen Menge <math>U</math>. Wir wiederholen noch einmal, dass es in <math>\mathsf{SEAR}</math> nicht die Potenzmenge einer Menge gibt, sondern dass wir jede Menge <math>B</math> zusammen mit einer Relation <math>\eps : A \looparrowright B</math> eine Potenzmenge von <math>A</math> nennen, wenn <math>\eps</math> wie in Axiom 3 eine 1:1 Korrespondenz zwischen den Teilmengen von <math>A</math> und den Elementen von <math>B</math> vermittelt. Wir suchen demnach eine Menge <math>U</math>, eine Funktion <math>X : \mathds{N} \to P(U)</math>, einen Isomorphismus <math>f : |X(0)| \to S</math> sowie eine Relation <math>\eps : U \looparrowright U</math>, sodass für jede natürliche Zahl <math>n : \mathds{N}</math> gilt, dass <math>|X(n+1)|</math> zusammen mit der Einschränkung <math>\eps_n : |X(n)| \looparrowright |X(n+1)|</math> von <math>\eps</math> eine Potenzmenge von <math>|X(n)|</math> ist.
 
Wir skizzieren nun den Beweis für die Existenz von <math>(U,X,f,\eps)</math>. Die Idee ist, induktiv für natürliche Zahlen <math>n : \mathds{N}</math> die Existenz passender Teilmengen <math>X(0),\dotsc,X(n)</math> etc. zu zeigen und dann Ende Axiom 5 anzuwenden. Für <math>n : \mathds{N}</math>, <math>U : \texttt{Set}</math>, <math>X : \mathds{N} \to P(U)</math>, <math>f : |X(0)| \to S</math>, <math>\eps : U \looparrowright U</math> definieren wir die Aussage <math>\phi(n,U,X,f,\eps)</math> dadurch, dass <math>f</math> ein Isomorphismus ist und für jede natürliche Zahl <math>m:\mathds{N}_{<n}</math> die Menge <math>|X(m+1)|</math> mit der Einschränkung <math>\eps_m : |X(m)| \looparrowright |X(m+1)|</math> von <math>\eps</math> eine Potenzmenge von <math>|X(m)|</math> ist. Für <math>n:\mathds{N}</math> und <math>U:\texttt{Set}</math> sei weiter <math>\psi(n,U)</math> dadurch definiert, dass es <math>X : \mathds{N} \to P(U)</math>, <math>f : |X(0)| \to S</math>, <math>\eps : U \looparrowright U</math> gibt, sodass <math>\phi(n,U,X,f,\eps)</math> gilt. Per Induktion nach <math>n : \mathds{N}</math> lässt sich zeigen: Für alle <math>n : \mathds{N}</math> gibt es <math>U : \texttt{Set}</math> mit <math>\psi(n,U)</math>. Im Induktionsschritt benutzen wir die Existenz von Koprodukten und von Potenzmengen. Jetzt können wir Axiom 5 anwenden und erhalten Funktionen <math>p : I \to \mathds{N}</math>, <math>V : I \to P(U)</math> wie dort beschrieben. Für jeden Index <math>i : I</math> gilt also <math>\psi(p(i),|V(i)|)</math>, d.h. es gibt <math>X(i) : \mathds{N} \to P(|V(i)|)</math>, <math>f(i) : |X(0)| \to S</math>, <math>\eps(i) : |V(i)| \looparrowright |V(i)|</math>, sodass <math>\phi(p(i),|V(i)|,X(i),f(i),\eps(i))</math> gilt. Was wir hier angedeutet haben, nämlich dass <math>X(i)</math>, <math>f(i)</math> und <math>\eps(i)</math> funktional von <math>i</math> abhängen, lässt sich tatsächlich durch eine Reparametrisierung erreichen. Weil Potenzmengen bis auf Isomorphie eindeutig bestimmt sind, können wir zu jeder natürlichen Zahl <math>n</math> einen Index <math>i</math> mit <math>p(i)=n</math> wählen und ihr dann die Folge von Teilmengen <math>X(i) : \mathds{N} \to P(|V(i)|) \to P(U)</math> zuordnen, ohne dass es hierbei auf die Wahl von <math>i</math> ankommen würde. Wir können daher annehmen, dass <math>p : \mathds{N} \to \mathds{N}</math> die Identität ist. Schließlich definieren wir die gesuchten Mengen durch eine Art Diagonalisierung mittels <math>n \mapsto X(n)(n)</math>.
 
Das System <math>\mathsf{SEARC}</math> entsteht aus <math>\mathsf{SEAR}</math> durch Hinzufügen des folgenden Auswahlaxioms:

Axiom 6. Sind <math>A,B</math> zwei Mengen und ist <math>f : A \to B</math> eine surjektive Funktion, so gibt es eine Funktion <math>g : B \to A</math> mit <math>f \circ g = \id_B</math>.<math>\blacktriangleleft</math>

Die Intuition hierbei ist, dass es zwar für jedes <math>b : B</math> ein Urbild <math>a : A</math> gibt mit <math>f(a)=b</math>, dass dies aber zur Definition einer konkreten Funktion <math>g : B \to A</math> mit <math>f(g(b))=b</math> nicht ohne Weiteres ausreicht, weil unklar ist, welches Urbild <math>a</math> man für <math>g(b)</math> genau auswählen sollte. Das Auswahlaxiom sagt also, dass es eine Funktion <math>g</math> gibt, welche diese Auswahl für alle Elemente von <math>B</math> gleichzeitig trifft.

Wenn <math>B</math> (oder sogar <math>A</math>) endlich ist, lässt sich das Auswahlaxiom mit einer Induktion nach der Kardinalität von <math>B</math> aus den Axiomen 1 bis 4 ableiten. Das Auswahlaxiom macht also vor allem eine Aussage über unendliche Mengen.
 
Eine äquivalente Formulierung des Auswahlaxioms lautet: Ist <math>R : A \looparrowright B</math> eine Relation mit der Eigenschaft, dass es für alle <math>a : A</math> ein <math>b : B</math> gibt mit <math>R(a,b)</math>, so gibt es eine Funktion <math>f : A \to B</math> mit <math>R(a,f(a))</math> für alle <math>a:A</math>.

Es gibt eine Reihe weiterer nützlicher Aussagen aus der Mathematik, die zum Auswahlaxiom äquivalent sind, zum Beispiel das Zornsche Lemma, der Wohlordnungssatz, die Existenz von Basen in Vektorräumen und die Existenz von maximalen Idealen in nichttrivialen Ringen.
 
Für den Nachweis, dass <math>\mathsf{SEAR}</math> und <math>\mathsf{ZF}</math> equikonsistent sind, verweisen wir auf den nLab-Artikel von Michael Shulman. Aus einem <math>\mathsf{ZF}</math>-Modell ein <math>\mathsf{SEAR}</math>-Modell zu konstruieren, ist ganz einfach. Zur Konstruktion eines <math>\mathsf{ZF}</math>-Modells aus einem <math>\mathsf{SEAR}</math>-Modell verwendet man allerdings Äquivalenzklassen von gewissen gerichteten Graphen als <math>\mathsf{ZF}</math>-Mengen, welche die aus <math>\mathsf{ZF}</math> bekannten Elementschachtelungen modellieren sollen. Entsprechend ist <math>\mathsf{SEARC}</math> zu <math>\mathsf{ZFC}</math> equikonsistent. Mit <math>\mathsf{SEAR}</math> bzw. <math>\mathsf{SEARC}</math> lassen sich nun praktisch alle Begriffe der alltäglichen Mathematik ableiten, und man kann mit ihnen weitestgehend wie gewohnt umgehen. Wir werden das im nächsten Abschnitt exemplarisch anhand der Definition eines Maßraumes aufzeigen.
 
Auch wenn <math>\mathsf{SEAR}</math> viele Probleme von <math>\mathsf{ZF}</math> beseitigt, ist dieses System immer noch nicht perfekt. Wenn wir schon mit Typen arbeiten, wäre es nur konsequent, die üblichen Definitionen von Sorten mathematischer Objekte als Typkonstruktoren anzusehen. So sollte zum Beispiel die übliche Definition einer Gruppe einen Typ <math>\texttt{Grp}</math> konstruieren und die Typdeklaration <math>G:\texttt{Grp}</math> bedeuten, dass <math>G</math> eine Gruppe ist. (In <math>\mathsf{SEAR}</math> können wir lediglich <math>\forall X : \texttt{Set}.\, \forall m : X \times X \to X.\, \text{'Gruppenaxiome'} \Rightarrow \dotsc</math> formulieren.) Das und einiges mehr ist in Martin-Löfs Typentheorie möglich. Diese wird zusammen mit einigen, aus der Homotopietheorie motivierten Axiomen auch Homotopietypentheorie genannt und stellt noch einmal eine gänzlich andere Fundierung der Mathematik dar. Bemerkenswert ist, dass hier im Gegensatz zu <math>\mathsf{ZF}</math>, <math>\mathsf{ETCS}</math> und <math>\mathsf{SEAR}</math> keine Prädikatenlogik vorausgesetzt werden muss bzw. diese bereits in der Typentheorie enthalten ist. Eine leicht verständliche Motivation für die (Homotopie-)Typentheorie hat Michael Shulman im nCafé geschrieben. Mehr Details findet man zum Beispiel im nLab.

6. Ein Beispiel: Maßräume

Ein Maßraum ist ein geordnetes Tripel <math>(\Omega,\mathcal{A},\mu)</math>, bestehend aus
 
• einer Menge <math>\Omega</math>,
• einer <math>\sigma</math>-Algebra <math>\mathcal{A}</math> auf <math>\Omega</math>, und
• einem Maß <math>\mu</math> auf <math>\mathcal{A}</math>.
 
Was eine Menge <math>\Omega</math> ist, muss nicht weiter gesagt werden. Eine <math>\sigma</math>-Algebra <math>\mathcal{A}</math> auf <math>\Omega</math> ist eine Teilmenge von <math>P(\Omega)</math>, die die leere Teilmenge <math>0:P(\Omega)</math> enthält, unter der Komplementbildung von Teilmengen

<math>\displaystyle P(\Omega) \to P(\Omega),\, T \mapsto T^c</math>

sowie abzählbaren Vereinigungen abgeschlossen ist. Letzteres bedeutet: Ist <math>X : \mathds{N} \to P(\Omega)</math> eine Funktion, sodass <math>X(n) \in \mathcal{A}</math> für alle <math>n : \mathds{N}</math> gilt, so gilt auch

<math>\displaystyle \bigcup_{n : \mathds{N}} X(n) \in \mathcal{A}.</math>

Dabei ist <math>\bigcup_{n : \mathds{N}} X(n)</math> die Teilmenge von <math>\Omega</math>, die aus den <math>\omega : \Omega</math> besteht, für die es ein <math>n : \mathds{N}</math> gibt mit <math>\omega \in X(n)</math> (bzw. eigentlich <math>\eps(\omega,X(n))</math>; wir benutzen hier stillschweigend die Korrespondenz zwischen Teilmengen von <math>\Omega</math> und Elementen von <math>P(\Omega)</math>).
 
Beachte, dass <math>\mathcal{A}</math> keine Menge ist. Die Realisierung <math>|\mathcal{A}|</math> hingegen ist eine Menge, und deren Elemente sind gewisse Teilmengen <math>A</math> von <math>\Omega</math>, die <math>\mathcal{A}</math>-messbar genannt werden und durch <math>A \in \mathcal{A}</math> charakterisiert sind. Diese sind ebenfalls keine Mengen, haben aber Mengen als Realisierungen, die wiederum Elemente besitzen können. In <math>\mathsf{ZF}</math> würde man die Elementkette <math>\omega \in A \in \mathcal{A}</math> für eine <math>\mathcal{A}</math>-messbare Menge <math>A</math>, die <math>\omega</math> enthält, anfinden. In <math>\mathsf{SEAR}</math> gibt es stattdessen die Typdeklarationen

<math>\displaystyle \omega : |A|, \quad A : |\mathcal{A}|.</math>

Ein (positives) Maß auf <math>\mathcal{A}</math> ist eine Funktion

<math>\displaystyle \mu : |\mathcal{A}| \to \mathds{R}_{\geq 0} \sqcup \{\infty\}</math>

mit zwei Eigenschaften: Erstens gilt für das Element <math>0 : |\mathcal{A}|</math>, das zur leeren Teilmenge gehört, die Gleichung

<math>\displaystyle \mu(0)=0,</math>

wobei rechts natürlich <math>0 : \mathds{R}_{\geq 0} \sqcup \{\infty\}</math> steht. Zweitens gilt für jede Funktion <math>X : \mathds{N} \to P(\Omega)</math> wie oben, sodass zusätzlich für alle <math>n:\mathds{N}</math>, <math>m:\mathds{N}</math> mit <math>n \neq m</math> die Teilmengen <math>X(n)</math>, <math>X(m)</math> von <math>\Omega</math> disjunkt sind, die Gleichung

<math>\displaystyle \mu\left(\bigcup_{n : \mathds{N}} X(n)\right)=\sum_{n : \mathds{N}} \mu(X(n)).</math>

Dabei definiert man die unendliche Summe

<math>\displaystyle \sum_{n : \mathds{N}} a(n) : \mathds{R}_{\geq 0} \sqcup \{\infty\}</math>

für eine Funktion <math>a : \mathds{N} \to \mathds{R}_{\geq 0} \sqcup \{\infty\}</math> als das Supremum (bezüglich der üblichen Ordnungsrelation auf <math>\mathds{R}_{\geq 0} \sqcup \{\infty\}</math>) der endlichen Summen

<math>\displaystyle s(m) = \sum_{n : \mathds{N},\, n < m} a(n)</math>

für <math>m : \mathds{N}</math>, welche sich wiederum rekursiv definieren lassen durch <math>s(0)=0</math> und <math>s(m+1)=s(m)+a(m)</math>.


Link auf diesen Artikel Link auf diesen Artikel  Druckbare Version Druckerfreundliche Version  Einen Freund auf diesen Artikel aufmerksam machen Weitersagen Kommentare zeigen Kommentare  
pdfFür diesen Artikel gibt es keine pdf-Datei


Arbeitsgruppe Alexandria Dieser Artikel ist im Verzeichnis der Arbeitsgruppe Alexandria eingetragen:
: Mathematik :: automatisch eingefügt und unbearbeitet :
SEAR: Mengen, Elemente und Relationen [von Triceratops]  
Eine strukturelle Mengenlehre Die Mathematik wird üblicherweise mithilfe der Mengenlehre fundiert, und die Mengenlehre wird üblicherweise als die Theorie des Axiomensystems mathsf{ZF} von Zermelo und Fraenkel bzw. seiner Varianten angesehen. Es gibt allerdings n
[Die Arbeitsgruppe Alexandria katalogisiert die Artikel auf dem Matheplaneten]

 
Verwandte Links
 
Besucherzähler 1247
 
Aufrufstatistik des Artikels
Insgesamt 6 externe Besuche zwischen 2017.02 und 2017.02 [Anzeigen]
DomainAnzahlProz
http://matheplanet.com350%50 %
http://google.ch116.7%16.7 %
http://google.de233.3%33.3 %

Aufrufer der letzten 5 Tage im Einzelnen
Insgesamt 3 Aufrufe in den letzten 5 Tagen. [Anzeigen]
DatumAufrufer-URL
2017.02.14-2017.02.19 (3x)https://www.google.de/

[Seitenanfang]

" Mathematik: SEAR: Mengen, Elemente und Relationen" | 12 Kommentare
 
Für den Inhalt der Kommentare sind die Verfasser verantwortlich.

Re: SEAR: Mengen, Elemente und Relationen
von tactac am Fr. 23. September 2016 21:23:35


Ein schöner Artikel ganz nach meinem Geschmack.  smile

 [Bearbeiten]

Re: SEAR: Mengen, Elemente und Relationen
von KidinK am Fr. 30. September 2016 10:59:23


Sehr schöner Artikel! Ich habe zwei Fragen. Erstens: Lässt sich so etwas, wie eine Zuordnung zwischen Typen definieren? Ich stelle mir darunter Folgendes vor, auch wenn ich nicht weiß, ob  das typentheoretisch und logisch korrekt formuliert ist. Seien <math>S</math> und <math>T</math> zwei Typen. Eine Zuordnung <math>\varphi\colon S\leadsto T</math> ist eine Formel <math>\varphi(s,t)</math> in Prädikatenlogik erster Stufe über Terme <math>s\colon S</math>, <math>t\colon T</math>, sodass es für jedes <math>s\colon S</math> genau ein <math>t\colon T</math> mit <math>\varphi(s,t)</math> gibt. Man kann das eindeutige <math>t\colon T</math> mit <math>\varphi(s,t)</math> dann als <math>\varphi(s)</math> schreiben.

Nun habe ich die Frage, ob sich der folgende Satz beweisen lässt: Sei <math>I\colon\mathsf{Set}</math>, <math>\varphi\colon I\leadsto\mathsf{Set}</math> eine Zuordnung. Dann gibt es ein <math>K\colon\mathsf{Set}</math> und für jedes <math>i\colon I</math> eine Funktion <math>\iota(i)\colon X(i)\longrightarrow K</math>, sodass <math>K</math> ein Koprodukt der <math>X(i)</math> im üblichen Sinne ist.

Nun ist mir während der Formulierung des Satzes gerade noch aufgefallen, dass Zuordnungen zwischen Typen noch gar nicht genügen, um den Satz richtig auszudrücken. Ich brauche ja für ein <math>A\colon\mathsf{Set}</math> eine Familie von Funktionen <math>f(i)\colon X(i)\longrightarrow A</math> mit unterschiedlicher Domäne. Wie kann ich das formulieren?

Als zweites hätte ich noch eine Frage, wieso Shulman wohl Relationen zu primitiven Konzepten gemacht hat und nicht Funktionen. Wäre letzteres nicht viel üblicher für einen Kategorientheoretiker? Man müsste dann davon ausgehen, dass jede Funktion <math>f\colon A\longrightarrow B</math> eine Zuordnung <math>A\leadsto B</math> liefert, und anstelle von Axiom 1, dass umgekehrt jede Zuordnung <math>A\leadsto B</math> von einer eindeutigen Funktion her kommt. Axiom 2 würde ich wohl durch die Existenz von Produkten ersetzen. Vielleicht sogar beliebige Produkte - wenn man das geeignet formulieren könnte; dann hätte man automatisch Funktionenmengen <math>B^A</math>, von denen man zeigen könnte, dass ihre Elemente eindeutig zu Funktionen <math>A\longrightarrow B</math> korrespondieren. Ersetzt man ferner die Existenz von <math>\{0\}</math> durch die Existenz von <math>2:=\{0,1\}</math>, sollte dadurch das Potenzmengenaxiom überflüssig werden. Eine Teilmenge <math>B\subseteq A</math> wäre dann für mich eine injektive Funktion <math>B\colon |B|\longrightarrow A</math> für ein <math>|B|\colon\mathsf{Set}</math>. Für <math>x\colon A</math> würde ich dann <math>x\in A</math> erklären durch <math>\exists y\colon|B|.B(y)=x</math>. Ich würde <math>B\le C</math> erklären durch <math>\forall x\colon A.x\in B\implies x\in C</math> und <math>B\sim C</math> durch <math>B\le C\le B</math>. Es sollte sich hiermit bereits zeigen lassen, dass jede Teilmenge zu einem Element <math>2^A</math> führt, dass die Zuordnung surjektiv ist und dass Teilmengen identifiziert werden, genau dann, wenn <math>B\sim C</math> gilt. Eine Relation wäre natürlich eine Teilmenge von <math>A\times B</math>.

Sollte diese Skizze von <math>\mathsf{SEAF}</math> nicht zu <math>\mathsf{SEAR}</math> äquivalent sein? Falls ja, wieso hat Shulman sich nicht hierfür entschieden?

Liebe Grüße,
KidinK

 [Bearbeiten]

Re: SEAR: Mengen, Elemente und Relationen
von Triceratops am Fr. 30. September 2016 12:10:58


@KidinK: Das sind gute Fragen, über die ich einmal länger nachdenken sollte. Spontane Antworten:

1) Das Problem ist, dass in <math>\mathsf{SEAR}</math> die Gleichheit zwischen Mengen nicht definiert ist. Es ist also nicht klar, was eine Zuordnung <math>\phi : I \leadsto \texttt{Set}</math> in deinem Sinne sein soll. Man kann lediglich verlangen, dass es für jedes <math>i:I</math> ein <math>A:\texttt{Set}</math> gibt mit <math>\phi(i,A)</math>, aber die Eindeutigkeit kann man nicht verlangen. Ich verstehe den Hintergrund deiner Frage, es geht halt um die Existenz von beliebigen Koprodukten von Mengen, und in gewisser Weise habe ich mich damit im Beispiel zum Ersetzungsaxiom beschäftigt. Es scheint so zu sein, dass wir eine universelle Eigenschaft von <math>A</math> in Abhängigkeit von <math>i</math> gegeben haben müssen. Ein typisches Beispiel ist die Zuordnung <math>\mathds{N} \leadsto \texttt{Set}</math>, <math>n \mapsto X^n</math> für eine Menge <math>X</math>. Es ist <math>X^n</math> nicht eindeutig bestimmt, sondern lediglich bis auf Isomorphie. Hier kann man allerdings <math>\coprod_{n \in \mathds{N}} X^n</math> noch direkt konstruieren. Aber im allgemeinen Fall ist mir leider nicht klar, wie man überhaupt die Existenz von Koprodukten formulieren sollte. Vielleicht hast du weitere Vorschläge dafür? Die (Martin-Löf-)Typentheorie erscheint mir in vielerlei Hinsicht eleganter zu sein. Die Existenz von Koprodukten von Typen ist dort durch abhängige <math>\Sigma</math>-Typen gesichert.
 
2) Axiom 2 ist mehr als nur die Existenz von binären Produkten, sondern endlicher Limites, oder? Die Existenz von beliebigen Produkten kann man vermutlich nicht so einfach formulieren (s.o.) und gerade deshalb spricht man daher zunächst von Funktionenmengen. Ja, die Existenz von Funktionenmengen impliziert die Existenz von Potenzmengen. In der Topostheorie hat sich das Potenzmengenaxiom wohl als primär durchgesetzt, zumal man dann daraus die Existenz des Unterobjektklassifizierers (hier: <math>2</math>) ableiten kann. Deine Definition von Teilmengen als injektive Funktionen wird auch so in <math>\mathsf{ETCS}</math> gewählt. Warum sich Shulman nicht für Funktionen, sondern für Relationen entschieden hat, kann ich nicht genau sagen. Man kann ihn per Mail anschreiben, da habe ich gute Erfahrungen mit gemacht. Eine mögliche Erklärung ist, dass (a) im Alltag, nicht nur auf Mathematik bezogen, Relationen in gewisser Weise noch viel fundamentaler und allgegenwärtiger als Funktionen sind, (b) das Potenzmengenaxiom damit einfacher zu formulieren ist, (c) es bereits eine strukturelle Mengenlehre auf Basis von Funktionen gibt, nämlich <math>\mathsf{ETCS}</math>. Noch zu (a): Der Typ <math>A \looparrowright B</math> ist öfters praxisnaher als der Typ <math>A \to P(B)</math>. Wenn man etwa wissen möchte, ob die Zahl <math>n:\mathds{N}</math> die Zahl <math>m:\mathds{N}</math> teilt, möchte man nicht unbedingt erst die Teilmenge von <math>\mathds{N}</math> der Teiler von <math>m</math> bilden und dann entscheiden müssen, ob <math>n</math> darin enthalten ist.

 [Bearbeiten]

Re: SEAR: Mengen, Elemente und Relationen
von Anonymous am Fr. 30. September 2016 13:51:57


Kleine Bemerkung: Der Link, der eig. zum nlab-Artikel von Mike Shulman verweisen soll (wo dieser nach Aussage des Artikels die Äquikonsitenz von ZFC und SEAR zeigt) funktioniert leider nicht. Man kommt stattdessen auf eine Seite mit dem Text:

"Creating SEAR"
Page "SEAR"" does not exist.
Please create it now, or hit the "back" button in your browser.".

Welche Metatheorie hat Mike Shulman denn benutzt, um diese Äquikonsistenz von ZFC und SEAR zu zeigen? ZFC oder SEAR, oder was ganz anderes?

-----

Ich versteh auch noch nicht ganz, was der Zweck von Axiomatisierungen und Fundierungen der Mathematik ist. Den einzigen Zweck, den ich in Fundierungen momentan sehe, ist, dass man dadurch Dinge wie "Beweisbarkeit in einem Axiomensystem" exakt definieren kann und dann diese Dinge mathematisch untersuchen kann. Oder werden Fundierungen gemacht, um mit ihnen zu arbeiten? Das kann ich mir eher weniger vorstellen, da man ja aus der Mathematik die Begriffe "Relation", "Menge", "Funktion", "Identitätsfunktion", "Äquivalenzrelation" usw. schon kennt, und sich erst danach mit den Fundierungen beschäftigt, obwohl man sich schon ziemlich sicher ist, was die genannten Begriffe bedeuten.

 [Bearbeiten]

Re: SEAR: Mengen, Elemente und Relationen
von Triceratops am Fr. 30. September 2016 14:10:09


@Anonymous:
1) Da war ein " zu wenig im Link. Wird korrigiert. Es ist natürlich derselbe Artikel gemeint wie der, der im Kopfbereich des Artikels verlinkt wird.
2) Es wird keine Metatheorie benötigt.
3) Du schreibst "ziemlich sicher". Es geht bei der Axiomatisierung der Grundlagen der Mathematik darum, sich "absolut sicher" zu sein. Es gibt z.B. kein Konzept von "Funktion", welches per se existiert, sondern wir legen erst einmal fest, wie sich dieses Konzept zu verhalten hat. Und das muss man zumindest einmal gemacht haben. Es gibt verschiedene Axiomatisierungen, und es ist keinesfalls so, dass es am Ende egal ist, welche Axiomatisierung man wählt. Das sieht man aber erst bei komplexeren Fragestellungen. Bei der Homotopietypentheorie sieht man auch ganz deutlich, dass man nicht einmal Mengen als Grundbausteine wählen muss, sondern dass Homotopietypen bzw. <math>\infty</math>-Gruppoide ebenfalls dazu geeignet sind. Ich möchte darauf hier eigentlich nicht weiter eingehen, denn das ist eigentlich eine Frage fürs Forum, die nichts spezifisch mit dem System <math>\mathsf{SEAR}</math> zu tun hat.

 [Bearbeiten]

Re: SEAR: Mengen, Elemente und Relationen
von Ex_Mitglied_46439 am Fr. 30. September 2016 14:31:11


@Tri.: Danke für die supermegaschnelle Antwort!

1) Du meinst wohl "zu viel" statt "zu wenig".
2) Wieso benötigt man dafür keine Metatheorie? In welcher Fundierung arbeitet man, wenn man beweisen will, dass ZFC äquikonsistent zu SEAR ist? (Bzw. welche Fundierung hat Mike dazu benutzt?)
3) Ich denke, es hat mit dem Artikel zu tun. Und zwar frage ich hier nach dem Grund bzw. der Motivation für den Artikel. (Du gibts berechtigterweise schon den Grund an, dass die üblichen "Fundierungen" unnatürlich sind. Aber warum brauchen wir eine natürliche Fundierung? Dass ZFC als pure Mengenlehre Vorteile als Fundierung gegenüber einer natürlichen Fundierung hat, erklärt Prof. Blass hier: mathoverflow.net/q/90945 )
Du sagst, dass es bei Fundierungen darum geht, sich absolut sicher zu sein. Das verstehe ich nicht. Absolut sicher kann man sich doch gar nicht sein (man muss ja irgendwas hinnehmen, sonst gerät man in einen regressus in/ad infinitum: de.wikipedia.org/wiki/Infiniter_Regress )?
Außerdem werden die in dem Artikel behandelten Begriffe "Funktion", "Äquivalenzrelation", "Indentitätsfunktion", usw. durch eine Axiomatisierung wie SEAR nicht klarer, als sie eh schon sind. (Im Gegenteil: Man könnte sogar behaupten, dass Fundierungen genau unsere Vorstellungen von den Begriffen "covern" soll. Wir haben also erst schon eine Vorstellung von den Begriffen; und danach schreiben wir elementare Regeln für den Umgang mit diesen Begriffen auf, die wir dann Axiome nennen.)

 [Bearbeiten]

Re: SEAR: Mengen, Elemente und Relationen
von KidinK am Fr. 30. September 2016 15:35:53


Im Artikel heißt es: "Eine allgemeine Regel der Typentheorie lautet, dass zwei Objekte nur dann miteinander verglichen werden können, wenn sie demselben Typ angehören." Wieso lassen sich denn Objekte des Typs <math>\colon A</math> oder <math>\colon A\longrightarrow B</math> vergleichen, aber nicht Objekte des Typs <math>\mathsf{Set}</math>? Das eigentlich strukturelle an solchen Mengenlehren ist ja auch, dass <math>A\in B</math> verboten wird, und nicht etwa <math>A=B</math>.

Wie man die Existenz von Produkten und Koprodukten formulieren kann, dazu habe ich keine weiteren Ideen. Jedenfalls sollte die Existenz von Produkten aus der Existenz von Koprodukten und Funktionenmengen folgen.

Im Folgenden gehe ich einmal weiter davon aus, dass man Gleichheit zweier Objekte desselben Typs testen kann (und die üblichen Regeln gelten - Gleichheit ist eine Äquivalenzrelation und in jeder Aussage in Prädikatenlogik erster Stufe lassen sich gleiche Objekte auswechseln, ohne dass sich der Wahrheitswert ändert).

Weil beliebige Produkte Probleme liefern, fordere ich zweifache Produkte, sowie Funktionenmengen. Ist nun <math>A\colon\mathsf{Set}</math>, so kann man jeder Teilmenge <math>B\subseteq A</math> eine Funktion <math>\chi_B\colon A\longrightarrow 2</math> zuordnen mit <math>\chi_B(x)=1\iff x\in B</math> für <math>x\colon A</math>. Es gilt <math>\chi_B=\chi_C\iff B\sim C</math>. Ich habe vorhin behauptet, dass jede Funktion <math>A\longrightarrow 2</math> die Form <math>\chi_B</math> hätte, aber das muss man natürlich als Axiom fordern, oder äquivalent dazu das klassische Aussonderungsaxiom. Dann ist auch klar, dass Axiom 2 aus dem Artikel folgt.

"Noch zu (a): Der Typ <math>A \looparrowright B</math> ist öfters praxisnaher als der Typ <math>A \to P(B)</math>. Wenn man etwa wissen möchte, ob die Zahl <math>n:\mathds{N}</math> die Zahl <math>m:\mathds{N}</math> teilt, möchte man nicht unbedingt erst die Teilmenge von <math>\mathds{N}</math> der Teiler von <math>m</math> bilden und dann entscheiden müssen, ob <math>n</math> darin enthalten ist." - Für mich hat eine Relation ja den Typ <math>\subseteq A\times B</math> und nicht etwa <math>A\longrightarrow P(B)</math>. So ist es ja auch üblich.

Liebe Grüße,
KidinK

 [Bearbeiten]

Re: SEAR: Mengen, Elemente und Relationen
von Anonymous am Fr. 30. September 2016 15:42:55


@KidinK: "Wieso lassen sich denn Objekte des Typs <math>\colon A</math> oder <math>\colon A\longrightarrow B</math> vergleichen, aber nicht Objekte des Typs <math>\mathsf{Set}</math>? Das eigentlich strukturelle an solchen Mengenlehren ist ja auch, dass <math>A\in B</math> verboten wird, und nicht etwa <math>A=B</math>."

In materiellen Mengenlehren definiert man die Gleichheit zwischen zwei Mengen $A$ und $B$ durch

<math>A= B:\iff \text{Fuer jedes $x$, $x\in A$ gdw $x\in B$}</math>

Da, wie du selber sagst, "<math>A\in B</math>" in strukturellen Mengenlehren verboten ist, lässt sich dieses Konzept der Gleichheit von Mengen nicht in strukturellen Mengenlehren formalisieren. Es lässt sich aber dennoch über Isomorphie von Mengen sprechen, was ein Ersatz für die Gleichheit von Mengen ist.

 [Bearbeiten]

Re: SEAR: Mengen, Elemente und Relationen
von Triceratops am Sa. 01. Oktober 2016 08:45:33


@3737737ee: Nur zu 3): Natürlich bezieht sich "absolut sicher" nur relativ zu den Axiomen, die ganz am Anfang stehen. Und ja, die Axiome sollen unsere intuitive Vorstellung und unsere Erfahrungen abbilden. Aber es geht bei Axiomensystemen eben darum, dies ein und für alle mal festzulegen und nicht, wie das lange Zeit in der Mathematik üblich war, einfach mal hier und da etwas als "intuitiv richtig" zu bezeichnen oder gar nicht so richtig zu wissen, was man genau verwendet. Das ist notwendigerweise subjektiv und führte dazu, dass jeder Mathematiker in einer potentiell anderen Welt arbeiten würde. Das erschwert die Kommunikation und die Zusammenarbeit ungemein.

@KidinK: Ich habe im Artikel lediglich das in eigenen Worten wiedergegeben, was Shulman sich ausgedacht hat und dazu noch einige Kommentare ergänzt. Die Gleichheit von Mengen ist in SEAR explizit nicht erlaubt. (Übrigens, sowohl in ETCS als auch in der Homotopietypentheorie HoTT ist sie erlaubt.) Und selbst wenn man sie hätte, müsste man noch festlegen, wie sie sich verhält. Naheliegend wäre Extensionalität, aber dieses kann hier nicht einmal formuliert werden. Zum einen, weil die Elementrelation keine Aussage, sondern eine Typdeklaration ist. Zum anderen, weil jedes Element sowieso immer nur einer Menge angehört. (Die Begründung von Anonymous im letzten Kommentar war falsch, denn Extensionalität würde ja nicht in Mengen enthaltende Mengen, sondern eben Elemente betreffen.) Aber wie Anonymous schon im letzten Kommentar gesagt hat, würde Extensionalität der Idee einer strukturellen Mengenlehre entgegenwirken. Wenn man nun keine Extensionalität hat, stellt sich die Frage, welche anderen nichttrivialen Axiome die Gleichheit überhaupt noch erfüllen soll? Auch wenn es anfangs natürlich eine gewisse Einschränkung darstellt oder jedenfalls so erscheint, nicht <math>A=B</math> hinschreiben zu können, so zeigt sich doch mit etwas mathematischer Erfahrung, dass der Typ <math>A \xrightarrow{\smash{\raisebox{-0.4ex}\sim}} B</math> viel relevanter ist. Zudem ist <math>A=B</math> (in der Prädikatenlogik, nicht in der Typentheorie!) lediglich eine Aussage, die wahr oder falsch ist, aber <math>A \xrightarrow{\smash{\raisebox{-0.4ex}\sim}} B</math> ist ein viel reichhaltiger Typ, welcher nämlich alle Bezeuger für die Isomorphie von <math>A</math> und <math>B</math> beinhaltet.

 [Bearbeiten]

Re: SEAR: Mengen, Elemente und Relationen
von Ex_Mitglied_47059 am Mo. 26. Dezember 2016 19:46:18


"Das eigentlich strukturelle an solchen Mengenlehren ist ja auch, dass <math>A\in B</math> verboten wird, und nicht etwa <math>A=B</math>."

Ja, strukturelle Mengen sind dasselbe wie Kardinalzahlen (Lawvere). Und Kardinalzahlen <math>A, B</math> sind bereits gleich, wenn es eine Bijektion (Isomorphismus) zwischen ihnen gibt.

Eine für mich interessante Frage wäre jetzt, ob in ETCS/SEAR folgendes beweisbar ist für jedes Prädikat <math>\phi(x)</math>: <math>\forall A, B:\text{SET}.\, \text{"$A$ und $B$ gleichmächtig"}\implies (\phi(A)\implies\phi(B))</math>.

Weißt du oder Tri etwas dazu?

 [Bearbeiten]

Re: SEAR: Mengen, Elemente und Relationen
von Triceratops am Mo. 26. Dezember 2016 20:59:21


@mathematischeIdee: Ja, diese Aussage gilt, und wird auch im Artikel erwähnt ("Man kann übrigens zeigen, dass jede im System <math>\mathsf{SEAR}</math> gebildete Aussage über eine Menge auch für jede dazu isomorphe Menge gilt."). Man beweist das induktiv nach dem Aufbau von <math>\phi(x)</math>. Ich würde die Aussage so formulieren (denn diese Verstärkung ist nützlich beim Beweis):

<math>\forall f : A \xrightarrow{\sim} B.\, \forall a_1,\dotsc,a_n : A.\, \phi(A,a_1,\dotsc,a_n) \iff \phi(B,f(a_1),\dotsc,f(a_n)).</math>

 [Bearbeiten]

Re: SEAR: Mengen, Elemente und Relationen
von Ex_Mitglied_47059 am Di. 27. Dezember 2016 22:59:31


Wäre es auch sinnvoll, in die Formel <math>\phi</math> Parameter einzubauen; also:

Satz: Für jede Formel <math>\phi(p_1, \dots, p_n, x)</math> gilt:
SEAR/ETCS kann die Formel <math>\forall p_1\dots\forall p_n\forall A, B:\mathsf{set}.\, A\cong B\implies (\phi(p_1, \dots, p_n, A)\implies \phi(p_1, \dots, p_n, B)</math> beweisen. Die $p_i$ können irgendeinen Typ haben.

Wäre das sinnvoll?

Antwort: Ja.

 [Bearbeiten]

 
All logos and trademarks in this site are property of their respective owner. The comments are property of their posters, all the rest © 2001-2017 by Matroids Matheplanet
This web site was made with PHP-Nuke, a web portal system written in PHP. PHP-Nuke is Free Software released under the GNU/GPL license.
Ich distanziere mich von rechtswidrigen oder anstößigen Inhalten, die sich trotz aufmerksamer Prüfung hinter hier verwendeten Links verbergen mögen.
Lesen Sie die Nutzungsbedingungen, die Distanzierung, die Datenschutzerklärung und das Impressum.
[Seitenanfang]