Final algebra semantics are characterised by the opposite assumption to that of
initial semantics, namely, that terms must be proved to be distinguishable,
otherwise they will be taken to be equivalent. The final algebra (if it
exists - see later) is also a model of the theory, that is, all the equations
must be satisfied; the difference is that instead of using the equations to
show the equivalence of otherwise distinct terms, we use them to prove
the distinctness of terms which will otherwise be assumed to be
equivalent. In order to do this usefully we must assume the distinctness of
certain objects; if we do not assume, for instance, that the constants
T and F in Bool are distinguishable in Numbers, then we can construct
the degenerate algebra where all the constructors of both sorts are
mapped onto the single element of the set
(or the member of
any other single-element set). This will (trivially)
satisfy all the equations and so be a model; in fact, it is a final
model.