background image

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 3.

(

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.

Definition 4.

Let

B

=

im

M

.

Theorem 5.

M

is a bijection from

B

to

B

.

Proof.

Surjectivity of

M

is obvious. Let’s prove injectivity.

Let

a, b

B

and

M

(

a

) =

M

(

b

)

. Consider all cases:

a, b

R

.

M

(

a

) =

E

1

a

;

M

(

b

) =

E

1

b

;

E

1

a

=

E

1

b

. Thus

a

=

b

because

E

1

is a bijection.

a

R

,

b

R

.

M

(

a

) =

E

1

a

;

M

(

b

) = (

t

;

b

)

;

M

(

a

)

S

;

M

(

b

)

S

. Thus

M

(

a

)

M

(

b

)

.

a

R

,

b

R

.

Analogous.

a, b

R

.

M

(

a

) = (

t

;

a

)

;

M

(

b

) = (

t

;

b

)

. Thus

M

(

a

) =

M

(

b

)

implies

a

=

b

.

Theorem 6.

M

E

=

id

S

.

Proof.

Let

x

S

. Then

Ex

R

;

M

(

Ex

) =

E

1

E x

=

x

.

I will call the above defined

B

and

M

the

ZF generalization

for a given generalization situation.

From the above follows that a ZF generalization is an arbitrary generalization.

6 Isabelle/ZF code

You can download the code from http://www.mathematics21.org/binaries/gen/isabelle-ZF.zip.

I formulate and prove the properties of generalization formally in the language ISAR of com-

puter proof assistant Isabelle.

First I define the theory file

ZF_Addons.thy

which contains some useful lemmas missing in the

current version of Isabelle/ZF core.

The main theory file

Generalization.thy

contains (among other) three locales:

generalization_situation

describing generalization situations;

arbitrary_generalization

describing arbitrary generalizations;

ZF_generalization

describing the ZF generalization.

Both

arbitrary_generalization

and

ZF_generalization

locales

are

derived

from

generalization_situation

locale.

Strictly speaking,

ZF_generalization

contains no new assumptions compared to its base,

generalization_situation

and all definitions from

ZF_generalization

could be put directly

into

generalization_situation

but I prefer to differentiate these two locales conceptually:

generalization_situation

being only about arbitrary generalization and not about ZF gen-

eralization in particular. Also this makes porting to other logics having no axiom of foundation
easier as only

ZF_generalization

locale is depended on the axiom of foundation.

Finally,

I

prove

that

ZF_generalization

is

a

special

case

(sublocale)

of

arbitrary_generalization

.

After that follows an example theory

int_obj_ex

. In this theory I define the set

int_obj

which is a set of integers considered as a generalization of the set

nat

of natural numbers. In this

example theory I prove the theorem that

int_obj

is a superset of

nat

. I suggest the convention to

use in Isabelle code the suffix

_obj

for sets

M

as in this example. (This convention is questionable

however, we may consider other possible conventions.)

Isabelle/ZF code

3