background image

Generalization 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 numbers 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/index.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 notion 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 notion of generalization.

In Isabelle proof assistant (both Isabelle/ZF and Isabelle/HOL) currently different sets are

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

. The only connection between these

provided is the function

inf_of

which transforms a natural number into the corresponding integer.

Also as an effect of this, operations (such as additions) are defined differently and independently
for naturals and integers.

. This document has been written using the GNU TEX

MACS

text editor (see

www.texmacs.org

).

1