1 Introduction↩︎

We study the definability of functional properties in the simplest modal-temporal language, obtained by adding the temporal operators \(G\) and \(H\) to the basic modal language with \(\Box\). This language is the standard bimodal combination of modal and tense logic (see e.g. [1]); in [2] it was given a functional interpretation and denoted \(L_{T\times W}\).

Throughout the paper we consider two semantic interpretations of the temporal operators \(G,H\): the standard interpretation, which follows the original semantics (including the current instant when a reflexive loop is present), and the strict interpretation, which always excludes the current instant. For clarity, we keep the notation \(G,H\) for the standard interpretation, and denote the strict interpretation by \(G^{\ast},H^{\ast}\). This notational convention allows us to compare both interpretations without mixing them within the same formula.

In [2], [3], the study of functional properties using \(L_{T\times W}\) was restricted to strict linear orders and global constraints—such as totality or the Uniform Domain (U-Dom) property. Two questions remained open: whether these properties are definable in isolation, and how their definability varies across a wider range of order structures

The present study addresses these questions by providing a systematic account of the expressive limits of \(L_{T\times W}\) across a wide range of order structures, including (strict) linear orders, partial orders, and (strict) preorders. We examine these functional properties independently of the global conditions previously required, such as totality or the Uniform Domain (U-Dom) property, to determine if they are definable in isolation. The functional properties under study are: totality, non-totality, injectivity, surjectivity, monotonicity, strict monotonicity, antitonicity, strict antitonicity, and constancy.

Rather than a mere descriptive map, our approach probes the expressive boundaries of the language to identify how its inherent limitations can be mitigated. To this end, we investigate to what extent the definability range can be expanded through semantic modifications and structural restrictions, without altering the syntax itself.

Our analysis proceeds in two stages. First, we establish the definability limits of \(L_{T\times W}\) in the so called arbitrary multiflow ordered setting. In this environment, the modal operators function as second-order quantifiers over the images of all functions simultaneously. To investigate this, we maintain a single \(L_{T\times W}\) language with its temporal operators \(G,H\), but consider two different semantic interpretations: the standard interpretation, for which we keep the notation \(G,H\), and the strict interpretation, which we denote by \(G^{\ast}, H^{\ast}\) for notational convenience¹. This notational convention allows us to compare both interpretations without mixing them within the same formula and demonstrate why they both fail within the multiflow architecture.

To overcome this without altering the syntax, we introduce a semantic refinement: minimal functional frames (the \(O^2\) family). By restricting each frame to a single accessibility function, we simplify the semantic landscape, allowing the second-order complexity of the multiflow to collapse into a first-order relational reading. Under this restriction, the advantage of the strict interpretation (\(G^\ast, H^\ast\)) over the standard one becomes evident, as it enables \(L_{T\times W}\) to achieve the same definability patterns as more complex indexed languages [4].

Interestingly, the same definability patterns are obtained when we impose the Uniform Domain (U-Dom) condition on the semantics of \(L_{T\times W}\), without abandoning the multiflow architecture. Indexed languages achieve the same result by syntactic means (explicit labels for functions), while U-Dom does it by domain uniformity. Minimal frames, which are a special case of U-Dom, achieve it by structural simplification. That three such different ways of controlling functional multiplicity lead to identical definability patterns shows that the expressive limitations of the original multiflow semantics arise from the indiscriminate quantification over many functions, not from any weakness of the operators of \(L_{T\times W}\).

Even after eliminating the interference between functions—whether by structural simplification, domain uniformity, or syntactic labels—a set of properties remains undefinable in all non-linear orders. This reveals that the lack of connectivity is a fundamental obstacle that persists regardless of how the original multiflow semantics is refined.

Methodologically, we establish undefinability for most properties by providing surjective p-morphisms that fail to preserve them. This method is conceptually rooted in the classical preservation theorems of modal logic [5], which show that surjective p-morphisms preserve validity and can therefore be used to prove undefinability. However, the functional semantics of \(L_{T\times W}\) requires extending those results to a non-Kripkean setting, where frames are equipped with both temporal relations and families of functions. Within this framework, we identify a significant exception: in the specific context of minimal functional frames, constancy remains invariant under such mappings. Consequently, we employ a distinct semantic equivalence argument to show that \(L_{T\times W}\) cannot distinguish between these functional behaviors.

The paper is organised as follows. Section 2 introduces the language \(L_{T\times W}\), its two temporal interpretations, and the algebraic semantics. Section 3 analyses definability in the ordered multiflow setting. Section 4 examines the gains obtained with minimal frames and compares the two temporal interpretations. Section 5 concludes and outlines directions for future work. Finally, detailed proofs of the results are deferred to the Appendix.

2 The Language \(L_{T\times W}\): Syntax, Semantics and Algebraic Characterisations↩︎

2.1 Notation and Order-Theoretic Preliminaries↩︎

In what follows, all domains and structures are assumed to be nonempty. For a binary relation \(R\) on a set \(A\), we write \[R(a) \;:=\; \{ a' \in A \mid (a,a') \in R \},\qquad R^{-1}(a) \;:=\; \{ a' \in A \mid (a',a) \in R \}\] for the sets of \(R\)-images and \(R\)-preimages of \(a\), respectively. To handle operators that exclude the evaluation point independently of the properties of \(R\) (such as reflexivity), we write \[R^{\bullet}(a) := R(a) \setminus \{a\}\] for each \(a \in A\). This notation is local: it removes only the point \(a\) itself from its own set of successors, leaving all other points unaffected.

When \(R\) is an order, we adopt standard order-theoretic notation. Let \(\le\) be a binary relation on a set \(X\); we call it an order when it is at least a preorder (reflexive and transitive). If \(\le\) is also antisymmetric, it is a partial order; if moreover it is total (\(x \le y\) or \(y \le x\) for all \(x, y \in X\)), it is a linear order. We denote by \(<\) the strict part of \(\le\), defined by \(x < y\) iff \(x \le y\) and \(x \neq y\). Dually, any irreflexive and transitive relation \(<\) is a strict preorder, which becomes a strict partial order if it is asymmetric, and a strict linear order if it satisfies trichotomy.

For any \(a \in A\) and \(X \subseteq A\), we employ the following operators: \[a\!\uparrow \;:=\; \{a' \mid a \leq a'\},\qquad a\!\uparrow^\ast \;:=\; \{a' \mid a < a'\}\] \[X\!\uparrow \;:=\; \bigcup_{a \in X} a\!\uparrow,\qquad X\!\uparrow^\ast \;:=\; \bigcup_{a \in X} a\!\uparrow^\ast\] with \(a\!\downarrow\) and \(a\!\downarrow^\ast\) defined dually (\(a\!\downarrow = \{a' \mid a' \leq a\}\), \(a\!\downarrow^\ast = \{a' \mid a' < a\}\)). Note that \(a\!\uparrow = a\!\uparrow^\ast \cup\, \{a\}\). By convention, \(\varnothing\!\uparrow = \varnothing\!\downarrow = \varnothing\!\uparrow^\ast = \varnothing\!\downarrow^\ast = \varnothing\). Furthermore, when \(R\) is an order \(\leq\), we have \(R(a) = a\!\uparrow\) and \(R^{\bullet}(a) = a\!\uparrow^\ast\). In linear orders, these operators coincide with standard interval notation, e.g., \(a\!\uparrow = [a, \rightarrow)\) and \(a\!\uparrow^\ast = (a, \rightarrow)\).

For a partial function \(f\colon A \rightharpoonup B\), we assume the standard definitions for totality, injectivity, surjectivity, and constancy. Regarding ordered structures, we refer to increasing and decreasing functions as monotonicity and antitonicity, respectively, including their strict variants.

We use function names (e.g., increasing) for classes of frames and in the text when referring to the behaviour of individual functions. Property names (e.g., monotonicity) are reserved for the logical notion of definability. Formula labels (e.g., \((Inc)\)) reflect the function name for consistency.

2.2 Syntax↩︎

Formulas of \(L_{T\times W}\) are generated by the grammar \[A ::= \bot \mid p \mid (A \to A) \mid \square A \mid G A \mid H A,\] where \(p \in \mathcal{V}\). The connectives \(\top, \land, \lor, \leftrightarrow, \lozenge, F, P\) are introduced by standard definitions.

Table [tab:intuitive] summarises the intended readings of the modal and temporal connectives. These readings correspond to the standard interpretation of the operators; the strict interpretation will be introduced semantically in Section 2.5.

Conn.	Informal reading	Meaning
\(G\)	Always in the future	\(A\) holds at every future moment.
\(H\)	Always in the past	\(A\) holds at every past moment.
\(F\)	Sometime in the future	There exists a future moment where \(A\) holds.
\(P\)	Sometime in the past	There exists a past moment where \(A\) holds.
\(\square\)	In all functional images	Every function applicable to the current state has an image satisfying \(A\).
\(\lozenge\)	In some functional images	There exists a function applicable to the current state whose image satisfies \(A\).

2.3 Semantics↩︎

Henceforth, we will simply say “functional frame” to refer to this notion, unless a distinction with the more specific formulations in [2] or [3] is required. The term “general” in Definition 1 emphasizes that, at this stage, the relations \(R_w\) are arbitrary and not yet restricted to any particular class of orders.

Note that the definition does not require \(\mathcal{F}\) to be closed under composition.

We use the term “arrow-style” to refer to inclusions comparing the image of an order segment, such as \(a\!\uparrow\), \(a\!\uparrow^{*}\), or interval notation, with another segment of the corresponding target order. These conditions take the schematic form \[\text{(per-function)}\quad f_{ww'}(X) \subseteq Y, \qquad\text{or}\qquad \text{(class-aggregate)}\quad \mathcal{F}_w(X) \subseteq Y,\] where \(X\) and \(Y\) are sets generated by the underlying order. The two forms correspond to two distinct readings: the per-function reading applies the inclusion separately to each accessibility function \(f_{ww'}\), while the class-aggregate reading compares instead the combined image \(\mathcal{F}_w(X)\) of all functions with source \(w\). We will specify which reading is intended whenever this affects the results.

2.4 Per-function characterisations↩︎

The following theorems establish the algebraic foundation for our definability results by relating functional properties to specific image-set inclusions. While the characterisations for linear orders (Theorem 1) extend the results in [3], their generalisation to preorders and posets (Theorem 2) follows the same logic of order preservation. In both cases, the proofs are straightforward verifications of set-theoretic inclusions under the \(\uparrow\) and \(\downarrow\) operators and are thus omitted.

The following theorem generalises the per-function characterisations for totality and surjectivity (items 1 and 3 of Theorem 1) to the multiflow setting. As will be seen, a similar generalisation is not possible for the remaining properties.

2.4.0.1 Expressive Limits.

The scope of arrow-style characterisations is strictly delimited by the connectivity of the underlying order. This approach is intentionally chosen because its reliance on upper and lower intervals matches the reach of the temporal operators in \(L_{T\times W}\). While more powerful frameworks exist, such as the equational approach in relation algebras (e.g., [6]) where injectivity is defined through composition and converse (\(f \circ f^{\smile} \subseteq I\)), these require a different modal basis. We discard such alternatives because they operate independently of the order structure; adopting them would necessitate a language with connectives that are not bound by temporal accessibility. Consequently, the arrow-style remains the only framework that is structurally compatible with the inherent locality of our temporal semantics.

2.5 Functional models and truth↩︎

We distinguish two analytical interpretations of the same language:

• The standard interpretation of \(G,H\) is given in Definition 3.

• The strict interpretation, denoted \(G^\ast,H^\ast\), evaluates \(G\) and \(H\) over the irreflexive core \(R_w^\bullet\) (see Section 2.1): \[h(G^\ast A) = \{t_w \mid R_w^\bullet(t_w) \subseteq h(A)\},\quad h(H^\ast A) = \{t_w \mid (R_w^\bullet)^{-1}(t_w) \subseteq h(A)\}.\]

In irreflexive frames, \(R_w = R_w^\bullet\), so both interpretations coincide.

Having established the general semantic framework, we now turn to definability, relating semantic properties of frames to syntactic characterisations.

3 Definability in the Arbitrary Ordered Multiflow Setting↩︎

To analyze the expressive limits of \(L_{T\times W}\), we first fix some notation. Let \(\mathbb{K}\) denote the class of all functional frames. We use \(\mathsf{O}\) for order types and \(P\) for functional properties. The expression \(\mathbb{K}^{\mathsf{O}}_{P}\) denotes the class of functional frames in \(\mathbb{K}^{\mathsf{O}}\) where the flows satisfy \(\mathsf{O}\) and the accessibility functions satisfy \(P\).

Consistent with our preliminary notation, we use property names (e.g., monotonicity, injectivity) when referring to the logical notion of definability, while function names (e.g., increasing, injective) describe the behavior of individual functions and identify the corresponding classes. For instance, if \(P\) is monotonicity, \(\mathbb{K}^{\mathsf{O}}_{\mathit{inc}}\) is the class of frames whose functions are increasing. Throughout the paper, we refer to these order types by their abbreviations: \(\mathsf{PRE}\) (preorder), \(\mathsf{sPRE}\) (strict preorder), \(\mathsf{PO}\) (partial order), \(\mathsf{LO}\) (linear order), and \(\mathsf{sLO}\) (strict linear order).

The collection of all such structures, where each flow is endowed with a fixed order type \(\mathsf{O}\) without further constraints, constitutes our primary object of study. We call this the arbitrary ordered multiflow setting: frames where each flow comes with a fixed order type \(\mathsf{O}\), but without any further restrictions—no limits on the number of flows or functions, no uniformity conditions, and no means to distinguish individual functions. This is the starting point for our analysis; it coincides with the semantics originally introduced in [2], [3], except that those works were restricted to strict linear orders.

The functional properties considered in this framework are all properties of a single function:

We begin by formalising the notion of definability.

Convention. When we say that a property \(P\) is (un)definable in an order type \(\mathsf{O}\), we mean that the subclass \(\mathbb{K}^{\mathsf{O}}_P\) is (un)definable in \(\mathbb{K}^{\mathsf{O}}\) (see Definition 5).

This convention is useful because it reflects the fact that definability in a restricted class \(\mathbb{K}^{\mathsf{O}}\) does not automatically transfer to a larger class. For example, totality is definable in \(\mathbb{K}^{\mathsf{sLO}}\), but it is not definable in the class of all functional frames \(\mathbb{K}\). In contrast, undefinability propagates upwards: if \(P\) is undefinable in \(\mathbb{K}^{\mathsf{O}}\), then it is also undefinable in any superclass of \(\mathbb{K}^{\mathsf{O}}\) (in particular, in \(\mathbb{K}\)). This is why, for instance, the undefinability of totality in \(\mathbb{K}^{\mathsf{sPRE}}\) implies its undefinability in all larger classes.

Proof:
By structural induction on \(A\). \(\blacksquare\)

Definability results will be established by providing explicit formulas for the intended properties. Conversely, with a single later exception, undefinability will be witnessed via surjective p-morphisms which, by inducing functional bisimulations (Lemma 1), ensure the preservation of validity.

Methodological Note. Undefinability will be witnessed via surjective p-morphisms \(\varphi: \Sigma \to \Sigma'\) between finite frames, where \(\Sigma\) satisfies a property \(P\) and \(\Sigma'\) does not. Since these p-morphisms induce functional bisimulations (Lemma 1), they ensure that no formula in \(L_{T\times W}\) can define \(P\).

Consequently, it suffices to present the relevant pairs of frames. For the sake of brevity, we employ Convention (RC) (Reflexive Closure) to adapt these counterexamples to reflexive classes. Detailed graphical representations and specific reading conventions are provided in the Appendix (see 5.3).

To facilitate the translation of functional properties into modal formulas, we begin with a simple set-theoretic observation.

Proof:
By Remark 1, the union \(\mathcal{F}_w(X)=\bigcup_{f\in\mathcal{F}_w} f(X)\) is disjoint; by Observation 1, we may equivalently write \(\mathcal{F}_w(X)=\bigcup_{t_w\in X} \mathcal{F}_w(\{t_w\})\).

Proof of (1): The following chain of equivalences holds: \[\begin{align} X\subseteq h(\square A) & \;\text{iff}\;\Big(\bigcup_{t_w\in X} \{t_w\}\Big)\subseteq h(\square A)\\ & \;\text{iff}\;\Big(\bigcup_{t_w\in X} \mathcal{F}_w(\{t_w\})\Big)\subseteq h(A)\\ & \;\text{iff}\;\mathcal{F}_w(X)\subseteq h(A). \end{align}\]

Proof of (2) (the proof of (3) is analogous): By Observation 1, \[\mathcal{F}_w(X)\!\uparrow^\ast = \bigcup_{t_w\in X} \mathcal{F}_w(\{t_w\})\!\uparrow^\ast.\] Then: \[\begin{align} \mathcal{F}_w(X)\!\uparrow^\ast\subseteq h(A) & \;\text{iff}\;\Big(\bigcup_{t_w\in X} \mathcal{F}_w(\{t_w\})\!\uparrow^\ast\Big)\subseteq h(A)\\ & \;\text{iff}\;\Big(\bigcup_{t_w\in X} \mathcal{F}_w(\{t_w\})\Big)\subseteq h(GA)\\ & \;\text{iff}\;\mathcal{F}_w(X)\subseteq h(GA). \end{align}\]

For \(\mathsf{PRE}, \mathsf{PO}\), and \(\mathsf{LO}\), the same proofs apply with \(\uparrow\) and \(\downarrow\) in place of \(\uparrow^\ast\) and \(\downarrow^\ast\).

Proof:
We divide the proof into positive cases (definability) and negative cases (undefinability).

i. Positive cases: Definability in linear and strict linear orders.

Totality. The formula \[(\mathit{Tot}): \square(Hp \land p \land Gp) \to (H\square p \land G\square p)\] defines \(\mathbb{K}^{\mathsf{sLO}^2}_{\mathit{tot}}\) in \(\mathbb{K}^{\mathsf{sLO}^2}\). In \(\mathsf{LO}^2\), reflexivity makes the conjunct \(p\) redundant, so the simplified formula \[(\mathit{Tot})^\circ: \square(Hp \land Gp) \to (H\square p \land G\square p)\] defines \(\mathbb{K}^{\mathsf{LO}^2}_{\mathit{tot}}\) in \(\mathbb{K}^{\mathsf{LO}^2}\) (the proof for totality in strict linear orders can be found in [3].)

Surjectivity. We show that the following formula defines \(\mathbb{K}^\mathsf{sLO}_{\mathit{surj}}\) in \(\mathbb{K}^\mathsf{sLO}\) (it is the same formula for \(\mathsf{LO}\)): \[(\mathit{Surj}) \quad (H\square p \land G\square p) \to \square(Hp \land Gp).\] \((\Rightarrow\)) Suppose that \(\Sigma\in \mathbb{K}^\mathsf{sLO}_\mathit{surj}\). Let \((\Sigma, h)\) be a model and let \(t_w\in {\cal C}\mathit{oord}_{\Sigma}\). Then: \[\begin{align} t_w \in h(H\square p \land G\square p) &\;\text{iff}\;t_w \in h(H\square p)\cap h(G\square p)\\ &\;\text{iff}\;t_w\!\downarrow^\ast \subseteq h(\square p)\;\text{and}\;t_w\!\uparrow^\ast\subseteq h(\square p) \\ &\;\text{iff}\; (t_w\!\downarrow^\ast\!\cup\, t_w\!\uparrow^\ast) \subseteq h(\square p)\\ &\;\text{iff}\;\mathcal{F}_w(t_w\!\downarrow^\ast)\cup\mathcal{F}_w( t_w\!\uparrow^\ast)\subseteq h(p) \quad\text{(Lemma~\ref{lem:image-modal-unified}(1))}\\ &\;\text{then}\;\mathcal{F}_w(\{t_w\})\!\downarrow^{\ast}\!\cup\,\mathcal{F}_w(\{t_w\})\!\uparrow^{\ast}\subseteq h(p) \quad\text{(Theorem~\ref{caracterizafunciones}(2))}\\ &\;\text{iff}\;\mathcal{F}_w(\{t_w\})\!\downarrow^{\ast}\subseteq h(p)\;\text{and}\;\mathcal{F}_w(\{t_w\})\!\uparrow^{\ast}\subseteq h(p)\\ &\;\text{iff}\;\mathcal{F}_w(\{t_w\})\subseteq h(Hp)\cap h(Gp) \quad\text{(Lemma~\ref{lem:image-modal-unified}(2),(3))}\\ &\;\text{iff}\;\mathcal{F}_w(\{t_w\})\subseteq h(Hp \land Gp) \\ &\;\text{iff}\;\{t_w\} \subseteq h(\square(Hp \land Gp)) \quad \text{(Lemma~\ref{lem:image-modal-unified}(1))}\\ &\;\text{iff}\;t_w \in h(\square(Hp \land Gp)). \end{align}\] Hence \((\mathit{Surj})\) is valid in \(\Sigma\).

(\(\Leftarrow\)) By contraposition: assume \(\Sigma \notin \mathbb{K}^{\mathsf{sLO}}_\mathit{surj}\). By Theorem 3(2), there exists \(t_w\) such that: \[\mathcal{F}_w(\{t_w\})\!\downarrow^\ast \cup \;\mathcal{F}_w(\{t_w\})\!\uparrow^\ast \nsubseteq \mathcal{F}_w(t_w\!\downarrow^\ast) \cup\, \mathcal{F}_w (t_w\!\uparrow^\ast) \] Define a model \((\Sigma, h)\), where \(h(p) = \mathcal{F}_w(t_w\!\downarrow^\ast) \cup \, \mathcal{F}_w(t_w\! \uparrow^\ast)\). By Lemma 2(1), we have \(t_w \!\downarrow^\ast\!\cup \, t_w\! \uparrow^\ast\, \subseteq h(\square p)\), which implies \(t_w \in h(H\square p \land G\square p)\). However, by \((\dagger)\), the condition \(\mathcal{F}_w(\{t_w\})\!\downarrow^\ast\!\cup \, \mathcal{F}_w(\{t_w\})\!\uparrow^\ast \subseteq h(p)\) fails. Thus \(t_w \notin h(\square(Hp \land Gp))\), and \((\mathit{Surj})\) is invalid in \(\Sigma\).

\(\mathsf{LO}\) case. The proof for \(\mathsf{LO}\) follows the same structure as for \(\mathsf{sLO}\). The only difference arises from the semantics of \(G\) and \(H\): in reflexive orders, \(t_w \in h(H\square p \land G\square p)\) already guarantees \(\mathcal{F}_w(\{t_w\}) \subseteq h(p)\). This allows us to augment the strict inclusions \(\mathcal{F}_w(\{t_w\})\!\downarrow^{\ast} \subseteq h(p)\) and \(\mathcal{F}_w(\{t_w\})\!\uparrow^{\ast} \subseteq h(p)\) with the point itself, yielding \(\mathcal{F}_w(\{t_w\}) \subseteq h(Hp) \cap h(Gp)\) in the reflexive sense. The remainder of the proof then proceeds identically to the \(\mathsf{sLO}\) case. \(\blacksquare\)

ii. Negative cases: Undefinability in preorders, strict preorders, and posets.

Totality and surjectivity are undefinable in \(\mathsf{sPRE}\) as witnessed by the following counterexamples in the Appendix:

Totality: Figure 1.

Surjectivity: Figure 2.

By Convention (RC), these configurations also establish undefinability in \(\mathsf{PRE}\) and \(\mathsf{PO}\). \(\blacksquare\)

We now proceed to examine other functional properties whose definability fails uniformly across all the order types under consideration.

Proof:
Undefinability in \(\mathsf{sPRE}\) and \(\mathsf{sLO}\) is established via the surjective frame homomorphisms illustrated in the following figures:

Non-totality, injectivity, and strict monotonicity: Figure 3.

Monotonicity and constancy: Figure 4.

Antitonicity and strict antitonicity: Figure 5.

By Convention (RC), the undefinability of these properties (including constancy and all forms of monotonicity/antitonicity) extends to \(\mathsf{PRE}, \mathsf{PO}\), and \(\mathsf{LO}\). \(\blacksquare\)

The preceding results yield the following complete classification of the expressive capacity of \(L_{T\times W}\):

Table 1 summarizes these results. A value of Yes indicates that the property is definable in the corresponding order type, while No indicates it is not.

0pt

3.1 Strict vs. Standard interpretation: Expressive divergence↩︎

Proof:
(i) The standard interpretation cannot be captured by the strict interpretation. Let \(\mathcal{M}\) be a model with a single point \(t\) such that \(tRt\), and let \(\mathcal{N}\) be a model with a single point \(t'\) such that \(\neg(t'Rt')\). In both models, every atom is false. The irreflexive core is empty (\(R^\bullet(t)=\varnothing\) and \({R'}^\bullet(t')=\varnothing\)). By structural induction, every formula evaluated under the strict interpretation (\(G^\ast,H^\ast\)) has the same truth value at \(t\) and \(t'\) (the only subformulas are \(\bot\), atoms, boolean connectives, and \(G^\ast,H^\ast\); all are interpreted identically). However, the formula \(Gp\) under the standard interpretation is false at \(t\) (because \(tRt\) and \(p\) is false) but true at \(t'\) (vacuously, as \(R'(t')=\varnothing\)).

(ii) The strict interpretation cannot be captured by the standard interpretation. Let \(\mathcal{M}\) be the same model as in (i) (a single reflexive point \(t\) with all atoms false). Let \(\mathcal{N}^\prime\) be a model consisting of two points \(t',u'\) such that \(t'R't'\), \(u'R'u'\), and \(t'R'u'\), with all atoms false at both points. A straightforward structural induction shows that \(t\) (in \(\mathcal{M}\)) and \(t'\) (in \(\mathcal{N}^\prime\)) satisfy exactly the same formulas under the standard interpretation. Indeed, the only difference is the extra point \(u'\) in \(\mathcal{N}^\prime\), but since all atoms are false there, its presence does not affect the truth of any formula. Consequently, \(t\) and \(t'\) are indistinguishable for \(L(G,H)\). On the other hand, they differ under the strict interpretation: \(G^\ast p\) is true at \(t\) (since \(R^\bullet(t)=\varnothing\)) but false at \(t'\) because \(u'\) is a strict successor of \(t'\) and \(p\) is false there. \(\blacksquare\)

3.2 Definability under the strict interpretation↩︎

We now examine whether adopting the strict interpretation (\(G^*, H^*\)) of our temporal operators alters the definability results in the multiflow setting.

Regarding positive results, the properties of totality and surjectivity remain definable in both \(\mathsf{LO}\) and \(\mathsf{sLO}\) frameworks, as shown in Theorem 4.

As for the negative results, the counterexamples in Figures 1–5 and 6 consist of strict orders where \(R_w = R^\bullet_w\). In these models, the standard interpretation and the strict interpretation are semantically equivalent. Although Convention (RC) allows these frames to represent reflexive closures, the strict interpretation ensures that \(G^*,H^*\) quantify exclusively over the underlying relation \(R^\ast_w\), ignoring any reflexive loops. This ensures that it evaluates the same structure as in the original strict counterexamples.

Consequently, the surjective p-morphisms established for the standard interpretation remain valid for the strict interpretation. All undefinability results therefore transfer directly across every order type, leaving Theorem 6 and Table 1 unchanged. The expressive limitations are inherent to the multiflow structure, not the choice of Priorean or strict semantics.

4 Structural Refinements: Minimal Functional Frames↩︎

The findings in Section 3 demonstrate that definability within the multiflow setting is severely constrained by its structural complexity. This section investigates whether these limitations can be overcome by imposing a simpler structure on the frames while keeping the language \(L_{T\times W}\) fixed.

To this end, we introduce minimal functional frames (the \(\mathsf{O}^2\) family)—structures restricted to at most two flows and a single accessibility function. This refinement effectively transforms our functional operators \(\square\) and \(\lozenge\) from second-order operators (which quantify over an arbitrary family of functions) into first-order ones, as they now refer to a single, fixed mapping.

Our analysis follows a two-step approach:

1. We examine definability in minimal frames using the standard pair \((G, H)\), establishing what gains can be achieved by structural simplification alone.

2. We evaluate the same minimalist environment using the strict pair \((G^\ast, H^\ast)\).

This allows us to determine whether the choice of temporal interpretation—which proved irrelevant in the general multiflow setting—becomes a decisive factor for expressivity once structural noise is eliminated.

4.1 Definability in Minimal Frames under the Standard Temporal Interpretation↩︎

We now examine minimal functional frames, a setting where definability is recovered for a significant range of properties. By reducing structural complexity to the \(\mathsf{O}^2\) family, these frames isolate functional behavior and allow for a focused analysis of the interaction between order types and the standard temporal operators \(G\) and \(H\). While the general multiflow setting restricted definability to just two properties—totality and surjectivity—and only within linear orders (strict or not), the minimal settingt enables the definability of several additional properties.

In what follows we assume the frame contains at least one function; the case \(\mathcal{F}=\varnothing\) does not affect the definability results. Thus \(\mathcal{F}_w = \{f_{ww'}\}\) for some \(w' \in W\), and the correspondences from Lemma 2 simplify to:

Proof:
The theorem follows from Lemmas 3 to 6 below. \(\blacksquare\)

Proof:
We first address definability, then undefinability.

Definability.

• Totality. As in Theorem 4, the formula \((\mathit{Tot})\) defines \(\mathbb{K}^{\mathsf{sLO}^2}_{\mathit{tot}}\) in \(\mathbb{K}^{\mathsf{sLO}^2}\); its simplified version \((\mathit{Tot})^\circ\) defines \(\mathbb{K}^{\mathsf{LO}^2}_{\mathit{tot}}\) in \(\mathbb{K}^{\mathsf{LO}^2}\). (Note that \((\mathit{Tot})\) also works in \(\mathsf{LO}^2\), where the conjunct \(p\) is redundant, but \((\mathit{Tot})^\circ\) does not hold in \(\mathsf{sLO}^2\).)

• Surjectivity. As in Theorem 4, the formula \((\mathit{Surj})\) defines \(\mathbb{K}^{\mathsf{sLO}^2}_{\mathit{surj}}\) in \(\mathbb{K}^{\mathsf{sLO}^2}\) and \(\mathbb{K}^{\mathsf{LO}^2}_{\mathit{surj}}\) in \(\mathbb{K}^{\mathsf{LO}^2}\).

The verification follows Theorem 4, adapted via Corollary 1 to the minimal setting. Below, we provide the details for the specific cases of non-totality, constancy, and injectivity, introducing their defining formulas in each section.

Non-totality. The following formula defines \(\mathbb{K}^{\mathsf{sLO}^2}_{\mathit{non-tot}}\) in \(\mathbb{K}^{\mathsf{sLO}^2}\): \[(\mathit{Non-Tot})^2:\;P\square\bot \lor \square\bot \lor F\square\bot.\] (\(\Rightarrow\)) Assume \(\Sigma \in \mathbb{K}^{\mathsf{sLO}^2}_{\mathit{non-tot}}\) and let \(f_{ww'}\) be its unique function. There exists \(t_w\) with \(f_{ww'}(\{t_w\}) = \varnothing\). Let \((\Sigma, h)\) be any model, then \(t_w \in h(\square\bot)\). In a strict linear order, every \(t'_w\) satisfies \(t'_w < t_w\), \(t'_w = t_w\), or \(t'_w > t_w\). Thus, \(t'_w \in h(P\square\bot)\), \(t'_w \in h(\square\bot)\), or \(t'_w \in h(F\square\bot)\), respectively. Hence \((\mathit{Non-Tot})^2\) is valid in \(\Sigma\).

(\(\Leftarrow\)) If \(\Sigma \notin \mathbb{K}^{\mathsf{sLO}^2}_{\mathit{non-tot}}\), then for every \(t_w\), \(f_{ww'}(\{t_w\}) \neq \varnothing\). Consequently, for any model \((\Sigma, h)\), we have \(t_w \in h(\neg\square\bot)\) for all \(t_w\). Since the frame is a strict linear order, \(t_w\!\downarrow^\ast \cup\, \{t_w\} \,\cup t_w\!\uparrow^\ast = T_w \subseteq h(\neg\square\bot)\). It follows that \(t_w \notin h(P\square\bot \lor \square\bot \lor F\square\bot)\), and therefore \((\mathit{Non-Tot})^2\) is invalid in \(\Sigma\).

Constancy. The following formula defines \(\mathbb{K}^{\mathsf{sLO}^2}_{\mathit{con}}\) in \(\mathbb{K}^{\mathsf{sLO}^2}\): \[(\mathit{Con})^2:\;\lozenge p \to (H\square p \land G\square p).\] Let \(\Sigma \in \mathbb{K}^{\mathsf{sLO}^2}\) and let \(f_{ww'}\) its unique function. By Theorem 1(6), \(f_{ww'}\) is constant iff for every \(t_w \in \mathrm{Dom}(f_{ww'})\), \[f_{ww'}(t_w\!\downarrow^\ast) \cup f_{ww'}(t_w\!\uparrow^\ast) \subseteq \{f_{ww'}(t_w)\}. \qquad (\mathit{con})\]

(\(\Rightarrow\)) Suppose \(\Sigma \in \mathbb{K}^{\mathsf{sLO}^2}_{\mathit{con}}\). Let \((\Sigma, h)\) be any model and suppose \(t_w \in h(\lozenge p)\). Since \(f_{ww'}\) is constant, by \((\mathit{con})\) we have \[f_{ww'}(t_w\!\downarrow^\ast) \cup f_{ww'}(t_w\!\uparrow^\ast) \subseteq \{f_{ww'}(t_w)\} \subseteq h(p). \] Applying Corollary 1(1) with \(X = t_w\!\downarrow^\ast \cup\, t_w\!\uparrow^\ast\) yields \[t_w\!\downarrow^\ast \cup\, t_w\!\uparrow^\ast \subseteq h(\square p). \] From (2), it follows that \(t_w\!\downarrow^\ast \subseteq h(\square p)\) and \(t_w\!\uparrow^\ast \subseteq h(\square p)\). Thus, Corollary 1(2) and (3) yield \(t_w \in h(H\square p)\) and \(t_w \in h(G\square p)\), respectively. Hence \[t_w \in h(H\square p \land G\square p),\] and therefore \((\mathit{Con})^2\) is valid in \(\Sigma\).

(\(\Leftarrow\)) Suppose \(\Sigma \notin \mathbb{K}^{\mathsf{sLO}^2}_{\mathit{con}}\). Because \(f_{ww'}\) is not constant, Theorem 1(6) gives a point \(t_w\) such that \((\mathit{con})\) fails. Consider a model \((\Sigma, h)\), where \(h(p) := \{f_{ww'}(t_w)\}\). Then \(t_w \in h(\lozenge p)\) (since \(f_{ww'}(t_w) \in h(p)\)). By the failure of \((\mathit{con})\), we have \[f_{ww'}(t_w\!\downarrow^\ast) \cup f_{ww'}(t_w\!\uparrow^\ast) \not\subseteq \{f_{ww'}(t_w)\}. \] Applying Corollary 1(1) yields \(t_w\!\downarrow^\ast \cup \, t_w\!\uparrow^\ast \not\subseteq h(\square p)\). Thus, by Corollary 1(2) and (3), \(t_w \notin h(H\square p)\) or \(t_w \notin h(G\square p)\), whence \(t_w \notin h(H\square p \land G\square p)\). Therefore \((\mathit{Con})^2\) is invalid in \(\Sigma\).

ii. Undefinability. For totality, non-totality, and surjectivity, the counterexamples from the general setting (Figures 1 and 2) remain valid in the minimal setting. They witness undefinability in \(\mathsf{sPRE}^2\); by Convention (RC), these counterexamples also establish undefinability in \(\mathsf{PRE}^2\) and \(\mathsf{PO}^2\).

Constancy requires a different approach because surjective p-morphisms preserve constancy, as the following claim shows.

Proof of the Claim Let \(f \colon P_1 \rightharpoonup P_2\), \(f' \colon P'_1 \rightharpoonup P'_2\) with \(\operatorname{Dom}(f) \neq \varnothing\), and let \(h_1 \colon P_1 \to P'_1\), \(h_2 \colon P_2 \to P'_2\) satisfy:

1. \(h_1|_{\operatorname{Dom}(f)}\) is onto \(\operatorname{Dom}(f')\);

2. \(f'(h_1(t)) = h_2(f(t))\) for every \(t \in \operatorname{Dom}(f)\).

Assume \(f\) constant but \(f'\) not. Then there exist \(a'_1, a'_2 \in \operatorname{Dom}(f')\) with \(f'(a'_1) \neq f'(a'_2)\). By (1) choose \(a_1, a_2 \in \operatorname{Dom}(f)\) with \(h_1(a_i) = a'_i\) (\(i=1,2\)). Condition (2) gives \(f'(a'_i) = h_2(f(a_i))\). Since \(f\) constant, \(f(a_1)=f(a_2)=:y\). Thus \(h_2(y)=f'(a'_1)=f'(a'_2)\), contradiction. Hence \(f'\) must be constant.

Since the p-morphism method fails to separate these frames, we establish their indistinguishability by a direct valuation mapping. For any formula falsifiable in a model over \(\Sigma'\), we construct a model over \(\Sigma\) that falsifies the same formula by copying the valuation pointwise, as described below.

Consider the following two minimal frames, where temporal relations are empty (reflexively closed for non-strict variants): \[\begin{align} \Sigma &: \; T_w = \{1_w, 2_w\},\; T_v = \{3_v\},\; \mathcal{F} = \{f_{wv}\},\; f_{wv}(1_w) = f_{wv}(2_w) = 3_v,\\[2pt] \Sigma' &: \; T'_{w'} = \{4_{w'}, 5_{w'}\},\; T'_{v'} = \{6_{v'}, 7_{v'}\},\; \mathcal{F}' = \{f'_{w'v'}\},\\ &\qquad f'_{w'v'}(4_{w'}) = 6_{v'},\; f'_{w'v'}(5_{w'}) = 7_{v'}. \end{align}\] We now show that if a formula \(A\) is falsifiable in a model over \(\Sigma'\), then it is also falsifiable in a model over \(\Sigma\). Let \(M_2 = (\Sigma', h')\) with \(M_2, x' \not\models A\). Build \(M_1 = (\Sigma, h)\) by case analysis:

We build \(M_1 = (\Sigma, h)\) by transferring the valuation pointwise. For every propositional variable \(p\) we define \(h(p)\) as follows, according to the position of the falsifying point \(x'\) in \(M_2\):

• If \(x' = 4_{w'}\): set \(1_w \in h(p)\) iff \(4_{w'} \in h'(p)\), and \(3_v \in h(p)\) iff \(6_{v'} \in h'(p)\).

• If \(x' = 5_{w'}\): set \(1_w \in h(p)\) iff \(5_{w'} \in h'(p)\), and \(3_v \in h(p)\) iff \(7_{v'} \in h'(p)\).

• If \(x' = 6_{v'}\) or \(x' = 7_{v'}\): set \(3_v \in h(p)\) iff \(x' \in h'(p)\).

Values at the remaining coordinates may be chosen arbitrarily. By structural induction on \(A\), \(M_1\) falsifies \(A\) at the corresponding coordinate. Consequently, no \(L_{T\times W}\)-formula can distinguish \(\Sigma\) from \(\Sigma'\). Since \(\Sigma\) has a constant function and \(\Sigma'\) has not, constancy is not definable in \(\mathsf{sPRE}^2\). The same construction with reflexive closures yields undefinability in \(\mathsf{PRE}^2\) and \(\mathsf{PO}^2\).\(\blacksquare\)

Proof:
The formula \[(\mathit{Inj})^2:\;\lozenge(Hp \land Gp) \to (H\square p \land G\square p)\] defines \(\mathbb{K}^{\mathsf{sLO}^2}_\mathit{inj}\) in \(\mathbb{K}^{\mathsf{sLO}^2}\).

Strict linear orders (\(\mathsf{sLO}^{2}\)). Let \(\Sigma \in \mathbb{K}^{\mathsf{sLO}^2}\) and let \(f_{ww'}\) be its unique function. By Theorem 1(2) \(f_{ww'}\) is injective iff for every \(t_w \in \mathrm{Dom}(f_{ww'})\), \[f_{ww'}(t_w\!\downarrow^{*})\cup f_{ww'}(t_w\!\uparrow^{*}) \subseteq f_{ww'}(t_w)\!\downarrow^{*}\cup\, f_{ww'}(t_w)\!\uparrow^{*}. \qquad (\mathit{inj})\]

(\(\Rightarrow\)) Assume \(\Sigma \in \mathbb{K}^{\mathsf{sLO}^2}_\mathit{inj}\). Let \((\Sigma, h)\) be any model and let \(t_w \in h(\lozenge(Hp \land Gp))\). Then \(f_{ww'}(t_w) \in h(Hp) \cap h(Gp)\), which implies \[f_{ww'}(t_w)\!\downarrow^{\ast} \cup\, f_{ww'}(t_w)\!\uparrow^{\ast} \subseteq h(p). \] By \((\mathit{inj})\) and (1), we obtain \(f_{ww'}(t_w\!\downarrow^{\ast}) \cup f_{ww'}(t_w\!\uparrow^{\ast}) \subseteq h(p)\). Applying Corollary 1(1) with \(X = t_w\!\downarrow^{\ast} \cup\, t_w\!\uparrow^{\ast}\) yields \[t_w\!\downarrow^{\ast} \cup\, t_w\!\uparrow^{\ast} \subseteq h(\square p). \] Hence \(t_w\!\downarrow^{\ast} \subseteq h(\square p)\) and \(t_w\!\uparrow^{\ast} \subseteq h(\square p)\). By Corollary 1(2) and (3), we obtain \(t_w \in h(H\square p)\) and \(t_w \in h(G\square p)\). Therefore \(t_w \in h(H\square p \land G\square p)\), hence \((\mathit{Inj})^2\) is valid in \(\Sigma\).

(\(\Leftarrow\)) Suppose \(\Sigma \notin \mathbb{K}^{\mathsf{sLO}^2}_\mathit{inj}\). Then \(f_{ww'}\) is not injective, so by Theorem 1(2) there exists \(t_w \in \mathrm{Dom}(f_{ww'})\) such that \((\mathit{inj})\) fails. Define a model \((\Sigma, h)\), where \(h(p) := f_{ww'}(t_w)\!\downarrow^{\ast} \cup\, f_{ww'}(t_w)\!\uparrow^{\ast}\). Then \(t_w \in h(\lozenge(Hp \land Gp))\) but \[f_{ww'}(t_w\!\downarrow^{\ast}) \cup f_{ww'}(t_w\!\uparrow^{\ast}) \not\subseteq h(p),\] so by Corollary 1(1), \(t_w\!\downarrow^{\ast} \cup\, t_w\!\uparrow^{\ast} \not\subseteq h(\square p)\). Hence \(t_w \notin h(H\square p)\) or \(t_w \notin h(G\square p)\), i.e. \(t_w \notin h(H\square p \land G\square p)\). Thus \((\mathit{Inj})^2\) is invalid in \(\Sigma\).

Undefinability elsewhere. Figure 6 exhibits a surjective p-morphism witnessing indefinability in \(\mathsf{sPRE}^2\); by Convention (RC) its reflexive closure yields indefinability in \(\mathsf{PRE}^2\) and \(\mathsf{PO}^2\). Figure 7 shows indefinability in \(\mathsf{LO}^2\). \(\blacksquare\)

Proof:
Monotonicity. We treat non-strict and strict orders separately, as they require different formulas.

Non-strict orders (\(\mathsf{PRE}^{2}\), \(\mathsf{PO}^{2}\), \(\mathsf{LO}^{2}\)). Let \(\Sigma \in \mathbb{K}^{\mathsf{O}^2}\) with \(\mathsf{O}\in \{\mathsf{PRE}, \mathsf{PO}, \mathsf{LO}\}\) and let \(f_{ww'}\) be its unique function. By Theorem 2(1), \(f_{ww'}\) is increasing iff for every \(t_w \in \mathrm{Dom}(f_{ww'})\), \[f_{ww'}(t_w\!\uparrow) \subseteq f_{ww'}(t_w)\!\uparrow. }\]

We show that \((\mathit{Inc})^{2}: \lozenge Gp \to G\square p\) defines monotonicity in these classes.

(\(\Rightarrow\)) Assume \(\Sigma \in \mathbb{K}^{\mathsf{O}^2}_{\mathit{inc}}\). Let \((\Sigma,h)\) be any model and suppose \(t_w \in h(\lozenge Gp)\). Then \(f_{ww'}(t_w) \in h(Gp)\), which in reflexive orders means \(f_{ww'}(t_w)\!\uparrow\,\subseteq h(p)\). From this and \((\mathit{inc})\) we obtain \(f_{ww'}(t_w\!\uparrow) \subseteq h(p)\). Applying Corollary 1(1) with \(X = t_w\!\uparrow\) yields \(t_w\!\uparrow \, \subseteq h(\square p)\), and Corollary 1(3) then gives \(t_w \in h(G\square p)\). Hence \((\mathit{Inc})^{2}\) is valid in \(\Sigma\).

(\(\Leftarrow\)) Assume \(\Sigma \notin \mathbb{K}^{\mathsf{O}^2}_{\mathit{inc}}\). Then \((\mathit{inc})\) fails at some \(t_w \in \mathrm{Dom}(f_{ww'})\). Define \(h(p) := f_{ww'}(t_w)\!\uparrow\). Clearly \(t_w \in h(\lozenge Gp)\). But \(f_{ww'}(t_w\!\uparrow) \not\subseteq h(p)\) by failure of \((\mathit{inc})\) and definition of \(h\), so by Corollary 1(1) we have \(t_w\!\uparrow \not\subseteq h(\square p)\), whence \(t_w \notin h(G\square p)\). Thus \((\mathit{Inc})^2\) is invalid in \(\Sigma\).

Strict orders (\(\mathsf{sPRE}^2\), \(\mathsf{sLO}^2\)). Let \(\Sigma \in \mathbb{K}^{\mathsf{O}^2}\) with \(\mathsf{O}\in \{\mathsf{sPRE}, \mathsf{sLO}\}\). For strict orders we replace \(\uparrow\) by \(\uparrow^{*}\) throughout. The characterisation becomes \[f_{ww'}(t_w\!\uparrow^{*}) \subseteq f_{ww'}(t_w)\!\uparrow^{*}\]and the defining formula is \[(\mathit{Inc})^{2}_s:\;\lozenge(p \land Gp) \to G\square p .\] The proof proceeds exactly as above, noting that \(f_{ww'}(t_w) \in h(Gp)\) now requires both \(f_{ww'}(t_w) \in h(p)\) and \(f_{ww'}(t_w)\!\uparrow^{*} \subseteq h(p)\).

Antitonicity. This follows by the same argument, replacing \(\uparrow\) with \(\downarrow\) in the consequent of \((\mathit{inc})\). The characterisation becomes \(f_{ww'}(t_w\!\uparrow) \subseteq f_{ww'}(t_w)\!\downarrow\) (Theorem 2(2)), yielding the formulas \((\mathit{Dec})^2: \lozenge Gp \to H\square p\) for non-strict orders and \((\mathit{Dec})^{2}_s: \lozenge(p \land Gp) \to H\square p\) for strict orders.

Since the argument covers every minimal order type, monotonicity and antitonicity are definable in all of them.

Proof:
Definability in \(\mathsf{sPRE}^2\) and \(\mathsf{sLO}^2\). The formulas \[(\mathit{Inc})^{2}:\;\lozenge Gp \to G\square p \qquad\text{and}\qquad (\mathit{Dec})^{2}:\;\lozenge Gp \to H\square p,\] which define ordinary monotonicity and antitonicity in non-strict orders, also define their strict counterparts in strict orders. In a strict order, \((\mathit{Inc})^{2}\) expresses precisely the condition \(f_{ww'}(t_w\!\uparrow^{*}) \subseteq f_{ww'}(t_w)\!\uparrow^{*},\) which is the characterisation of strict monotonicity (Theorem 1(4)). The verification is identical to the proof of Lemma 5 for the non-strict case, replacing \(\uparrow,\downarrow\) everywhere by \(\uparrow^{*},\downarrow^{*}\).

Undefinability elsewhere. Figure 7 contains a surjective homomorphism that shows strict monotonicity is not definable in \(\mathsf{PRE}^{2}\), \(\mathsf{PO}^{2}\) or \(\mathsf{LO}^{2}\); Figure 8 does the same for strict antitonicity. \(\blacksquare\)

0pt

4.2 Definability Improvements under the Strict Temporal Interpretation↩︎

The strict interpretation \(G^\ast, H^\ast\) significantly expands the definability landscape. By disregarding reflexive loops, it breaks certain surjective homomorphisms that preserved truth for the standard interpretation \(G, H\), turning them into non-bisimulations.

Proof:
Proof sketch. In strict orders, the standard and strict interpretations coincide semantically. In reflexive orders, the strict interpretation ignores reflexive loops and evaluates only the strict part \(\uparrow^\ast,\downarrow^\ast\). Hence, from the perspective of the strict interpretation, all orders are effectively assimilated to their strict counterparts: \(\mathsf{PRE}^2\) and \(\mathsf{PO}^2\) behave like \(\mathsf{sPRE}^2\), and \(\mathsf{LO}^2\) behaves like \(\mathsf{sLO}^2\).

Definability transfers directly from the standard to the strict setting:

• Totality, surjectivity, constancy, and non-totality: the proofs for \(\mathsf{sLO}^2\) under the standard interpretation (Lemma 3) apply unchanged to \(\mathsf{LO}^2\) and \(\mathsf{sLO}^2\) under the strict interpretation.

• Monotonicity and antitonicity: the proofs for \(\mathsf{sPRE}^2\) and \(\mathsf{sLO}^2\) under the standard interpretation (Lemma 5) extend to all minimal order types under the strict interpretation.

Undefinability in \(\mathsf{PRE}^2\), \(\mathsf{sPRE}^2\), and \(\mathsf{PO}^2\) follows from the same counterexamples used for the standard interpretation (Figures 1, 2, 6) together with Convention (RC). For constancy, the semantic equivalence argument from Theorem 8 applies unchanged to the strict interpretation in \(\mathsf{sPRE}^2\) and, via Convention (RC), to \(\mathsf{PRE}^2\) and \(\mathsf{PO}^2\). \(\blacksquare\)

Proof:

The algebraic characterizations for injectivity (Theorem 1(2)) and strict monotonicity (Theorem 1(5)) involve only the strict intervals \(\uparrow^*\) and \(\downarrow^*\). Under the strict interpretation, \(G^*\) and \(H^*\) quantify precisely over these strict intervals, even in reflexive orders. Therefore, the verification follows exactly the same pattern as in Lemma 4 for injectivity in \(\mathsf{sLO}^2\) and Lemma 6 for strict monotonicity in \(\mathsf{sPRE}^2\) and \(\mathsf{sLO}^2\), replacing \(G,H\) with \(G^*,H^*\) throughout. The explicit algebraic manipulations are omitted to avoid repetition; the reader may consult the aforementioned lemmas for the detailed step-by-step derivation.

Proof:
Lemma 7(1) shows totality, non-totality, surjectivity, and constancy are definable in \(\mathsf{LO}^2\) and \(\mathsf{sLO}^2\), while Lemma 8(1) adds injectivity to this linear-order class.

From Lemma 7(1) and Lemma 8(2), monotonicity, antitonicity, and their strict variants are definable in all minimal order types.

Finally, Lemma 7(2) establishes that these five properties remain undefinable in \(\mathsf{PRE}^2\), \(\mathsf{sPRE}^2\), and \(\mathsf{PO}^2\). \(\blacksquare\)

The definability results under the strict interpretation are summarized in Table 3.

0pt

4.3 Relation to Other Frameworks: Indexed Languages and Uniform Domains↩︎

Our results can be viewed in light of two existing frameworks: indexed modal languages [4] and uniform-domain frames [3].

4.3.1 Relation to indexed modal languages: a structural insight.↩︎

Indexed languages achieve their expressivity by employing indexed modal operators (\([i], \langle i \rangle\), where \(i\) is an index for a flow) to distinguish the range of functions that are otherwise indistinguishable in an arbitrary ordered multiflow setting. By attaching these indices to the connectives, the language allows specific accessibility functions to be uniquely identified, as each index \(i\) points to the destination flow of a single function \(f_{wi}\). This strategy was systematically analyzed for strict linear orders (\(\mathsf{sLO}\)) and the same group of functional properties as in this paper in [4].

The fact that our definability patterns for minimal frames (\(\mathsf{O}^{2}\)) coincide precisely with those established for indexed languages is not accidental. If a functional property \(P\) holds in an indexed frame, it must hold for each function \(f_{wi}\) individually. Consequently, any definability argument—including those in [4]—necessarily focuses on a single function and the two flows it connects, rendering the rest of the multiflow structure logically inert.

This insight provides a direct translation between our results and those for indexed languages:

• Definability: If a formula \(A\) of \(L_{T\times W}\) defines a property \(P\) in the minimal class \(\mathsf{O}^{2}\) (as established in Section 4), then \(P\) is also defined in the class of indexed frames of type \(\mathsf{O}\) by the indexed schema \[\{A(i) \mid i \in I\},\] where each \(A(i)\) is obtained by replacing \(\square\) with \([i]\) and \(\lozenge\) with \(\langle i\rangle\). The verification is identical to that of Theorem 8, simply replacing \(f_{ww'}\) with \(f_{wi}\).

• Undefinability: Every undefinability counterexample in Appendix (see Figs. 1, 2, 6, 7, and 8, complemented by the (RC) convention where applicable) involves only two flows and a single function. Interpreting the target flow as an index \(i\) yields an immediate counterexample for the indexed setting, via the same surjective homomorphism.

This bidirectional correspondence ensures that the results established in Tables 2 and 3 are exhaustive for the group of functional properties analyzed in this study.

Regarding the choice of sources, we take [4] as our primary reference because it is the first indexed work where functional properties appear in isolation, matching our current approach. Earlier treatments [8] invariably combined them with totality, preventing an independent analysis of each property. Furthermore, while subsequent work introduced double-indexing to achieve completeness for surjective functions (see [9]), such refinements are redundant for definability. Since modal evaluation begins at a specific “actual” flow, the destination index alone uniquely identifies the function, making additional domain indexing unnecessary for the purposes of this study.

Thus, our minimal-frame approach reveals that adding explicit indices to the operators (syntactic indexing) achieves the same definability patterns as structurally simplifying the frames (restricting to at most two flows), regardless of which temporal interpretation (standard or strict) is adopted for \(G,H\). This equivalence demonstrates that indices essentially serve to isolate individual functions within a multiflow setting; once this structural complexity is eliminated, the basic temporal-modal operators of \(L_{T\times W}\) already provide the same definability patterns for the functional properties considered.

In fact, the connection between minimal frames and indexed languages is not limited to the specific properties examined here. As shown in the Appendix (Theorem 12), it constitutes a general definability equivalence theorem: for any order type and any functional property that concerns a single function, definability in minimal frames is equivalent to definability in indexed frames. The full technical development—including the formal definition of minimal projection and the proof of the equivalence—is presented there.

4.3.2 Comparison with Uniform-Domain Constraints↩︎

Unlike minimal frames, U-Dom frames retain a genuine arbitrary ordered multiflow structure—the modal operators \(\square\) and \(\lozenge\) still quantify over all accessibility functions. The uniformity of domains restores the arrow-style characterisations in linear orders (strict or non-strict) that fail in arbitrary ordered multiflow frames (see Example 1), because the aggregate image \(\mathcal{F}_w(X)\) of a set \(X \subseteq T_w\) now behaves as if it came from a single function. This uniformity is captured formally by the following condition: for every \(w \in W\), \(\operatorname{Dom}(f_{ww'}) = \operatorname{Dom}(f_{ww''})\) for all \(f_{ww'}, f_{ww''} \in \mathcal{F}_w\); this common domain is denoted by \(\operatorname{Dom}_U(\mathcal{F}_w)\).

These characterisations lead directly to defining formulas in \(L_{T\times W}\). The formulas for totality, non-totality, and surjectivity from Section 3 remain valid under U-Dom and are omitted here. For the remaining properties, the U-Dom condition introduces the disjunct \(\square\bot\) to handle points outside the common domain \(\operatorname{Dom}_U(\mathcal{F}_w)\). We present the formulas separately for the two temporal interpretations. With the exception of totality and non-totality, which require specific treatment based on the order’s reflexivity, these adapted formulas extend the results of [3] to all order types.

Under the standard interpretation (\(G,H\)). \[\begin{align} (UD\text{-}Inj) &: \square(Hp \land Gp) \to (\square\bot \lor (H\square p \land G\square p)) \\[4pt] (UD\text{-}Inc) &: \square Gp \to (\square\bot \lor G\square p) \qquad\text{(non-strict orders)}\\[4pt] (UD\text{-}StrInc) &: \square(p \land Gp) \to (\square\bot \lor G\square p) \qquad\text{(strict orders)}\\[4pt] (UD\text{-}Dec) &: \square Gp \to (\square\bot \lor H\square p) \qquad\text{(non-strict orders)}\\[4pt] (UD\text{-}StrDec) &: \square(p \land Gp) \to (\square\bot \lor H\square p) \qquad\text{(strict orders)}\\[4pt] (UD\text{-}Con) &: \square p \to (\square\bot \lor (H\square p \land G\square p)) \end{align}\]

Under the strict interpretation (\(G^\ast,H^\ast\)). For the strict interpretation, the formulas from Lemma 7 carry over directly, with the addition of \(\square\bot\) as above. Totality, non-totality, and surjectivity are given by the formulas in Lemma 7(1a) with \(G,H\) replaced by \(G^\ast,H^\ast\); we omit them here. For the remaining properties, the strict interpretation already excludes the present, so the distinction between non-strict and strict orders disappears: \[\begin{align} (UD\text{-}Inj)_\ast &: \square(H^\ast p \land G^\ast p) \to (\square\bot \lor (H^\ast\square p \land G^\ast\square p)) \\[4pt] (UD\text{-}Inc)_\ast &: \square G^\ast p \to (\square\bot \lor G^\ast\square p) \\[4pt] (UD\text{-}StrInc)_\ast &: \square(p \land G^\ast p) \to (\square\bot \lor G^\ast\square p) \\[4pt] (UD\text{-}Dec)_\ast &: \square G^\ast p \to (\square\bot \lor H^\ast\square p) \\[4pt] (UD\text{-}StrDec)_\ast &: \square(p \land G^\ast p) \to (\square\bot \lor H^\ast\square p) \\[4pt] (UD\text{-}Con)_\ast &: \square p \to (\square\bot \lor (H^\ast\square p \land G^\ast\square p)) \end{align}\]

Proof:
[Proof sketch] The verification follows the same pattern established in Section 3 for totality and surjectivity: each arrow-style characterisation in Theorem 10 is translated into the corresponding modal formula via Lemma 2. The disjunct \(\square\bot\) handles points outside the common domain \(\operatorname{Dom}_U(\mathcal{F}_w)\), where no function is defined.

Undefinability follows from the same counter-examples used for minimal frames (see the Appendix). Since each involves at most two flows and one function, it trivially satisfies the U-Dom condition while witnessing the indefinability of the corresponding property.\(\blacksquare\)

This coincidence reveals that functional multiplicity only obscures definability when functions are allowed to diverge in their domains. Once a common structural ground is established—whether through the geometric simplicity of minimal frames or the domain regularity of the U-Dom condition—the basic operators of \(L_{T\times W}\) recover their full capacity to characterize functional mappings. Thus, while U-Dom frames retain a genuine multiflow architecture, their domain regularity yields exactly the same definability patterns for the functional properties under study as minimal frames.

5 Conclusions and Future Work↩︎

This work provides a systematic map of definability for basic functional properties in the modal-temporal language \(L_{T\times W}\) across different order types. The results show that definability is governed by two factors: the locality of the Priorean operators (under both their standard (\(G,H\)) and strict (\(G^*,H^*\)) interpretations) and the structural complexity of the underlying frames.

In the original multiflow setting, definability is severely limited: only totality and surjectivity are definable, and only within linear orders. To overcome these limitations, we introduced minimal frames, which restrict each frame to at most two flows and a single accessibility function. This simplification transforms the modal operators \(\square, \lozenge\) from second-order quantifiers over arbitrary families of functions into first-order ones, yielding substantial gains in definability. In this setting, monotonicity and antitonicity become definable in all order types, and for linear orders the picture is nearly complete: all nine properties become definable, with the sole exception of injectivity in \(\mathsf{LO}\) when evaluated under the standard interpretation.

Even in minimal frames, however, a core set of properties remains undefinable in non-linear orders. Totality, non-totality, injectivity, surjectivity, and constancy cannot be defined in \(\mathsf{PRE}, \mathsf{sPRE}\), or \(\mathsf{PO}\). This limitation stems from the inherent locality of temporal modalities, which cannot relate points in incomparable or isolated parts of the domain.

The strict interpretation (\(G^*,H^*\)) partially overcomes this barrier. In minimal frames, it allows us to define strict monotonicity and strict antitonicity across all order types, and to recover injectivity in \(\mathsf{LO}\). Nevertheless, totality, non-totality, surjectivity, and constancy remain undefinable in non-linear orders even under this strict reading.

A methodological point concerns constancy in the minimal setting. Unlike the other properties studied, constancy is preserved by surjective p-morphisms in minimal frames, making the usual counterexample technique inapplicable. We therefore used a semantic equivalence argument to show that, in non-linear orders, \(L_{T\times W}\) cannot distinguish constant from non-constant functions. This exceptional behaviour highlights that constancy occupies a special place among the properties considered.

Our comparison with indexed languages and Uniform Domain (U-Dom) frames confirms that minimal frames capture the same definability patterns while maintaining a simpler architecture. Once the structural noise of multiple divergent domains is eliminated, the basic operators of \(L_{T\times W}\) recover their full capacity to characterize functional mappings. These results point to two natural directions for future research. Both share a common trait: they address definability not by refining the order type, but by introducing mechanisms that operate independently of it.

The first is to strengthen the connectivity of temporal orders by means of cohesive frames, where every flow is finitely connected [10]. Capturing the finite bidirectional paths between any two points naturally leads to infinitary connectives. The key question is whether such an enrichment can extend definability of the “hard core” beyond the linear case, by shifting the focus from the order type to the structural property of cohesiveness.

The second direction is to add operators that quantify over all points in a flow independently of the temporal order, such as the universal modality \([U]\) [11] or the universal inequality operator \([\neq]\) [12]. These operators allow the logic to “jump” across time. Because they bypass the order entirely, they are not appropriate for treating orders as such, but they offer a radically different route to definability for arbitrary functional frames.

Appendix↩︎

5.1 Summary of Defining Formulas↩︎

Tables 4 and 5 below show that the strict interpretation (\(G^\ast,H^\ast\)) yields a more uniform pattern of definability across the minimal order types of the \(O^2\) family. Several properties that require different schemata under the standard interpretation (\(G,H\)) admit a single, uniform formula under the strict reading.

This uniformity reflects a shift in the definability profile. The strict interpretation loses sensitivity to reflexive loops but gains uniformity for properties tied to irreflexive accessibility.

5.2 Formal correspondence between minimal and indexed frames↩︎

We now establish a precise formal correspondence between the minimal frame family \(\mathsf{O}^2\) and the class of indexed frames of type \(\mathsf{O}\). An indexed frame is a structure \(\Sigma^{\mathfrak{I}} = (W,\mathcal{T},\mathcal{F})\) where \(W\) is a set of worlds, \(\mathcal{T}\) a family of orders \((T_w,R_w)\) as in Definition 1, and \(\mathcal{F}\) a family of accessibility functions \(f_{wi}\) indexed by \(i\in\mathfrak{I}\), each \(f_{wi}: T_w \rightharpoonup T_i\). The modal operators are then \([i]\) and \(\langle i\rangle\), interpreted as: \[h([i]A) = \{t_w \mid f_{wi}(\{t_w\})\subseteq h(A)\}, \qquad h(\langle i\rangle A) = \{t_w \mid f_{wi}(\{t_w\})\cap h(A)\neq\varnothing\}.\] (We refer to [4] for the full details.)

Proof:
\((\Rightarrow)\) Suppose \(P\) is \(L_{T\times W}\)-definable in minimal frames \(\mathsf{O}^2\) by a formula \(A \in L_{T\times W}\). Let \(\Sigma^{\mathfrak{I}}\) be an indexed frame of type \(\mathsf{O}\).

If every function \(f_{wi}\) in \(\Sigma^{\mathfrak{I}}\) satisfies \(P\), then each minimal projection \(\Sigma_{wi}\) validates \(A\) (since \(A\) defines \(P\) in \(\mathsf{O}^2\)). By Lemma 9, the set \(\{A(i) \mid i \in \mathfrak{I}\}\) is valid in \(\Sigma^{\mathfrak{I}}\).

If some function \(f_{wi}\) in \(\Sigma^{\mathfrak I}\) fails \(P\), then its corresponding projection \(\Sigma_{wi}\) falsifies \(A\), so by the lemma the set \(\{A(i)\}\) is not valid in \(\Sigma^{\mathfrak{I}}\).

Therefore \(\{A(i)\}\) defines the class of indexed frames whose functions all satisfy \(P\), which is exactly the \(L^I\)-definability of \(P\) in \(\mathsf{O}\).

\((\Leftarrow)\) Let \(\Gamma = \{A(i) \mid i \in \mathfrak{I}\}\) define \(P\) in indexed frames of type \(\mathsf{O}\), i.e., \(P\) is \(L^I\)-definable in \(\mathsf{O}\). Define \(A\) by replacing every occurrence of \([i]\) with \(\square\) and \(\langle i\rangle\) with \(\lozenge\) in any formula of \(\Gamma\). (The choice of index is irrelevant, as all \(A(i)\) are syntactically identical up to the index label.)

Take an arbitrary minimal frame \(\Sigma_{ww'}\) of type \(\mathsf{O}^2\). Choose an index \(i \in \mathfrak{I}\) and rename the flow \(w'\) as \(i\), obtaining an indexed frame \(\Sigma^{\mathfrak{I}}\) with a single relevant index and the same temporal structure. By construction, \(\Sigma_{ww'}\) satisfies \(P\) iff \(\Sigma^{\mathfrak{I}}\) satisfies \(P\). Since \(\Gamma\) defines \(P\) in indexed frames of type \(\mathsf{O}\), we have that \(\Gamma\) is valid in \(\Sigma^{\mathfrak{I}}\) iff \(\Sigma^{\mathfrak{I}}\) satisfies \(P\). Applying Lemma 9, we obtain that \(\Gamma\) is valid in \(\Sigma^{\mathfrak{I}}\) iff \(A\) is valid in \(\Sigma_{ww'}\). Therefore, \(A\) is valid in \(\Sigma_{ww'}\) iff \(\Sigma_{ww'}\) satisfies \(P\), i.e., \(A\) defines \(P\) in \(\mathsf{O}^2\). Hence \(P\) is \(L_{T\times W}\)-definable in \(\mathsf{O}^2\).

5.3 Figures of undefinability↩︎

The following eight figures provide a catalogue of counterexamples illustrating the indefinability of functional properties across different order types. Each figure shows a pair of frames connected by a surjective p-morphism, where the property in question holds in the source but fails in the target. The appendix thus complements the proofs in the text by offering a systematic gallery of undefinability patterns.

Conventions for establishing undefinability.

Convention (RC). All counterexample figures in the Appendix (except Figures 7 and 8) depict strict orders. To obtain counterexamples for the reflexive classes \(\mathsf{PRE}\), \(\mathsf{PO}\), and \(\mathsf{LO}\), we take the reflexive closure of the depicted strict order (i.e., we add a reflexive loop at every point). The resulting frame is a counterexample for the corresponding reflexive order type.

Graphical elements (rectangles, circles, arrows) are explained only at their first occurrence; the explanation is not repeated in later figures. If a figure introduces no new elements, its caption will state: “No new graphical elements are introduced in this figure.” Figures that depict strict orders can be reused for reflexive classes by applying the reflexive closure (Convention RC).

References↩︎

---

1. The strict interpretation was the only one employed in [2], [3].↩︎