[Om3] Symbol Definitions in the Description elements

[Professor James Davenport]

On Mon, September 29, 2008 12:09 am, Chris Rowley wrote:
> Professor James Davenport wrote --
>> > Thus I would allow multiple definitions but insist that they are
>> > compatible.
>> A plausible point of view. It makes the concept of non-cyclicity
>> non-deterministic, since it might depend which definitions one used: I
>> would wish to insist on NEVER CYCLIC.
>
> Agreed.  With 'proof'?
With as much of a 'proof' as can be provided, i.e. the proofs are
dependent on the actual definitions (as opposed to merely the semantics)
of all the objects involved.
>
>> > Moving on, one could usefully insist on a _mathematical_ proof of all
>> > of such things: compatibility, non-cyclicity, finiteness etc.  Or not!
>> Non-cyclicity is a feature of the entire graph of CDs, and therefore
>> subject to change, whereas consistency of definitions in a CD is a fact
>> of
>> that CD (assuming that the SEMANTICS, as opposed to the way they are
>> expressed, of objects depended on does not change, and this is illegal).
>
> Not sure that I agree here.  Non-cyclicity for one CD is surely only a
> property of the 'dependency subgraph generated by the contents of that
> CD', not the entire dependency graph of CDs.  And the former is
> exactly the subgraph whose nodes need to be studied (in greater
> detail) when checking consistency.
Not quite, would be my view. If I am (a theorem-prover) interested in
checking consistency, then I can stop when I reach a node I 'understand'
[of course, if I 'understand' it incorrectly, all bets are off, but that's
OM for you], whereas another theorem-prover might have to descend.

So, if I have two different definitions (DeFMPs) of aardvarks in terms of
wombats, and my theorem prover understands wombats, then these two
definitions are all that the ThP needs to look at. If in addition, we have
a definition (DefMP) of aardvarks in terms of mobats, and FMPs defining
moBats in terms of wombats, our ThP is happy.

If I have a ThP that understands mobats but not wombats, it does not know
that these are consistent. I can make it happy by adding (the right)
definitions of wombats in terms of mobats. both ThP are happy, but with
different traversals of the graph.

BUT, if I make the wonbat=>mobat and mobat=>wombat into DefMP, both ThP
are still happy (since a DefMP is no more than a FMP as far as a strict
ThP is concerned), but I have now introduced circularity, and a ThP that
understand neither wombats nor mobats would go in a loop.

James Davenport
Hebron & Medlock Professor of Information Technology
Formerly RAE Coordinator and Undergraduate Director of Studies, CS Dept
Lecturer on CM30070, 30078, 50209, 50123, 50199
Chairman, Powerful Computing WP, University of Bath
OpenMath Content Dictionary Editor
IMU Committee on Electronic Information and Communication