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 classiﬁcation: 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 deﬁne 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 diﬀer ent sets a re
deﬁned 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 eﬀect of this, ope rations (such as additions) are deﬁned diﬀerently 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