Coalgebras of polynomial functors constructed from sets of
observable elements have been found useful in modelling various kinds of data
types and state-transition systems. This paper continues the study of
equational logic and model theory for polynomial coalgebras begun in
Equational Logic of Polynomial Coalgebras, where it was shown that
Boolean combinations of equations between terms of observable type form a
natural language of
observable formulas for
specifying properties of polynomial coalgebras, and for giving a
Hennessy-Milner style logical characterisation of observational
indistinguishability (bisimilarity) of states.
Here we give a structural characterisation of classes of coalgebras definable by observable formulas. This is an analogue for polynomial coalgebras of Birkhoff's celebrated characterisation of equationally definable classes of abstract algebras as being those closed under homomorphic images, subalgebras, and direct products. The coalgebraic characterisation involves new notions of observational ultraproduct and ultrapower of coalgebras, obtained from the classical construction of ultraproducts by deleting states that assign ``nonstandard'' values to terms of observable type. A class of polynomial coalgebras is shown to be the class of all models of a set of observable formulas if, and only if, it is closed under images of bisimulation relations, disjoint unions and observational ultrapowers.
Observational ultraproducts are also used to discuss compactness---which holds only under limited conditions; to characterize finitely axiomatizable classes of polynomial coalgebras; and to show that there are axiomatizable classes that are not finitely axiomatizable.