[om] Bug in definition of `strict_order'

[Olga Caprotti]

Hi Scott.


Scott L. Burson wrote:
> Hi,
> 
> I just now learned about OpenMath as I was using Google to look for some
> definitions.
> 
> I seem to have found a bug in the definition of `strict_order', or more
> precisely, in that of `antireflexive' on which it depends.  A strict order
> is irreflexive, meaning `forall(x) ~R(x, x)'.  The current definition of
> `antireflexive', however, says
> 
>    forall(x, y) R(x, y) -> R(y, x) -> x = y
> 
> But this definition does not work as part of the definition of
> `strict_order', because by irreflexivity and transitivity, there are no x, y
> such that `R(x, y) & R(y, x)'.  

Yes, this is what the definition of strict order implies and it is the 
goal of the definition to make sure that an order relation R is such 
that if Rxy then ~Ryx, like < (less than).

-olga


It could be written instead as something
> like
> 
>    forall(x, y) (R(x, y) = R(y, x)) -> x = y
> 
> and then it would work for both reflexive and irreflexive relations.
> 




> Please CC: me in replies as I am not on the mailing list.
> 
> -- Scott
> --
> om at openmath.org  -  general discussion on OpenMath
> Post public announcements to om-announce at openmath.org
> Automatic list maintenance software at majordomo at openmath.org
> Mail om-owner at openmath.org for assistance with any problems
> 
> 
--
om at openmath.org  -  general discussion on OpenMath
Post public announcements to om-announce at openmath.org
Automatic list maintenance software at majordomo at openmath.org
Mail om-owner at openmath.org for assistance with any problems