[Om] logic1 CD revision?

[David Carlisle]

> 1) doesn't anyone see anything wrong with the FMP for 'equivalent'?  It 
> seems to use a circular definition.

FMP (and CMP) are not necessarily definitional so as long as they are
true it's OK if they are circular, there is no implication that you can
generate some terminating rewrite rules to define the symbol. There have
been various proposals over the years to have some version of FMP that
could be used as a definition (so in particular could be relied on not
to have circular dependencies). The kind attribute was added to FMP in
content dictionaries in OM version 2 to allow FMP to be classified in
variuos ways for this kind of purpose, but at the time no particular
kinds were standardised, and it's not used in the core Cds.

http://www.openmath.org/standard/om20-2004-06-30/omstd20html-4.xml#sect_func

A Formal Mathematical Property may be given an optional
	    kind attribute.  An author of a Content Dictionary
	    may use this to indicate whether, for example, the property provides an
	    algorithm for evaluation of the concept it is associated with.  At
	    present no fixed scheme is mandated for how this information should be
	    encoded or used by an application.

David