[Om] Multistep "equation" symbol?

[Professor James Davenport]

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