  We bring forward a logical system of transition algebras that enhances
many-sorted first-order logic using features from dynamic logics. The sentences
we consider include compositions, unions, and transitive closures of transition
relations, which are treated similarly to the actions used in dynamic logics in
order to define necessity and possibility operators. This leads to a higher
degree of expressivity than that of many-sorted first-order logic. For example,
one can finitely axiomatize both the finiteness and the reachability of models,
neither of which are ordinarily possible in many-sorted first-order logic. We
introduce syntactic entailment and study basic properties such as compactness
and completeness, showing that the latter does not hold when standard finitary
proof rules are used. Consequently, we define proof rules having both finite
and countably infinite premises, and we provide conditions under which
completeness can be proved. To that end, we generalize the forcing method
introduced in model theory by Robinson from a single signature to a category of
signatures, and we apply it to obtain a completeness result for signatures that
are at most countable.
