James
Good morning! Everyone, This message starts from our sparring and moves towards supporting the K&D extension to OM3 ... But maybe not sharing their reasoning! Presumably this restores normality by putting me at odds with David C again:-). On the way it expresses some concerns about universally parametrised expressions and their expressivity for 'mathematics as we (or I) know it'. chris >>> On Mon, March 23, 2009 12:07 am, [email protected] wrote: > > > Well spotted, James: but you are making an (entirely reasonable) > assumption > about the measure. > > Add |cos z| = 1 to the domain if you wish but then you will complain that > it is (assuming z is a 'real variable', of course). Which I did since $z<0$. I (subconsciously) played Axiom in my head and looked for an ordered set with a cos functions. >>> ... maybe not you, but I would have started from the assumtion that z --> 'complex variable' until, as you found, that becomes untenable and starting to 'calculate the universal element in some subcategory'. The moral (or executive summary) being that this is exactly how many mathematical formulas communicate their meaning: both by using assumptions about deductions that the reader will make and/or by (more or less implicitly) pointing out that the assumptions may be wrong. This shows both the communicative (to humans) power of such very abbreviated maths notations and the fact that much of it works only with humans who make exactly the correct deductions about unstated assumptions (particularly about 'variables'). The question is whether the 'mathematical semantics' can be said to be captured without making explicit certain features that are often, but not always, absent or very much implicit in the notation typically used. They probably can in the computational and logical sense of semantics but is this level of expressivity: -- all that OM3 is trying to achieve? -- sufficient for the 'semanticly rich encoding of mathematical material' For example, when encoding useful, concrete 'mathematical semantics' in the 21C, is the concept of an: expression in a 'universal' or 'unconditional' bound variable sufficient to encode 'a function' or only a 'template for a collection of functions'? Further if it is the only the latter, what has this got to do with concrete mathematics as she is done and taught by many mathematicians? Thus it is the (apparently or actually) 'unconditioned variables' that worry me: they are great for symbolic logic but that is not much of 'mathematics as we know it'. Even 19C (and probably 17-18C) 'variables' were not 'universal' but are (possibly by assumption) 'real' or 'complex' variables or integers (or often more concretely 'quantities'). As soon as the variables get conditioned then one gets some idea of the 'domain over which they range': something that is essential if they are in fact being used to 'describe a function'. And in anything I would describe as 'every day mathematics' such function-like things, with definite domains available when needed, are (and have been at least since Cauchy) fundamental and omni-present. Hence I want all 'bindings' in OM to require a 'condition on the bound variables'. Syntactically this can, perhaps, be omitted but with an assumed default value. Manifesto: a pure, context-free lambda-expression neither describes a mathematical function nor expresses any 'mathematical semantics'. --------------------------------------------------------------------------- The Open University is incorporated by Royal Charter (RC 000391), an exempt charity in England & Wales and a charity registered in Scotland (SC 038302) _______________________________________________ Om3 mailing list [email protected] http://openmath.org/mailman/listinfo/om3
