Bisimulation and Apartness in Coalgebraic Specification

. A first basic fact in algebra (or, in algebraic specification) is the existence of free algebras, as suitable sets of terms. In coalgebraic specification, terminal coalgebras are known to exist in Sets (and in other categories) via the standard limit construction. Here we characterize these terminal coalgebras as sets of "trees of observations". It is a standard result that elements of (the carrier of) a coalgebra are bisimilar (i.e. indistinguishable via the coalgebra operations) if and only if they have the same interpretation in the terminal coalgebra. This now becomes: if and only if they have the same tree of observations. Instead of putting emphasis on bisimulation---which is a rather evasive notion---we consider its negation, which we write as #, and call "apartness ". It behaves like apartness in constructive mathematics. Indeed, the big advantage of apartness over bisimulation is that it can be established in a finite number of steps. It is a positive notion. Finally we show..