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

[Professor James Davenport]

On Mon, 3 Nov 2008, Chris Rowley wrote:
> 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 think Michael is expecting it to be a Boolean-valued expression in the 
lose sense: since OM is not a CA system, we can't ask much more. 
> 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
I disagree. It is irrelevant IN PRINCIPLE, but in practice (and if we want 
to be reasonably close to "the mathematical vernacular") it does matter.
> 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.
Yes - important ones. Note that, as is implicit in what Chris wrote, no 
conditions are NECESSARY: the question is whether they are useful.
James