 APPENDIX A

Using logic of generalizations

A.1. Logic of generalization

In mathematics it is often encountered that a smaller set

S

naturally bijectively

corresponds to a subset

R

of a larger set

B

. (In other words, there is specified an

injection from

S

to

B

.) It is a widespread practice to equate

S

with

R

.

Remark

1946

.

I denote the first set

S

from the first letter of the word “small”

and the second set

B

from the first letter of the word “big”, because

S

is intuitively

considered as smaller than

B

. (However we do not require card

S <

card

B

.)

The set

B

is considered as a generalization of the set

S

, for example: whole

numbers generalizing natural numbers, rational numbers generalizing whole num-

bers, real numbers generalizing rational numbers, complex numbers generalizing

real numbers, etc.

But strictly speaking this equating may contradict to the axioms of ZF/ZFC

because we are not insured against

S

B

6

=

incidents. Not wonderful, as it is

often labeled as “without proof”.

To work around of this (and formulate things exactly what could benefit com-

puter proof assistants) we will replace the set

B

with a new set

B

0

having a bijection

M

:

B

B

0

such that

S

B

0

. (I call this bijection

M

from the first letter of the

word “move” which signifies the move from the old set

B

to a new set

B

0

).

The following is a formal but rather silly formalization of this situation in

ZF. (A more natural formalization may be done in a smarter formalistic, such as

dependent type theory.)

A.1.1. The formalistic.

Let

S

and

B

be sets. Let

E

be an injection from

S

to

B

. Let

R

= im

E

.

Let

t

=

P

S S

S

.

Let

M

(

x

) =

E

1

x

if

x

R

;

(

t, x

) if

x /

R.

Recall that in standard ZF (

t, x

) =

{

t,

{

t, x

}}

by definition.

Theorem

1947

.

(

t, x

)

/

S

.

Proof.

Suppose (

t, x

)

S

. Then

{

t,

{

t, x

}} ∈

S

. Consequently

{

t

} ∈

S

S

;

{

t

} ⊆

S S

S

;

{

t

} ∈

P

S S

S

;

{

t

} ∈

t

what contradicts to the axiom of foundation

(aka axiom of regularity).

Definition

1948

.

Let

B

0

= im

M

.

Theorem

1949

.

S

B

0

.

Proof.

Let

x

S

. Then

Ex

R

;

M

(

Ex

) =

E

1

Ex

=

x

;

x

im

M

=

B

0

.

Obvious

1950

.

E

is a bijection from

S

to

R

.

Theorem

1951

.

M

is a bijection from

B

to

B

0

.

Proof.

Surjectivity of

M

is obvious. Let’s prove injectivity. Let

a, b

B

and

M

(

a

) =

M

(

b

). Consider all cases:

386