[Om3] On 'restricting bound variables' in Basic OpenMath

[Chris Rowley]

Michael

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
true/false?

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.

Thanks,  chris