Re: Ordered Rings

[Grzegorz Bancerek <bancerek@math.uwb.edu.pl>]

Hello,

On Wed, 3 Nov 1999, Christoph Schwarzweller wrote:

> We are thinking about introducing ordered rings in Mizar.
> The question is how to introduce the order:
> 
>   - extending the structure by an additional field and defining 
>     necessary attributes (reflexivity, ... or whatever) about 
>     this field 

You do not have to define these attributes.  You should define a new
structure prefixed by ring structure (FieldStr) and poset structure
(RelStr) like this

definition
  struct (FieldStr, RelStr) OrderedRingStr
   (#
      carrier -> set,
      mult, add -> BinOp of the carrier,
      unity, Zero -> Element of the carrier,
      InternalRel -> Relation of the carrier, the carrier 
   #)
end;

After that, you will have possibility to use for the new structure the  
terminology already introduced for each prefixing structure, like
"reflexive" and "add-associative".  Theorems already proved for rings and
posets will be also ready to use for the new structure.

> 
> or
> 
>   - by an internal definition without an additional field in 
>     the structure, that is defining the set of positive elements 
>     of a ring and using this set the order.
> 

Anyway, you have to introduce attribute stated whether the InternalRel
field is the relation fulfilling ring order conditions.

Grzegorz Bancerek               e-mail: bancerek@mizar.org 
                                        (bancerek@math.uwb.edu.pl)
Dept. of Applied Logic          http://math.uwb.edu.pl/~bancerek/
Institute of Computer Science   fax. +48 (85) 745-7073
University of Bialystok         tel. +48 (85) 745-7559 (office)
15-267 Bialystok, Poland             +48 (85) 719-1984 (home)