Über diesen Artikel
Online veröffentlicht: 20. Juli 2019
Seitenbereich: 139 - 152
Akzeptiert: 27. Mai 2019
DOI: https://doi.org/10.2478/forma-2019-0015
Schlüsselwörter
© 2019 Sebastian Koch, published by Sciendo
This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.
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.