Mostowski's Fundamental Operations --- Part II

Grzegorz Bancerek

Warsaw University, Bialystok

Andrzej Kondracki

Warsaw University

Summary.

The article consists of two parts. The first part is translation of chapter II.3 of [13]. A section of $D_{H}(a)$ determined by $f$ (symbolically $S_{H}(a,f)$) and a notion of predicative closure of a class are defined. It is proved that if following assumptions are satisfied: (o) $A=\bigcup_{\xi}A_{\xi}$, (i) $A_{\xi} \subset A_{\eta}$ for $\xi < \eta$, (ii) $A_{\lambda}=\bigcup_{\xi<\lambda}A_{\lambda}$ ($\lambda$ is a limit number), (iii) $A_{\xi}\in A$, (iv) $A_{\xi}$ is transitive, (v) $(x,y\in A) \rightarrow (x\cap y\in A)$, (vi) $A$ is predicatively closed, then the axiom of power sets and the axiom of substitution are valid in $A$. The second part is continuation of [12]. It is proved that if a non-void, transitive class is closed with respect to the operations $A_{1}-A_{7}$ then it is predicatively closed. At last sufficient criteria for a class to be a model of ZF-theory are formulated: if $A_{\xi}$ satisfies o - iv and $A$ is closed under the operations $A_{1}-A_{7}$ then $A$ is a model of ZF.

MML Identifier: ZF_FUND2

Contents (PDF format)

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek. A model of ZF set theory language. Journal of Formalized Mathematics, 1, 1989.

[3] Grzegorz Bancerek. Models and satisfiability. Journal of Formalized Mathematics, 1, 1989.

[4] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.

[5] Grzegorz Bancerek. Sequences of ordinal numbers. Journal of Formalized Mathematics, 1, 1989.

[6] Grzegorz Bancerek. Increasing and continuous ordinal sequences. Journal of Formalized Mathematics, 2, 1990.

[7] Grzegorz Bancerek. The reflection theorem. Journal of Formalized Mathematics, 2, 1990.

[8] Grzegorz Bancerek. Replacing of variables in formulas of ZF theory. Journal of Formalized Mathematics, 2, 1990.

[9] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[10] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[11] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.

[12] Andrzej Kondracki. Mostowski's fundamental operations --- part I. Journal of Formalized Mathematics, 2, 1990.

[13] Andrzej Mostowski. \em Constructible Sets with Applications. North Holland, 1969.

[14] Andrzej Nedzusiak. $\sigma$-fields and probability. Journal of Formalized Mathematics, 1, 1989.

[15] Bogdan Nowak and Grzegorz Bancerek. Universal classes. Journal of Formalized Mathematics, 2, 1990.

[16] Andrzej Trybulec. Enumerated sets. Journal of Formalized Mathematics, 1, 1989.

[17] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[18] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[19] Andrzej Trybulec and Agata Darmochwal. Boolean domains. Journal of Formalized Mathematics, 1, 1989.

[20] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[21] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.