%%% ==================================================================== %%% Text-file from project *Principia Mathematica II* %%% %%% Language: German %%% ==================================================================== *Axiome und erste Definitionen der Mengenlehre* Diese Datei ist Bestandteil des Open-Source-Projektes *Principia Mathematica II*. Dieses Projekt will mathematisches Wissen in einer formal korrekten Art und Weise darstellen. Unter http://www.pmii.org sind weitere Informationen zu diesem Projekt zu finden. Dieses Modul enthält die Axiome und ersten Definitionen der Neumann-Bernays-Gödelschen Mengenlehre. Module admin: principa@meyling.com This module has the following specification: Name: set1 Module version: 1.00.00 Rule version: 1.00.00 Locations: . Author(s) of this module: Michael Meyling Needs following modules: Name: predaxiom Module version: 1.00.00 Rule version: 1.00.00 Locations: . (def:in) Definition des Prädikats 'ist ein Element der Klasse` %1 "in" %2 (def:set) Definition des Prädikats 'ist eine Menge`. Definition set(x) := exists y x in y Ist eine Klasse also Element einer anderen Klasse, dann wird sie auch als *Menge* bezeichnet. (axiom:kompr) Das Axiom der Klassenbildung ist das folgende: Axiom exists x all y (y in x <=> (set(y) & Pred1(y))) Dieses Axiom wird auch 'Komprehensionsaxiom` genannt. Es ist zu beachten, dass für die Prädikatvariable beliebige Formeln eingesetzt werden können\footnote{in denen \qedeq{x} gar nicht und \qedeq{y} frei vorkommen müssen}, in denen auch weitere Subjektvariablen frei vorkommen können. (def:equal) Die Gleichheit zweier Klassen kann definiert werden durch die Eigenschaft, dass sie dieselben Elemente besitzen. Definition x = y := all z (z in x <=> z in y) Es wird von der 'Umfangsgleichheit` gesprochen. (thm:set:equal1) Die Definition der Gleichheit von Klassen führt zur den gewohnten Eigenschaften. Zunächst die Reflexivität. Proposition x = x Proof: 1: (Pred2(y) => (Pred1(y) <=> Pred1(y))) ;P2 => (P1 <=> P1) ist eine Tautologie 2: (set(y) => (y in x <=> y in x)) 3: all y (set(y) => (y in x <=> y in x)) 4: x = x ;[def:equal] qed (thm:set:equal2) Es folgt die Symmetrie. Proposition (x = y => y = x) Proof: 1: let x = y 2: all z (set(z) => (z in x <=> z in y)) ;[def:equal] 3: all z (set(z) => (z in y <=> z in x)) 4: y = x 5: so (x = y => y = x) ;aus 1, 4 qed (thm:set:equal3) Und nun folgt die Transitivität der Gleichheit. Proposition ((x = y & y = z) => y = z) Proof: 1: let (x = y & y = z) 2: (all u (set(u) => (u in x <=> u in y)) & all u (set(u) => (u in y <=> u in z))) ;[def:equal] 3: all u ((set(u) => (u in x <=> u in y)) & (set(u) => (u in y <=> u in z))) 4: all u (set(u) => ((u in x <=> u in y) & (u in y <=> u in z))) 5: all u (set(u) => (u in x <=> u in z)) 6: so y = z ;aus 1, 5 7: ((x = y & y = z) => y = z) ;aus 1, 6 qed (thm:extens2) Die Ersetzbarkeit für die Enthaltenseinsbeziehung in der einen Richtung (rechts von $in$) kann direkt aus der Definition der Gleichheit abgeleitet werden. Proposition ((x = y & z in x) => z in y) Proof: 1: let (x = y & z in x) 2: (all u u in x <=> u in y) & z in x 3: (z in x <=> z in y) & z in x 4: so z in y 5: (x = y & z in x) => z in y qed (axiom:extens) Die Definition der Umfangsgleichheit reicht jedoch nicht aus, um eine Klasse durch eine gleiche Klasse ersetzen zu können. Der Zusammenhang von Umfangsgleichheit und die Ersetzbarkeit für die Enthaltenseinsbeziehung in der anderen Richtung (links von $in$) wird erst durch das Axiom der Extensionalität garantiert. Axiom ((x = y & x in z) => y in z) (rule:leibnitz) Rule Neben der Reflexivität ist die 'Leibnitzsche Ersetzbarkeit` eine wichtige Forderung an die mathematische Gleichheit: \qedeq{(x = y & Pred1(x)) => Pred1(y)}. Da die Gleichheit hier innerhalb der Mengenlehre definiert wurde, kann die Aussage in dieser Form nicht bewiesen werden. Weil jedoch alle Aussagen der Mengenlehre aus Prädikaten bestehen, die ausschliesslich aus der Enthaltenseinsbeziehung und logischen Operatoren gebildet werden, kann aus [thm:extens2] und [axiom:extens] die Gültigkeit der Leibnitzschen Ersetzbarkeit für alle konkreten mengentheoretischen Aussagen bewiesen werden\footnote{So folgt beispielsweise aus \qedeq{x = y & (x in z | z in x)} nach dem logischen Distributivgesetz \qedeq{(x = y & x in z) | (x = y & z in x)} und mit [thm:extens2] und [axiom:extens] folgt dann logisch \qedeq{y in z | z in y}. Entsprechend kann auch für die Negation und die Quantifizierung argumentiert werden.}. Deshalb wird die Leibnitzsche Ersetzbarkeit als Metaregel aufgenommen. Nach ihrer Anwendung muss allerdings das Prädikat durch ein konkretes mengentheoretisches Prädikat ersetzt werden. \par Aus dieser Form der Leibnitzschen Ersetzbarkeit kann auch die schärfere Formulierung \qedeq{(x = y => (Pred1(x) <=> Pred1(y))} abgeleitet werden. Für gleiche Mengen gelten also dieselben Aussagen. (abr:set1) Durch die Extensionalität und das Komprehensionsaxiom wird nun der Zusammenhang zwischen einer Aussage \qedeq{Pred1(y)} und der durch diese Aussage definierten Klasse festgelegt. Das Komprehensionsaxiom behaupted die Existenz mindestens einer durch die Aussage \qedeq{Pred1(y) & set(y)} definierten Klasse. Die Gleichheitsdefinition sichert unter Berücksichtigung der Extensionalität, dass es höchstens eine solche Klasse gibt: irgend zwei Klassen, welche dieselben Elemente besitzen, sind gleich im Sinne der Ersetzbarkeit in allen einschlägigen Aussagen. Mit anderen Worten: es gibt nur genau eine solche Klasse. Deshalb können wir eine neue abkürzende Schreibweise einführen. Abbreviation x in {y | Pred1(y)} := (set(x) & Pred1(x)) (abr:set2) Für die Beziehung in der anderen Richtung muss das Folgende gelten. Abbreviation {y | Pred1(y)} in x := exists z (all y ((set(y) & Pred1(y)) <=> y in z) & z in x) (rule:predset) Rule Im Folgenden verwenden wir diese abkürzenden Schreibweisen in allen prädikativen Aussagen. (thm:set:equal1) Die Kompatiblität mit dem Extensionalitätsaxiom ist gewährleistet. Proposition ({y | Pred1(y)} in x <=> (exists z (z = {y | Pred1(y)} & z in x))) Proof: 1: ({y | Pred1(y)} in x <=> {y | Pred1(y)} in x) ;(P1 <=> P1) ist eine Tautologie 2: <=> exists z (all y ((set(y) & Pred1(y)) <=> y in z) & z in x)) ;[abr:set2] 3: <=> exists z (all u ((set(u) & Pred1(u)) <=> u in z) & z in x)) 4: <=> exists z (all u (u in z <=> (set(u) & Pred1(u))) & z in x)) 5: <=> exists z (all u (u in z <=> u in {y | Pred1(y)}) & z in x)) 6: <=> exists z (z = {y | Pred1(y)} & z in x)) qed (thm:set:equal1) Aus den Abkürzungen ergibt sich für die Gleichheit von derartigen Mengen das Folgende. Proposition ({x | Pred1(x)} = {x | Pred2(x)} <=> (all x (set(x) => (Pred1(x) <=> Pred2(x))))) Proof: 1: ({x | Pred1(x)} = {x | Pred2(x)} 2: <=> all y (y in {x | Pred1(x)} <=> y in {x | Pred2(x)})) ;[def:equal] 3: <=> all y ((set(y) & Pred1(y)) <=> (set(y) & Pred2(y)))) ;[abr:set1] 4: <=> all y (((set(y) & Pred1(y)) => (set(y) & Pred2(y))) & ((set(y) & Pred1(y)) => (set(y) & Pred2(y))))) 5: <=> all y (((set(y) & Pred1(y)) => Pred2(y)) & ((set(y) & Pred2(y)) => Pred2(y)))) 6: <=> all y ((set(y) => (Pred1(y) => Pred2(y))) & (set(y) => (Pred2(y) => Pred1(y))))) 7: <=> all y (set(y) => ((Pred1(y) => Pred2(y)) & (Pred2(y) => Pred1(y))))) 8: <=> all y (set(y) => (Pred1(y) <=> Pred2(y)))) qed (thm:set:describe) Jede Klasse lässt sich durch eine Aussage beschreiben. Proposition x = {y | y in x} Proof 1: x = x ;[thm:set:equal1] 2: all z (z in x <=> z in x) ;[def:equal] 3: all z (z in x <=> (set(z) & z in x)) ;[def:set] 4: all z (z in x <=> z in {y | y in x}) ;[abr:set1] mit Pred1(z) = z in x 5: x = {y | y in x} ;[def:equal] (abr:set:union) Die Möglichkeit eine Menge durch eine Aussage zu beschreiben, ermöglicht die Definition einer Verknüpfung zweier Klassen: die Vereinigung zweier Klassen. Abbreviation (x + y) := {z | z in x | z in y} (abr:set:intersection) Entsprechend wird der Durchschnitt zweier Klassen definiert. Abbreviation (x * y) := {z | z in x & z in y} (thm:set:in:union) Ob eine Menge ein Element der Vereinigung zweier Klassen ist, kann natürlich auch direkt angegeben werden. Proposition z in (x + y) <=> z in x | z in y Proof 1: z in (x + y) 2: <=> z in {u | u in x | u in y} ;[abr:set:union] 3: <=> z in x | z in y ;[abr:set1] (thm:set:in:intersection) Entsprechendes gilt für den Durchschnitt zweier Klassen. Proposition z in (x * y) <=> z in x & z in y Proof 1: z in (x * y) 2: <=> z in {u | u in x & u in y} ;[abr:set:intersection] 3: <=> z in x & z in y ;[abr:set1] Mit die letzten beiden Sätze [thm:set:in:union] und [thm:set:in:intersection] zeigen die Übertragbarkeit der Eigenschaften der logischen Verknüpfungen \qedeq{|} und\qedeq{&} auf die Mengenverknüpfungen \qedeq{+} und \qedeq{*}. Deshalb lassen sich die entsprechenden logischen Gesetzmässigkeiten direkt auf die Mengenverknüpfungen übertragen. (thm:union:asso) Assoziativität der Vereinigung Proposition ((x + y) + z) = (x + (y + z)) Proof: 1: ((x + y) + z) = ((x + y) + z) ;[thm:set:equal1] 2: all u in ((x + y) + z) <=> u in ((x + y) + z) ;[def:equal] 3: all u in ((x + y) + z) <=> u in (x + y) | u in z ;[abr:set:union] 4: all u in ((x + y) + z) <=> (u in x | u in y) | u in z ;[abr:set:union] 5: all u in ((x + y) + z) <=> u in x | (u in y | u in z) 6: all u in ((x + y) + z) <=> u in x | u in (y + z) ;[abr:set:union] 7: all u in ((x + y) + z) <=> u in (x + (y + z)) ;[abr:set:union] 8: ((x + y) + z) = (x + (y + z)) ;[def:equal] (thm:union:asso) Assoziativität des Durchschnitts Proposition ((x * y) * z) = (x * (y * z)) Proof: 1: ((x * y) * z) = ((x * y) * z) ;[thm:set:equal1] 2: all u in ((x * y) * z) <=> u in ((x * y) * z) ;[def:equal] 3: all u in ((x * y) * z) <=> u in (x * y) | u in z ;[abr:set:intersection] 4: all u in ((x * y) * z) <=> (u in x | u in y) | u in z ;[abr:set:intersection] 5: all u in ((x * y) * z) <=> u in x | (u in y | u in z) 6: all u in ((x * y) * z) <=> u in x | u in (y * z) ;[abr:set:intersection] 7: all u in ((x * y) * z) <=> u in (x * (y * z)) ;[abr:set:intersection] 8: ((x * y) * z) = (x * (y * z)) ;[def:equal]