Go backward to 6.1 Further NotionsGo up to 6 More on FunctionsGo forward to 6.3 Embedding Sets |

A set is

Sis finite : <=>S=0\/( existsninN_{>0},f:f:N_{n}->^{bijective}S);| S| :=ifS=0then0else( suchninN_{>0}:existsf:f:N_{n}->^{bijective}S).

Sis infinite : <=> ~Sis finite.

Sometimes the set size |`S`| is also denoted as #`S`. Please
note that |`S`| is only defined, if `S` is finite. In this case,
however, it is uniquely defined because the number of elements is independent
of the order in which we count them, i.e., independent of the particular
bijection chosen.

( forallS!=0,ninN,minN,f:N_{n}->^{bijective}S,g:N_{m}->^{bijective}S:m=n).

Assume `m` < `n` (the case `m` > `n` proceeds
analogously). We know `f` o `g`^{-1}: **N**_{n} ->^{bijective} **N**_{m}. However, since **N**_{n} has `n` elements,
**N**_{m} has `m` elements, and `m` < `n`,
`f` o `g`^{-1} cannot be injective (*pigeonhole
principle*, a fact that has to be proved separately).

- The set S := {0, 2, 4} is finite; its size is 3 because we can
define a function
`f`:**N**_{3}->^{bijective}`S`as

i.e., f = [0, 2, 4]. The length of f is the same as the length of [0, 4, 2], [4, 2, 0] or of any other bijection to`f`(0):= 0 `f`(1):= 2 `f`(2):= 4 `S`. - The set
**N**is infinite. If it were finite, we had some`n`in**N**and some f:**N**_{n}->^{bijective}**N**. Take`k`:= 1+max{`f`(`i`):`i`in**N**_{n}}. Then, by construction,`k`in**N**but**forall**i in**N**_{n}:`f`(i) !=`k`, i.e.,`f`is not surjective on**N**.

A constructive way to determine the number of elements of a set is shown by the following recursive definition:

size( S) :=ifS=0then0else lete= (suchx:xinS):1+size( S-e)

We then have |`S`| = size(`S`), for every finite set
`S`. However, to show that above recursive definition indeed defines
a function itself relies on the termination term |`S`|: therefore we
give a constructive definition in terms of
set reduction:

| S| := reduce(count,S, 0);count( e,i) :=i+1.

**Logic Evaluator**
The constructive definitions introduced above can be implemented as follows:

We sometimes count the number of values for which a proposition holds.

#is a term wherex:F

|{x:F}|.

Please note that the value of such a "number" term is only defined if the base formula is true for a finite number of assignments for the bound variable.

We state the following facts (whose proofs can be easily given by induction).

The size of the Cartesian product of two sets is the product of their sizes:

forallA,B,minN,ninN:( AintersectionB=0/\ |A| =m/\ |B| =n) => |AunionB| =m+n.

If A and B have size

forallA,B,minN,ninN:(| A| =m/\ |B| =n) => |AxB| =m*n.

If

forallA,B,minN,ninN:(| A| =m/\ |B| =n) => |A->B| =n^{m}.

forallA,ninN:| A| =n=> |{SinP(S): T}| = 2^{n}.

It may seem surprising, but we are able to distinguish between different kinds of "infinity", i.e., some sets are "more infinite" than others.

Sis countable : <=>existsf:f:N->^{bijective}S.

- The set
**Z**is infinite but it is countable because we can define a function`f`:**N**->^{bijective}**Z**as

i.e.,`f`(`x`) :=**if**`x`is even**then**-`x`/2**else**(`x`+1)/2`f`= [0, 1, -1, 2, -2, 3, -3, ...]. - The set
**Q**is infinite but countable; we sketch the construction of a corresponding enumeration. We can list all positive rationals in an infinite matrix that holds at position <`i`,`j`> the rational`i`+1/`j`+1:1/1 1/2 1/3 1/4 ... / / / 2/1 2/2 2/3 ... ... / / 3/1 3/2 ... ... ... / 4/1 ... ... ... ... ... ... ... ... ... `x`+`y`=2, then all fractions with`x`+`y`=3, then all fractions with`x`+`y`=4, and so on (always enumerating the fractions`x`+`y`=`c`in the order of increasing`x`).From this sequence, we have to remove all "doubles" (such as 2/2 which has already appeared previously as 1/1) constructing a corresponding sequence

`f`':**N**->**Q**that contains each positive rational number in*exactly*one position. Finally we can define an enumeration of the rationals by`g`:**N**->^{bijective}**Q**defined as

i.e.,`g`(`x`) :=**if**`x`= 0**then**0**else if**`x`is even**then**-`f`'(`x`/2)**else**`f`'((`x`-1)/2)`g`= [0, 1, -1, 1/2, -1/2, 2/1, -2/1, 1/3, -1/3, 3/1, -3/1, ...]. - The set of all infinite sequences over {0, 1} is
*not*countable: if it were, we had some`f`:**N**->^{bijective}(**N**-> {0,1}). Take`s`:**N**-> {0, 1} defined as`s`(`i`) :=`f`(`i`)_{i}:= 1-`d``d`. Then`s`differs from`f`(`i`) in the`i`-th digit (for every`i`in**N**), thus`s`is not contained in`f`.

The argument called`f`(0) =`f`(1) =`f`(2) =`f`(3) =... [ `f`(0)_0`f`(0)_{1}`f`(0)_{2}`f`(0)_{3}...] [ `f`(1)_{0}`f`(1)_1`f`(1)_{2}`f`(1)_{3}...] [ `f`(2)_{0}`f`(2)_{1}`f`(2)_2`f`(2)_{3}...] [ `f`(3)_{0}`f`(3)_{1}`f`(3)_{2}`f`(3)_3...] ... ... ... ... ... `s`:= [,`f`(0)_{0},`f`(1)_{1},`f`(2)_{2},...]`f`(3)_{3}*diagonalization (Diagonalisierung)*has been invented by Cantor to show the following result. - The set
**R**is*not*countable: every infinite sequence`d`of decimal digits represents a real number 0.`d`_{0}`d`_{1}`d`_{2}.... Since the set of all infinite sequences is not countable (and every real number is represented by a countable set of such sequences), also**R**is not countable.

Above example shows us that there exists a bijection between **N** and **Z**,
i.e., there is one distinct natural number for every integer number and vice
versa. It is therefore natural to consider **N** and **Z** of the *same
size*^{4}. The concept
of bijections can therefore be used to compare the size of sets.

One set isAandBare of same size : <=>existsf:f:A->^{bijective}B.

One set isAis not larger thanB: <=>existsf:f:A->^{injective}B.

Ais smaller thanB: <=>( Ais not larger thanB) /\ ~(AandBhave same size).

For finite sets, above notions clearly coincide with the definition of | |.

| A| = |B|=> AandBhave same size;| A| <= |B|=> Ais not larger thanB;| A| < |B|=> Ais smaller thanB.

However the new notions also allow us to compare the sizes of *infinite*
sets.

**N**has the same size as**Z**.**Z**has the same size as**Q**.**Q**is smaller than**R**.

**R**has the same size as**C**.

**N**,**Z**,**Q**(the enumerable ones),**R**,**C**(the not enumerable ones).

The hierarchy of "infiniteness" is not limited, because we can construct for every (also infinite) set a still larger set.

forallS:Sis smaller thanP(S).

Assume that

f:S->^{injective}P(S)f(x) := {x}.

Take `A` := {`x` in `S`: `x` not in `f`(`x`)}. Since `f` is surjective and `A` subset `S`, i.e., `A` in **P**(`S`),
we have some `a` in `S` with
`f`(`a`) = `A`. But then we know

ainA<=>anot inf(a) <=>anot inA.

Consequently, we know that **N** is smaller than **P**(**N**) which is
smaller than **P**(**P**(**N**)) which is smaller than
**P**(**P**(**P**(**N**))) which is ....

We also have the following result.

forallA,B:Bis smaller thanA->B.

**Permutations**
Bijections on subsets of **N** also of importance for sorting elements in a
particular order.

pis permutation of lengthn: <=>p:N_{n}->^{bijective}N_{n}.

pos= [b,a,e,d,c].

**Logic Evaluator**
Permutations can be easily implemented as follows.

**Input**:`A`...the element domain,- <= subset
`A`x`A`...a reflexive, antisymmetric, and transitive relation, `n`in**N**...the length of the sequence,`s`:**N**_{n}->`A`...a sequence of length`n`on`A`.

**Output**:`t`:**N**_{n}->`A`such that`t`is permutation of`s`,`t`is sorted with respect to <= .

`t`is permutation of`s`: <=>**let**`n`= length(`t`):`n`= length(`s`) /\**exists**`p`:`p`is permutation of length`n`/\`p`o`s`=`t`;`t`is sorted with respect to <= : <=>**forall**0 <=`i`< length(`t`):`t`_{i}<=`t`_{i+1}.

The set of permutations is closed under function composition.

The inverse of a permutation is a permutation of the same length:

forallninN,p,_{0}p:_{1}( pis permutation of length_{0}n/\p_{1}is permutation of lengthn) =>p_{0}op_{1}is permutation of lengthn.

forallninN,p:pis permutation of lengthn=>p^{-1}is permutation of lengthn.

e.g., (poq= [1,2,0,4,3],

e.g.,

p^{-1}= [2,0,1,4,3]

pop^{-1}=p^{-1}op= [0,1,2,3,4].

The following establishes some basic combinatorial knowledge.

forallninN: |{f:fis permutation of lengthn}| = 2^{n}.

If `n`=0, then the only permutation is `p` = [ ].

Assume |{`f`: `f`
is permutation of length `n`}| = 2^{n}.

We define

which returns the sequence constructed from

insert( x,i,f) :=suchs:length(s) = 1+length( f) /\foralljinN_{n+1}:j<i=>s(j) =f(j) /\j=i=>s(j) =x/\j>i=>s(j) =f(j-1)

Then we have

|{ f:fis permutation of lengthn+1}|= |{insert( n+1,i,f): i inN_{n+1}/\fis permutation of lengthn}|= ( n+1)*|{f:fis permutation of lengthn}|= ( n+1)*n= ( n+1)!

Author: Wolfgang Schreiner

Last Modification: October 4, 1999