major problem with diff:replacement

There is a major difference between the entailment relation a expressed 
by the => sign in cwm and the diff:replacement, which I think indicates 
a big conceptual difference between these two methods.

In any theory you can consistently have any number of entailment 
relations with the same antecedent.

So
	The cat is on the mat => the mat is under the cat
	The cat is on the mat => the cat is happy

could be consistently held to be true.
On the other hand:

	The cat is on the mat
	{The cat is on the mat} diff:replace { The cat is on the table }
	{The cat is on the mat} diff:replace { The cat is on grass }

Assuming we have somehow limited ourselves to describing the same point 
in time, the above cannot be consistently held. One has to make a 
choice, between the diff replacements holds. A cat cannot be at two 
places at once. Yet each one of the two statements by itself is a valid 
application of the diff:replace relation.

I think part of the reason for this is that implication is a relation 
within first order logic, whereas diff:replace is a relation between 
theories.  Implication preserves truth conditions, whereas diff:replace 
changes them. diff:replace is a mapping between theories. It says: the 
second theory can be reached by changing the first theory in this way. 
As an image I think the following will help (if file attachments are 
allowed on this list)



This represents a file containing two diff:replace statements, 
concerning the same objects. Each diff replacement maps to a different 
and incompatible theory.

Before continuing let me check that this mailing list accepts image 
attachments.

Henry