%%% ==================================================================== %%% Text-file from project *Hilbert 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: Axiomatic Set Theory Module version: 1.00.00 (Rev. 2.01a) Rule version: 2.00.00 Locations: http://www.qedeq.org/0_01_05/axiomatic_set_theory.txt *Axioms and first definitions of axiomatic set theory* [DRAFT] This file is part of the project 'Hilbert II'. This open source project wants to present mathematical knowledge in a highly standardized and 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 Morse and Kelley (MK) - a variant of the von Neumann-Bernays- G???del set theory (NBG). The following logical operator symbols are used in formulas: "~" negation (prefix notation with exact one argument) "&" conjunction (infix notation with exact two arguments) "v" disjunction (infix notation with exact two arguments) "->" implication (infix notation with exact two arguments) "<->" equivalence (infix notation with exact two arguments) "A" universal quantor (prefix notation with exact two arguments) "E" existential quantor (prefix notation with exact two arguments) Table of operator priority, sorted from highest to lowest: "~", "A", "E" "&" "v" "->", "<->" Undefined (primitive) predicate for the domain: "in" solely needed set theoretic predicate constant (infix notation with exact two arguments) Defined predicates for the domain: "set" defined predicate constant (prefix notation with exact one argument) "=" defined predicate constant (infix notation with exact two arguments) The subject domain consists of classes. Class variables are written as single lower case letters like "x", "y", etc. Module admin: mime@qedeq.org Author(s) of this module: Michael Meyling Franz Fritsche Needs following modules: Name: propaxiom Module version: 1.00.00 Rule version: 1.00.00 Locations: ../0_00_52/ Name: predaxiom Module version: 1.00.00 Rule version: 1.00.00 Locations: ../0_00_52/ (primitive:in) Application 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) :<-> Ey x in y If x is a member of a class, it is called a {\bf set}. (axiom:kompr) The axiom of class constructing is the following: Axiom ExAy(y in x <-> set(y) & P(y)) // if x does not occure free in P(y) This axiom (or rather axiom schema) is also called 'comprehension axiom'. Notice that for \qedeq{P(y)} arbitrary formulas could be substituted\footnote{in which \qedeq{x} does not occur (free) and \qedeq{y} occurs 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 :<-> Az(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. (thm:set:equal1) This definition of equality leads to the common properties: First reflexivity. Proposition x = x Proof: 1. a in x <-> a in x ;P <-> P is a tautology 2. Az(z in x <-> z in x) ;A-Intro 3. x = x ;[def:equal] qed (thm:set:equal2) Symmetry is following. Proposition x = y -> y = x Proof 1. x = y ;assume 2. Az(z in x <-> z in y) ;[def:equal] 3. Az(z in y <-> z in x) ;commutativity of <-> 4. y = x ;[def:equal] 5. x = y -> y = x ;from 1,4 (->Intro) qed (thm:set:equal3) Now the transitivity property is shown. Proposition x = y & y = z -> x = z Proof 1. x = y & y = z ;assume 2. Au(u in x <-> u in y) & Au(u in y <-> u in z) ;[def:equal] 3. Au((u in x <-> u in y) & (u in y <-> u in z)) ;theorem 4. (a in x <-> a in y) & (a in y <-> a in z) ;A-Elim 5. a in x <-> a in z ;from 4 6. Au(u in x <-> u in z) ;A-Intro 7. x = z ;[def:equal] 8. x = y & y = z -> x = z ;from 1,7 (->Intro) 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. x = y & z in x ;assume 2. z in x ;from 1 (&Elim) 3. x = y ;from 1 (&Elim) 4. Au(u in x <-> u in y) ;[def:equal] 5. z in x <-> z in y ;A-Elim 6. z in y ;from 2,5 7. x = y & z in x -> z in y ;from 1,6 (->Intro) 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 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:leibniz) Rule Neben der Reflexivit???t ist die "Leibniz'sche Ersetzbarkeit" eine wichtige Forderung an die mathematische Gleichheit: \qedeq{(x = y & P(x)) -> P(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 ausschlie??lich aus der Enthaltenseinsbeziehung und logischen Operatoren gebildet werden, kann aus [thm:extens2] und [axiom:extens] die G??ltigkeit der Leibniz'schen Ersetzbarkeit f??r alle konkreten mengentheoretischen Aussagen bewiesen werden\footnote{So folgt beispielsweise aus \qedeq{x = y & (x in z v z in x)} nach dem logischen Distributivgesetz \qedeq{(x = y & x in z) v (x = y & z in x)} und mit [thm:extens2] und [axiom:extens] folgt dann logisch \qedeq{y in z v z in y}. Entsprechend kann auch f??r die Negation und die Quantifizierung argumentiert werden.}. Deshalb wird die Leibniz'sche 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 Leibniz'schen Ersetzbarkeit kann auch die sch???rfere Formulierung \qedeq{(x = y -> (P(x) <-> P(y))} abgeleitet werden. F??r gleiche Mengen gelten also dieselben Aussagen. (abr:set1) Deshalb k??nnen wir eine neue abk??rzende Schreibweise einf??hren. 'set builder notation' Abbreviation x in {y | P(y)} :<-> set(x) & P(x) (abr:set2) F??r die Beziehung in der anderen Richtung muss das Folgende gelten. Abbreviation {y | P(y)} in x :<-> Ez(Ay((set(y) & P(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 | P(y)} in x <-> Ez(z = {y | P(y)} & z in x) Proof 1. {y | P(y)} in x <-> {y | P(y)} in x ;P <-> P is a tautology 2. <-> Ez(Ay((set(y) & P(y)) <-> y in z) & z in x) ;[abr:set2] 3. <-> Ez(Au((set(u) & P(u)) <-> u in z) & z in x) 4. <-> Ez(Au(u in z <-> (set(u) & P(u))) & z in x) 5. <-> Ez(Au(u in z <-> u in {y | P(y)}) & z in x) 6. <-> Ez(z = {y | P(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 | P(x)} = {x | Q(x)} <-> (Ax(set(x) -> (P(x) <-> Q(x)))) Proof 1. {x | P(x)} = {x | Q(x)} 2. <-> Ay(y in {x | P(x)} <-> y in {x | Q(x)})) ;[def:equal] 3. <-> Ay((set(y) & P(y)) <-> (set(y) & Q(y)))) ;[abr:set1] 4. <-> Ay(((set(y) & P(y)) -> (set(y) & Q(y))) & ((set(y) & P(y)) -> (set(y) & Q(y))))) 5. <-> Ay(((set(y) & P(y)) -> Q(y)) & ((set(y) & Q(y)) -> Q(y)))) 6. <-> Ay((set(y) -> (P(y) -> P(y))) & (set(y) -> (Q(y) -> P(y))))) 7. <-> Ay(set(y) -> ((P(y) -> Q(y)) & (Q(y) -> P(y))))) 8. <-> Ay(set(y) -> (P(y) <-> Q(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. Az(z in x <-> z in x) ;[def:equal] 3. Az(z in x <-> (set(z) & z in x)) ;[def:set] 4. Az(z in x <-> z in {y | y in x}) ;[abr:set1] with P(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 union y) :<-> {z | z in x v z in y} (abr:set:intersection) Entsprechend wird der Durchschnitt zweier Klassen definiert. Abbreviation (x inter 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 union y) <-> z in x v z in y Proof 1. z in (x union y) 2. <-> z in {u | u in x v u in y} ;[abr:set:union] 3. <-> z in x v z in y ;[abr:set1] (thm:set:in:intersection) Entsprechendes gilt f??r den Durchschnitt zweier Klassen. Proposition z in (x inter y) <-> z in x & z in y Proof 1. z in (x inter y) 2. <-> z in {u | u in x & u in y} ;[abr:set:intersection] 3. <-> z in x & z in y ;[abr:set1] Die letzten beiden S??tze [thm:set:in:union] und [thm:set:in:intersection] zeigen die ??bertragbarkeit der Eigenschaften der logischen Verkn??pfungen \qedeq{v} 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 union y) union z) = (x union (y union z)) Proof 1. ((x union y) union z) = ((x union y) union z) ;[thm:set:equal1] 2. Au(u in ((x union y) union z) <-> u in ((x union y) union z)) ;[def:equal] 3. Au(u in ((x union y) union z) <-> u in (x union y) v u in z) ;[abr:set:union] 4. Au(u in ((x union y) union z) <-> (u in x v u in y) v u in z) ;[abr:set:union] 5. Au(u in ((x union y) union z) <-> u in x v (u in y v u in z)) 6. Au(u in ((x union y) union z) <-> u in x v u in (y union z)) ;[abr:set:union] 7. Au(u in ((x union y) union z) <-> u in (x union (y union z))) ;[abr:set:union] 8. ((x union y) union z) = (x union (y union z)) ;[def:equal] (thm:union:asso) Assoziativit??t des Durchschnitts Proposition ((x inter y) inter z) = (x inter (y inter z)) Proof 1. ((x inter y) inter z) = ((x inter y) inter z) ;[thm:set:equal1] 2. Au(u in ((x inter y) inter z) <-> u in ((x inter y) inter z)) ;[def:equal] 3. Au(u in ((x inter y) inter z) <-> u in (x inter y) v u in z) ;[abr:set:intersection] 4. Au(u in ((x inter y) inter z) <-> (u in x v u in y) v u in z) ;[abr:set:intersection] 5. Au(u in ((x inter y) inter z) <-> u in x v (u in y v u in z)) 6. Au(u in ((x inter y) inter z) <-> u in x v u in (y inter z)) ;[abr:set:intersection] 7. Au(u in ((x inter y) inter z) <-> u in (x inter (y inter z))) ;[abr:set:intersection] 8. ((x inter y) inter z) = (x inter (y inter z)) ;[def:equal]