A two-dimensional metric temporal logic

TL;DR

This paper introduces a novel two-dimensional metric temporal logic with dense linear orderings for internal and external time flows, providing semantics, a sequent calculus, and proving completeness and cut-elimination.

Contribution

It presents the first formalization of a two-dimensional metric temporal logic with dense orderings, including semantics, proof calculus, and key metatheoretical results.

Findings

Established semantics for the logic

Developed a sequent calculus with axioms

Proved completeness and cut-elimination

Abstract

We introduce a two-dimensional metric (interval) temporal logic whose internal and external time flows are dense linear orderings. We provide a suitable semantics and a sequent calculus with axioms for equality and extralogical axioms. Then we prove completeness and a semantic partial cut-elimination theorem down to formulas of a certain type.

Equations

$${\square }_{[m,n]}{\square }_{]m,n]}{\square }_{[m,n[}{\square }_{]m,n[}{\square }_{[m,\infty [}{\square }_{]m,\infty [}.$$

$$⊢X=X;X=Y,\rho [X/Z]⊢\rho [Y/Z](\rho \text{mbox}anatomicformulain{F}_{e,r})$$

$$⊢T:x=x;T:x=y,T:\rho [x/z]⊢T:\rho [y/z]$$

$$T=S,\ T:\eta\vdash S:\eta\qquad\mbox{($\eta$ an atomic formula in $\overline{F}_{i,l}\cup F_{i,r}$})$$

$$X<X⊢;X<Y,Y<Z⊢X<Z;⊢X<Y,X=Y,Y<X$$

$$⊢C<X,C=X;X<Y⊢\exists Z(X<Z\wedge Z<Y)$$

$$⊢X<F(X);X<Y⊢F(X)<F(Y);⊢\underset{n\in \omega }{\bigvee }(X<F^n(C))$$

$$A⊢A\text{id}tensy\text{vbox}spread0.0ptplus0.0001fil\text{penalty}1\Gamma ⊢A,\Delta \Gamma ,A⊢\Delta plus0.0001fil\text{vrule}height=0.25002pt,depth=0.25002pt,width=90.27756pt\text{cut}\Gamma ⊢\Delta$$

$$⊢T:(\alpha \wedge {\square }_{[0,\infty [}(\alpha \to {\square }_{[0,1]}\alpha ))\to {\square }_{[0,\infty [}\alpha (1)$$

$$⊢T:t:(\eta \wedge {\square }_{[0,\infty [}(\eta \to {\square }_{[0,1]}\eta ))\to {\square }_{[0,\infty [}\eta (2)$$

$$\mathcal{M}=(\mathbf{M},(p^{\mathbf{M}}{)}_{p\in \mathbf{P}})$$

$$\mbox{for all $\mathcal{M}$ as in (\ref{one}),}\hskip 19.91692pt\mathcal{M},0\models\alpha.$$

$${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 1.82132pt\hbox{$\displaystyle\penalty 1\Gamma^{\prime}\vdash\Delta^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox to30.19482pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{\kern 3.00003pt$$

}}}\hbox{\kern 0.0pt\hbox{${\Gamma }^n⊢{\Delta }^n$}}}}.$$

$${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1B_{1},\ldots,B_{k}\vdash D_{1},\ldots,D_{m}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox to85.22926pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{\kern 3.00003pt$$

}}}\hbox{\kern 5.51852pt\hbox{${\Gamma }^n⊢D_1,\dots ,D_m,{\Delta }^n$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\Gamma^{n},D_{1}\vdash\Delta^{n}

$$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=165.44427pt\hbox{\kern 3.00003pt$$

cut

$$}}}\hbox{\kern 45.62604pt\hbox{$$

\displaystyle\Gamma^{n}\vdash D_{2},\ldots,D_{m},\Delta^{n}

$$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\Gamma^{n},D_{2}\vdash\Delta^{n}$$

}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=259.32254pt\hbox{\kern 3.00003pt$cut$}}}\hbox{\kern 114.2359pt\hbox{$⋮cuts$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\Gamma^{n},D_{m}\vdash\Delta^{n}

$$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=355.31767pt\hbox{\kern 3.00003pt$$

cut

$$}}}\hbox{\kern 162.56142pt\hbox{$$

\displaystyle\Gamma^{n}\vdash\Delta^{n}

$$}}}}$$

$

$${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma^{n},T:t:\xi\vdash\Delta^{n}\qquad\Gamma^{n}\vdash T:t:\eta,\Delta^{n}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox to156.41689pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{\kern 3.00003pt$$

}}}\hbox{\kern 63.11102pt\hbox{${\Gamma }^n⊢{\Delta }^n$}}}}$$

$${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma^{n}\vdash T:f^{i}(t)\leq s,\Delta^{n}\quad\Gamma^{n}\vdash T:s\leq f^{j}(t),\Delta^{n}\quad\Gamma^{n},T:s:\eta\vdash\Delta^{n}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox to266.69878pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{\kern 3.00003pt$$

}}}\hbox{\kern 118.25197pt\hbox{${\Gamma }^n⊢{\Delta }^n$}}}}$$

$$A_2,\dots ,A_q,T:f^i(t)\le s,A_1{A}_2,\dots ,A_q,T:s\le f^j(t),A_1$$

$${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\{\Gamma^{n},T:t\mathchar 12604\relax f^{i}(c)\vdash\Delta^{n}\}_{i\in\omega}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox to109.08241pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{\kern 3.00003pt$$

}}}\hbox{\kern 39.44379pt\hbox{${\Gamma }^n⊢{\Delta }^n$}}}}$$

$${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma^{n},T:t:\eta\vdash T:t:\xi,\Delta^{n}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox to106.22203pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{\kern 3.00003pt$$

}}}\hbox{\kern 38.0136pt\hbox{${\Gamma }^n⊢{\Delta }^n$}}}}$$

$${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma^{n},T:f^{i}(t)\leq x,T:x\leq f^{j}(t)\vdash T:x:\eta,\Delta^{n}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox to189.39241pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{\kern 3.00003pt$$

}}}\hbox{\kern 79.59879pt\hbox{${\Gamma }^n⊢{\Delta }^n$}}}}$$

$${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma^{n}\vdash T:t\mathchar 12604\relax f^{m}(c),\Delta^{n}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox to90.14392pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{\kern 3.00003pt$$

}}}\hbox{\kern 29.97455pt\hbox{${\Gamma }^n⊢{\Delta }^n$}}}}$$

$$S\sim T\iff (S=T)\in \overline{\Gamma }.$$

$$M=\{T^{\sim }:T\in T_e\};F^{\mathbf{M}}(T^{\sim })=F(T{)}^{\sim };C^{\mathbf{M}}=C^{\sim };S^{\sim }{<}^{\mathbf{M}}{T}^{\sim }\iff (S<T)\in \overline{\Gamma }.$$

$$t_1{\sim }_S{t}_2\iff (S:t_1=t_2)\in \overline{\Gamma }.$$

$$N_S=\{t^S:t\in T_i\};f^{{\mathbf{N}}_S}(t^S)=f(t{)}^S;c^{{\mathbf{N}}_S}=c^S;$$

$$t_1^S{<}^{{\mathbf{N}}_S}{t}_2^S\iff (S:t_1<t_2)\in \overline{\Gamma }.$$

$$\mathcal{M}=(\mathbf{M},{\mathbf{N}}_{S^{\sim }},(p^{{\mathbf{N}}_{S^{\sim }}}{)}_{p\in \mathbf{P}},\sigma ,{\sigma }_{S^{\sim }}{)}_{S\in T_e}.$$

$$\mathcal{M}/\models T:x:\eta ;\mathcal{M}\models T:f^i(t)\le x;\mathcal{M}\models T:x\le f^j(t).$$

Full text

1 Introduction

In recent years, metric temporal logics gained popularity because of their applicative aspects, for instance those relative to the formalization of time-critical systems. At the same time, under the paradigm of time granularity, there appeared in the literature a number of proposals on how to combine temporal logics into $n$-dimensional systems (very often with $n=2$). See, for instance, [4, 5, 11]. To the best of our knowledge, proof-theoretic properties of those multi-dimensional systems have not been investigated yet.

In computer science, multi-dimensional temporal structures and the corresponding logics are often used. For instance, there are temporal structures modelling computations, with internal and external temporal quantifications ranging on states and computations respectively. There are also the structures for time granularity, which come equipped with an internal time flow (for each of the so called time grains) and an external one (for the whole structure of time grains). In this paper we took inspiration from the latter structures to develop a corresponding two-dimensional metric temporal logic, where both time flows are dense linear orderings. First of all we establish completeness of the proposed system with respect to a suitable class of structures. Secondly we get a semantic proof of cut-elimination as a byproduct of the technique used to establish completeness. More specifically, regarding cut-elimination, we aim at a semantic partial cut-elimination result in the vein of [7, Theorem 2.7.1]. We get our result by using semantic techniques, as done in [7, 3.1.9]. We show that every provable sequent has a proof whose cut formulas are among those occurring in some extralogical axiom.

We recall that, in presence of extralogical axioms, a full cut-elimination result that preserves the subformula property does not hold in general. See [7, Remark 2.7.7 ] for an example.

For simplicity, in the following we will simply refer to our result as to cut-elimination.

In [2] we introduced an infinitary extension of a fragment of the Metric Interval Temporal Logic over dense time domains, called ${\rm MTL}_{\infty}.$ We recall that Metric Interval Temporal Logic was introduced in [1] as a fragment of Metric Temporal Logic in which temporal operators may “quantify” over nonsingular intervals only. More precisely, the logic ${\rm MTL}_{\infty}$ is a modification and an extension of a system proposed in [9]. Same as with the latter system, only quantifications over nonsingular intervals are allowed in ${\rm MTL}_{\infty}$. Differently from the system in [9], an induction schema is provable in ${\rm MTL}_{\infty},$ thanks to the presence of some infinitary rules and axioms. Moreover, applications of the cut rule can be restricted to very simple formulas (see [2, Theorem 3.4]). In ${\rm MTL}_{\infty}$ there are relational formulas that describe properties of the underlying time flow and labelled formulas that express temporal statements. Regarding labelled deductive systems, we refer the reader to [6, 12].

In ${\rm MTL}_{\infty},$ binary propositional connectives only apply to formulas of the same kind and the deduction rules deal separately (as much as possible) with the relational and the labelled component of the deductive system.

Apart from recovering an induction schema and retaining a suitable cut-elimination property, a motivation for studying ${\rm MTL}_{\infty}$ was the remark made in [9] that, differently from the fully developed model checking techniques, proof-theoretic investigations of Metric Temporal Logic had been only partly attempted until that time.

Although familiarity with the content of [2] might be helpful, we will keep this paper as much self-contained as possible. We will refer to [2] to avoid unnecessary repetitions or for comments and further motivations for introducing ${\rm MTL}_{\infty}$.

In this paper we aim at temporalizing ${\rm MTL}_{\infty}.$ More precisely, but still vaguely, we want to put a copy of ${\rm MTL}_{\infty}$ on top of itself and investigate the properties of the resulting two-dimensional system, to be called ${\rm MTL}_{\infty}^{2}.$ The semantic intuition is that there are two kinds of time flows, an internal one and an external one, each being a dense linear ordering with least but no greatest element. At each point of the external flow it corresponds a copy of the internal time flow. Roughly speaking, each copy of the internal time flow and the external one will be governed by the ${\rm MTL}_{\infty}$ logic of [2]. Temporal operators do quantify over (possibly unbounded) intervals in the same way as in ${\rm MTL}_{\infty}.$

It is worth mentioning that the temporalization of certain systems has been studied in [4], where the authors investigate the so called external way of temporalizing a logic system. In the external approach it is not necessary to have detailed knowledge about the components of the system. We anticipate that, differently from [4], we will need a detailed knowledge of the components in order to establish cut elimination for the resulting system.

Various techniques for combining temporal logic systems have been developed also in [5]. In that approach, constraints need to be specified in order to ensure that properties of the combining logics are retained by the combined system. More precisely, in [5] the authors investigate the transfer of soundness, completeness and decidability from the components to the system they generate. We point out that they do not establish any proof-theoretic property of the resulting systems. In this paper, in addition to proving soundness and completeness of ${\rm MTL}_{\infty}^{2}$ with respect to adequate semantics and sequent calculus, we will also get a semantic proof of a partial cut-elimination theorem.

We also point out that a two-dimensional system can be used to describe a temporal logic for time granularity. For such a logic can be regarded as a combination of simpler temporal logics in a way that properties of the resulting system can be derived from those of its components. For a survey on temporal logics for time granularity, we refer the reader to [3].

Eventually we recall that, in the literature, one can find general methods for obtaining a system that admits full cut-elimination, starting from a system with axioms. They are based on the replacement of axioms with rules. See the method introduced in [10] and subsequently developed by the same authors in other works. In our opinion, the technique proposed in [10] is a clever way of hiding the cuts within the added rules. The reader should bear in mind that, differently from our work, [10] originates from purely proof-theoretical motivations. A stronger motivation for dealing with a system which is not completely cut-free is that application of the technique in [10] to a concrete deduction system with axioms like ours results in the replacement of naturally formulated axioms (whose intuitive meaning is clearly understood) with rules which are far less intuitive. In our opinion, the latter phenomenon is not a point in favor of a potential usability of the resulting system.

The rest of the paper is organized as follows.

In Section 2, we introduce syntax and semantics of ${\rm MTL}_{\infty}^{2}.$

In Section 3 we introduce the sequent calculus. We also point out that two induction schemas (one for each kind of time flow) are provable in ${\rm MTL}_{\infty}^{2}.$

In Section 5 we establish completeness and we get cut-elimination, by suitably modifying the reduction tree construction technique of predicate logic. Differently from [2], we do not make use of any first order translation of the ${\rm MTL}_{\infty}^{2}$ temporal formulas, but we directly construct the reduction tree of a sequent by means of the ${\rm MTL}_{\infty}^{2}$ deduction rules.

Eventually, by applying a result in [2], we get completeness of ${\rm MTL}_{\infty}^{2}$ with respect to the family of structures where the underlying time flows are given by the nonnegative rational numbers and the time intervals are determined by a very simple function.

2 Syntax and semantics

We recall that the logic $L_{\omega_{1}\omega}$ is an extension of first order logic where countable conjunctions and disjunctions are allowed (see [8]).

As is usual we identify a language $L$ with its extra logical symbols. We write $\varphi\in L$ as an abbreviation for “$\varphi$ is an $L$-formula”. Similarly with $L$-terms.

We denote the set of natural numbers by $\omega.$

2.1 Syntax

The language of ${\rm MTL}^{2}_{\infty}$ is formed by an internal language $L_{i}$ and an external language $L_{e}.$ Each of these two languages comprises a relational component $L_{*,r}.$ and a labelled component $L_{*,l},$ where $*\in\{i,e\}.$ We begin by introducing the two components of $L_{i}$ and the corresponding formulas.

• •

$L_{i,r}=\{f,<,c\}$ is a first order language with equality and $f$, $<$, $c$ are a unary function, a binary relation and a constant symbol respectively. We have one additional connective $\bigvee$ for (countable) infinitary disjunction. We use lower case letters $v,w,x,y,z$ (possibly indexed) for the (meta)variables of $L_{i,r}.$ We denote by $V_{i}$ the set of $L_{i,r}$-variables.

We denote by $T_{i}$ the set of $L_{i,r}$-terms. We use letters $s,t,u$ (possibly indexed) for the $L_{i,r}$-terms. The set $F_{i,r}$ of $L_{i,r}$-formulas (to be called internal relational formulas) is the least set containing:

1. –

the finitary $L_{i,r}$-formulas; 2. –

all the subformulas (in the sense of the $L_{\omega_{1}\omega}$ logic) of the infinitary formulas of the form $\forall x\bigvee_{n\in\omega}(x\mathchar 12604\relax f^{n}(c)).$ Hence the set of subformulas of $\forall x\bigvee_{n\in\omega}(x\mathchar 12604\relax f^{n}(c))$ contains the formula itself, $\bigvee_{n\in\omega}(t\mathchar 12604\relax f^{n}(c))$ and $t\mathchar 12604\relax f^{k}(c)$ for all relational terms $t$ and all $k\in{\omega}.$ (Here and in the following we let $f^{0}(t)=t$ for all terms $t.$)

• •

$L_{i,t}$ is a propositional language with a set $\mathbf{P}=\{p_{n}:n\in\omega\}$ of propositional letters; the propositional connectives and, for all $m<n$ in ${\omega},$ the temporal operators

[TABLE]

The semantics of the temporal operators will be introduced in Section 2.2. We write $\Box_{(m,n)}$ to denote any of the above operators, where $m\in\omega$ and $n\in\omega\cup\{\infty\}.$

The set $F_{i,t}$ of $L_{i,t}$-formulas (to be called internal temporal formulas) is the least set $A$ that contains the proposition symbols and is closed under application of the propositional connectives and under the following formation rules: if $\alpha\in A$ then $\Box_{(m,n)}\alpha$ is in $A,$ where $\Box_{(m,n)}$ is any of the temporal operators.

The set $F_{i,l}$ of internal labelled formulas is the set of all expressions of the form $s:\psi,$ where $s\in T_{i}$ and $\psi\in F_{i,t}.$

What we have introduced so far is basically the syntax of ${\rm MTL}_{\infty}.$ Logic ${\rm MTL}_{\infty}$ has two kinds of formulas: the relational and the labelled ones. To sum up: the formulas in $F_{i,t}$ are those of the propositional metric temporal logic underlying ${\rm MTL}_{\infty}.$ A formula $\alpha\in F_{i,t}$ can be decorated by an internal label $s$ (an element of $T_{i}$) to form the internal labelled formula $s:\alpha.$ Once $s:\alpha$ has been formed, it cannot be used to construct a more complicated formula. By this we mean that, for instance, the conjunction of two internal labelled formulas is not an internal labelled formula, but it will be a formula at the second level of the temporalization, as we explain below.

As we said already, ${\rm MTL}^{2}_{\infty}$ is obtained by putting a copy of ${\rm MTL}_{\infty}$ on top ${\rm MTL}_{\infty}$ itself. Therefore we define $L_{e,r},T_{e},F_{e,r},$ (“e” for “external”) as above, by using the same symbols, this time in upper case, for the extralogical symbols and the variables. There will be no ambiguity in using $<$ for both the internal and the external predicate symbols.

Let $\overline{F}_{i,l}$ be the the set obtained by closing $F_{i,l}$ under application of (external) propositional connectives and temporal operators. The intuition is that the formulas in $F_{i,l}$ play the role of the atomic temporal formulas for the external logic and $\overline{F}_{i,l}$ is thus the set of all the external temporal formulas. The set $F_{e,l}$ of external labelled formulas is the set of all expressions of the form $S:\beta,$ where $S\in T_{e}$ and $\beta\in\overline{F}_{i,l}\cup F_{i,r}.$ The definition of $F_{e,l}$ agrees with the spirit of ${\rm MTL}_{\infty},$ where the relational and the labelled formulas are not “mixed”. We will use upper case letters $A,B,\dots$ (possibly indexed) to denote formulas in $F_{e,r}\cup F_{e,l}.$ We say that a formula $S:\beta$ in $F_{e,l}$ is atomic if the formula $\beta$ is atomic.

Here is a simple example: let $S$ be an external term and $t_{1}:\alpha_{1},t_{2}:\alpha_{2}$ be internal labelled formulas. As we said above, the expression $(t_{1}:\alpha_{1})\land(t_{2}:\alpha_{2})$ is not an internal labelled formula, but $S:(t_{1}:\alpha_{1})\land(t_{2}:\alpha_{2})$ is an external labelled one. Even if we have not defined the semantics yet, to help the reader’s intuition we anticipate that the latter formula will be true in a structure at the external time instant “$S$” if, in the internal time flow corresponding to “$S$”, formulas $\alpha_{1}$ and $\alpha_{2}$ are true at time instants “$t_{1}$” and “$t_{2}$” respectively.

In the following we will deal with sequents. As is usual, a sequent is a formal expression of the form $A_{1},\dots,A_{m}\vdash B_{1},\dots,B_{n},$ for some $m,n\in\omega,$ where $A_{1},\dots,A_{m}$ and $B_{1},\dots,B_{n}$ are lists of formulas in $F_{e,r}\cup F_{e,l}.$

2.2 Semantics

The notation introduced in section 2.1 is in force. In the following we use standard model-theoretic notation (see, for instance, [8]).

A pre-structure is a a tuple of the form $(\mathbf{M},(\mathbf{N}_{a})_{a\in A}))$ such that:

$\mathbf{M}=(M,<,0,g:M\rightarrow M),$ where $(M,<,0)$ a dense linear ordering with least element 0 but no greatest element and $g$ a strictly increasing function such that, for all $a\in M,$ $a<g(a)$ and the sequence $\{g^{n}(0):n\in\omega\}$ is cofinal in $M$ (namely, for all $a\in M$ there exists $n\in\omega$ such that $a<g^{n}(0)$);

• -

for each $a\in M,$ $\mathbf{N}_{a}=(N_{a},<_{a},0_{a},g_{a}:N_{a}\rightarrow N_{a})$ is a first-order structure that satisfies analogous properties to those of $\mathbf{M}.$

For notational simplicity, we will write $(\mathbf{M},\mathbf{N}_{a})_{a\in A}$ for $(\mathbf{M},(\mathbf{N}_{a})_{a\in A})).$

In order to assign a truth value to a formula (internal or external) we fix

an assignment $\sigma:V_{e}\rightarrow M,$ where we denote by $V_{e}$ the set of $L_{e,r}$-variables; 2. -

a family of assignments $\{\sigma_{a}:V_{i}\rightarrow N_{a}\}_{a\in M},$ where where we denote by $V_{i}$ the set of $L_{i,r}$-variables; 3. -

a family $\{p^{\mathbf{N}_{a}}:p\in\mathbf{P}\}$ of subsets of $N_{a},$ for each $a\in M.$ The set $p^{\mathbf{N}_{a}}$ is intended to be the set of points in $N_{a}$ where the propositional letter $p$ is true.

We write $t^{\mathbf{N}_{a},\sigma_{a}}$ to denote the interpretation of $t\in T_{i}$ in $\mathbf{N}_{a}$ under $\sigma_{a}.$ Let $b\in N_{a}.$ We denote by $\sigma_{a}(x/b)$ the assignment that differs from $\sigma_{a}$ at most on the variable $x,$ on which it takes value $b.$

The truth value of an $L_{i,r}$-formula in $\mathbf{N}_{a}$ under $\sigma_{a}$ is given by its first-order semantics.

Let $t\in T_{i}$ and let $\psi\in F_{i,t}.$ We fix $a\in M.$ Let $\overline{b}=t^{\mathbf{N}_{a},\sigma_{a}}.$ We recursively define $\mathbf{N}_{a},\sigma_{a},(p^{\mathbf{N}_{a}})_{p\in\mathbf{P}}\models t:\psi$ as follows.

$\mathbf{N}_{a},\sigma_{a},(p^{\mathbf{N}_{a}})_{p\in\mathbf{P}}\models t:p$  if  $\overline{b}\in p^{\mathbf{N}_{a}};$ 2. -

the cases relative to the propositional connectives are treated as expected; 3. -

$\mathbf{N}_{a},\sigma_{a},(p^{\mathbf{N}_{a}})_{p\in\mathbf{P}}\models t:\Box_{[m,n]}\psi$ if, for all $d\in N_{a}$ such that $(g_{a})^{m}(\overline{b})\leq_{a}d\leq_{a}(g_{a})^{n}(\overline{b}),$ it holds that ${\mathbf{N}_{a}},\sigma_{a}(x/d),(p^{\mathbf{N}_{a}})_{p\in\mathbf{P}}\models x:\psi.$ 4. -

$\mathbf{N}_{a},\sigma_{a},(p^{\mathbf{N}_{a}})_{p\in\mathbf{P}}\models t:\Box_{]m,\infty[}\alpha$ if, for all $d\in N_{a}$ such that $g_{a}^{m}(\overline{b})<_{a}d,$ it holds that ${\mathbf{N}_{a}},\sigma_{a}(x/d),(p^{\mathbf{N}_{a}})_{p\in\mathbf{P}}\models x:\psi.$

(The cases relative to the other temporal operators are similar.)

We let $\mathcal{M}=(\mathbf{M},\mathbf{N}_{a},(p^{\mathbf{N}_{a}})_{p\in\mathbf{P}},\sigma,\sigma_{a})_{a\in M}$ and, with a little abuse of the model-theoretic terminology, we call $\mathcal{M}$ a structure. We say that $\mathcal{M}$ is based on the pre-structure $(\mathbf{M},\mathbf{N}_{a})_{a\in M}.$

As with the internal relational formulas, the truth value of an $L_{e,r}$-formula $\alpha$ in $\mathbf{M}$ under $\sigma$ is given by by its first-order semantics. Relative to such an $\alpha,$ we will often write $\mathcal{M}\models\alpha$ instead of $\mathbf{M},\sigma\models\alpha,$ since there is no ambiguity.

Relative to $\mathbf{M},\sigma$ we will use the same notation previously introduced for $\mathbf{N}_{a},\sigma_{a},$ $a\in M.$ Let $T\in T_{e}$ and let $\overline{a}\in M$ be the interpretation $T^{\mathbf{M},\sigma}$ of $T$ in $\mathbf{M}$ under $\sigma.$

If $\varphi\in F_{i,r},$ then $\mathcal{M}\models T:\varphi$ if $\mathbf{N}_{\overline{a}},\sigma_{\overline{a}}\models\varphi.$

Next we say when $\mathcal{M}\models T:\varphi,$ for $\varphi\in\overline{F}_{i,l}.$ Basically we will repeat (with the necessary changes) the definition that we gave in the case of the internal formulas. We provide some details for sake of clarity. Recall that the “atomic” formulas in $\overline{F}_{i,l}$ are those of the form $t:\psi,$ where $t\in T_{i}$ and $\psi\in F_{i,t}.$

$\mathcal{M}\models T:t:\psi$ if $\mathbf{N}_{\overline{a}}\models t:\psi;$

• -

the propositional cases are treated as expected;

• -

$\mathcal{M}\models T:\Box_{[m,n]}\eta$ if, for all $d\in M$ such that $g^{m}(\overline{a})\leq d\leq g^{n}(\overline{a}),$ it holds that $(\mathbf{M},\mathbf{N}_{a},(p^{\mathbf{N}_{a}})_{p\in\mathbf{P}},\sigma(X/d),\sigma_{a})_{a\in M}\models X:\eta.$

(The other cases are similar.)

We say that a sequent $\Gamma\vdash\Delta$ is true, or satisfied, in a structure $\mathcal{M}$ (and we write $\mathcal{M}\models\Gamma\vdash\Delta$) if $\mathcal{M}$ does not satisfy some of the formulas in $\Gamma$ or satisfies some of the formulas in $\Delta.$ A sequent is valid if it is true in all structures.

3 Sequent calculus

In this section we introduce the axioms and the rules of $\mbox{MTL}_{\infty}^{2}.$ Most of the axioms are formulated as Post rules.

In the following we first introduce some axiom schemas, then we will consider instances of those schemas. We assume that the reader can easily figure out what we mean by an instance of some axiom schema. For instance, for all $S_{1},S_{2}$ in $T_{e},$ the sequent $S_{1}=S_{2},\rho[S_{1}/Z]\vdash\rho[S_{2}/Z]$ is an instance of the axiom schema $X=Y,\rho[X/Z]\vdash\rho[Y/Z]$.

The reason for dealing with instances rather than with schemas is to obtain a suitable cut-elimination theorem. The reader who is not interested in proof-theoretic issues may opt for axiom schemas.

Axioms for equality

Among the axioms for equality are all instances of the following axiom schemas.

[TABLE]

[TABLE]

$(T\in T_{e},\ \rho\mbox{\ an atomic formula in\ }F_{i,r})$

In addition, we have the following equality axioms:

[TABLE]

As it can be immediately realized, the axiom schemas on the second line are obtained from those on the first one by using internal variables/symbols and by “decorating” with a same external label all the formulas involved. Loosely speaking, we will say that the latter schemas are the internal formulations of the former. Later we will adopt the same terminology relative to the rules.

Extralogical axioms

With the extralogical axioms we axiomatize the class of structures under consideration (see Section 2.2).

We start with external extralogical axiom schemas stating that $<$ is a dense linear ordering with least element $C$:

[TABLE]

[TABLE]

We do not include an axiom stating that there is no greatest element, because the latter property can be derived from the leftmost axiom of the following list.

The external extralogical axioms also express the properties of the function symbol $F$ and of the sequence $\{F^{n}(C):n\in\omega\}$:

[TABLE]

The external extralogical axioms are all instances of the above schemas.

As with the axioms for equality, we have internal versions of all the external extralogical axioms. We leave to the reader the easy task of formulating them.

In the following we refer to [7, Chapter 2] for a formulation of the rules of first-order sequent calculus.

Identity axiom and cut rule

They are:

[TABLE]

respectively. They apply to any formula $A\in F_{e,r}\cup F_{e,l}.$

Structural rules

The structural rules are those of Weakening, Exchange and Contraction from sequent calculus. They apply to any formula in $F_{e,r}\cup F_{e,l}.$

Rules for relational formulas

The rules for the external relational formulas are those of the first-order sequent calculus for the finitary connectives and the quantifiers. In addition, we have the following rules for the infinitary disjunction:

{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 2.63889pt\hbox{\displaystyle\penalty 1{\Gamma,T\mathchar 12604\relax F^{n}(C)\vdash\Delta}{n\in\omega}}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=102.82834pt\hbox{\kern 3.00003pt$$}}}\hbox{\kern 0.0pt\hbox{\displaystyle\Gamma,\bigvee{n\in\omega}(T\mathchar 12604\relax F^{n}(C))\vdash\Delta}}}}   {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 12.15132pt\hbox{\displaystyle\penalty 1\Gamma\vdash T\mathchar 12604\relax F^{m}(C),\Delta}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=103.93945pt\hbox{\kern 3.00003pt\quad\mbox{for all $m\in\omega.$}}}}\hbox{\kern 0.0pt\hbox{\displaystyle\Gamma\vdash\bigvee_{n\in\omega}(T\mathchar 12604\relax F^{n}(C)),\Delta}}}}

We also have internal versions of all the rules above for the labelled external formulas of the form $T:\rho,$ where $T\in T_{e}$ and $\rho\in F_{i,r}.$ For sake of clarity, we formulate the rules concerning the infinitary disjunction:

{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 2.63889pt\hbox{\displaystyle\penalty 1{\Gamma,T:t\mathchar 12604\relax f^{n}(c)\vdash\Delta}{n\in\omega}}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=109.39053pt\hbox{\kern 3.00003pt$$}}}\hbox{\kern 0.0pt\hbox{\displaystyle\Gamma,T:\bigvee{n\in\omega}(t\mathchar 12604\relax f^{n}(c))\vdash\Delta}}}}   {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 12.15132pt\hbox{\displaystyle\penalty 1\Gamma\vdash T:t\mathchar 12604\relax f^{m}(c),\Delta}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=110.50165pt\hbox{\kern 3.00003pt\quad\mbox{for all $m\in\omega.$}}}}\hbox{\kern 0.0pt\hbox{\displaystyle\Gamma\vdash T:\bigvee_{n\in\omega}(t\mathchar 12604\relax f^{n}(c)),\Delta}}}}

Propositional rules

The propositional rules for the external labelled formulas closely follow the standard propositional rules. As an example, we give the the rules for implication:

{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1\Gamma,T:\alpha\vdash T:\beta,\Delta}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=77.2126pt\hbox{\kern 3.00003pt$$}}}\hbox{\kern 4.17186pt\hbox{\displaystyle\Gamma\vdash T:\alpha\rightarrow\beta,\Delta}}}}     {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1\Gamma,T:\beta\vdash\Delta\qquad\Gamma\vdash T:\alpha,\Delta}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=123.46254pt\hbox{\kern 3.00003pt$$}}}\hbox{\kern 27.85239pt\hbox{\displaystyle\Gamma,T:\alpha\rightarrow\beta\vdash\Delta}}}}\hskip 5.69054pt\ (\alpha,\beta\in\overline{F}_{i,l}\mbox{\ or\ }\alpha,\beta\in F_{i,r})

Notice the constraint on the application of the two rules above, which is a consequence of the constraint that we put on the formation of the set $F_{e,l}$ of external labelled formulas. As we already said, we do not want to “mix up” the relational and temporal components of the system.

We also have internal versions of all the propositional rules for the external labelled formulas. For instance, the internal versions of the last two rules are the following:

{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1\Gamma,T:t:\eta\vdash T:t:\xi,\Delta}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=98.38829pt\hbox{\kern 3.00003pt$$}}}\hbox{\kern 10.14401pt\hbox{\displaystyle\Gamma\vdash T:t:\eta\rightarrow\xi,\Delta}}}}   {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1\Gamma,T:t:\xi\vdash\Delta\qquad\Gamma\vdash T:t:\eta,\Delta}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=144.63823pt\hbox{\kern 3.00003pt$$}}}\hbox{\kern 33.82454pt\hbox{\displaystyle\Gamma,T:t:\eta\rightarrow\xi\vdash\Delta}}}}\quad(\eta,\xi\in F_{i,t})

Temporal rules

The rules for temporal operators are essentially the same as in [2]. As above, we have a “duplication” of the rules to take into account the internal and the external level of the deductive system. For instance, the rules governing $\Box_{[m,n]}$ are:

{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1\Gamma,F^{m}(T)\leq X,X\leq F^{n}(T)\vdash X:\alpha,\Delta}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=160.45943pt\hbox{\kern 3.00003pt\qquad\mbox{($\alpha\in\overline{F}_{i,l};$ $X$ not free in $\Gamma\cup\Delta\cup\{T\}$) }}}}\hbox{\kern 43.53978pt\hbox{\displaystyle\Gamma\vdash T:\Box_{[m,n]}\alpha,\Delta}}}}

{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1\Gamma\vdash F^{m}(T)\leq S,\Delta\quad\Gamma\vdash S\leq F^{n}(T),\Delta\quad\Gamma,S:\alpha\vdash\Delta}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=225.87593pt\hbox{\kern 3.00003pt$$}}}\hbox{\kern 76.80359pt\hbox{\displaystyle\Gamma,T:\Box_{[m,n]}\alpha\vdash\Delta}}}}\qquad(\alpha\in\overline{F}_{i,l})

{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1\Gamma,T:f^{m}(t)\leq x,T:x\leq f^{n}(t)\vdash T:x:\eta,\Delta}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=185.2809pt\hbox{\kern 3.00003pt\quad\mbox{($\eta\in F_{i,t};$ $x$ not free in $\Gamma\cup\Delta\cup\{t\}$})}}}\hbox{\kern 50.69421pt\hbox{\displaystyle\Gamma\vdash T:t:\Box_{[m,n]}\mathfrak{\eta},\Delta}}}}

{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1\Gamma\vdash T:f^{m}(t)\leq s,\Delta\quad\Gamma\vdash T:s\leq f^{n}(t),\Delta\quad\Gamma,T:s:\eta\vdash\Delta}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=254.69743pt\hbox{\kern 3.00003pt$$}}}\hbox{\kern 85.95804pt\hbox{\displaystyle\Gamma,T:t:\Box_{[m,n]}\eta\vdash\Delta}}}}\qquad(\eta\in F_{i,t})

The rules for the other temporal operators are similar. They can be easily derived from the rules above.

Proofs are standardly defined. Notice that, although each branch in a proof is finite, the proof itself may have infinite height because of the infinitary rules.

It may help the reader’s intuition to keep in mind that, from the point of view of the internal logic, the atomic temporal formulas are those in the set $\mathbf{P}$ of propositional letters. The latter set gets closed under (internal) boolean connectives and (internal) modal operators to form the set $F_{i,t}$ of internal temporal formulas.

From the point of view of the external logic, the formulas in the set $F_{i,l}$ of internal labelled formulas play the role of atomic temporal formulas. By taking the closure $\overline{F}_{i,l}$ of $F_{i,l}$ under (external) boolean connectives and (external) modal operators we get the external temporal formulas.

Forgetting about the labels, the deduction rules governing $F_{i,t}$ are those of propositional sequent calculus and those for the (internal) temporal operators. Similarly, the deduction rules governing $\overline{F}_{i,l}$ are those of propositional sequent calculus and those for the (external) temporal operators. Basically, we have two copies of the same sequent calculus, one for each level.

Each relational component is governed by the deduction rules of the first-order sequent calculus, plus the corresponding infinitary rule for disjunction.

As is usual, we denote by $\vdash$ the provability relation in $\mbox{MTL}_{\infty}^{2}.$

We end this section by remarking that two induction schemas are provable in $\mbox{MTL}_{\infty}^{2}.$ More precisely, let $T\in T_{e}$ and $\alpha\in\overline{F}_{i,l}.$ Then

[TABLE]

is provable in $\rm{MTL}_{\infty}^{2}.$ Up to typographic changes, the proof is the same as the induction schema in [2]. In a similar way, for every $T\in T_{e},t\in T_{i}$ and $\eta\in F_{i,t},$ we have

[TABLE]

We refer the reader to [2] for a remark on the unprovability of (1) when the infinitary axiom $\vdash\bigvee_{n\in\omega}(X<F^{n}(C))$ gets removed. The example given therein can be easily adapted to show the unprovability of (2) without the axiom $\vdash T:\bigvee_{n\in\omega}(x<f^{n}(c)).$

4 Underlying unlabelled systems

Some labelled logics are built on top of unlabelled systems. Even if we have deliberately chosen not to describe in full detail a possible unlabelled system underlying $\mbox{MTL}_{\infty}^{2},$ in this subsection we provide some insight about the semantics of the latter. We are reluctant to call the resulting object a logic. For it should be clear that, for the purposes of this paper, a logic is made of two components: a semantic and a deductive one. Indeed the reader can easily convince himself that deduction rules for the temporal operators corresponding to those introduced in Section 3 cannot be formulated in absence of labels, even in case of the one-dimensional system $\mbox{MTL}_{\infty}$ introduced in [2].

For sake of simplicity, let us consider $\mbox{MTL}_{\infty}.$ The formation rules for the underlying unlabelled formulas are those of propositional first-order logic expanded with those for the temporal operators $\Box_{(m,n)},$ with $m\in\omega$ and $n\in\omega\cup\{\infty\}.$ More precisely: if $\alpha$ is a formula then so is $\Box_{(m,n)}\alpha,$ for all possible choices of the operator $\Box_{(m,n)}.$

The pre-structures which are adequate to interpret those unlabelled formulas are of the form $\mathbf{M}=(M,<,0,g:M\rightarrow M),$ where $(M,<,0)$ is a dense linear ordering with least element 0 but no greatest element and $g$ a strictly increasing function such that, for all $a\in M,$ $a<g(a)$ and the sequence $\{g^{n}(0):n\in\omega\}$ is cofinal in $M.$ In order to get a structure we must provide a family $\{p^{\mathbf{M}}:p\in\mathbf{P}\}$ of subsets of $M$. We let

[TABLE]

The semantics is Kripke-like. Let $\mathcal{M}$ be as in (1) and $m\in M.$ The definition of $\mathcal{M},m\models\alpha$ is by induction on $\alpha.$ We skip the the details (see Section 2 or [2] for insights).

We stipulate that an unlabelled formula $\alpha$ is valid if, for all $\mathcal{M}$ as in (1) and all $m\in M,$ $\mathcal{M},m\models\alpha.$

We make the trivial observation that, for $\mathcal{M}$ as (1) and $m\in M,$ by letting $M_{m}=\{x\in M:m\leq x\}$ and by denoting with the same names the restrictions of by $<$ and $g$ to $M_{m}$ respectively, the tuple $\mathbf{M}_{m}=(M_{m},<,m,g)$ together with the family $\{p^{\mathbf{M}}\cap M_{m}:p\in\mathbf{P}\}$ forms a structure as in (1). It follows that validity of $\alpha$ is equivalent to the following:

[TABLE]

Eventually, we notice that the latter is equivalent to the validity of the labelled formula $c:\alpha$ with respect to the $\mbox{MTL}_{\infty}$ semantics. By soundness and completeness of $\mbox{MTL}_{\infty}$ (see [2, Theorem 3.4]), validity of the unlabelled formula $\alpha$ is equivalent to the provability in $\mbox{MTL}_{\infty}$ of the labelled sequent $\vdash c:\alpha.$

Therefore we may use the $\mbox{MTL}_{\infty}$ calculus to investigate validity in the underlying unlabelled system. Admittedly, this is of limited interest because of the above mentioned fact that the unlabelled system lacks deduction rules for its temporal operators. As such, it is not a logic whose validity or provability relation we may want to investigate within another logic.

In light of soundness and completeness (see Corollary 5.2), we may proceed as above in the case of $\mbox{MTL}_{\infty}^{2}$ In this latter case, the underlying system should have two families of temporal operators $\Box^{i}_{(m,n)}$ and $\Box^{e}_{(m,n)},$ with $m\in\omega$ and $n\in\omega\cup\{\infty\}$ and with the obvious intuitive meaning of the superscripts i and e. We should also impose, among others, syntactic restrictions on the formation rules of formulas. For instance, no $\Box^{e}_{(m,n)}$ can occur on the right-hand side of a $\Box^{i}_{(m,n)}$ operator. The structures which are adequate to interpret the resulting class of formulas can be easily defined, by closely following Section 2.2.

As in the case of $\mbox{MTL}_{\infty},$ it is possibile to relate validity in the unlabelled system to validity with respect to the $\mbox{MTL}_{\infty}^{2}$ semantics. We skip the details and we provide a simple example: validity of the unlabelled formula $\Box^{e}_{[0,1]}\Box^{i}_{[0,1]}p$ turns out to be equivalent to the validity of the sequent $\vdash C:\Box_{[0,1]}c:\Box_{[0,1]}p.$

The same considerations as in the one-dimensional case apply. Unfortunately, even in this case the unlabelled system lacks deduction rules for the temporal operators.

5 Reduction tree construction and completeness

At the end of Section 2.2 we already said when a sequent is valid. It is a lengthy but easy task to verify that all the axioms are valid and that every provable sequence is valid. To prove the latter, proceed by induction on a derivation of a provable sequent.

We aim at proving that $\rm{MTL}_{\infty}^{2}$ is complete with respect to the class of structures that we introduced in Section 2.2.

5.1 The reduction tree

In this section we suitably modify the reduction tree construction technique of first order logic (see, for instance, Theorem 3.1.9, Remarks 3.1.11 and 3.1.12 in [7, §3.1]). Our aim is to get either a proof in $\rm{MTL}^{2}_{\infty}$ of a sequent $\Gamma\vdash\Delta$ or a tree with an infinite branch whose root is labelled $\Gamma\vdash\Delta.$ In Section 5.2 we will derive the unprovability of $\Gamma\vdash\Delta$ from the existence of such an infinite branch.

For simplicity we identify a node in a tree with its associated label.

We fix a sequent $\Gamma\vdash\Delta.$ We also fix

an ordering $A_{1},\ldots,A_{m}$ of all the formulas in $\Gamma\vdash\Delta$ (recall that all the $A_{i}$’s belong to $F_{e,r}\cup F_{e,l}$); 2. 2.

an enumeration of all axioms different from id, in which each axiom is repeated infinitely many times; 3. 3.

an enumeration ${\{{t}_{i}}\}_{i<\omega}$ of the set $T_{i}$ of $L_{i,r}$-terms; 4. 4.

an enumeration ${\{{S}_{i}}\}_{i<\omega}$ of the set $T_{e}$ of $L_{e,r}$-terms.

Next we recursively define a sequence $\{\mathbb{T}_{n}\}_{n<\omega}$ of well founded trees. We say that a branch in $\mathbb{T}_{n}$ is closed if its leaf is an axiom (of any kind), otherwise it is called open. It is intended that the following construction only applies to the open branches in a tree. Therefore, if for some $n$ all branches in $\mathbb{T}_{n}$ are closed, then $\mathbb{T}_{n}=\mathbb{T}_{m}$ for all $n<m.$

basis

$\mathbb{T}_{0}$ is $\Gamma\vdash\Delta$.

recursion

Assume that the trees $\mathbb{T}_{m},$ $m\leq n,$ have been already defined in a way that, for all $h<k\leq m,$ $\mathbb{T}_{k}$ is an upwards extension of $\mathbb{T}_{h}.$ If all the branches in $\mathbb{T}_{n}$ are closed, we stop. If not, we define $\mathbb{T}_{n+1}$ by extending each of the open branches in $\mathbb{T}_{n}$ upwards. With each open branch we proceed as follows.

Let $\Gamma^{n}\vdash\Delta^{n}$ be the leaf of an open branch in $\mathbb{T}_{n}.$  The formulas in $\Gamma^{n}\vdash\Delta^{n}$ come equipped with an ordering $A_{1},\ldots,A_{q}$ that has been determined by the previous steps of the construction (see cases 1–3 below).

We examine various cases, depending on the first formula $A_{1}$ in the ordering.

In the following, we write {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1S_{1}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox to9.50832pt{\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}}\hbox{\kern 3.00003pt$$}}}\hbox{\kern 0.0pt\hbox{\displaystyle S_{2}}}}} if the sequent $S_{2}$ can be proved from the sequent $S_{1}$ by application of finitely many structural rules.

1. 1.

$\Gamma^{n}\vdash\Delta^{n}$ is provable by means of structural rules only from some axiom (of any kind), say from $\Gamma^{\prime}\vdash\Delta^{\prime}$. In this case we extend $\Gamma^{n}\vdash\Delta^{n}$ upwards with the corresponding bit of derivation.

[TABLE]

Notice that the branch so obtained is closed. Therefore it will not be further extended. 2. 2.

Case 1 does not happen and $A_{1}$ is atomic.

In this case we examine the $n$-th element in the enumeration of the axioms. Let $B_{1},\ldots,B_{k}\vdash D_{1},\ldots,D_{m}$ be such element.

If $B_{1},\ldots,B_{k}$ all occur in $\Gamma^{n},$ we extend $\Gamma^{n}\vdash\Delta^{n}$ upwards as follows:

[TABLE]

For each $1\leq i\leq m,$ the ordering of the formulas in the leaf $\Gamma^{n},D_{i}\vdash\Delta^{n}$ is $A_{2},\ldots,A_{q},D_{i},A_{1}.$

If some among $B_{1},\ldots,B_{k}$ does not occur in $\Gamma^{n},$ we do not add any node to the current branch and we re-order the formulas in $\Gamma^{n}\vdash\Delta^{n}$ as follows: $A_{2},\dots,A_{q},A_{1}.$ 3. 3.

Case 1 does not happen and $A_{1}$ is not atomic. We consider several cases and subcases (one for each logical rule of the calculus). In the following we deal with few cases only. We invite the reader to work out the missing cases.

1. (a)

$A_{1}$ occurs in $\Gamma^{n}.$

1. (a1)

$A_{1}$ is $T:t:\eta\rightarrow\xi.$ We extend $\Gamma^{n}\vdash\Delta^{n}$ upwards as follows:

[TABLE]

The new orderings of the formulas in the left and the right leaf are $A_{2},\ldots,A_{q},T:t:\xi,A_{1}$ and $A_{2},\ldots,A_{q},T:t:\eta,A_{1}$ respectively. 2. (a2)

$A_{1}$ is $T:t:\Box_{[i,j]}\eta.$ Let $s$ be the first term in the enumeration ${\{{t}_{i}}\}_{i<\omega}$ that has not been used in the current branch in a previous application of this case to the formula $A_{1}$. We extend $\Gamma^{n}\vdash\Delta^{n}$ upwards as follows

[TABLE]

The orderings of the formulas in the new leaves are (from left to right):

[TABLE]

and $A_{2},\ldots,A_{q},T:s:\eta,A_{1}.$ 3. (a3)

$A_{1}$ is $T:\bigvee_{i\in\omega}(t\mathchar 12604\relax f^{i}(c)).$ We extend $\Gamma^{n}\vdash\Delta^{n}$ upwards as follows

[TABLE]

The ordering of the formulas in the leaf $\Gamma^{n},T:t\mathchar 12604\relax f^{i}(c)\vdash\Delta^{n}$ is $A_{2},\ldots,A_{q},T:t\mathchar 12604\relax f^{i}(c),A_{1},$ for all $i\in\omega.$ 2. (b)

$A_{1}$ occurs in $\Delta^{n}.$

1. (b1)

if $A_{1}$ is $T:t:\eta\rightarrow\xi.$ We extend $\Gamma^{n}\vdash\Delta^{n}$ upwards as follows

[TABLE]

The ordering of the formulas in the new leaf is:

$A_{2},\ldots,A_{q},T:t:\eta,T:t:\xi,A_{1}$ 2. (b2)

$A_{1}$ is $T:t:\Box_{[i,j]}\mathfrak{\eta}.$ We pick an internal variable $x$ that does not occur free in $\Gamma^{n}\cup\Delta^{n}\cup\{t\}$ and we extend $\Gamma^{n}\vdash\Delta^{n}$ upwards as follows

[TABLE]

The ordering of the formulas in the new leaf is

$A_{2},\ldots,A_{q},T:f^{i}(t)\leq x,T:x\leq f^{j}(t),T:x:\eta,A_{1}$ 3. (b3)

$A_{1}$ is $T:\bigvee_{i\in\omega}(t\mathchar 12604\relax f^{i}(c)).$ Let $m$ be the least natural number $k$ such that $T:t\mathchar 12604\relax f^{k}(c)$ does not occur in $\Delta^{n}.$ We extend $\Gamma^{n}\vdash\Delta^{n}$ upwards as follows

[TABLE]

The ordering of the formulas in the new leaf is

$A_{2},\ldots,A_{q},T:t\mathchar 12604\relax f^{m}(c),A_{1}.$

Remark 5.1*.*

By construction, $\mathbb{T}=\bigcup_{n\in\omega}\mathbb{T}_{n}$ is a tree, called the reduction tree of $\Gamma\vdash\Delta.$ Notice that the presence of axioms with empty premiss and the fact that each axiom different from id is repeated infinitely many times in the enumeration imply that any open branch keeps on being extended upwards. Therefore if $\mathbb{T}$ has no infinite branch there exists some $n\in\omega$ such that all the branches in the tree $\mathbb{T}_{n}$ are closed. It follows immediately from the construction that $\mathbb{T}=\mathbb{T}_{n}$ yields a proof $\Gamma\vdash\Delta.$ Since all applications of the cut rule take place in case 2, we actually get a proof of $\Gamma\vdash\Delta$ where all cut-formulas occur in the righthand side of some axiom different from id.

If there is some infinite branch in $\mathbb{T},$ in Section 5.2 we show how to get a countermodel of $\Gamma\vdash\Delta$ from such an infinite branch.

5.2 Completeness

Let us assume that the reduction tree $\mathbb{T}$ of the sequent $\Gamma\vdash\Delta$ constructed in Section 5.1 has an infinite branch $(\Gamma_{n}\vdash\Delta_{n})_{n\in\omega}.$ Let ${\overline{\Gamma}}=\bigcup\Gamma_{n}$ and ${\overline{\Delta}}=\bigcup\Delta_{n}.$

We define a structure $\mathcal{M}=(\mathbf{M},\mathbf{N}_{a},(p^{\mathbf{N}_{a}})_{p\in\mathbf{P}},\sigma,\sigma_{a})_{a\in M}$ by using $\overline{\Gamma}$ and $\overline{\Delta}.$

First we define $\mathbf{M}.$ We define a relation $\sim$ on the set $T_{e}$ of external terms by letting

[TABLE]

The tree construction and the first order axioms for equality imply that $\sim$ is an equivalence relation. Let $T^{\sim}$ be the $\sim$-equivalence class of term $T.$ We let

[TABLE]

We let $\mathbf{M}=(M,<^{\mathbf{M}},C^{\mathbf{M}},F^{\mathbf{M}}).$ (Notice the small notational abuse.) The axioms for equality and the reduction tree construction imply that everything is well-defined. Furthermore, the extralogical axioms and the reduction tree construction imply that $\mathbf{M}$ satisfies the required properties. Namely, $(M,<^{\mathbf{M}},C^{\mathbf{M}})$ is a dense linear ordering with least element $C^{\mathbf{M}}$ but no greatest element; the function $F^{\mathbf{M}}$ is strictly increasing; for all $T^{\sim}\in M,$ $T^{\sim}<^{\mathbf{M}}F(T)^{\sim}$ and the sequence $\{F^{n}(C)^{\sim}:n\in\omega\}$ is cofinal in $M.$

We define $\sigma:V_{e}\rightarrow M$ as follows: $\sigma(X)=X^{\sim}.$ By induction on external terms it follows that the interpretation $T^{{\mathbf{M}},\sigma}$ of term $T$ in $\mathbf{M}$ under $\sigma$ is just $T^{\sim},$ for each $T\in T_{e}.$

Next we basically repeat the construction of $\mathbf{M}$ to get $\mathbf{N}_{a},$ for each $a\in M.$ For each $S\in T_{e},$ we define an equivalence relation $\sim_{S}$ on $T_{i}$ as follows:

[TABLE]

Let $t^{S}$ be the $\sim_{S}$-equivalence class of $t\in T_{i}.$ For each $S\in T_{e},$ we let

[TABLE]

[TABLE]

Moreover, for each $p\in\mathbf{P},$ we let $p^{\mathbf{N}_{S}}=\{t^{S}:(S:t:p)\in\overline{\Gamma}\}.$ (Recall that we denote by $p^{\mathbf{N}_{S}}$ the set of points in $N_{S}$ where $p$ is true.)

As above, the reduction tree construction implies that everything is well-defined and that, for all $S\in T_{e},$ $\mathbf{N}_{S}$ satisfies the required properties.

We define $\sigma_{S}:V_{i}\rightarrow N_{S}$ as follows: $\sigma(x)=x^{S}.$ It follows easily that, for each $t\in T_{i},$ $t^{\mathbf{N}_{S},\sigma_{S}}=t^{S}.$

The careful reader may have already noticed that the support of the external time flow is the $\{T^{\sim}:T\in T_{e}\},$ but we defined above a family $\{\mathbf{N}_{S}\}_{S\in T_{e}}$ (instead of an indexed family on the $\sim$-equivalence classes of $T_{e},$ as required by the definition of pre-structure). We explain why: from the axioms and the construction of the reduction tree it follows that $\mathbf{N}_{S}=\mathbf{N}_{T}$ whenever $T^{\sim}=S^{\sim}.$ For instance, let us assume that $T=S$ and $T:t=s$ are both in $\Gamma^{n}$ and that $T=S,T:t=s\vdash S:t=s$ is the $n$-th element in the enumeration of the axioms (one such $n$ does exist because of the infinitely many repetitions). Then, extending upwards $\Gamma^{n}\vdash\Delta^{n}$ as prescribed by case 2 of the reduction tree construction, we get that $\Gamma^{n+1}\vdash\Delta^{n+1}$ is $\Gamma^{n},S:t=s\vdash\Delta^{n}.$ Hence $S:t=s$ is in $\overline{\Gamma}.$ Similarly, assuming $T^{\sim}=S^{\sim},$ we get $\sigma_{S}=\sigma_{T}$ and $p^{\mathbf{N}_{S}}=p^{\mathbf{N}_{T}},$ for all $p\in\mathbf{P}.$

Hence we simply let $\mathbf{N}_{S^{\sim}}=\mathbf{N}_{T}$ for some (for all) $T\in T_{e}$ such that $S\sim T.$ Similar considerations apply to $p^{\mathbf{N}_{S^{\sim}}}$ and $\sigma_{S^{\sim}}.$ Thus we get the structure

[TABLE]

However, motivated by the above considerations (and for sake of notational simplicity), in the following we identify $\mathcal{M}$ with $(\mathbf{M},\mathbf{N}_{S},(p^{\mathbf{N}_{S}})_{p\in\mathbf{P}},\sigma,\sigma_{S})_{S\in T_{e}}.$

Next we show that $\mathcal{M}$ witnesses the unprovability of the sequent $\Gamma\vdash\Delta.$ To do that we prove a stronger result.

Theorem 5.1**.**

Let $\mathcal{M}$ be the structure defined above. For every formula $A\in F_{e,r}\cup F_{e,l}$ it holds that

1. (1)

$A\in{\overline{\Gamma}}\Rightarrow\mathcal{M}\models A;$** 2. (2)

$A\in{\overline{\Delta}}\Rightarrow\mathcal{M}\not\models A.$**

Proof.

We prove simultaneously (1) and (2) by induction on each of the various classes of formulas.

$A\in F_{r,e}.$ The deduction rules governing $A$ are the rules for relational formulas (see Section  3). For those rules, the construction of the reduction tree proceeds as in the first order case. Therefore (1) and (2) can be proved in the same way as in the construction of the reduction tree for first order logic. The infinitary formulas are taken care of by the cases corresponding to (a3) and (b3) in the construction of the reduction tree for the external relational formulas. For instance, let us assume that $\bigvee_{n\in\omega}(T<F^{n}(C))$ occurs in $\overline{\Delta}.$ Notice that such formula becomes infinitely many times the first formula in the ordering of formulas in a sequent occurring in some infinite branch. Moreover, same as in case (b3) above, the reduction tree is constructed by systematically adding, for each $n\in\omega,$ the formula $T<F^{n}(C)$ to $\overline{\Delta}.$ Therefore, by inductive assumption, $\mathcal{M}\not\models T<F^{n}(C),$ for all $n\in\omega.$ The conclusion follows. 2. 2.

$A$ is of the form $T:\beta,$ for some $\beta\in F_{i,r}.$ We notice that the rules governing $A$ are “labelled” versions of those involved in the previous case. Basically, we proceed as in that case to get (1) and (2). 3. 3.

$A$ is of the form $T:\beta,$ for some $\beta\in\overline{F}_{i,l}.$

1. (a)

First we simultaneously prove (1) and (2) for $\beta$ of the form $t:\alpha,$ for some $t\in T_{i}$ and $\alpha\in F_{i,t}.$ We proceed by induction on $\alpha.$

Since $T^{\mathbf{M},\sigma}=T^{\sim}$ and $t^{\mathbf{N}_{T},\sigma_{T}}=t_{T},$ the cases when $\alpha$ is some propositional letter $p$ hold by definition of $p^{\mathbf{N}_{T}}$.

The propositional cases are straightforward by the construction of the reduction tree and by inductive assumption.

We are left with the case when $\alpha$ is of the form $\Box_{[i,j]}\eta$ (the cases relative to the other temporal operators are similar).

Let us assume that $T:t:\alpha$ is in $\overline{\Gamma}$. Let $n\in\omega$ be such that $T:t:\alpha$ is the first in the ordering of the formulas in $\Gamma_{n}\vdash\Delta_{n}.$ (Notice that there are infinitely many such $n$’s.) With reference to case 3(a2) of the reduction tree construction, we notice that:

1. –

if $f^{i}(t)_{T}\leq_{T}s_{T},$ namely if $T:f^{i}(t)\leq s$ is in $\overline{\Gamma},$ then $\Gamma^{n+1}\vdash\Delta^{n+1}$ cannot be the leftmost leaf; 2. –

if $s_{T}\leq_{T}f^{j}(t)_{T},$ then, similarly to the previous case, we get that $\Gamma^{n+1}\vdash\Delta^{n+1}$ cannot be the middle leaf.

Therefore, for all $s$ such that $f^{i}(t)_{T}\leq_{T}s_{T}\leq_{T}f^{j}(t)_{T},$ it holds that $T:s:\eta$ is in $\overline{\Gamma}.$ Hence, by inductive assumption, $\mathcal{M}\models T:s:\eta.$

Since, in 3(a2), $s$ was chosen as the first term in the enumeration $\{t_{i}\}_{i\in\omega}$ which was not used so far, for all $s\in T_{i}$ the formula $T:s:\eta$ is in $\overline{\Gamma}.$ Therefore $\mathcal{M}\models T:t:\alpha.$

Next, we assume that $T:t:\alpha$ is in $\overline{\Delta}.$ Let $n\in\omega$ be such that $T:t:\alpha$ is the first in the ordering of the formulas in $\Gamma_{n}\vdash\Delta_{n}.$ With reference to case 3(b2) of the reduction tree construction, we have that, for a suitably chosen variable $x$, $T:f^{i}(t)\leq x$ and $T:x\leq f^{j}(t)$ are in $\overline{\Gamma}$ and $T:x:\eta$ is in $\overline{\Delta}.$ By inductive assumption and by the semantics, we get

[TABLE]

Therefore $\mathcal{M}\not\models T:t:\Box_{[m,n]}\eta.$ 2. (b)

The propositional cases are straightforward. 3. (c)

Let $\beta$ be of the form $\Box_{[i,j]}\gamma,$ for some $\gamma\in\overline{F}_{i,l}.$ By the same argument used in 3a in the case relative to the the temporal operator, we get the required conclusion.

∎

Corollary 5.2**.**

(Completeness) Every valid sequent is provable in $\rm{MTL}_{\infty}^{2}.$

Proof.

If a sequent is valid then, by Theorem 5.1, its reduction tree has no infinite branch. Therefore the reduction tree yields a proof of the sequent. ∎

In the following we extend to pre-structures the isomorphism relation $\simeq$ between first order structures. We still use $\simeq$ for the extended relation.

We say that two pre-structures $(\mathbf{D},\mathbf{E}_{d})_{d\in D}$ and $(\mathbf{D}^{\prime},\mathbf{E}^{\prime}_{d})_{d\in D^{\prime}}$ are isomorphic if there exists a first-order isomorphism $g:\mathbf{D}\rightarrow\mathbf{D}^{\prime}$ such that, for all $d\in D,$ $\mathbf{E}_{d}\simeq\mathbf{E}^{\prime}_{g(d)}.$

Let $\mathbb{Q}^{+}$ be the set of nonnegative rationals and let $h:\mathbb{Q}^{+}\rightarrow\mathbb{Q}^{+}$ be the function defined by $h(q)=q+1.$ Let $\mathbf{Q}=(\mathbb{Q}^{+},<,0,h).$ We call canonical the pre-structure $\mathbf{Q}^{2}=(\mathbf{Q},\mathbf{Q}_{r})_{r\in\mathbb{Q}^{+}},$ where, for all $r\in\mathbb{Q}^{+},$ $\mathbf{Q}_{r}=\mathbf{Q}.$

Next we recall [2, Proposition 3.3], which is a variant of the back-and-forth technique by means of which the $\aleph_{0}$-categoricity of the theory of linear orders without endpoints is established. The content of the above mentioned proposition is the following: let $\mathbf{M}=(M,<,0,g:M\rightarrow M),$ where $(M,<,0)$ is a countable dense linear ordering with least element 0 but no greatest element; $g$ is a strictly increasing function such that, for all $a\in M,$ $a<g(a)$ and the sequence $\{g^{n}(0):n\in\omega\}$ is cofinal in $M.$ Then $\mathbf{M}$ is isomorphic to $\mathbf{Q}.$

We apply [2, Proposition 3.3] to $\mathbf{M}$ and $\mathbf{N}_{S}$ defined as in Section 5.1 and we get $\mathbf{M}\simeq\mathbf{Q}\simeq\mathbf{N}_{S},$ for all $S\in T_{e}.$ It follows that $(\mathbf{M},\mathbf{N}_{S})_{S\in T_{e}}\simeq(\mathbf{Q},\mathbf{Q}_{r})_{r\in\mathbb{Q}^{+}}.$

By Remark 5.1, we finally get the following strong form of a completeness theorem:

Theorem 5.3**.**

Let $\Gamma\vdash\Delta$ be a sequent. Then exactly one of the following holds:

1. (1)

there exists a proof of $\Gamma\vdash\Delta$ in $\rm{MTL}_{\infty}^{2}$ where each cut–formula occurs in the righthand side of some axiom different from id; 2. (2)

there exists a structure $\mathcal{M}$ having $\mathbf{Q}^{2}$ as underlying pre-structure such that $\mathcal{M}\not\models\Gamma\rightarrow\Delta.$

In particular, $\mbox{MTL}^{2}_{\infty}$ is complete with respect to the family of structures whose underlying pre-structure is the canonical one.

6 Final remarks

An application to be pursued in a future work is the mechanization of the ${\rm MTL}_{\infty}^{2}$ sequent calculus. Mechanization is a relevant issue within the class of temporal logics, in light of its strong connections with the area of formal verification. There are two main approaches to mechanization: one based on model checking; the other based on proof coding in a so called logical framework or proof assistant (CoQ or Isabelle, for instance). By the nature of the ${\rm MTL}_{\infty}^{2}$ sequent calculus, in which the deduction rules relative to each operator are independent of the others, and by the validity of a suitable form of cut-elimination, the proof coding approach seems to be the most promising.

Regarding the theoretical issues, we stress that ours is a study of the meaning of temporal operators in a two-dimensional time structure. The ${\rm MTL}_{\infty}^{2}$ rules do obey the structural proof theory paradigm that deduction rules must syntactically provide the “meaning” of each operator. It is worth noticing that the ${\rm MTL}_{\infty}^{2}$ rules show great similarity with those for bounded first order quantifiers.

Moreover, our approach does not require the temporalized and the temporalizing system being the same. In particular, the underlying time flows might have different structures or the systems might be endowed with different temporal operators. What is crucial is that both system do have a reasonably good sequent calculus. In this regard, we may investigate an intuitionistic version of ${\rm MTL}_{\infty}^{2}$ so to address issues like the the computational content of proofs; the Brower-Heyting-Kolmogorov interpretation of temporal operators; the existence of a lambda-calculus having the ${\rm MTL}_{\infty}^{2}$ formulas as types.

Notice that we have obtained a completeness theorem by using a syntax-driven technique. In our opinion, a Hilbert style formulation of ${\rm MTL}_{\infty}^{2}$ would hardly allow to achieve completeness.

It is worth noticing that application of our temporalization technique can be iterated in order to obtain an $n$-dimensional system, for each $n>2.$ All the constructions and the results obtained in this paper generalize to $n$-dimensional systems.

We point out that our technique does not allow to express properties of the interaction between the two dimensions. This requires the introduction of new types of formulas, the definition of their semantics and an extension of the deductive system. In this way the resulting system would be closer to a full combination of logics, rather than to the temporalization of one logic by means of another. As pointed out in [5], a full combination may affect completeness or the cut-elimination property. It may worth investigating to what extent it is possible to increase the expressive power of the resulting system while retaining the properties of the logics to be combined.

It may also worth investigating the decidability of ${\rm MTL}_{\infty}^{2}.$ One first step would be to establish the decidability of the one-dimensional logic ${\rm MTL}_{\infty}.$ We notice that the ${\rm MTL}_{\infty}$ axioms for the relational component do extend the axioms of a first order theory of dense linear orderings. The decidability of the latter theory can be quite easily achieved by means of model-theoretic techniques. Decidability is likely to be inherited by our extension.

In this regard, we recall the decidability result for Metric Interval Temporal Logic that has been obtained in [1] by reducing the satisfiability problem for that logic to a decidable problem for timed automata. The latter result refers to a subclass of our class of structures (the so called timed state sequences), but it is possible that a similar reduction technique applies to our setting.

Still it is not clear whether it is possible to combine two such completely different decision procedures in order to establish decidability of ${\rm MTL}_{\infty},$ also in consideration of the interaction between the relational and the temporal component of ${\rm MTL}_{\infty}$ due to the presence of labels.

In conclusion, even proving decidability of the one-dimensional ${\rm MTL}_{\infty}$ seems to be nontrivial. We leave it as an open problem.