Model-theoretic Forcing in Transition Algebra

TL;DR

This paper introduces a forcing technique for a complex many-sorted logic called Transition Algebra, proving key theorems despite its high expressivity and non-compactness, and extends proof systems for finite models.

Contribution

It develops a generalized forcing method for Transition Algebra, establishing L"owenheim-Skolem and Omitting Types theorems in a non-compact setting, and extends proof rules for finite transition models.

Findings

Established a forcing technique for Transition Algebra.

Proved L"owenheim-Skolem and Omitting Types theorems in this logic.

Extended proof systems to finite and constructor-based transition algebras.

Abstract

We study L\"owenheim-Skolem and Omitting Types theorems in Transition Algebra, a logical system obtained by enhancing many sorted first-order logic with features from dynamic logic. The sentences we consider include compositions, unions, and transitive closures of transition relations, which are treated similarly to actions in dynamic logics to define necessity and possibility operators. We show that Upward L\"owenheim-Skolem theorem, any form of compactness, and joint Robinson consistency property fail due to the expressivity of transitive closures of transitions. In this non-compact many-sorted logical system, we develop a forcing technique method by generalizing the classical method of forcing used by Keisler to prove Omitting Types theorem. Instead of working within a single signature, we work with a directed diagram of signatures, which allows us to establish Downward L\"owenheim-Skolem and Omitting Types theorems despite the fact that models interpret sorts as sets, possibly empty. Building on a complete system of proof rules for Transition Algebra, we extend it with additional proof rules to reason about constructor-based and/or finite transition algebras. We then establish the completeness of this extended system for a fragment of Transition Algebra obtained by restricting models to constructor-based and/or finite transition algebras.