Natural Addition of Ordinals

Sebastian Koch

doi:10.2478/forma-2019-0015

.blurhash-client-img { display: none !important; }

Natural Addition of Ordinals

Formalized Mathematics

Volume 27 (2019): Issue 2 (July 2019)

By: Sebastian Koch

Open Access

|Jul 2019

Abstract

In [3] the existence of the Cantor normal form of ordinals was proven in the Mizar system [6]. In this article its uniqueness is proven and then used to formalize the natural sum of ordinals.

References

[1] Alexander Abian. The theory of sets and transfinite arithmetic. Saunders mathematics books. Saunders, Philadelphia [u.a.], 1965.
Search in Google Scholar Back to article
[2] Heinz Bachmann. Transfinite Zahlen. Ergebnisse der Mathematik und ihrer Grenzgebiete, (1). Springer, Berlin [u.a.], 2., neubearb. aufl. edition, 1967.
Search in Google Scholar Back to article
[3] Grzegorz Bancerek. Epsilon numbers and Cantor normal form. Formalized Mathematics, 17(4):249–256, 2009. doi:10.2478/v10037-009-0032-8.10.2478/v10037-009-0032-8
Open DOI Search in Google Scholar Back to article
[4] Georg Cantor. Beiträge zur begründung der transfiniten mengenlehre. Mathematische Annalen, 49(2):207–246, 1897.10.1007/BF01444205
Search in Google Scholar Back to article
[5] Oliver Deiser. Einführung in die Mengenlehre: die Mengenlehre Georg Cantors und ihre Axiomatisierung durch Ernst Zermelo. Springer, Berlin [u.a.], 2., verb. und erw. aufl. edition, 2004. ISBN 3-540-20401-6.
Search in Google Scholar Back to article
[6] Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1.10.1007/s10817-015-9345-1
Open DOI Search in Google Scholar Back to article
[7] Piotr Rudnicki and Andrzej Trybulec. Multivariate polynomials with arbitrary number of variables. Formalized Mathematics, 9(1):95–110, 2001.
Search in Google Scholar Back to article
[8] Wacław Sierpiński. Cardinal and ordinal numbers. Polska Akademia Nauk. Monografie matematyczne, (34) (in Polish). PWN, Warszawa, 2. ed., rev edition, 1965.
Search in Google Scholar Back to article
[9] Tetsuya Tsunetou, Grzegorz Bancerek, and Yatsuka Nakamura. Zero-based finite sequences. Formalized Mathematics, 9(4):825–829, 2001.
Search in Google Scholar Back to article