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 [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.
The terminology and notation used in this paper have been
introduced in the following articles
[20]
[19]
[15]
[22]
[23]
[13]
[14]
[16]
[21]
[4]
[2]
[3]
[6]
[1]
[5]
[17]
[7]
[9]
[12]
[18]
[8]
[11]
[10]
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.
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.
Received August 13, 1990
[
Download a postscript version,
MML identifier index,
Mizar home page]