%%% ==================================================================== %%% Text-file from project *Principia Mathematica II* %%% %%% Permission is granted to copy, distribute and/or modify this %%% document under the terms of the GNU Free Documentation License, %%% Version 1.2 or any later version published by the %%% Free Software Foundation; with no Invariant Sections, %%% no Front-Cover Texts, and no Back-Cover Texts. %%% See under "http://www.gnu.org/licenses/fdl.html". %%% ==================================================================== This module has the following specification: Name: set Module version: 1.00.00 Rule version: 2.00.00 Locations: http://www.qedeq.org/0_01_05/ *Axioms and first definitions of axiomatic set theory* This file is part of the project `Principia Mathematica II' see This open source project wants to present mathematical knowledge in a formal correct form. Under \href{http://www.qedeq.org/}{http://www.qedeq.org/} more information about this project could be found. This file contains the axioms and first definitions of the axiomatic set theory due to Neumann-Bernays-G"odel. The following operator symbols are used in formulas: "-" logical negation (prefix notation with exact one argument) "&" logical conjunktion (infix notation with at least two arguments) "|" logical disjunktion (infix notation with at least two arguments) "=>" logical implication (infix notation with at least two arguments) "<=>" logical equivalence (infix notation with at least two arguments) "all" universal quantor (prefix notation with exact two arguments) "exists" existential quantor (prefix notation with exact two arguments) "in" set theoretic operator, solely needed predicate constant (infix notation with exact two arguments) "=" defined predicate constant (infix notation with exact two arguments) Table of operator priority, sorted from highest to lowest: "in", "=" "-" "&" "|" "=>", "<=>" "all", "exists" Module admin: mime@qedeq.org Author(s) of this module: Michael Meyling Needs following modules: Name: propaxiom Module version: 1.00.00 Rule version: 1.00.00 Locations: ../0_00_51/ Name: predaxiom Module version: 1.00.00 Rule version: 1.00.00 Locations: ../0_00_51/ (def:in) Definition of the predicate constant 'is a member of the class` %1 "in" %2 (def:set) Definition of the predicate 'is a set`. Definition set(x) := exists y x in y Is a class member of another class it is called a {\bf set}. (axiom:kompr) The axiom of class constructing is the following: Axiom exists x all y (y in x <=> (set(y) & Pred1(y))) This axiom is also called 'comprehension axiom`. Notice that for \qedeq{Pred1(y)} arbitrary formulas could be substituted\footnote{in which \qedeq{x} does not occur and \qedeq{y} occurrs free}, in which some other subject variables could occur free. (def:equal) The equality of two classes could be defined by the property that they have precisely the same members. Definition x "=" y := all z (z in x <=> z in y) So a set is determined uniquely by its members. Some treatments of axiomatic set theory prefer to assume that equality is a primitive symbol in predicate logic, and instead treat the above statement not as a definition but as an axiom of equality. (thm:set:equal1) This definition of equality leads to the common properties: First the relexivity. Proposition x = x Proof: 1: (Pred2(y) => (Pred1(y) <=> Pred1(y))) ;P2 => (P1 <=> P1) is a tautology 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) Symmetry is following. 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) Now the transitivity property is shown. 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) The substitutability for the member relation could be deduced for one direction (right of \qedeq{in}) directly from the definition. 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 logicaln 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 logicaln 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. 'set builder notation` 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 cup y) := {z | z in x | z in y} (abr:set:intersection) Entsprechend wird der Durchschnitt zweier Klassen definiert. Abbreviation (x cap 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 cup y) <=> z in x | z in y Proof 1: z in (x cup 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 cap y) <=> z in x & z in y Proof 1: z in (x cap 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 logicaln Verknüpfungen \qedeq{|} und\qedeq{&} auf die Mengenverknüpfungen \qedeq{+} und \qedeq{*}. Deshalb lassen sich die entsprechenden logicaln Gesetzmässigkeiten direkt auf die Mengenverknüpfungen übertragen. (thm:union:asso) Assoziativität der Vereinigung Proposition ((x cup y) cup z) = (x cup (y cup z)) Proof: 1: ((x cup y) cup z) = ((x cup y) cup z) ;[thm:set:equal1] 2: all u in ((x cup y) cup z) <=> u in ((x cup y) cup z) ;[def:equal] 3: all u in ((x cup y) cup z) <=> u in (x cup y) | u in z ;[abr:set:union] 4: all u in ((x cup y) cup z) <=> (u in x | u in y) | u in z ;[abr:set:union] 5: all u in ((x cup y) cup z) <=> u in x | (u in y | u in z) 6: all u in ((x cup y) cup z) <=> u in x | u in (y cup z) ;[abr:set:union] 7: all u in ((x cup y) cup z) <=> u in (x cup (y cup z)) ;[abr:set:union] 8: ((x cup y) cup z) = (x cup (y cup z)) ;[def:equal] (thm:union:asso) Assoziativität des Durchschnitts Proposition ((x cap y) cap z) = (x cap (y cap z)) Proof: 1: ((x cap y) cap z) = ((x cap y) cap z) ;[thm:set:equal1] 2: all u in ((x cap y) cap z) <=> u in ((x cap y) cap z) ;[def:equal] 3: all u in ((x cap y) cap z) <=> u in (x cap y) | u in z ;[abr:set:intersection] 4: all u in ((x cap y) cap z) <=> (u in x | u in y) | u in z ;[abr:set:intersection] 5: all u in ((x cap y) cap z) <=> u in x | (u in y | u in z) 6: all u in ((x cap y) cap z) <=> u in x | u in (y cap z) ;[abr:set:intersection] 7: all u in ((x cap y) cap z) <=> u in (x cap (y cap z)) ;[abr:set:intersection] 8: ((x cap y) cap z) = (x cap (y cap z)) ;[def:equal]