Strong Arithmetic of Real Numbers

Andrzej Trybulec

Warsaw University, Bialystok

Supported by RPBP.III-24.B1.

Summary.

This abstract contains the second part of the axiomatics of the Mizar system (the first part is in abstract [4]). The axioms listed here characterize the Mizar built-in concepts that are automatically attached to every Mizar article. We give definitional axioms of the following concepts: element, subset, Cartesian product, domain (non empty subset), subdomain (non empty subset of a domain), set domain (domain consisting of sets). Axioms of strong arithmetics of real numbers are also included.

MML Identifier: AXIOMS

Contents (PDF format)

Bibliography

[1] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek. Sequences of ordinal numbers. Journal of Formalized Mathematics, 1, 1989.

[3] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.

[4] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[5] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[6] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.