Algebraic General Topology. Vol 1: Paperback / E-book || Axiomatic Theory off Formulas: Paperback / E-book

As an Amazon Associate I earn from qualifying purchases.

Gene rali zation in ZF
by Victor Porton
November 4, 2011
Abstract
In the framework of ZF are formally considered generalizations, such as whole numbers
generalizing natural numbers, rational numbers generalizing whole numbers, real numbers
generalizing rational numbers, complex numbers generalizing real numbers, etc. The formal
consideration of this may be especially useful for computer proof assistants. The article is
accompanied with usable Isabelle/ZF code.
Keywords: ZF, ZFC, generalization, formalistics, bijection, injection
A.M.S. subject classification: 03B30, 03E20
Table of contents
1 Preface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
2 Current state of the issue . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
3 The rationale and examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
4 Generalization situation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
5 ZF generalization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
6 Isabelle/ZF code . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
7 Future directions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1 Preface
In this article I define the notion of generalization in ZF set theory.
Examples: whole numb e rs generalizing natural numbers, rational numbers generalizing whole
numbers , real numbers generalizing rational numbers, complex numbers generalizing real numbers,
etc.
I also have implemented this theory in Isabelle/ZF proof assistant (see
http://isabelle.in.tum.de/inde x.html) formal language. This implementation is a candidate to be
actually useful in development of Isabelle/ZF theories. However my implementation may be not
ideal and may need further polishing before actual using in practice.
2 Current state of the issue
Whilst in informal mathematics is actively used the notio n of generalization, it usually refers
to intuition of the reader rather than to a formal consideration. This article provides a formal
consideration compatible with usual intuitive n otion of generalization.
In Isabelle proof assistant (both Isab elle/ZF and Isabelle/HOL) c urrently differ ent sets a re
defined independently. For example in Isabelle/ZF there are sets nat (natural numbers) and int
(integer numbers). It is not assumed that nat is a subset of int. T he only con ne c tion between these
provided is the function inf_of which tr ansforms a natural number into the corresponding integer.
Also as an effect of this, ope rations (such as additions) are defined differently and independently
for naturals and integers.
. This document has been written using the GNU T
E
X
MACS
text editor (see www.texmacs.org).
1
That state is not good.
3 The rationale and examples
In mathematics it is often encountered that a small set S naturally bijectively corresponds to a
subset R of a larger set B. (In other words, there is spe c ified an injection E from S t o B.) It is a
widespread practice to equate S with R.
Remark 1. I denote the first set S from the rst 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.) I denote the injection as E from the rst letter of
the word “e mbed because it embeds t he set S to the set B.
The set B is considered as a gene ralization of the set S, for example: whole numbe rs generalizing
natural numbers, rational numbers generalizing w hole numbers, real numbers gener alizing rational
numbers , complex numbers generalizing real numbe rs, etc.
Through these examples we see that B can be considered a generalization of S.
But strictly speaking this equating may contradict to the axioms of ZF/ZFC because we are
not insured against S B
incidents. Not wonderful, as it is ofte n labeled as “without proof”.
To work around of this (and formulate things exactly what could benefit computer proof
assistants) we will replace the se t B with a new set B
having a bijection M : B B
such that
M E = id
S
. (I call this bijection M from the first letter of the word “move” which signifies the
move from the old set B to a ne w set B
).
4 Generalization situatio n
Now to the formalis tic: I will call a generalization situation sets S and B together with an injection
E from S to B. I will call, given a generaliza tion situation, an arbitrary generalization a set B
and a bijection M : B B
such that M E = id
S
.
For every generalization situation I will de note R = im E.
Propositio n 2. For every arbitrary generalization:
1. S B
.
2. E is a bijection from S to R.
3. E = M
1
|
S
.
Proof.
1. S = im(id
S
) = im(M E) im M = B
.
2. Obvious.
3. M E = id
S
M
1
M E = M
1
id
S
E = M
1
|
S
.
Assuming axiom of foundation (one of the axioms of ZF, also known as axiom of regul arity) I will
prove that an arbitrary generalization always exist for every generalization situation. Specifically
I will prove that ZF generalization (see below) is an arbitra ry generalizatio n.
In absence of the axiom of foundation one could reasonably assert existence of a bijection M:
B B
such that M E = id
S
as an axiom. (Let’s call it the axiom of generalization.) This axiom
does not contradict to ZF because it is a conse quence of the axiom o f foundation.
5 ZF generalization
Let S and B are sets. Let E is an injection from S to B. (So we have a generalization situation.)
Let R = im E.
2 Section 5
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
Ex = x.
I will call the above defined B
and M the Z F 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 prope rties 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 le Generalization.thy contains (among other) three locales:
generalization_situation describing generaliza tion s ituations;
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 theo ry int_obj_ex. In this the ory I define the s e t int_obj
which is a set of integers considered as a generalization of the set nat of natural number s. 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 co nsider other possible conventions.)
Isabelle/ZF code 3
7 Future directions
There are advantages and disadvantages of both untyped (such as Isabelle/ZF) and strongly typed
(such as Isabelle/HOL) logical systems.
In this work I have shown that in untyped sy ste ms can be mastered the notion of generalization.
I think that we should invent something having advantages of both untyped and typed systems.
We need a good idea how to crossbr ed different type systems to provide common advantages.
Defining generalization in ZF seems being a s tep in this direction.
As a smaller challenge we also should polish my implementation and usage of generalizations
in Isabelle/ZF bec ause my implementation is not ideal.
4 Section 7