[Om] Multistep "equation" symbol?

[Professor James Davenport]

On Mon, May 11, 2009 10:22 pm, Lars Hellström wrote:
>> The reason I say that is what you have is really a (part of) a proof
>> here,
>> especially when one looks at the annotations.
>
> Indeed, or at least the skeleton of (part of) a proof. In my case the
> annotations would mainly specify which identity is applied and where
> (which is not at all obvious -- especially for derivations that employ
> previously derived rules).
>
>>>   * There are several steps in this thing, yet it constitutes
>>>     a natural unit (in whatever document it is part of).
>> Quite. It is a 'proof' and could be a free-standing Lemma. One might not
>> wish to do so for expositional reasons, but a proof ought to be capable
>> of being a chain of sub-proofs.
>>>   * Not all steps employ the same relation.
>> True, but, and this is the hard part to formalise, they must be
>> "logically compatible".
> Well, I don't see much point in formalising that; it must in the end be
> up to the party who constructs this kind of proof to draw some logical
> conclusion from it. Attempts to construct a syntactic description of
> the cases where this is possible are likely to be futile.
Which is one reason I didn't like the syntactic n-ary relation.
But one wishes such a chain to be such that a "sufficiently clever"
verifier could verify it, and one probably wants some subset of such
prrofs to be verifiable by pretty simple verifiers.

>>> PS: While typing up the example, I noticed that it probably wouldn't be
>>> correct since limit1#tendsto (MathML3-ish?) is defined to be ternary,
>>> requesting a type-of-limit as first argument. While I suppose one could
>>> use a lambda to work around that, I can't help wondering why the limit
>>> type is an argument in the first place; wouldn't an attribution be more
>>> appropriate?
>> I expect because of the 'optionality' of attributes, at least in OM1.
>
> Aha!
Having said which, it would be better to define a symbol rather than keep
generating such lambda-expressions, if this applicatin were to go that
way.

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