Mostowski's Fundamental Operations --- Part I

Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

Mostowski's Fundamental Operations --- Part I

Andrzej Kondracki: Warsaw University

Summary.

In the chapter II.4 of his book [11] A.~Mostowski introduces what he calls fundamental operations:\\ \indent $A_{1}(a,b)=\lbrace\lbrace\langle0,x\rangle,\langle1,y\rangle\rbrace: x\in y \wedge x\in a \wedge y\in a \rbrace$,\\ \indent $A_{2}(a,b)=\lbrace a,b\rbrace$,\\ \indent $A_{3}(a,b)=\bigcup a$,\\ \indent $A_{4}(a,b)=\lbrace\lbrace\langle x,y\rangle\rbrace: x\in a \wedge y\in b \rbrace$,\\ \indent $A_{5}(a,b)=\lbrace x\cup y : x\in a \wedge y\in b \rbrace$,\\ \indent $A_{6}(a,b)=\lbrace x\setminus y : x\in a \wedge y\in b \rbrace$,\\ \indent $A_{7}(a,b)=\lbrace x\circ y : x\in a \wedge y\in b \rbrace$.\\ He proves that if a non-void class is closed under these operations then it is predicatively closed. Then he formulates sufficient criteria for a class to be a model of ZF set theory (theorem 4.12). \par The article includes the translation of this part of Mostowski's book. The fundamental operations are defined (to be precise not these operations, but the notions of closure of a class with respect to them). Some properties of classes closed under these operations are proved. At last it is proved that if a non-void class $X$ is closed with respect to the operations $A_{1}-A_{7}$ then $D_{H}(a)\in X$ for every $a$ in $X$ and every $H$ being formula of ZF language ($D_{H}(a)$ consists of all finite sequences with terms belonging to $a$ which satisfy $H$ in $a$).

MML Identifier: ZF_FUND1

The terminology and notation used in this paper have been introduced in the following articles [13] [9] [15] [4] [5] [6] [1] [10] [16] [12] [2] [3] [7] [8] [14]

Contents (PDF format)