On Wed, May 13, 2009 10:27 pm, Michael Kohlhase wrote: > > > On 14.05.2009 0:03 Uhr, Professor James Davenport wrote: >> On Wed, May 13, 2009 12:39 am, Michael Kohlhase wrote: >> One can even have formalised reasons inside a CD - see logic3 for this. >> > Ah, I was unaware of logic3, I will have to have a look at that. And of > course, this corresponds very much to what we are using in OMDoc as > "proof terms" via the Curry/Howard Isomorphism (CHI). And indeed using > the CHI, one could interpret the equations as Proof terms (embedded > into) mathematical discourse in general. As I said, I will have to think > about an example here. Please do - logic3 was intended as the start of a debate here.
>>> Now, this already points to a problem in OpenMath, we can _informally_ >>> say this in a CMP, but not formally in a FMP, since OM does not have a >>> concept of sequence variables (or meta-level elision) that can be >>> quantified over. >>> >> We've had this problem before, and maybe the time is coming to have this >> debate more formally, maybe in a business session/panel at OM2009? >> > I am not sure that the business section would be the right spot, but I > think we may have to make a panel for open issues, which this certainly Whatever. > is. Given that I have been thinking about the "semantics of OpenMath", > we also have to talk about the "linguistics of OpenMath", I think. It > seems to me that formulae in mathematical texts are used and have a > meaning on two levels (which is something we see in linguistics): > > 1. the "compositional" level (I do not have a good word for this, so > I will try this). Here we have the formulae as interpreted > objects, where we cannot look into them (therefore the word > compositional, since there the meaning of a complex object is only > determined by the meanings of the operator and arguments). The > compositional meaning of 2+3 _is_ 5 (as an indivisible > mathematical object). But many OM-processors do not have this level of interpretation (typesetters, data bases etc.). > 2. the "representational" level, where an object is just a formula > (tree) i.e. (almost) an OpenMath Object. Here we can talk about > subterms (and names of bound variables in fact). This level is > also used in Math, we can point to subformulae (that are > inaccesible at the compositional level): e.g. in "... note that > the second argument of the left hand side of the equation above is > not in standard form, so..." > > I think that in a "discourse theory of mathematics" (as I am attempting > to make in OMDoc) this is an important thing to understand. And I think > that it may be important for OM as well. > > OK, I hope you are not too bored at my attempts of philosophy. Not at all, but isn't level 1 what we have been calling "evaluation" (perhaps better expressed, though). James Davenport Visiting Full Professor, University of Waterloo Otherwise: Hebron & Medlock Professor of Information Technology and Chairman, Powerful Computing WP, University of Bath OpenMath Content Dictionary Editor and Programme Chair, OpenMath 2009 IMU Committee on Electronic Information and Communication _______________________________________________ Om mailing list [email protected] http://openmath.org/mailman/listinfo/om
