PS: a question about <forall> element

Hi,

I just realized that there is yet another problem with this definition:

>>
>>  "The forall element represents the universal quantifier of logic. It
>>  must be used in conjunction with one or more bound variables, an
>>  optional condition element, and an assertion, which should take the
>>  form of an apply element. In MathML 1.0, the reln element was also
>>  permitted here: this usage is now deprecated."
>>
>> And from the validation grammer, C.2.3.18:
>>
>>  "Signature
>>    (bvar*,condition?,apply) -> boolean    (bvar*,condition?,(reln)) 
>> -> boolean "
>
Like the integration operator, which is used in examples in the MathML 
document either as binding its own variables or as operating on 
functions, and which can therefore be used both with and without bvar 
qualifiers, it is (perhaps surprisingly) quite common to do something 
similar with the standard quantifiers, especially in linguistics/formal 
semantics texts.  It is quite common there to use

<apply>
  <forall/>
  <lambda> <bvar> <ci>x</ci> </bvar>
    ...
  </lambda>
</apply>

that is to interpret forall as an operator acting on predicates.  This 
usage would be forbidden by the current definition.

I believe I suggested years ago that the equivalence of variable binding 
operators and their interpretation as operators acting on functions (or 
in this case, predicates) be respected by MathML, and was told that that 
was a good idea and MathML would do so, as indeed it has in the case of 
<int/>.

Please use int as a precedent and state in very general terms that an 
apply with bvar qualifiers can always be re-phrased as an apply with a 
single lambda term argument in this manner, and that therefore there are 
no operators in the language that require bvar qualifiers.

Thanks,

 -- Andreas

Received on Wednesday, 7 May 2003 04:06:15 UTC