[om] Bug in definition of `strict_order'
Professor James Davenport
jhd at cs.bath.ac.uk
Mon Jul 14 17:46:55 CEST 2003
On Wed, 9 Jul 2003, Scott L. Burson wrote:
> I just now learned about OpenMath as I was using Google to look for some
> definitions.
Thanks
> 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
I can't find antireflexive, but there is antisymmetric, which does indeed
have the definition you quote below, which I think is correct for
antisymmetric.
> 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
I don't quite follow this point. I do agree that the definition is over
the top, as irreflexive and transitive imply anisymmetric, but I don't
think it's wrong as such.
> such that `R(x, y) & R(y, x)'. 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.
James Davenport
OpenMath CD Editor
--
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
More information about the Om
mailing list