Formalizing "no junk, no confusion" Goguen has popularized the initial algebra view of semantics via his "no junk, no confusion" slogan.  By "no junk", he means that models of a theory presentation should not have unnecessary elements, and "no confusion" that terms should not be mapped to equal values unless they are provably equal.  Sometimes, "no junk" is also interpreted as every element in the model is a denotation of a term, while "no confusion" as two different terms denote different elements in the model.  [These are classically equivalent statements, but they are not intuinistically equivalent, so I mention both].
My questions are:


*

*What is a 'good' formalization of this slogan?  By this I mean an explicit statement of "no junk, no confusion" in the meta-logic (since we're talking about models), where the logical strength of the corresponding statement is well understood.

*Are there logics in which these requirements can be internalized?

*What would be the corresponding slogan to "no junk, no confusion" for final coalgebras?
 A: The way I understand each of the slogans is as follows: 


*

*"No junk" I just take to mean that an appropriate induction principle is valid -- that is, we should look for initial models in the appropriate category of algebras for the theory. This also implies that every element of the model is in the image of the interpretation of the the algebraic theory. 
Presumably the dualization to coalgebras would just be the validity of using bisimilarity to prove equality. 

*"No confusion" is traditionally interpreted to mean that we should look for models in which two elements of the model are semantically equal if and only if the corresponding syntaxes are provably equal. This is the really bizarre requirement, since it amounts to requiring that the model be isomorphic to the term model! And yet Goguen and the algebraic specification community were emphatically not happy with decreeing the term model to be the intended model -- they work very hard to get the "right" model.
I personally (ie, I don't know that anyone else believes this) take the way this requirement is phrased to be an artifact of the history of algebraic specification. IIRC, they started out with purely algebraic theories -- that is, theories in which the equational axioms are all pure equalities. (E.g., the axioms for groups.) Now, of course every such algebraic theory has a degenerate model, since the one-element model validates all equalities.  So the no-confusion principle is intended to rule out such degenerate models. 
These days, of course, the algebraic specification crowd has no problem with theories with inequalities (e.g., the field axioms), and I think this additional freedom lets us state the no-confusion principle in a better way. Namely, we should design algebraic theories whose models are categorical. That is, we want theories for which all models are isomorphic. This implies the traditional no-confusion criterion, and also explains why people try to adjust the signature when they can't prove it. (Of course, this is a non-first-order property in general, as you need higher-order logic or set theory to quantify over models.) 
A: Belatedly, an answer in set-based situations to


*

*What would be the corresponding slogan to "no junk, no confusion" for final coalgebras?


Given an initial algebra, any algebra will have a special subobject which is the image of the initial structure. The subobject may have confused elements (terms) of the initial algebra, and the object may have extra junk. A map between objects will map the first special subobject to the second, possibly confusing more. The initial algebra has no confusion and no junk.
Given a final/terminal coalgebra, the elements of any coalgebra will have a special colouring in terms of images in the elements of the terminal structure. The object may have more than one element with the same colour, and the object may not use all the colours. A map between objects will preserve the colouring, the domain possibly using fewer colours. The terminal coalgebra colours without ambiguity and without redundancy. If two things behave the same way, they are the same; all behaviours are covered.
No junk, no confusion; No redundancy, no ambiguity.
A: The slogan is a meaningful english phrase.  After removing negation, we may obtain this phrase: "stay clean, stay clear".  So then, here is an actual theorem of quantified boolean formulas that describes both qualities formally:
Linear Corollary:  Quantified  monotone  boolean formulas are linearly decidable. 
That is, no matter how many alternating quantifiers are in the prefix, when the body of the formula has "zero negations," then the monotonicity of the formula makes any quantifier prefix linearly decidable;  plug T for existentially quantified variables, NIL for universally quantified variables, then evaluate the boolean form, entirely linear in the size of the QBF. 
Goguen may also enjoy the car/cdr Structure of Common Sense:  Good ideas   Usually have   Two words.  
