- From: Andreas Strotmann <Strotmann@rrz.uni-koeln.de>
- Date: Wed, 07 May 2003 10:06:01 +0200
- To: Andreas Strotmann <Strotmann@rrz.uni-koeln.de>
- CC: Robert Miner <RobertM@dessci.com>, www-math@w3.org

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