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.

翻译：我们提出了一种转移代数的逻辑系统，该利用动态逻辑的特征增强了多类一阶逻辑。我们考虑的语句包括转移关系的复合、并及传递闭包，这些处理方式类似于动态逻辑中用于定义必然性和可能性算子的动作。这使得其表达能力高于多类一阶逻辑。例如，可以有限公理化的表达模型的有限性和可达性，而这些在多类一阶逻辑中通常无法实现。我们引入了语法蕴涵，并研究了紧致性和完备性等基本性质，表明在使用标准有限推理规则时完备性不成立。因此，我们定义了同时包含有限可数无限前提的推理规则，并给出了可以证明完备性的条件。为此，我们将罗宾逊在模型论中引入的强制方法从单签名推广到签名的范畴，并将其应用于获得至多可数签名的完备性结果。