Model-Theoretic Forcing in Transition Algebra

Hashimoto, Go; Găină, Daniel

doi:10.4230/LIPIcs.MFCS.2025.55

Model-Theoretic Forcing in Transition Algebra

Go Hashimoto

Kyushu University, Fukuoka, Japan Daniel Găină

Kyushu University, Fukuoka, Japan

Abstract

We study Löwenheim-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öwenheim-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öwenheim-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.

Keywords and phrases:

institutional model theory, algebraic specification, transition algebra, forcing, omitting types property, Löwenheim-Skolem properties, completeness

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Logic and verification

Related Version:

Full paper, including proofs: http://arxiv.org/abs/2506.22828 [20]

Funding:

The work presented in this paper has been partially supported by Japan Society for the Promotion of Science, grant number 23K11048.

DOI:

10.4230/LIPIcs.MFCS.2025.55

Event:

50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Editors:

Paweł Gawrychowski, Filip Mazowiecki, and Michał Skrzypczak

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Transition Algebra [19], abbreviated ${\mathsf{TA}}$ , offers a logical framework for modeling and reasoning about state transitions in systems, particularly in concurrency theory and computer science. Closely related to modal logics and algebraic specification languages executable by rewriting, it provides a structured approach to describing system evolution based on predefined rules. The key concepts in transition algebra are (a) states, which are characterized using equational theories, and (b) transitions, which are represented as labeled relations between states. Transition algebra can be broadly viewed as an extension of many-sorted first-order logic, incorporating features from dynamic logic. It includes algebraic operators that define how transitions combine, such as (a) Sequential composition ( $\mathbin{\mathchoice{\raisebox{-1.94444pt}{\leavevmode\resizebox{6.11111pt}{6.% 24998pt}{\hbox{\raisebox{1.94444pt}{$\displaystyle\hbox{ ;}$}}}}}{\raisebox{-1% .94444pt}{\leavevmode\resizebox{6.11111pt}{6.24998pt}{\hbox{\raisebox{1.94444% pt}{$\textstyle\hbox{ ;}$}}}}}{\raisebox{-1.3611pt}{\leavevmode\resizebox{4.95% 836pt}{4.37498pt}{\hbox{\raisebox{1.3611pt}{$\scriptstyle\hbox{ ;}$}}}}}{% \raisebox{-0.97221pt}{\leavevmode\resizebox{4.37506pt}{3.12498pt}{\hbox{% \raisebox{0.97221pt}{$\scriptscriptstyle\hbox{ ;}$}}}}}}$ ): if a system moves from state $t_{1}$ to $t_{2}$ according to transition rule $\mathfrak{a}_{1}$ , and then from $t_{1}$ to $t_{2}$ under transition rule $\mathfrak{a}_{2}$ , this is written as $\mathfrak{a}_{1}\mathbin{\mathchoice{\raisebox{-1.94444pt}{\leavevmode% \resizebox{6.11111pt}{6.24998pt}{\hbox{\raisebox{1.94444pt}{$\displaystyle% \hbox{ ;}$}}}}}{\raisebox{-1.94444pt}{\leavevmode\resizebox{6.11111pt}{6.24998% pt}{\hbox{\raisebox{1.94444pt}{$\textstyle\hbox{ ;}$}}}}}{\raisebox{-1.3611pt}% {\leavevmode\resizebox{4.95836pt}{4.37498pt}{\hbox{\raisebox{1.3611pt}{$% \scriptstyle\hbox{ ;}$}}}}}{\raisebox{-0.97221pt}{\leavevmode\resizebox{4.3750% 6pt}{3.12498pt}{\hbox{\raisebox{0.97221pt}{$\scriptscriptstyle\hbox{ ;}$}}}}}}% \mathfrak{a}_{2}$ , (b) Choice ( $\cup$ ): represents nondeterministic choices between transitions. (c) Iteration ( $*$ ): denotes repeated transitions, analogous to the Kleene star in formal language theory. Iteration ( $*$ ), has been employed in the literature to enhance the expressive power of first-order logic, albeit at the expense of compactness. Notably, Fagin’s work on Transitive Closure Logic (TCL) has been extensively studied within the frameworks of finite model theory and descriptive complexity [9, 10]. However, apart from the work on ${\mathsf{TA}}$ [19], we are not aware of any model-theoretic studies of first-order logic with iteration beyond the scope of finite model theory. Moreover, when sorts – possibly infinitely many – and models interpreting those sorts as sets – possibly empty – are permitted, extending existing techniques to such a framework poses significant challenges and lacks a straightforward solution.

In [19], it is shown that transition algebra possesses an essential property for modularization, known as the satisfaction condition. This condition states that truth remains invariant under changes in notation. Here, a change in notation refers to the translation between local languages constructed from vocabularies, often called signatures. Consequently, transition algebra is formalized as an institution [11], a category-theoretic framework that captures the notion of logic by incorporating its syntax, semantics, and the satisfaction relation between them. Similarly, the logic underlying CafeOBJ [8] satisfies the satisfaction condition for signature morphisms, allowing it to be formalized as an institution. However, its models cannot distinguish between different transitions occurring between the same states, as transitions are represented by preorder relations. In contrast, Rewriting Logic [25] – the foundation of Maude [4] – offers greater expressivity by treating transitions as arrows in a category, where states serve as objects. This expressiveness comes at a cost, as the satisfaction condition does not hold in Rewriting Logic. On the other hand, transition algebra retains the modular properties of the preorder algebras in CafeOBJ due to its institutional structure while achieving the same level of expressivity as Rewriting Logic.

Given a set of properties formalized as first-order sentences, practitioners seek to study a restricted class of transition algebras that satisfy these properties. In fields such as formal methods and functional programming – where computation and reasoning rely on abstract data types and term rewriting – many algebraic structures are naturally described using constructor operators, such as numbers with 0 and succ, or lists with nil and cons. Pattern matching on constructors further simplifies function definitions. A related example is Finite Model Theory [24, 12], which focuses on logical structures with a finite domain. This area is particularly relevant to database theory, complexity theory, and various computer science applications. Building on a complete system of proof rules for ${\mathsf{TA}}$ , such as the one proposed in [19], we extend it with additional proof rules to reason about constructor-based and/or finite transition algebras. We refer the reader to [2, 1, 17] for theoretical foundations of constructor-based models and to [27] for a formal method developed for reasoning about such models. We then establish the completeness of this extended system for the fragment of ${\mathsf{TA}}$ obtained by restricting the semantics to constructor-based and/or finite transition algebras.

In this work, we use Omitting Types Theorem (OTT) to extend completeness of ${\mathsf{TA}}$ to a fragment obtained by restricting the semantics to constructor-based transition algebras with finite carrier sets. The OTT states that if a first-order theory $\Phi$ does not require a certain type (a set of formulas describing a potential element) to be realized, then there exists a model of $\Phi$ that omits this type. This ensures the existence of models that exclude specific unwanted elements. A key challenge arises from the fact that models with potentially empty carrier sets are allowed in ${\mathsf{TA}}$ . In this model-theoretic framework, extending the initial signature with an infinite number of constants cannot always be achieved while preserving the satisfiability of the underlying theory. To address this, we employ a forcing technique introduced in [19] to prove completeness of ${\mathsf{TA}}$ . Forcing was originally introduced by Paul Cohen [5, 6] in set theory to show the independence of the continuum hypothesis from the other axioms of Zermelo-Fraenkel set theory. Robinson [28] developed an analogous theory of forcing in model theory. The forcing technique has been studied in institutional model theory at an abstract, category-theoretic level, in works such as [18, 14, 15]. The forcing method proposed in [19] generalizes classical forcing from a single signature to a category of signatures, enabling the dynamic addition of both constants and sentences while preserving satisfiability. Notably, this dynamic forcing method is particularly suited for logical systems that are not compact, such as ${\mathsf{TA}}$ .

Additionally, we show that ${\mathsf{TA}}$ theories have some control over the cardinality of their models. The Upward Löwenheim–Skolem Theorem does not hold in general, as there exist theories that uniquely determine a model up to isomorphism, provided that the model’s size is exactly the cardinality of the power of its underlying signature.¹¹1The power of a signature is the cardinality of the set of all sentences that can be formed in its language. It is interesting to note that the Downward Löwenheim–Skolem Theorem does hold, as for any model whose size exceeds the power of its underlying signature, one can construct an elementary submodel whose size matches the power of the signature.

2 Transition algebra

In this section, we recall the logic of many-sorted transition algebras [19], or transition algebra ( ${\mathsf{TA}}$ ), for short. We present, in order: signatures, models, sentences, and the ${\mathsf{TA}}$ satisfaction relation.

Signatures.

The signatures we consider are ordinary algebraic signatures endowed with polymorphic transition labels. We denote them by triples of the form $(S,F,L)$ , where:

$\blacksquare$

$(S,F)$ is a many-sorted algebraic signature consisting of a set of sorts $S$ and a set of function symbols $F=\{\sigma:w\to s\mid w\in S^{*}\text{ and }s\in S\}$ ;
$\blacksquare$

$L$ is a set whose elements we call transition labels.

Given a function symbol $\sigma:w\to s\in F$ , we refer to $w\in S^{*}$ as its arity and $s\in S$ as its sort. When $w$ is the empty arity, we may speak of $\sigma\colon\to s$ as a constant of sort $s$ .

Throughout the paper, we let $\Sigma$ , $\Sigma^{\prime}$ , and $\Sigma_{i}$ range over signatures of the form $(S,F,L)$ , $(S^{\prime},F^{\prime},L^{\prime})$ , and $(S_{i},F_{i},L_{i})$ , respectively.

As usual in institution theory [7, 29], important constructions such as signature extensions with constants as well as open formulae and quantifiers are realized in a multi-signature setting, so moving between signatures is common. A signature morphism $\chi\colon\Sigma\to\Sigma^{\prime}$ consists of a triple $\chi=(\chi^{st},\chi^{op},\chi^{lb})$ , where (a) $\chi^{st}:S\to S^{\prime}$ is a function mapping sorts, (b) $\chi^{op}:F\to F^{\prime}$ maps each function symbol $\sigma:s_{1}\dots s_{n}\to s\in F$ to a function symbol $\chi^{op}(\sigma):\chi^{st}(s_{1})\dots\chi^{st}(s_{n})\to\chi(s)\in F^{\prime}$ and (c) $\chi^{lb}:L\to L^{\prime}$ is a function mapping labels. For convenience, we typically omit the superscripts $s t$ , $o p$ and $l b$ in the notation.

$\blacktriangleright$ Remark 1.

Signature morphisms compose componentwise. This composition is associative and has identities, forming a category $\mathsf{Sig}$ of signatures.

Models.

Given a signature $\Sigma$ , a $\Sigma$ -model $\mathfrak{A}$ consists of:

$\blacksquare$

an $(S,F)$ -algebra $\mathfrak{A}$ , where each sort $s\in S$ is interpreted by $\mathfrak{A}$ as a set $\mathfrak{A}_{s}$ and each function symbol $\sigma:s_{1}\dots s_{n}\to s\in F$ is interpreted by $\mathfrak{A}$ as a function $\sigma^{\mathfrak{A}}:\mathfrak{A}_{s_{1}}\times\ldots\times\mathfrak{A}_{s_{n% }}\to\mathfrak{A}_{s}$ ;
$\blacksquare$

an interpretation of each label $\varrho\in L$ as a many-sorted transition relation $\varrho^{\mathfrak{A}}\subseteq\mathfrak{A}\times\mathfrak{A}$ , where $\varrho^{\mathfrak{A}}=\{\varrho^{\mathfrak{A}}_{s}\}_{s\in S}$ and $\varrho^{\mathfrak{A}}_{s}\subseteq\mathfrak{A}_{s}\times\mathfrak{A}_{s}$ for all sorts $s\in S$ . ²²2In principle, relations of any arity could be defined, and the results presented in this paper would still hold. However, in algebraic specification languages that are executable via rewriting, the only relations considered are transitions, which are defined between pairs of elements of the same sort. Furthermore, the iteration operator ( $*$ ) can be applied exclusively to transitions.

A homomorphism $h:\mathfrak{A}\to\mathfrak{B}$ over a signature $\Sigma$ is an algebraic $(S,F)$ -homomorphism that preserves transitions: $h(\varrho^{\mathfrak{A}})\subseteq\varrho^{\mathfrak{B}}$ for all $\varrho\in L$ . It is easy to see that $\Sigma$ -homomorphisms form a category, which we denote by $\mathsf{Mod}^{\mathsf{TA}}(\Sigma)$ , under their obvious componentwise composition.

$\blacktriangleright$ Remark 2.

Every signature morphism $\chi\colon\Sigma\to\Sigma^{\prime}$ determines a model-reduct functor $\_\mathord{\upharpoonright}_{\chi}\colon\mathsf{Mod}^{\mathsf{TA}}(\Sigma^{% \prime})\to\mathsf{Mod}^{\mathsf{TA}}(\Sigma)$ such that:

$\blacksquare$

for every $\Sigma^{\prime}$ -model $\mathfrak{A}^{\prime}$ , $(\mathfrak{A}^{\prime}\mathord{\upharpoonright}_{\chi})_{s}=\mathfrak{A}^{% \prime}_{\chi(s)}$ for each sort $s\in S$ , $\sigma^{(\mathfrak{A}^{\prime}\mathord{\upharpoonright}_{\chi})}=\chi(\sigma)^% {\mathfrak{A}^{\prime}}$ for each symbol $\sigma\in F$ , and $\varrho^{(\mathfrak{A}^{\prime}\mathord{\upharpoonright}_{\chi})}=\chi(\varrho% )^{\mathfrak{A}^{\prime}}$ for each label $\varrho\in L$ ; and
$\blacksquare$

for every $\Sigma^{\prime}$ -homomorphism $h^{\prime}\colon\mathfrak{A}^{\prime}\to\mathfrak{B}^{\prime}$ , $(h^{\prime}\mathord{\upharpoonright}_{\chi})_{s}=h^{\prime}_{\chi(s)}$ for each $s\in S$ .

Moreover, the mapping $\chi\mapsto\_\mathord{\upharpoonright}_{\chi}$ is functorial.

For any signature morphism $\chi:\Sigma\to\Sigma^{\prime}$ , any $\Sigma$ -model $\mathfrak{A}$ and any $\Sigma^{\prime}$ -model $\mathfrak{A}^{\prime}$ if $\mathfrak{A}=\mathfrak{A}^{\prime}\mathord{\upharpoonright}_{\chi}$ , we say that $\mathfrak{A}$ is the $\chi$ -reduct of $\mathfrak{A}^{\prime}$ , and that $\mathfrak{A}^{\prime}$ is a $\chi$ -expansion of $\mathfrak{A}$ . For example, for a many-sorted set $X$ (say, of variables) that is disjoint from the set of constants in $\Sigma$ , consider the inclusion morphism $\iota_{X}:\Sigma\hookrightarrow\Sigma[X]$ , where $\Sigma[X]=(S,F[X],L)$ is the signature obtained from $\Sigma$ by adding the elements of $X$ to $F$ as new constants of appropriate sort. Then an expansion of a $\Sigma$ -model $\mathfrak{A}$ along $\iota_{X}$ can be seen as a pair $\mathfrak{A}^{\prime}={\langle}\mathfrak{A},f:X\to\mathfrak{A}{\rangle}$ , where $f$ is a valuation of $X$ in $\mathfrak{A}$ .

As in many-sorted algebra, there is a special, initial model in $\mathsf{Mod}^{\mathsf{TA}}(\Sigma)$ , which we denote by $T_{\Sigma}$ , whose elements are ground terms built from function symbols, and whose transitions are all empty. The $\Sigma$ -model $T_{\Sigma}(X)$ of terms with variables from $X$ is defined as the $\iota_{X}$ -reduct of $T_{\Sigma[X]}$ ; i.e., $T_{\Sigma}(X)=T_{\Sigma[X]}\mathord{\upharpoonright}_{\iota_{X}}$ .

Sentences.

Given a signature $\Sigma$ , the set $A$ of actions is defined by the following grammar:

\mathfrak{a}\leavevmode\nobreak\ \Coloneqq\leavevmode\nobreak\ \varrho% \leavevmode\nobreak\ \mid\leavevmode\nobreak\ \mathfrak{a}\mathbin{\mathchoice% {\raisebox{-1.94444pt}{\leavevmode\resizebox{6.11111pt}{6.24998pt}{\hbox{% \raisebox{1.94444pt}{$\displaystyle\hbox{ ;}$}}}}}{\raisebox{-1.94444pt}{% \leavevmode\resizebox{6.11111pt}{6.24998pt}{\hbox{\raisebox{1.94444pt}{$% \textstyle\hbox{ ;}$}}}}}{\raisebox{-1.3611pt}{\leavevmode\resizebox{4.95836pt% }{4.37498pt}{\hbox{\raisebox{1.3611pt}{$\scriptstyle\hbox{ ;}$}}}}}{\raisebox{% -0.97221pt}{\leavevmode\resizebox{4.37506pt}{3.12498pt}{\hbox{\raisebox{0.9722% 1pt}{$\scriptscriptstyle\hbox{ ;}$}}}}}}\mathfrak{a}\leavevmode\nobreak\ \mid% \leavevmode\nobreak\ \mathfrak{a}\cup\mathfrak{a}\leavevmode\nobreak\ \mid% \leavevmode\nobreak\ \mathfrak{a}^{*}

where $\varrho$ is a transition label. We let $A$ denote the set of all actions and extend our notational convention for signature components to their corresponding sets of actions. Specifically, we use: (a) $A^{\prime}$ to denote the set of actions over a signature $\Sigma^{\prime}$ , (b) $A_{i}$ to denote the set of actions over a signature $\Sigma_{i}$ , and similarly for other variations. Moreover, through a slight abuse of notation, we also denote by $\chi\colon A\to A^{\prime}$ the canonical map determined by a signature morphism $\chi\colon\Sigma\to\Sigma^{\prime}$ .

To define sentences, we assume a countably infinite set of variable names $\{v_{i}\mid i<\omega\}$ . A variable for a signature $\Sigma$ is a triple ${\langle}v_{i},s,\Sigma{\rangle}$ , where (a) $v_{i}$ is a variable name and (b) $s$ is a sort in $\Sigma$ . The third component is used only to ensure that variables are distinct from the constants declared in $\Sigma$ , which is essential when dealing with quantifiers. The set $\mathsf{Sen}^{\mathsf{TA}}(\Sigma)$ of sentences over $\Sigma$ is given by the following grammar:

\phi\Coloneqq t=t^{\prime}\mid\mathfrak{a}(t_{1},t_{2})\mid\neg\phi\mid\lor% \Phi\mid\exists X\,{\cdot}\,\phi^{\prime}

where (a) $t$ and $t^{\prime}$ are $\Sigma$ -terms of the same sort; (b) $\mathfrak{a}$ is any action; (c) $t_{1}$ and $t_{2}$ are $\Sigma$ -terms of the same sort; (d) $\Phi$ is a finite set of $\Sigma$ -sentences; and (e) $X$ is a finite block of $\Sigma$ -variables, that is, $X$ is a finite set of variables such that if ${\langle}v_{i},s_{1},\Sigma{\rangle},{\langle}v_{j},s_{2},\Sigma{\rangle}\in X$ and $s_{1}\neq s_{2}$ then $i\neq j$ ; and (f) $\phi^{\prime}$ is a $\Sigma[X]$ -sentence. A sentence $\mathfrak{a}(t_{1},t_{2})$ is called a transition rule, which can also be written in infix notation $t_{1}\mathrel{\mathfrak{a}}t_{2}$ . An atomic sentence is a ground equation $t=t^{\prime}$ or a ground transition rule of the form $t_{1}\mathrel{\varrho}t_{2}$ , where $\varrho\in L$ is a transition label.

Besides the above core connectives, we also make use of the following convenient (and standard) abbreviations: $\land\Phi\coloneqq\neg\lor_{\phi\in\Phi}\neg\phi$ for finite conjunctions; $\bot\coloneqq\lor\emptyset$ for falsity; $\top\coloneqq\land\emptyset=\neg\bot$ for truth; $\phi_{1}\Rightarrow\phi_{2}\coloneqq\neg\phi_{1}\vee\phi_{2}$ for implications; and $\forall X\,{\cdot}\,\phi^{\prime}\coloneqq\neg\exists X\,{\cdot}\,\neg\phi^{\prime}$ for universally quantified sentences.

$\blacktriangleright$ Remark 3.

Any signature morphism $\chi\colon\Sigma\to\Sigma^{\prime}$ can be canonically extended to a sentence-translation function $\chi\colon\mathsf{Sen}^{\mathsf{TA}}(\Sigma)\to\mathsf{Sen}^{\mathsf{TA}}(% \Sigma^{\prime})$ given by:

$\blacksquare$

$\chi(t=t^{\prime})\coloneqq(\chi(t)=\chi(t^{\prime}))$ ;
$\blacksquare$

$\chi(t_{1}\mathrel{\mathfrak{a}}t_{2})\coloneqq\chi(t_{1})\mathrel{\chi(% \mathfrak{a})}\chi(t_{2})$ ;
$\blacksquare$

$\chi(\neg\phi)\coloneqq\neg\chi(\phi)$ ;
$\blacksquare$

$\chi(\lor\Phi)\coloneqq\lor\chi(\Phi)$ ; and
$\blacksquare$

$\chi(\exists X\,{\cdot}\,\phi^{\prime})\coloneqq\exists X^{\prime}\,{\cdot}\,% \chi^{\prime}(\phi^{\prime})$ , where $X^{\prime}=\{{\langle}v_{i},\chi(s),\Sigma^{\prime}{\rangle}\mid{\langle}v_{i}% ,s,\Sigma{\rangle}\in X\}$ and $\chi^{\prime}:\Sigma[X]\to\Sigma^{\prime}[X^{\prime}]$ is the extension of $\chi:\Sigma\to\Sigma^{\prime}$ mapping each ${\langle}v_{i},s,\Sigma{\rangle}\in X$ to ${\langle}v_{i},\chi(s),\Sigma^{\prime}{\rangle}\in X^{\prime}$ .

Moreover, this sentence-translation mapping is functorial in $\chi$ .

For the sake of simplicity, we identify variables only by their name and sort, provided that there is no danger of confusion. Using this convention, each inclusion morphism $\iota\colon\Sigma\hookrightarrow\Sigma^{\prime}$ determines an inclusion function $\iota\colon\mathsf{Sen}^{\mathsf{TA}}(\Sigma)\hookrightarrow\mathsf{Sen}^{% \mathsf{TA}}(\Sigma^{\prime})$ , which corresponds to the approach of classical model theory. This simplifies the presentation greatly. A situation when we cannot apply this convention arises when translating a $\Sigma$ -sentence $\exists X\,{\cdot}\,\phi$ along the inclusion $\iota_{X}:\Sigma\hookrightarrow\Sigma[X]$ .

Satisfaction relation.

Actions are interpreted as binary relations in models. Given a model $\mathfrak{A}$ over a signature $\Sigma$ , and actions $\mathfrak{a},\mathfrak{a}_{1},\mathfrak{a}_{2}\in A$ , we have:

$\blacksquare$

$(\mathfrak{a}_{1}\mathbin{\mathchoice{\raisebox{-1.94444pt}{\leavevmode% \resizebox{6.11111pt}{6.24998pt}{\hbox{\raisebox{1.94444pt}{$\displaystyle% \hbox{ ;}$}}}}}{\raisebox{-1.94444pt}{\leavevmode\resizebox{6.11111pt}{6.24998% pt}{\hbox{\raisebox{1.94444pt}{$\textstyle\hbox{ ;}$}}}}}{\raisebox{-1.3611pt}% {\leavevmode\resizebox{4.95836pt}{4.37498pt}{\hbox{\raisebox{1.3611pt}{$% \scriptstyle\hbox{ ;}$}}}}}{\raisebox{-0.97221pt}{\leavevmode\resizebox{4.3750% 6pt}{3.12498pt}{\hbox{\raisebox{0.97221pt}{$\scriptscriptstyle\hbox{ ;}$}}}}}}% \mathfrak{a}_{2})^{\mathfrak{A}}=\mathfrak{a}_{1}^{\mathfrak{A}}\mathbin{% \mathchoice{\raisebox{-1.94444pt}{\leavevmode\resizebox{6.11111pt}{6.24998pt}{% \hbox{\raisebox{1.94444pt}{$\displaystyle\hbox{ ;}$}}}}}{\raisebox{-1.94444pt}% {\leavevmode\resizebox{6.11111pt}{6.24998pt}{\hbox{\raisebox{1.94444pt}{$% \textstyle\hbox{ ;}$}}}}}{\raisebox{-1.3611pt}{\leavevmode\resizebox{4.95836pt% }{4.37498pt}{\hbox{\raisebox{1.3611pt}{$\scriptstyle\hbox{ ;}$}}}}}{\raisebox{% -0.97221pt}{\leavevmode\resizebox{4.37506pt}{3.12498pt}{\hbox{\raisebox{0.9722% 1pt}{$\scriptscriptstyle\hbox{ ;}$}}}}}}\mathfrak{a}_{2}^{\mathfrak{A}}$ (i.e., diagrammatic composition of binary relations);
$\blacksquare$

$(\mathfrak{a}_{1}\cup\mathfrak{a}_{2})^{\mathfrak{A}}=\mathfrak{a}_{1}^{% \mathfrak{A}}\cup\mathfrak{a}_{2}^{\mathfrak{A}}$ (the union of binary relations); and
$\blacksquare$

$(\mathfrak{a}^{*})^{\mathfrak{A}}=(\mathfrak{a}^{\mathfrak{A}})^{*}$ (the reflexive and transitive closure of binary relations).

We define the satisfaction relation between models and sentences as follows:

$\blacksquare$

$\mathfrak{A}\models t=t^{\prime}$ iff $t^{\mathfrak{A}}=t^{\prime\mathfrak{A}}$ ;
$\blacksquare$

$\mathfrak{A}\models t_{1}\mathrel{\mathfrak{a}}t_{2}$ iff $(t_{1}^{\mathfrak{A}},t_{2}^{\mathfrak{A}})\in\mathfrak{a}^{\mathfrak{A}}$ ;
$\blacksquare$

$\mathfrak{A}\models\neg\phi$ iff $\mathfrak{A}\not\models\phi$ ;
$\blacksquare$

$\mathfrak{A}\models\lor\Phi$ iff $\mathfrak{A}\models\phi$ for some sentence $\phi\in\Phi$ ; and
$\blacksquare$

$\mathfrak{A}\models\exists X\,{\cdot}\,\phi^{\prime}$ iff $\mathfrak{A}^{\prime}\models\phi^{\prime}$ for some expansion $\mathfrak{A}^{\prime}$ of $\mathfrak{A}$ to the signature $\Sigma[X]$ .

Proposition 4 (Satisfaction condition).

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

The satisfaction condition for ${\mathsf{TA}}$ is given in [19].

Logical framework.

Throughout this paper, we work within a fragment $\mathcal{L}$ of ${\mathsf{TA}}$ which is obtained by (a) restricting the category of signatures – without prohibiting signature extensions with constants – and (b) discarding a subset of sentence or/and action operators from the grammar which is used to define sentences in ${\mathsf{TA}}$ . When there is no danger of confusion we drop (a) the subscript $\mathcal{L}$ from the notations $\mathsf{Sig}^{\mathcal{L}}$ and $\mathsf{Sen}^{\mathcal{L}}$ , and (b) the subscript ${\mathsf{TA}}$ from the notation $\mathsf{Mod}^{\mathsf{TA}}$ . We denote by $\mathsf{Sen}_{0}:\mathsf{Sig}\to\mathbb{S}\mathsf{et}$ the sub-functor of $\mathsf{Sen}:\mathsf{Sig}\to\mathbb{S}\mathsf{et}$ , which maps each signature $\Sigma$ in $\mathcal{L}$ to the set $\mathsf{Sen}_{0}(\Sigma)$ of atomic sentences from $\mathsf{Sen}(\Sigma)$ .

3 Related concepts

We define the necessary concepts and present the existing results for presenting our advancements. We make the following notational conventions:

$\blacksquare$

Recall that in any category $\mathcal{C}$ , the notation $|\mathcal{C}|$ refers to the class of objects in $\mathcal{C}$ .
$\blacksquare$

Let $\mathbb{C}\mathsf{lass}$ denote the large category whose objects are classes and whose morphisms are class functions. ³³3By contrast, a small category is one in which both the collection of objects and the collection of morphisms form sets, rather than proper classes.
$\blacksquare$

Assume a set $C$ and a cardinal $\alpha$ . Let $\mathcal{P}_{\alpha}(C)\coloneqq\{C_{1}\subseteq C\mid\mathsf{card}(C_{1})<\alpha\}$ , the set of all subsets of $C$ of cardinality strictly less than $\alpha$ . We write $C_{1}\subseteq_{\alpha}C$ if $C_{1}\in\mathcal{P}_{\alpha}(C)$ .

Presentations.

Let $\Sigma$ be a signature, and assume a class of $\Sigma$ -models $\mathbb{M}$ and a set of $\Sigma$ -sentences $\Phi$ .

$\blacksquare$

We write $\mathbb{M}\models\Phi$ if $\mathfrak{A}\models\Phi$ for all models $\mathfrak{A}\in\mathbb{M}$ .
$\blacksquare$

Let $\mathbb{M}^{\bullet}=\{\varphi\in\mathsf{Sen}(\Sigma)\mid\mathbb{M}\models\Phi\}$ , the set of sentences satisfied by all models in $\mathbb{M}$ .
$\blacksquare$

Let $\Phi^{\bullet}=\{\mathfrak{A}\in|\mathsf{Mod}(\Sigma)|\mid\mathfrak{A}\models\Phi\}$ , the class of models which satisfy $\Phi$ .
$\blacksquare$

Let $\mathsf{Mod}(\Sigma,\Phi)$ be the full subcategory of $\mathsf{Mod}(\Sigma)$ of models which satisfy $\Phi$ .

A presentation is a pair $(\Sigma,\Phi)$ consisting of a signature $\Sigma$ and a set of $\Sigma$ -sentences $\Phi$ . A theory is a presentation $(\Sigma,\Phi)$ such that $\Phi=\Phi^{\bullet\bullet}$ . A presentation morphism $\chi:(\Sigma,\Phi)\to(\Sigma^{\prime},\Phi^{\prime})$ consist of a signature morphism $\chi:\Sigma\to\Sigma^{\prime}$ such that $\Phi^{\prime}\models_{\Sigma^{\prime}}\chi(\Phi)$ . A theory morphism is a presentation morphism between theories.

Substitutions.

Let $\Sigma$ be a signature, $C_{1}$ and $C_{2}$ two $S$ -sorted sets of new constants for $\Sigma$ . A substitution $\theta:C_{1}\to C_{2}$ over $\Sigma$ is a mapping from $C_{1}$ to $T_{\Sigma}(C_{2})$ . As in case of signature morphisms, a substitution $\theta:C_{1}\to C_{2}$ determines

$\blacksquare$

a sentence functor $\mathsf{Sen}(\theta):\mathsf{Sen}(\Sigma[C_{1}])\to\mathsf{Sen}(\Sigma[C_{2}])$ , which preserves $\Sigma$ and maps each constant $c\in C_{1}$ to a term $\theta(c)$ , and
$\blacksquare$

a reduct functor $\mathord{\upharpoonright}_{\theta}:\mathsf{Mod}(\Sigma[C_{2}])\to\mathsf{Mod}(% \Sigma[C_{1}])$ , which preserves the interpretation of $\Sigma$ and assigns to each constant $c\in C_{1}$ the interpretation of the term $\theta(c)\in T_{\Sigma}(C_{2})$ in the category $\mathsf{Mod}(\Sigma[C_{2}])$ , that is, for all $\mathfrak{A}\in|\mathsf{Mod}(\Sigma[C_{2}])|$ we have (a) $(\mathfrak{A}\mathord{\upharpoonright}_{\theta})_{s}=\mathfrak{A}_{s}$ for all sorts $s$ in $\Sigma$ , (b) $x^{(\mathfrak{A}\mathord{\upharpoonright}_{\theta})}=x^{\mathfrak{A}}$ for all function or transition symbols $x$ in $\Sigma$ , and (c) $c^{(\mathfrak{A}\mathord{\upharpoonright}_{\theta})}=\theta(c)^{\mathfrak{A}}$ for all constants $c\in C_{1}$ .

As in the case of signature morphisms, we use $\theta$ to denote both the substitution $\theta:C_{1}\to C_{2}$ and the functor $\mathsf{Sen}(\theta):\mathsf{Sen}(\Sigma[C_{1}])\to\mathsf{Sen}(\Sigma[C_{2}])$ . The following result is a straightforward generalization of [7, Proposition 5.6].

Proposition 5 (Satisfaction condition for substitutions).

For all substitutions $\theta:C_{1}\to C_{2}$ , all $\Sigma[C_{2}]$ -models $\mathfrak{A}$ and all $\Sigma[C_{1}]$ -sentences $\phi$ we have: $\mathfrak{A}\mathord{\upharpoonright}_{\theta}\models\phi\quad\text{iff}\quad% \mathfrak{A}\models\theta(\phi)$ .

A reachable (transition) algebra [26] defined over a signature $\Sigma$ is a (transition) $\Sigma$ -algebra $\mathfrak{A}$ such that the unique homomorphism $h:T_{\Sigma}\to\mathfrak{A}$ is surjective. By [17, Proposition 8], a $\Sigma$ -algebra $\mathfrak{A}$ is reachable iff for all sets of new constants $C$ for $\Sigma$ and all expansions $\mathfrak{B}$ of $\mathfrak{A}$ to $\Sigma[C]$ , there exists a substitution $\theta:C\to\emptyset$ such that $\mathfrak{A}\mathord{\upharpoonright}_{\theta}=\mathfrak{B}$ .

4 Compactness and Upward Löwenheim-Skolem Property

${\mathsf{TA}}$ is very expressive and its sentences can control the cardinality of all its models under the the following assumptions:

$\blacksquare$

Generalized Continuum Hypothesis (GCH) holds, that is, for any infinite cardinal number $\alpha$ , the next larger cardinal is exactly $2^{\alpha}$ ; and
$\blacksquare$

there are no inaccessible cardinals ( $\neg\mathrm{IC}$ ).

Theorem 6 (Categoricity).

Assume that $\mathcal{L}={\mathsf{TA}}$ . Let $\mathfrak{A}$ be a model defined over a signature $\Sigma=(S,F,L)$ . There exists a sort preserving inclusion of signatures $\iota^{\circ}:\Sigma\hookrightarrow\Sigma^{\circ}$ and a reachable $\iota^{\circ}$ -expansion $\mathfrak{A}^{\circ}$ of $\mathfrak{A}$ such that any model of $(\Sigma^{\circ},Th(\mathfrak{A}^{\circ}))$ is isomorphic to $\mathfrak{A}^{\circ}$ , where $Th(\mathfrak{A}^{\circ})=\{\phi\in\mathsf{Sen}(\Sigma^{\circ})\mid\mathfrak{A}% ^{\circ}\models\phi\}$ .

Theorem 6 is proven assuming $\mathrm{ZFC}+\mathrm{GCH}+\neg\mathrm{IC}$ . These axioms are consistent relative to $\mathrm{ZFC}$ – that is, if $\mathrm{ZFC}$ is consistent, then so is the extended theory. Consequently, Theorem 6 (and its conclusion) cannot be refuted within $\mathrm{ZFC}$ . This illustrates that certain logical properties cannot be established within ${\mathsf{TA}}$ from ZFC alone. The following example shows that joint Robinson consistency property fails in ${\mathsf{TA}}$ .

Example 7 (Robinson Consistency).

Consider a complete (first-order) theory $(\Sigma,T)$ with at least two non-isomorphic models $\mathfrak{A}$ and $\mathfrak{B}$ . Construct a pushout as illustrated on the left side of the diagram below.

Since $\mathfrak{A}\models T$ and $\mathfrak{A}^{\circ}\mathord{\upharpoonright}_{\Sigma}=\mathfrak{A}$ , we have $T\subseteq Th(\mathfrak{A}^{\circ})$ . Similarly, since $\mathfrak{B}\models T$ and $\mathfrak{B}^{\circ}\mathord{\upharpoonright}_{\Sigma}=\mathfrak{B}$ , we have $T\subseteq Th(\mathfrak{B}^{\circ})$ . However, $\chi_{1}(Th(\mathfrak{A}^{\circ}))\cup\chi_{2}(Th(\mathfrak{B}^{\circ}))$ is not consistent, because any model of $\chi_{1}(Th(\mathfrak{A}^{\circ}))\cup\chi_{2}(Th(\mathfrak{B}^{\circ}))$ , by Theorem 6, would imply that $\mathfrak{A}$ is isomorphic to $\mathfrak{B}$ .

Typically, the cardinality of a model $\mathcal{A}$ over a signature $\Sigma=(S,F,L)$ is defined as the sum of the cardinalities of its carrier sets, that is, $\mathsf{card}(\mathfrak{A})=\sum_{s\in S}\mathsf{card}(\mathfrak{A}_{s})$ . The following example illustrates that the classical Upward Löwenheim-Skolem (ULS) property does not hold when sorts are treated as unary predicates rather than as distinct domains.

Example 8.

Let $\Sigma$ be a signature with countably infinitely many sorts $\{s_{n}\}_{n<\omega}$ , where each sort $s_{n}$ has exactly one constant symbol $c_{n}:\to s_{n}$ , and there are no transition labels. Define the set of equations $\Gamma\coloneqq\{\forall x_{n}\,{\cdot}\,(x_{n}=c_{n})\mid n<\omega\}$ , which asserts that each sort $s_{n}$ contains exactly one element.

Note that $\Sigma$ is a first-order signature, and $\Gamma$ is a set of $\Sigma$ -sentences that has an infinite model. However, $\Gamma$ has no models of cardinality greater than $\omega$ , indicating that the ULS property, as traditionally stated, fails to apply in this setting. The following definition of the ULS property applies to many-sorted first-order logic.

Definition 9 (Upward Löwenheim-Skolem Property).

$\alpha$ -Upward Löwenheim-Skolem property holds for an infinite cardinal $\alpha$ whenever for all signatures $\Sigma=(S,F,L)$ , all $\Sigma$ -models $\mathfrak{A}$ and all sorts $s\in S$ such that $\alpha\geq\mathsf{card}(\mathsf{Sen}(\Sigma))$ and $\alpha\geq\mathsf{card}(\mathfrak{A}_{s})\geq\omega$ there exists an elementary extension $\mathfrak{B}$ of $\mathfrak{A}$ such that $\mathsf{card}(\mathfrak{B}_{s})=\alpha$ .

Recall that $\alpha$ -compactness holds whenever for all signatures $\Sigma$ and all sets of $\Sigma$ -sentences $\Phi$ , $\Phi$ has a model iff all subsets $\Psi\in\mathcal{P}_{\alpha}(\Phi)$ have a model. From Theorem 6, one can show that both ULS property and compactness fail.

Corollary 10.

Assume that $\mathcal{L}={\mathsf{TA}}$ . Then (a) $\alpha$ -ULS fails for all cardinals $\alpha>\omega$ , and (b) $\alpha$ -compactness fails for all infinite cardinals $\alpha$ .

Corollary 10 shows that the iteration operator for actions provides enough expressive power to control the cardinality of models. Moreover, compactness fails in all its forms. In this setting, we aim to develop a model construction method that does not rely on compactness, yet still supports the proof of logical properties such as Downward Löwenheim-Skolem (DLS) theorem and OTT. It is worth noting that the results presented in the following sections hold without assuming either GCH or $\lnot\mathrm{IC}$ .

5 Forcing

In this section, we present a forcing technique, originally proposed in [19], which extends classical forcing from one signature to a category of signatures in a non-trivial way. To illustrate the motivation behind our approach, we recall Example 28 from [19].

Example 11.

Let $\Sigma$ be a signature defined as follows: (a) $S\coloneqq\{s_{i}\mid i\in\omega\}$ , (b) $F\coloneqq\{c:\to s_{0},d:\to s_{0}\}$ , and (c) $L\coloneqq\{\lambda\}$ . Let $\Phi$ be a set of $\Sigma$ -sentences which consists of: (a) $\lambda^{*}(c,d)$ , and (b) $(\exists x_{n}\,{\cdot}\,\top)\Rightarrow\neg\lambda^{n}(c,d)$ for all $n\in\omega$ , where $x_{n}$ is a variable of sort $s_{n}$ .

The first sentence asserts that there is a transition from $c$ to $d$ in a finite number of steps. For each natural number $n$ , the sentence $(\exists x_{n}\,{\cdot}\,\top)\Rightarrow\neg\lambda^{n}(c,d)$ states that if the sort $s_{n}$ is not empty then there is no transition from $c$ to $d$ in exactly $n$ steps. Classical model construction techniques typically involve introducing an infinite number of constants for each sort – commonly referred to as Henkin constants – followed by the application of quantifier elimination methods that select witnesses for existentially quantified variables. Let $C=\{C_{s_{n}}\}_{n<\omega}$ be a collection of Henkin constants, that is, newly introduced constants such that each $C_{s_{n}}$ is countably infinite for all $n<\omega$ . Although the original theory $(\Sigma,\Phi)$ is satisfiable, its extension $(\Sigma[C],\Phi)$ becomes unsatisfiable upon the addition of these constants. This discrepancy highlights the limitations of classical approaches and motivates the need for a novel method to handle the introduction of Henkin constants effectively.

Definition 12 (Forcing property).

A forcing property is a tuple $\mathbb{P}=(P,\leq,\Delta,f)$ , where:

1.

$(P,\leq)$ is a partially ordered set with a least element $0$ .

The elements of $P$ are traditionally called conditions.
2.

$\Delta:(P,\leq)\to\mathsf{Sig}$ is a functor, which maps each arrow $(p\leq q)\in(P,\leq)$ to an inclusion $\Delta(p)\subseteq\Delta(q)$ .
3.

$f:(P,\leq)\to\mathbb{S}\mathsf{et}$ is a functor from the small category $(P,\leq)$ to the category of sets $\mathbb{S}\mathsf{et}$ such that $f\subseteq\Delta;\mathsf{Sen}_{0}$ is a natural transformation, that is: (a) $f(p)\subseteq\mathsf{Sen}_{0}(\Delta(p))$ for all conditions $p\in P$ , and (b) $f(p)\subseteq f(q)$ for all relations $(p\leq q)\in(P,\leq)$ .
4.

If $f(p)\models\phi$ then $\phi\in f(q)$ for some $q\geq p$ , for all atomic sentences $\phi\in\mathsf{Sen}_{0}(\Delta(p))$ .

A classical forcing property is a particular case of forcing property such that $\Delta(p)=\Delta(q)$ for all conditions $p,q\in P$ . As usual, forcing properties determine suitable relations between conditions and sentences.

Definition 13 (Forcing relation).

Let $\mathbb{P}=\langle P,\leq,\Delta,f\rangle$ be a forcing property. The forcing relation $\Vdash$ between conditions $p\in P$ and sentences from $\mathsf{Sen}(\Delta(p))$ is defined by induction on the structure of sentences, as follows:

$\blacksquare$

$p\Vdash\varphi$ if $\varphi\in f(p)$ , for all atomic sentences $\varphi\in\mathsf{Sen}_{0}(\Delta(p))$ .
$\blacksquare$

$p\Vdash(\mathfrak{a}_{1}\mathbin{\mathchoice{\raisebox{-1.94444pt}{\leavevmode% \resizebox{6.11111pt}{6.24998pt}{\hbox{\raisebox{1.94444pt}{$\displaystyle% \hbox{ ;}$}}}}}{\raisebox{-1.94444pt}{\leavevmode\resizebox{6.11111pt}{6.24998% pt}{\hbox{\raisebox{1.94444pt}{$\textstyle\hbox{ ;}$}}}}}{\raisebox{-1.3611pt}% {\leavevmode\resizebox{4.95836pt}{4.37498pt}{\hbox{\raisebox{1.3611pt}{$% \scriptstyle\hbox{ ;}$}}}}}{\raisebox{-0.97221pt}{\leavevmode\resizebox{4.3750% 6pt}{3.12498pt}{\hbox{\raisebox{0.97221pt}{$\scriptscriptstyle\hbox{ ;}$}}}}}}% \mathfrak{a}_{2})(t_{1},t_{2})$ if $p\Vdash\mathfrak{a}_{1}(t_{1},t)$ and $p\Vdash\mathfrak{a}_{2}(t,t_{2})$ for some $t\in T_{\Delta(p)}$ .
$\blacksquare$

$p\Vdash(\mathfrak{a}_{1}\cup\mathfrak{a}_{2})(t_{1},t_{2})$ if $p\Vdash\mathfrak{a}_{1}(t_{1},t_{2})$ or $p\Vdash\mathfrak{a}_{2}(t_{1},t_{2})$ .
$\blacksquare$

$p\Vdash\mathfrak{a}^{*}(t_{1},t_{2})$ if $p\Vdash\mathfrak{a}^{n}(t_{1},t_{2})$ for some natural number $n<\omega$ .
$\blacksquare$

$p\Vdash\neg\phi$ if there is no $q\geq p$ such that $q\Vdash\phi$ .
$\blacksquare$

$p\Vdash\vee\Phi$ if $p\Vdash\phi$ for some $\phi\in\Phi$ .
$\blacksquare$

$p\Vdash\exists X\,{\cdot}\,\phi$ if $p\Vdash\theta(\phi)$ for some substitution $\theta:X\to T_{\Delta(p)}$ .

The relation $p\Vdash\phi$ in $\mathbb{P}$ , is read as $p$ forces $\phi$ .

A few basic properties of forcing are presented below.

Lemma 14 (Forcing properties [19]).

Let $\mathbb{P}=(P,\leq,\Delta,f)$ be a forcing property. For all conditions $p\in P$ and all sentences $\phi\in\mathsf{Sen}(\Delta(p))$ we have:

1.

$p\Vdash\neg\neg\phi$ iff for each $q\geq p$ there is a condition $r\geq q$ such that $r\Vdash\phi$ .
2.

If $p\leq q$ and $p\Vdash\phi$ then $q\Vdash\phi$ .
3.

If $p\Vdash\phi$ then $p\Vdash\neg\neg\phi$ .
4.

We can not have both $p\Vdash\phi$ and $p\Vdash\neg\phi$ .

The second property stated in the above lemma shows that the forcing relation is preserved along inclusions of conditions. The fourth property shows that the forcing relation is consistent, that is, a condition cannot force all sentences. The remaining conditions are about negation.

Definition 15 (Generic set).

Let $\mathbb{P}=(P,\leq,\Delta,f)$ be a forcing property. A non-empty subset of conditions $G\subseteq P$ is generic if

1.

$G$ is an ideal, that is: (a) $G\neq\emptyset$ , (b) for all $p\in G$ and all $q\leq p$ we have $q\in G$ , and (c) for all $p,q\in G$ there exists $r\in G$ such that $p\leq r$ and $q\leq r$ ; and
2.

for all conditions $p\in G$ and all sentences $\phi\in\mathsf{Sen}(\Delta(p))$ there exists a condition $q\in G$ such that $q\geq p$ and either $q\Vdash\phi$ or $q\Vdash\neg\phi$ holds.

We write $G\Vdash\phi$ if $p\Vdash\phi$ for some $p\in G$ .

A generic set $G$ describes a reachable model which satisfies all sentences forced by the conditions in $G$ .

$\blacktriangleright$ Remark 16.

Since $\Delta:(G,\leq)\to\mathsf{Sig}$ is a directed diagram of signature inclusions, one can construct a co-limit $\mu:\Delta\Rightarrow\Delta_{G}$ of the functor $\Delta:(G,\leq)\to\mathsf{Sig}$ such that $\mu_{p}:\Delta(p)\to\Delta_{G}$ is an inclusion for all $p\in G$ . ⁴⁴4Note that $\Delta_{G}$ refers both to the vertex of the colimit of the diagram $\Delta$ , and the constant functor from the poset $(G,\leq)$ to the category $\mathsf{Sig}$ , which maps every object in $G$ to the signature $\Delta_{G}$ .

The results which leads to DLS and OTT are developed over a signature $\Delta_{G}$ such as the one described in Remark 16.

Definition 17 (Generic model).

Let $\mathbb{P}=(P,\leq,\Delta,f)$ be a forcing property and $G\subseteq P$ a generic set. A model $\mathfrak{A}$ defined over $\Delta_{G}$ is a generic model for $G$ iff for every sentence $\phi\in\bigcup_{p\in G}\mathsf{Sen}(\Delta(p))$ , we have $\mathfrak{A}\models\phi\mbox{ iff }G\Vdash\phi$ .

The notion of generic model is the semantic counterpart of the definition of generic set. The following result shows that every generic set has a generic model.

Theorem 18 (Generic Model Theorem [19]).

Let $\mathbb{P}=(P,\leq,\Delta,f)$ be a forcing property and $G\subseteq P$ a generic set. Then there is a generic model $\mathfrak{A}$ for $G$ which is reachable.

6 Semantic Forcing

As an example of forcing property, we introduce semantic forcing and study its properties. Let us fix an arbitrary signature $\Sigma$ and let $\alpha\coloneqq\mathsf{card}(\mathsf{Sen}(\Sigma))$ be the power of $\Sigma$ . Consider an $\mathcal{S}$ -sorted set of new constants $C=\{C_{s}\}_{s\in S}$ such that $\mathsf{card}(C_{s})=\alpha$ for all sorts $s\in S$ . These constants, traditionally known as Henkin constants, are used in the construction of models. Throughout this section we assume the following:

1.

a partially ordered set $(\mathcal{K},\preceq)$ with a least element $0_{\mathcal{K}}$ ;
2.

a signature functor $\Omega:(\mathcal{K},\preceq)\to\mathsf{Sig}$ which maps (a) $0_{\mathcal{K}}$ to $\Sigma$ , (b) each element $\kappa\in\mathcal{K}$ to a signature $\Sigma[C_{\kappa}]$ , where $C_{\kappa}$ is a subset of $C$ with cardinality strictly less than $\alpha$ , that is, $C_{\kappa}\in\mathcal{P}_{\alpha}(C)$ , and (c) each relation $(\kappa\preceq\ell)\in(\mathcal{K},\preceq)$ to an inclusion of signatures $\Sigma[C_{\kappa}]\subseteq\Sigma[C_{\ell}]$ ;
3.
a model functor $\mathcal{M}:(\mathcal{K},\preceq)\to\mathbb{C}\mathsf{lass}^{op}$ such that the following hold: ⁵⁵5 $\mathbb{C}\mathsf{lass}^{op}$ is the opposite category of $\mathbb{C}\mathsf{lass}$ , which means: (a) it has the same objects as $\mathbb{C}\mathsf{lass}$ , that is, classes, but (b) morphisms are reversed, that is, a morphism $f:A\to B$ in $\mathbb{C}\mathsf{lass}^{op}$ corresponds to a class function $f:B\to A$ in $\mathbb{C}\mathsf{lass}$ .
1. (a)
  
  $\mathcal{M}\subseteq\Omega\mathbin{\mathchoice{\raisebox{-1.94444pt}{% \leavevmode\resizebox{6.11111pt}{6.24998pt}{\hbox{\raisebox{1.94444pt}{$% \displaystyle\hbox{ ;}$}}}}}{\raisebox{-1.94444pt}{\leavevmode\resizebox{6.111% 11pt}{6.24998pt}{\hbox{\raisebox{1.94444pt}{$\textstyle\hbox{ ;}$}}}}}{% \raisebox{-1.3611pt}{\leavevmode\resizebox{4.95836pt}{4.37498pt}{\hbox{% \raisebox{1.3611pt}{$\scriptstyle\hbox{ ;}$}}}}}{\raisebox{-0.97221pt}{% \leavevmode\resizebox{4.37506pt}{3.12498pt}{\hbox{\raisebox{0.97221pt}{$% \scriptscriptstyle\hbox{ ;}$}}}}}}|\mathsf{Mod}|$ is a natural transformation, that is, (a) $\mathcal{M}(\kappa)\subseteq|\mathsf{Mod}(\Omega(\kappa))|$ for all elements $\kappa\in\mathcal{K}$ , and (b) $\mathcal{M}(\ell)\mathord{\upharpoonright}_{\Omega(\kappa)}\subseteq\mathcal{M% }(\kappa)$ for all relations $(\kappa\preceq\ell)\in(\mathcal{K},\preceq)$ ;
2. (b)
  
  Assume an element $\kappa\in\mathcal{K}$ , a model $\mathfrak{A}\in\mathcal{M}(\kappa)$ and a set of constants $C_{1}\subseteq_{\alpha}C\setminus C_{\kappa}$ . For all expansions $\mathfrak{B}$ of $\mathfrak{A}$ to $\Sigma[C_{\kappa}\cup C_{1}]$ , there exists $\ell\succeq\kappa$ such that $C_{\ell}=C_{\kappa}\cup C_{1}$ and $\mathfrak{B}\in\mathcal{M}(\ell)$ .

The condition 3 (b) implies that all sets of constants from $\mathcal{P}_{\alpha}(C)$ appear in some signature from the image of $\Omega$ .

Example 19.

Let $\mathfrak{A}$ be a model defined over a signature $\Sigma$ .

1.

$\mathcal{K}=\{(\Sigma[C^{\prime}],\mathfrak{A}^{\prime})\mid C^{\prime}\in% \mathcal{P}_{\alpha}(C)\text{ and }\mathfrak{A}^{\prime}\in|\mathsf{Mod}(% \Sigma[C^{\prime}])|\text{ such that }\mathfrak{A}^{\prime}\mathord{% \upharpoonright}_{\Sigma}=\mathfrak{A}\}$ , and

$(\Sigma[C^{\prime}],\mathfrak{A}^{\prime})\preceq(\Sigma[C^{\prime\prime}],% \mathfrak{A}^{\prime\prime})$ iff $C^{\prime}\subseteq C^{\prime\prime}$ and $\mathfrak{A}^{\prime\prime}\mathord{\upharpoonright}_{\Sigma[C^{\prime}]}=% \mathfrak{A}^{\prime}$ ;
2.

$\Omega:(\mathcal{K},\preceq)\to\mathsf{Sig}$ is the forgetful functor mapping each $(\Sigma[C^{\prime}],\mathfrak{A}^{\prime})$ to $\Sigma[C^{\prime}]$ ;
3.

$\mathcal{M}:(\mathcal{K},\preceq)\to\mathbb{C}\mathsf{lass}^{op}$ is the model functor which maps each $(\Sigma[C^{\prime}],\mathfrak{A}^{\prime})\in\mathcal{K}$ to $\{\mathfrak{A}^{\prime}\}$ .

Example 19 shows that $(\mathcal{K},\preceq)$ can have a more complex structure than $(\mathcal{P}_{\alpha}(C),\subseteq)$ .

Example 20.

Let $\Phi$ be any set of sentences defined over a signature $\Sigma$ .

1.

$\mathcal{K}=\{(\Sigma[C^{\prime}],\Phi)\mid C^{\prime}\in\mathcal{P}_{\alpha}(% C)\}$ , and $(\Sigma[C^{\prime}],\Phi)\preceq(\Sigma[C^{\prime\prime}],\Phi)$ iff $C^{\prime}\subseteq C^{\prime\prime}$ ;
2.

$\Omega:(\mathcal{K},\preceq)\to\mathsf{Sig}$ is the forgetful functor mapping each $(\Sigma[C^{\prime}],\Phi)$ to $\Sigma[C^{\prime}]$ ;
3.

$\mathcal{M}:(\mathcal{K},\preceq)\to\mathbb{C}\mathsf{lass}^{op}$ is the functor which maps each $(\Sigma[C^{\prime}],\Phi)\in\mathcal{K}$ to $|\mathsf{Mod}(\Sigma[C^{\prime}],\Phi)|$ , the class of $\Sigma[C^{\prime}]$ -models which satisfy $\Phi$ .

Definition 21 (Semantic Forcing Property).

The semantic forcing property $\mathbb{P}(\Omega,\mathcal{M})=(P,\leq,\Delta,f)$ is defined as follows:

1.

A condition $p$ is a pair $(\kappa_{p},\Phi_{p})$ , where $\kappa_{p}\in\mathcal{K}$ and $\Phi_{p}\subseteq_{\alpha}\mathsf{Sen}(\Omega(\kappa_{p}))$ such that $\mathcal{M}(\kappa_{p})\cap\Phi_{p}^{\bullet}\neq\emptyset$ , that is, there exists at least one model in $\mathcal{M}(\kappa_{p})$ which satisfies $\Phi_{p}$ .
2.

$p\leq q$ iff $\kappa_{p}\preceq\kappa_{q}$ and $\Phi_{p}\subseteq\Phi_{q}$ , for all conditions $p=(\kappa_{p},\Phi_{p}),q=(\kappa_{q},\Phi_{q})\in P$ .
3.

$\Delta:(P,\leq)\to\mathsf{Sig}$ is the functor mapping each condition $p=(\kappa_{p},\Phi_{p})\in P$ to $\Omega(\kappa_{p})\in|\mathsf{Sig}|$ .
4.

Let $f(p)=\mathsf{Sen}_{0}(\Omega(\kappa_{p}))\cap(\mathcal{M}(\kappa_{p})\cap\Phi_% {p}^{\bullet})^{\bullet}$ , for all conditions $p\in P$ . In other words, $f(p)$ is the set of atomic sentences satisfied by all models of $\Phi_{p}$ from $\mathcal{M}(\kappa_{p})$ .

From a category theory perspective, several observations are worth noting.

$\blacktriangleright$ Remark 22.

Definition 21 describe the following mathematical structures:

$\blacksquare$

$\Lambda:(P,\leq)\to(\mathcal{K},\prec)$ , defined by $\Lambda(p)=\kappa_{p}$ for all $p\in P$ , is a monotone function such that $\Delta=\Lambda\mathbin{\mathchoice{\raisebox{-1.94444pt}{\leavevmode\resizebox% {6.11111pt}{6.24998pt}{\hbox{\raisebox{1.94444pt}{$\displaystyle\hbox{ ;}$}}}}% }{\raisebox{-1.94444pt}{\leavevmode\resizebox{6.11111pt}{6.24998pt}{\hbox{% \raisebox{1.94444pt}{$\textstyle\hbox{ ;}$}}}}}{\raisebox{-1.3611pt}{% \leavevmode\resizebox{4.95836pt}{4.37498pt}{\hbox{\raisebox{1.3611pt}{$% \scriptstyle\hbox{ ;}$}}}}}{\raisebox{-0.97221pt}{\leavevmode\resizebox{4.3750% 6pt}{3.12498pt}{\hbox{\raisebox{0.97221pt}{$\scriptscriptstyle\hbox{ ;}$}}}}}}\Omega$ .
$\blacksquare$
$\Gamma:(P,\leq)\to\mathbb{S}\mathsf{et}$ , defined by $\Gamma(p)=\Phi_{p}$ for all $p\in P$ , is a functor such that the inclusion $\subseteq\leavevmode\nobreak\ :\Gamma\Rightarrow(\Lambda\mathbin{\mathchoice{% \raisebox{-1.94444pt}{\leavevmode\resizebox{6.11111pt}{6.24998pt}{\hbox{% \raisebox{1.94444pt}{$\displaystyle\hbox{ ;}$}}}}}{\raisebox{-1.94444pt}{% \leavevmode\resizebox{6.11111pt}{6.24998pt}{\hbox{\raisebox{1.94444pt}{$% \textstyle\hbox{ ;}$}}}}}{\raisebox{-1.3611pt}{\leavevmode\resizebox{4.95836pt% }{4.37498pt}{\hbox{\raisebox{1.3611pt}{$\scriptstyle\hbox{ ;}$}}}}}{\raisebox{% -0.97221pt}{\leavevmode\resizebox{4.37506pt}{3.12498pt}{\hbox{\raisebox{0.9722% 1pt}{$\scriptscriptstyle\hbox{ ;}$}}}}}}\Omega\mathbin{\mathchoice{\raisebox{-% 1.94444pt}{\leavevmode\resizebox{6.11111pt}{6.24998pt}{\hbox{\raisebox{1.94444% pt}{$\displaystyle\hbox{ ;}$}}}}}{\raisebox{-1.94444pt}{\leavevmode\resizebox{% 6.11111pt}{6.24998pt}{\hbox{\raisebox{1.94444pt}{$\textstyle\hbox{ ;}$}}}}}{% \raisebox{-1.3611pt}{\leavevmode\resizebox{4.95836pt}{4.37498pt}{\hbox{% \raisebox{1.3611pt}{$\scriptstyle\hbox{ ;}$}}}}}{\raisebox{-0.97221pt}{% \leavevmode\resizebox{4.37506pt}{3.12498pt}{\hbox{\raisebox{0.97221pt}{$% \scriptscriptstyle\hbox{ ;}$}}}}}}\mathsf{Sen})$ is a natural transformation, that is:
1. 1.
  
  $\Gamma(p)\subseteq\mathsf{Sen}(\Delta(p))$ for all conditions $p\in P$ , and
2. 2.
  
  $\Gamma(p)\subseteq\Gamma(q)$ for all relations $(p\leq q)\in(P,\leq)$ .

Let $p\in P$ be a condition.

1.

We let $\mathsf{Mod}(p)$ denote $\mathcal{M}(\Lambda(p))\cap\Gamma(p)^{\bullet}$ , the class of models in $\mathcal{M}(\Lambda(p))$ satisfying $\Gamma(p)$ .
2.

We write $p\models\phi$ iff $\phi$ is satisfied by all models in $\mathsf{Mod}(p)$ , in symbols, $\mathsf{Mod}(p)\models\phi$ .

The perspective of category theory can be disregarded if the reader is not familiar with it. However, Remark 22 lays the groundwork for a generalization to an abstract level, as defined by the notion of institution [11].

We define a notion of distance between conditions, which provides a principled method for regulating the addition of Henkin constants from $C$ to the starting signature $\Sigma$ .

Definition 23 (Distance & weak forcing).

The distance between two conditions $p$ and $q$ , with $p\leq q$ , is defined as the number of constants and sentences that must be added to $p$ to obtain $q$ , that is, $d(p,q):=\mathsf{card}(\Delta(q)\setminus\Delta(p))+\mathrm{card}(\Gamma(q)% \setminus\Gamma(p))$ . A condition $p$ weakly forces $\phi$ , in symbols, $p\Vdash^{w}\phi$ , if for all $q\geq p$ there exists $r\geq q$ such that $d(q,r)<\omega$ and $r\Vdash\phi$ .

Using Lemma 14 (2) and the reflexivity of $\leq$ , it is not difficult to show that $p\Vdash\phi$ implies $p\Vdash^{w}\phi$ . In the classical setting, weak forcing does not involve any notion of distance: $p\Vdash^{w}\phi$ if and only if, for all $q\geq p$ , there exists $r\geq q$ such that $r\Vdash\phi$ ; and this, in turn, holds if and only if $p\Vdash\neg\neg\phi$ . The notion of distance is introduced in this paper to extend the applicability of the results to all signatures – including those of singular cardinality – by controlling the number of constants introduced during the construction of the generic sets.

Theorem 24 (Semantic Forcing Theorem).

For all conditions $p\in P$ and all sentences $\phi\in\mathsf{Sen}(\Delta(p))$ , we have: (a) $p\models\phi$ iff (b) $p\Vdash^{w}\phi$

7 Downward Löwenheim-Skolem Theorem

Consider a semantic forcing property $\mathbb{P}(\Omega,\mathcal{M})$ such that the functors $\Omega$ and $\mathcal{M}$ are defined as in Example 19. We use $\mathbb{P}(\Omega,\mathcal{M})$ to give a proof of Downward Löwenheim-Skolem Theorem. The key to proving any result based on forcing is the construction of a generic set for a given condition $p$ .

Lemma 25 (Existence).

Let $\mathbb{P}(\Omega,\mathcal{M})=(P,\leq,\Delta,f)$ be a semantic forcing property such that the functors $\Omega$ and $\mathcal{M}$ are defined as in Example 19. Any condition $p\in P$ belongs to a generic set $G_{p}$ .

Proof.

Let $pair:\alpha\times\alpha\to\alpha$ be any bijection such that for all ordinals $i,j,\beta<\alpha$ if $\beta=pair(i,j)$ then $i\leq\beta$ . For any condition $q\in P$ , let $\gamma(q):\alpha\to\mathsf{Sen}(\Delta(q))$ be an enumeration of the sentences in $\mathsf{Sen}(\Delta(q))$ .

First, we define an increasing chain of conditions $p_{0}\leq p_{1}\leq\ldots\leq p_{\beta}\leq\ldots$ with the following property: for all ordinals $\beta<\alpha$ there exists $n<\omega$ such that $d(p,p_{\beta})\leq n\cdot\mathrm{card}(\beta)$ .⁶⁶6When $\alpha$ is a singular cardinal, the entire set of constants $C$ may be used along a chain $\{p_{i}\}_{i<\beta}$ with $\beta<\alpha$ . To avoid this uncontrolled increase in the size, we use the distance measure $d$ . We proceed by induction on ordinals $\beta<\alpha$ .

( $\beta=0$ )

Let $p_{0}\coloneqq p$ .

( $\beta\Rightarrow\beta+1$ )

Let $(i,j)\coloneqq pair^{-1}(\beta)$ . Notice that $i\leq\beta$ , which means $p_{i}$ is already defined. Condition $p_{\beta+1}$ is obtained by adding a finite set of constants from $C$ and a finite set of sentences to $p_{\beta}$ , according to a case distinction detailed below:

( $q\Vdash\gamma(p_{i},j)$ for some $q\geq p_{\beta}$ ): Since $q\Vdash\gamma(p_{i},j)$ , by Theorem 24, $q\models\gamma(p_{i},j)$ . It follows that $r\coloneqq(\Lambda(p_{\beta}),\Gamma(p_{\beta})\cup\{\gamma(p_{i},j)\})\in P$ . Since $r\vDash\gamma(p_{i},j)$ , by Theorem 24, there exists $p_{\beta+1}\geq r$ such that $p_{\beta+1}\Vdash\gamma(p_{i},j)$ and $d(r,p_{\beta+1})<\omega$ . By induction hypothesis, there exists $n<\omega$ such that $d(p,p_{\beta+1})\leq n\cdot\mathsf{card}(\beta+1)$ .
( $q\not\Vdash\gamma(p_{i},j)$ for every $q\geq p_{\beta}$ ): Let $p_{\beta+1}\coloneqq p_{\beta}$ . In this case, $p_{\beta+1}\Vdash\neg\gamma(p_{i},j)$ .

( $\beta<\alpha$ is a limit ordinal)

At this point, for all $i<\beta$ we have defined $p_{i}=(\Lambda(p_{i}),\Gamma(p_{i}))$ , where $\Lambda(p_{i})=(\Delta(p_{i}),\mathfrak{A}_{i})$ and $\mathfrak{A}_{i}$ is an expansion of $\mathfrak{A}$ to $\Delta(p_{i})$ .

$\blacksquare$

Let $C_{\Lambda(p_{\beta})}\coloneqq\bigcup_{i<\beta}C_{\Lambda(p_{i})}$ and $\Delta(p_{\beta})=\Sigma[C_{\Lambda(p_{\beta})}]$ and $\Gamma(p_{\beta})\coloneqq\bigcup_{i<\beta}\Gamma(p_{i})$ . Since $\mathsf{card}(C_{\Lambda(p_{i})})\leq\mathsf{card}(\beta)$ for all $i<\beta$ , we get $\mathsf{card}(C_{\Lambda(p_{\beta})})\leq\mathsf{card}(\beta)<\alpha$ . Similarly, $\mathsf{card}(\Gamma(p_{\beta}))\leq\mathsf{card}(\beta)<\alpha$ .
$\blacksquare$

A model $\mathfrak{A}_{i}\in\mathcal{M}(\Lambda(p_{i}))$ , where $i<\beta$ , can be regarded as a pair $(\mathfrak{A},g_{i}:C_{\Lambda(p_{i})}\to\mathfrak{A})$ , consisting of the model $\mathfrak{A}$ and an interpretation of the constants in $C_{\Lambda(p_{i})}$ into the elements of $\mathfrak{A}$ given by the function $g_{i}$ . Define $g_{\beta}\coloneqq\bigcup_{i<\beta}g_{i}$ , let $\mathfrak{A}_{\beta}\coloneqq(\mathfrak{A},g_{\beta})$ and $\Lambda(p_{\beta})\coloneqq(\Delta(p_{\beta}),\mathfrak{A}_{\beta})$ .
$\blacksquare$

Let $p_{\beta}\coloneqq(\Lambda(p_{\beta}),\Gamma(p_{\beta}))$ . By its definition, $\mathfrak{A}_{\beta}\mathord{\upharpoonright}_{\Delta(p_{i})}=\mathfrak{A}_{i}$ for all $i<\beta$ . Since $\mathfrak{A}_{i}\models\Gamma(p_{i})$ for all $i<\beta$ , by satisfaction condition, $\mathfrak{A}_{\beta}\models\Gamma(p_{\beta})$ . Hence, $p_{\beta}$ is well-defined. Since for all $i<\beta$ there exists $n_{i}\in\mathbb{N}$ such that $d(p,p_{i})\leq n_{i}\cdot\mathsf{card}(i)$ , we get $d(p,p_{\beta})\leq\mathsf{card}(\beta)$ .

Secondly, one can easily show that $G_{p}\coloneqq\{q\in P\mid q\leq p_{\beta}\text{ for some }\beta<\alpha\}$ is a generic set. $\hfill\blacktriangleleft$

Theorem 26 (Downward Löwenheim-Skolem Theorem).

Let $\mathfrak{A}$ be a model over a signature $\Sigma=(S,F,L)$ of power $\alpha$ such that $\mathsf{card}(\mathfrak{A}_{s})\geq\alpha$ for some sort $s\in S$ . Then there exists an elementary submodel $\mathfrak{B}$ of $\mathfrak{A}$ such that $\mathsf{card}(\mathfrak{B}_{s})=\alpha$ .

8 Omitting Types Theorem

Consider a semantic forcing property $\mathbb{P}(\Omega,\mathcal{M})$ such that $\Omega$ and $\mathcal{M}$ are defined as in Example 20. We use $\mathbb{P}(\Omega,\mathcal{M})$ to give a proof of Omitting Types Theorem in ${\mathsf{TA}}$ .

Definition 27 (Types).

A type for a signature $\Sigma$ of power $\alpha$ is a set of sentences $T$ defined over $\Sigma[X]$ , where $X$ is a block of variables for $\Sigma$ such that $\alpha^{\mathsf{card}(X)}\leq\alpha$ . A $\Sigma$ -model $\mathfrak{A}$ realizes $T$ if $\mathfrak{B}\models T$ for some expansion $\mathfrak{B}$ of $\mathfrak{A}$ to $\Sigma[X]$ . $\mathfrak{A}$ omits $T$ if $\mathfrak{A}$ does not realize $T$ .

For all infinite cardinals $\alpha$ we have $\alpha<\alpha^{\mathrm{cf(\alpha)}}$ , where $\mathrm{cf}(\alpha)$ is the cofinality of $\alpha$ . Consequently, the condition $\alpha^{\mathsf{card}(X)}\leq\alpha$ implies that $\mathsf{card}(X)<\mathrm{cf}(\alpha)$ . The converse also holds under the assumption of GCH. The inequality $\alpha^{\mathsf{card}(X)}\leq\alpha$ ensures that the number of mappings from $X$ to the set of ground terms – that is, substitutions $\theta:X\to\emptyset$ – does not exceed $\alpha$ . Note that if $\alpha$ is the cardinality of real numbers and $X$ is countable then $\alpha^{\mathsf{card}(X)}\leq\alpha$ holds.

Definition 28 (Isolated types).

Let $\Sigma$ be a signature of power $\alpha$ . A set of sentences $\Phi\subseteq\mathsf{Sen}(\Sigma)$ is said to isolate a type $T\subseteq\mathsf{Sen}(\Sigma[X])$ iff there exist:

$\blacksquare$

an $S$ -sorted set of new constants $D$ for $\Sigma$ with $\mathsf{card}(D)<\alpha$ ,
$\blacksquare$

a set $\Gamma\subseteq\mathsf{Sen}(\Sigma[D])$ with $\mathsf{card}(\Gamma)<\alpha$ and such that $T\cup\Gamma$ is satisfiable over $\Sigma[D]$ , and
$\blacksquare$

a substitution $\theta:X\to D$ ,

such that $\Phi\cup\Gamma\models_{\Sigma[D]}\theta(T)$ . We say that $\Phi$ locally omits $T$ if $\Phi$ does not isolate $T$ .

Our definitions for type, realization, and isolation align with those provided in [16], with one key difference: we do not restrict the block of variables $X$ to be finite. Definition 28 is similar to the definition of locally omitting types for first-order logic without equality from [22]. If the fragment $\mathcal{L}$ of ${\mathsf{TA}}$ is closed under Boolean operators and first-order quantifiers, the above definition coincides with the classical one for isolated types.

Lemma 29.

Assume that (a) $\mathcal{L}$ is semantically closed under Boolean operators and first-order quantifiers, and (b) $\mathcal{L}$ is compact or $\alpha=\omega$ . Then $\Phi\subseteq\mathsf{Sen}(\Sigma)$ isolates a type $T\subseteq\mathsf{Sen}(\Sigma[X])$ iff there exists a set of sentences $\Gamma\in\mathcal{P}_{\alpha}(\mathsf{Sen}(\Sigma[X]))$ such that $T\cup\Gamma$ is satisfiable over $\Sigma[X]$ and $\Phi\cup\Gamma\models_{\Sigma[X]}T$ .

The proof is conceptually identical with the proof of [16, Lemma 45].

Definition 30 (Omitting Types Property).

Let $\alpha$ be an infinite cardinal. The fragment $\mathcal{L}$ has $\alpha$ -Omitting Types Property ( $\alpha$ -OTP) whenever

1.

for all signatures $\Sigma$ of power $\alpha$ ,
2.

all satisfiable sets of sentences $\Phi\subseteq\mathsf{Sen}(\Delta)$ , and
3.

all families of types $\{T_{i}\subseteq\mathsf{Sen}(\Sigma[X_{i}])\mid i<\alpha\}$ ,

such that $\Phi$ locally omits $T_{i}$ for all $i<\alpha$ , there exists a $\Sigma$ -model of $\Phi$ which omits $T_{i}$ for all $i<\alpha$ . If $\alpha=\omega$ then we say that $\mathcal{L}$ has OTP rather than $\mathcal{L}$ has $\omega$ -OTP.

Theorem 31 (Omitting Types Theorem).

Let $\Sigma$ be a signature of power $\alpha$ . If $\alpha>\omega$ then we assume that fragment $\mathcal{L}$ is compact. Then $\mathcal{L}$ has $\alpha$ -OTP.

Any fragment $\mathcal{L}$ obtained from ${\mathsf{TA}}$ by (a) discarding a subset of sentence or/and action operators, and (b) restricting the category of signatures – without prohibiting signature extensions with constants – has $\omega$ -OTP. Any star-free fragment $\mathcal{L}$ of ${\mathsf{TA}}$ is compact and therefore has $\alpha$ -OTP for all cardinals cardinal $\alpha\geq\omega$ . In particular, many-sorted first-order logic has $\alpha$ -OTP for all cardinals cardinal $\alpha\geq\omega$ .

Lemma 32.

Assume that $\mathcal{L}$ is closed under Boolean operators and first-order quantifiers. Let $\Sigma=(S,F)$ be a signature, where $S\coloneqq\{s_{n}\mid n>0\}$ and $F\coloneqq\emptyset$ .

$\blacksquare$

Let $\phi_{n}\coloneqq\exists z_{n}\,{\cdot}\,\top\Rightarrow\exists x_{1},\dots,x_% {n}\,{\cdot}\,\bigwedge_{i\neq j}x_{i}\neq x_{j}$ be a $\Sigma$ -sentence, where $n>0$ , where $z_{n}$ is a variable of sort $s_{n}$ , and $x_{1},\dots,x_{n}$ are variables of sort $s_{1}$ . Note that $\phi_{n}$ states that if there exists an element of sort $s_{n}$ then there exists at least $n$ elements of sort $s_{1}$ .
$\blacksquare$

Let $T\coloneqq\{\exists x_{1},\dots,x_{n}\,{\cdot}\,\bigwedge_{i\neq j}x_{i}\neq x% _{j}\land\bigwedge_{i=1}^{n}y\neq x_{i}\mid n>0\}$ be a type with one variable $y$ of sort $s_{1}$ , expressing that there are infinitely many elements of sort $s_{1}$ .

Then $\Phi\coloneqq\{\phi_{n}\mid n>0\}$ locally omits $T$ .

Let $\Sigma$ , $\Phi$ and $T$ be as defined in Lemma 32. Recall that the set of Henkin constants is $C=\{C_{s_{n}}\}_{n<\omega}$ , where $\mathsf{card}(C_{s_{n}})=\omega$ for all $n<\omega$ . Note that $(\Sigma,\Phi)$ is a satisfiable first-order presentation that does not involve the transitive closure operator $*$ , as it contains no relation symbols. By Lemma 32, $\Phi$ locally omits $T$ . By Theorem 31, there exists a model $\mathfrak{A}$ for $\Phi$ which omits $T$ . Since every model of $(\Sigma[C],\Phi)$ realizes $T$ , the model $\mathfrak{A}$ must be constructed over a proper subset of $C$ , in contrast to the classical first-order logic approach, where results are developed over the entire $\Sigma[C]$ . Consequently, the OTT as presented in [23, 3, 21, 14, 16] does not apply in this context.

Lemma 33.

Let $\Sigma=(S,F)$ be a signature such that $S\coloneqq\{s\}$ and $F\coloneqq\{c:\to s\mid c\in\mathbb{R}\}$ , where $\mathbb{R}$ denotes the set of real numbers. Let $T\coloneqq\{x_{i}\neq c\mid c:\to s\in F\text{ and }i<\omega\}$ be a type with a countably infinite number of variables from $X\coloneqq\{x_{i}\mid i<\omega\}$ . Then $\Phi$ locally omits $T$ , where $\Phi$ is any countable and satisfiable set of $\Sigma$ -sentences.

By Theorem 31, there exists a model $\mathfrak{A}$ of $\Phi$ which omits $T$ . Consequently, the number of elements in $\mathfrak{A}$ that are not denotations of real numbers – considered unwanted elements – is finite and may therefore be regarded as negligible. Lemma 33 demonstrates that types involving infinitely many variables are not difficult to construct and can naturally arise in applications.

9 $\omega$ -Completeness

Although a transition algebra may satisfy a given set of sentences, it may not be relevant to the intended semantics. In many cases, formal methods practitioners are interested in the properties of a restricted class of transition algebras, such as: (a) those reachable through a set of constructor operators, (b) those with a finite number of elements, or (c) those satisfying both conditions. Using Omitting Types Theorem we can extend the completeness result in [19] to fragments obtained from $\mathcal{L}$ by restricting the semantics to the aforementioned transition algebras. Concretely, given a sound and complete proof system for $\mathcal{L}$ , we introduce additional proof rules so that the resulting system remains sound and complete for fragments of $\mathcal{L}$ obtained by restricting the class of transition algebras to those of interest.

Definition 34 (Entailment relation).

An entailment relation is a family of binary relations between sets of sentences $\vdash=\{\vdash_{\Sigma}\}_{\Sigma\in|\mathsf{Sig}^{\mathcal{L}}|}$ with the following properties:

$(Monotonicity)\displaystyle\frac{\Phi_{1}\subseteq\Phi_{2}}{\Phi_{2}\vdash\Phi% _{1}}$	$(Transitivity)\displaystyle\frac{\Phi_{1}\vdash\Phi_{2}\leavevmode\nobreak\ % \leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode% \nobreak\ \Phi_{2}\vdash\Phi_{3}}{\Phi_{1}\vdash\Phi_{3}}$
$(Union)\displaystyle\frac{\Phi_{1}\vdash\varphi_{2}\text{ for all }\phi_{2}\in% \Phi_{2}}{\Phi_{1}\vdash\Phi_{2}}$	$(Translation)\displaystyle\frac{\Phi_{1}\vdash_{\Sigma}\Phi_{2}}{\chi(\Phi_{1}% )\vdash_{\Sigma^{\prime}}\chi(\Phi_{2})}$ where $\chi:\Sigma\to\Sigma^{\prime}$

An entailment relation $\vdash$ is sound (complete) if $\vdash\subseteq\models$ ( $\models\subseteq\vdash$ ).

Completeness fails when $\mathcal{L}$ is closed under $*$ and includes uncountable signatures [19, Proposition 15]. Therefore, throughout this section, we assume that the fragment $\mathcal{L}$ has only countable signatures if it is closed under $*$ . Additionally, we assume that $\mathcal{L}$ is semantically closed under Boolean operators.

Constructor-based algebras.

Many algebraic structures can be naturally described using a set of constructor operators. For instance, numbers can be defined using a constant $z e r o$ and a unary function symbol $s u c c$ , while lists can be defined using a constant $n i l$ and a binary function symbol $c o n s$ .

Definition 35 (Constructor-based algebras).

Let $\Sigma=(S,F,L)$ be a signature and $F^{c}\subseteq F$ a subset of constructor operators. We let $\Sigma^{c}$ denote the signature of constructors $(S,F^{c})$ . The constructors create a partition of the set of sorts $S$ .

1.

A sort $s\in S$ that has a constructor – i.e., there exists a constructor $(\sigma:w\to s)\in F^{c}$ – is called constrained. We denote the set of all constrained sorts by $S^{c}$ .
2.

A sort that is not constrained is called loose. We denote the set of all loose sorts by $S^{l}$ .

A constructor-based transition algebra $\mathfrak{A}$ is a transition algebra for which there exist (a) a set of loose variable $Y=\{Y_{s}\}_{s\in S^{l}}$ and (b) an expansion $\mathfrak{B}$ of $\mathfrak{A}$ to $\Sigma[Y]$ , such that $\mathfrak{B}\mathord{\upharpoonright}_{\Sigma^{c}[Y]}$ is reachable.

Example 36 (Lists).

Let $\Sigma=(S,F)$ be an algebraic signature such that (a) $S=\{Elt,List\}$ and (b) $F=\{empty:\to List,\_;\_:List\leavevmode\nobreak\ Elt\to List,add:List% \leavevmode\nobreak\ List\to List\}$ . Let $F^{c}=\{empty:\to List,\_;\_:List\leavevmode\nobreak\ Elt\to List\}$ be a set of constructors.

$\blacksquare$

$E l t$ is a loose sort while $L i s t$ is a constrained sort.
$\blacksquare$

Let $\mathfrak{A}$ be a constructor-based algebra obtained from $T_{\Sigma^{c}}(\omega)$ by interpreting $a d d$ as follows: (a) $add^{\mathfrak{A}}(\ell,empty)=\ell$ , and (b) $add^{\mathfrak{A}}(\ell,\ell^{\prime};n)=add^{\mathfrak{A}}(\ell,\ell^{\prime}% );n$ for all lists of natural numbers $\ell,\ell^{\prime}\in\mathfrak{A}_{List}$ and all natural numbers $n\in\mathfrak{A}_{Elt}$ .

By refining the syntax with a subset of constructor operators and restricting the semantics to constructor-based transition algebras, we obtain a new logic $\mathcal{L}^{c}$ from $\mathcal{L}$ . This restriction in semantics alters the satisfaction relation $\models$ between sets of sentences: $\Phi\models^{c}\phi$ means that all constructor-based transition algebras of $\Phi$ are models of $\phi$ . Consequently, there may exist non-restricted models of $\Phi$ that do not satisfy $\phi$ . In order to obtain an institution, we need to restrict the class of signature morphisms such that the reduct of a constructor-based algebra is again a constructor-based algebra [17, 13, 2]. So, the category of signatures of $\mathcal{L}^{c}$ has

1.

objects of the form $(S,F^{c}\subseteq F,L)$ , where $(S,F,L)$ is a signature in $\mathcal{L}$ , and
2.

signature morphisms of the form $\chi:(S,F^{c}\subseteq F,L)\to(S^{\prime},F^{\prime c}\subseteq F^{\prime},L^{% \prime})$ , where (a) $\chi:(S,F,L)\to(S^{\prime},F^{\prime},L^{\prime})$ is a signature morphism in $\mathcal{L}$ , (b) constructors are preserved, that is, $\chi(F^{c})\subseteq F^{\prime c}$ , and (c) constructors are reflected, that is, for all $\sigma^{\prime}:w^{\prime}\to\chi(s)\in F^{\prime c}$ there exists $\sigma:w\to s\in F^{c}$ such that $\chi(\sigma:w\to s)=\sigma^{\prime}:w^{\prime}\to\chi(s)$ .

Finite algebras.

Computer science applications often focus on properties that hold in finite structures. Therefore, we refine the fragment $\mathcal{L}^{c}$ defined above to include constructor-based transition algebras, where certain distinguished sorts are interpreted as finite sets. Let $\mathcal{L}^{f}$ be a fragment of $\mathcal{L}^{c}$ obtained by (a) refining the syntax with a subset of sorts of finite domains, and (b) by restricting constructor-based models such that the sorts for finite domains are interpreted as finite sets. This means that the category of signatures in $\mathcal{L}^{f}$ has

1.

objects of the form $(S^{f}\subseteq S,F^{c}\subseteq F,L)$ , where $(S,F^{c}\subseteq F,L)$ is a signature in $\mathcal{L}^{c}$ , and
2.

arrows of the form $\chi:(S^{f}\subseteq S,F^{c}\subseteq F,L)\to(S^{\prime f}\subseteq S^{\prime}% ,F^{\prime c}\subseteq F^{\prime},L^{\prime})$ such that (a) $\chi:(S,F^{c}\subseteq F,L)\to(S^{\prime},F^{\prime c}\subseteq F^{\prime},L^{% \prime})$ is a signature morphism in $\mathcal{L}^{c}$ , and (b) the finite sorts are preserved, that is, $\chi(S^{f})\subseteq S^{\prime f}$ .

Definition 37.

Let $\vdash$ be an entailment relation for $\mathcal{L}$ . The entailment relation $\vdash^{f}$ for $\mathcal{L}^{f}$ is the least entailment relation that includes $\vdash$ and it is closed under the following proof rules:

1.

$(CB)\leavevmode\nobreak\ \displaystyle\frac{\Phi\vdash^{f}\forall var(t)\,{% \cdot}\,\psi(t)\text{ for all }t\in T_{\Sigma^{c}}(Y)}{\Phi\vdash^{f}\forall x% \,{\cdot}\,\psi(x)}$ , where (a) $x$ is a variable of constrained sort, (b) $Y$ is a $S^{l}$ -sorted block of variables such that $\mathsf{card}(Y_{s})=\omega$ for all loose sorts $s\in S^{l}$ , and (c) $var(t)$ is the set of all variables occuring in $t$ .
2.
$(FN)\leavevmode\nobreak\ \displaystyle\frac{\Phi\cup\{\Gamma_{\overline{n}}\}% \vdash^{f}\psi\text{ for all }\overline{n}\in\omega^{\alpha}}{\Phi\vdash^{f}\psi}$ , where
1. (a)
  
  $\alpha\coloneqq\mathsf{card}(S^{f})$ and $\{s_{i}\}_{i<\alpha}$ is an enumeration of $S^{f}$ ,
2. (b)
  $\Gamma_{\overline{n}}$ denotes the set of sentences $\{\gamma_{s_{i},\overline{n}(i)}\mid i<\alpha\}$ for all tuples $\overline{n}\in\omega^{\alpha}$ , where
  - $\blacksquare$
    
    $\overline{n}(i)$ is the natural number in position $i$ from $\overline{n}$ , for all tuples $\overline{n}\in\omega^{\alpha}$ and all $i<\alpha$ ;
  - $\blacksquare$
    
    $\gamma_{s,n}$ denotes the sentence $\forall x_{1},\dots,x_{n+1}\,{\cdot}\,\lor_{i\neq j}x_{i}=x_{j}$ , for all natural numbers $n<\omega$ , all sorts $s\in S^{f}$ and all variables $x_{1},\dots,x_{n+1}$ of sort $s$ .
Note that $\gamma_{s,n}$ states that the sort $s$ has at most $n$ elements. If $n=0$ then $\gamma_{0,s}=\forall x_{1}\,{\cdot}\,\vee\emptyset$ , which is satisfied only by transition algebras whose carrier set for the sort $s$ is empty.

$(CB)$ asserts that to prove the property $\psi$ for an arbitrary element $x$ , it suffices to establish $\psi$ for all constructor terms $t$ in $T_{(S,F^{c})}(Y)$ . $(CB)$ should be disregarded if the base logic $\mathcal{L}$ is not closed under first-order quantification. $(FN)$ states that the number of elements of any sort in $S^{f}$ is finite. It is straightforward to show that $\vdash^{f}$ is sound for $\mathcal{L}^{f}$ provided that $\vdash$ is sound for $\mathcal{L}$ . Establishing completeness is generally more challenging, but it can be achieved with the help of the OTP.

Theorem 38 (Completeness).

The entailment relation $\vdash^{f}$ is complete for $\mathcal{L}^{f}$ if $\vdash$ is complete for $\mathcal{L}$ and $\mathcal{L}$ has OTP.

10 Conclusions

In this contribution, we focused on two main aspects of ${\mathsf{TA}}$ . First, we examined its model-theoretic properties, including the Löwenheim-Skolem and Omitting Types properties. Due to its increased expressivity, TA does not possess the Löwenheim-Skolem property. We then developed a semantic forcing property based on recent developments from [19], which enabled us to prove the Löwenheim-Skolem Theorem and the Omitting Types Theorem. Given that the full expressivity of ${\mathsf{TA}}$ is not required in many practical case studies, our study was conducted on a fragment of TA that restricts the syntax while preserving the semantics.

Secondly, we explored applications of the Omitting Types Theorem to formal methods. Software engineers often seek a restricted class of models for a given theory, such as constructor-based and/or finite models. We extended the system of proof rules proposed in [19] with new rules that are sound for these models of interest, ensuring that completeness is maintained. This approach provides sound and complete proof rules for fragments of TA obtained by restricting the syntax and/or the semantics.

An interesting future research direction involves developing specification and verification methodologies based on the proof rules we have defined for the fragments of ${\mathsf{TA}}$ . Additionally, we aim to propose a notion of Horn clauses for ${\mathsf{TA}}$ , which could make specifications defined in ${\mathsf{TA}}$ executable through rewriting or narrowing.

References

[1] Michel Bidoit and Rolf Hennicker. Constructor-based observational logic. J. Log. Algebraic Methods Program., 67(1-2):3–51, 2006. doi:10.1016/J.JLAP.2005.09.002.
[2] Michel Bidoit, Rolf Hennicker, and Alexander Kurz. Observational logic, constructor-based logic, and their duality. Theor. Comput. Sci., 3(298):471–510, 2003. doi:10.1016/S0304-3975(02)00865-4.
[3] C. C. Chang and H. J. Keisler. Model Theory, volume 73 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam, third edition, 1990.
[4] Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn L. Talcott, editors. All About Maude – A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of LNCS. Springer Berlin, Heidelberg, 2007. doi:10.1007/978-3-540-71999-1.
[5] Paul J. Cohen. The independence of the continuum hypothesis. Proceedings of the National Academy of Sciences of the United States of America, 50(6):1143–1148, December 1963. doi:10.1073/pnas.50.6.1143.
[6] Paul J. Cohen. The independence of the continuum hypothesis, II. Proceedings of the National Academy of Sciences of the United States of America, 51(1):105–110, January 1964. doi:10.1073/pnas.51.1.105.
[7] Răzvan Diaconescu. Institution-Independent Model Theory. Studies in Universal Logic. Birkhäuser, 2008.
[8] Răzvan Diaconescu and Kokichi Futatsugi. Logical foundations of CafeOBJ. Theoretical Computer Science, 285(2):289–318, 2002. doi:10.1016/S0304-3975(01)00361-9.
[9] Ronald Fagin. Generalized First-Order Spectra and Polynomial-Time Recognizable Sets. In Richard M. Karp, editor, Complexity of Computation, volume 7 of SIAM-AMS Proceedings, pages 43–73. American Mathematical Society, 1974. doi:10.1090/psapm/007.
[10] Ronald Fagin. Finite-model theory - a personal perspective. Theoretical Computer Science, 116:3–31, 1993. doi:10.1016/0304-3975(93)90218-I.
[11] Joseph A. Goguen and Rod M. Burstall. Institutions: Abstract Model Theory for Specification and Programming. J. ACM, 39(1):95–146, 1992. doi:10.1145/147508.147524.
[12] Erich Grädel, Phokion Kolaitis, Libkin G., Marx Leonid, Spencer Maarten, Vardi Joel, Y. Moshe, Yde Venema, and Scott Weinstein. Finite Model Theory and its Applications. Springer, 2007. doi:10.1007/3-540-68804-8.
[13] Daniel Găină. Interpolation in logics with constructors. Theor. Comput. Sci., 474:46–59, 2013. doi:10.1016/J.TCS.2012.12.002.
[14] Daniel Găină. Forcing, Downward Löwenheim-Skolem and Omitting Types Theorems, Institutionally. Logica Universalis, 8(3-4):469–498, 2014. doi:10.1007/S11787-013-0090-0.
[15] Daniel Găină. Forcing and Calculi for Hybrid Logics. Journal of the Association for Computing Machinery, 67(4):1–55, 2020. doi:10.1145/3400294.
[16] Daniel Găină, Guillermo Badia, and Tomasz Kowalski. Omitting types theorem in hybrid dynamic first-order logic with rigid symbols. Annals of Pure and Applied Logic, 174(3):103212, 2023. doi:10.1016/J.APAL.2022.103212.
[17] Daniel Găină, Kokichi Futatsugi, and Kazuhiro Ogata. Constructor-based Logics. Journal of Universal Computer Science, 18(16):2204–2233, August 2012. doi:10.3217/JUCS-018-16-2204.
[18] Daniel Găină and Marius Petria. Completeness by forcing. Journal of Logic and Computation, 20(6):1165–1186, 2010. doi:10.1093/LOGCOM/EXQ012.
[19] Go Hashimoto, Daniel Găină, and Ionut Ţuţu. Forcing, Transition Algebras, and Calculi. In Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson, editors, 51st International Colloquium on Automata, Languages, and Programming, ICALP 2024, July 8-12, 2024, Tallinn, Estonia, volume 297 of LIPIcs, pages 143:1–143:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.ICALP.2024.143.
[20] Go Hashimoto and Daniel Găină. Model-theoretic forcing in transition algebra, 2025. arXiv:2506.22828.
[21] Wilfrid Hodges. A Shorter Model Theory. Cambridge University Press, Cambridge, UK, 1997.
[22] H. Jerome Keisler and Arnold W. Miller. Categoricity without equality. Fundamenta Mathematiae, 170:87—-106, 2001.
[23] H.J. Keisler. Forcing and the omitting types theorem. In M.D. Morley, editor, Studies in Model Theory, MAA Studies in Mathematics, volume 8, pages 96–133, 1973.
[24] Leonid Libkin. Elements of Finite Model Theory. Texts in Theoretical Computer Science. Springer, Berlin, Heidelberg, 2004. doi:10.1007/978-3-662-07003-1.
[25] José Meseguer. Conditional rewriting logic: Deduction, models and concurrency. In Stéphane Kaplan and Mitsuhiro Okada, editors, Conditional and Typed Rewriting Systems, 2nd International CTRS Workshop, Montreal, Canada, June 11-14, 1990, Proceedings, volume 516 of LNCS, pages 64–91. Springer, 1990. doi:10.1007/3-540-54317-1_81.
[26] Marius Petria. An Institutional Version of Gödel’s Completeness Theorem. In Till Mossakowski, Ugo Montanari, and Magne Haveraaen, editors, Algebra and Coalgebra in Computer Science, Second International Conference, CALCO 2007, Bergen, Norway, August 20-24, 2007, Proceedings, volume 4624 of LNCS, pages 409–424. Springer, 2007. doi:10.1007/978-3-540-73859-6_28.
[27] Adrián Riesco, Kazuhiro Ogata, Masaki Nakamura, Daniel Găină, Duong Dinh Tran, and Kokichi Futatsugi. Proof scores: A survey. ACM Comput. Surv., April 2025. doi:10.1145/3729166.
[28] Abraham Robinson. Forcing in model theory. Symposia Mathematica, 5:69–82, 1971.
[29] Donald Sannella and Andrzej Tarlecki. Foundations of Algebraic Specification and Formal Software Development. Monographs in Theoretical Computer Science. An EATCS Series. Springer, 2012. doi:10.1007/978-3-642-17336-3.

[bib.bib1] [1] Michel Bidoit and Rolf Hennicker. Constructor-based observational logic. J. Log. Algebraic Methods Program., 67(1-2):3–51, 2006. doi:10.1016/J.JLAP.2005.09.002.

[bib.bib2] [2] Michel Bidoit, Rolf Hennicker, and Alexander Kurz. Observational logic, constructor-based logic, and their duality. Theor. Comput. Sci., 3(298):471–510, 2003. doi:10.1016/S0304-3975(02)00865-4.

[bib.bib3] [3] C. C. Chang and H. J. Keisler. Model Theory, volume 73 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam, third edition, 1990.

[bib.bib4] [4] Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn L. Talcott, editors. All About Maude – A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of LNCS. Springer Berlin, Heidelberg, 2007. doi:10.1007/978-3-540-71999-1.

[bib.bib5] [5] Paul J. Cohen. The independence of the continuum hypothesis. Proceedings of the National Academy of Sciences of the United States of America, 50(6):1143–1148, December 1963. doi:10.1073/pnas.50.6.1143.

[bib.bib6] [6] Paul J. Cohen. The independence of the continuum hypothesis, II. Proceedings of the National Academy of Sciences of the United States of America, 51(1):105–110, January 1964. doi:10.1073/pnas.51.1.105.

[bib.bib7] [7] Răzvan Diaconescu. Institution-Independent Model Theory. Studies in Universal Logic. Birkhäuser, 2008.

[bib.bib8] [8] Răzvan Diaconescu and Kokichi Futatsugi. Logical foundations of CafeOBJ. Theoretical Computer Science, 285(2):289–318, 2002. doi:10.1016/S0304-3975(01)00361-9.

[bib.bib9] [9] Ronald Fagin. Generalized First-Order Spectra and Polynomial-Time Recognizable Sets. In Richard M. Karp, editor, Complexity of Computation, volume 7 of SIAM-AMS Proceedings, pages 43–73. American Mathematical Society, 1974. doi:10.1090/psapm/007.

[bib.bib10] [10] Ronald Fagin. Finite-model theory - a personal perspective. Theoretical Computer Science, 116:3–31, 1993. doi:10.1016/0304-3975(93)90218-I.

[bib.bib11] [11] Joseph A. Goguen and Rod M. Burstall. Institutions: Abstract Model Theory for Specification and Programming. J. ACM, 39(1):95–146, 1992. doi:10.1145/147508.147524.

[bib.bib12] [12] Erich Grädel, Phokion Kolaitis, Libkin G., Marx Leonid, Spencer Maarten, Vardi Joel, Y. Moshe, Yde Venema, and Scott Weinstein. Finite Model Theory and its Applications. Springer, 2007. doi:10.1007/3-540-68804-8.

[bib.bib13] [13] Daniel Găină. Interpolation in logics with constructors. Theor. Comput. Sci., 474:46–59, 2013. doi:10.1016/J.TCS.2012.12.002.

[bib.bib14] [14] Daniel Găină. Forcing, Downward Löwenheim-Skolem and Omitting Types Theorems, Institutionally. Logica Universalis, 8(3-4):469–498, 2014. doi:10.1007/S11787-013-0090-0.

[bib.bib15] [15] Daniel Găină. Forcing and Calculi for Hybrid Logics. Journal of the Association for Computing Machinery, 67(4):1–55, 2020. doi:10.1145/3400294.

[bib.bib16] [16] Daniel Găină, Guillermo Badia, and Tomasz Kowalski. Omitting types theorem in hybrid dynamic first-order logic with rigid symbols. Annals of Pure and Applied Logic, 174(3):103212, 2023. doi:10.1016/J.APAL.2022.103212.

[bib.bib17] [17] Daniel Găină, Kokichi Futatsugi, and Kazuhiro Ogata. Constructor-based Logics. Journal of Universal Computer Science, 18(16):2204–2233, August 2012. doi:10.3217/JUCS-018-16-2204.

[bib.bib18] [18] Daniel Găină and Marius Petria. Completeness by forcing. Journal of Logic and Computation, 20(6):1165–1186, 2010. doi:10.1093/LOGCOM/EXQ012.

[bib.bib19] [19] Go Hashimoto, Daniel Găină, and Ionut Ţuţu. Forcing, Transition Algebras, and Calculi. In Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson, editors, 51st International Colloquium on Automata, Languages, and Programming, ICALP 2024, July 8-12, 2024, Tallinn, Estonia, volume 297 of LIPIcs, pages 143:1–143:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.ICALP.2024.143.

[bib.bib20] [20] Go Hashimoto and Daniel Găină. Model-theoretic forcing in transition algebra, 2025. arXiv:2506.22828.

[bib.bib21] [21] Wilfrid Hodges. A Shorter Model Theory. Cambridge University Press, Cambridge, UK, 1997.

[bib.bib22] [22] H. Jerome Keisler and Arnold W. Miller. Categoricity without equality. Fundamenta Mathematiae, 170:87—-106, 2001.

[bib.bib23] [23] H.J. Keisler. Forcing and the omitting types theorem. In M.D. Morley, editor, Studies in Model Theory, MAA Studies in Mathematics, volume 8, pages 96–133, 1973.

[bib.bib24] [24] Leonid Libkin. Elements of Finite Model Theory. Texts in Theoretical Computer Science. Springer, Berlin, Heidelberg, 2004. doi:10.1007/978-3-662-07003-1.

[bib.bib25] [25] José Meseguer. Conditional rewriting logic: Deduction, models and concurrency. In Stéphane Kaplan and Mitsuhiro Okada, editors, Conditional and Typed Rewriting Systems, 2nd International CTRS Workshop, Montreal, Canada, June 11-14, 1990, Proceedings, volume 516 of LNCS, pages 64–91. Springer, 1990. doi:10.1007/3-540-54317-1_81.

[bib.bib26] [26] Marius Petria. An Institutional Version of Gödel’s Completeness Theorem. In Till Mossakowski, Ugo Montanari, and Magne Haveraaen, editors, Algebra and Coalgebra in Computer Science, Second International Conference, CALCO 2007, Bergen, Norway, August 20-24, 2007, Proceedings, volume 4624 of LNCS, pages 409–424. Springer, 2007. doi:10.1007/978-3-540-73859-6_28.

[bib.bib27] [27] Adrián Riesco, Kazuhiro Ogata, Masaki Nakamura, Daniel Găină, Duong Dinh Tran, and Kokichi Futatsugi. Proof scores: A survey. ACM Comput. Surv., April 2025. doi:10.1145/3729166.

[bib.bib28] [28] Abraham Robinson. Forcing in model theory. Symposia Mathematica, 5:69–82, 1971.

[bib.bib29] [29] Donald Sannella and Andrzej Tarlecki. Foundations of Algebraic Specification and Formal Software Development. Monographs in Theoretical Computer Science. An EATCS Series. Springer, 2012. doi:10.1007/978-3-642-17336-3.

Model-Theoretic Forcing in Transition Algebra

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

2 Transition algebra

Signatures.

▶ Remark 1.

Models.

▶ Remark 2.

Sentences.

▶ Remark 3.

Satisfaction relation.

Proposition 4 (Satisfaction condition).

Logical framework.

3 Related concepts

Presentations.

Substitutions.

Proposition 5 (Satisfaction condition for substitutions).

4 Compactness and Upward Löwenheim-Skolem Property

Theorem 6 (Categoricity).

Example 7 (Robinson Consistency).

Example 8.

Definition 9 (Upward Löwenheim-Skolem Property).

Corollary 10.

5 Forcing

Example 11.

Definition 12 (Forcing property).

Definition 13 (Forcing relation).

Lemma 14 (Forcing properties [19]).

Definition 15 (Generic set).

▶ Remark 16.

Definition 17 (Generic model).

Theorem 18 (Generic Model Theorem [19]).

6 Semantic Forcing

Example 19.

Example 20.

Definition 21 (Semantic Forcing Property).

▶ Remark 22.

Definition 23 (Distance & weak forcing).

Theorem 24 (Semantic Forcing Theorem).

7 Downward Löwenheim-Skolem Theorem

Lemma 25 (Existence).

Proof.

Theorem 26 (Downward Löwenheim-Skolem Theorem).

8 Omitting Types Theorem

Definition 27 (Types).

Definition 28 (Isolated types).

Lemma 29.

Definition 30 (Omitting Types Property).

Theorem 31 (Omitting Types Theorem).

Lemma 32.

Lemma 33.

9 𝝎-Completeness

Definition 34 (Entailment relation).

Constructor-based algebras.

Definition 35 (Constructor-based algebras).

Example 36 (Lists).

Finite algebras.

Definition 37.

Theorem 38 (Completeness).

10 Conclusions

References

$\blacktriangleright$ Remark 1.

$\blacktriangleright$ Remark 2.

$\blacktriangleright$ Remark 3.

$\blacktriangleright$ Remark 16.

$\blacktriangleright$ Remark 22.

9 $\omega$ -Completeness