Journal of Formalized Mathematics
Addenda, 1989
University of Bialystok
Copyright (c) 1989
Association of Mizar Users
Strong Arithmetic of Real Numbers

Andrzej Trybulec

Warsaw University, Bialystok

Supported by RPBP.III24.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 builtin 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
The terminology and notation used in this paper have been
introduced in the following articles
[4]
[3]
[6]
[1]
[2]
[5]
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.
Received January 1, 1989
[
Download a postscript version,
MML identifier index,
Mizar home page]