Ordered Rings - Part I

Michal Muzalewski

Warsaw University, Bialystok

Leslaw W. Szczerba

Siedlce University

Summary.

This series of papers is devoted to the notion of the ordered ring, and one of its most important cases: the notion of ordered field. It follows the results of [5]. The idea of the notion of order in the ring is based on that of positive cone i.e. the set of positive elements. Positive cone has to contain at least squares of all elements, and be closed under sum and product. Therefore the key notions of this theory are that of square, sum of squares, product of squares, etc. and finally elements generated from squares by means of sums and products. Part I contains definitions of all those key notions and inclusions between them.

MML Identifier: O_RING_1

Contents (PDF format)

Bibliography

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.

[3] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[4] Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski. Abelian groups, fields and vector spaces. Journal of Formalized Mathematics, 1, 1989.

[5] Wanda Szmielew. \em From Affine to Euclidean Geometry, volume 27. PWN -- D.Reidel Publ. Co., Warszawa -- Dordrecht, 1983.

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

[7] Wojciech A. Trybulec. Vectors in real linear space. Journal of Formalized Mathematics, 1, 1989.

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