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

Contents (PDF format)

#### Bibliography

 Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.
 Grzegorz Bancerek. A model of ZF set theory language. Journal of Formalized Mathematics, 1, 1989.
 Grzegorz Bancerek. Models and satisfiability. Journal of Formalized Mathematics, 1, 1989.
 Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
 Grzegorz Bancerek. Sequences of ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
 Grzegorz Bancerek. Increasing and continuous ordinal sequences. Journal of Formalized Mathematics, 2, 1990.
 Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
 Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
 Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
 Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.
 Andrzej Mostowski. \em Constructible Sets with Applications. North Holland, 1969.
 Bogdan Nowak and Grzegorz Bancerek. Universal classes. Journal of Formalized Mathematics, 2, 1990.
 Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
 Andrzej Trybulec and Agata Darmochwal. Boolean domains. Journal of Formalized Mathematics, 1, 1989.
 Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
 Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.