[om] forall

[Michael Kohlhase]

Dear Andrew,

I agree that it would be very nice to have a sorted quantifier. Actually
this concept has been floating around in discussions for some time, and
this is central operator in many logical systems. 

One solution in OpenMath I have heard proposed is to use attribuition for
the bound variables, e.g. in 

<OMBIND>
  <OMS cd="quant1" name="forall"/>
  <OMBVAR>
   <OMATTR>
     <OMATP>
       <OMS cd="don't remember" name="type"/>
       <OMS cd="concrete-sets" name="real"/>
     </OMATP>
     <OMV name="X"/>
     ...
</OMBIND> 

this is very well, but there is nothing in the OpenMath standard that says
that the attributes have to be taken into account by the OpenMath
applications. Dropping them would (as you point out) change the
semantics. 

I think that this issue would bear some discussion, now that the OpenMath
Standard has stabilized in other areas. 

     Michael


--
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