Forcing, Transition Algebras, and Calculi

TL;DR

This paper introduces a logical system of transition algebras that extends many-sorted first-order logic with dynamic logic features, enabling richer expressivity including axiomatization of finiteness and reachability, and develops proof methods for completeness.

Contribution

It presents a novel logical framework combining transition algebras with dynamic logic features and establishes proof rules for completeness in countable signatures.

Findings

Enhanced expressivity over many-sorted first-order logic

Finiteness and reachability can be finitely axiomatized

Completeness achieved under certain conditions with generalized forcing

Abstract

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.