Dynamic Temporal Logical Operations in Multi-Agent Logics

We study temporal multi-agent logics using a new approach to defining time for individual agents. It is assumed that in any time state each agent (in a sense) generates its own future time, which will only be available for analysis in the future. That is, the defined time interval depends both on the agent and on the initial state where the agent starts to act. It is also assumed that the agent may have intervals of forgotten (lost) time. We investigate problems of unification and problems of computable recognizing admissible inference rules. An algorithm is found for solving these problems based on the construction of a finite computable set of formulas which is a complete set of unifiers. We use the technique of projective formulas developed by S. Ghilardi. It is proved that any unifiable formula is in fact projective and an algorithm is constructed which creates its projective unifier. Thereby we solve the unification problem, and based at this, find the solution to the open problem of computable recognizing admissible inference rules.

Introduction

Modern mathematical nonclassical logic actively investigates and applies multi-agent and temporal logics. These applications are connected as with technical complexity and attractiveness of appearing problems as well as with consequent usage results in computer science. In particular, well known are applications modelling agents’ analysis and conclusions concerning reliability of information. In many cases these applications use time as an important and defying resource. Historically, introduction of temporal mathematical logic and its location to a separate discipline may be connected with works of A. Prior in the early 1950s. Nowadays logical investigations in this direction have shaped into an active research area, including different branches in mathematical logic and computer science (cf. [1,2,3]). One important case of such logics is the linear temporal logic ℒ𝔗ℒ, which has been used in analysis of protocols for computations, verification of correctness [4]. Initially, the time was viewed as a linear relation from the past to the future, matching well with human intuition. At the same time, with progress in mathematical tools for computation it was noted that mathematical structures could be more effectively represented by using branching computational threads. Based at this, the conception of branching time was formalized and applied. For instance, the logic of branching time CTL, which admits various different threads of computation in any point of computation state, was introduced in [5, 6]. Later, temporal logics with nontransitive time accessibility relations were investigated (see [7,8,9]).

The conception of branching time, in particular, motivated interest in multi-agent logic. The matter is that branching and further parallel computations may be treated as multi-agent ones. Any computational thread can be viewed as reasoning of a separate agent. Multi-agent logics were investigated by many researchers [10, 11], and else any multi-agent logic may be viewed as a multimodal one [12]. Unification problem was introduced in [13] concerning the task of automatical deduction (see also [14] concerning the rewriting problem). A bit later investigations shifted to the domain of logical unification—the case when instead of terms the formulas are viewed and instead of equality we may consider logical equivalence (or semantical equivalence) [15].

Basic problem of unification is a partial case of the problem of unification with parameters (coefficients)—the case when substitution is allowed only for pure variables but not for parameters (coefficients). (This, generally speaking, corresponds to just solving algebraic equations with coefficients.) The problem mentioned was solved by the author of the present paper for modal logics S4, Grz, and intuitionistic logic Int [16, 17].

The problem of unification for intuitionistic logic Int and modal logics over K4 has been studied by S. Ghilardi [18,19,20]. His approach was based on properties of projective formulas and projective approximations. For the logics under investigation, he worked out a technique for constructing finite complete sets of unifiers. In particular, when we have complete finite sets of unifiers we can directly solve the problem of admissibility for inference rules in these logics (Subsequently, Ghilardi’s technique was effectively used by many authors for study of inference rules.)

It would look very attractive to use the technique of projective formulas for solving unification problems and admissibility problems in temporal and especially multi-agent logics. First interesting results in this direction were obtained in [21], where it was proved that all formulas unifiable in the linear modal logic S4.3 are projective. (In that paper, it was noted that the ideas similar to projectivity in modal linear logics were suggested in [22].) Extending this result, Rybakov [23] proved that the same is true for linear temporal logic LTL (without operation NEXT; with NEXT, as shown in [24], there are unifiable but not projective formulas).

In the present paper, we consider temporal multi-agent logics which use dynamic operations of temporal accessibility. Our approach is underpinned by the idea that any agent being in any time state generates in a sense itself a future time relation which is accessible for him as all the possible future. In other words, this time interval depends both on the state point where the agent stays and on the view of the agent itself. Besides, we admit that any agent may possess intervals of completely forgotten time.

Our paper looks at problems of unification and problems of computable recognizing admissible inference rules. Here we use the technique of projective formulas developed by Ghilardi. It is proved that any unifiable formula is in fact projective, and we construct an algorithm which creates its projective unifier. Using this result, we solve the unification problem, and based at this, find the solution to the problem of computable recognizing admissible inference rules.

1. DEFINITIONS AND THE NOTATION

In this paper we extend research in multi-valued logics which are a popular field in nonclassical logic and information sciences. Here we introduce two new components: (i) a dynamic interpretation for time accessibility relations, and (ii) a concept of forgotten time—a presence of time intervals which are not accessible for agents analysis. In technical terms, we will study the unification problem (cf. [13,14,15]) and the problem of recognizing admissible inference rules (cf. [16, 17]). An instrumental framework for our research is the technique of working with multi-agents’ logics, which we constructed in the last 5 years, and the technique of projective formulas evolved by Ghilardi since 1997 (cf. [18,19,20]).

First, we recall some necessary definitions and the basic notation. Our logical language is an extension of the language of temporal logics. It includes the language of standard Boolean logic and the temporal logical operations U_j for agents where formation rules for formulas are as usual:

(a) any propositional letter is a formula;

(b) if φ and ψ are formulas, then φ ∧ ψ, φ ∨ ψ, φ → ψ, φ U_jψ, and ￢ φ are also formulas.

The formula φ U_jψ has a special meaning: it says that the formula φ always remains true until the formula ψ emerges first time as true in the perception of the agent j. Later we will give a semantical meaning of truth for that formula.

We start by defining linear frames for temporal logics. Any frame is a model (or an algebraic system) which has a (potentially infinite) base set S of all possible time states. That set S possesses a binary relation ≤ of temporal linear order.

The relation ≤ is meant as inducing a well ordering, which signifies that any nonempty subset X of S has a smallest (w.r.t. ≤) state a_X. We write

$${\forall }_{y}\in X\left({a}_{X}\le y\right).$$

The above assumption for S to be a well ordering is very important, in a sense crucial, for obtaining the main result of this paper. As an example of well ordering, we may take the set of all natural numbers N with usual linear order ≤ or any finite connections of this frame—for example,

$$N \oplus N \oplus N \oplus \cdots \oplus N, \mathrm{m \ times},$$

as well as any infinite concatenations of N, like

$$N \oplus N \oplus \dots N \oplus \dots ,$$

as well as all ordinal numbers, etc.

For any agent j ∈ J, the set X_j is a subset of the set S and X_j denotes the set of temporal states which are not accessible for the agent j (the states of time forgotten by j). Let us recall the following:

Definition 1. Frame F := <S,≤,X_j, j ∈ J> is said to be a frame of linear time with forgotten times X_j, j ∈ J.

Definition 2. A model M on a frame F is defined by assigning some valuation V on S for some set of propositional letters p, where V (p) ⊆ S, and all states from V (p) are meant as all time states where p is true w.r.t. V . And T(M) := S is said to be the base set of the model M.

Now we introduce the main new technical component of our models—namely a dynamicdefinition of accessibility by time for agents. We extend temporal models with the assumption that in any time state any agent has its own perception of time and the length of a visible time interval is its own (i.e. for any agent in any time state not depending on other time states).

Definition 3. A linear temporal nontransitive frame is the tuple

$$\mathcal{F}:=\langle S,\le ,\left\{{R}_{x}\left|x\in S\right.\right\}\rangle ,$$

where ≤ is a linear well ordering on S, and for all x ∈ S, relations R_x are standard linear orders which are just restrictions of ≤ from the frame to the interval

$$\left[x,{a}_{x}\right]:=\left\{y\left|y\in S\left(x\le y\le {a}_{x}\right)\right.\right\}$$

for some a_x ≥ x, a_x ∈ S. It is also possible that R_x is the linear order on the whole set {y | x ≤ y}.

In this definition, we can likewise put xR_xa_x, y ∈ (x, a_x), and ￢(yR_ya_x). That is, y is the state situated earlier than x, but y remembers even less than x. Besides, it is clear that all temporal accessibility relations together form a nontransitive relation: it may so happen that xR_xa_x, x < y < ax, i.e. (aR_xy) and (yR_ya_y), but ￢(xR_ya_y).

Thus any time state x ∈ S generates its own time relation R_x. Therefore the time now starts to be a dynamic not very stable relation which may change from one time state to another. At the same time, the global time R_x,0—time accessibility relation for the agent 0—remains to be the usual complete linear order ≤ on the whole frame, as before.

A model M on any frame F is defined by introducing a certain valuation V on F for some set of propositional letters p, V (p) ⊆ S. Recall that the frame and correspondingly the model may have sets of time states X_j forgotten by the agents j ∈ J (it is possible that X_j = ∅ for some (or all j)).

Now we may extend the valuations V to all possible formulas, but using the relation R_x instead of ≤ for computing truth values of formulas of kind φU_jψ (if j ≠ = 0) at any state x.

Definition 4. For all a ∈ T(M), put

$$\left(F,a\right)\Vert {-}_{V}p\Leftrightarrow p\in V\left(p\right).$$

For all Boolean logical connectives, the definition is standard.

For formulas φU_jψ, the definition is as follows (recall that U₀ is the logical operation for global time):

$$\begin{array}{c}\left(F,a\right)\Vert {-}_{V}\left(\varphi {\mathbf{U}}_{0}\psi \right)\Leftrightarrow \\ \left(\exists b\in T\right.\left(M\right)\left[\left(a\le b\right)\wedge \left(\left(F,b\right)\Vert {-}_{V}\psi \right)\right.\\ \&\forall c\left(a\le c<b\right)\Rightarrow \left.\left(F,c\right)\left.\Vert {-}_{V}\psi \right]\right);\\ \left(*\right)\left(F,a\right)\Vert {-}_{V}\left(\varphi {\mathbf{U}}_{j}\psi \right)\left(j\ne 0\right)\Leftrightarrow \\ \left[\left(F,a\right)\Vert {-}_{V}\psi \right]\vee \left(\left(F,a\right)\Vert {-}_{V}\varphi \right)\&\exists b\in T\left(M\right)\left(b\notin {X}_{j}\&\left(a{R}_{a}b\right)\right.\\ \&\left(F,b\right)\Vert {-}_{V}\psi \&\forall c\left(a<c<b\&c\notin {X}_{j}\right)\Rightarrow \left(F,c\right)\left.\Vert {-}_{V}\varphi \right).\end{array}$$

The fact that (F, a) ∥–_V φ in (∗) above fixes the state where the computation of truth is started.

Definition 5. The logic ${\mathcal{L}}_{\mathcal{D}}^{\mathcal{A}}$ is the set of all formulas which are true at all states of all models on linear temporal nontransitive frames.

2. TECHNIQUE OF PROJECTIVE FORMULAS

In this section we recall some information on unification and projective formulas needed in what follows. Initially, unification appeared in mathematical logic and computer science as the task of identifying if two different terms may be made equal by substituting other terms for variables. Then, the problem was extended to a wider area—problems of logical unification, i.e. the case when instead of equality we may use logical equivalence.

Let some logic L (the one introduced above in particular) having a modal logical operation □ (necessary) be fixed (in our case □φ = ￢(TU₀φ)). Let For_L be the set of all formulas in the language of this logic and P be a set of some propositional letters. A substitution for P is a mapping ε of P into For_L. Any substitution ε may be extended to the set of all formulas constructed out of P by the rule

$$\varepsilon \left(\varphi \left({x}_{1},\dots ,{x}_{n}\right)\right):=\varphi \left(\varepsilon \left({x}_{1}\right),\dots ,\varepsilon \left({x}_{n}\right)\right).$$

Definition 6. A formula φ is said to be unifiable in a logic L if there is a substitution ε (which is called a unifier for φ) such that ε(φ) ∈ L.

Definition 7. A unifier ε (for a formula φ in a logic L) is more general than a unifier ε₁ if there is a substitution δ such that for any propositional letter x,

$$\left[{\varepsilon }_{1}\left(x\right)\equiv \delta \left(\varepsilon \left(x\right)\right)\right]\in L.$$

Definition 8. A set of unifiers CU for a formula φ in a logic L is a complete set of unifiers if it has the following property:

for any unifier σ for φ in L there is σ1 in CU, where σ₁ is more general than the unifier σ.

If a one-element set {σ_p} is a complete set of unifiers for φ, then σ_p is said to be a most general unifier for φ.

If a logic has operation □ (necessary) expressible in the logic (in our case, for example, □φ = ￢(TU₀φ)), then the property of being projective can be expressed as follows.

Definition 9. A formula φ is said be projective for a logic L iff there is a substitution σ that is a unifier for φ (which is called projective) such that □φ → [x_i ≡ σ(x_i)] ∈ L for any letter x_i from φ.

Note that if a substitution σ_p is projective for some formula φ in a logic L, then {σ_p} forms a complete set of unifiers for φ (i.e. σ_p is a more general unifier for φ).

THEOREM 10. Let a logic L be decidable and there be an algorithm for verifying unifiability of any given formula in L. Let any unifiable formula be projective and there be an algorithm for constructing a projective unifier for any unifiable formula. Then the admissibility problem for the logic L is decidable.

The proof follows immediately from the definitions. This simple (and almost obvious theorem) allows us to resolve the admissibility problem in logics possessing the projective property, for which application of the earlier existing technique will not be very effective. Of course, not all interesting logics have the property mentioned. For example, for logic S4, Ghilardi used the property of finite projective approximation; Rybakov [17] applied the property of saturation by co-covers. But if it so happens that logics have all these properties then a chance to find a compact proof that solves a whole class of such problems looks very attractive and interesting.

In this paper we (rather unusually) do not first prove the decidability of a logic and only then embark on the proof of admissibility for that logic. Instead, we directly turn to the admissibility problem by using the above-mentioned technique of projective formulas invented by Ghilardi [18,19,20] and our technique for solving the satisfiability problem in multi-agent logics.

3. LOGICS WITH DYNAMIC RELATIONS OF TEMPORAL ACCESSIBILITY

In this section we present our main result on the unification and admissibility problems obtained for unusual new temporal logics with dynamic temporal accessibility. We extend temporal models assuming that any agent in any temporal state generates its own time relation and its own intervals—in any time state and for any agent—not depending on other states. Recall that a linear temporal nontransitive frame is the tuple

$$\mathcal{F}:=\langle S,\le ,\left\{{R}_{x}\left|x\in S\right.\right\}\rangle ,$$

where ≤ is a linear well ordering on S, and for all x ∈ S, R_x is the standard linear order on the interval [x, a_x] for some a_x ≥ x (a_x ∈ S) which is induced by the initial linear order ≤ on S (it is also possible that R_x is a linear order on the whole [x,∞)).

As an illustration, recall that xR_xa_x, y ∈ (x, a_x), and possibly not(yR_ya_x). Therefore y is a state situated earlier than x, but y remembers even less than x. Moreover, it is easy to see that all temporal accessibility relations together may form a nontransitive temporal accessibility relation.

Thus any state x ∈ S generates its own time relation R_x. Therefore time starts to be a dynamic relation which may by modified being transferred from one time state to another. At the same time, the global temporal relation R_x,0—temporal accessibility of the agent 0—remains to be the complete relation ≤ on S in all frames.

A model ℳ at any frame ℱ is defined by introducing a valuation V on ℱ for some set of propositional letters p, V (p) ⊆ N. Then we may introduce sets of forgotten times X_j for agents j, as we did earlier in this paper. Next the valuation V can be extended to all formulas, as shown above, for computing truth values of formulas φU_jψ (when j ≠ 0) at any state x using the relation R_x instead of ≤ as has been common in linear logic. At the beginning of this paper, we defined a temporal multi-agent logic ${\mathcal{L}}_{\mathcal{D}}^{\mathcal{A}}$ in a standard manner—as the set of all formulas which are true in all states of all models w.r.t. all possible valuations. Now we turn to prove our main result.

THEOREM 11. There is an algorithm which verifies unifiability of formulas in the logic ${\mathcal{L}}_{\mathcal{D}}^{\mathcal{A}}$. Any formula unifiable in ${\mathcal{L}}_{\mathcal{D}}^{\mathcal{A}}$ is projective and there is an algorithm constructing its projective unifier.

Proof. If a formula φ is unifiable in ${\mathcal{L}}_{\mathcal{D}}^{\mathcal{A}}$, and σ (where σ(x_i) := g_i), is some substitution unifying it, then by replacing all letters appearing in all formulas g_i of this substitution by ⊤ again we obtain a unifying substitution σ₁(x_i) := f_i. Then any formula f_i of the new substitution is equivalent to either formula ⊤ or formula ￢⊤. In particular, a formula φ has a simple unifier, a substitution of variables into a set of some formulas consisting of formulas ⊤ and ￢⊤ in some order. The last property is easy to verify. It is sufficient to check the truth of a formula φ on a one-element model F(1) with reflexive ≤. So, assume that φ is a unifiable formula and its unifiability can be proved and verified as shown above. Suppose that the verification is done and the substitution (T(x_i) := ⊥ or T(x_i) := ⊤) satisfying φ at F(1) is chosen.

Let Sub(□φ) be the set of all subformulas of the formula □φ. For any subsets X, Y ⊆ Sub(□φ), we define the relation X ≠_U Y as follows:

$$\begin{array}{c}X{\ne }_{U}Y\iff \left[\exists \left(\psi {U}_{j}\xi \right)\left[\left(\psi {U}_{j}\xi \in X\right)\&\psi {U}_{j}\xi \notin Y\right]\right]\\ \vee \left[\exists \left(\psi {U}_{j}\xi \right)\left[\left(\psi {U}_{j}\xi \notin X\right)\&\psi {U}_{j}\xi \notin Y\right]\right].\end{array}$$

Now for any letter x_i occurring in φ, we define a substitution σ. Let X ⊆ Sub(□φ) and

$${Sub}_{R}\left(\square \mathrm{\varphi },\mathrm{X}\right):=\left\{{p}_{i}\left|{p}_{i}\right.\in Prop\right\}\cup \left\{\psi {U}_{j}\xi \left|\psi {U}_{j}\xi \in X\right.\right\},$$

where Prop is the set of all letters from Sub(□φ), and

$$\begin{array}{c}Ds{\left(X\right)}^{+},:=\square \mathrm{\varphi }\wedge \underset{{p}_{i}\in {Sub}_{R}\left(\square \mathrm{\varphi },\mathrm{X}\right)}{\bigwedge }{p}_{i}\wedge \underset{{p}_{i}\in Prop\backslash X}{\bigwedge }\neg {p}_{i}\\ \wedge \underset{j\in \left\{\mathrm{0,1},\cdots ,k\right\},\psi {U}_{j}\xi \in {Sub}_{R}\left(\square \mathrm{\varphi },\mathrm{X}\right)}{\bigwedge }\psi {U}_{j}\xi \\ \wedge \underset{j\in \mathrm{0,1},\cdots ,k,\psi {U}_{j}\xi \in Sub\left(\mathrm{\varphi },\mathrm{X}\right),\psi {U}_{j}\xi \notin X}{\bigwedge }\neg \left(\psi {U}_{j}\xi \right).\end{array}$$

Let Char(X) := {p_i | p_i ∈ X ∩ Prop}, and for any letter x_i, T(X, x_i) := ⊤ if x_i ∈ Char (X), and T(X, x_i) := ⊥ otherwise.

A substitution σ is defined as follows:

$$\begin{array}{c}\sigma \left({x}_{i}\right):=\left(\square \mathrm{\varphi }\left({x}_{i},\dots ,{x}_{n}\right)\wedge {x}_{i}\right)\vee \left(\neg \right.\square \mathrm{\varphi }\wedge \diamondsuit \square \mathrm{\varphi }\\ \begin{array}{c}\wedge \underset{X \subseteq {Sub}_{R}\left(\square \mathrm{\varphi },\mathrm{X}\right)}{\bigvee }\square \left.\left[\neg \square \mathrm{\varphi }\wedge \diamondsuit \square \mathrm{\varphi }\to \neg \square \mathrm{\varphi }{U}_{0}Ds{\left(X\right)}^{+}\wedge T\left(X,{x}_{i}\right)\right]\right)\\ \vee \left(\neg \diamondsuit \square \mathrm{\varphi }\wedge T\left({x}_{i}\right)\right).\end{array}\end{array}$$

LEMMA 12. The substitution σ is projective for φ.

The proof follows easily from the fact that the formula (□φ (x₁, . . . , x_n) ∧ x_i) is the first disjunct of the formula defining the substitution σ(x_i) above.

Now we prove that the substitution σ is a unifier for φ. Take any infinite ordinary model M_T for the logic ${\mathcal{L}}_{\mathcal{D}}^{\mathcal{A}}$ with root w_t and valuation V₁ of all letters from φ. If w_t ∥–_V1□φ, then by the definition of σ we obtain w_t ∥–V1 σ(φ).

Assume that w_t ∥–_V1￢□φ. Then w_t ∥–_V1 σ(φ) (cf. definition of σ and F(1), definition of V on F(1) and what is T(x_i) above).

Suppose now that w_t ∥–_V1￢□φ but there is a ∈ M_T, where a∥–_V1□φ, and a is minimal with this property.

Consider X as the set of all subformulas of the formula □φ of which each is true w.r.t. V₁ at a and look over the definition of the set Sub_R(□φ, Y ) above. We see that

$$Ds{\left(X\right)}^{+}\wedge \underset{Y\ne UX}{\bigwedge }\neg Ds{\left(Y\right)}^{+}$$

is true w.r.t. V₁ at a. Besides, the formula ￢□φ ∧ ◇□φ ∧ ￢□φ U₀Ds(X)⁺ is true at any own predecessor b of the state a.

Notice that for any other Ds(Y )⁺, this is not the case. Therefore a valuation of the formula σ(x_i) w.r.t. V₁ for each i in model M_T at any own predecessor b of the state a (and in particular at w_t in the model M_T chosen above) coincides with the valuation of the letter x_i at the state a in the model M_T .

LEMMA 13. For any formula ψ ∈ Sub(□φ) (in particular for the ones with letters from the domain of the substitution σ) and for any own predecessor b of the state a, (M_T , a) ∥–_V1 ψ ⇔ (M_T , b) ∥–_V1 σ(ψ).

Proof. First, note that for any own predecessor b of the state a and any letter x_i,

$$\left({M}_{T},\alpha \right){\parallel }_{{-V}_{1}}{x}_{i}\iff \left({M}_{T},b\right){\parallel }_{{-V}_{1}}\sigma \left({x}_{i}\right)$$

by the definition of σ. Now we use induction on the length of the formula. Let us check that

$$\left({M}_{T},\alpha \right){\parallel }_{{-V}_{1}}{\psi }_{1}{U}_{j}{\psi }_{2}\iff \left({M}_{T},b\right){\parallel }_{{-V}_{1}}\sigma \left({\psi }_{1}{U}_{j}{\psi }_{2}\right).$$

(A) Assume first that (M_T , a) ∥–_V1 ψ₁U_jψ₂ and ψ₁, ψ₂ ∈ Sub(□φ). Suppose

$$\left({M}_{T},\alpha \right){\parallel }_{{-V}_{1}}{\psi }_{2}.$$

By inductive hypothesis, for all c < a we obtain (M_T , c) ∥–_V1 σ(ψ₂); in particular, (M_T , b) ∥–_V1 σ(ψ₁U_jψ₂).

(B) Now suppose that (M_T , a) ∥–_V1 ψ₁, and for some c we have

$$a<c,\&\left(a{R}_{a}c\right),\&c\notin {X}_{j},\& \left({M}_{T},c\right){\parallel }_{{-V}_{1}}{\psi }_{2}$$

and

$$\forall d\left(a<d<c \&\left(a{R}_{a}d\right)\&\left(d\notin {X}_{j}\right)\Rightarrow \left({M}_{T},d\right){\parallel }_{{-V}_{1}}{\psi }_{1}\right).$$

By using the inductive hypothesis, we then obtain (M_T , b) ∥–_V1 σ(ψ₁) for all b ≤ a. The valuation V1 of all letters of all formulas σ(x_i) do coincide at all states higher than a. Therefore, we conclude that for all c ≤ a,

$$\left({M}_{T},c\right){\parallel }_{{-V}_{1}}\sigma \left({\psi }_{1}{U}_{j}{\psi }_{2}\right).$$

Consider the opposite assumption that

$$\left({M}_{T},b\right){\parallel }_{{-V}_{1}}\sigma \left({\psi }_{1}{U}_{j}{\psi }_{2}\right), {\psi }_{1}{U}_{j}{\psi }_{2}\in Sub\left(\square \mathrm{\varphi }\right).$$

(C) If (M_T , b) ∥–_V1 σ (ψ₁U_jψ₂) and (M_T , b) ∥–_V1 σ(ψ₂), then it follows by the inductive hypothesis that (M_T , a) ∥–_V1 ψ₂ and (M_T , a) ∥_–V1 ψ₁U_jψ₂.

(D) Assume now that (M_T , b) ∦–_V1 σ(ψ₂). By inductive assumption, we then obtain (M_T , a) ∦–_V1 ψ₂ for all s, and if s ≤ a then (M_T , s) ∦–_V1 σ(ψ₂).

Since (M_T , b) ∥_–V1 σ(ψ₁U_jψ₂), there is c such that

$$b<c \& a<c \& \left(b{R}_{b}c\right) \& \left({M}_{T},c\right) \& \left({M}_{T},c\right){\parallel }_{{-V}_{1}}\sigma \left({\psi }_{2}\right)$$

and

$$\forall d\left(\alpha \le d<c \&d \notin {X}_{j}\right) \& \left(b{R}_{b}d\right)\left(\left({M}_{T},d\right){\parallel }_{{-V}_{1}}\sigma \left({\psi }_{1}\right)\right).$$

Then (M_T , c) ∥_–V1 ψ₂ and

$$\forall d\left(\alpha \le d<c \&d \notin {X}_{j}d\notin {X}_{j}\& \left(b{R}_{b}d\right)\right) \left(\left({M}_{T},d\right){\parallel }_{{-V}_{1}}\sigma {\psi }_{1}\right..$$

Besides, in view of (M_T , b) ∥_–V1 σ(ψ₁U_jψ₂) we conclude that (M_T , b) ∥_–V1 σ(ψ₁), and using inductive hypothesis yields (M_T , a) ∥_–V1 ψ₁ and

$$\left({M}_{T},d\right){\parallel }_{{-V}_{1}}\psi 1Uj\psi 2.$$

Thus Lemma 13 is proved and the substitution σ is projective. This completes the proof of Theorem 11.

Theorem 11 provides an algorithm for constructing a most general unifier for formulas unifiable in ℒ𝒯ℒ_U. The construction of this projective unifier is given in the proof in detail: we write out formulas σ(x_i) which yield the most general unifier. As a consequence, we obtain the solution of the admissibility problem in logic ${\mathcal{L}}_{\mathcal{D}}^{\mathcal{A}}$.

THEOREM 14. The problem of recognizing admissible rules in ${\mathcal{L}}_{\mathcal{D}}^{\mathcal{A}}$ is decidable, and correspondingly the logic ${\mathcal{L}}_{\mathcal{D}}^{\mathcal{A}}$ is itself decidable.

These results extend the ones in [21, 23] about projectivity of unifiable formulas in modal logic S4.3 and linear temporal logic LTL with deleted operation NEXT, respectively, on multi-agent temporal logics.

As proved above, the admissibility problem in the logic ${\mathcal{L}}_{\mathcal{D}}^{\mathcal{A}}$ is decidable. This result extends the theorems from [7, 8, 25] about admissibility problem in the linear temporal logic LTL to linear temporal logics with multi-agent operations with lost time and dynamic definition of operations of temporal accessibility.

4. A SHORT NOTE ON WEAKLY PROJECTIVE FORMULAS

Here we briefly describe our idea concerning weakly projective formulas (which has also been outlined in our recent paper submitted for publication). Consider temporal logics with logical operations responsible for future and for past and consider the standard definition of projective formulas. Any formula φ is said to be projective if it has a unifier σ such that

$$\square \mathrm{\varphi }\to \left[{x}_{i}\equiv \sigma \left({x}_{i}\right)\right]\in L$$

for any letter x_i from □φ. By analyzing definitions and known applications of projectivity it is easy to see that in essence only one property of □φ (of course besides the definition of projectivity itself) is used—namely, that □φ ∈ L if and only if φ ∈ L.

So, we suggest that in the definition of projectivity the formula □_x is exchanged by another formula F(x) which would have the same properties:

$$F\left(\varphi \right)\in L\iff \varphi \in L.$$

Definition 15. A formula φ is weakly projective if there are a formula F(x) and a substitution σ (which is called a weakly projective unifier) for φ such that σ is a unifier for φ and F(φ) → [x_i ≡ σ(x_i)] ∈ L for any letter x_i from φ.

Given the definition above, we may work with weak projectivity in the same way as with projectivity, and all the proofs obtained will do. The advantage of this approach is that the formula F(x) may vary depending on the form of φ, which can open up some extra opportunities.

We point out an example based on universal modality. Recall that a logical operation □_U is a universal modality if, for any model M of a given logic with the base set |M| and any valuation V for any state a ∈ |M|, the following holds:

$$\left(M,a\right){\parallel }_{{-V}_{1}}{\square }_{U}x\iff \forall b \in \left|M\right|\left(\left(M,b\right){\parallel }_{{-V}_{1}}x\right).$$

We may extend the domain of our work using temporal logical operations for future and past (UNTIL and SINCE) and also models based on the set of all natural numbers as in this paper, or on the set of all integer numbers. Then we define modalities □⁺ and □⁻—necessary for future and necessary for past respectively—and the superposition □⁺□⁻ will be a universal modality in such logics. In this case, assuming that F(x) := □⁺□ ⁻x, the substitution

$${x}_{i} \Rightarrow \left[{\square }^{+}{\square }^{-}\varphi \wedge {x}_{i}\right]\vee \left[\neg {\square }^{+}{\square }^{-}\varphi \wedge {\alpha }_{i}\right],$$

where x_i ⇒ a_i, a_i ∈ {⊤, ⊥}, makes φ true in a one-element model and it is a weakly projective unifier.

Accordingly, we have then weak projectivity for any unifiable formula and problems of admissibility, decidability, and satisfiability, all decidable in such logics. If we take only modal operations □⁺ and □⁻ as additional not Boolean operations in the definition of logic, then all what has been described above remains valid, but this case too is virtually trivial.

Now we look at yet another possible and more substantial application. Consider arbitrary logics which are obtained from our basic logic by imposing various restrictions on the competence of the agents—for example, the case when in models we always have X_i ⊆ X_i+1, i.e. the ith agent is more competent than the (i + 1)th agent; in other words, □_ix_j → □_i+1x_j for any letter x_j. Moreover, we may consider all Boolean formulas F(x₁, . . . , x_n), and a logic L(F) for each formula will be the logic generated by all models where

$$F\left({X}_{1},\cdots ,{X}_{n}\right)=\mathrm{\top }.$$

THEOREM 16. Any formula unifiable in L(F) is projective and there is an algorithm for constructing its projective unifier.

The proof repeats verbatim the proof of Theorem 11: we need only note that it does not touch the condition F(X₁, . . . ,X_n) = ⊤ in models. Using Theorem 16, we derive the main result for such logics.

THEOREM 17. The admissibility problem for inference rules in L(F) is decidable, and correspondingly the logic L(F) is itself decidable for each L(F).

Thus, we obtain results for all such logics defined by different choices of formulas F(x₁, . . . , x_n).