Logical definability is investigated for certain classes
of coalgebras related to
state-transition systems, hidden algebras and Kripke
models. The filter
enlargement of a coalgebra A is
introduced as a new coalgebra A+ whose
states are special ``observationally rich'' filters on
the state set of A. The
ultrafilter enlargement is the subcoalgebra A*
of A+ whose
states are ultrafilters.
Boolean combinations of equations between terms of observable(or
output) type are identified as a natural class
of formulas for
specifying properties of coalgebras. These observable
formulasare
permitted to have a single state variable, and form a
language in which
modalitiesdescribing the effects of state transitions
are implicitly
present. A* and A+ validate
the same observable formulas.
It is shown that a class of coalgebras is definable by
observable formulas iff the
class is closed under disjoint unions, images of bisimulations,
and (ultra)filter
enlargements. (Closure under images of bisimulations
is equivalent to
closure under images and domains of coalgebraic morphisms.)
Moreover, every set
of observable formulas has the same models as some set
of conditional
equations.
Examples are constructed to show that the use of enlargements
is essential
in these characterisations, and that there are classes
of coalgebras
definable by conditional observable equations, but not
by equations alone.
The main conclusion of the paper is that to structurally
characterise classes of
coalgebras that are logically definable by modal languages
requires a new
construction, of ``Stone space'' type, in addition to
the coalgebraic duals of
the three constructions (homomorphisms, subalgebras,
direct products) that occur
in Birkhoff's original variety theorem for algebras.