力迫、转移代数与演算
Forcing, Transition Algebras, and Calculi
AI总结：
提出转移代数逻辑系统，通过引入动态逻辑特性增强多类一阶逻辑，并推广力迫方法至标记范畴，证明了具有可数无限前提证明规则的完备性。
摘要：
我们提出了一种转移代数的逻辑系统，它利用动态逻辑的特性增强了许多种类的一阶逻辑。我们考虑的句子包括转移关系的复合、并集和传递闭包，这些被类似于动态逻辑中使用的动作来处理，以定义必然性和可能性算子。这导致了比许多种类的一阶逻辑更高的表达力。例如，可以有限公理化模型的有限性和可达性，这两者在许多种类的一阶逻辑中通常是不可能的。我们引入了语法蕴含并研究了紧致性和完备性等基本性质，表明当使用标准有限证明规则时，后者不成立。因此，我们定义了具有有限和可数无限前提的证明规则，并提供了可以证明完备性的条件。为此，我们将模型论中由Robinson引入的力迫方法从单一标记推广到标记范畴，并将其应用于获得至多可数标记的完备性结果。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
