Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

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

- The goal is show that the reflection theorem holds. The theorem is as usual in the Morse-Kelley theory of classes (MK). That theory works with universal class which consists of all sets and every class is a subclass of it. In this paper (and in another Mizar articles) we work in Tarski-Grothendieck (TG) theory (see [15]) which ensures the existence of sets that have properties like universal class (i.e. this theory is stronger than MK). The sets are introduced in [13] and some concepts of MK are modeled. The concepts are: the class $On$ of all ordinal numbers belonging to the universe, subclasses, transfinite sequences of non-empty elements of universe, etc. The reflection theorem states that if $A_\xi$ is an increasing and continuous transfinite sequence of non-empty sets and class $A = \bigcup_{\xi \in On} A_\xi$, then for every formula $H$ there is a strictly increasing continuous mapping $F: On \to On$ such that if $\varkappa$ is a critical number of $F$ (i.e. $F(\varkappa) = \varkappa > 0$) and $f \in A_\varkappa^{\bf VAR}$, then $A,f\models H \equiv\ {A_\varkappa},f\models H$. The proof is based on [11]. Besides, in the article it is shown that every universal class is a model of ZF set theory if $\omega$ (the first infinite ordinal number) belongs to it. Some propositions concerning ordinal numbers and sequences of them are also present.

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.
Increasing and continuous ordinal sequences.
*Journal of Formalized Mathematics*, 2, 1990. - [7]
Grzegorz Bancerek.
Replacing of variables in formulas of ZF theory.
*Journal of Formalized Mathematics*, 2, 1990. - [8]
Grzegorz Bancerek.
Tarski's classes and ranks.
*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] Andrzej Mostowski. \em Constructible Sets with Applications. North Holland, 1969.
- [12]
Andrzej Nedzusiak.
$\sigma$-fields and probability.
*Journal of Formalized Mathematics*, 1, 1989. - [13]
Bogdan Nowak and Grzegorz Bancerek.
Universal classes.
*Journal of Formalized Mathematics*, 2, 1990. - [14]
Andrzej Trybulec.
Enumerated sets.
*Journal of Formalized Mathematics*, 1, 1989. - [15]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [16]
Andrzej Trybulec.
Subsets of real numbers.
*Journal of Formalized Mathematics*, Addenda, 2003. - [17]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989. - [18]
Edmund Woronowicz.
Relations and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989.

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