A syntax and semantics of types, terms and formulas for
coalgebras of polynomial functors is developed, extending earlier work
on monomial coalgebras to include functors
constructed using coproducts. A modified ultrapower construction
for polynomial coalgebras is introduced, adapting the conventional ultrapower
to retain only those states that evaluate observable terms in a standard way.

A special role is played by terms that take observable values and are
"rigid": their free variables do not occur in any state-valued subterm. The
following "co-Birkhoff" theorem is proved:  a class of polynomial coalgebras
is definable by Boolean combinations of equations between rigid terms iff the class
is closed under disjoint unions, images of bisimulations, and observable
ultrapowers.

The paper is an extended abstract, surveying all the rlevant concepts and
explaining the results, but leaving out the more technical results. Full
details will appear in two planned papers:
Equational Logic of Polynomial Coalgebras and
Observational Ultrapowers of Polynomial Coalgebras.