================================================================================
UTF-8-file     qedeq_set_theory_v1
Generated from http://www.qedeq.org/0_04_00/doc/math/qedeq_set_theory_v1.xml
Generated at   2010-12-28 21:19:37.005
================================================================================

If the characters of this document don't display correctly try opening this
document within a webbrowser and if necessary change the encoding to
Unicode (UTF-8)

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.



Axiomatic Set Theory
════════════════════

Michael Meyling


The source for this document can be found here:

http://www.qedeq.org/0_04_00/doc/math/qedeq_set_theory_v1.xml


Copyright by the authors. All rights reserved.


If you have any questions, suggestions or want to add something to the list of 
modules that use this one, please send an email to the address mime@qedeq.org


The authors of this document are:
    Michael Meyling <michael@meyling.com>




___________________________________________________


Preface
═══════

Mathematics is a science with a structure that achieved enormous dimensions in
the course of time. This huge stronghold has only a small set theoretic
foundation and its firmness rests upon simple predicate calculus mortar. In
principle the assembly could be comprehended by any mathematician. From every
newest turret of mathematical cognition each path of logical dependency could be
followed all the way down to its set theoretic roots.

This document wants to provide some help to accomplish this task. What we aim at
is to get an understandable presentation of the set theoretic roots. But despite
all comprehensibility it is possible to drill very deep into details. Even into
the level of a formal proof. For that purpose this document will exist in
different detail levels. The original source of this document is written in a
formal language. So it is possible to prove the propositions automatically with
a computer program.

Lets start by the roots...

This document is not finished and is updated from time to time. Especially at
the locations marked with „+++” additions or changes will be made.

I am deeply grateful to my wife  G e s i n e  D r ä g e r  and our son
 L e n n a r t  for their support and patience.

Hamburg, december 2010
  Michael Meyling



___________________________________________________


Introduction
════════════

Within this document we use the results of [l]. After mathematical logic has
provided us with the methods of reasoning we start with a very basic theory. Set
theory deals with objects and their collections. This theory is interesting for
two reasons. First, nearly all mathematical fields use it. Second, every
mathematical statement or proof could be cast into formulas within set theory.
Number theory, algebra, analysis an all other theories could be constructed
within.

This document contains the mathematical foundation of set theory. Goal is the
presentation of elementary results which are needed in other mathematical
disciplines. After the basics the    b o o l e a n   a l g e b r a   o f
 c l a s s e s is in focus. Next are some thoughts about  r e l a t i o n s  and
 f u n c t i o n s . An important achievement is the definition of the
 n a t u r a l    n u m b e r s  and their fulfillment of the  P e a n o
 a x i o m s . Also the concept of  r e c u r s i o n  is discussed. Furthermore
the axiom of choice is examined. At the end the continuum is thematised.

Although the presentation is axiomatic the results shall match the mathematical
usage. Therefore the set theoretic axiom system of  A .  P .  M o r s e  and
 J .  L .  K e l l e y  (MK) was chosen. The presentation is very much along the
lines of  E .  J .  L e m m o n s excellent and strongly recommended
book [lemmon].



___________________________________________________


Chapter 1 


Basics
══════

In this chapter we start with the very basic axioms and definitions of set
theory. We shall make no attempt to introduce a formal language
          ┌
          │ Despite of this, in the original text of this document the formulas
          │ of axioms, definitions and propositions are written in a formal
          │ language. The original text is a XML file with a syntax defined by
          │ the XSD  http://www.qedeq.org/current/xml/qedeq.xsd . A more
          │ detailed description of the formula language is given in
          │  http://www.qedeq.org/current/doc/project/qedeq_logic_language_en.pdf .
          └
 but shall be content with the common logical operators. To be more precise:
precondition is a first-order predicate calculus with identity.

 G .  C a n t o r , who is considered the founder of set theory, gave in a
publication in 1895 a description of the term  s e t .
       By a „set” we are to understand any collection into a whole M of definite
      and separate objects m of our intuition or our thought. These objects are
      called the „elements” of M.


This collection can be specified by giving a  c o n d i t i o n   f o r
 m e m b e r s h i p . Around 1900 various paradoxes in this naive set theory
were discovered. These paradoxes base on giving tricky conditions for
membership.

There exist different ways out of those contradictions. In this text we don’t
restrict the condition for membership but we call the result a  c l a s s .
Additional axioms allow us to call certain classes sets again. All sets are
classes, but not all classes are sets. Sets are classes which are themselves
members of classes, whilst a class which is not a set is a class which is not a
member of any class.


1.1 Classes and Sets
――――――――――――――――――――

Although we want to speak about  s e t s  at the very beginning we have
 c l a s s e s . No formal definition of a class will be given. Informally, a
class is a collection of objects, the involved objects are called the
 e l e m e n t s  or  m e m b e r s  of the class. Sets will be construed as a
special kind of class.

The following definitions and axioms are due to a strengthened version of
 v o n  N e u m a n n - B e r n a y s - G ö d e l’ s  set theory ( N B G ). This
version is called  M K  which is short for  M o r s e - K e l l e y .


The theory of sets introduced here has initial objects, called  c l a s s e s .
Furthermore the only predefined symbol is for a binary relation called
 m e m b e r s h i p .

☉ initial Definition 1  (Membership Operator)  [definition:in]

     x ∈ y

We also say „x  i s   e l e m e n t   o f  y”, „x  b e l o n g s   t o  y”, „x
 i s   a   m e m b e r   o f  y” or „x  i s   i n  y”. Beside identity this is
the only predicate we start with. All other will be defined. Also no function
constants are initially given. Later on we will successively fix their meaning.


Although we simply can negate the membership predicate we also want to define a
shorthand notation for it.

☉ Definition 2  (Non Membership Operator)  [definition:notIn]

     x ∉ y  :↔  ¬ x ∈ y


Our first axiom states that, for any classes x and y, if the membership of x and
y are the same, then x and y are the same.

☉ Axiom 1  (Extensionality)  [axiom:extensionality]

     ∀ z (z ∈ x ↔ z ∈ y) → x  =  y

The classes x and y may be defined in entirely different ways, for example:

 x   =   class of all nonnegative integers,
 y   =   class of all integers, that can be written as sum of four squares,

but if they have the same members, they are the same class.


Now to our first proposition. We can reverse the implication in the axiom of
extensionality.

☉ Proposition 1   [theorem:extensonalityEquivalence]

     ∀ z (z ∈ x ↔ z ∈ y) ↔ x  =  y

Proof:
This a simple consequence of the second identity axiom. We assume x=y. Then
follows φ(x) ↔ φ(y) for any predicate φ. So follows z ∈ x ↔ z ∈ y for any z.
Therefore we have ∀  z  z ∈ x ↔  z ∈ y. So we derived x = y  →  ∀  z  z ∈ x ↔  z
∈ y. Together with axiom 1 we get the desired result.
q.e.d.

If identity were not part of our underlying logic, then we should need to take
this as a definition of identity. But then another axiom is needed and the
theory presentation is not so smooth for technical reasons (derivation of the
identity axioms).
          ┌
          │  Additional to the identity definition we need the following form of
          │ the extensionality axiom: (x = y ∧ x ∈ z)  → y ∈ z. This is a
          │ special case of the Leibniz’s replacement rule that we know already
          │ as axiom 8 [l]. The correctness of the general rule can be proved by
          │ recursion over formula building. See also [schmidt] § 6.
          │ 
          │ Alternatively one can define (x = y ↔ (∀ z  (x ∈ z  →  y ∈ z)) ∧ ∀ z
          │ (x ∈ z  →  z ∈ y)).
          └



Now we specify  s e t s .

☉ Definition 3  (Set)  [definition:isSet]

     ℳ(x)  :↔  ∃ y x ∈ y

So sets are nothing else than special classes. A class is a set iff it is a
member of any class.


A trivial consequence of this definition is the following equivalence.

☉ Proposition 2   [theorem:inSetEqualInSetAndIsSet]

     x ∈ y ↔ (ℳ(x) ∧ x ∈ y)

Proof:
‘⇒’: Assume x ∈ y. It follows ∃  u  x ∈ u and therefore ℳ(x) and logically ℳ(x)
∧ x ∈ y.

‘⇐’: From ℳ(x) ∧ x ∈ y we conclude x ∈ y.
q.e.d.


Now we can rewrite the axiom of extensionality as follows.
          ┌
          │ The quantification over z is restricted to sets.
          └


☉ Proposition 3   [theorem:extensionalitySetRestricted]

     x  =  y ↔ ∀  ℳ(z)  (z ∈ x ↔ z ∈ y)

Proof:
‘⇒’: Simulary to proof of proposition 1 we get the first implication by the
second identity axiom.

‘⇐’: Assume ∀  ℳ(z)  ( z ∈ x  ↔  z ∈ y). Let u be an arbitrary class. If u ∈ x
then u is a set by definition 3, and hence by the assumption, u ∈ y. similarly u
∈ y  →  u ∈ x. Since u is arbitrary, it follows that ∀ u  (u ∈ x  ↔  u ∈ y).
Thus by the axiom 1, x = y.
q.e.d.

Proof:


 x = y   ↔   ∀  z  ( z ∈ x  ↔  z ∈ y)   this is proposition 1
   ↔   ∀  z  ( ℳ(z) ∧ z ∈ x  ↔  ℳ(z) ∧ z ∈ y)   proposition 2
   ↔   ∀  z  ( ℳ(z) → (z ∈ x  ↔  z ∈ y))   proposition 1 (bh) [l]
   ↔   ∀  ℳ(z)  z ∈ x  ↔  z ∈ y)   axiom 11 [l]

q.e.d.


Our next set theoretic axiom makes it simple to create new classes. A class
could be characterized by a predicate calculus formula.

☉ Axiom 2  (Comprehension)  [axiom:comprehension]

     ∃ x ∀ y (y ∈ x ↔ (ℳ(y) ∧ φ(y)))

By a small modification of the above axiom we could get a  N B G  axiom system
of set theory due to  J o h n   v o n   N e u m a n n ,  I s a a k
 B e r n a y s  and  K u r t   G ö d e l . For that purpose we call a formula
 p r e d i c a t i v e , if all of its bound subject variables are restricted to
sets. Therefore predicative formulas formalize ‘set properties’.
          ┌
          │ A little bit more formal: within a predicative formula all
          │ quantifier variables run over sets: ∀  ℳ(x)  ∃  ℳ(y) ...
          └
 If we postulate φ to be predicative we achieve a NBG system
          ┌
          │ Some other axioms --- similar to the following --- are needed as
          │ well.
          └



By the comprehension axiom and the axiom of extensionality a relationship
between a formula φ(y) and the class defined by this formula is described. The
comprehension axiom proposes the existence of at least one class, where the
proposition ℳ(y) ∧ φ(y) holds for all of its elements. The axiom of
extensionality and the identity axioms make sure, that there is maximal one
class of this kind: two classes with the same elements are equal in the sense of
replacement in all appropriate propositions. In other words: there is one and
only one such class.

☉ Proposition 4   [theorem:comprehension]

     ∃! x ∀ y (y ∈ x ↔ (ℳ(y) ∧ φ(y)))

Proof:
We must show:
  ∃ x   ∀ y  (y ∈ x ↔  ℳ(y) ∧ φ(y))
 ∧  ∀ u  ∀ v   (∀ y  (y ∈ u ↔ ℳ(y) ∧ φ(y))  ∧  ∀ y  ( y ∈ v ↔  ℳ(y) ∧ φ(y)))
      → u = v)
 Let u and v be arbitrary. Furthermore let us assume:

∀ y  (y ∈ u ↔  ℳ(y) ∧ φ(y)) ∧  ∀ y  ( y ∈ v ↔ ℳ(y) ∧ φ(y)))

Now with proposition 2 (f) [l]: ∀ y  ((y ∈ u ↔ ℳ(y) ∧ φ(y)) ∧ (y ∈ v ↔ ℳ(y) ∧
φ(y)))

With proposition 2 (bg) [l] we derive: ∀ y  ((y ∈ u ↔ y ∈ v )). And with
proposition 1 follows u = v. So we have shown:

∀ u  ∀ v  (∀ y  (y ∈ u ↔ ℳ(y) ∧ φ(y)) ∧  ∀ y  (y ∈ v ↔ ℳ(y) ∧ φ(y))) → u = v)

Together with axiom 2 we get the proposition.
q.e.d.


Starting with proposition 4 we can extend the syntax and provide a new
abbreviation.

☉ Rule 1  (Class definition)  [rule:classDefinition]

For every formula α(x₁) we define the term expression { x₁  |  α(x₁)} where x₁
is a subject variable that is not bound within α(x₁). The free variables of { x₁
|  α(x₁)} are the are the free variables of α(x₁). The bound variables
correspond to the bound variables of α(x₁) enhanced by x₁.

All deduction rules are accordingly extended.

Based on: 
 \ref{theorem:comprehension}
In particular the substitution rules must be adapted because now a term can have
bound subject variables.
          ┌
          │ Luckily we formulated the substitution rules with this extension
          │ already in our mind, so we have nothing to do.
          └
 In the following this new notation is used.


We want to give the new syntax a meaning and by looking at proposition 4 we
introduce the following axiom.

☉ Axiom 3  (Class Definition Axiom)  [axiom:classDefinition]

     y ∈ { x  |  φ(x) }  ↔ (ℳ(y) ∧ φ(y))

This axiom together with rule 1 is a  c o n s e r v a t i v e  extension of our
formal language. This means that no additional formulas that fulfill the old
syntax can be derived. It is just convenient to have an elegant new notation.
          ┌
          │  A conservative extension is defined by the following. Let ℒ be a
          │ language and ℒ’ an extension of ℒ. Because ℒ’ ⊃ ℒ it follows
          │ Formula_(\mathfrak)L’ ⊃ Formula_(\mathfrak)L. If now for every set
          │ of formulas Γ ⊆ Formula_(\mathfrak)L and each formula α ∈
          │ Formula_(\mathfrak)L this proposition holds: Γ ⊢_(\mathfrak)L’ α  ⇒
          │ Γ ⊢_(\mathfrak)L α, then ℒ’ is called a  c o n s e r v a t i v e
          │ extension of ℒ.
          └



This new notation can be easily transformed in the old syntax. Using the new
term type with the initial predicates can be expressed as follows.

☉ Proposition 5   [theorem:setNotation]

  (a)  y ∈ { x  |  φ(x) }  ↔ (ℳ(y) ∧ φ(y))
  (b)  y  =  { x  |  φ(x) }  ↔ ∀ z (z ∈ y ↔ z ∈ { x  |  φ(x) } )
  (c)  { x  |  φ(x) }  =  { x  |  ψ(x) }  ↔ ∀ z (z ∈ { x  |  φ(x) }  ↔ z ∈ { x  
|  ψ(x)
} )
  (d)  { x  |  φ(x) } ∈ { x  |  ψ(x) }  ↔ ∀ u ∀ v ((u  =  { x  |  φ(x) }  ∧ v  =
  { x
|  ψ(x) } ) → u ∈ v)
  (e)  { x  |  φ(x) } ∈ y ↔ ∀ u (u  =  { x  |  φ(x) }  → u ∈ y)

+++ if the formula would be rendered correctly it should look like this:
  y ∈ { x | φ(x) }   ↔ ℳ(y) ∧ φ(y) (a)
 y = { x |  φ(x) }   ↔ ∀ z  (z ∈ y ↔ z ∈ { x | φ(x) }) (b)
 { x | φ(x) } = { x | ψ(x) }   ↔ ∀ z  (z ∈ { x | φ(x) } (c)
       ↔ z ∈ {x | ψ(x) })
 { x | φ(x) } ∈ { x | ψ(x) }   ↔ ∀ u  ∀ v  ((u = { x | φ(x) }
      ∧  v = { x | ψ(x) }) → u ∈ v) (d)
 { x | φ(x) } ∈ y   ↔ ∀ u  (u = { x | φ(x) } → u ∈ y) (e)

Proof:
The formula a) is simply axiom 3. We get b) and c) with proposition 1. And d)
and e) come from identity theormes.
q.e.d.

Therefore the new syntax can be eliminated by successive applying the above
theorems.


Because the new notation fixes a term completely the following must be true.

☉ Proposition 6   [theorem:setDefinitionUnique]

     ∃! x x  =  { y  |  φ(y) }

Proof:


 ∃!  x  ∀  z  ( z ∈ x  ↔  ℳ(z) ∧ φ(z))   this is proposition 4
 ∃!  x  ∀  z  ( z ∈ x  ↔ z ∈ { y  |   φ(y) }   proposition 5 (a)
 ∃!  x  x = { y  |   φ(y) }   proposition 1
q.e.d.


The equivalence of properties enables us to conclude the identity of the
associated classes.

☉ Proposition 7   [theorem:propositionEqualImplClassEqual]

     ∀ x (φ(x) ↔ ψ(x)) → { x  |  φ(x) }  =  { x  |  ψ(x) }

Proof:


 (φ(x) ↔ ψ(x)) →   (φ(x) ∧ ℳ(x) ↔ ψ(x) ∧ ℳ(x))    proposition 1 (bl) [l]
 ∀ x  ((φ(x) ↔ ψ(x)) →   (φ(x) ∧ ℳ(x) ↔ ψ(x) ∧ ℳ(x)))    rule 11 [l]
 ∀ x  (φ(x) ↔ ψ(x)) →   ∀ x  (φ(x) ∧ ℳ(x) ↔ ψ(x) ∧ ℳ(x))    proposition 2 [l]
 →   ∀ x ( x ∈ { y | φ(y) } ↔ x ∈ { y | ψ(y) })    proposition 5 (a)
 →    { y  |  φ(y) } = { y  |  ψ(y) }    proposition 5 (c)
q.e.d.

We remark that the reverse implication is false. This is due to the fact that
the class notation embraces only sets. For example: if φ(x) ↔ x ≠ x and ψ(x) ↔ ∀
y  (y ∈ x → y ∉ y) then the associated classes are identical to the empty class
(definition 6). No class fulfills φ(x) but Russells class (definition 4)
satifies ψ(x).


Every class can be described by a property: being a member of the class.

☉ Proposition 8   [theorem:classDescriptionPossible]

     x  =  { y  |  y ∈ x }

Proof:


 z ∈ x   ↔   z ∈ x ∧ ℳ(z)   proposition 2
 z ∈ x   ↔   z ∈ {y  |  y }   proposition 5 (a)
 ∀ z  (z ∈ x   ↔   z ∈ {y  |  y })   rule 11 [l]
 x   =   {y  |  y }   proposition 1
q.e.d.



1.2 Special Classes
―――――――――――――――――――

In this section we define our first classes.


Russells class can now be simply defined.

☉ Definition 4  (Russell Class)  [definition:RussellClass]

     ℛu  ≔  { x  |  x ∉ x }


The Russell class is a  p r o p e r  class. This means it is no set.

☉ Proposition 9   [theorem:RussellClassIsClass]

     ¬ ℳ(ℛu)

Proof:


 y ∈ { x  |  φ(x) }   ↔   ℳ(y) ∧ φ(y)   this is proposition 5 (a)
 y ∈ { x  |  x ∉ x }   ↔   ℳ(y) ∧ y ∉ y   substitution for φ
 y ∈ ℛu   ↔   ℳ(y) ∧ y ∉ y   definition 4
 ℛu ∈ ℛu   ↔   ℳ(ℛu) ∧ ℛu ∉ ℛu   substitution for y
 ℳ(ℛu) ∧ ℛu ∈ ℛu   ↔   ℳ(ℛu) ∧ ℛu ∉ ℛu   proposition 2
   ¬ ℳ(ℛu)     proposition 1 (bi) [l]
q.e.d.


The  u n i v e r s a l   c l a s s  should contain everything.

☉ Definition 5  (Universal Class)  [definition:universalClass]

     Ʋ  ≔  { x  |  x  =  x }


It is no wonder that the following is true because a class has only sets as
elements.

☉ Proposition 10   [theorem:isInUniversalClass]

     x ∈ Ʋ ↔ ℳ(x)

Proof:


 x ∈ { y  |  φ(y) }   ↔   ℳ(x) ∧ φ(x)   this is proposition 5 (a)
 x ∈ { y  |  y = y }   ↔   ℳ(x) ∧ y = y   substitution for φ
 x ∈ Ʋ   ↔   ℳ(x) ∧ y = y   definition 5
 x ∈ Ʋ   ↔   ℳ(x)   proposition 1 (au) [l] and axiom 7 [l]
q.e.d.

Being in the universal class is therefore the same as being a set.


The universal class contains all sets.

☉ Proposition 11   [theorem:universalClassContainsAllSets]

     Ʋ  =  { x  |  ℳ(x) }

Proof:


 Ʋ   =   { x  |  x = x}   definition 5
 ∀ y  (y ∈ Ʋ   ↔   y ∈ { x  |  x = x}   proposition 1
 ∀ y  (y ∈ Ʋ   ↔   ℳ(y) ∧ y = y   proposition 5 (a)
 ∀ y  (y ∈ Ʋ   ↔   ℳ(y) ∧ ⊤   rule 10 [l]
 ∀ y  (y ∈ Ʋ   ↔   ℳ(y)   proposition 1 (au) [l]
 ∀ y  (y ∈ Ʋ   ↔    ℳ(y) ∧ ℳ(y)   proposition 1 (al) [l]
 ∀ y  (y ∈ Ʋ   ↔   y ∈ { x  |  ℳ(x)}   proposition 5
 Ʋ   =   { x  |  ℳ(x)}   proposition 1
q.e.d.


Analogous we define the  e m p t y   c l a s s . Later on we will learn that the
empty class is a set. To achieve this result we lack some other set axioms.
Nevertheless we might already call this class  e m p t y   s e t  sometime.

☉ Definition 6  (Empty Class)  [definition:emptySet]

     ∅  ≔  { x  |  x  ≠  x }


No class is element of the empty class.

☉ Proposition 12   [theorem:noClassIsMemberOfEmptySet]

     ∀ z z ∉ ∅

Proof:
Asumption: z ∈ ∅

 z ∈ { x  |  x ≠ x}   definition 6
 ℳ(z)  ∧ z  ≠ z   axiom 3
 z ≠ z   elementary logic
 ¬  (z = z)   definition 4 [l]

So we have a contradiction to axiom 7 [l] and our asumption must be false. So we
have ¬ (z ∈ ∅) and can conclude the following.

 ¬  ( z ∈ ∅)
 z ∉ ∅   definition 2
 ∀ z  z ∉ ∅   rule 11 [l]
q.e.d.


A class with no elements is the empty class.

☉ Proposition 13   [theorem:noClassIsMemberIsEmptySet]

     ∀ z z ∉ x ↔ x  =  ∅

Proof:


 x = ∅   ↔   ∀ z  (z ∈ x ↔ z ∈ ∅)   proposition 1
   ↔   ∀ z  (z ∉ x ↔ z ∉ ∅)   rule 8 [l] with proposition 1 (ao) [l]
   ↔   ∀ z  (z ∉ x ↔  ⊤)   proposition 12
   ↔   ∀ z  z ∉ x   rule 8 [l] with proposition 1 (be) [l]
q.e.d.




___________________________________________________


Chapter 2 


Boolean Algebra of Classes
══════════════════════════

Now the elementary class operations and their properties are described. A
 b o o l e a n   a l g e b r a  is an algebraic structure that abstracts from
the logical operators  a n d ,  o r ,  n o t  and their set theoretic
connectives  i n t e r s e c t i o n ,  u n i o n ,  c o m p l e m e n t .

The name is due to  G .   B o o l e  who defined this structure to be able to
use algebraic methods within propositional calculus.


2.1 Boolean Class Operators
―――――――――――――――――――――――――――

With the classs notation rule 1 we can define new class operators with the help
of logical connectives.


The union of two classes contains exactly all elements of both classes.

☉ Definition 7  (Union Operator)  [definition:union]

     (x ∪ y)  ≔  { z  |  (z ∈ x ∨ z ∈ y) }


Analogous the intersection of two classes is defined as the class which contains
exactly those elements that are member of both classes.

☉ Definition 8  (Intersection Operator)  [definition:intersection]

     (x ∩ y)  ≔  { z  |  (z ∈ x ∧ z ∈ y) }


Also the complement of a class can be simply defined.

☉ Definition 9  (Complement Operator)  [definition:complement]

     ∁x  ≔  { z  |  z ∉ x }


If a set is an element of the union of two classes can be checked directly.

☉ Proposition 14   [theorem:unionMember]

     z ∈ (x ∪ y) ↔ (z ∈ x ∨ z ∈ y)

Proof:


 (x ∪ y)   =   { z  |  (z ∈ x ∨ z ∈ y ) }   definition 7
 u ∈ (x ∪ y)   ↔   u ∈ { z  |  (z ∈ x ∨ z ∈ y ) }   proposition 3 [l]
 u ∈ (x ∪ y)   ↔   (ℳ(u) ∧ (u ∈ x ∨ u ∈ y))   axiom 3
 u ∈ (x ∪ y)   ↔   ((ℳ(u) ∧ u ∈ x ) ∨ (ℳ(u) ∧ u ∈ y))   proposition 1 (at) [l]
 u ∈ (x ∪ y)   ↔   (u ∈ x ∨ u ∈ y)   proposition 2
q.e.d.


Membership of an intersection can be written down directly too.

☉ Proposition 15   [theorem:intersectionMember]

     z ∈ (x ∩ y) ↔ (z ∈ x ∧ z ∈ y)

Proof:


 (x ∩ y)   =   { z  |  (z ∈ x ∧ z ∈ y ) }   definition 7
 u ∈ (x ∩ y)   ↔   u ∈ { z  |  (z ∈ x ∧ z ∈ y ) }   proposition 3 [l]
 u ∈ (x ∩ y)   ↔   (ℳ(u) ∧ (u ∈ x ∧ u ∈ y))   axiom 3
 u ∈ (x ∩ y)   ↔   ((ℳ(u) ∧ u ∈ x ) ∧ u ∈ y))   proposition 1 (aj) [l]
 u ∈ (x ∩ y)   ↔   (u ∈ x ∧ u ∈ y)   proposition 2
q.e.d.


For the membership of the complement we have a similar result but here we must
check the property  i s   a   s e t  explicitly.

☉ Proposition 16   [theorem:complementMember]

     z ∈ ∁x ↔ (ℳ(z) ∧ z ∉ x)

Proof:


 ∁x   =   { z  |  z ∉ x }   definition 9
 u ∈ ∁x   ↔   u ∈ { z  |  z ∉ x }   proposition 3 [l]
 u ∈ ∁x   ↔   (ℳ(u) ∧ u ∉ x)   axiom 3
q.e.d.


By the previous propositions we learned how to transform the logical operators
∨, ∧ and ¬ into the class operators ∪, ∩ and ‾ . So we are now able to transform
the logical laws into set theoretic propositions.

☉ Proposition 17   [theorem:unionIntersectionComplement]

  (a)  (x ∪ y)  =  (y ∪ x)
  (b)  (x ∩ y)  =  (y ∩ x)
  (c)  ((x ∪ y) ∪ z)  =  (x ∪ (y ∪ z))
  (d)  ((x ∩ y) ∩ z)  =  (x ∩ (y ∩ z))
  (e)  x  =  (x ∪ x)
  (f)  x  =  (x ∩ x)
  (g)  ∁∁x  =  x
  (h)  ∁(x ∪ y)  =  (∁x ∩ ∁y)
  (i)  ∁(x ∩ y)  =  (∁x ∪ ∁y)
  (j)  (x ∪ (y ∩ z))  =  ((x ∪ y) ∩ (x ∪ z))
  (k)  (x ∩ (y ∪ z))  =  ((x ∩ y) ∪ (x ∩ z))
  (l)  ∁∅  =  Ʋ
  (m)  ∁Ʋ  =  ∅
  (n)  (x ∩ Ʋ)  =  x
  (o)  (x ∩ ∅)  =  ∅
  (p)  (x ∪ Ʋ)  =  Ʋ
  (q)  (x ∪ ∅)  =  x
  (r)  (x ∪ ∁x)  =  Ʋ
  (s)  (x ∩ ∁x)  =  ∅

Proof:
MISSING! OTHER: Exemplarisch beweisen wir (g).

 u ∈ x   ↔   (ℳ(u) ∧ u ∈ x)   definition 9
   ↔   (⊥ ∨ (ℳ(u) ∧ u ∈ x))   proposition 1 (ax) [l]
   ↔   ((ℳ(u) ∧ ¬ ℳ(u)) ∨ (ℳ(u) ∧ u ∈ x))   proposition 1 (az) [l]
   ↔   (ℳ(u) ∧ (¬ ℳ(u)) ∧ u ∈ x))   proposition 1 (at) [l]
   ↔   (ℳ(u) ∧ (¬ ℳ(u)) ∧ ¬ ¬ u ∈ x))   proposition 1 (am) [l]
   ↔   (ℳ(u) ∧ (¬ ℳ(u)) ∧ ¬ u ∉ x))   definition 2
   ↔   (ℳ(u) ∧ ¬ (ℳ(u)) ∨ u ∉ x))   proposition 1 (aq) [l]
   ↔   (ℳ(u) ∧ ¬ (u ∈ ∁x))   proposition 16
   ↔   (ℳ(u) ∧ u ∉ ∁x)   definition 2
   ↔   u ∈ ∁∁x   proposition 16

Also haben wir gezeigt: u ∈ x ↔ u ∈ ∁∁x Nun können wir weiter schließen.

 u ∈ x   ↔   u ∈ ∁∁x
 ∀ u  (u ∈ x   ↔   u ∈ ∁∁x)   rule 11 [l]
 ∀ u  u ∈ x   ↔   ∀ u  u ∈ ∁∁x   proposition 2 [l]
 x   =   ∁∁x   proposition 3
q.e.d.



2.2 Boolean Algebra
―――――――――――――――――――

The classes build together with the operators ∩, ∪, ‾  and the constants ∅ a
Boolean algebra,

+++ References to commutative law, associative law, distributive law,
idempotence, etc.



2.3 Order
―――――――――

For a boolean algebra a  p a r t i a l   o r d e r  relation can be defined.
Therefore we can do the same for the boolean class algebra.


We define the  s u b c l a s s   r e l a t i o n  ( i n c l u s i o n ) by an
intersection.

☉ Definition 10  (Subclass Predicate)  [definition:subclass]

     x  ⊆  y  :↔  (x ∩ y)  =  x

If x and y are sets we also say: x is  s u b s e t  of y.


Now we get the common subclass definition as a proposition.

☉ Proposition 18   [theorem:subsetIfMemberschipImpl]

     x  ⊆  y ↔ ∀ z (z ∈ x → z ∈ y)


This relation is reflexive, transitive and antisymmetric. As intended it is a
partial order relation with ∅ as minimum and Ʋ as maximum element.

☉ Proposition 19   [theorem:subsetIsPartialOrdered]

  (a)  x  ⊆  x
  (b)  (x  ⊆  y ∧ y  ⊆  z) → x  ⊆  z
  (c)  (x  ⊆  y ∧ y  ⊆  x) ↔ x  =  y
  (d)  ∅  ⊆  x
  (e)  x  ⊆  Ʋ
  (f)  x  ⊆  ∅ → x  =  ∅
  (g)  Ʋ  ⊆  x → x  =  Ʋ


An intersection is always a subclass of its original classes.

☉ Proposition 20   [theorem:intersectionIsSubset]

  (a)  (x ∩ y)  ⊆  x
  (b)  (x ∩ y)  ⊆  y


A union has its original classes as subclasses.

☉ Proposition 21   [theorem:unionIsSuperset]

  (a)  x  ⊆  (x ∪ y)
  (b)  y  ⊆  (x ∪ y)


With two classes the union of both is also subclass. And if a class is subclass
of two other classes it is also subclass of their intersection. For both
implications the reverse is also true.

☉ Proposition 22   [theorem:subsetAndAddition]

  (a)  (x  ⊆  z ∧ y  ⊆  z) ↔ (x ∪ y)  ⊆  z
  (b)  (z  ⊆  x ∧ z  ⊆  y) ↔ z  ⊆  (x ∩ y)


Intersection and union of a class does not change an existing subclass relation.

☉ Proposition 23   [theorem:subsetAddition]

  (a)  x  ⊆  y → (x ∪ z)  ⊆  (y ∪ z)
  (b)  x  ⊆  y → (x ∩ z)  ⊆  (y ∩ z)


Complement building inverts the subclass relation.

☉ Proposition 24   [theorem:subsetComplement]

     x  ⊆  y ↔ ∁y  ⊆  ∁x


For the complement and subclass relation the following equivalences hold.

☉ Proposition 25   [theorem:subsetComplementEquations]

  (a)  x  ⊆  y ↔ (x ∩ ∁y)  =  ∅
  (b)  x  ⊆  y ↔ (∁x ∪ y)  =  Ʋ
  (c)  x  ⊆  ∁y ↔ (x ∩ y)  =  ∅
  (d)  (x ∩ y)  ⊆  z ↔ x  ⊆  (∁y ∪ z)



2.4 Singletons and Class Pairs
――――――――――――――――――――――――――――――

A class can be defined by explicitly listing its members.


Especially by saying that one element is inside the class we can define the so
called  s i n g l e t o n . With proposition 4 again we can extend the syntax
and provide a new abbreviation.

☉ Definition 11  (Singleton)  [definition:singleton]

     { x }  ≔  { y  |  (ℳ(x) → y  =  x) }

If x is a proper class the term {x} is also defined. In this case all sets y
fulfill the condition ℳ(y) ∧ (ℳ(x) → y = x) and the singleton is identical with
the universal class. This leads to a smother handling of the singleton.
          ┌
          │ Other authors as K. Gödel for example define {x} = {y | y = x}.
          └



For sets the singleton has only the set itself as a member.

☉ Proposition 26   [theorem:setSingletonHasSetAsOnlyElement]

     ℳ(x) → ∀ z (z ∈ { x } ↔ z  =  x)


If we have a proper class the singleton is the universal class.

☉ Proposition 27   [theorem:properSingletonIsUniversalClass]

     ¬ ℳ(x) → { x }  =  Ʋ


Beeing a set singleton is equivalent to be member of its singleton.

☉ Proposition 28   [theorem:setSingletonEqualHasItselfAsElement]

     ℳ(x) ↔ x ∈ { x }


Now we can simply define the  p a i r  class as union of two singletons.

☉ Definition 12  (Pair)  [definition:pair]

     { x, y }  ≔  ({ x } ∪ { y })


A class pair can be described directly without referencing singletons.

☉ Proposition 29   [theorem:classPairIsEqual]

     { x, y }  =  { z  |  ((ℳ(x) ∧ ℳ(y)) → (z  =  x ∨ z  =  y)) }


For set pairs beeing a member of a pair can canonically be simplified.

☉ Proposition 30   [theorem:membershipOfClassPair]

     (ℳ(x) ∧ ℳ(y)) → ∀ z (z ∈ { x, y } ↔ (z  =  x ∨ z  =  y))


If one of the classes for building a class pair is proper the resulting pair is
identical to the universal set.

☉ Proposition 31   [theorem:properClassPairIsUniversalClass]

     (¬ ℳ(x) ∨ ¬ ℳ(y)) → { x, y }  =  Ʋ


We note that building a class pair is commutative.

☉ Proposition 32   [theorem:classPairBuildingIsCommutative]

     { x, y }  =  { y, x }


The singleton can be expressed as a special case of a class pair.

☉ Proposition 33   [theorem:singletonIsClassPair]

     { x }  =  { x, x }


Being a set is equivalent to being element of a class pair.

☉ Proposition 34   [theorem:setEquiInClassPair]

     ℳ(x) ↔ x ∈ { x, y }


For sets being an element is equal to being a subclass of its singleton.

☉ Proposition 35   [theorem:elementEquiSingletonSubclass]

     ℳ(x) → (x ∈ y ↔ { x }  ⊆  y)


Identity of set pairs behaves as expected.

☉ Proposition 36   [theorem:pairIdentities]

     (ℳ(x) ∧ ℳ(y) ∧ ℳ(u) ∧ ℳ(v)) → ({ x, y }  =  { u, v } → ((x  =  u ∧ y  =  v)
∨ (x
=  v ∧ y  =  u)))



2.5 Infinite Boolean Operators
――――――――――――――――――――――――――――――

It is also possible to build infinite intersections and unions. It must only be
declared which classes are used to build the result.


For a class of sets a  p r o d u c t  is defined: all sets that are elements of
each set are member of the product.

☉ Definition 13  (Set Product)  [setProduct]

     ⋂  x  ≔  { z  |  ∀ y (y ∈ x → z ∈ y) }

This function can be viewed as a generalization of the intersection operation.
See also proposition 46.

We also say the class x defines a  f a m i l y   o f   s e t s . Any element of
x is a member of the family.


As usual we can describe the membership of the set product as follows.

☉ Proposition 37   [theorem:setProductMembership]

     z ∈ ⋂  x ↔ (ℳ(z) ∧ ∀ y (y ∈ x → z ∈ y))


We find for the special case of x = ∅.

☉ Proposition 38   [theorem:emptySetProduct]

     ⋂  ∅  =  Ʋ


If we build the set product of a non empty class we can drop the set condition.

☉ Proposition 39   [theorem:nonEmptySetProductMembership]

     x  ≠  ∅ → (z ∈ ⋂  x ↔ ∀ y (y ∈ x → z ∈ y))


Analogous we can define the  s e t   s u m . Exactly the elements, that are
member of some set in the family, should be member of the set sum.

☉ Definition 14  (Set Sum)  [definition:setSum]

     ⋃  x  ≔  { z  |  ∃ y (y ∈ x ∧ z ∈ y) }


The set sum membership can be expressed by the following formula.

☉ Proposition 40   [theorem:setSumMembership]

     z ∈ ⋃  x ↔ ∃ y (y ∈ x ∧ z ∈ y)

Here we can drop the set condition ℳ(z).


For the empty class we obtain.

☉ Proposition 41   [theorem:emptySetSum]

     ⋃  ∅  =  ∅


The subclass relation behaves to the set product and sum as follows.

☉ Proposition 42   [theorem:subsetSumProductImplication]

  (a)  x  ⊆  y → ⋂  y  ⊆  ⋂  x
  (b)  x  ⊆  y → ⋃  x  ⊆  ⋃  y


The membership relation induces subclass relations in the following way.

☉ Proposition 43   [theorem:membershipToSetProductAndSum]

  (a)  x ∈ y → x  ⊆  ⋃  y
  (b)  x ∈ y → ⋂  y  ⊆  x


The union and intersection operation match with the set sum and set product as
follows.

☉ Proposition 44   [theorem:unionIntersectionSetSumProduct]

  (a)  ⋂  (x ∪ y)  =  (⋂  x ∩ ⋂  y)
  (b)  ⋃  (x ∪ y)  =  (⋃  x ∪ ⋃  y)
  (c)  ⋃  (x ∩ y)  ⊆  (⋃  x ∩ ⋃  y)


In case of a non empty set family we have this.

☉ Proposition 45   [theorem:nonEmptySumProductSubSet]

     ∀ x (x  ≠  ∅ → ⋂  x  ⊆  ⋃  x)


For set pairs we get the expected results.

☉ Proposition 46   [theorem:setPairSetSumProduct]

  (a)  (ℳ(x) ∧ ℳ(y)) → ⋂  { x, y }  =  (x ∩ y)
  (b)  (ℳ(x) ∧ ℳ(y)) → ⋃  { x, y }  =  (x ∪ y)


For set singletons we get analogous statements.

☉ Proposition 47   [theorem:singletonSetSumProduct]

  (a)  ℳ(x) → ⋂  { x }  =  x
  (b)  ℳ(x) → ⋃  { x }  =  x



2.6 Power Class Building
――――――――――――――――――――――――

We can now introduce an important new class operator.


The subset relation helps us to create another class operator: the  p o w e r
 c l a s s   o p e r a t i o n .

☉ Definition 15  (Power Class)  [definition:power]

     ℘(x)  ≔  { z  |  z  ⊆  x }


For this new operator the following propositions hold.

☉ Proposition 48   [theorem:powerPropositions]

  (a)  z ∈ ℘(x) ↔ (ℳ(x) ∧ z  ⊆  x)
  (b)  ℘(Ʋ)  =  Ʋ
  (c)  ℘(∅)  =  { ∅ }
  (d)  ℳ(x) ↔ x ∈ ℘(x)
  (e)  x  ⊆  y → ℘(x)  ⊆  ℘(y)
  (f)  (ℳ(x) ∧ ℘(x)  ⊆  ℘(y)) → x  ⊆  y
  (g)  ℘((x ∩ y))  =  (℘(x) ∩ ℘(y))
  (h)  (℘(x) ∪ ℘(y))  ⊆  ℘((x ∪ y))
  (i)  x  ⊆  ℘(⋃  x)
  (j)  ⋃  ℘(x)  ⊆  x


Especially for power sets the following proposition holds.

☉ Proposition 49   [theorem:powerSetPropositions]

     ℳ(x) → x  =  ⋃  ℘(x)

Later on we can drop the set condition because of new axioms.




___________________________________________________


Chapter 3 


Sets, Relations and Functions
═════════════════════════════

In this chapter we concentrate on the property  i s   a   s e t  and we
introduce new axioms to assure the existence of sets.

To be able to define relations within our theory we need the new class operator
 o r d e r e d   p a i r . With this operator we can define  C a r t e s i a n
 p r o d u c t s  of classes. Relations are no other than subclasses of
Cartesian products and fulfill the laws of an  u n i v e r s a l   a l g e b r a
.

A special kind of relations are the  e q u i v a l e n c e   r e l a t i o n s
which form a more abstract form of equality. Functions are also a special kind
of relations. The axiom of replacement guaranties that sets are mapped onto
sets.


3.1 Sets
――――――――

For the presentation of the boolean class algebra we needed no set theoretic
axioms. In the following we get some more axioms that give conditions for being
a set.


The empty class should be a set.

☉ Axiom 4  (Empty Set Axiom)  [axiom:emptySet]

     ℳ(∅)

This is the first time we know about the existence of a set.


To ensure the set property for set pairs we have out next axiom.

☉ Axiom 5  (Pairing Set Axiom)  [axiom:pairingSet]

     (ℳ(x) ∧ ℳ(y)) → ℳ({ x, y })


The sum set of a set should be a set too.

☉ Axiom 6  (Axiom of the Sum Set)  [axiom:setSumSet]

     ℳ(x) → ℳ(⋃  x)


´The power class of a set should also be a set.

☉ Axiom 7  (Power Set Axiom)  [axiom:powerSet]

     ℳ(x) → ℳ(℘(x))


The subclass of a set should also be a set.

☉ Axiom 8  (Subset Axiom)  [axiom:subset]

     (ℳ(x) ∧ y  ⊆  x) → ℳ(y)


The above set axioms enables us to construct sets. Starting with axiom 4 we have
one first set ∅. By applying axiom 7 we get the set { ∅ }. Building the power
class again provides the set { ∅, { ∅ } }. By repeating this procedure we get an
infinite number of sets.
          ┌
          │ One can easily show that they are all different.
          └


Furthermore we notice that our current axioms can show only the existence of
sets with a finite number of members. These finite classes are ‘save’ in the
following sense: they alone can not lead to the contradictions as the
unrestricted set theory of Zermelo.

The new axioms enable us to derive some more propositions.

☉ Proposition 50   [theorem:isSet]

  (a)  (¬ ℳ(y) ∧ y  ⊆  x) → ¬ ℳ(x)
  (b)  ¬ ℳ(Ʋ)
  (c)  (ℳ(x) ∧ ℳ(y)) → ℳ((x ∪ y))
  (d)  (ℳ(x) ∧ ℳ(y)) → ℳ((x ∩ y))
  (e)  ℳ(x) → ℳ({ x })
  (f)  ℳ(x) → ¬ ℳ(∁x)
  (g)  x  =  ⋃  ℘(x)
  (h)  ℳ(x) ↔ ℳ(⋃  x)
  (i)  ⋂  Ʋ  =  ∅
  (j)  ⋃  Ʋ  =  Ʋ
  (k)  x  ≠  ∅ → ℳ(⋂  x)



3.2 Ordered Pair
――――――――――――――――

The concept of an ordered pair is vital for our further development. It enables
us to arrange objects. Till now our object collections did not depend on the
order of gathering. We wish to figure out which element was  f i r s t  and
which element was  s e c o n d  after wards.


Our definition of an  o r d e r e d   p a i r  〈 x, y〉 is due to
 N .  W i e n e r  (1914) and  K .  K u r a t o w s k i  (1921).

☉ Definition 16  (Ordered Pair)  [definition:orderedPair]

     〈 x, y 〉  ≔  { { x }, { x, y } }


For an ordered pair of sets the order of the defining elements matters. Ordered
pairs should only be identical if their first elements are identical and their
second elements are identical.

☉ Proposition 51   [theorem:orderedPairEquality]

     (ℳ(x) ∧ ℳ(y) ∧ ℳ(u) ∧ ℳ(v)) → (〈 x, y 〉  =  〈 u, v 〉 → (x  =  u ∧ y  =  v))


An ordered pair made of sets is also a set. The reverse is also true.

☉ Proposition 52   [theorem:orderedPairOfSets]

     (ℳ(x) ∧ ℳ(y)) ↔ ℳ(〈 x, y 〉)


If one of the classes is not a set the resulting ordered pair is identical with
the universal class.

☉ Proposition 53   [theorem:orderedPairWithNonSet]

     (¬ ℳ(x) ∨ ¬ ℳ(y)) → 〈 x, y 〉  =  Ʋ


To speak of ordered pairs we need a predicate that says ‘is an ordered pair’.

☉ Definition 17  (Ordered Pair Property)  [definition:isOrderedPair]

     isOrderedPair(x)  :↔  ∃ u ∃ v x  =  〈 u, v 〉

We notice that Ʋ is also an ordered pair. But because we mostly speak about
class members we must only deal with sets that might be ordered pairs.



3.3 Cartesian Product
―――――――――――――――――――――

For the ordered pairs we need a meta structure. We just assemble ordered pairs
into a class.


The  C a r t e s i a n   p r o d u c t
          ┌
          │ Named after the the French philosopher and mathematician
          │  R .  D e s c a r t e s  also known as  C a r t e s i u s .
          └
 also called  d i r e c t   p r o d u c t  is the class of all ordered pairs,
which elements are members of the origin classes.

☉ Definition 18  (Cartesian Product)  [definition:cartesianProduct]

     ( x × y)  ≔  { z  |  ∃ u ∃ v (u ∈ x ∧ v ∈ y ∧ z  =  〈 u, v 〉) }



3.4 Relations
―――――――――――――

It is important to be able to express relations between mathematical objects and
to handle them as objects too. It turns out that we do not have to introduce new
kinds of objects. Our current structures are sufficient.


We are now able to define a  r e l a t i o n  within our set theory.

☉ Definition 19  (Relation)  [definition:relation]

     ℛℯℓ(x)  :↔  ∀ y (y ∈ x → isOrderedPair(y))


Some propositions about relations.

☉ Proposition 54   [theorem:relationProperties]

  (a)  ℛℯℓ(∅)
  (b)  ℛℯℓ(( Ʋ × Ʋ))
  (c)  (ℛℯℓ(x) ∧ ℛℯℓ(y)) → ℛℯℓ((x ∩ y))
  (d)  (ℛℯℓ(x) ∧ ℛℯℓ(y)) → ℛℯℓ((x ∪ y))


We now give an universal definition of the concept  d o m a i n .

☉ Definition 20  (Domain)  [definition:domain]

     Dℴm(x)  ≔  { y  |  ∃ z 〈 y, z 〉 ∈ x }


Analogous to the domain we specify the  r a n g e  of a class.

☉ Definition 21  (Range)  [definition:range]

     ℛnℊ(x)  ≔  { y  |  ∃ z 〈 z, y 〉 ∈ x }



3.5 Relation Algebra
――――――――――――――――――――

+++



3.6 Equivalence Relations
―――――――――――――――――――――――――

+++



3.7 Maps and Functions
――――――――――――――――――――――

+++


A function is just a special sort of relation.

☉ Definition 22  (Function)  [definition:function]

     ℱunct(x)  :↔  ℛℯℓ(x) ∧ ∀ y (y ∈ Dℴm(x) → ∃! z 〈 y, z 〉 ∈ x)


If the domain of a function is a set so its range should be a set too.

☉ Axiom 9  (Fraenkel’s Replacement Axiom)  [axiom:FraenkelsReplacement]

     (ℱunct(f) ∧ ℳ(Dℴm(f))) → ℳ(ℛnℊ(f))




___________________________________________________


Chapter 4 


Natural Numbers
═══════════════

+++


4.1 Foundation and Infinity
―――――――――――――――――――――――――――

+++


Sets x should not contain itself as a member, or contain an element that
contains x. To avoid these and further membership circles we provide the
following axiom.

☉ Axiom 10  (Axiom of Foundation)  [axiom:foundation]

     x  ≠  ∅ → ∃ y (y ∈ x ∧ (y ∩ x)  =  ∅)

This axiom is also called axiom of regularity.


A canonical class extension is the union with its singleton.

☉ Definition 23  (Successor)  [definition:successor]

     x’  ≔  (x ∪ { x })

Because x ∉ x the successor function adds just one element to the original
class.


We want to have a set with an infinite number of elements. So we just postulate
its existence.

☉ Axiom 11  (Axiom of Infinity)  [axiom:infinity]

     ∃ x (ℳ(x) ∧ ∅ ∈ x ∧ ∀ y (y ∈ x → y’ ∈ x))



4.2 Definition and Basic Properties
―――――――――――――――――――――――――――――――――――

+++



4.3 Induction
―――――――――――――

+++



4.4 Sequences and Normal Functions
――――――――――――――――――――――――――――――――――

+++



4.5 Recursion
―――――――――――――

+++




___________________________________________________


Chapter 5 


Axiom of Choice
═══════════════

+++


5.1 Well-Ordering
―――――――――――――――――

MISSING! OTHER: +++


Now we come to the famous axiom of choice. We write it down for relations.

☉ Axiom 12  (Axiom of Choice)  [axiom:choice]

     ℛℯℓ(x) → ∃ y (ℱunct(y) → (y  ⊆  x ∧ Dℴm(x)  =  Dℴm(y)))



5.2 Applications of the Axiom of Choice
―――――――――――――――――――――――――――――――――――――――






___________________________________________________


Chapter 6 


Continuum
═════════

MISSING! OTHER: 



___________________________________________________




Bibliography
════════════




Used other QEDEQ modules:

[l] qedeq_logic_v1  http://www.qedeq.org/0_04_00/doc/math/qedeq_logic_v1.xml


Other references:

[lemmon]  E .   J .   L e m m o n , Introduction to Axiomatic Set Theory, 
Routledge &
Kegan Paul Ltd, London 1968

[monk]  J .   D .   M o n k , Introduction to Set Theory, McGraw-Hill, New York 
1996

[schmidt]  J .   S c h m i d t , Mengenlehre I, BI, Mannheim 1966