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

[Chris Rowley]

At present in OpenMath, binding seems to me to be doing nothing more than
defining exactly which (and when) so-called '\alpha-substitutions'
'preserve the semantics of an OpenMath object'.

Michael's idea of adding 'condition' at a basic level relates more
closely to typing rather than to this pure concept of binding.

Adding Michael's idea to binding seems therefore to be inappropriate.
But I am not sure that I have seen a precise definition of what his
suggested addition would be, so I may have misunderstood.

More generally, there is a more major problem with adding anything
like conditions to Basic OpenMath: that this would require the
introduction of a Basic OpenMath Object of type 'set membership' or,
equivalently (I think:-), 'Boolean', which could be called 'bit'.

Thus, if anything needs to be added to basic OpenMath then I would
suggest that some Basic Object to represent the primal concept of
duality is a prime candidate.  This fits with my thoughts on looking
at the sets CD too: something there should be introduced at a more
fundamental level.

One could argue that a Basic Object such as 'integers' imply that 'a
total order relation' and hence 'membership in a set of size 2' is
also a Basic Object but there is no harm in making this more
fundamental idea explicit.  Also, it is not entirely clear whether the
phrase 'integers in the mathematical sense' implies that the standard
order relation is also Basic.