Definability of Functional Properties in the Basic Modal-Temporal Language over Ordered Frames

Alfredo Burrieza

arxiv: 2607.01110 · v1 · pith:VQGKGNBPnew · submitted 2026-07-01 · 💻 cs.LO · math.LO

Definability of Functional Properties in the Basic Modal-Temporal Language over Ordered Frames

Alfredo Burrieza This is my paper

Pith reviewed 2026-07-02 03:55 UTC · model grok-4.3

classification 💻 cs.LO math.LO

keywords definabilitymodal-temporal logicfunctional propertiesordered framesminimal functional framesstrict readingmultiflow semanticsuniform domain

0 comments

The pith

Restricting to minimal functional frames makes many functional properties definable in the basic modal-temporal language, with the strict reading enabling definitions such as injectivity even in reflexive orders.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper studies the expressive power of the basic modal-temporal language obtained by adding the temporal operators G and H to the basic modal language with box, denoted L_{T×W} under its functional interpretation. It compares the standard reading of the temporal operators, which includes the current instant, against the strict reading that excludes it, across nine functional properties and five order types. In the original multiflow setting the language remains weak and the two readings coincide, but the restriction to minimal functional frames in the O² family increases expressive power and makes the choice of reading matter. The same definability patterns emerge when functional multiplicity is controlled via indexed languages or the Uniform Domain condition, indicating that uncontrolled multiplicity rather than operator weakness caused the original limitations, while lack of connectivity leaves some properties undefinable in non-linear orders.

Core claim

When the semantics are restricted to the O² family of minimal functional frames, many of the nine functional properties become definable and the strict reading can define properties such as injectivity even in reflexive orders; the identical patterns appear under indexed languages and the Uniform Domain condition on L_{T×W}, showing that the expressive limitations of the multiflow setting stem from uncontrolled functional multiplicity rather than from any weakness of the operators themselves, while lack of connectivity remains a fundamental obstacle in all non-linear orders.

What carries the argument

the O² family of minimal functional frames, which restricts functional multiplicity to make properties such as injectivity, surjectivity, and monotonicity definable under the L_{T×W} language.

If this is right

Many of the nine functional properties become definable once semantics are restricted to the O² family.
The strict reading of the temporal operators defines injectivity even on reflexive orders.
Indexed languages and the Uniform Domain condition produce the same definability patterns as the O² restriction.
A set of properties remains undefinable in all non-linear orders because of lack of connectivity.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Similar multiplicity controls could be tested in other combinations of modal and temporal operators to check whether expressivity increases in the same way.
The results separate multiplicity control from connectivity as two distinct requirements for definability over orders.
One could add connectivity axioms to non-linear orders and check whether the previously undefinable properties then become expressible.
The patterns suggest examining whether the same multiplicity controls affect definability results in related bimodal languages.

Load-bearing premise

The analysis assumes that the identical definability patterns across multiflow, minimal functional frames, indexed languages, and uniform domain conditions are caused specifically by the control of functional multiplicity rather than by other unexamined semantic or syntactic factors in the language.

What would settle it

Finding a mismatch in which functional properties are definable under the O² frames versus under the Uniform Domain condition would show that multiplicity control is not the determining factor.

Figures

Figures reproduced from arXiv: 2607.01110 by Alfredo Burrieza.

**Figure 3.** Figure 3 [PITH_FULL_IMAGE:figures/full_fig_p014_3.png] view at source ↗

**Figure 1.** Figure 1: Undefinability of totality in strict preorders. In Σ totality holds, [PITH_FULL_IMAGE:figures/full_fig_p035_1.png] view at source ↗

**Figure 2.** Figure 2: Undefinability of non-totality and surjectivity in strict preorders. In [PITH_FULL_IMAGE:figures/full_fig_p036_2.png] view at source ↗

**Figure 3.** Figure 3: Undefinability of non-totality, injectivity, and strict monotonicity in [PITH_FULL_IMAGE:figures/full_fig_p037_3.png] view at source ↗

**Figure 4.** Figure 4: Undefinability of monotonicity and constancy in strict preorders and [PITH_FULL_IMAGE:figures/full_fig_p038_4.png] view at source ↗

**Figure 5.** Figure 5: Undefinability of antitonicity and strict antitonicity in strict preorders [PITH_FULL_IMAGE:figures/full_fig_p039_5.png] view at source ↗

**Figure 6.** Figure 6: Undefinability of injectivity in strict preorders. In Σ, the function [PITH_FULL_IMAGE:figures/full_fig_p040_6.png] view at source ↗

**Figure 7.** Figure 7: Undefinability of injectivity and strict monotonicity in preorders, [PITH_FULL_IMAGE:figures/full_fig_p041_7.png] view at source ↗

**Figure 8.** Figure 8: Undefinability of strict antitonicity in preorders, posets, and linear [PITH_FULL_IMAGE:figures/full_fig_p042_8.png] view at source ↗

read the original abstract

We study the expressive power of the simplest modal-temporal language, obtained by adding Prior's temporal operators \(G\) and \(H\) to the basic modal language with \(\Box\). This language is the standard bimodal combination of modal and tense logic; under its functional interpretation it is denoted \(L_{T\times W}\). To analyse its definability across five order types, we consider two semantic readings of the temporal operators: the standard reading (\(G,H\)), which includes the current instant, and the strict reading (\(G^{\ast},H^{\ast}\)), which always excludes it. We examine nine functional properties -- totality, non-totality, injectivity, surjectivity, monotonicity, strict monotonicity, antitonicity, strict antitonicity, and constancy -- over preorders, strict preorders, partial orders, linear orders, and strict linear orders. Our analysis reveals two different levels of expressive power. In the original multiflow setting, the language is quite weak and the two readings coincide. When we restrict the semantics to minimal functional frames (the \(O^{2}\) family), many properties become definable, and the choice of reading becomes crucial: the strict reading can define properties such as injectivity even in reflexive orders. The same definability patterns appear with indexed languages and with the Uniform Domain condition on the semantics of \(L_{T\times W}\). That three such different ways of controlling functional multiplicity lead to identical definability patterns indicates that the expressive limitations of the original framework come from the uncontrolled multiplicity of functions, not from any weakness of the operators. Even after controlling functional multiplicity, a set of properties remains undefinable in all non-linear orders, showing that the lack of connectivity is a fundamental obstacle.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper maps definability gains from controlling functional multiplicity in modal-temporal logic but the argument that this isolates multiplicity as the cause has some gaps.

read the letter

The one or two things to know: this paper systematically compares the definability of nine functional properties in the basic modal-temporal language over five order types, under standard and strict readings of the temporal operators. It finds that moving to minimal functional frames, indexed languages, or uniform domain conditions all produce the same boost in definability, leading the authors to attribute the original limitations to uncontrolled functional multiplicity rather than operator weakness. Connectivity still blocks some properties in non-linear orders.

The paper does a solid job of laying out these comparisons and highlighting where the strict reading gains an edge, such as defining injectivity in reflexive orders. The observation that three quite different controls yield identical patterns is the main new contribution and gives a clear picture of what changes when multiplicity is tamed.

The soft spot is in the causal inference. The three controls modify different aspects of the semantics or syntax, not just multiplicity, so the matching results do not fully isolate multiplicity as the sole source of the weakness. The abstract presents the results at a high level without derivations or counter-models, which makes it hard to verify the strength of the claims without the full proofs. That said, the patterns themselves seem consistent with the described setup.

This kind of work is for researchers in modal logic and tense logic focused on definability and frame properties. A reader already familiar with the L_{T×W} language and ordered frames would get the most out of the comparisons. It deserves a serious referee because the systematic analysis is new and the questions it raises about multiplicity versus other factors are worth pursuing in review.

Referee Report

2 major / 2 minor

Summary. The manuscript examines the expressive power of the basic modal-temporal language obtained by adding Prior's G and H to the basic modal language (denoted L_{T×W} under functional interpretation). It studies definability of nine functional properties (totality, non-totality, injectivity, surjectivity, monotonicity, strict monotonicity, antitonicity, strict antitonicity, constancy) over five order types (preorders, strict preorders, partial orders, linear orders, strict linear orders), comparing the standard reading (G, H, including the current instant) and strict reading (G*, H*, excluding it). The central claim is that the language is weak in the multiflow setting with coinciding readings, but many properties become definable when restricting to minimal functional frames (the O² family), where the choice of reading matters (e.g., strict reading defines injectivity even in reflexive orders); identical patterns hold under indexed languages and the Uniform Domain condition. This coincidence is taken to show that expressive limitations stem from uncontrolled functional multiplicity rather than operator weakness, while lack of connectivity remains an obstacle in non-linear orders.

Significance. If the definability results and the isolation of multiplicity as the key factor hold, the work would clarify how semantic restrictions interact with modal-temporal operators to determine expressive power, distinguishing operator limitations from frame multiplicity issues. The observation that connectivity is a persistent barrier even after multiplicity control, and that strict readings unlock additional definability in reflexive settings, offers concrete guidance for applications in temporal reasoning and verification. The cross-comparison across three distinct controls is a methodological strength when the variable isolation is made explicit.

major comments (2)

[Abstract] Abstract (final paragraph): the inference that identical definability patterns across multiflow, O² minimal frames, indexed languages, and Uniform Domain 'indicates that the expressive limitations ... come from the uncontrolled multiplicity of functions, not from any weakness of the operators' is load-bearing for the central claim but requires explicit isolation that these controls differ only (or primarily) in multiplicity and share no confounding interactions with the five order types or the standard/strict readings of G/H. The manuscript should supply a side-by-side comparison or counter-model analysis showing that other semantic factors are held constant.
[Abstract] The abstract states that 'our analysis reveals two different levels of expressive power' and that 'the same definability patterns appear' under the three controls, yet provides no derivation sketches, counter-model constructions, or error analysis for the nine properties. Without these, it is impossible to verify whether the reported patterns for, e.g., injectivity under strict reading in reflexive orders are robust or sensitive to unexamined interactions with order types.

minor comments (2)

[Abstract] The notation O² family and L_{T×W} are introduced without a brief definitional reminder in the abstract; a one-sentence gloss would aid readers unfamiliar with the multiflow semantics.
[Abstract] The nine properties and five order types are listed but not cross-referenced to any table or numbered list; adding such a reference would improve traceability when the patterns are discussed.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive report. We respond to each major comment below, agreeing where revisions will strengthen the isolation of the multiplicity factor and improve cross-references to the supporting analyses.

read point-by-point responses

Referee: [Abstract] Abstract (final paragraph): the inference that identical definability patterns across multiflow, O² minimal frames, indexed languages, and Uniform Domain 'indicates that the expressive limitations ... come from the uncontrolled multiplicity of functions, not from any weakness of the operators' is load-bearing for the central claim but requires explicit isolation that these controls differ only (or primarily) in multiplicity and share no confounding interactions with the five order types or the standard/strict readings of G/H. The manuscript should supply a side-by-side comparison or counter-model analysis showing that other semantic factors are held constant.

Authors: We agree that an explicit demonstration of isolation would strengthen the central claim. Each control (O² minimal frames, indexed languages, Uniform Domain) is constructed to vary only functional multiplicity while holding the five order types and both readings of G/H fixed. In revision we will insert a side-by-side comparison table (new subsection or appendix) that tabulates the semantic parameters across the three controls, confirming constancy of order types and readings, together with two short counter-model examples illustrating that a property becomes definable precisely when multiplicity is controlled. revision: yes
Referee: [Abstract] The abstract states that 'our analysis reveals two different levels of expressive power' and that 'the same definability patterns appear' under the three controls, yet provides no derivation sketches, counter-model constructions, or error analysis for the nine properties. Without these, it is impossible to verify whether the reported patterns for, e.g., injectivity under strict reading in reflexive orders are robust or sensitive to unexamined interactions with order types.

Authors: The abstract summarises results whose full derivations, formulas, counter-models, and error analyses appear in Sections 3–5 of the manuscript. The definability of injectivity under the strict reading on reflexive orders, for instance, is witnessed by an explicit formula verified directly in the O² semantics. To make this linkage immediate from the abstract we will add a single sentence directing readers to the relevant sections for the nine properties; this is a minor textual change that preserves abstract length while improving verifiability. revision: partial

Circularity Check

0 steps flagged

No circularity; definability claims rest on direct semantic frame restrictions

full rationale

The paper derives definability results by applying the language's semantics (standard vs. strict readings of G/H) to explicitly defined frame classes (multiflow, O² minimal functional frames, indexed languages, Uniform Domain) over five order types and nine properties. No equations reduce a 'prediction' to a fitted input by construction, no self-citations are invoked as load-bearing uniqueness theorems, and no ansatz or renaming of known results occurs. The inference that identical patterns across three controls implicate multiplicity (rather than other factors) is an interpretive claim about causation, not a self-definitional or fitted reduction; the derivation chain remains self-contained against the stated semantic definitions.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper rests on standard Kripke semantics for modal and tense operators over ordered frames; no free parameters, invented entities, or ad-hoc axioms are introduced beyond the usual background of modal logic.

axioms (1)

standard math Standard Kripke semantics for the basic modal operator Box and Prior's temporal operators G and H (or their strict variants) over ordered frames.
Invoked throughout the abstract when defining the language L_T×W and its two readings.

pith-pipeline@v0.9.1-grok · 5850 in / 1327 out tokens · 35640 ms · 2026-07-02T03:55:44.012851+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

17 extracted references

[1]

A Temporal×Modal Approach to the Definability of Properties of Functions,

A. Burrieza and I. P. de Guzm´ an, “A Temporal×Modal Approach to the Definability of Properties of Functions,” in A. Armando (Ed.),Frontiers of Combining Systems, FroCoS 2002, Lecture Notes in Artificial Intelligence, vol. 2309, Springer-Verlag, Berlin Heidelberg, 2002, pp. 239–254

2002
[2]

Indexed Flows in Tem- poral×Modal Logic with Functional Semantics,

A. Burrieza, I. P. de Guzm´ an, and E. Mu˜ noz, “Indexed Flows in Tem- poral×Modal Logic with Functional Semantics,”Proceedings of the Ninth International Symposium on Temporal Representation and Reason- ing (TIME 2002), IEEE Computer Society, pp. 141–148, 2002

2002
[3]

A functional approach for temporal× modal logics,

A. Burrieza and I. P. de Guzm´ an, “A functional approach for temporal× modal logics,”Acta Informatica, vol. 39, pp. 71–96, 2003

2003
[4]

Functional systems in the context of temporal×modal logics with indexed flows,

A. Burrieza, I. P. de Guzm´ an, and E. Mu˜ noz-Velasco, “Functional systems in the context of temporal×modal logics with indexed flows,”Interna- tional Journal of Computer Mathematics, vol. 86, nos. 10–11, pp. 1696– 1706, Oct.–Nov. 2009

2009
[5]

Burrieza, A., I

A. Burrieza, A., I. Fortes, and I. P´ erez de Guzm´ an,Completeness of a functional system for surjective functions. Mathematical Logic Quarterly, 63(6), 574–597, 2017

2017
[6]

Burrieza, M

A. Burrieza, M. Fortes, and I. P. de Guzm´ an. A temporal logic for mul- tiflows with a double-indexing language.Mathematical Logic Quarterly, 64(1-2):112–135, 2018

2018
[7]

Axiomatic classes in propositional modal logic,

R. Goldblatt and S. K. Thomason, “Axiomatic classes in propositional modal logic,” inAlgebra and Logic, J. N. Crossley (ed.), Springer Lecture Notes in Mathematics, Vol. 450, pp. 163–173, Springer, 1974

1974
[8]

Using the universal modality: gains and ques- tions,

V. Goranko and S. Passy, “Using the universal modality: gains and ques- tions,”Journal of Logic and Computation, vol. 2, no. 1, pp. 5–30, 1992

1992
[9]

G. E. Hughes and M. J. Cresswell.A Companion to Modal Logic. Methuen, London, 1984

1984
[10]

Boolean algebras with operators. Part I,

B. J´ onsson and A. Tarski, “Boolean algebras with operators. Part I,”Amer- ican Journal of Mathematics, vol. 73, pp. 891–939, 1951. 31

1951
[11]

Manna and A

Z. Manna and A. Pnueli.The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1992

1992
[12]

de Rijke

M. de Rijke. The modal logic of inequality.Journal of Symbolic Logic, 57(2):566–584, 1992

1992
[13]

Tarski and S

A. Tarski and S. Givant.A Formalization of Set Theory Without Variables (Vol. 41, Colloquium Publications). American Mathematical Society
[14]

R. H. Thomason. Combinations of tense and modality. In D. Gabbay and F. Guenthner, editors,Handbook of Philosophical Logic, Vol. II: Extensions of Classical Logic, pages 135–165. Reidel, Dordrecht, 1984

1984
[15]

Correspondence theory,

J. van Benthem, “Correspondence theory,” in D. Gabbay and F. Guenth- ner (eds.),Handbook of Philosophical Logic, Vol. II, pp. 167–247, Reidel, Dordrecht,1984. 32 Appendix 1 Summary of Defining Formulas Tables 4 and 5 below show that the strict interpretation (G ∗, H∗) yields a more uniform pattern of definability across the minimal order types of theO 2 f...

1984
[16]

The label “allO 2” indicates definability across all minimal order types in theO 2 family
[17]

No new graphical elements are introduced in this figure

For properties of order preservation, mirror-image formulations usingH andH ∗ are also possible and equivalent over minimal frames to the future- oriented ones listed. 33 2 Formal correspondence between minimal and indexed frames We now establish a precise formal correspondence between the minimal frame familyO 2 and the class of indexed frames of typeO. ...

[1] [1]

A Temporal×Modal Approach to the Definability of Properties of Functions,

A. Burrieza and I. P. de Guzm´ an, “A Temporal×Modal Approach to the Definability of Properties of Functions,” in A. Armando (Ed.),Frontiers of Combining Systems, FroCoS 2002, Lecture Notes in Artificial Intelligence, vol. 2309, Springer-Verlag, Berlin Heidelberg, 2002, pp. 239–254

2002

[2] [2]

Indexed Flows in Tem- poral×Modal Logic with Functional Semantics,

A. Burrieza, I. P. de Guzm´ an, and E. Mu˜ noz, “Indexed Flows in Tem- poral×Modal Logic with Functional Semantics,”Proceedings of the Ninth International Symposium on Temporal Representation and Reason- ing (TIME 2002), IEEE Computer Society, pp. 141–148, 2002

2002

[3] [3]

A functional approach for temporal× modal logics,

A. Burrieza and I. P. de Guzm´ an, “A functional approach for temporal× modal logics,”Acta Informatica, vol. 39, pp. 71–96, 2003

2003

[4] [4]

Functional systems in the context of temporal×modal logics with indexed flows,

A. Burrieza, I. P. de Guzm´ an, and E. Mu˜ noz-Velasco, “Functional systems in the context of temporal×modal logics with indexed flows,”Interna- tional Journal of Computer Mathematics, vol. 86, nos. 10–11, pp. 1696– 1706, Oct.–Nov. 2009

2009

[5] [5]

Burrieza, A., I

A. Burrieza, A., I. Fortes, and I. P´ erez de Guzm´ an,Completeness of a functional system for surjective functions. Mathematical Logic Quarterly, 63(6), 574–597, 2017

2017

[6] [6]

Burrieza, M

A. Burrieza, M. Fortes, and I. P. de Guzm´ an. A temporal logic for mul- tiflows with a double-indexing language.Mathematical Logic Quarterly, 64(1-2):112–135, 2018

2018

[7] [7]

Axiomatic classes in propositional modal logic,

R. Goldblatt and S. K. Thomason, “Axiomatic classes in propositional modal logic,” inAlgebra and Logic, J. N. Crossley (ed.), Springer Lecture Notes in Mathematics, Vol. 450, pp. 163–173, Springer, 1974

1974

[8] [8]

Using the universal modality: gains and ques- tions,

V. Goranko and S. Passy, “Using the universal modality: gains and ques- tions,”Journal of Logic and Computation, vol. 2, no. 1, pp. 5–30, 1992

1992

[9] [9]

G. E. Hughes and M. J. Cresswell.A Companion to Modal Logic. Methuen, London, 1984

1984

[10] [10]

Boolean algebras with operators. Part I,

B. J´ onsson and A. Tarski, “Boolean algebras with operators. Part I,”Amer- ican Journal of Mathematics, vol. 73, pp. 891–939, 1951. 31

1951

[11] [11]

Manna and A

Z. Manna and A. Pnueli.The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1992

1992

[12] [12]

de Rijke

M. de Rijke. The modal logic of inequality.Journal of Symbolic Logic, 57(2):566–584, 1992

1992

[13] [13]

Tarski and S

A. Tarski and S. Givant.A Formalization of Set Theory Without Variables (Vol. 41, Colloquium Publications). American Mathematical Society

[14] [14]

R. H. Thomason. Combinations of tense and modality. In D. Gabbay and F. Guenthner, editors,Handbook of Philosophical Logic, Vol. II: Extensions of Classical Logic, pages 135–165. Reidel, Dordrecht, 1984

1984

[15] [15]

Correspondence theory,

J. van Benthem, “Correspondence theory,” in D. Gabbay and F. Guenth- ner (eds.),Handbook of Philosophical Logic, Vol. II, pp. 167–247, Reidel, Dordrecht,1984. 32 Appendix 1 Summary of Defining Formulas Tables 4 and 5 below show that the strict interpretation (G ∗, H∗) yields a more uniform pattern of definability across the minimal order types of theO 2 f...

1984

[16] [16]

The label “allO 2” indicates definability across all minimal order types in theO 2 family

[17] [17]

No new graphical elements are introduced in this figure

For properties of order preservation, mirror-image formulations usingH andH ∗ are also possible and equivalent over minimal frames to the future- oriented ones listed. 33 2 Formal correspondence between minimal and indexed frames We now establish a precise formal correspondence between the minimal frame familyO 2 and the class of indexed frames of typeO. ...