[Om] Multistep "equation" symbol?

[Lars Hellström]

Michael Kohlhase skrev:
> 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).
>   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..."

That aligns fairly well with the distinction between Model and Theory 
in mathematical logic, does it not? E.g. in Theory you cannot apply 
Modus Ponens to A and A=>B to derive B unless the two A's are 
representationally the same, whereas in a Model you can only consider 
the truth values of formulae (w.r.t. a given assignment of values to 
the free variables) so any representation equivalent to A will do.

> OK, I hope you are not too bored at my attempts of philosophy.

Mathematical logic is on the border towards philosophy, so I think any 
complete discussion of these issues must consider also philosophical 
aspects.

Lars Hellström