%%% ====================================================================
%%% This file is part of the open source project *Hilbert II*, which 
%%% wants to present mathematical knowledge in a standardized and 
%%% formal correct form.
%%% See "http://www.qedeq.org" for more information about this project.
%%% 
%%% 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 (Rev. 1.2)
  Rule version:   2.00.00
  Locations:      http://www.qedeq.org/0_01_05/set.txt


*Axioms and first definitions of axiomatic set theory* 


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)

The subject domain consists of classes. Class variables are written as single
letters like "x", "y", etc.

Undefined (primitive) operators for the domain:
"in"     set theoretic operator, solely needed predicate constant
         (infix notation with exact two arguments)

Defined operators for the domain:
"set"    defined predicate constant (prefix notation with exact one argument)
"="      defined predicate constant (infix notation with exact two arguments)

Table of operator priority, sorted from highest to lowest:

  "set"
  "in", "="
  "~", "A", "E"
  "&"
  "v"
  "->", "<->"


Module admin: mime@qedeq.org

Authors of this module: 
Michael Meyling <mime@qedeq.org>
Franz Fritsche <info@simple-line.de>


Needs following modules:

  Name:           propaxiom
  Module version: 1.00.00
  Rule version:   1.00.00
  Locations:      ../0_00_53/

  Name:           predaxiom
  Module version: 1.00.00
  Rule version:   1.00.00
  Locations:      ../0_00_53/


(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 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. z in x <-> z in x                        ;P <-> P is a tautology
  2. Az(z in x <-> z in y)                    ;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)                  ;renaming of variables
  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                          ;tautologies
  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. | Au(u in x <-> u in y) & z in x             ;[def:equal]
  3. | (z in x <-> z in y) & z in x               ;A-Elim
  4. | z in y                                     ;tautologies
  5. x = y & z in x -> z in y                     ;from 1,4 (->Intro)       
qed


(axiom:extens) 
The definition of equality by having the same members is not sufficient
to be able to replace one class by an equal one. The close connection
between this equality and the possiblity to replace a class in an
"is member of" formula is only garantied by the axiom of extensionality:

Axiom
x = y & x in z -> y in z


(rule:leibniz)
Rule
Beside the reflexivity the 'Leibnizsche Ersetzbarkeit` is an important
requirement for mathematical identy:
\qedeq{(x = y & P(x)) -> P(y)}. 
Because here equality is defined inside set theory, this proposition
couldn't be proved in this general form.  
But all propositions of set theory consist of predicats which are build
exclusively by the member of relation and logical operators. Therefore
from [thm:extens2] and [axiom:extens] the validity of 
\qedeq{(x = y & P(x)) -> P(y)} could be proved for every concrete
set theoretic proposition.\footnote{For example: out of
\qedeq{x = y & (x in z v z in x)} could be derived
\qedeq{(x = y & x in z) v (x = y & z in x)} with the logical distributive
law and with [thm:extens2] and [axiom:extens] follows logically
\qedeq{y in z v z in y}.
An analogus argument could be found for the negation and quantification.}
For this reason the 'Leibnizsche Ersetzbarkeit' is added as a new
meta rule, provided that the predicate is always replaced by an concrete
set theoretical predicate.
\par
It follows even the advanced form: \qedeq{(x = y -> (P(x) <-> P(y))}.
Therefore for equal classes the same propositions are valid.


(abr:set1) 
Now we could introduce a new notation to characterize sets. This
set builder notation is defined as follows:

Abbreviation
x in {y | P(y)} :<-> set(x) & P(x)


(abr:set2) 
For the other direction the following must be true:

Abbreviation
{y | P(y)} in x :<-> Ez(Ay((set(y) & P(y)) <-> y in z) & z in x)


(rule:predset)
Rule
The above abbreviations could be used further on in any predicative
propositions.


(thm:set:equal1) 
The compatiblity with the extensionality axiom is assured.

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) 
The abbreviations lead to the following description of identity of those
sets.

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)
Every class could be characterised by a proposition.

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] mit P(z) : z in x
  5. x = {y | y in x}                          ;[def:equal]
  
    
(abr:set:union)
This characterisation makes it possible to define an operation of two 
classes: the union of two classes.

Abbreviation
(x union y) :<-> {z | z in x v z in y}


(abr:set:intersection)
Analogus the intersection of two classes is defined.

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)
For the intersection of two classes an analogus proposition holds.

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]


The last two propositions [thm:set:in:union] and 
[thm:set:in:intersection] show the portability of properties of the
logical operators \qedeq{v} and \qedeq{^} into the set operators 
\qedeq{+} and \qedeq{*}. Therefore the appropriate logical laws could
be transfered into set theoretical ones.


(thm:union:asso)
Associativity of Union

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 of Intersection

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]