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 presents a calculus of terms for operations on such coalgebras, based on a simple type theory, and develops its semantics. The terms admit a single state-valued \textit{parameter}, but may also have state-valued variables. In a ``rigid'' term all state-variables are bound.

Boolean combinations of equations between terms of observable type are shown to form a natural language for specifying properties of polynomial coalgebras, and for giving a Hennessy-Milner style logical characterisation of bisimilarity of states: two states are bisimilar when they satisfy the same rigid observable formulas. Also, our syntax of terms is expressive enough to show, alternatively, that two states are bisimilar when they assign the same values to all ground observable terms. The proof involves a characterisation of bisimulations as relations preserved by certain functions induced by ``paths'' between functors. An analysis of the definability of path actions shows that our language is capable of defining certain modalities. These can be used to express modal assertions to the effect that certain formulas will be true after the execution of a state transition.