[Om3] On 'restricting bound variables' in Basic OpenMath
C.A.Rowley at open.ac.uk
Mon Nov 3 16:34:02 CET 2008
Sorry, I was unclear. My point is:
what is a 'condition element', expressed at the level of Basic OpenMath,
which as I wrote, appears to have no notion of membership or
More formally, we need complete information about the content for
<OMC>: is it any valid OpenMath expression? Thanks!
I cannot argue with you on the normally accepted meaning of 'type' or
'guard' in logic/computing.
My problem is that the 'number of variables' seems to be irrelevant to
a mathematician. Two Reals is just one element of R^2 so a single
bound variable will do fine, as in:
$\forall p [ \pi_1(p) - \pi_2(p) \ne 0 ] 1/( \pi_1(p) - \pi_2(p) ) \ne 0$
Are we happy that this has the same mathematical meaning?
Can I then add a 'logical type' to the variable p to express that it
is in this subset of R^2?
These are genuine questions about the normal use of these terms.
More information about the Om3