Two variable fragment of Term Modal Logic

TL;DR

This paper proves that a specific two-variable fragment of Term Modal Logic is decidable, contrasting with the undecidability of similar fragments in first-order modal logic.

Contribution

It establishes the decidability of the two-variable fragment of Term Modal Logic, a notable exception in the landscape of undecidable modal logics.

Findings

Two-variable fragment of TML is decidable.

Contrasts with undecidability of two-variable first-order modal logic.

Provides a new decidability result for complex modal logics.

Abstract

Term modal logics (TML) are modal logics with unboundedly many modalities, with quantification over modal indices, so that we can have formulas of the form $\exists y. \forall x. (\Box_x P(x,y) \supset\Diamond_y P(y,x))$. Like First order modal logic, TML is also "notoriously" undecidable, in the sense that even very simple fragments are undecidable. In this paper, we show the decidability of one interesting fragment, that of two variable TML. This is in contrast to two-variable First order modal logic, which is undecidable.

Figures

Equations

$$\phi ::=P(\overline{x})\mid \neg \phi \mid (\phi \wedge \phi )\mid (\phi \vee \phi )\mid \exists x\text{leavevmode}\phi \mid \forall x\text{leavevmode}\phi \mid {\square }_x\phi \mid {◊}_x\phi$$

$$\begin{array}[]{|lcl|}\hline\cr M,w,\sigma\vDash P(x_{1},\ldots,x_{n})&\Leftrightarrow&(\sigma(x_{1}),\ldots,\sigma(x_{n}))\in\rho(w,P)\\ M,w,\sigma\vDash\neg\varphi&\Leftrightarrow&M,w,\sigma\nvDash\varphi\\ M,w,\sigma\vDash(\varphi\land\psi)&\Leftrightarrow&M,w,\sigma\vDash\varphi\text{ and }M,w,\sigma\vDash\psi\\ M,w,\sigma\vDash\exists x\leavevmode\nobreak\ \varphi&\Leftrightarrow&\text{there is some $d\in\delta(w)$ such that M, w, $\sigma_{[x\mapsto d]}\vDash\varphi$ }\\ M,w,\sigma\vDash\Box_{x}\leavevmode\nobreak\ \varphi&\Leftrightarrow&M,v,\sigma\vDash\varphi\text{ for all $v$ s.t.\ $(w,\sigma(x),v)\in R$}\\ \hline\cr\end{array}$$

$$\underset{i\le a}{\bigwedge }{s}_i\wedge \underset{z\in \{x,y\}}{\bigwedge }({\square }_z\alpha \wedge \underset{j\le m_z}{\bigwedge }{◊}_z{\beta }_j)\wedge \underset{z\in \{x,y\}}{\bigwedge }(\forall z\text{leavevmode}\gamma \wedge \underset{k\le n_z}{\bigwedge }\exists z\text{leavevmode}{\delta }_k)\wedge \forall x\forall y\text{leavevmode}\phi \wedge \underset{l\le b}{\bigwedge }\forall x\exists y\text{leavevmode}{\psi }_l$$

$$\underset{i\le a}{\bigwedge }{s}_i\wedge \underset{z\in \{x,y\}}{\bigwedge }({\square }_z{\alpha }^z\wedge \underset{j\le m_z}{\bigwedge }{◊}_z{\beta }_j^z)\wedge \underset{z_1\in \{x,y\}}{\bigwedge }(\forall z_2\text{leavevmode}{\gamma }^{z_1}\wedge \underset{k\le n_z}{\bigwedge }\exists z_2\text{leavevmode}{\delta }_k^{z_1})\wedge \forall x\forall y\text{leavevmode}\phi \wedge \underset{l\le b}{\bigwedge }\forall x\exists y\text{leavevmode}{\psi }_l$$

$$\underset{i\le a}{\bigwedge }{s}_i\wedge \underset{z\in \{x,y\}}{\bigwedge }({\square }_z{\alpha }^z\wedge \underset{j\le m_z}{\bigwedge }{◊}_z{\beta }_j^z)\wedge \underset{z\in \{x,y\}}{\bigwedge }(\forall z\text{leavevmode}{\gamma }^z\wedge \underset{k\le n_z}{\bigwedge }\exists z{\delta }_k^z)\wedge \forall x\forall y\phi \wedge \underset{l\le b}{\bigwedge }\forall x\exists y{\psi }_l$$

Full text

Two variable fragment of Term Modal Logic

Anantha Padmanabha

  

R Ramanujam

1 Introduction

Propositional multi-modal logics ($\mathsf{ML}$) are extensively used in many areas of computer science and artifical intelligence ([2, 9]). $\mathsf{ML}$ is built upon propositional logic by adding modal operators $\Box_{i}$ and $\Diamond_{i}$ for every index $i$ in a fixed finite set $Ag$ which is often interpreted as a set of agents (or reasoners). Typically, the satisfiability problem is decidable for most instances of $\mathsf{ML}$.

A natural question arises when we wish the set of modalities to be unbounded. This is motivated by a range of applications such as client-server systems, dynamic networks of processes, games with unboundedly many players, etc. In such systems, the number of agents is not fixed a priori. For some cases, the agent set can vary not only across models, but also from state to state (ex. when new clients enter the system or old clients exit the system).

Term Modal logic ($\mathsf{TML}$) introduced by Fitting, Voronkov and Thalmann [6] addresses this requirement. $\mathsf{TML}$ is built upon first order logic, but the variables now range over modalities: so we can index the modality by terms $(\Box_{x}\alpha)$ and these terms can be quantified over. State assertions describe properties of these ‘agents’. Thus we can write formulas of the form: $\forall x(\Box_{x}P(x)\supset\exists y\leavevmode\nobreak\ \Box_{y}\Diamond_{x}R(x,y))$. In [15] we have advocated $\mathsf{PTML}$, the propositional fragment of $\mathsf{TML}$, as a suitable logical language for reasoning about systems with unboundedly many agents. $\mathsf{TML}$ has been studied in dynamic epistemic contexts in [11] and in modelling situations where the identity of agents is not common knowledge among the agents [22].

The following examples illustrate the flavour of properties that can be expressed in $\mathsf{TML}$.

• •

For every agent $x$ there is some agent $y$ such that $P(x,y)$ holds at all $x$-successors or there is some $y$-successor where $\neg P(x,y)$ holds.

\forall x\exists y\leavevmode\nobreak\ \big{(}\Box_{x}P(x,y)\lor\Diamond_{y}(\neg P(x,y))\big{)}

• •

Every agent of type $A$ has a successor where some agent of type $B$ exists.

\forall x\big{(}A(x)\supset\Diamond_{x}\exists y\leavevmode\nobreak\ B(y)\big{)}.

• •

There is some agent $x$ such that for all agents $y$ if there are no $y$ successors then in all successors of $x$, there is a $y$ successor.

\exists x\forall y\leavevmode\nobreak\ \big{(}\Box_{y}\bot\supset\Box_{x}\Diamond_{y}\top).

Since $\mathsf{TML}$ contains first order logic, its satisfiability is clearly undecidable. We are then led to ask: can we build term modal logics over decidable fragments of first order logic? Natural candidates are the monadic fragment, the two-variable fragment and the guarded fragment [13, 1].

$\mathsf{TML}$ itself can be seen as a fragment of first order modal logic ($\mathsf{FOML}$) [5] which is built upon first order logic by adding modal operators. There is a natural translation of $\mathsf{TML}$ into $\mathsf{FOML}$ by inductively translating $\Box_{x}\alpha$ into $\Box(P(x)\supset\alpha)$ and $\Diamond_{x}\alpha$ into $\Diamond(P(x)\land\alpha)$ to get an equi-satisfiable formula, where $P$ is a new unary predicate. Sadly, this does not help much, since $\mathsf{FOML}$ is notorious for undecidability. The modal extension of many simple decidable fragments of first order logic become undecidable. For instance, the monadic fragment[12] or the two variable fragment [10] of $\mathsf{FOML}$ are undecidable. In fact $\mathsf{FOML}$ with two variables and a single unary predicate is already undecidable [18]. Analogously, in [15] we show that the satisfiability problem for $\mathsf{TML}$ is undecidable even when the atoms are restricted to propositions. In the presence of equality (even without propositions), this result can be further strengthened to show ‘Trakhtenbrot’ like theorem of mutual recursive inseparability.

On the other hand, as we show in [15], the monodic fragment of $\mathsf{PTML}$ (the propositional fragment) is decidable (a formula $\varphi$ is monodic if each of its modal subformulas of the form $\Box_{x}\psi$ or $\Diamond_{x}\psi$ has a restriction that the free variables of $\psi$ is contained in $\{x\}$). Further, via the $\mathsf{FOML}$ translation above, we can show that the monodic restriction of $\mathsf{TML}$ based on the guarded fragment of first order logic and monadic first order logic are decidable [23].

In a different direction, Wang ([21]) considered a fragment of $\mathsf{FOML}$ in which modalities and quantifiers are bound to each other. In particular he considered the fragment with $\exists\Box$ and showed it to be decidable in PSPACE. In [17] it is proved that this technique of bundling quantifiers and modalities gives us interesting decidable fragments of $\mathsf{FOML}$, and as a corollary, the bundled fragment of $\mathsf{TML}$ is decidable where quantifiers and modalities always occur in bundled form: $\forall x\Box_{x}\alpha,\exists x\Box_{x}\alpha$ and their duals. However, more general bundled fragments of $\mathsf{TML}$ (such as those based on the guarded fragment of first order logic) have been shown to be decidable by Orlandelli and Corsi ([14]), and by Shtakser ([19]). From all these results, it is clear that the one variable fragment of $\mathsf{TML}$ is decidable, and that the three variable fragment of $\mathsf{PTML}$ is undecidable.

In this paper, we show that the two variable fragment of $\mathsf{TML}$ ($\mathsf{TML}^{2}$) is decidable. This is in contrast with $\mathsf{FOML}$, for which the two variable fragment is undecidable [10]. Quoting Wolter and Zakharyaschev from [23], where they discuss the root of undecidability of $\mathsf{FOML}$ fragments:

All undecidability proofs of modal predicate logics exploit formulas of the form $\Box\leavevmode\nobreak\ \psi(x,y)$ in which the necessity operator applies to subformulas of more than one free variable; in fact, such formulas play an essential role in the reduction of undecidable problems to those fragments$\ldots$

Note that this is not expressible in $\mathsf{TML}^{2}$ where there is no ‘free’ modality; every modality is bound an index ($x$ or $y$). With a third variable $z$, we could indeed encode $\Box P(x,y)$ as $\forall z\Box_{z}P(x,y)$, but we do not have it. The decidability of the two variable fragment of $\mathsf{TML}$, without constants or equality, hinges crucially on this lack of expressiveness. Thus, $\mathsf{TML}^{2}$ provides a decidable fragment of $\mathsf{FOML}^{2}$. From $\mathsf{FO}^{2}$ view point, Gradel and Otto[8] show that most of the natural extensions of $\mathsf{FO}^{2}$ (like transitive closure, lfp) are undecidable except for the counting quantifiers. In this sense, $2$-variable $\mathsf{TML}$ can be seen as another rare extension of $\mathsf{FO}^{2}$ that still remains decidable. Note that in this paper we consider the two variable fragment of $\mathsf{TML}$ without the bundling or guarded or monodic restriction. Also, there is no natural translation of two variable $\mathsf{TML}$ to any known decidable fragment of $\mathsf{FO}$ such as the two variable fragment of $\mathsf{FO}$ with $2$ equivalence relations etc (cf [20]).

Thus, the contribution of this paper is technical, mainly in the identification of a decidable fragment of $\mathsf{TML}$. As is standard with two variable logics, we first introduce a normal form which is a combination of Fine’s normal form for modal logics ([4]) and the Scott normal form ([7]) for $\mathsf{FO}^{2}$. We then prove a bounded agent property using an argument that can be construed as modal depth induction over the ‘classical’ bounded model construction for $\mathsf{FO}^{2}$.

2 $\mathsf{TML}$ syntax and semantics

We consider relational vocabulary with no constants or function symbols, and without equality.

Definition 2.1** ($\mathsf{TML}$ syntax).**

Given a countable set of variables Var and a countable set of predicate symbols $\mathcal{P}$, the syntax of $\mathsf{TML}$ is defined as follows:

[TABLE]

where $x\in\textsf{Var}$, $\overline{x}$ is a vector of length $n$ over $Var$ and $P\in\mathcal{P}$ of arity $n$.

The free and bound occurrences of variables are defined as in $\mathsf{FO}$ with $\textsf{Fv}(\Box_{x}\varphi)=\textsf{Fv}(\varphi)\cup\{x\}$. We write $\varphi(\overline{x})$ if all the free variables in $\varphi$ are included in $\overline{x}$. Given a $\mathsf{TML}$ formula $\varphi$ and $x,y\in\textsf{Var}$, if $y\not\in\textsf{Fv}(\varphi)$ then we write $\varphi[y/x]$ for the formula obtained by replacing every occurrence of $x$ by $y$ in $\varphi$. A formula $\varphi$ is called a sentence if $\textsf{Fv}(\varphi)=\emptyset$. The notion of modal depth of a formula $\varphi$ (denoted by $\textsf{md}(\varphi)$) is also standard, which is simply the maximum number of nested modalities occurring in $\varphi$. The length of a formula $\varphi$ is denoted by $|\varphi|$ and is simply the number of symbols occurring in $\varphi$.

In the semantics, the number of accessibility relations is not fixed, but specified along with the structure. Thus the Kripke frame for $\mathsf{TML}$ is given by $(W,D,R)$ where $W$ is a set of worlds, $D$ is the potential set of agents and $R\subseteq(W\times D\times W)$. The agent dynamics is captured by a function ($\delta:W\rightarrow 2^{D}$ below) that specifies, at any world $w$, the set of agents live (or meaningful) at $w$. The condition that whenever $(u,d,v)\in R$, we have that $d\in\delta(u)$ ensures only an agent alive at $u$ can consider $v$ accessible.

A monotonicity condition is imposed on the accessibility relation as well: whenever $(u,d,v)\in R$, we have that $\delta(u)\subseteq\delta(v)$. This is required to handle interpretations of free variables (cf [3, 6, 5]). Hence the models are called ‘increasing agent’ models.

Definition 2.2** ($\mathsf{TML}$ structure).**

An increasing agent model for $\mathsf{TML}$ is defined as the tuple $M=(W,D,\delta,R,\rho)$ where $W$ is a non-empty countable set of worlds, $D$ is a non-empty countable set of agents, $R\subseteq(W\times D\times W)$ and $\delta:W\to 2^{D}$. The map $\delta$ assigns to each $w\in W$ a non-empty local domain such that whenever $(w,d,v)\in R$ we have $d\in\delta(w)\subseteq\delta(v)$ and $\rho:(W\times\mathcal{P})\to\bigcup_{n\in\omega}2^{D^{n}}$ is the valuation function where for all $P\in\mathcal{P}$ of arity $n$ we have $\rho(w,P)\subseteq[\delta(w)]^{n}$.

For a given model $M$, we use $W^{M},D^{M},\delta^{M},R^{M},\rho^{M}$ to refer to the corresponding components. We drop the superscript when $M$ is clear from the context. We often write $D_{w}$ for $\delta(w)$. A constant agent model is one where $D_{w}=D$ for all $w\in W$. To interpret free variables, we need a variable assignment $\sigma:\textsf{Var}\to D$. Call $\sigma$ relevant at $w\in W$ if $\sigma(x)\in\delta(w)$ for all $x\in\textsf{Var}$. The increasing agent condition ensures that if $\sigma$ is relevant at $w$ and $(w,d,v)\in R$ then $\sigma$ is relevant at $v$ as well. In a constant agent model, every assignment $\sigma$ is relevant at all the worlds.

Definition 2.3** ($\mathsf{TML}$ semantics).**

Given a $\mathsf{TML}$ structure $M=(W,D,\delta,R,\rho)$ and a $\mathsf{TML}$ formula $\varphi$, for all $w\in W$ and $\sigma$ relevant at $w$, define $M,w,\sigma\vDash\varphi$ inductively as follows:

[TABLE]

where $\sigma_{[x\mapsto d]}$ denotes another assignment that is the same as $\sigma$ except for mapping $x$ to $d$.

The semantics for $\varphi\lor\psi,\forall x\leavevmode\nobreak\ \varphi$ and $\Diamond_{x}\leavevmode\nobreak\ \varphi$ are defined analogously. Note that $M,w,\sigma\vDash\varphi$ is inductively defined only when $\sigma$ is relevant at $w$. We often abuse notation and say ‘for all $w$ and for all interpretations $\sigma$’, when we mean ‘for all $w$ and for all interpretations $\sigma$ relevant at $w$’ (and we will ensure that relevant $\sigma$ are used in proofs). In general, when considering the truth of $\varphi$ in a model, it suffices to consider $\sigma:\textsf{Fv}(\varphi)\mapsto D$, assignment restricted to the variables occurring free in $\varphi$. When $\textsf{Fv}(\varphi)\subseteq\{x_{1},\ldots,x_{n}\}$ and $\overline{d}\in[D_{w}]^{n}$ is a vector of length $n$ over $D_{w}$, we write $M,w\vDash\varphi[\overline{d}]$ to denote $M,w,\sigma\vDash\varphi(\overline{x})$ where for all $i\leq n,\ \sigma(x_{i})=d_{i}$. When $\varphi$ is a sentence, we simply write $M,w\models\varphi$. A formula $\varphi$ is valid, if $\varphi$ is true in all models $M$ at all $w$ for all interpretations $\sigma$ (relevant at $w$). A formula $\varphi$ is satisfiable if $\neg\varphi$ is not valid.

Now we take up the satisfiability problem which is the central theme of this paper. First we observe that the satisfiability problem is equally hard for constant and increasing agent models for $\mathsf{TML}$.

First we prove that the satisfiability problem over constant agent structures and increasing agent structures is equally hard for most fragments. To see why this is true, if a formula $\varphi\in\mathsf{TML}$ is satisfiable in some increasing agent model, then we can turn the model into constant agent model as follows. We introduce a new unary predicate $E$ and ensure that $E(d)$ is true at $w$ if $d$ is a member of $\delta(w)$ in the given increasing agent model. But now, all quantifications have to be relativized with respect to the new predicate $E$. This translation is similar in approach to the one for $\mathsf{FOML}$[23]. The syntactic translation is defined as follows:

Definition 2.4**.**

Let $\varphi$ be any $\mathsf{TML}$ formula and let $E$ be a new unary predicate not occurring in $\varphi$. The translation is defined inductively as follows:

• •

$\textsf{Tr}_{1}(P(x_{1},\ldots,x_{n}))=P(x_{1},\ldots,x_{n})$**

• •

$\textsf{Tr}_{1}(\neg\varphi)=\neg\textsf{Tr}_{1}(\varphi)$* and $\textsf{Tr}_{1}(\varphi\land\psi)=\textsf{Tr}_{1}(\varphi)\land\textsf{Tr}_{1}(\psi)$*

• •

$\textsf{Tr}_{1}(\Box_{x}\varphi)=\Box_{x}(\textsf{Tr}_{1}(\varphi))$**

• •

$\textsf{Tr}_{1}(\exists x\leavevmode\nobreak\ \varphi)=\exists x\leavevmode\nobreak\ (E(x)\land\textsf{Tr}_{1}(\varphi))$**

With this translation, we also need to ensure that the predicate $E$ respects monotonicity. Hence we have \gamma_{\varphi}=\bigwedge\limits_{i+j\leq\textsf{md}(\varphi)}(\forall y\Box_{y})^{i}\big{(}\forall x\leavevmode\nobreak\ E(x)\supset(\forall y\Box_{y})^{j}E(x)\big{)}. Now, we can prove that $\varphi$ is satisfiable in an increasing model iff $\textsf{Tr}_{1}(\varphi)\land\gamma_{\varphi}$ is satisfiable in a constant agent model. Moreover, both the formulas are satisfiable over the same agent set $D$.

Lemma 2.5**.**

Let $\varphi$ be any $\mathsf{TML}$ formula. $\varphi$ is satisfiable in an increasing agent model with agent set $D$ iff $\gamma_{\varphi}\land\textsf{Tr}_{1}(\varphi)$ is satisfiable in a constant agent model with agent set $D$.

Proof 2.6**.**

$(\Rightarrow)$* Suppose $M^{I}=(W,D,\delta^{I},R,\rho^{I})$ is an increasing agent model with $r\in W$ such that $M^{I},r,\sigma\models\varphi$. Define the constant domain model $M^{C}=(W,D,\delta^{C},R,\rho^{C})$ where $\delta^{C}(w)=D$ for all $w\in W$ and $\rho^{C}$ is the same as $\rho^{I}$ for all predicates except $E$ and for all $w\in W$ and $d\in D$ we have $d\in\rho^{C}(w,E)$ iff $d\in\delta(w)$.*

Since $\delta^{I}$ is monotone, $M^{C},r,\sigma\models\gamma_{\varphi}$. Note that $M^{I},w\models P(\overline{d})$ iff $M^{C},w\models P(\overline{d})$ and we have $d\in\delta^{I}(w)$ iff $M^{C},w\models E(d)$. Thus, we can set up a routine induction and prove that for all subformulas $\psi$ of $\varphi$ and for all $w\in W$ and for all interpretation $\sigma^{\prime}$ relevant at $w$, we have $M^{I},w,\sigma^{\prime}\models\psi$ iff $M^{C},w,\sigma^{\prime}\models\textsf{Tr}_{1}(\psi)$. Hence, $M^{C},r,\sigma\models\textsf{Tr}_{1}(\varphi)$.

$(\Leftarrow)$* Suppose $M^{C}=(W,D,\delta^{C},R,\rho^{C})$ is a tree model of depth at most $\textsf{md}(\varphi)$ with $r\in W$ such that $M^{C},r,\sigma\models\gamma_{\varphi}\land\textsf{Tr}_{1}(\varphi)$. Define the increasing agent model $M^{I}=(W,D,\delta^{I},R,\rho)$ where $c\in\delta^{I}(w)$ iff $M,w\models E(c)$.*

Note that $\delta^{I}$ defined above is monotone since $M^{C},r\models\gamma_{\varphi}$. Again, we can set up a routine induction and prove that for all subformulas $\psi$ of $\varphi$ and for all $w\in W$ and for all interpretation $\sigma^{\prime}$ relevant at $w$ we have $M^{C},w,\sigma^{\prime}\models\textsf{Tr}_{1}(\psi)$ iff $M^{I},w,\sigma^{\prime}\models\psi$.

The propositional term modal logic $(\mathsf{PTML})$ is a fragment of $\mathsf{TML}$ where the atoms are restricted to propositions. Note that the variables still appear as index of modalities. For $\mathsf{PTML}$, the valuation function can be simply written as $\rho:W\mapsto 2^{\mathcal{P}}$ where $\mathcal{P}$ is the set of propositions. Now we prove that the satisfiability problem for $\mathsf{PTML}$ is as hard as that for $\mathsf{TML}$. The reduction is based on the translation of an arbitrary atomic predicate $P(x_{1},\ldots,x_{n})$ to $\Diamond_{x_{1}}\ldots\Diamond_{x_{n}}p$ where $p$ is a new proposition which represents the predicate $P$. However, this cannot be used always111for instance, this translation will not work for the formula $\exists x\leavevmode\nobreak\ P(x)\land\forall y\leavevmode\nobreak\ \Box_{y}\bot$. Thus, we use a new proposition $q$, to distinguish the ‘real worlds’ from the ones that are added because of the translation. But now, the modal formulas have to be relativized with respect to the proposition $q$. The formal translation is given as follows:

Definition 2.7**.**

Let $\varphi$ be any $\mathsf{TML}$ formula where $P_{1},\ldots,P_{m}$ are the predicates that occur in $\varphi$. Let $\{p_{1},\ldots,p_{m}\}\cup\{q\}$ be a new set of propositions not occurring in $\varphi$. The translation with respect to $q$ is defined inductively as follows:

• •

$\textsf{Tr}_{2}(P_{i}(x_{1},\ldots,x_{n});q)=\Diamond_{x_{1}}(\neg q\land\Diamond_{x_{2}}(\ldots\neg q\land\Diamond_{x_{n}}(\neg q\land p_{i})\ldots))$**

• •

$\textsf{Tr}_{2}(\neg\varphi;q)=\neg\textsf{Tr}_{2}(\varphi;q)$* and $\textsf{Tr}_{2}(\varphi\land\psi;q)=\textsf{Tr}_{2}(\varphi;q)\land\textsf{Tr}_{2}(\psi;q)$*

• •

$\textsf{Tr}_{2}(\Box_{x}\varphi;q)=\Box_{x}(q\supset\textsf{Tr}_{2}(\varphi;q))$**

• •

$\textsf{Tr}_{2}(\exists x\leavevmode\nobreak\ \varphi;q)=\exists x\leavevmode\nobreak\ \textsf{Tr}_{2}(\varphi;q)$**

Lemma 2.8**.**

For any $\mathsf{TML}$ formula $\varphi$, we have $\varphi$ is satisfiable in an increasing (constant) agent model with agent set $D$ iff $q\land\textsf{Tr}_{2}(\varphi;q)$ is satisfiable in an increasing (constant) agent model with agent set $D$.

Proof 2.9**.**

Let $P_{\varphi}$ be the set of all predicates occurring in $\varphi$ and $k$ be the maximum arity among the predicates in $P_{\varphi}$. For any model $M$ and $u\in W$ let $\overline{c}\in D_{u}^{*}$ denote a (possibly empty) string of finite length over $D_{u}$.

$(\Rightarrow)$* Suppose the $\mathsf{TML}$ formula $\varphi$ is satisfiable. Let $M^{T}=(W^{T},D,\delta^{T},R^{T},\rho^{T})$ be a $\mathsf{TML}$ model and $w\in W$ such that $M^{T},w,\sigma\models\varphi$. Define the $\mathsf{PTML}$ model $M^{P}=(W^{P},D,\delta^{P},R^{P},val^{P})$ where:*

$W^{P}=\{u_{\overline{c}}\mid u\in W^{T}$* and $\overline{c}\in D^{*}_{u}$ of length at most $k\}$.*

• -

For all $u_{\overline{c}}\in W^{P}$ we have $\delta^{P}(u_{\overline{c}})=\delta^{T}(u)$.

• -

$R^{P}=\{(u_{\epsilon},c,v_{\epsilon})\mid(u,c,v)\in R^{T}\}\cup\{(u_{\overline{c}},d,u_{\overline{c}d})\mid u_{\overline{c}},u_{\overline{c}d}\in W^{P}\}$**

• -

$\rho^{P}(u_{\epsilon})=\{s\mid s$* is a proposition in $P_{\varphi}$ and $M,u\models s\}\cup\{q\}$ and*

$\rho^{P}(u_{c_{1}\ldots c_{n}})=\{p_{i}\mid M,u\models P_{i}(c_{1},\ldots,c_{n})\}$.

Note that $M^{T},u,\sigma\models P_{i}(x_{1},\ldots,x_{n})$ iff $M^{P},u_{\epsilon},\sigma\models\Diamond_{x_{1}}(\neg q\land\Diamond_{x_{2}}(\ldots\neg q\land\Diamond_{x_{n}}(\neg q\land p_{i})\ldots))$ and for all $u\in W^{T}$ we have $M,u_{\epsilon}\models q$. Thus a standard inductive argument shows that for all subformulas $\psi$ of $\varphi$ and for all $u\in W^{T}$ and for all interpretation $\sigma^{\prime}$ we have $M^{T},u,\sigma^{\prime}\models\psi$ iff $M^{P},u_{\epsilon},\sigma^{\prime}\models r\land\textsf{Tr}_{2}(\psi)$.

Also note that if $M^{T}$ is an increasing (constant) agent model over $D$ then $M^{P}$ is also an increasing (constant) agent model over $D$.

$(\Leftarrow)$* Suppose $M^{P}=(W^{P},D,\delta^{P},R^{P},\rho^{P})$ such that $M,w\models r\land\textsf{Tr}_{2}(\varphi)$. Define $M^{T}=(W^{T},D,\delta^{T},R^{T},\rho^{T})$ where*

$W^{T}=\{u\in W^{P}\mid M^{P},u\models q\}$.

• -

For all $u\in W^{T}$ we have $\delta^{T}(u)=\delta^{P}(u)$.

• -

$R^{T}=R^{P}\cap(W^{T}\times W^{T})$.

• -

$\rho^{T}(u,P)=\{(c_{1},\ldots,c_{n})\mid M^{P},u\models\Diamond_{c_{1}}(\neg q\land(\ldots\Diamond_{c_{n}}(\neg q\land p)\}$* and*

$q\in\rho^{T}(u)$* iff $q\in\rho^{P}(u)$.*

Note that for all $u\in W^{P}$ we have $M^{P},u\models\Diamond_{c_{1}}(\neg q\land(\ldots\Diamond_{c_{n}}(\neg q\land p_{i})$ iff $M^{T},w\models P_{i}(c_{1},\ldots,c_{n})$. Also, since $M^{P},w\models q$ we have $w\in W^{T}$. Again, an inductive argument shows that for all subformulas $\psi$ of $\varphi$ and for all $u\in W^{T}$ and for all interpretation $\sigma^{\prime}$ relevant at $w$, we have $M^{P},u,\sigma^{\prime}\models\textsf{Tr}_{2}(\psi)$ iff $M^{T},u,\sigma^{\prime}\models\psi$. Thus we have $M^{T},w,\sigma\models\varphi$.

To complete the proof, again note that if $M^{P}$ is an increasing (constant) agent model over $D$ then $M^{T}$ is also an increasing(constant) agent model over $D$.

3 Two variable fragment

Note that all the examples discussed in the introduction section use only 2 variables. Thus, $\mathsf{TML}$ can express interesting properties even when restricted to two variables. We now consider the satisfiability problem of $\mathsf{TML}^{2}$. The translation in Def. 2.7 preserves the number of variables. Therefore it suffices to consider the satisfiability problem for the two variable fragment of $\mathsf{PTML}$.

Let $\mathsf{PTML}^{2}$ denote the two variable fragment of $\mathsf{PTML}$. We first consider a normal form for the logic. In [4], Fine introduces a normal form for propositional modal logics which is a disjunctive normal form ($\mathsf{DNF}$) with every clause of the form $(\bigwedge\limits_{i}(s_{i})\land\Box\alpha\land\bigwedge\limits_{j}\Diamond\beta_{j})$ where $s_{i}$ are literals and $\alpha,\beta_{j}$ are again in the normal form. For $\mathsf{FO}^{2}$, we have Scott normal form [7] where every $\mathsf{FO}^{2}$ sentence has an equi-satisfiable formula of the form $\forall x\forall y\leavevmode\nobreak\ \varphi\land\bigwedge\limits_{i}\forall x\exists y\leavevmode\nobreak\ \psi_{i}$ where $\varphi$ and $\psi_{i}$ are all quantifier free. For $\mathsf{PTML}^{2}$, we introduce a combination of these two normal forms, which we call the Fine Scott Normal form given by a $\mathsf{DNF}$, where every clause is of the form:

[TABLE]

where $a,m_{x},m_{y},n_{x},n_{y},b\geq 0$ and $s_{i}$ denotes literals. Further, $\alpha,\beta_{j}$ are recursively in the normal form and $\gamma,\delta_{k},\varphi,\psi_{l}$ do not have quantifiers at the outermost level and all modal subformulas occurring in these formulas are (recursively) in the normal form. The normal form is formally defined in the next subsection.

Note that the first two conjuncts mimic the modal normal form and the last two conjuncts mimic the $\mathsf{FO}^{2}$ normal form. The additional conjuncts handle the intermediate step where only one of the variable is quantified and the other is free.

We now formally define the normal form and prove that every $\mathsf{PTML}^{2}$ formula has a corresponding equi-satisfiable formula in the normal form. After this we prove the bounded agent property for formulas in the normal form using an inductive $\mathsf{FO}^{2}$ type model construction.

3.1 Normal form

We use $\{x,y\}\subseteq\textsf{Var}$ as the two variables of $\mathsf{PTML}^{2}$. We use $z$ to refer to either $x$ or $y$ and refer to variables $z_{1},z_{2}$ to indicate the variables $x,y$ in either order. We use $\Delta_{z}$ to denote any modal operator $\Delta\in\{\Box,\Diamond\}$ and $z\in\{x,y\}$. A literal is either a proposition or its negation. Also, we assume that the formulas are given in negation normal form(NNF) where the negations are pushed in to the literals.

Definition 3.1** (FSNF normal form).**

We define the following terms to introduce the Fine Scott normal form (FSNF) for $\mathsf{PTML}^{2}$:

• •

A formula $\varphi$ is a module if $\varphi$ is a literal or $\varphi$ is of the form $\Delta_{z}\alpha$.

• •

For any formula $\varphi$, the outer most components of $\varphi$ given by $\mathsf{C}(\varphi)$ is defined inductively where for any $\varphi$ which is a module, $\mathsf{C}(\varphi)=\{\varphi\}$ and $\mathsf{C}(Qz\ \varphi)=\{Qz\ \varphi\}$ where $z\in\{x,y\}$ and $Q\in\{\forall,\exists\}$. Finally $\mathsf{C}(\varphi\odot\psi)=\mathsf{C}(\varphi)\cup\mathsf{C}(\psi)$ where $\odot\in\{\land,\lor\}$.

• •

A formula $\varphi$ is quantifier-safe if every $\psi\in\mathsf{C}(\varphi)$ is a module.

• •

We define $Fine\leavevmode\nobreak\ Scott\leavevmode\nobreak\ normal\leavevmode\nobreak\ form$(FSNF) normal form ($\mathsf{DNF}$* and conjunctions) inductively as follows:*

• –

Any conjunction of literals is an FSNF conjunction.

• –

$\varphi$* is said to be in $\textsf{FSNF}\leavevmode\nobreak\ \mathsf{DNF}$ if $\varphi$ is a disjunction where every clause is an FSNF conjunction.*

• –

*Suppose $\varphi$ is quantifier-safe and for every $\Delta_{z}\psi\in\mathsf{C}(\varphi)$ if $\psi$ is in $\textsf{FSNF}\leavevmode\nobreak\ \mathsf{DNF}$ normal form then we call $\varphi$ a quantifier-safe  *normal formula.

• –

*Let $a,b,m_{x},m_{y},n_{x},n_{y}\geq 0$. *

Suppose $s_{1},\ldots,s_{a}$ are literals, $\alpha^{x},\alpha^{y},\beta^{x}_{1},\ldots,\beta^{x}_{m_{x}},\beta^{y}_{1},\ldots,\beta^{y}_{m_{y}}$ are formulas in $\textsf{FSNF}\leavevmode\nobreak\ \mathsf{DNF}$ and $\gamma^{x},\gamma^{y},\delta^{x}_{1},\ldots,\delta^{x}_{n_{x}},\delta^{y}_{1},\ldots,\delta^{y}_{n_{y}},\varphi,\psi_{1},\ldots,\psi_{b}$ are quantifier-safe  ** normal formulas then:

[TABLE]

is an FSNF conjunction.

Quantifier-safe formulas are those in which no quantifiers occur outside the scope of modalities. Note that the superscripts in $\alpha^{x},\alpha^{y}$ etc only indicate which variable the formula is associated with, so that it simplifies the notation. For instance, $\alpha^{x}$ does not say anything about the free variables in $\alpha^{x}$. In fact there is no restriction on free variables in any of these formulas.

Further, note that by setting the appropriate indices to [math], we can have FSNF conjunctions where one or more of the components corresponding to $s_{i},\beta^{x},\beta^{y},\delta^{x},\delta^{y},\psi_{l}$ are absent. We also consider the conjunctions where one or more of the components corresponding to $\Box_{x}\alpha^{x},\Box_{y}\alpha^{y},\varphi$ are also absent. As we will see in the next lemma, for any sentence $\varphi\in\mathsf{PTML}^{2}$, we can obtain an equi-satisfiable sentence, which at the outer most level, is a $\mathsf{DNF}$ where every clause is of the form $\bigwedge\limits_{i\leq a}s_{i}\leavevmode\nobreak\ \land\leavevmode\nobreak\ \forall x\forall y\leavevmode\nobreak\ \varphi\land\bigwedge\limits_{l\leq b}\forall x\exists y\leavevmode\nobreak\ \psi_{l}$.

Lemma 3.2**.**

For every formula $\varphi\in\mathsf{PTML}^{2}$ there is a corresponding formula $\psi$ in $\textsf{FSNF}\leavevmode\nobreak\ \mathsf{DNF}$ such that $\varphi$ and $\psi$ are equi-satisfiable.

Proof 3.3**.**

We prove this by induction on the modal depth of $\theta$. Suppose $\theta$ has modal depth [math], then all modules occurring in $\varphi$ are literals. Observe that if $\alpha$ is a propositional formula then for $Q\in\{\forall,\exists\}$ and $z\in\{x,y\}$ and for all model $M$ we have $M,w,\sigma\models Qz\leavevmode\nobreak\ \alpha$ iff $M,w,\sigma\models\alpha$. Hence we can simply ignore all the quantifiers and get an equivalent $\mathsf{DNF}$ over literals, which is an $\textsf{FSNF}\leavevmode\nobreak\ \mathsf{DNF}$.

For the induction step, suppose $\textsf{md}(\theta)=h$. First observe that we can get an equivalent $\mathsf{DNF}$ formula for $\theta$ (say $\theta_{1}$) over $\mathsf{C}(\theta)$ using propositional validities. Now if $\theta_{1}$ is an $\textsf{FSNF}\leavevmode\nobreak\ \mathsf{DNF}$ then we are done. Otherwise, there are some clauses in $\theta_{1}$ that are not FSNF clause. Let $\theta_{1}:=\bigvee_{i}\zeta_{i}$ and $I_{\theta}=\{\zeta_{i}\mid\zeta_{i}$ is not a FSNF clause$\}$ be the clauses that are not FSNF conjunctions. To reduce $\theta_{1}$ in to $\textsf{FSNF}\leavevmode\nobreak\ \mathsf{DNF}$, we replace every $\zeta_{i}\in I_{\theta}$ with their corresponding equi-satisfiable $\textsf{FSNF}\leavevmode\nobreak\ \mathsf{DNF}$ in $\theta_{1}$.

Pick a clause $\zeta\in I_{\theta}$ and let $\zeta:=\omega_{1}\land\ldots\land\omega_{n}$ that is not an FSNF conjunction. If $\textsf{md}(\zeta)<h$ then by induction hypothesis, there is an equi-satisfiable $\textsf{FSNF}\leavevmode\nobreak\ \mathsf{DNF}$ formula of $\zeta$. Thus $\zeta$ can be replaced by its corresponding equi-satisfiable $\textsf{FSNF}\leavevmode\nobreak\ \mathsf{DNF}$ in $\theta_{1}$. Now suppose $\textsf{md}(\zeta)=h$. Call each $\omega_{i}$ as a conjunct.

In the first step, consider the conjuncts with exactly $1$ free variable. Let $I_{z}=\{\omega_{i}\mid\textsf{Fv}(\omega)=\{z\}\}$ for $z\in\{x,y\}$ be the index of all conjuncts where $z$ is the only free variable. Let $z_{1},z_{2}$ be the variables $x,y$ in either order. Pick any $\omega_{i}\in I_{z_{1}}$ which means $z_{2}$ is bounded in $\omega_{i}$. Hence, without loss of generality, $\omega_{i}$ is of the form $\forall z_{2}\leavevmode\nobreak\ \eta$. We will first ensure that $\eta$ is quantifier-safe. This is done by iteratively removing the non-modules from $\mathsf{C}(\eta)$ and replacing it with a equi-satisfiable quantifier-safe formula. Set $\chi_{0}:=\forall z_{2}\leavevmode\nobreak\ \eta$.

1. a.

if there is some strict subformula of the form $Qz_{2}\ \lambda\in\mathsf{C}(\chi_{0})$ where $\lambda$ is quantifier-safe, let $P$ be a new (intermediate) unary predicate. Define $\chi_{1}:=\chi_{0}[P(z_{1})/Qz_{2}\leavevmode\nobreak\ \lambda]$ and $\tau_{1}:=P(z_{1})\Leftrightarrow Qz_{2}\leavevmode\nobreak\ \lambda$. Note that if $Q=\forall$ then $\tau_{1}$ can be equivalently written as $\forall z_{2}\leavevmode\nobreak\ (\neg P(z_{1})\lor\lambda)\land\exists z_{2}\leavevmode\nobreak\ (P(z_{1})\lor\neg\lambda)$ and if $Q=\exists$ then $\tau_{1}$ will be $\exists z_{2}\leavevmode\nobreak\ (\neg P(z_{1})\lor\lambda)\land\forall z_{2}\leavevmode\nobreak\ (P(z_{1})\lor\neg\lambda)$. 2. b.

if there is some strict subformula of the form $Qz_{1}\leavevmode\nobreak\ \lambda\in\mathsf{C}(\chi_{0})$ where $\lambda$ is quantifier-safe, let $P$ be a new unary predicate. Define $\chi_{1}:=\chi_{0}[P(z_{2})/Qz_{1}\leavevmode\nobreak\ \lambda]$ and $\tau_{1}:=\forall z_{2}\leavevmode\nobreak\ (P(z_{2})\Leftrightarrow Qz_{1}\leavevmode\nobreak\ \lambda)$. Again, that if $Q=\forall$ then $\tau_{1}$ is equivalent to $\forall z_{2}\forall z_{1}(\neg P(z_{2})\lor\lambda)\land\forall z_{2}\exists z_{1}(P(z_{2})\lor\neg\lambda)$ and if $Q=\exists$ then $\tau_{1}$ is $\forall z_{2}\forall z_{1}\leavevmode\nobreak\ (P(z_{2})\lor\neg\lambda)\land\forall z_{2}\exists z_{1}\leavevmode\nobreak\ (\neg P(z_{2})\lor\lambda)$.

Now remove the conjunct $\omega_{i}$ from $\zeta$ and replace it with $\chi_{1}\land\tau_{1}$. Note that $\chi_{1}$ has at least one less quantifier than $\chi_{0}$ and $\tau_{1}$ introduces either conjuncts with no free variables or a formula with one free variable of the form $Qz\leavevmode\nobreak\ \lambda$ where $\lambda$ is quantifier-safe. To see that this step preserves equi-satisfiability, note that in both cases, $\chi_{1}\land\tau_{1}$ implies $\chi_{0}$ and for the other direction, we can define the valuation $\rho$ for the new unary predicate $P$ appropriately in the given model in which $\psi$ is satisfiable.

Repeat this step for $\chi_{1},\chi_{2},\ldots,\chi_{m}$ till $\chi_{m}$ is of the form $\forall z_{2}\lambda$ where $\lambda$ is quantifier-safe. Then we would have $\chi_{m}\land\tau_{1}\ldots\land\tau_{m}$ as new conjuncts replacing $\omega_{i}$ in $\zeta$. Now this step increases the number of conjuncts in $\zeta$ which have no free variables, but all new conjuncts with one free variable is of the form $Qz\leavevmode\nobreak\ \lambda$ where $\lambda$ is quantifier-safe (it needs to be further refined since it is not yet quantifier-safe  FSNF).

Repeat this step for all $\omega_{i}\in I_{z}$ for $z\in\{x,y\}$. Let the resulting clause be $\zeta_{1}$ which is equi-satisfiable to $\zeta$. Now for $z\in\{x,y\}$, if there are two conjuncts of the form $\forall z\leavevmode\nobreak\ \lambda$ and $\forall z\leavevmode\nobreak\ \lambda^{\prime}$ in $\zeta_{1}$, remove both of them from and add $\forall z\leavevmode\nobreak\ (\lambda\land\lambda^{\prime})$ to $\zeta_{1}$. Repeat this till there a single conjunct in $\zeta_{1}$ of the form $\forall z\leavevmode\nobreak\ \gamma^{z}$ for each $z\in\{x,y\}$ where $\gamma^{z}$ is quantifier-safe. Note that there are some new unary predicates introduced and hence this intermediate formula $\zeta_{1}$ is not in $\mathsf{PTML}^{2}$ (but is in $\mathsf{TML}^{2}$).

Let $\zeta_{1}:=\omega^{\prime}_{1}\land\ldots\land\omega^{\prime}_{n_{1}}$ which is the result of rewriting of the clause $\zeta$ after the above steps. Now consider conjuncts with no free variables and make them quantifier-safe. Let $I=\{\omega^{\prime}_{i}\mid\textsf{Fv}(\psi^{\prime})=\{x,y\}\}$. For any $\omega^{\prime}_{i}\in I$, since neither variable is free, without loss of generality assume that $\omega^{\prime}_{i}$ is of the form $\forall x\leavevmode\nobreak\ \eta$.

Pick any $\omega^{\prime}_{i}\in I$ and set $\chi_{0}:=\forall x\leavevmode\nobreak\ \eta$ and $z_{1},z_{2}$ refer to $x,y$ in either order. If $Qz_{2}\leavevmode\nobreak\ \lambda\in\mathsf{C}(\eta)$, let $P$ be a new unary predicate. Define $\chi_{1}:=\chi_{0}[P(z_{1})/Qz_{2}\leavevmode\nobreak\ \lambda]$ and $\tau_{1}:=\forall z_{1}\leavevmode\nobreak\ (P(z_{1})\Leftrightarrow Qz_{2}\leavevmode\nobreak\ \lambda$). Similar to previous step, $\tau_{1}$ can be equivalently written as two conjuncts of the form $\forall z_{1}\forall z_{2}\leavevmode\nobreak\ \lambda\land\forall z_{1}\exists z_{2}\leavevmode\nobreak\ \lambda$ where $\lambda$ and $\lambda^{\prime}$ are quantifier-safe formulas (but not quantifier-safe  FSNF, yet).

Now remove the conjunct $\omega^{\prime}_{i}$ from $\zeta_{1}$ and replace it with $\chi_{1}\land\tau_{1}$. Note that $\chi_{1}$ has at least one less quantifier than $\chi_{0}$ and $\tau_{1}$ introduces only conjuncts of the form $Q_{1}z_{1}Q_{2}\leavevmode\nobreak\ z_{2}\leavevmode\nobreak\ \lambda$ where $\lambda$ is quantifier-safe. Again for the equi-satisfiability argument, note that $\chi_{1}\land\tau_{1}\supset\chi_{0}$ is a validity and for the other direction, the new predicates can be interpreted appropriately in the same model of $\zeta_{1}$.

Repeat this step for $\chi_{1},\chi_{2},\ldots,\chi_{m}$ till $\chi_{m}$ is of the form $\forall x\lambda$ where $\lambda$ is quantifier-safe. Then we would have $\chi_{m}\land\tau_{1}\ldots\land\tau_{m}$ as new conjuncts replacing $\omega^{\prime}_{i}$. Now rename the variables appropriately in the newly introduced conjuncts so that we have formulas only of the form $\forall x\forall y\leavevmode\nobreak\ \lambda$ or $\forall x\exists y\leavevmode\nobreak\ \lambda^{\prime}$ where $\lambda,\lambda^{\prime}$ are quantifier-safe formulas.

Repeat this step for all $\omega^{\prime}_{i}\in I$. Let the resulting conjunct be $\zeta_{2}$ which is equi-satisfiable to $\zeta_{1}$. Now if there are two conjuncts of the form $\forall x\forall y\leavevmode\nobreak\ \lambda$ and $\forall x\forall y\leavevmode\nobreak\ \lambda^{\prime}$ in $\zeta_{2}$, remove both of them and add a new conjunct $\forall x\forall y\leavevmode\nobreak\ (\lambda\land\lambda^{\prime})$ to $\zeta_{2}$. Repeat this till at most one conjunct the form $\forall x\forall y\leavevmode\nobreak\ \lambda$ in $\zeta_{2}$. Note that we still have unary predicates in $\zeta_{2}$ and hence $\zeta_{2}$ is also a $\mathsf{TML}^{2}$ formula but not a $\mathsf{PTML}^{2}$ formula. Further, all subformulas inside the scope of quantifiers are now quantifier-safe, but needs to be converted into quantifier-safe  FSNF.

Let $\zeta_{2}:=\omega^{\prime\prime}_{1}\land\ldots\land\omega^{\prime\prime}_{n_{2}}$ be the resulting formula after the above steps. Now to eliminate the newly introduced unary predicates, apply the translation in definition 2.7 to $\zeta_{2}$ and obtain an equi-satisfiable $\mathsf{PTML}$ formula $\zeta_{3}$. It is clear from the construction that the new predicates are introduced only at the outermost level (not inside the scope of any modality). Thus, in the translation occurrence of the newly introduced predicate of the form $P(z)$ will be replaced by $\Diamond_{z}(\neg r\land p)$ and $\neg P(z)$ will be translated to $\neg\Diamond_{z}(\neg r\land p)$ which can be equivalently written as $\Box_{z}(r\lor\neg p)$.

Now consider conjuncts that are modal formulas. For $z\in\{x,y\}$, if there are two conjuncts of the form $\Box_{z}\leavevmode\nobreak\ \lambda$ and $\Box_{z}\leavevmode\nobreak\ \lambda^{\prime}$ in $\zeta_{3}$, remove both of them from and add $\Box_{z}\leavevmode\nobreak\ (\lambda\land\lambda^{\prime})$ to $\zeta_{3}$. Repeat this till there at most one conjunct in $\zeta_{3}$ of the form $\Box_{z}\leavevmode\nobreak\ \alpha^{z}$ for each $z\in\{x,y\}$. Note that this step preserves equi-satisfiability because of the validity \forall z\leavevmode\nobreak\ \big{(}(\Box_{z}\alpha\land\Box_{z}\beta)\Leftrightarrow\Box_{z}(\alpha\land\beta)\big{)}.

By rearranging the conjuncts, we obtain the formula $\zeta_{3}$ in the form:

[TABLE]

where $\gamma,\delta^{z}_{k},\varphi$ and $\psi_{l}$ are quantifier-safe.

As a final step, we need to ensure that $\alpha^{x},\alpha^{y},\beta^{x}_{1},\ldots,\beta^{x}_{m_{x}},\beta^{y}_{1},\ldots,\beta^{y}_{m_{y}}$ are formulas in $\textsf{FSNF}\leavevmode\nobreak\ \mathsf{DNF}$ and $\gamma^{x},\gamma^{y},\delta^{x}_{1},\ldots,\delta^{x}_{n_{x}},\delta^{y}_{1},\ldots,\delta^{y}_{n_{y}},\varphi,\psi_{1},\ldots,\psi_{b}$ are not just quantifier-safe, but also quantifier-safe  FSNF formulas.

Note $\alpha^{z},\beta^{z}_{j}$ have modal depth less than $h$. Hence, inductively we have equi-satisfiable $\textsf{FSNF}\leavevmode\nobreak\ \mathsf{DNF}$ which each of them can be correspondingly replaced in $\zeta_{3}$. This preserves equi-satisfiability since we can inductive maintain that the translated formulas are satisfied in the same model of the given formula by just by tweaking the $\rho$ function.

To translate the formulas $\gamma^{x},\gamma^{y},\delta^{x}_{1},\ldots,\delta^{x}_{n_{x}},\delta^{y}_{1},\ldots,\delta^{y}_{n_{y}},\varphi,\psi_{1},\ldots,\psi_{b}$ into quantifier-safe  FSNF, first note that these formulas are already quantifier-safe. Now for every $\Delta_{z}\chi\in\mathsf{C}(\mu)$ for $\mu$ is one of the above formulas, we have $\textsf{md}(\chi)\leq h$. Again, inductively we have equi-satisfiable FSNF formulas for each of them. Replacing each such subformula with their corresponding $\textsf{FSNF}\leavevmode\nobreak\ \mathsf{DNF}$ formula gives us the required FSNF conjunction $\zeta_{4}$ which is equi-satisfiable to $\zeta$ that we started with. Thus $\zeta$ can be replaced by $\zeta_{4}$ in $\theta_{1}$.

Repeating this for every $\zeta\in I_{\theta}$ and replacing it in $\theta_{1}$ we obtain an equi-satisfiable $\textsf{FSNF}\leavevmode\nobreak\ \mathsf{DNF}$ for $\theta$.

Since we repeatedly convert the formula into $\mathsf{DNF}$ (inside the scope of every modality), if we start with a formula of length $n$, the final translated formula has length $2^{O(n^{2})}$. However, observe that the number of modules in the translated formula is linear in the size of the given formula $\varphi$. Furthermore, the given formula is satisfiable in a model $M$ iff the translation is satisfiable in $M$ with appropriate modification of the $\rho$ (valuation function).

3.2 Bounded agent property

Now we prove that any formula $\theta\in\mathsf{PTML}^{2}$ in $\textsf{FSNF}\leavevmode\nobreak\ \mathsf{DNF}$ is satisfiable iff $\theta$ is satisfiable in a model $M$ where the size of $D$ is bounded. Note that for any $\mathsf{PTML}$ formula $\theta$, if $M,w,\sigma\models\theta$ then $M^{T},w,\sigma\models\theta$ where $M^{T}$ is the standard tree unravelling of $M$ with $w$ as root [15]. Further, $M^{T}$ can be restricted to be of height at most $\textsf{md}(\theta)$. Hence, we restrict our attention to tree models of finite depth.

First we define the notion of types for agents at every world. In classical $\mathsf{FO}^{2}$ the $2$-types are defined on atomic predicates. In $\mathsf{PTML}^{2}$ we need to define the types with respect to modules. In any given tree model $M$ rooted at $r$, for any $w\in W$ and $c,d\in D_{w}$ the 2-type of $(c,d)$ at $w$ is simply the set of all modules that are true at $w$ where the two variables are assigned $c,d$ in either order. The 1-type of $c$ at $w$ includes the set of all modules that are true at $w$ when both $x,y$ are assigned $c$. Further, for every non-root node $w$, suppose ($w^{\prime}\xrightarrow{a}w$) then the 1-type of any $c\in D_{w}$ should capture how $c$ behaves with respect to $a$ and the $1$-$\textsf{type}(w,c)$ should also include the information of how $c$ acts with respect to $d$, for every $d\in D_{w}$. Thus the 1-type of $c$ at $w$ is given by a 3-tuple where the first component is the set of all modules that are true when both $x,y$ are assigned $c$, the second component captures how $c$ behaves with respect to the incoming edge of $w$ and the third component is a set of subsets of formulas such that for each $d\in D_{w}$ there is a corresponding subset of formulas capturing the $2$-type of $c,d$. To ensure that the type definition also carries the information of the height of the world $w$, if $w$ is at height $h$ then we restrict 1-type and 2-type at $w$ to modules of modal depth at most $\textsf{md}(\varphi)-h$.

For any formula $\varphi$, let $\textsf{SF}(\varphi)$ be the set of all subformulas of $\varphi$ closed under negation. We always assume222Let $p_{0}$ be some proposition occurring in $\varphi$, then $\top$ is defined as $p_{0}\lor\neg p_{0}$. that $\top\in\textsf{SF}(\varphi)$. Let $\textsf{SF}^{h}(\varphi)\subseteq\textsf{SF}(\varphi)$ be the set of all subformulas of modal depth at most $\textsf{md}(\varphi)-h$. Thus we have $\textsf{SF}(\varphi)=\textsf{SF}^{0}(\varphi)\supseteq\textsf{SF}^{1}(\varphi)\supseteq\ldots\supseteq\textsf{SF}^{\textsf{md}(\varphi)}(\varphi)$.

Definition 3.4** ($\mathsf{PTML}\leavevmode\nobreak\ \textsf{type}$).**

For any $\mathsf{PTML}^{2}$ formula $\varphi$ and for any tree model $M$ rooted at $r$ with height at most $\textsf{md}(\varphi)$, for all $w\in W$ at height $h$:

• •

For all $c,d\in\delta(w)$, define 2-$type(w,c,d)=(\Gamma_{xy};\Gamma_{yx})$* where*

$\Gamma_{xy}=\{\psi(x,y)\in\textsf{SF}^{h}(\varphi)\mid M,w\models\psi(c,d)\}$* and *

$\Gamma_{yx}=\{\psi(x,y)\in\textsf{SF}^{h}(\varphi)\mid M,w\models\psi(d,c)\}$.

• •

If $w$ is a non root node, (say $w^{\prime}\xrightarrow{a}w$) then for all $c\in\delta(w)$ define $1$-$\textsf{type}(w,c)=(\Lambda_{1};\Lambda_{2};\Lambda_{3})$* where $\Lambda_{1}=2$-$\textsf{type}(w,c,c)$ and $\Lambda_{2}=2$-$\textsf{type}(w,c,a)$ and $\Lambda_{3}=\{2$-$\textsf{type}(w,c,d)\mid d\in\delta(w)\}$.*

• •

For the root node $r$, for all $c\in\delta(r)$ define $1$-$\textsf{type}(w,c)=(\Lambda_{1};\{\top\};\Lambda_{3})$* where *

$\Lambda_{1}=2$-$\textsf{type}(w,c,c)$* and $\Lambda_{3}=\{2$-$\textsf{type}(w,c,d)\mid d\in\delta(w)\}$.*

The second component of 1-$\textsf{type}(r,c)$ is added to maintain uniformity. For all $w\in W$ define 1-$\textsf{type}(w)=\{$1-$\textsf{type}(w,c)\mid c\in D_{w}\}$ and 2-$\textsf{type}(w)=\{$2-$\textsf{type}(w,c,d)\mid c,d\in D_{w}\}$. We use $\Lambda,\Pi$ to represent elements of 1-$\textsf{type}(w)$ and $\Lambda_{1},\Pi_{2}$ etc for the respective components.

If a formula $\theta$ is satisfiable in a tree model, the strategy is to inductively come up with bounded agent models for every subtree of the given tree (based on types), starting from leaves to the root. While doing this, when we add new type based agents to a world at height $h$, to maintain monotonicity, we need to propagate the newly added agents throughout its descendants. For this, we define the notion of extending any tree model by addition of some new set of agents.

Suppose in a tree model $M$, world $w$ has local agent set $D_{w}$ and we want to extend $D_{w}$ to $D_{w}\cup C$, then first we have $\Omega:C\mapsto D_{w}$ which assigns every new agent to some already existing agent. The intended meaning is that the newly added agent $c\in C$ at $w$ mimics the ‘type’ of $\Omega(c)$. If $w$ is a leaf node, we can simply extend $\delta(w)$ to $D_{w}\cup C$. If $w$ is at some arbitrary height, along with adding the new agents to the live agent set to $w$, we also need to create successors for every $c\in C$, one for each successor subtree of $\Omega(c)$ and inductively add $C$ to all the successor subtrees.

Definition 3.5** (Model extension).**

Suppose $M$ is a tree model rooted at $r$ with finite agent set $D$ and for every $w\in W$ let $M^{w}$ be the subtree rooted at $w$. Let $C$ be some finite set such that $C\cap D=\emptyset$ and for any $w\in W$ let $\Omega:C\mapsto D_{w}$ be a function mapping $C$ to agent set live at $w$. Define the operation of ‘adding $C$ to $M^{w}$ guided by $\Omega$’ by induction on the height of $w$ to obtain a new subtree rooted at $w$ (denoted by $M^{w}_{(C,\Omega)}$ and the components denoted by $\delta^{\prime},\rho^{\prime}$ etc).

• •

If $w$ is a leaf, then $M^{w}_{(C,\Omega)}$ is a tree with a single node $w$ with new $\delta^{\prime}(w)=\delta(w)\cup C$ and $\rho^{\prime}(w)=\rho(w)$.

• •

If $w$ is at height $h$ then the new tree $M^{w}_{(C,\Omega)}$ is obtained from $M^{w}$ rooted at $w$ with new $\delta^{\prime}(w)=\delta(w)\cup C$ and $\rho^{\prime}(w)=\rho(w)$ and replacing all the subtrees $M^{u}$ rooted at every successor $u$ of $w$ by $M^{u}_{(C,\Omega)}$. Furthermore, for every $c\in C$ and every $(w,\Omega(c),u)\in R$ create a new copy of $M^{u}_{(C,\Omega)}$ and rename its root as $u^{c}$ and add an edge $(w,c,u^{c})$ to $R^{\prime}$.

Since we do not have equality in the language, this transformation will still continue to satisfy the same formulas.

Lemma 3.6**.**

Let $M$ be any tree model of finite depth rooted at $r$ with finite agent set $D$ and let $w\in W$. Let $M^{w}_{(C,\Omega)}$ (rooted at $w$) be an appropriate model extension of $M^{w}$ (rooted at $w$). For any interpretation $\sigma:\textsf{Var}\mapsto(C\cup D_{w})$ let $\hat{\sigma}:\textsf{Var}\mapsto D_{w}$ where $\hat{\sigma}(x)=\Omega(\sigma(x))$ if $\sigma(x)\in C$ and $\hat{\sigma}(x)=\sigma(x)$ if $\sigma(x)\in D_{w}$. Then for all $u\in W$ which is a descendant of $w$ in $M$ and for all $\sigma:\textsf{Var}\mapsto(C\cup D_{w})$ and for all $\mathsf{PTML}$ formula $\varphi$, we have $M^{w}_{(C,\Omega)},u,\sigma\models\varphi$ iff $M,u,\hat{\sigma}\models\varphi$.

Proof 3.7**.**

The proof is by reverse induction on the height of $w$. In the base case $w$ is a leaf. Note that $\rho(w)$ remains the same both the models. Hence all propositional formulas continue to equi-satisfy in both the models at $w$. Since $w$ is a leaf, there are no descendants in both the models and hence all modal formulas continue to equi-satisfy. Finally, since $\delta$ is non-empty in both the models at $w$, for all formula $\alpha\in\mathsf{PTML}$ we have $M^{w}_{(C,\Omega)},w,\sigma\models Q\leavevmode\nobreak\ x\leavevmode\nobreak\ \alpha$ iff $M,w,\hat{\sigma}\models Q\leavevmode\nobreak\ x\leavevmode\nobreak\ \alpha$ where for $Q\in\{\forall,\exists\}$.

For the induction step, let $w$ be at height $h$. Now we induct on the structure of $\varphi$. Again, if $\varphi$ is a proposition, then the claim follows since $\rho(w)$ remains same. The cases of $\neg$ and $\land$ are standard.

For the case of $\Diamond_{x}\leavevmode\nobreak\ \varphi$, we need to consider two cases: when $\sigma(x)\in C$ and $\sigma(x)\in D_{w}$.

• •

If $\sigma(x)\in C$ then let $\Omega(c)=d$ and hence $\hat{\sigma}(x)=d$. Now, if $M^{w}_{(C,\Omega)},w,\sigma\models\Diamond_{x}\varphi$ then there is some $(w,c,w^{\prime})\in R^{w}_{(C,\Omega)}$ such that $M^{w}_{(C,\Omega)},w^{\prime},\sigma\models\varphi$. By construction, $w^{\prime}$ is of the form $u^{c}$ and the subtree rooted at $u^{c}$ is a copy of $M^{u}_{(C,\Omega)}$ for some $(w,d,u)\in R$. Hence $M^{u}_{(C,\Omega)},u,\sigma\models\varphi$ and by induction hypothesis $M,u,\hat{\sigma}\models\varphi$. Thus, $M,w,\hat{\sigma}\models\Diamond_{x}\varphi$.

Suppose $M,w,\hat{\sigma}\models\Diamond_{x}\varphi$, then there is some $(w,d,u)\in R$ such that $M,u,\hat{\sigma}\models\varphi$. By induction hypothesis, $M^{u}_{(C,\Omega)},u,\sigma\models\varphi$ . Now, since $\Omega(c)=d$, by construction there is $(w,d,u^{c})\in R^{w}_{(C,\Omega)}$ such that the sub-tree rooted at $u^{c}$ is a copy of $M^{u}_{(C,\Omega)}$. Hence $M^{w}_{(C,\Omega)},u^{c},\sigma\models\varphi$. Thus $M^{w}_{(C,\Omega)},w,\sigma\models\Diamond_{x}\varphi$.

• •

If $\sigma(x)\in D_{w}$, let $\sigma(x)=d$. Now $M^{w}_{(C,\Omega)},w,\sigma\models\Diamond_{x}\varphi$ iff there is some $(w,d,u)\in R^{w}_{(C,\Omega)}$ such that $M^{w}_{(C,\Omega)},u,\sigma\models\varphi$ iff (by construction) $(w,d,u)\in R$ and the sub-tree rooted at $u$ in $M^{w}_{(C,\Omega)}$ is a copy of $M^{u}_{(C,\Omega)}$ iff $M^{u}_{(C,\Omega)},u,\sigma\models\varphi$ iff (by induction) $M,u,\hat{\sigma}\models\varphi$ iff $M,w,\hat{\sigma}\models\Diamond_{x}\varphi$.

For the case of $\exists x\leavevmode\nobreak\ \varphi$, we have $M^{w}_{(C,\Omega)},w,\sigma\models\exists x\leavevmode\nobreak\ \varphi$ iff there is some $c\in C\cup D_{w}$ such that $M^{w}_{(C,\Omega)},w,\sigma_{[x\mapsto c]}\models\varphi$ iff (by induction) $M,w,\hat{\sigma}_{[x\mapsto c]}\models\varphi$ iff $M,w,\hat{\sigma}\models\exists x\leavevmode\nobreak\ \varphi$.

For any formula in the normal form, we use the same notations as in Def. 3.1. For a given formula $\theta\in\mathsf{PTML}^{2}$ in $\textsf{FSNF}\leavevmode\nobreak\ \mathsf{DNF}$ form, let $\boldsymbol{\delta}_{\theta}^{x}=\{\exists y\leavevmode\nobreak\ \delta^{x}\in\textsf{SF}(\theta)\}$. Similarly we have $\boldsymbol{\delta}_{\theta}^{y}=\{\exists x\leavevmode\nobreak\ \delta^{y}\in\textsf{SF}(\theta)\}$ and $\boldsymbol{\psi}_{\theta}=\{\forall x\exists y\leavevmode\nobreak\ \psi\in\textsf{SF}(\varphi)\}$.

For any tree model $M$, let $\#\not\in D$. For every $w\in W$ and for all $\exists y\leavevmode\nobreak\ \delta\in\boldsymbol{\delta}_{\theta}^{x}$ let the function $g^{w}_{\delta}:D_{w}\mapsto D_{w}\cup\{\#\}$ be a mapping such that $M,w\models\delta(c,g^{w}_{\delta}(c))$ and $g^{w}_{\delta}(c)=\#$ only if there is no $d\in D_{w}$ such that $M,w\models\delta(c,d)$. Similarly for all $\exists x\leavevmode\nobreak\ \delta\in\boldsymbol{\delta}_{\theta}^{y}$ let $h^{w}_{\delta}:D_{w}\mapsto D_{w}\cup\{\#\}$ such that $M,w\models\delta(h^{w}_{\delta}(c),h)$ and $h^{w}_{\delta}(c)=\#$ only if there is no $d\in D_{w}$ such that $M,w\models\delta(d,c)$. Again for all $\forall x\exists y\leavevmode\nobreak\ \psi\in\boldsymbol{\psi}_{\theta}$ let $f^{w}_{\psi}:D_{w}\mapsto D_{w}\cup\{\#\}$ such that $M,w\models\psi(c,f^{w}_{\psi}(c))$ and $f^{w}_{\psi}(c)=\#$ only if there is no $d\in D_{w}$ such that $M,w\models\psi(c,d)$.

The functions $g,h,f$ provide the witnesses at a world for every agent (if it exists) for the existential formulas respectively.

Theorem 3.8**.**

Let $\theta\in\mathsf{PTML}^{2}$ be in an $\textsf{FSNF}\leavevmode\nobreak\ \mathsf{DNF}$ sentence. Then $\theta$ is satisfiable iff $\theta$ is satisfiable in a model with bounded number of agents.

Proof 3.9**.**

It suffices to prove $(\Rightarrow)$. Let $M$ be a tree model of height at most $\textsf{md}(\theta)$ rooted at $r$ such that $M,r\models\theta$.

Let $E_{\theta}=\boldsymbol{\delta}_{\theta}^{x}\cup\boldsymbol{\delta}_{\theta}^{y}\cup\boldsymbol{\psi}_{\theta}$ and hence $|\textsf{E}_{\theta}|\leq|\theta|$ (say $q$). Let $\textsf{E}_{\theta}=\{\chi_{1},\ldots\chi_{q}\}$ be some enumeration. For every $w\in W$ and $a\in\delta(w)$ let $\textsf{Wit}(a)=\{b_{1}\ldots b_{q}\}$ be the witnesses for $a$ where $b_{i}=g^{w}_{\delta}(c)$ if $\chi_{i}$ is of the form $\exists y\leavevmode\nobreak\ \delta\in\boldsymbol{\delta}^{x}_{\theta}$ (similarly $b_{i}=h^{w}_{\delta}(c)$ or $b_{i}=f^{w}_{\psi}(c)$ corresponding to $\chi_{i}$ of the from $\exists x\leavevmode\nobreak\ \delta^{y}$ and $\forall x\exists y\leavevmode\nobreak\ \psi$ respectively). If $b_{i}=\#$ then set $b_{i}=b$ for some arbitrary but fixed $b\in\delta(w)$.

For all $w\in W$ and \Lambda\in\leavevmode\nobreak\1-$\textsf{type}(w)$ fix some $a^{w}_{\Lambda}\in\delta(w)$ such that 1-$\textsf{type}(w,a^{w}_{\Lambda})=\Lambda$. Furthermore, if $c$ is the incoming edge of $w$ and 1-$\textsf{type}(w,c)=\Lambda$ then let $a^{w}_{\Lambda}=c$. Let $A^{w}=\{a^{w}_{\Lambda}\mid\Lambda\in$1-$\textsf{type}(w)\}$.

Now we define the bounded agent model. For every $w\in W$ let $M^{w}$ be the subtree model rooted at $w\in W$. For every such $M^{w}$, we define a corresponding type based model with respect to $\theta$ (denoted by $T^{w}_{\theta}$ with components denoted by $\delta^{w}_{\theta},\rho^{w}_{\theta}$ etc) inductively as follows:

• •

If $w$ is a leaf then $T^{w}_{\theta}$ is a tree with a single node $w$ with

$\delta^{w}_{\theta}(w)=$* 1-$\textsf{type}(w)\times[1\ldots q]\times\{0,1,2\}$ and $\rho^{w}_{\theta}(w)=\rho(w)$.*

• •

If $w$ is at height $h$, $T^{w}_{\theta}$ is a tree rooted at $w$ with $\delta^{w}_{\theta}(w)=$ 1-$\textsf{type}(w)\times[1\ldots q]\times\{0,1,2\}$* and $\rho^{w}_{\theta}(w)=\rho(w)$.*

Before defining the successors of $w$ in $T^{w}_{\theta}$ note that for every $(w,a,u)\in R$ we have $T^{u}_{\theta}$ which is the inductively constructed type based model rooted at $u$. Also, inductively we have $\delta^{u}_{\theta}(u)=$1-$\textsf{type}(u)\times[1\ldots q]\times\{0,1,2\}$.

Now for every $a^{w}_{\Lambda}\in A^{w}$ let $\{b_{1}\ldots b_{q}\}$ be the corresponding witnesses as described above. For every successor $(w,a^{w}_{\Lambda},u)\in R$ and for every $1\leq e\leq q$ and $f\in\{0,1,2\}$, create a new copy of $T^{u}_{\theta}$ (call it $N^{(\Lambda,e,f)}$) and name its root as $u^{(\Lambda,e,f)}$. Now add $\delta^{w}_{\theta}(w)$ to $N^{(\Lambda,e,f)}$ at $u^{(\Lambda,e,f)}$ guided by $\Omega$ where $\Omega$ is defined as follows:

• –

For all $\Pi\in 1$-$\textsf{type}(w)$* we have $a^{w}_{\Pi}\in A^{w}$. Define $\Omega((\Pi,e,f))=($1-$\textsf{type}(u,a^{w}_{\Pi}),e,f)$.*

• –

for all $k\leq q$ if 1-$\textsf{type}(u,b_{k})=\Pi$* then *$\Omega((\Pi,k,f^{\prime}))=($1-$\textsf{type}(u,b_{k}),e,f)$

where $f^{\prime}=f+1\mod 3$.

• –

Let $f^{\prime}=f-1\mod 3$. For all \Pi\in\leavevmode\nobreak\1-$\textsf{type}(w)$ let the witness set of $a^{w}_{\Pi}$ be $\{d_{1}\ldots d_{q}\}$.

For all $l\leq q$ if $1$-$\textsf{type}(w,d_{l})=\Lambda$* then by $\Lambda_{3}$ component, there is some $a\in\delta(w)$ such that $2$-$\textsf{type}(w,d_{l},a^{w}_{\Pi})=2$-$\textsf{type}(w,a^{w}_{\Lambda},a)$.   Define $\Omega((\Pi,l,f^{\prime}))=($1-$\textsf{type}(u,a),e,f)$.*

• –

For all $(\Pi,e^{\prime},f^{\prime})\in\delta^{w}_{\theta}(w)$ if $\Omega(\Pi,e^{\prime},f^{\prime})$ is not yet defined, then set $\Omega(\Pi,e^{\prime},f^{\prime})=($1-$\textsf{type}(u,a^{w}_{\Pi}),e,f)$.

Add an edge $(w,(\Lambda,e,f),u^{(\Lambda,e,f)})$ to $R^{w}_{\theta}$.

Note that $\Omega$ is well defined since the first three steps are defined for the indices $f,(f$+$1\mod 3)$ and $(f$-$1\mod 3)$ respectively, which are always distinct. Also note that $T^{r}_{\theta}$ is a model that satisfies bounded agent property. Thus, it is sufficient to prove that $T^{r}_{\theta},r\models\theta$.

Claim.* For every $w\in W$ at height $h$ and for all $\lambda\in\textsf{SF}^{h}(\theta)$ the following holds:*

Suppose $\lambda$ is a sentence and $M,w\models\lambda$ then $T^{w}_{\theta},w\models\lambda$. 2. 2.

If $\textsf{Fv}(\lambda)\subseteq\{x,y\}$ and for all \Lambda,\Pi\in\leavevmode\nobreak\1-$\textsf{type}(w)$ if $M,w,[x\mapsto a^{w}_{\Lambda},y\mapsto a^{w}_{\Pi}]\models\lambda$ then for all $1\leq e\leq q$ and $f\in\{0,1,2\}$ we have $T^{w}_{\theta},w,[x\mapsto(\Lambda,e,f),y\mapsto(\Pi,e,f)]\models\lambda$.

Note that the theorem follows from claim (1), since $\theta$ is sentence and $M,r\models\theta$.

The proof of the claim is by reverse induction on $h$. In the base case $h=\textsf{md}(\theta)$ which implies $\lambda$ is modal free and hence is a $\mathsf{DNF}$ over literals. Thus, both the claims follow since $\rho(w)=\rho^{w}_{\theta}(w)$.

For the induction step, let $w$ be at height $h$. Now we induct on the structure of $\lambda$. Again if $\lambda$ is a literal then both the the claims follow since $\rho(w)=\rho^{w}_{\theta}(w)$. The case of $\land$ and $\lor$ are standard.

For the case $\Box_{x}\lambda$, we only need to prove claim(2). Now suppose $M,w,[x\mapsto a^{w}_{\Lambda},y\mapsto a^{w}_{\Pi}]\models\Box_{x}\lambda$. Pick arbitrary $e$ and $f$. We need to prove that $T^{w}_{\theta},w,[x\mapsto(\Lambda,e,f),y\mapsto(\Pi,e,f)]\models\Box_{x}\lambda$. Pick any $(w,(\Lambda,e,f),u^{(\Lambda,e,f)})\in R^{w}_{\theta}$, then by construction we have $(w,a^{w}_{\Lambda},u)\in R$ and since $M,w,[x\mapsto a^{w}_{\Lambda},y\mapsto a^{w}_{\Pi}]\models\Box_{x}\lambda$, we have $M,u,[x\mapsto a^{w}_{\Lambda},y\mapsto a^{w}_{\Pi}]\models\lambda$. Let $a^{u}_{\Pi^{\prime}}\in A^{u}$ such that 1-$\textsf{type}(u,a^{u}_{\Pi^{\prime}})=$1-$\textsf{type}(u,a^{w}_{\Pi})$ and since $a^{w}_{\Lambda}$ is the incoming edge of $u$, by $\Pi_{2}$ component, we have 2-$\textsf{type}(u,a^{w}_{\Pi},a^{w}_{\Lambda})=$2-$\textsf{type}(u,a^{u}_{\Pi^{\prime}},a^{w}_{\Lambda})$ and also $a^{w}_{\Lambda}\in A^{u}$ . Hence $M,u,[x\mapsto a^{w}_{\Lambda},y\mapsto a^{u}_{\Pi^{\prime}}]\models\lambda$ and by induction hypothesis $T^{u}_{\theta},u,[x\mapsto($1-$\textsf{type}(u,a^{w}_{\Lambda}),e,f),y\mapsto($1-$\textsf{type}(u,a^{u}_{\Pi^{\prime}}),e,f)]\models\lambda$. Now by construction, at $u^{(\Lambda,e,f)}$ we have $\Omega{(\Lambda,e,f)}=($1-$\textsf{type}(w,a^{w}_{\Lambda}),e,f)$ and $\Omega(\Pi,e,f)=($1-$\textsf{type}(u,a^{u}_{\Pi^{\prime}}),e,f)$. Thus, by Lemma 3.6, $T^{w}_{\theta},u^{(\Lambda,e,f)},[x\mapsto(\Lambda,e,f),y\mapsto(\Pi,e,f)]\models\lambda$. Hence, we have $T^{w}_{\theta},w,[x\mapsto(\Lambda,e,f),y\mapsto(\Pi,e,f)]\models\Box_{x}\lambda$.  The case for $\Box_{y}\lambda$ is analogous.

For the case $\Diamond_{y}\lambda$, again only claim(2) applies. Suppose $M,w,[x\mapsto a^{w}_{\Lambda},y\mapsto a^{w}_{\Pi}]\models\Diamond_{y}\lambda$. Now pick $e$ and $f$ appropriately. We need to prove that $T^{w}_{\theta},w,[x\mapsto(\Gamma,e,f),y\mapsto(\Pi,e,f)]\models\Diamond_{y}\lambda$. By supposition, there is some $w\xrightarrow{a^{w}_{\Pi}}u$ such that $M,u,[x\mapsto a^{w}_{\Lambda},y\mapsto a^{w}_{\Pi}]\models\lambda$. Using the argument similar to the previous case, we can prove that $T^{w}_{\theta},u^{(\Lambda,e,f)},[x\mapsto(\Lambda,e,f),y\mapsto(\Pi,e,f)]\models\lambda$ and hence $T^{w}_{\theta},w,[x\mapsto(\Gamma,e,f),y\mapsto(\Pi,e,f)]\models\Diamond_{y}\lambda$.   The case of $\Diamond_{x}\lambda$ is symmetric.

For the case $\exists y\leavevmode\nobreak\ \lambda$ (where $x$ is free at the outer most level), for claim (2) first note that since $\theta$ is in the normal form, $\lambda$ is quantifier-safe. Also note that $\exists y\leavevmode\nobreak\ \lambda=\chi_{i}$ for some $\chi_{i}\in E_{\theta}$. Now, suppose $M,w,[x\mapsto a^{w}_{\Lambda}]\models\exists y\leavevmode\nobreak\ \lambda$ then we need to prove that $T^{w}_{\theta},w,[x\mapsto(\Lambda,e,f)]\models\exists y\leavevmode\nobreak\ \lambda$. Let the $i^{th}$ witness of $a^{w}_{\Lambda}$ be $b_{i}$ and hence $M,w,[x\mapsto a^{w}_{\Lambda},y\mapsto b_{i}]\models\lambda$. Let 1-$\textsf{type}(w,b_{i})=\Pi^{\prime}$, we claim that $T^{w}_{\theta},w,[x\mapsto(\Lambda,e,f),y\mapsto(\Pi^{\prime},i,f^{\prime})]\models\lambda$ where $f^{\prime}=f+1\mod 3$. Suppose not, then $\land$ and $\lor$ can be broken down and we get some module such that $M,w,[x\mapsto a^{w}_{\Lambda},y\mapsto b_{i}]\models\Delta_{z}\lambda^{\prime}$ and $T^{w}_{\theta},w,[x\mapsto(\Lambda,e,f),y\mapsto(\Pi^{\prime},i,f^{\prime})]\not\models\Delta_{z}\lambda^{\prime}$ where $\Delta\in\{\Box,\Diamond\}$ and $z\in\{x,y\}$. Assume $\Delta=\Box$ and $z=x$ (other cases are analogous). This implies $T^{w}_{\theta},w,[x\mapsto(\Lambda,e,f),y\mapsto(\Pi^{\prime},i,f^{\prime})]\models\Diamond_{x}\neg\lambda^{\prime}$ and hence there is some $w\xrightarrow{(\Lambda,e,f)}u^{(\Lambda,e,f)}$ such that $T^{w}_{\theta},u^{(\Lambda,e,f)},[x\mapsto(\Lambda,e,f),y\mapsto(\Pi^{\prime},i,f^{\prime})]\models\neg\lambda^{\prime}$(). By construction, there is a corresponding $w\xrightarrow{a^{w}_{\Lambda}}u$ in $M$. Now since $M,w,[x\mapsto a^{w}_{\Lambda},y\mapsto b_{i}]\models\Box_{x}\lambda^{\prime}$, we have $M,u,[x\mapsto a^{w}_{\Lambda},y\mapsto b_{i}]\models\lambda^{\prime}$. Let $b_{i}^{\prime}\in A^{u}$ such that 1-$\textsf{type}(u,b_{i})=$1-$\textsf{type}(u,b_{i}^{\prime})$. Since $a^{w}_{\Lambda}$ is the incoming edge to $u$ by $\Pi^{\prime}_{2}$ component, we have 2-$\textsf{type}(u,b_{i},a^{w}_{\Lambda})=$2-$\textsf{type}(u,b_{i}^{\prime},a^{w}_{\Lambda})$ and $a^{w}_{\Lambda}\in A^{u}$. Thus, $M,u,[x\mapsto a^{w}_{\Lambda},y\mapsto b^{\prime}_{i}]\models\lambda^{\prime}$ and by induction hypothesis, $T^{u}_{\theta},u,[x\mapsto(\Lambda,e,f),y\mapsto(1$-$\textsf{type}(u,b_{i}^{\prime}),e,f)]\models\lambda^{\prime}$. Again by construction, at $u$ we have $\Omega((\Lambda,e,f))=(\Lambda,e,f)$ and $\Omega((\Pi^{\prime},i,f^{\prime}))=(1$-$\textsf{type}(u,b_{i}^{\prime}),e,f)$ and hence by Lemma 3.6, $T^{w}_{\theta},u^{(\Lambda,e,f)},[x\mapsto(\Lambda,e,f),y\mapsto(\Pi^{\prime},i,f^{\prime})]\models\lambda^{\prime}$ which is a contradiction to ().    The case of $\exists y\leavevmode\nobreak\ \lambda$ is analogous.

For the case of $\forall x\leavevmode\nobreak\ \lambda$ (where $y$ is free at the outer most level), suppose $M,w,[y\mapsto a^{w}_{\Pi}]\models\forall x\leavevmode\nobreak\ \lambda$. We need to prove that $T^{w}_{\theta},w,[y\mapsto(\Pi,e,f)]\models\forall x\leavevmode\nobreak\ \lambda$. Pick any $(\Lambda^{\prime},e^{\prime},f^{\prime})\in\delta^{w}_{\theta}(w)$, now we claim $T^{w}_{\theta},w,[x\mapsto(\Lambda^{\prime},e^{\prime},f^{\prime}),y\mapsto(\Pi,e,f)]\models\lambda$ (otherwise, like in the previous case, since $\lambda$ is quantifier-safe, we can reach a module where they differ and obtain a contradiction).    The case $\forall y\leavevmode\nobreak\ \lambda$ is analogous.

Finally we come to sentences which are relevant for claim (1). Note that in the normal form, at the outermost level, a sentence will have only literals or formulas of the form $\forall x\exists y\leavevmode\nobreak\ \psi_{l}$ or $\forall x\forall y\leavevmode\nobreak\ \varphi$.

For the case $M,w\models\forall x\exists y\leavevmode\nobreak\ \psi_{l}$, let $\forall x\exists y\leavevmode\nobreak\ \psi_{l}$ be $i^{th}$ formula in $E_{\theta}$. We need to prove $T^{w}_{\theta},w\models\forall x\exists y\leavevmode\nobreak\ \psi_{l}$. Pick any $(\Lambda,e,f)\in\delta^{w}_{\theta}(w)$ and we have $a^{w}_{\Lambda}\in A^{w}$. Let the $i^{th}$ witness for $a^{w}_{\Lambda}$ be $b_{i}$. Thus we have $M,w,[x\mapsto a_{\Gamma},y\mapsto b_{i}]\models\psi_{l}$. Let $1$-$\textsf{type}(w,b_{i})=\Pi^{\prime}$. Again we claim that $T^{w}_{\theta},w,[x\mapsto(\Gamma,e,f),y\mapsto[\Pi^{\prime},e,f^{\prime})]\models\psi_{l}$ where $f^{\prime}=f+1\mod 3$. Suppose not, again $\land$ and $\lor$ can be broken down and we get some module such that $M,w,[x\mapsto a^{w}_{\Lambda},y\mapsto b_{i}]\models\Delta_{z}\lambda^{\prime}$ and $T^{w}_{\theta},w,[x\mapsto(\Lambda,e,f),y\mapsto(\Pi^{\prime},i,f^{\prime})]\not\models\Delta_{z}\lambda^{\prime}$ where $\Delta\in\{\Box,\Diamond\}$ and $z\in\{x,y\}$. Assume $\Delta=\Diamond$ and $z=y$ (other cases are analogous). This implies $T^{w}_{\theta},w,[x\mapsto(\Lambda,e,f),y\mapsto(\Pi^{\prime},i,f^{\prime})]\models\Box_{y}\neg\lambda^{\prime}$ (). Now let $a^{w}_{\Pi^{\prime}}\in A^{w}$ such that 1-$\textsf{type}(w,a^{w}_{\Pi^{\prime}})=1$-$\textsf{type}(w,b_{i})=\Pi^{\prime}$. Thus by $\Pi^{\prime}_{3}$ component, there is some $d\in\delta^{w}_{\theta}$ such that 2-$\textsf{type}(w,a^{w}_{\Pi^{\prime}},d)=2$-$\textsf{type}(w,b_{i},a^{w}_{\Lambda})$ and hence $M,w,[x\mapsto d,y\mapsto a^{w}_{\Pi^{\prime}}]\models\Diamond_{y}\lambda^{\prime}$. Hence there is some $w\xrightarrow{a^{w}_{\Pi^{\prime}}}u$ such that $M,u,[x\mapsto d,y\mapsto a^{w}_{\Pi^{\prime}}]\models\lambda^{\prime}$. Now let 1-$\textsf{type}(u,d)=1$-$\textsf{type}(u,d^{\prime})$ such that $d^{\prime}\in A^{u}$ and since $a^{w}_{\Pi^{\prime}}$ is the incoming edge, we have $M,u,[x\mapsto d^{\prime},y\mapsto a^{w}_{\Pi^{\prime}}]\models\lambda^{\prime}$ and by induction hypothesis, $T^{u}_{\theta},u,[x\mapsto(1$-$\textsf{type}(u,d^{\prime}),i,f^{\prime}),y\mapsto(1$-$\textsf{type}(u,a^{w}_{\Pi^{\prime}}),i,f^{\prime})]\models\lambda^{\prime}$ and while constructing $u^{(\Pi^{\prime},i,f^{\prime})}$ (case 3 applies for $a^{w}_{\Lambda}$ since its $i^{th}$ witness has same 1-type as $a^{w}_{\Pi^{\prime}}$) we have $\Omega((\Lambda,e,f^{\prime}-1))=(1$-$\textsf{type}(u,d^{\prime}),i,f^{\prime})$. Thus by Lemma 3.6 (since $f^{\prime}-1=f$), $T^{w}_{\theta},u^{(\Pi^{\prime},i,f^{\prime})},[x\mapsto(\Lambda,e,f),y\mapsto(\Pi^{\prime},i,f^{\prime})]\models\lambda^{\prime}$ which contradicts ().

Finally, for the case $\forall x\forall y\leavevmode\nobreak\ \varphi$ suppose $M,w\models\forall x\forall y\leavevmode\nobreak\ \varphi$, then for any $(\Gamma,e,f),\leavevmode\nobreak\ (\Delta,e^{\prime},f^{\prime})\in\delta^{w}_{\theta}(w)$ we claim that $T^{w}_{\theta},w,[x\mapsto(\Gamma,e,f),y\mapsto(\Delta,e^{\prime},f^{\prime})]\models\varphi$ (else again, go to the smallest module and prove contradiction).

Note that in the type based model, at any world $w$ we have $|\delta^{w}_{\theta}|=2^{2^{O(|\textsf{SF}(\theta)|)}}$. Now if we start with a $\mathsf{PTML}^{2}$ formula $\varphi$, then though its corresponding equi-satisfiable formula $\theta$ is exponentially larger, the number of distinct subformulas in $\theta$ is still linear in the size of $\varphi$.

Corollary 3.10**.**

$\mathsf{TML}^{2}$* satisfiability is in 2-EXPSPACE.*

Proof 3.11**.**

Any $\mathsf{TML}^{2}$ formula $\alpha$ is satisfiable iff (by Lemma.2.8) its corresponding $\mathsf{PTML}^{2}$ translation $\varphi$ is satisfiable iff (by Theorem 3.8) the corresponding normal form $\theta$ of $\varphi$ is satisfiable over agent set $D$ of size $2^{2^{O(|\varphi|)}}$ iff (by Lemma. 2.5) $\hat{\theta}\in\mathsf{PTML}^{2}$ is satisfiable in a constant domain model over $D$.

Thus we can expand the quantifiers of $\hat{\theta}$ by corresponding $\bigwedge$ and $\bigvee$ for $\forall$ and $\exists$ respectively and we get a propositional multi-modal formula. This satisfiability is in PSPACE. But in terms of the size of the formulas, $|\hat{\theta}|=2^{2^{|\alpha|^{2}}}$. Thus we have a 2-EXPSPACE algorithm.

3.3 Example

We illustrate the construction of type based models with an example. Consider the $\mathsf{PTML}^{2}$ sentence $\theta:=\forall x\leavevmode\nobreak\ \Box_{x}\Box_{x}\bot\land\forall x\exists y\leavevmode\nobreak\ (\Box_{x}(\Diamond_{y}(\neg p)\land\exists y\leavevmode\nobreak\ \Diamond_{y}p))$ which is in $\textsf{FSNF}\leavevmode\nobreak\ \mathsf{DNF}$. Let $M$ be the model described in Fig. 1 where

• •

$W=\{r\}\cup\{u^{i},v^{i},w^{i}\mid i\in\mathcal{N}\}$

• •

$D=\mathcal{N}$

• •

$\delta(r)=\{2i\mid i\in\mathcal{N}\}$ (all even numbers) and

$\delta(w^{i})=\delta(u^{i})=\delta(v^{i})=\mathcal{N}$

• •

$R=\{(r,2i,w^{i}),(w^{i},2i+1,u^{i}),(w^{i},2i+2,v^{i})\mid i\in\mathcal{N}\}$

• •

$\rho(r)=\rho(w^{i})=\rho(v^{i})=\emptyset$ and $\rho(u^{i})=p$ for all $i\in\mathcal{N}$.

Clearly, $M,r\models\theta$. Let $f^{r}:D_{r}\mapsto D_{r}$ be defined by $f^{r}(2i)=2i+2$ and at all $w^{i}$, $g^{i}(j)=2i+1$ for all $i\in\mathcal{N}$ be the two (relevant) witness functions. The one and two types at every world are described as follows:

At leaf nodes $u^{i}$ and $v^{i}$ there is only one distinct one type and two types. At $w^{i}$, note that $r\xrightarrow{2i}w_{i}$ is the incoming edge and only $2i+1$ and $2i+2$ have outgoing edges. Thus, there are $3$ distinct 1-type members at $w^{i}$, each for $(2i+1),(2i+2)$ and [the rest]. Let $b,c,d$ be the respective types. Finally at the root again we have only a single distinct type (call it $a$).

Since there are $2$ existential formulas, the root of the type based model has $(1\times 2\times 3)=6$ agents let it be $\{a^{e}_{f}\mid 1\leq e\leq 2,\leavevmode\nobreak\ 0\leq f\leq 2\}$ and [math] be the representative. At $w^{0}$ we have $(3\times 2\times 3)=18$ agents. Let the representatives be $1,2,0$ for $b,c,d$ respectively. Note that we cannot pick any other representative for [the rest] other than [math] since [math] is the incoming edge to $w^{0}$. Let the bounded agent set be $\{b^{e}_{f},\leavevmode\nobreak\ c^{e}_{f},\leavevmode\nobreak\ d^{e}_{f}\mid 1\leq e\leq 2,\leavevmode\nobreak\ 0\leq f\leq 2\}$. The corresponding bounded model $M^{\prime}$ is described in Figure 2. It can be verified that $M^{\prime},r\models\theta$.

4 Discussion

We have proved that the two variable fragment of $\mathsf{PTML}^{2}$ (and hence $\mathsf{TML}^{2}$) is decidable. The upper bound shown is in 2-EXPSPACE. A NEXPTIME lower bound follows since $\mathsf{FO}^{2}$ satisfiability can be reduced to $\mathsf{PTML}^{2}$ satisfiability. We believe that by careful management of the normal form, space can be reused and the upper bound can in fact be brought down by one exponent. That would still leave a significant gap between lower and upper bounds to be addressed in future work.

We can also prove that addition of constants makes $\mathsf{PTML}^{2}$ undecidable. In fact, with the addition of a single constant $\mathbf{c}$ we can use $\Box_{\mathbf{c}}$ to simulate the ‘free’ $\Box$ of $\mathsf{FOML}^{2}$, thus yielding undecidability. When it comes to equality, the situation is more tricky: note that we can no longer use model extension (Def.3.5 and Lemma 3.6) since equality might restrict the number of agents at every world.

The most important issue is expressiveness. What kind of accessibility relations or model classes can be characterized by 2-variable $\mathsf{TML}$? This is unclear, but there are sufficiently intriguing examples and applications making the issue an interesting challenge.