Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

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

- 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 [10]) 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.

Contents (PDF format)

- [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.
Zermelo theorem and axiom of choice.
*Journal of Formalized Mathematics*, 1, 1989. - [7]
Grzegorz Bancerek.
Curried and uncurried functions.
*Journal of Formalized Mathematics*, 2, 1990. - [8]
Grzegorz Bancerek.
Increasing and continuous ordinal sequences.
*Journal of Formalized Mathematics*, 2, 1990. - [9]
Grzegorz Bancerek.
Ordinal arithmetics.
*Journal of Formalized Mathematics*, 2, 1990. - [10]
Grzegorz Bancerek.
The reflection theorem.
*Journal of Formalized Mathematics*, 2, 1990. - [11]
Grzegorz Bancerek.
Replacing of variables in formulas of ZF theory.
*Journal of Formalized Mathematics*, 2, 1990. - [12]
Grzegorz Bancerek.
Tarski's classes and ranks.
*Journal of Formalized Mathematics*, 2, 1990. - [13]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [14]
Czeslaw Bylinski.
Functions from a set to a set.
*Journal of Formalized Mathematics*, 1, 1989. - [15]
Czeslaw Bylinski.
Some basic properties of sets.
*Journal of Formalized Mathematics*, 1, 1989. - [16]
Agata Darmochwal.
Finite sets.
*Journal of Formalized Mathematics*, 1, 1989. - [17]
Andrzej Nedzusiak.
$\sigma$-fields and probability.
*Journal of Formalized Mathematics*, 1, 1989. - [18]
Bogdan Nowak and Grzegorz Bancerek.
Universal classes.
*Journal of Formalized Mathematics*, 2, 1990. - [19]
Andrzej Trybulec.
Enumerated sets.
*Journal of Formalized Mathematics*, 1, 1989. - [20]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [21]
Andrzej Trybulec.
Subsets of real numbers.
*Journal of Formalized Mathematics*, Addenda, 2003. - [22]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989. - [23]
Edmund Woronowicz.
Relations and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989.

[ Download a postscript version, MML identifier index, Mizar home page]