Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Forcing, Transition Algebras, and Calculi

Hashimoto Go, Daniel Găină, Ionuţ Ţuţu

TL;DR

This work introduces transition algebra (TA), a many-sorted first-order extension that integrates dynamic logic-style actions to model state transitions, compositions, unions, and reachability. It develops a two-layer entailment framework (basic and dynamic) and shows that TA is not compact, motivating a generalized forcing technique over a category of signatures to prove completeness for the countable-signature fragment TA^c. The authors establish a sound proof system for TA and prove a completeness theorem for TA^c using syntactic forcing and generic models, while also providing CCS encodings to demonstrate the expressive power. The results advance institutional model theory for algebraic specifications and point to practical implications for languages like CafeOBJ, CASL, and Maude, with future work on subsorting, omitting types, and interpolation.

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.

Forcing, Transition Algebras, and Calculi

TL;DR

This work introduces transition algebra (TA), a many-sorted first-order extension that integrates dynamic logic-style actions to model state transitions, compositions, unions, and reachability. It develops a two-layer entailment framework (basic and dynamic) and shows that TA is not compact, motivating a generalized forcing technique over a category of signatures to prove completeness for the countable-signature fragment TA^c. The authors establish a sound proof system for TA and prove a completeness theorem for TA^c using syntactic forcing and generic models, while also providing CCS encodings to demonstrate the expressive power. The results advance institutional model theory for algebraic specifications and point to practical implications for languages like CafeOBJ, CASL, and Maude, with future work on subsorting, omitting types, and interpolation.

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.
Paper Structure (9 sections, 13 theorems, 5 equations, 1 figure)

This paper contains 9 sections, 13 theorems, 5 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Transition algebra
  3. Entailment relations
  4. Basic entailment relation
  5. Dynamic entailment relation
  6. Forcing
  7. Completeness
  8. Conclusions
  9. Proofs for the results presented in Section \ref{['section:transition-algebra']}

Key Result

Proposition 5

For all signature morphisms $\chi:\Sigma\to\Sigma'$, all $\Sigma'$-models $\mathfrak{A}$ and all sentences $\phi\in\mathsf{Sen}(\Sigma)$ we have: $\mathfrak{A}\mathord{\upharpoonright}_{\chi}\models\phi \quad\text{iff}\quad \mathfrak{A}\models\chi(\phi)$.

Figures (1)

  • Figure 1: Proof tree for the continuous output of theorems by the process Institute.

Theorems & Definitions (31)

  • Remark 1
  • Remark 2
  • Remark 3
  • Remark 4
  • Proposition 5
  • Example 6: CCS
  • Example 7
  • Definition 8: Entailment relation
  • Definition 9: Entailment properties
  • Definition 10: Basic entailment relation
  • ...and 21 more