June 30, 2026
Probability logic (\(\mathsf{PL}\)) extends propositional logic with countably many probability operators, one for each rational number between 0 and 1. The formulas of this logic are interpreted over the class of Markov processes, i.e., structures of the form \(\langle \Omega, \Sigma, T \rangle\), where \(\langle \Omega, \Sigma \rangle\) is a measurable space and \(T\) is a Markov kernel.
The main contribution of this paper is the establishment of the Goldblatt-Thomason theorem for probability logic. As an application, we show that the class of Harsanyi type spaces is definable in \(\mathsf{PL}\). Moreover, we obtain some variants of the Goldblatt-Thomason theorem for specific subclasses of Markov processes.
Probability logic aims to provide a formal framework for studying probabilistic systems, such as Markov processes. It supports reasoning about quantitative statements of the form ‘an event occurs with probability at least \(r\)’ and has been widely applied in diverse areas, including theoretical computer science [@deshar:bisim02; @panan:lmp09], artificial intelligence [@fagin:logic90], and economics [@Aum1999; @heifmon:prob01].
There are different syntactic frameworks for studying probabilistic systems, such as first-order syntax (see, e.g., [@keisler]) which may provide a more expressive language, or modal syntax (see, e.g., [@fagin:logic90; @heifmon:prob01]) which is less expressive but decidable. Throughout this paper, we investigate the modal framework. Probability logic is a multimodal extension of propositional logic obtained by adding a family of modal operators \(\{L_r \mid r \in \mathbb{Q} \cap [0,1]\}\). The intended interpretation of a formula \(L_r \varphi\) is that ‘the probability of \(\varphi\) is at least \(r\)’.
Markov processes provide a mathematically rigorous model for probabilistic state-based systems, particularly in theoretical computer science. A (labeled) Markov process consists of a measurable state space equipped with transition probability kernels (indexed by actions), thereby modeling systems that combine probabilistic evolution with observable interaction. Such structures serve, for example, as denotational models for probabilistic programming languages and as semantic foundations for verification, equivalence, abstraction, and compositional reasoning in stochastic systems. Formally, a Markov process is a structure \(\langle\Omega,\Sigma,T\rangle\), where \(\langle\Omega,\Sigma\rangle\) is a measurable space and \(T: \Omega \times \Sigma \to [0,1]\) is a Markov kernel.
In this paper, we investigate definability of classes of Markov processes by means of theories in probability logic. Our main result establishes a version of the Goldblatt-Thomason theorem for this setting. The classical theorem of Goldblatt and Thomason characterizes the modally definable elementary classes of Kripke frames in terms of certain frame constructions. It states that an elementary (first-order definable) class of Kripke frames is modally definable if and only if it is closed under disjoint unions, generated subframes, bounded morphic images, and reflects ultrafilter extensions. The original proof is algebraic in nature, relying on representation theory for modal algebras. It is further shown that a class of general frames– i.e., Kripke frames equipped with a Boolean algebra of admissible sets–is modally definable precisely when it is closed under disjoint unions, generated subframes, bounded morphic images, and both closed under and reflective of ultrafilter extensions. Subsequently, van Benthem provided a model-theoretic proof of the original Goldblatt-Thomason theorem [@benthem:revisited93].
Goldblatt-Thomason style characterizations have since been established for numerous extensions of modal and intuitionistic logics, including graded modal logic [@sano:gtgraded10], intuitionistic logic [@rodenburg2016intuitionistic; @sano2020goldblatt; @de2020goldblatt; @ma2025goldblatt], and coalgebraic modal logic [@kurz:golcoal07]. In particular, van Benthem studied definable classes of finite (transitive) frames [@van1988notes]. He showed that for every finite transitive point-generated frame \(\mathfrak{F}\) there exists a formula \(\varphi_{\mathfrak{F}}\), known as a Jankov-Fine formula, such that whenever \(\varphi_{\mathfrak{F}}\) is satisfiable on a frame \(\mathfrak{G}\), there exists a surjective bounded morphism from a generated subframe of \(\mathfrak{G}\) onto \(\mathfrak{F}\). Variants of such Jankov-Fine constructions have been employed to characterize definable classes of finite structures in other logical settings, for example, in conditional logic over finite posets [@fornasiere2024frame].
The study of definability in probability logic presents substantial additional difficulties. A central obstacle is the failure of compactness. The classical Goldblatt-Thomason theorem is formulated for elementary classes and can be weakened in terms of closure under ultrapowers. In contrast, satisfaction of probability formulas is not preserved under ultraproducts, and compactness fails accordingly. Our approach therefore follows the version for general frames and replaces closure under ultrapowers with ultrafilter extensions. However, defining suitable ultrafilter extensions for Markov processes is technically non-trivial. To address this issue, we adapt ideas from [@kozen2013stone], working with Markov processes whose \(\sigma\)-algebras admit countable generating sets. Indeed, Kozen and coauthors [@kozen2013stone] studied Stone duality for Markov processes. In order to analyze the corresponding algebraic structures, known as Aumann algebras, they introduced an ultrafilter construction on a particular class of Markov processes, termed Stone-Markov processes. They proved the duality between countable Aumann algebras and Stone-Markov Markov processes. Accordingly, we also consider the class of Markov processes with countably generated \(\sigma\)-algebras, and employ methods similar to those in [@kozen2013stone] to define ultrafilter extensions of Markov processes.
In addition to the general case, we investigate definability over the class of finite Markov processes, obtaining a corresponding characterization for this important special case.
The outline of this article is as follows. In Section 2, a brief review of the basic notions and facts needed for other parts is given. In Section 3, model-theoretic constructions used in the Goldblatt-Thomason theorem are introduced. In Section 4, a version of the Goldblatt-Thomason theorem is established. Finally, in Section 5, a version of the Goldblatt-Thomason theorem for the class of finite Markov processes is given.
In this section, we review the basic materials needed for the main results of this paper.
Let \(\mathbb{P}\) be a countable set of propositional variables. The formulas of probability logic (\(\mathsf{PL}\)) are defined recursively by the following grammar: \[\begin{align} \varphi ::&=\;\;p\mid \neg\varphi \mid \varphi \land \varphi \mid L_r \varphi \end{align}\] where \(p \in \mathbb{P}\) and \(r\in \mathbb{Q}_0\;:= [0,1] \cap \mathbb{Q}\). The Boolean connectives \(\top\), \(\perp\), \(\to\), \(\leftrightarrow\), and \(\vee\) are defined in the usual way. For a formula \(\varphi\), the expression \(L_r \varphi\) is interpreted as ‘the probability of \(\varphi\) is at least \(r\)’. Likewise, \(M_r \varphi\) is defined as an abbreviation for \(L_{1-r}\neg \varphi\) and is interpreted as ‘the probability of \(\varphi\) is at most \(r\)’. Moreover, for \(r_1,\dots,r_k \in \mathbb{Q}_0\), we use the formula \(L_{r_1\dots r_k} \varphi\) as an abbreviation for \(L_{r_1} \dots L_{r_k} \varphi\). Additionally, \(L_r^0 \varphi := \varphi\) and \(L_r^n \varphi:= \underbrace{ L_r \; \dots\; L_r}_\text{n-times} \varphi\) for each \(n>0\) and \(r\in \mathbb{Q}_0\).
Definition 1. Let \(\langle{\Omega, \Sigma}\rangle\) be a measurable space. A function \(T: \Omega\times \Sigma\to [0, 1]\) is called a Markov kernel* (or transition probability) if the following conditions hold:*
for each \(w \in \Omega\), the mapping \(T(w, .): N \mapsto T(w, N)\) is a probability measure on \(\Sigma\);
for each \(N \in \Sigma\), the mapping \(T(., N): w \mapsto T(w, N)\) is a measurable function on \(\Omega\).
The triple \(\langle{\Omega, \Sigma, T}\rangle\) is then called a Markov process* on the state space \(\langle{\Omega, \Sigma}\rangle\). For convenience, we may write \(T(w)(N)\) instead of \(T(w, N)\).*
Definition 2. A Markov process \(\mathfrak{P}= \langle{\Omega, \Sigma, T}\rangle\) is said (countably) generated* by a (countable) subalgebra \(\mathcal{B}\) of \(\Sigma\) if \(\mathcal{B}\) is a (countable) Boolean algebra and \(\Sigma:= \sigma(\mathcal{B})\), the smallest \(\sigma\)-algebra containing \(\mathcal{B}\). We always assume that \(F_r(N) := \{w\in\Omega\;|\; T(w)(N)\geq r\}\in \mathcal{B}\), for each \(N \in \mathcal{B}\) and \(r\in \mathbb{Q}_0\). We also define \(F_{r_1\dots r_n}(N)\) as \(F_{r_1}\dots F_{r_n}(N)\), for \(r_1, \dots, r_n\in \mathbb{Q}_0\).*
Convention 1. If we represent the Markov process \(\mathfrak{P}\) as \(\langle{\Omega, \mathcal{B}, T}\rangle\), then we mean that \(\Sigma= \sigma(\mathcal{B})\).
Definition 3. A Markov model, or simply a model, over (or based on) a Markov process \(\mathfrak{P}= \langle{\Omega, \mathcal{B}, T}\rangle\) is a tuple \(\mathfrak{M} = \langle{\Omega, \mathcal{B}, T, v}\rangle\) where \(v: \mathbb{P} \to \mathcal{B}\) is a valuation function which assigns to every propositional variable \(p \in \mathbb{P}\), a set \(v(p)\in\mathcal{B}\).
Note that restricting the valuation to the generating subalgebra \(\mathcal{B}\) is analogous to defining valuations on general Kripke frames, in which each propositional variable \(p\) is assigned a value in the augmented algebra associated with the frame. This restriction is necessary in order to adapt the method used in proving the Goldblatt–Thomason theorem for general frames to the setting of Markov processes.
Definition 4. The satisfaction relation* for arbitrary formulas in a given model \(\mathfrak{M} = \langle{\Omega, \mathcal{B}, T, v}\rangle\), is defined inductively as follows:*
\(\mathfrak{M}, w \vDash p \;\) iff \(\; w \in v(p)\),
\(\mathfrak{M}, w \vDash \neg\varphi \;\) iff \(\; \mathfrak{M}, w \nvDash \varphi\),
\(\mathfrak{M}, w \vDash \varphi\land \psi\;\) iff \(\; \mathfrak{M}, w \vDash \varphi\) and \(\mathfrak{M}, w \vDash \psi\),
\(\mathfrak{M}, w \vDash L_r \varphi \;\) iff \(\; T(w, [\![\varphi]\!]_{\mathfrak{M}}) \geq r\), where \([\![\varphi]\!]_{\mathfrak{M}} = \{ w \in \Omega\;| \; \mathfrak{M}, w \vDash \varphi \}\).
A set \(\Gamma\) of formulas is satisfiable in the world \(w\) if \(\mathfrak{M}, w \vDash \varphi\) for each \(\varphi \in \Gamma\).
Note that by Convention 1, we have \([\![\varphi]\!]_{\mathfrak{M}}\in\mathcal{B}\), for each formula \(\varphi\).
Definition 5. A formula \(\varphi\) is valid in a model \(\mathfrak{M}= \langle{\Omega, \mathcal{B}, T, v}\rangle\), denoted by \(\mathfrak{M}\vDash \varphi\), if \(\mathfrak{M}, w \vDash \varphi\) for all \(w \in \Omega\). Similarly, \(\varphi\) is valid in a Markov process \(\mathfrak{P} = \langle{\Omega, \mathcal{B}, T}\rangle\), denoted by \(\mathfrak{P}\vDash \varphi\), if it is valid in every model based on \(\mathfrak{P}\). We say that \(\varphi\) is valid in a class \(\mathcal{C}\)* of Markov processes, denoted by \({\vDash}_{\mathcal{C}}\; \varphi\), if it is valid in every element \(\mathfrak{P}=\langle{\Omega, \Sigma, T}\rangle\) of \(\mathcal{C}\). For abbreviation, we may omit the subscript \(\mathcal{C}\) and instead write \({\vDash}\; \varphi\) when it is the class of all Markov processes. A set of formulas \(\Gamma\) is satisfiable in the class \(\mathcal{C}\) if there is a Markov process \(\mathfrak{P}\in\mathcal{C}\) and a model \(\mathfrak{M}\) based on \(\mathfrak{P}\) such that \(\mathfrak{M},w\models\Gamma\) for some \(w\in\Omega\). Likewise, \(\Gamma\) is finitely satisfiable in \(\mathcal{C}\) if each finite subset \(\Gamma'\subseteq\Gamma\) is satisfiable in \(\mathcal{C}\).*
Let \(\varphi\) be a formula and \(\mathfrak{P} = \langle{\Omega, \Sigma, T}\rangle\) a Markov process. Then the following conditions are equivalent:
\(\varphi\) is valid in \(\mathfrak{P} = \langle{\Omega, \Sigma, T}\rangle\).
\(\varphi\) is valid in \(\mathfrak{P} = \langle{\Omega, \mathcal{B}, T}\rangle\), for every subalgebra \(\mathcal{B}\) of \(\Sigma\) with \(\Sigma= \sigma(\mathcal{B})\).
\(\varphi\) is valid in every \(\mathfrak{P}' = \langle{\Omega, \Sigma', T'}\rangle\), where \(\Sigma'\) is a countably generated \(\sigma\)-subalgebra of \(\Sigma\) and \(T' = T \upharpoonright\Sigma'\).
\(\varphi\) is valid in every \(\mathfrak{P}' = \langle{\Omega, \mathcal{B}', T'}\rangle\), where \(\mathcal{B}'\) is a countable subalgebra of \(\Sigma\) and \(T'= T\upharpoonright \sigma(\mathcal{B}')\).
Proof. The equivalence of Parts 1 and 2, and respectively, Parts 3 and 4 are obvious. To see that Part 4 implies Part 1, notice that if \(\varphi\) is not valid in \(\mathfrak{P} = \langle{\Omega, \Sigma, T}\rangle\), then there exists a valuation \(v:\mathbb{P}\to \Sigma\) such that in \(\mathfrak{M} = \langle{\mathfrak{P}, v}\rangle\), we have that \(\mathfrak{M}, w \nvDash \varphi\), for some \(w\in \Omega\). Now if we take \(\mathcal{B}' = \{[\![\theta]\!]_{\mathfrak{M}}\;|\; \theta\; \text{is a formula}\}\), then \(\varphi\) is not valid in \(\mathfrak{P}'= \langle{\Omega, \mathcal{B}', T\upharpoonright \sigma(\mathcal{B}')}\rangle\). Finally, It is clear that Part 2 implies Part 4. ◻
Definition 6. A class of Markov processes \(\mathcal{C}\) is definable in probability logic or P-definable, if there is a set of formulas \(\Gamma\) such that for any Markov process \(\mathfrak{P}\) we have \(\mathfrak{P}\in\mathcal{C}\) if and only if \(\mathfrak{P}\models\Gamma\).
Definition 7. [@kozen2013stone] Let \(\langle{\Omega, \mathcal{B}, T}\rangle\) be a countably generated Markov process. We say that this process is a Stone-Markov process* if \(\mathcal{B}\) is a countable base of clopen sets for the topology generated by \(\mathcal{B}\), named \(\tau_{\mathcal{B}}\), that satisfies the Baire property (also called *topologically complete).**
Note that if \(\langle\Omega, \tau_\mathcal{B}\rangle\) is a Polish space or a compact separable space, then \(\langle{\Omega, \mathcal{B}, T}\rangle\) is a Stone-Markov process. This property is referred to as saturation in [@kozen2013stone].
In this section, we introduce several model-theoretic constructions that are needed for the proof of the Goldblatt–Thomason Theorem for probability logic.
We begin by defining the notion of a Markov sub-process.
Definition 8 (Markov sub-process). Let \(\mathfrak{P} = \langle \Omega, \Sigma, T\rangle\) be a Markov process, and let \(\Omega' \in \Sigma\) be a measurable subset such that \[T(w,\Omega') = 1 \quad \text{for all } w \in \Omega'.\] Let \(\Sigma' = \{ N \cap \Omega' \mid N \in \Sigma \}\) be the induced \(\sigma\)-algebra on \(\Omega'\). Define the transition function \(T' \colon \Omega' \times \Sigma' \to [0,1]\) by \[T'(w, N \cap \Omega') = T(w,N),\] for all \(w \in \Omega'\) and \(N \in \Sigma\).
Lemma 1. Under the assumptions of Definition 8:
the triple \(\mathfrak{P}' = \langle \Omega', \Sigma', T' \rangle\) is a Markov process;
if \(\mathfrak{P}\) is countably generated, then so is \(\mathfrak{P}'\).
Proof.
The main point is to show that \(T'\) is well defined. Let \(N_1, N_2\in\Sigma\) and \(N_1=N_2\). Since \(T(w,\Omega') = 1\) for all \(w \in \Omega'\), we have \[T'(w,N_1 \cap \Omega') = T(w,N_1) = T(w,N_2) = T'(w,N_2 \cap \Omega'),\] so \(T'\) is well defined. Standard arguments show that \(T'\) is a Markov kernel.
Suppose that \(\mathcal{B}\) is a countable Boolean algebra generating \(\Sigma\). Then \[\mathcal{B}' = \{ B \cap \Omega' \mid B \in \mathcal{B} \}\] generates \(\Sigma'\). Moreover, for each \(r \in [0,1]\) and \(B \in \mathcal{B}\), \[F_r(B \cap \Omega') = \{ w \in \Omega' \mid T'(w,B \cap \Omega') \ge r \} = F_r(B) \cap \Omega'.\] Thus \(\mathfrak{P}'\) is countably generated.
◻
Once the notion of a sub-process has been established, we can define the corresponding notion of a sub-model.
Definition 9. Let \(\mathfrak{M} = \langle \Omega, \Sigma, T, v \rangle\) be a Markov model. Suppose that \(\Omega' \in \Sigma\) satisfies the conditions of Definition 8, and let \(\mathfrak{P}' = \langle \Omega', \Sigma', T' \rangle\) be the corresponding sub-process. Define a valuation \(v'\) by setting \[v'(p) = v(p) \cap \Omega' \quad \text{for each } p \in \mathbb{P}.\] Then \(\mathfrak{M}' = \langle \Omega', \Sigma', T', v' \rangle\) is called a sub-model* of \(\mathfrak{M}\).*
Lemma 2. Let \(\mathfrak{M}'\) be a sub-model of \(\mathfrak{M}\). Then for every formula \(\varphi\) and every \(w \in \Omega'\), \[\mathfrak{M}, w \vDash \varphi \quad \text{iff} \quad \mathfrak{M}', w \vDash \varphi.\]
Corollary 1. Let \(\varphi\) be a formula. If \(\mathfrak{P} \vDash \varphi\) and \(\mathfrak{P}'\) is a sub-process of \(\mathfrak{P}\), then \(\mathfrak{P}' \vDash \varphi\).
Proof. Suppose not. Then there exists a valuation \(v'\) on \(\mathfrak{P}'\) and a state \(w \in \Omega'\) such that \(\mathfrak{M}', w \nvDash \varphi\). Extend \(v'\) to a valuation \(v\) on \(\mathfrak{P}\) by setting \(v(p)=v'(p)\) for all \(p \in \mathbb{P}\). By the previous lemma, \(\mathfrak{M}, w \nvDash \varphi\), contradicting \(\mathfrak{P} \vDash \varphi\). ◻
For a given model \(\mathfrak{M}\) the following lemma introduces a sub-model \(\mathfrak{M}'\) of \(\mathfrak{M}\) which plays the same role as a generated sub-model in the context of the Kripke semantics.
Lemma 3. Suppose \(\mathfrak{M} = \langle \Omega, \Sigma,T, v\rangle\) is a model, \(w\in \Omega\) and \(\Gamma\) is a set of formulas such that \(\mathfrak{M}, w \vDash L_1^n \varphi\) for each \(\varphi\in \Gamma\) and \(n\geq 0\). Then there exists a sub-model \(\mathfrak{M}' = \langle \Omega', \Sigma',T', v'\rangle\) such that \(w\in \Omega'\) and \(\mathfrak{M}'\vDash \Gamma\).
Proof. Let \(\Gamma = \{\varphi_0, \varphi_1, \dots\}\). So we have \(\mathfrak{M}, w \vDash L_1^n \varphi_i\) for each \(i , n \geq 0\). Therefore, \(T(w, [\![L_1^{n}\varphi_i]\!]_\mathfrak{M})= 1\), for each \(i,n\geq 0\). Put \(\Omega_{i,n} = [\![L_1^{n}\varphi_i]\!]_\mathfrak{M}\) and \(\Omega' = \bigcap_{i, n} \Omega_{i,n}\). Then, \(w\in \Omega'\) and \(\Omega'\) is a measurable set. Moreover, for each \(w'\in \Omega'\) and \(i, n\geq 0\), we have \(\mathfrak{M}, w' \vDash L_1^{n+1}\varphi_i\). Hence, \(T(w', \Omega_{i,n})= 1\), for each \(i,n\geq 0\). This implies that \(T(w',\Omega')=1\). Now, if we take \(\mathfrak{M}' = \langle \Omega', \Sigma',T', v'\rangle\) as a sub-model of \(\mathfrak{M}\), then \(\mathfrak{M}'\) satisfies the required claim. ◻
Definition 10. Let \(\mathfrak{P}=\langle \Omega, \Sigma, T \rangle\) be a Markov process. We say that a Markov process \(\mathfrak{P}'=\langle \Omega, \Sigma', T' \rangle\) is an event sub-process* of \(\mathfrak{P}\) if \(\Sigma'\) is a \(\sigma\)-sub-algebra of \(\Sigma\) and \(T' = T\upharpoonright_{\Sigma'}\) is a Markov kernel.*
The following lemma is immediate by Proposition [validity].
Lemma 4. Let \(\mathfrak{P}'\) be an event sub-process of \(\mathfrak{P}\). Then \(\mathfrak{P}\models\varphi\) implies that \(\mathfrak{P}'\models\varphi\), for any formula \(\varphi\).
Next, we define disjoint unions of Markov processes.
Definition 11 (Disjoint union).
Let \(I\) be a non-empty index set, and for each \(i \in I\) let \(\mathfrak{P}_i = \langle \Omega_i, \Sigma_i, T_i \rangle\) be a Markov process. The disjoint union \(\biguplus_{i \in I} \mathfrak{P}_i\) is the Markov process \(\mathfrak{P} = \langle \Omega, \Sigma, T \rangle\) defined as follows:
\(\Omega = \biguplus_{i \in I} \Omega_i\);
\(\Sigma\) is the \(\sigma\)-algebra generated by the algebra of all sets of the form \(\biguplus_{i \in I} N_i\), where \(N_i \in \Sigma_i\);
For all \(j\in I\) and \(w \in \Omega_j\), \[T(w,\biguplus_{i \in I} N_i) = T_j(w,N_j).\]
If \(\mathfrak{M}_i = \langle \Omega_i, \Sigma_i, T_i, v_i \rangle\) is a Markov model for each \(i \in I\), then the disjoint union \(\biguplus_{i \in I} \mathfrak{M}_i\) is the Markov model \(\mathfrak{M} = \langle \biguplus_{i \in I} \mathfrak{P}_i, v \rangle\), where \[v(p) = \biguplus_{i \in I} v_i(p) \quad \text{for all } p \in \mathbb{P}.\]
Lemma 5. The disjoint union \(\mathfrak{P} = \biguplus_{i \in I} \mathfrak{P}_i\) and \(\mathfrak{M}=\biguplus_{i \in I}\mathfrak{M}_i\) are respectively a Markov process and a Markov model.
Lemma 6.
Let \(\{\mathfrak{M}_i\}_{i \in I}\) be a family of Markov models and let \(\varphi\) be a formula. Then for each \(w \in \Omega_i\), \[\biguplus_{i \in I} \mathfrak{M}_i, w \vDash \varphi \quad \text{iff} \quad \mathfrak{M}_i, w \vDash \varphi.\]
Let \(\{\mathfrak{P}_i\}_{i \in I}\) be a family of Markov processes. Then for every formula \(\varphi\), \[\biguplus_{i \in I} \mathfrak{P}_i \vDash \varphi \quad \text{iff} \quad \mathfrak{P}_i \vDash \varphi \text{ for all } i \in I.\]
Next, the notion of zigzag morphisms are presented that gives rise to an important notion of similarity between two Markov processes.
Definition 12 (Zigzag morphisms). Let \(\mathfrak{P} = \langle \Omega, \Sigma, T \rangle\) and \(\mathfrak{P}' = \langle \Omega', \Sigma', T' \rangle\) be two Markov processes. A surjective measurable function \(f: \Omega \to \Omega'\) is called a zigzag morphism* from \(\mathfrak{P}\) to \(\mathfrak{P}'\) if it satisfies the condition: \[T(w, f^{-1}(N')) = T'(f(w), N'),\] for each \(w \in \Omega\) and \(N' \in \Sigma'\).*
A zigzag morphism from \(\mathfrak{M} =\langle\mathfrak{P}, v \rangle\) to \(\mathfrak{M}' = \langle\mathfrak{P}', v' \rangle\) is a zigzag morphism \(f\) from \(\mathfrak{P}\) to \(\mathfrak{P}'\) such that \(v(p)= f^{-1} (v'(p))\), for each \(p\in \mathbb{P}\).
Subsequently, the following preservation property can be derived.
Lemma 7. Let \(\mathfrak{P} = \langle \Omega, \Sigma, T \rangle\) and \(\mathfrak{P}' = \langle \Omega', \Sigma', T' \rangle\) be two Markov processes. If there exists a zigzag morphism between \(\mathfrak{P}\) and \(\mathfrak{P}'\), then, \(\mathfrak{P} \vDash \varphi \; \text{implies} \; \mathfrak{P}' \vDash \varphi\), for every formula \(\varphi\).
Proof. Assume that \(\mathfrak{P} \vDash \varphi\). Let \(\mathfrak{M} = \langle \mathfrak{P}, v \rangle\) and \(\mathfrak{M}' = \langle \mathfrak{P}', v' \rangle\) be arbitrary models, and let \(f : \mathfrak{M} \to \mathfrak{M}'\) be a zigzag morphism. By the invariance of satisfaction under zigzag morphisms, for every world \(w \in \Omega\) we have \[\mathfrak{M}, w \vDash \varphi \; \text{if and only if} \; \mathfrak{M}', f(w) \vDash \varphi .\] Since \(\mathfrak{P} \vDash \varphi\), it follows that \(\mathfrak{M}, w \vDash \varphi\) for all \(w \in \Omega\), and hence \(\mathfrak{M}', w' \vDash \varphi\) for all \(w' \in \Omega'\). Therefore, \(\mathfrak{P}' \vDash \varphi\). ◻
We now introduce ultrafilter extensions for countably generated Markov processes, a construction that parallels the classical ultrafilter extension of Kripke structures. Throughout this section, we assume familiarity with ultrafilters on Boolean algebras. We recall from [@kuter:model13] the definition of the ultrafilter limit of a sequence \((r_w)_{w \in \Omega}\) of real numbers with respect to an ultrafilter \(\mathfrak{u}\) over a Boolean algebra \(\mathcal{B}\). This limit, denoted by \(\lim_\mathfrak{u} r_w\), is defined as the unique real number \(r \in [0,1]\) such that \[\{ w \in \Omega \mid |r_w - r| < \varepsilon \} \in \mathfrak{u} \quad \text{for every } \varepsilon > 0.\]
Let \((r_w)_{w \in \Omega}\) be a sequence of real numbers in \([0,1]\), and let \(\mathfrak{u}\) be an ultrafilter over \(\Omega\). Then the following properties hold:
If \(\{ w \in \Omega \mid r_w \geq r \} \in \mathfrak{u}\), then \(\lim_\mathfrak{u} r_w \geq r\).
If \(\lim_\mathfrak{u} r_w > r\), then \(\{ w \in \Omega \mid r_w > r \} \in \mathfrak{u}\).
\(\lim_\mathfrak{u} r_w \geq r\) if and only if \(\{ w \in \Omega \mid r_w \geq s \} \in \mathfrak{u}\) for every \(s < r\).
Definition 13. Let \(\mathfrak{P} = \langle \Omega, \mathcal{B}, T \rangle\) be a countably generated Markov process. We define the structure \(\langle \mathcal{U}^*, \mathcal{B}^*, K^* \rangle\) as follows:
\(\mathcal{U}^*\) is the set of all ultrafilters on \(\mathcal{B}\);
\(\mathcal{B}^* := \{ A^* \mid A \in \mathcal{B} \}\), where \[A^* := \{ \mathfrak{u} \in \mathcal{U}^* \mid A \in \mathfrak{u}\};\]
\(K^* : \mathcal{U}^* \times \mathcal{B}^* \to [0,1]\) is defined by \[K^*(\mathfrak{u}, A^*) := \lim_\mathfrak{u} T(w, A).\]
Lemma 8. The triple \(\langle \mathcal{U}^*, \mathcal{B}^*, K^* \rangle\) satisfies the following properties:
\(\mathcal{B}^*\) is a countable Boolean algebra over \(\mathcal{U}^*\). Moreover, \(\mathcal{B}^*\) forms a basis of clopen sets for the compact Hausdorff Stone topology \(\beta(\mathcal{U}^*)\);
for each \(\mathfrak{u} \in \mathcal{U}^*\), the function \(K^*(\mathfrak{u}, \cdot) : \mathcal{B}^* \to [0,1]\) is a pre-measure.
Proof.
For \(A,B \in \mathcal{B}\), the following equalities hold: \[A^* \cap B^* = (A \cap B)^*, \qquad A^* \cup B^* = (A \cup B)^*, \qquad (A^*)^c = (A^c)^*,\] since elements of \(\mathcal{U}^*\) are ultrafilters. The remaining claims follow from standard results in Stone duality; see, for example, [@Johnstone1982].
It is straightforward to verify that \(K^*(\mathfrak{u},\cdot)\) is finitely additive. Now suppose \((B_n^*)_{n \in \mathbb{N}}\) is a decreasing sequence in \(\mathcal{B}^*\) such that \[\bigcap_{n=1}^\infty B_n^* = \varnothing.\] Since each \(B_n^*\) is clopen in the compact space \(\beta(\mathcal{U}^*)\), there exists \(N \in \mathbb{N}\) such that \(B_n^* = \varnothing\) for all \(n > N\). Consequently, \[K^*(\mathfrak{u}, B_n^*) = 0 \quad \text{for all } n > N,\] and hence \(\lim_{n \to \infty} K^*(\mathfrak{u}, B_n^*) = 0\).
◻
By Carathéodory’s Extension Theorem, the pre-measure \(K^*\) extends uniquely to a Markov kernel \[T^* : \mathcal{U}^* \times \Sigma^* \to [0,1],\] where \(\Sigma^*\) is the Borel \(\sigma\)-algebra generated by \(\mathcal{B}^*\).
Corollary 2. Let \(\mathfrak{P} = \langle \Omega, \mathcal{B}, T \rangle\) be a countably generated Markov process. Then the structure \[\mathfrak{P}^* = \langle \mathcal{U}^*, \mathcal{B}^*, T^* \rangle\] is a countably generated Stone–Markov process.
Proof. It suffices to verify that for each \(N \in \Sigma^*\), the function \[T^*(\cdot, N) : \mathcal{U}^* \to [0,1]\] is measurable. That is, for every \(r \in \mathbb{Q}_0\), \[\{ \mathfrak{u} \in \mathcal{U}^* \mid T^*(\mathfrak{u}, N) \geq r \} \in \Sigma^*.\] Without loss of generality, assume \(N = B^*\) for some \(B \in \mathcal{B}\). By Fact [lim](3), we have \[F_r(B^*) = \{ \mathfrak{u} \in \mathcal{U}^* \mid T^*(\mathfrak{u}, B^*) \geq r \} = \bigcap_{s<r} (F_s(B))^*.\] Since \((F_s(B))^* \in \Sigma^*\) for all \(s < r\), it follows that \(F_r(B^*) \in \Sigma^*\). ◻
Next, we isolate the key notion of nested Archimedean ultrafilters, which constitute the basic building blocks of ultrafilter extensions.
Definition 14. Let \(\mathfrak{P} = \langle \Omega, \mathcal{B}, T \rangle\) be a countably generated Markov process. An ultrafilter \(\mathfrak{u}\) on \(\mathcal{B}\) is called a nested Archimedean ultrafilter* if, for all \(t_1,\dots,t_n,r \in \mathbb{Q}_0\) and all \(A \in \mathcal{B}\), the following condition holds: whenever \[F_{t_1 \dots t_n s}(A) \in \mathfrak{u} \quad \text{for all } s < r,\] then \[F_{t_1 \dots t_n r}(A) \in \mathfrak{u}.\]*
Let \(\mathcal{U}^*_{na}\) denote the set of all nested Archimedean ultrafilters. We show that \(\mathcal{U}^*_{na}\) forms a \(G_{\delta}\)-subspace of \(\mathcal{U}^*\) such that \(T^*(u, \mathcal{U}^*_{na}) = 1\), for each \(\mathfrak{u}\in \mathcal{U}^*_{na}\).
Lemma 9. The following properties hold.
\(\mathcal{U}^*_{na}\) forms a dense \(G_{\delta}\)-subspace of \(\mathcal{U}^*\);
\(T^*(\mathfrak{u}, \mathcal{U}^*_{na}) = 1\), for each \(\mathfrak{u}\in \mathcal{U}^*_{na}\);
\(\{\mathfrak{u}\in \mathcal{U}^*_{na}\;|\; T^*(\mathfrak{u}, B^*) \geq r \} = (F_r(B))^* \cap \mathcal{U}^*_{na}\), for each \(B \in \mathcal{B}\).
Proof.
It is shown in [@kozen2013stone] that \[\mathcal{U}^*_{na}= \bigcap_{B\in \mathcal{B}} \;\; \bigcap_{t_1, \dots, t_n, r\in \mathbb{Q}_0} \Big(\bigcup_{s<r} \big(F^c_{t_1\cdots t_n s} (B)\big)^* \;\cup\; \big(F_{t_1\cdots t_n r} (B)\big)^*\Big).\] Since \(\mathcal{O}_{t_1\cdots t_n r}(B):= \Big(\bigcup_{s<r} \big(F^c_{t_1\cdots t_n s} (B)\big)^* \cup \big(F_{t_1\cdots t_n r} (B)\big)^*\Big)\) is an open subset of \(\mathcal{U}^*\), it follows that \(\mathcal{U}^*_{na}\) is a \(G_{\delta}\)-subspace of \(\mathcal{U}^*\). Moreover, by Rasiowa–Sikorski Lemma [@RasiowaSikorski1950], there exists an ultrafilter \(\mathfrak{u}\in \mathcal{U}^*\) such that for \(\emptyset \not= B'\in \mathcal{B}\) and \(t_1, \dots, t_n, r\in \mathbb{Q}_0\), we have that \(B'\in \mathfrak{u}\) and whenever \[F_{t_1\cdots t_n s} (B)\in \mathfrak{u}\;\;\;\; \text{for all}\; s<r,\] then \[F_{t_1\cdots t_n r} (B)\in \mathfrak{u}.\] Therefore, \(\mathfrak{u}\in \mathcal{O}_{t_1\cdots t_n r}(B) \cap (B')^*\). This implies that \(\mathcal{O}_{t_1\cdots t_n r}(B)\) is dense and open. But, Since \(\mathcal{U}^*\) is topologically complete, \(\mathcal{U}^*_{na}\) is dense.
It follows from Item 1 that \(\mathcal{U}^*_{na}\in \Sigma^*\). Now to show the claim, it suffices to prove that for each \(\mathfrak{u}\in\mathcal{U}^*_{na}\!\) , \[T^*(\mathfrak{u}, \mathcal{U}^*\setminus\mathcal{U}^*_{na}) =0.\] Equivalently, we have to show that for each \(B\in \mathcal{B}\) and \(t_1, \dots, t_n, r\in \mathbb{Q}_0\), \[\begin{align} &\;T^*(\mathfrak{u}, \bigcap_{s<r} \big(F_{t_1\cdots t_n s} (B)\big)^* \cap \big(F^c_{t_1\cdots t_n r} (B)\big)^* ) \\ =& \;T^*(\mathfrak{u}, \bigcap_{s<r} \big(F_{t_1\cdots t_n s} (B)\big)^*) - T^*(\mathfrak{u}, \big(F_{t_1\cdots t_n r} (B)\big)^* )\\ =& \; \inf_{s<r}{\{T^*(\mathfrak{u}, \big(F_{t_1\cdots t_n s} (B)\big)^*) \}} - T^*(\mathfrak{u}, \big(F_{t_1\cdots t_n r} (B)\big)^* )\\ =& \; 0 \end{align}\]
Let \(\beta := T^*(\mathfrak{u}, \big(F_{t_1\cdots t_n r} (B)\big)^* )\). Then,
Claim: For each positive \(\epsilon \in \mathbb{Q}_0\), there exists \(s<r\) such that \[T^*(\mathfrak{u}, \big(F_{t_1\cdots t_n s} (B)\big)^* ) \leq \epsilon +\beta.\] Proof of claim: Suppose not. Then, for some \(\epsilon\), we have \[\lim_u T(w, F_{t_1\cdots t_n s} (B)) > \epsilon +\beta,\] for each \(s< r\). Now pick \(\epsilon' \in \mathbb{Q}_0\) such that \(0 \leq \beta< \epsilon' \leq \epsilon +\beta\). Then, for each \(s< r\), \[\{w\in \Omega\;|\; T(w, F_{t_1\cdots t_n s}(B))\geq \epsilon'\}\in \mathfrak{u}.\] Since \(\mathfrak{u}\) is a nested Archimedean ultrafilter, it follows that \[\{w\in \Omega\;|\; T(w, F_{t_1\cdots t_n r}(B))\geq \epsilon'\}\in \mathfrak{u}.\] So, \[\lim_\mathfrak{u} T(w, F_{t_1\cdots t_n r} (B)) = \beta \geq \epsilon',\] a contradiction.
This holds, since \((F_r(B))^*\cap \mathcal{U}^*_{na} = \bigcap_{s<r} ((F_s(B))^* \cap \mathcal{U}^*_{ua})\).
◻
In light of the above lemma, we define the ultrafilter extensions.
Definition 15 (Ultrafilter extensions). Given a Markov process \(\mathfrak{P} = \langle \Omega, \mathcal{B}, T \rangle\), we define the ultrafilter extension* of \(\mathfrak{P}\) as \(\mathfrak{Ue(P)} = \langle \mathcal{U}^*_{na}, \Sigma^*_{na}, T^*_{na}\rangle\) where*
\(\Sigma^*_{na} := \{ N\cap\mathcal{U}^*_{na} \;|\;N\in \Sigma^*\}\);
\(T^*_{na}:\mathcal{U}^*_{na}\times \Sigma^*_{na} \to [0, 1]\) such that for each \(\mathfrak{u}\in \mathcal{U}^*_{na}\) and \(N\in \Sigma^*\), \[T^*_{na} (\mathfrak{u}, N\cap\mathcal{U}^*_{na}) = T^*(\mathfrak{u}, N).\]
Equivalently, \(\mathfrak{Ue(P)}\) is a sub-process of \(\mathfrak{P}^* = \langle \mathcal{U}^*, \mathcal{B}^*, T^* \rangle\), introduced in Corollary 2. Notice that \(\mathfrak{Ue(P)} = \langle \mathcal{U}^*_{na}, \mathcal{B}^*_{na}, T^*_{na} \rangle\) where \(\mathcal{B}^*_{na}:= \{B^* \cap\mathcal{U}^*_{na}\;|\; B\in\mathcal{B} \}\).
In the following lemma, we show that the validity of formulas is reflected by the ultrafilter extensions. To prove this, we first examine the following lemma.
Lemma 10. Let \(\mathfrak{M} = \langle \Omega, \mathcal{B}, T, v \rangle\) be a model such that \(\mathcal{B}\) is countable. Consider the model \(\mathfrak{Ue(M)} = \langle \mathfrak{Ue(P)}, v^*_{na} \rangle\) where \(\mathfrak{Ue(P)} = \langle\mathcal{U}^*_{na}, \mathcal{B}^*_{na}, T^*_{na} \rangle\) and \(v^*_{na}\) is a valuation on \(\mathfrak{Ue(P)}\) defined as \[v^*_{na}(p):= \{ \mathfrak{u}\in\mathcal{U}^*_{na}\;|\; v(p) \in \mathfrak{u} \},\;\;\; \text{for each p\in \mathbb{P}}.\] Then, the following conditions hold:
\(v^*_{na}(p) = \mathcal{U}^*_{na} \cap (v(p))^*\in\mathcal{B}^*_{na}\), for each \(p\in \mathbb{P}\).
For each formula \(\varphi\) and \(\mathfrak{u}\in \mathcal{U}^*_{na}\), we have \[\mathfrak{Ue(M)}, \mathfrak{u}\vDash \varphi \;\;\text{if and only if}\;\; \{w\in \Omega\;|\; \mathfrak{M}, w\vDash \varphi\}\in \mathfrak{u}.\] Therefore, \([\![\varphi]\!]_{\mathfrak{Ue(M)}} = \mathcal{U}^*_{na} \cap ([\![\varphi]\!]_{\mathfrak{M}})^*\).
Proof.
This follows immediately by definition.
This can be shown by induction on the complexity of formulas. The basic and induction steps for Boolean connectives are clear. We assume that the induction hypothesis holds for \(\psi\). Now for \(\varphi= L_r \psi\), we have \[\begin{align} [\![ L_r \psi]\!]_{\mathfrak{Ue(M)}} &= \{\mathfrak{u}\in\mathcal{U}^*_{na} \;|\; T^*_{na}(\mathfrak{u}, [\![\psi]\!]_{\mathfrak{Ue(M)}})\geq r\}\\ &= \{\mathfrak{u}\in \mathcal{U}^*_{na} \;|\; T^*(\mathfrak{u}, \;\mathcal{U}^*_{na} \cap ([\![\psi]\!]_{\mathfrak{M}})^*)\geq r\}, \;(\text{by induction hypothesis for \psi})\\ &= \{\mathfrak{u}\in \mathcal{U}^*_{na} \;|\; T^*(\mathfrak{u}, \;([\![\psi]\!]_{\mathfrak{M}})^*)\geq r\}, \;(\text{by Definition \ref{ultrafil} (2))}\\ &= \mathcal{U}^*_{na} \cap ([\![L_r \psi]\!]_{\mathfrak{M}})^*, \;(\text{by Lemma \ref{star} (3))}\\ &= \mathcal{U}^*_{na} \cap ([\![L_r \psi]\!]_{\mathfrak{M}})^*. \end{align}\]
◻
Lemma 11. Suppose \(\mathfrak{P} = \langle \Omega, \Sigma, T \rangle\) is a countably generated Markov processes. Then, for each formula \(\varphi\), \[\mathfrak{Ue(P)}\vDash \varphi \;\;\text{implies} \;\;\mathfrak{P}\vDash \varphi.\]
Proof. Assume the above claim is not true for some formula \(\varphi\) . Then by Proposition [validity] (2), there exists a countable subalgebra \(\mathcal{B}\) of \(\Sigma\) such that \(\langle \Omega, \mathcal{B}, T \rangle\nvDash \varphi\). Hence, for some model \(\mathfrak{M}= \langle \mathfrak{P}, v \rangle\) and \(w\in \Omega\), we have that \(\mathfrak{M}, w \nvDash \varphi\). So \(\emptyset \neq [\![\neg\varphi]\!]_{\mathfrak{M}} \in \mathcal{B}\). Now consider an ultrafilter \(\mathfrak{u}\in \mathcal{U}^*_{na}\) with \([\![\neg\varphi]\!]_{\mathfrak{M}} \in u\), which exists by Rasiowa–Sikorski Lemma. Then on the basis of Lemma 10 (2), we have \(\mathfrak{Ue(M)}, u \nvDash \varphi\), a contradiction. ◻
The proof of the above lemma easily yields the following corollary.
Corollary 3. Under the condition of the above corollary, for each formula \(\varphi\),
\(\mathfrak{P}\vDash \varphi\) implies \(\langle \mathcal{U}^*_{na}, \mathcal{B}^*_{na}, T^*_{na}\rangle \vDash \varphi.\)
We can conclude this section by the following lemma which shows that for a given theory \(\Gamma\), the class of all Markov processes in which \(\Gamma\) is valid is closed under the constructions introduced above.
Lemma 12. Assume that \(\Gamma\) is a set of formulas and let \(\mathcal{C}_\Gamma=\{\mathfrak{P} \mid \mathfrak{P}\models\Gamma\}\), then \(\mathcal{C}_\Gamma\) is closed under Markov sub-processes, event sub-processes, disjoint unions, zigzag morphisms and reflected by ultrafilter extensions of countably generated Markov processes2. Furthermore, \(\mathfrak{P}\in\mathcal{C}\) if and only if every countably generated event sub-process of \(\mathfrak{P}\) is in \(\mathcal{C}\).
Since the conditions stated in the above lemma are important conditions for proving the Goldblatt-Thomason theorem, we isolate those classes that satisfy the conditions of the above lemma.
Definition 16. Let \(\mathcal{C}\) be a class of Markov processes. The class \(\mathcal{C}\) is said to have the Goldblatt-Thomason property (GT-property for short) if it satisfies the conditions of Lemma 12.
In this section we prove the Goldblatt-Thomason theorem for probability logic. Motivated by the same theorem in the context of basic modal logic with Kripke semantics we consider the ultrafilter extension as replacement of ultraproduct construction. This also rooted back to the original paper of Goldblatt and Thomason [@gt:axiom75].
Recall that a class of Markov processes \(\mathcal{C}\) is closed under ultrafilter extensions, if for every countably generated Markov process \(\mathfrak{P}\), if \(\mathfrak{P}\in\mathcal{C}\), then \(\mathfrak{Ue(P)}\in\mathcal{C}\).
Theorem 2 (Goldblatt-Thomason Theorem). Let \(\mathcal{C}\) be a class of Markov processes that is closed under taking ultrafilter extensions. Then \(\mathcal{C}\) is P-definable if and only if it has the GT-property.
Proof. The implication from left to right follows directly from Lemma 12. For the converse direction, let \(Th(\mathcal{C})\) denote the set of all formulas of an arbitrary countable language \(\mathcal{L}\) that are valid in the class \(\mathcal{C}\). We show that \(Th(\mathcal{C})\) defines \(\mathcal{C}\), i.e., for any Markov processes \(\mathfrak{P} =\langle \Omega, \Sigma,T\rangle\), we have \[\mathfrak{P}\in \mathcal{C}\;\;\text{iff}\; \;\mathfrak{P} \vDash Th(\mathcal{C}).\]
By definition of \(Th(\mathcal{C})\), the forward implication is immediate. Hence, assume that \(\mathfrak{P} \vDash Th(\mathcal{C})\). By Proposition [validity], we may assume without loss of generality that \(\mathfrak{P} =\langle \Omega, \mathcal{B},T\rangle\), where \(\mathcal{B}\) is a countable Boolean algebra and \(\Sigma=\sigma(\mathcal{B})\).
Now consider the language \(\mathcal{L}_{\mathfrak{P}}\) consisting of propositional variables \(\{p_A\;|\; A\in \mathcal{B}\}\). Define a valuation \(v_{\mathfrak{P}}\) on \(\mathfrak{P}\) by setting \(v_{\mathfrak{P}}(p_A) = A\), for each \(A\in \mathcal{B}\). Let \(\mathfrak{M} = \langle \mathfrak{P}, v_{\mathfrak{P}}\rangle\) and let \(\Gamma = Th(\mathfrak{M})\) be the set of formulas valid in \(\mathfrak{M}\). Observe that \(\Gamma\) contains the following formulas \[\begin{align} \neg p_{\emptyset} \\ p_A\wedge p_B &\leftrightarrow p_{A\cap B}\\ p_A &\leftrightarrow \neg p_{A^c}\\ p_{F_rA} &\leftrightarrow L_r p_A \end{align}\] for each \(A, B \in \mathcal{B}\) and \(r\in \mathbb{Q}_0\). Moreover, if \(\varphi\in \Gamma\) then \(L_1\varphi\in \Gamma\).
Now for each \(w\in \Omega\), define \(\Gamma_w = \{ \gamma\in \mathcal{L}_{\mathfrak{P}} \;|\; \mathfrak{M}, w\vDash \gamma\}\). Clearly, \(Th(\mathcal{C})\subseteq \Gamma\subseteq \Gamma_w\).
Claim 1: \(\Gamma_w\) is finitely satisfiable in \(\mathcal{C}\).
Suppose otherwise. Then there exists a finite subset \(\Delta \subseteq \Gamma_w\) that is not satisfiable in \(\mathcal{C}\). By definition of \(Th(\mathcal{C})\), this implies \[\neg \bigwedge \Delta \in Th(\mathcal{C}) \subseteq \Gamma_w,\] contradicting \(\Delta\subseteq \Gamma_w\).
For each finite \(\Delta\subseteq \Gamma_w\), let \(\mathfrak{N}_\Delta= \langle \mathfrak{Q}_\Delta, v_\Delta\rangle\) be a model satisfying \(\Delta\) with \(\mathfrak{Q}_\Delta\in \mathcal{C}\). Define \(\mathfrak{N}'_w = (\mathfrak{Q}'_w, v_w)\) where \(\mathfrak{Q}'_w=\biguplus_{\Delta \subseteq \Gamma_w}\mathfrak{Q}_\Delta\in\mathcal{C}\) and \(v_w=\biguplus_{\Delta \subseteq \Gamma_w}v_\Delta\). Let \(\mathcal{B}_w = \{[\![\varphi]\!]_{\mathfrak{N}_w}|\; \varphi \in \mathcal{L}_{\mathfrak{P}}\}\), and define \(\mathfrak{N}_w =\mathfrak{N}'_w\upharpoonright_{\mathcal{B}_w}\). Then \(\mathfrak{N}_w\) is an event sub-process based on \(\mathfrak{Q}_w=(\mathfrak{Q}'_w)\upharpoonright_{\mathcal{B}_w}\in\mathcal{C}\). One can verify that \(\mathfrak{u}_w= \{[\![\varphi]\!]_{\mathfrak{N}_w}|\; \varphi \in \Gamma_w\}\) is a nested Archimedean ultrafilter over \(\mathcal{B}_w\). Hence, \(\mathfrak{u}_w \in \mathfrak{Ue}(\mathfrak{N}_w)\) and \(\mathfrak{Ue}(\mathfrak{Q}_w)\in \mathcal{C}\), since \(\mathcal{C}\) is closed under taking ultrafilter extensions. Moreover, by Lemma 10, \(\mathfrak{Ue}(\mathfrak{N}_w), \mathfrak{u}_w\vDash \Gamma_w\). Applying Lemma 3 to \(\Gamma\), we obtain a sub-model \(\mathfrak{M}'_w = \langle \mathfrak{P}'_w,v'_w\rangle\) with \(\mathfrak{P}'_w \in \mathcal{C}\) and \(\mathfrak{u}_w\in \mathfrak{M}'_w\) such that \(\mathfrak{M}'_w\vDash \Gamma\) and \(\mathfrak{M}'_w, \mathfrak{u}_w\vDash\Gamma_w\). Define \[\mathfrak{M}' = (\biguplus_{w \in \Omega} \mathfrak{M}_w)\upharpoonright_{\mathcal{B}'} = \langle \mathfrak{P}',v'\rangle,\] and \(\mathfrak{P}' = \langle \Omega', \mathcal{B}', T',v'\rangle\), where \(\mathcal{B}' = \{[\![\varphi]\!]_{\biguplus_{w \in \Omega}\mathfrak{N}_w}|\; \varphi \in \mathcal{L}_{\mathfrak{P}}\}\). Thus, \(\mathfrak{Ue}(\mathfrak{P'})\in \mathcal{C}\).
Claim 2: There is a zigzag morphism from \(\mathfrak{Ue}(\mathfrak{P}')\) to \(\mathfrak{Ue}(\mathfrak{P})\).
Define \(f: \mathfrak{Ue}(\mathfrak{P}') \to \mathfrak{Ue}(\mathfrak{P})\) by \(f(\mathfrak{u}') = \{A \in \mathcal{B}\;|\; \mathfrak{Ue}(\mathfrak{M}'), \mathfrak{u}' \vDash p_A\}\), for each \(\mathfrak{u}' \in \Omega'\).
\(Im(f)\subseteq\mathfrak{Ue}(\mathfrak{P})\): By the definition of \(\Gamma\) and this fact that \(p_A\to p_B \equiv \top\) for each \(A\subseteq B \in \mathcal{B}\), it is easy to see that \(f(\mathfrak{u}')\) is an ultrafilter over \(\mathcal{B}\), for each \(\mathfrak{u}' \in \Omega'\). To prove that it is a nested Archimedean ultrafilter, assume that \[F_{t_1\dots t_n s} A \in f(\mathfrak{u}') \; \; \; \; \; \forall s<r.\] Then, \[\mathfrak{Ue}(\mathfrak{M}), \mathfrak{u}' \vDash L_{t_1\dots t_n s} p_A \; \; \; \; \; \forall s<r.\] So we have \(\mathfrak{Ue}(\mathfrak{M}), \mathfrak{u}' \vDash L_{t_1\dots t_n r} p_A\) and by applying axiom 4 of \(\Gamma\), \(\mathfrak{Ue}(\mathfrak{M}), \mathfrak{u}' \vDash p_{F_{t_1\dots t_n r} A}\). So \(F_{t_1\dots t_n r} A\in f(\mathfrak{u}')\).
\(f\) is surjective: Let \(\mathfrak{u}\) be a nested Archimedean ultrafilter over \(\mathcal{B}\). Then, consider \(\mathfrak{v}:= \{[\![p_A]\!]_{\mathfrak{M}'}\;|\; A\in \mathfrak{u}\}\). We show that \(\mathfrak{v}\) is a nested Archimedean ultrafilter on \(\mathcal{B}'\). Since all formulas of \(\Gamma\) are valid in \(\mathfrak{M}'\), it follows that every formula \(\varphi\) in the language \(\mathcal{L}_{\mathfrak{P}}\) is logically equivalent to a propositional variable \(p_A\). Now since \(\mathfrak{u}\) is an ultrafilter over \(\mathcal{B}\), either \([\![p_A]\!]_{\mathfrak{M}'}\in \mathfrak{v}\) or \([\![p_A]\!]^c_{\mathfrak{M}'}\in \mathfrak{v}\). Also, if \([\![p_A]\!]_{\mathfrak{M}'} , [\![p_B]\!]_{\mathfrak{M}'} \in \mathfrak{v}\), then so \([\![p_A]\!]_{\mathfrak{M}'} \cap [\![p_B]\!]_{\mathfrak{M}'} = [\![p_{A\cap B}]\!]_{\mathfrak{M}'} \in \mathfrak{v}\). Moreover, since \(A\in \mathfrak{u}\) is non-empty, there exists \(w\in A\). Therefore, \([\![p_A]\!]_{\mathfrak{M}'} \in \mathfrak{u}_w = \{[\![\varphi]\!]_{\mathfrak{N}_w}|\; \varphi \in \Gamma_w\}\). This implies \([\![p_A]\!]_{\mathfrak{M}'}\neq\emptyset\). Hence \(\emptyset\not\in\mathfrak{v}\). Finally, to show that \(\mathfrak{v}\) is a nested Archimedean ultrafilter, let \(A\in \mathfrak{u}\) and \[F_{t_1\dots t_ns} [\![p_A]\!]_{\mathfrak{M}'}\in\mathfrak{v} \; \; \; \; \; \forall s<r.\] Then \[F_{t_1\dots t_ns} [\![p_A]\!]_{\mathfrak{M}'} = [\![p_{F_{t_1\dots t_ns} A}]\!]_{\mathfrak{M}'} \in \mathfrak{v} \; \; \; \; \; \forall s<r.\] Therefore, \[F_{t_1\dots t_ns} A\in \mathfrak{u} \; \; \; \; \; \forall s<r.\] But since \(\mathfrak{u}\) is a nested Archimedean ultrafilter, it follows that \(F_{t_1\dots t_nr} A\in \mathfrak{u}\). So, \([\![p_{F_{t_1\dots t_nr} A}]\!]_{\mathfrak{M}'} = F_{t_1\dots t_nr} [\![p_{ A}]\!]_{\mathfrak{M}'} \in \mathfrak{v}\).
\(f\) is a measurable zigzag morphism: We have to verify that for \(A^* = \{\mathfrak{u}\in \mathcal{U}^*_{na}\;|\; A\in \mathfrak{u}\}\), \(f^{-1}(A^*)\) is measurable and \[T'^*_{na}(\mathfrak{u}, f^{-1}(A^*)) = T^*_{na}(f(\mathfrak{u}), A^*) \;\;\;\;(\star)\] for each \(\mathfrak{u}\in \Omega'\). To see the measurability of \(f\), notice that \[f^{-1}(A^*)= \{\mathfrak{u}'\in \mathcal{U}'^*_{na} \; | \; [\![p_A]\!]_{\mathfrak{M}'} \in \mathfrak{u}'\} \in \mathcal{B}^*_{na}.\] On the other hand, to show \((\star)\), assume for some \(r\in \mathbb{Q}_0\), we have \[T'^*_{na}(\mathfrak{u}, f^{-1}(A^*)) = \lim_{\mathfrak{u}'} T'(w', [\![p_A]\!]_{\mathfrak{M}'}) \geq r.\] As \(\mathfrak{u}'\) is a nested Archimedean ultrafilter and \([\![p_{F_r A}]\!]_{\mathfrak{M}'} = [\![L_r p_{A}]\!]_{\mathfrak{M}'}\), we have \([\![p_{F_r A}]\!]_{\mathfrak{M}'} \in \mathfrak{u}'\). Therefore, \(F_r A \in f(\mathfrak{u}')\). So \(\mathfrak{Ue}(\mathfrak{M}), \mathfrak{u}'\vDash L_r p_A\) which implies that \[T_{\mathcal{G}}(f(\mathfrak{u}'), [\![p_A]\!]_{\mathfrak{Ue}(\mathfrak{M})}) = T_{\mathcal{G}}(f(\mathfrak{u}'), A^*)\geq r.\] Conversely, one can show that if \(T^*_{na}(f(\mathfrak{u}'), A^*)\geq r\), then so \(T'^*_{na}(\mathfrak{u}', f^{-1}(A^*))\geq r\). Thus, \((\star)\) is achieved.
Since \(f\) is a zigzag morphism, \(\mathfrak{Ue(P)}\in\mathcal{C}\). Moreover, as \(\mathcal{C}\) reflects ultrafilter extensions, it follows that \(\mathfrak{P}\in\mathcal{C}\). ◻
Here in this subsection, we show that the class of Harsanyi type spaces [@harsan:games68] is an important instance for a P-definable class which is closed under ultrafilter extensions, and has the GT-property.
Example 1. For a Markov process \(\mathfrak{P}=\langle{\Omega, \Sigma, T}\rangle\) and \(w\in \Omega\) let \[[T(w)] = \{w'\in \Omega \mid T(w)=T(w')\}.\] Recall that a Markov process \(\mathfrak{P}\) is of Harsanyi type* if \(T(w,E)=1\), for each \(w\in\Omega\) and \(E\in\Sigma\) with \([T(w)]\subseteq E\). Note that \([T(w)]\) is not necessarily in \(\Sigma\), unless \(\Sigma\) is countably generated [@zhou:hars14]. In fact in case of countably generated Markov process \(\mathfrak{P}=\langle\Omega,\mathcal{B},T\rangle\), \[\begin{align} \label{t40w41} [T(w)] & = \bigcap_{B\in \mathcal{B}} \{w'\in \Omega\;|\; T(w)(B) = T(w')(B) \}\\ &= \bigcap_{B\in \mathcal{B}} \bigcap_{r\in \mathbb{Q}_0} \{w'\in \Omega\;|\; T(w)(B)\geq r\leftrightarrow T(w')(B)\geq r \}. \end{align}\tag{1}\] We denote the class of all Harsanyi type spaces by \(\mathcal{H}ar\).*
Assume that \(\mathfrak{P}\) is a countably generated Harsanyi type space. Then \(\mathfrak{P}\in\mathcal{H}ar\) if and only if the following set of formulas is valid in \(\mathfrak{P}\): \[\Gamma_{har}= \{L_rp\to L_1L_rp \mid r\in\mathbb{Q}_0 \} \cup \{\neg L_rp\to L_1\neg L_rp \mid r\in\mathbb{Q}_0 \}.\]
Proof. It is known that,[@zhou:hars14], these formulas are valid on any Harsanyi type space.
Now assume that \(\mathfrak{P}=\langle{\Omega,\Sigma, T}\rangle\) is a countably generated Markov process which is not Harsanyi type. Hence, there is \(w\in\Omega\) such that \(T(w)([T(w)])<1\). Therefore, \(T(w)([T(w)]^c)>0\). Let \(\Sigma=\sigma(\mathcal{B})\) where \(\mathcal{B}\) is countable. By 1 , we have \[[T(w)]^c = \bigcup_{B\in \mathcal{B}} \bigcup_{r\in \mathbb{Q}_0} \{w'\in \Omega\;|\; T(w)(B)\geq r\leftrightarrow T(w')(B)\geq r \}^c.\] Thus, there are \(B\in \mathcal{B}\) and \(r \in \mathbb{Q}_0\) such that either \(T(w)(B) \geq r\), while \(T(w)((F_r (B))^c) >0\) or \(T(w)(B)< r\), while \(T(w)(F_r (B)) >0\). In either of these cases, if we define a valuation \(v\) over \(\mathfrak{P}\) as \(v(p) = B\), then we turn \(\mathfrak{P}\) into a model \(\mathfrak{M}\) such that we have either \[\mathfrak{M},w\models L_rp\wedge \neg L_1L_rp \;\;\;\;\text{or} \;\;\;\; \mathfrak{M},w\models \neg L_rp\wedge L_1 \neg L_rp.\] ◻
The class of all countably generated Harsanyi type spaces is closed under ultrafilter extensions.
Proof. Assume that \(\mathfrak{P}=\langle\Omega,\mathcal{B},T\rangle\) is a Harsanyi type space with \(\mathcal{B}\) countable. Let \(\mathfrak{u}\in\mathcal{U}^*_{na}\). Then \[\begin{align} [T_{na}^*(\mathfrak{u})] & = \bigcap_{B^*\in \mathcal{B}^*_{na}} \{\mathfrak{u}'\in \mathcal{U}^*_{na}\;|\; T^*_{na}(\mathfrak{u}, B^*) = T^*_{na}(\mathfrak{u}' ,B^*) \}\\ &= \bigcap_{B^*\in \mathcal{B}^*_{na}} \bigcap_{r\in \mathbb{Q}_0} \{\mathfrak{u}'\in \mathcal{U}^*_{na}\;|\; T^*_{na}(\mathfrak{u} ,B^*)\geq r\leftrightarrow T^*_{na}(\mathfrak{u}',B^*)\geq r \}. \end{align}\] Now for \(B\in\mathcal{B}\) and \(r\in\mathbb{Q}_0\) there are two cases to consider.
Case 1: \(T^*_{na}(\mathfrak{u},B^*)< r\). In this case \[\begin{align} \{\mathfrak{u}'\in \mathcal{U}^*_{na}\;|\; T^*_{na}(\mathfrak{u} ,B^*)\geq r\leftrightarrow T^*_{na}(\mathfrak{u}',B^*)\geq r \} & =\{\mathfrak{u}'\in \mathcal{U}^*_{na}\;|\; T^*_{na}(\mathfrak{u}',B^*)< r \}\\ & = \{\mathfrak{u}'\in \mathcal{U}^*_{na}\;|\; (F_r(B))^c \in\mathfrak{u'}\}. \end{align}\] So \[\begin{align} T^*_{na}(\mathfrak{u}, \{\mathfrak{u}'\in \mathcal{U}^*_{na}\;|\; T^*_{na}(\mathfrak{u}',B^*)< r \}) &= \lim_{\mathfrak{u}} T(w,(F_r(B))^c) \end{align}\] On the other hand \(T^*_{na}(\mathfrak{u},B^*) =\lim_{\mathfrak{u}} T(w,B)<r\). Therefore \(\{w\in\Omega \; \mid\; T(w,B)<r\}\in\mathfrak{u}\). Notice that since \(\mathfrak{P}\) is Harsanyi, \[\{w\in\Omega \mid T(w,B)<r\} \subseteq \{w\in\Omega \mid T(w,(F_r(B))^c)=1\}\in\mathfrak{u}.\] Thus \(\lim_{\mathfrak{u}} T(w,(F_r(B))^c) =1\).
Case 2: \(T^*_{na}(\mathfrak{u},B^*)\geq r\). In this case we have \[\begin{align} \{\mathfrak{u}'\in \mathcal{U}^*_{na}\;|\; T^*_{na}(\mathfrak{u} ,B^*)\geq r\leftrightarrow T^*_{na}(\mathfrak{u}',B^*)\geq r \} & =\{\mathfrak{u}'\in \mathcal{U}^*_{na}\;|\; T^*_{na}(\mathfrak{u}',B^*)\geq r \}\\ & = \{\mathfrak{u}'\in \mathcal{U}^*_{na}\;|\; F_s(B) \in\mathfrak{u'}, \; \forall s<r\}\\ & = \{\mathfrak{u}'\in \mathcal{U}^*_{na}\;|\; F_r(B) \in\mathfrak{u'}\}. \end{align}\] We also have \(T^*_{na}(\mathfrak{u},B^*) =\lim_{\mathfrak{u}}T(w,B) >s\), for each \(s<r\). So, \[\{w\in\Omega \mid T(w,B)> s\}\subseteq\{w\in\Omega \mid T(w,B)\geq s\}\in\mathfrak{u}, \; \; \forall s<r.\] Hence \(\{w\in\Omega \mid T(w,B)\geq r\} \in\mathfrak{u}\), since \(\mathfrak{u}\) is a nested Archimedean ultrfilter. Again this yields that \(\{w\in\Omega \mid T(w,F_r(B)) =1 \}\in\mathfrak{u}\), and \(\lim_{\mathfrak{u}} T(w,F_r(B)) =1\). The above argument shows that \(T^*_{na}(\mathfrak{u}, (F_r(B))^*)=1\).
From both cases we conclude that \[T^*_{na}(\mathfrak{u},\{\mathfrak{u}'\in \mathcal{U}^*_{na}\;|\; T^*_{na}(\mathfrak{u} ,B^*)\geq r\leftrightarrow T^*_{na}(\mathfrak{u}',B^*)\geq r \})=1,\] for each \(B\in\mathcal{B}\) and \(r\in\mathbb{Q}_0\). Thus \(T^*_{na}(\mathfrak{u},[T^*_{na}(\mathfrak{u})])=1\). ◻
The class \(\mathcal{H}ar\) has the GT-property.
Proof. We only show that \(\mathcal{H}ar\) reflects the ultrafilter extensions, since the other properties can be easily shown. Assume that \(\mathfrak{Ue(P)}=\langle \mathcal{U}^*_{na}, \Sigma^*,T^*_{na}\rangle \in \mathcal{H}ar\) for a countably generated \(\mathfrak{P}=\langle\Omega,\Sigma,T\rangle\). Then \(\mathfrak{Ue(P)}\models\Gamma_{har}\). So, by Lemma 11, we have \(\mathfrak{P}\models\Gamma_{har}\). But, since \(\mathfrak{P}\) is countably generated by Lemma [har32def], we conclude that \(\mathfrak{P}\in\mathcal{H}ar\) ◻
Corollary 4. The class \(\mathcal{H}ar\) is P-definable.
In this section, we study an alternative version of the Goldblatt-Thomason theorem for the class of finite Markov processes with rational Markov kernels, denoted by \(\mathrm{FMP}_{\mathbb{Q}_0}\). This important subclass of Markov processes can be also seen as a natural generalization of finite Kripke structures for which there exists a version of the Goldblatt-Thomason theorem [@van1988notes]. So it would be natural to investigate a variant of this theorem for \(\mathrm{FMP}_{\mathbb{Q}_0}\). So throughout this section, by a finite process we mean a Markov process \(\mathfrak{P}=\langle\Omega, \mathcal{P}(\Omega), T\rangle\), where \(\Omega\) is finite and \(T(w,w'):= T(w,\{w'\})\in\mathbb{Q}_0\).
One can associate to any finite Markov process \(\mathfrak{P}=\langle\Omega, \mathcal{P}(\Omega), T\rangle\) a finite directed graph (or Kripke frame) \((\Omega,R_\mathfrak{P})\), which enables us to translate certain model theoretic concepts of probability logic into the corresponding notions of basic modal logic.
Definition 17. Let \(\mathfrak{P}=\langle\Omega, \mathcal{P}(\Omega), T\rangle\) be a finite Markov processes. Define a binary relation \(R_\mathfrak{P}\subseteq\Omega\times\Omega\) as \[wR_\mathfrak{P}w' \; \text{ if and only if } \; T(w,w')>0.\]
Let \(R_\mathfrak{P}(w)=\{w' \mid wR_\mathfrak{P}w'\}\). Then we have \(T(w,R_\mathfrak{P}(w))=1\), for each \(w\in\Omega\). Assume that \(\bar{R}_\mathfrak{P}\) is the reflexive and transitive closure of \(R_\mathfrak{P}\). Then for each \(w'\in \bar{R}_\mathfrak{P}(w)\) we have \(R_\mathfrak{P}(w')\subseteq \bar{R}_\mathfrak{P}(w)\). So, \(T(w',\bar{R}_\mathfrak{P}(w))=1\), for each \(w'\in \bar{R}_\mathfrak{P}(w)\). Hence one can consider the sub-processes \[\mathfrak{P}_w=\langle \bar{R}_\mathfrak{P}(w), \mathcal{P}(\bar{R}_\mathfrak{P}(w)) , T\upharpoonright_{\bar{R}_\mathfrak{P}(w)}\rangle.\] \(\mathfrak{P}_w\) serves as a point-generated sub-frame of \((\Omega,R_\mathfrak{P})\).
A Markov process \(\mathfrak{P}\) is called a point-generated process if there is \(w\in \Omega\) such that \(\mathfrak{P}=\mathfrak{P}_w\).
Note that if \(\mathfrak{P}_w\) is a point generated finite process, then \(\mathfrak{P}_w\models\varphi\) if and only if \(\mathfrak{P}_w,w\models L_1^k\varphi\) for some \(k\geq 0\).
Recall that for directed graph \((\Omega, R_\mathfrak{P})\) and \(w,v\in\Omega\) the distance between \(w,v\), denoted by \(d(w,v)\), is the length of the shortest path from \(w\) to \(v\) if there exists a path between them and \(\infty\) if there is no such path. Then, for \(n\geq0\) by \({R}_\mathfrak{P}(w)\upharpoonright_n\) we mean the set of all \(v\in\Omega\) with \(d(w,v)\leq n\).
Below we define the notion of a local \(n\)-zigzag morphism. Before defining this notion notice that for two finite processes \(\mathfrak{P}=\langle\Omega,\mathcal{P}(\Omega),T\rangle\) and \(\mathfrak{P}'= \langle\Omega',\mathcal{P}(\Omega'),T'\rangle\) the function \(f:\Omega\to\Omega'\) is a zigzag morphism if it is surjective and for each \(z\in\Omega\) and \(z'\in\Omega'\) we have \[\label{n32zig32equ} T(z,f^{-1}(z')) = T'(f(z),z').\tag{2}\]
Also note that any finite Markov process \(\mathfrak{P}\) is a zigzag image of the disjoint union of its point-generated sub-processes, i.e., there is a zigzag morphism \(f:\biguplus_{w\in\Omega}\mathfrak{P}_w \to \mathfrak{P}\), where for each \(v\in \biguplus_{w\in\Omega}\mathfrak{P}_w\), \(f(v)\) is equal to its corresponding state in \(\Omega\).
Definition 18 (Local \(n\)-Zigzag). Let \(\mathfrak{P}_w\) and \(\mathfrak{P}'_{w'}\) be two finite point generated processes. A local \(n\)-zigzag function, for \(n\geq 0\) is a function \(f:\Omega\to\Omega'\) such that \({R'}(w')\upharpoonright_n \subseteq Img(f)\) and (2 ) holds for all \(z\in {R}(w)\upharpoonright_n\) and \(z'\in {R'}(w')\upharpoonright_n\).
Likewise a local \(n\)-zigzag morphism from \(\mathfrak{M}=\langle\mathfrak{P}_w,v\rangle\) to \(\mathfrak{M}'=\langle\mathfrak{P}'_{w'},v'\rangle\) is a local \(n\)-zigzag morphism \(f\) from \(\mathfrak{P}_w\) to \(\mathfrak{P}'_{w'}\) such that \(v(p)= f^{-1}(v'(p))\), for each \(p\in\mathbb{P}\).
We recall that \(deg_p(\varphi)\in\mathbb{N}\) is defined inductively as follows:
\(deg_p(q) =0\), for \(q\in\mathbb{P}\),
\(deg_p(\neg\varphi) = deg_p(\varphi)\),
\(deg_p(\varphi\wedge\psi) = \max{(deg_p(\varphi), deg_p(\psi))}\),
\(deg_p(L_r\varphi) = deg_p(\varphi)+1\).
Lemma 13. Assume that \(\mathfrak{M}_w=\langle\Omega,\mathcal{P}(\Omega),T,v\rangle\) and \(\mathfrak{M}'_{w'}=\langle \Omega',\mathcal{P}(\Omega'), T',v'\rangle\) are two point-generated models and \(f:\Omega\to \Omega'\) is a local \(n\)-zigzag morphism. Then \[\mathfrak{M},w\models\psi \; \text{ if and only if } \; \mathfrak{M}',f(w)\models\psi,\] for each \(\psi\) with \(deg_p(\psi)\leq n\).
Proof. We prove it by induction on \(n\) and complexity of \(\psi\). We only prove the induction step for \(L_r\theta\), assuming \(deg_p(\theta)\leq n\). Suppose that \(f\) is a local \((n+1)\)-zigzag morphism. Then by induction hypothesis, we have \[\llbracket\theta\rrbracket_{\mathfrak{M}}\cap R(w) = f^{-1}(\llbracket\theta\rrbracket_{\mathfrak{M}'}\cap R'(f(w))),\] since for each \(z\in R(w)\), the function \(f\upharpoonright_{\bar{R}(z)}: \bar{R}(z) \to \bar{R}'(f(z))\) is a local \(n\)-zigzag morphism between \(\mathfrak{P}_z\) and \(\mathfrak{P}'_{f(z)}\). Hence, \[T(w,\llbracket\theta\rrbracket_{\mathfrak{M}}) = T(w,\llbracket\theta\rrbracket_{\mathfrak{M}}\cap R(w)) = T(f(w), \llbracket\theta\rrbracket_{\mathfrak{M}'}\cap R'(f(w)) ) = T(f(w),\llbracket\theta\rrbracket_{\mathfrak{M}'}).\] But this implies \[\mathfrak{M},w\models L_r\theta \; \text{ if and only if } \mathfrak{M}',f(w)\models L_r\theta.\] ◻
Below we prove a version of the Goldblatt-Thomason theorem for a class of finite Markov processes with rational probabilities. Before stating the theorem we isolate an important property which is necessary for a subclass \(\mathcal{C}\) of \(\mathrm{FMP}_{\mathbb{Q}_0}\) to be definable.
Definition 19. Let \(\mathcal{C}\) be a subclass of \(\mathrm{FMP}_{\mathbb{Q}_0}\). We say that \(\mathcal{C}\) is closed under local zigzag morphism if for each point-generated process \(\mathfrak{P}_w\) we have \(\mathfrak{P}_w\in\mathcal{C}\) whenever for each \(n>0\) there is a point-generated process \(\mathfrak{P}'_n\in\mathcal{C}\) where there is a local \(n\)-zigzag from \(\mathfrak{P}'_n\) to \(\mathfrak{P}\).
Let \(\Gamma\) be a set of formulas and assume that \(\mathcal{C}\) is the class of all finite Markov processes \(\mathfrak{P}\) in which \(\Gamma\) is valid. Then \(\mathcal{C}\) is closed under local zigzag morphisms.
Proof. Assume that \(\mathfrak{P}_w= \langle\Omega_w,\mathcal{P}(\Omega_w),T\rangle\) is a point generated Markov process in \(\mathrm{FMP}_{\mathbb{Q}_0}\) such that it is an image of local zigzag morphisms. We have to show that \(\mathfrak{P}_w\models\Gamma\). Assume not. Then for some \(\varphi\in\Gamma\) we have \(\mathfrak{P}_w\not\models\varphi\). Hence there exist \(\mathfrak{M}=\langle \mathfrak{P}_w,v\rangle\) and \(k\geq 0\) such that \(\mathfrak{M},w\not\models L_1^k\varphi\). Now take \(n\geq \max{(|\Omega_w|, deg_p(L_1^k\varphi))}\), \(\mathfrak{P}_{w'}\in\mathcal{C}\) and \(f:\mathfrak{P}_{w'}\to \mathfrak{P}_w\) a local \(n\)-zigzag morphism. By the choice of \(n\), we conclude that \(f\) is a surjection. Moreover, we can define \(v'\) on \(\mathfrak{P}_{w'}\) such that \(f\) is a local \(n\)-zigzag morphism from \(\mathfrak{M}'=\langle\mathfrak{P}_{w'},v'\rangle\) to \(\mathfrak{M}=\langle\mathfrak{P}_w,v\rangle\). Hence in the light of Lemma 13, we have \(\mathfrak{M}',w'\not\models L_1^k\varphi\). Therefore, \(\mathfrak{P}_{w'}\not\models\varphi\), a contradiction. ◻
Theorem 3. Assume that \(\mathcal{C}\) is a subclass of \(\mathrm{FMP}_{\mathbb{Q}_0}\). Then \(\mathcal{C}\) is definable if and only if it is closed under generated sub-processes, finite disjoint unions, and local zigzag morphisms.
Proof. The nontrivial direction is the right-to-left one, so assume that \(\mathfrak{P}\) is a finite process with \(\mathfrak{P}\models Th(\mathcal{C})\). We have to show that \(\mathfrak{P}\in\mathcal{C}\).
By Remark [point32generate] and since \(\mathcal{C}\) is closed under finite disjoint unions, without loss of generality, we can assume that \(\mathfrak{P}\) is point-generated. Suppose \(\Omega=\{w_0,w_1,\dots,w_m\}\) where \(\mathfrak{P}=\mathfrak{P}_{w_0}\). Let \(n>0\) be arbitrary. Consider the language \(\mathcal{L}_\mathfrak{P}=\{p_0,\dots, p_m\}\), and the valuation \(v\) on \(\mathfrak{P}\) as \(v(p_i) =\{w_i\}\), for each \(1\leq i\leq n\). Define the following formulas:
i. \(p_{_0}\).
ii. \(L_r p_{_i} \wedge M_r p_{_i}\), if \(T(w_0,w_i)=r\).
iii. \(L_1^k(p_0\vee\dots\vee p_m)\), for \(0\leq k\leq n\).
iv. \(L_1^k (p_i\to \neg p_j)\), for \(0\leq k\leq n\) and \(i\neq j\).
v. \(L_1^k(p_i\to (L_r p_{_j} \wedge M_r p_{_j}))\), for \(0\leq k\leq n\) if \(T(w_i,w_j)=r\).
While (i) and (ii) are satisfied in \(w_0\), the other ones are valid on \(\mathfrak{M}\), and in particular, are satisfied in \(w_0\). Let \(\varphi_{n,w_0}\) be the conjunction of the above formulas. Clearly, \(\varphi_{n,w_0}\in Th(\mathcal{C})\) and is satisfiable in \(\mathcal{C}\), as otherwise \(\neg\varphi_{n,w_0}\in Th(\mathcal{C})\), which is a contradiction. So there exists \(\mathfrak{N}_n=\langle\mathfrak{P}'_n,v'\rangle\) with \(\mathfrak{P}'_n=\langle\Omega',\mathcal{P}(\Omega'),T'\rangle\in\mathcal{C}\) such that \(\mathfrak{N}_n,z_0\models\varphi_{n,w_0}\) for some \(z_0\in\Omega'\). Again, without loss of generality, we can assume that \(\mathfrak{P}'\) is point-generated with \(\mathfrak{P}'=\mathfrak{P}'_{z_0}\).
Now define \(f_n:\Omega'\to \Omega\) as \(f_n(z) =w_i\) if \(z\in R(v_0)\upharpoonright_n\) and \(\mathfrak{N}_n,z\models p_i\). Otherwise let \(f_n(z)=w_0\). We show that \(f_n\) is a local \(n\)-zigzag morphism.
\(f_n\) is well-defined: assume that \(z\in R(z_0)\upharpoonright_n\). Hence \(d(v_0,z)=k\leq n\), and \(\mathfrak{N}_n,v_0\models L_1^k (p_0\vee\dots \vee p_m)\). Therefore, this implies that \(\mathfrak{N}_n,z\models (p_0\vee\dots \vee p_m)\). Thus, there is \(0\leq i\leq m\) such that \(\mathfrak{N}_n,z\models p_i\). Furthermore, for \(i\neq j\) we have \(\mathfrak{N}_n,z_0\models L_1^k(p_i\to\neg p_j)\) which implies that \(\mathfrak{N}_n,z\models p_i\to \neg p_j\). So we conclude that there is a unique \(i\) such that \(f_n(z)=w_i\).
\(Img(f_n)\subseteq R(w_0)\upharpoonright_n\): Assume that \(w\in\Omega\) and \(d(w_0,w)=k\leq n\). So there are \(w_{j_1},\dots, w_{j_k}\in\Omega\) with \(w_0Rw_{j_1}\dots Rw_{j_k}\) and \(w_{j_k}=w\). Suppose that \(T(w_{j_i},w_{j_{i+1}})=r_i>0\), for each \(0\leq i\leq k-1\). Since \(\mathfrak{M},w_0\models L_{r_1}p_{j_1} \wedge L_1(p_{j_1}\to L_{r_2}p_{j_2})\), it follows that \(\mathfrak{N}_n,v_0\models L_{r_1}p_{j_1} \wedge L_1(p_{j_1}\to L_{r_2}p_{j_2})\). Hence, \(T'(z_0,\llbracket p_{j_1}\rrbracket_{\mathfrak{N}_n})=r_1>0\) and \(T'(z_0,\llbracket p_{j_1}\to L_{r_2}p_{j_2}\rrbracket_{\mathfrak{N}_n})=1\). So there is \(z_1\in\Omega'\) such that \(T'(z_0,z_1)>0\) and \(\mathfrak{N}_n,z_1\models p_{i_1}\wedge L_{r_2}p_{j_2}\). Again, since \(\mathfrak{M},w_0\models L_1^2(p_{j_2}\to L_{r_3}p_{j_3})\), it follows that \(T'(z_1,\llbracket p_{j_2}\to L{r_3}p_{j_3}\rrbracket_{\mathfrak{N}_n})=1\). Thus there is \(z_2\in\Omega'\) such that \(\mathfrak{N},z_2\models p_{i_2}\) and \(T'(z_1,z_2)>0\). Continuing this method, one can find a sequence \(z_0R'z_1\dots R'z_{i}\) such that \(\mathfrak{N}_n,z_i\models p_{j_i}\) for each \(0<i\leq k\). So, \(f_n(z_k)=w\).
\(f_n\) is a local \(n\)-zigzag morphism: note that the measurability of \(f_n\) is automatic. So, we only need to show that \[T'(z,f_n^{-1}(w)) = T(f_n(z),w),\] for each \(w\in R(w)\upharpoonright_n\) and \(z\in R'(z_0)\upharpoonright_n\). Assume that for some \(0\leq i,j\leq m\) we have \(\mathfrak{N},z\models p_i\) and \(\mathfrak{M},w\models p_j\). Thus \(f(z) = w_i\). If \(T(w,w_i)=r\), then for each \(0\leq k\leq n\), \[\mathfrak{M},w_0\models L_1^k(p_j\to (L_r p_i\wedge M_r p_i)).\] So \[\mathfrak{N}_n,z_0\models L_1^k(p_j\to (L_r p_i\wedge M_r p_i)).\] Hence, \[T'(z,\llbracket p_i\rrbracket_{\mathfrak{N}_n})=T'(z,f_n^{-1}(w))=r.\]
Since \(\mathfrak{P}'_n\in\mathcal{C}\) and \(f_n:\mathfrak{P}'_n\to\mathfrak{P}\) is a local \(n\)-zigzag morphism, it follows that \(\mathfrak{P}\in\mathcal{C}\), as required. ◻
In this paper, we established a Goldblatt-Thomason-style theorem for probability logic, characterizing the classes of Markov processes definable in probability logic via suitable model-theoretic closure properties. We also obtained a corresponding result for finite Markov processes. These results connect probabilistic modal logic with the classical model-theoretic theory of definability.
A natural direction for future research is to extend these results to infinitary probability logics, which allow countable conjunctions and disjunctions and whose expressive power is closely related to the \(\sigma\)-additivity of probability measures. As shown in [@ChopoghlooPourmahdian2024], important stochastic properties of Markov processes, such as stationarity, invariance, irreducibility, and recurrence, are expressible in this setting. This indicates that infinitary probability logics provide a more suitable framework for capturing genuinely measure-theoretic probabilistic phenomena. Accordingly, an important problem for future work is to establish a Goldblatt-Thomason-style theorem for infinitary probability logic and to characterize the associated model-theoretic closure conditions for definability.
[@*]