Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users

Mahlo and Inaccessible Cardinals


Josef Urban
Charles University, Praha

Summary.

This article contains basic ordinal topology: closed unbounded and stationary sets and necessary theorems about them, completness of the centered system of Clubs of $M$, Mahlo and strongly Mahlo cardinals, the proof that (strongly) Mahlo is (strongly) inaccessible, and the proof that Rank of strongly inaccessible is a model of ZF.

MML Identifier: CARD_LAR

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

Contents (PDF format)

  1. Clubs and Mahlo Cardinals
  2. Proof that Strongly Inaccessible is Model of ZF

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek. Models and satisfiability. Journal of Formalized Mathematics, 1, 1989.
[3] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[4] Grzegorz Bancerek. Sequences of ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[5] Grzegorz Bancerek. Countable sets and Hessenberg's theorem. Journal of Formalized Mathematics, 2, 1990.
[6] Grzegorz Bancerek. K\"onig's theorem. Journal of Formalized Mathematics, 2, 1990.
[7] Grzegorz Bancerek. Tarski's classes and ranks. Journal of Formalized Mathematics, 2, 1990.
[8] Grzegorz Bancerek. On powers of cardinals. Journal of Formalized Mathematics, 4, 1992.
[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] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[12] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.
[13] Bogdan Nowak and Grzegorz Bancerek. Universal classes. Journal of Formalized Mathematics, 2, 1990.
[14] Beata Padlewska. Families of 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] Josef Urban. Basic facts about inaccessible and measurable cardinals. Journal of Formalized Mathematics, 12, 2000.
[19] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

Received August 28, 2000

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