[Prev][Next][Index][Thread]

Re: Wand on final algebra semantics


To: meyer@theory.LCS.MIT.EDU
Cc: coraki!pratt@sun.com
In-Reply-To: Your message of 20 Nov 88 23:26:49 PST (Sun).
	     <8811210726.AA11362@>
Date: 21 Nov 88 09:39:21 PST (Mon)

Some tidy ups:

Picky point: replace "maximal" by "greatest" in my statement of Wand's
theorem.  "Maximal" conventionally means not dominated by any other
element.

Since "standard conservative" is a bit of a mouthful how about
"biconservative" for "standard conservative?"

Wand's theorem in its elementary (noncategorical) form then reads as
follows.

Theorem.  Every biconservative extension of an equational theory has a
greatest base-conservative augment.

This is a really nice theorem.

	I'm not entirely sure, but it seems to me it ought to be possible to
	drop "standard" from the theorem.  Counterexample, anyone?

Silly conjecture.  Both Satish's example and my F(Z) example are
obvious counterexamples.  In my example there exist base-conservative
augments containing respectively F(Z)=X and F(Z)=Y, whose union is no
longer a theory.  And the closure of (i.e. theory generated by) that
union contains X=Y which is not base-conservative.

However, by analogy with Adi Shamir's optimal fixpoint, my intuition is
that there should be some notion of "optimal" base-conservative augment
of a conservative extension, namely one which doesn't make any
"controversial" identifications.  This would presumably be proved by
showing that there is a greatest directed set of base-conservative
augments, whose greatest element would be the optimal augment.

Also it seems reasonable to generalize "base-conservative augment of
an extension" to mean one that makes no identifications of base terms
*other than those already made by the extension itself*. 

If both of these ideas could be made to work, Wand's theorem would look
even nicer:

Theorem?  Every extension of an equational theory has an optimal
base-conservative augment.

together with the observation that when the extension is standard there
is a greatest such augment and it coincides with the optimal one.

This would then be the optimal-base-conservative-augment property of
theory extensions.  The property would be true of equational theories.
It is reasonable to ask whether it holds for Horn theories (seems
plausible) and beyond (less plausible but not obviously false to me
right now).

There is only thing bothering me about all this.  It seems too nice,
elementary, and useful to be not already known to logicians.  Anyone
seen anything like this outside Wand's paper?
-v