The Reflection Theorem

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

The Reflection Theorem

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

Summary.

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.

MML Identifier: ZF_REFLE

The terminology and notation used in this paper have been introduced in the following articles [15] [14] [17] [16] [18] [9] [10] [3] [4] [5] [1] [12] [8] [13] [2] [6] [7]

Contents (PDF format)