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

## Consequences of the Reflection Theorem

Grzegorz Bancerek
Warsaw University, Bialystok
Supported by RPBP.III-24.C1.

### Summary.

Some consequences of the reflection theorem are discussed. To formulate them the notions of elementary equivalence and subsystems, and of models for a set of formulae are introduced. Besides, the concept of cofinality of a ordinal number with second one is used. The consequences of the reflection theorem (it is sometimes called the Scott-Scarpellini lemma) are: (i) If $A_\xi$ is a transfinite sequence as in the reflection theorem (see ) and $A = \bigcup_{\xi \in On} A_\xi$, then there is an increasing and continuous mapping $\phi$ from $On$ into $On$ such that for every critical number $\kappa$ the set $A_\kappa$ is an elementary subsystem of $A$ ($A_\kappa \prec A$). (ii) There is an increasing continuous mapping $\phi: On \to On$ such that ${\bf R}_\kappa \prec V$ for each of its critical numbers $\kappa$ ($V$ is the universal class and $On$ is the class of all ordinals belonging to $V$). (iii) There are ordinal numbers $\alpha$ cofinal with $\omega$ for which ${\bf R}_\alpha$ are models of ZF set theory. (iv) For each set $X$ from universe $V$ there is a model of ZF $M$ which belongs to $V$ and has $X$ as an element.

#### MML Identifier: ZFREFLE1

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. Zermelo theorem and axiom of choice. Journal of Formalized Mathematics, 1, 1989.
 Grzegorz Bancerek. Curried and uncurried functions. Journal of Formalized Mathematics, 2, 1990.
 Grzegorz Bancerek. Increasing and continuous ordinal sequences. Journal of Formalized Mathematics, 2, 1990.
 Grzegorz Bancerek. Ordinal arithmetics. Journal of Formalized Mathematics, 2, 1990.
 Grzegorz Bancerek. The reflection theorem. Journal of Formalized Mathematics, 2, 1990.
 Grzegorz Bancerek. Replacing of variables in formulas of ZF theory. Journal of Formalized Mathematics, 2, 1990.
 Grzegorz Bancerek. Tarski's classes and ranks. 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 Nedzusiak. $\sigma$-fields and probability. Journal of Formalized Mathematics, 1, 1989.
 Bogdan Nowak and Grzegorz Bancerek. Universal classes. Journal of Formalized Mathematics, 2, 1990.
 Andrzej Trybulec. Enumerated sets. Journal of Formalized Mathematics, 1, 1989.
 Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
 Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
 Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
 Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.