Tero Tulenheimo
email: tero.tulenheimo@univ-lille3.fr

Insights into Modal Slash Logic and Modal Decidability *

Keywords: complementation, decidability, expressivity, IF logic, independence, modal logic, slash logic

. We push the study of this logic deeper at several points: a model-theoretic criterion is presented which serves to tell when a formula of MsL0 is not truth-equivalent to any formula of basic modal logic (ML); the game-theoretic property of 'bounded quasi-positionality' of MsL0 is studied in detail; an alternative syntax for MsL0 is discerned and the logic obtained is shown to enjoy the property of quasi-locality (generalizing the notion of locality familiar from ML); and we formulate an asymmetric bisimulation concept and use it to prove that MsL0 is not closed under complementation. Drawing from insights provided by the study of MsL0, we conclude by general observations about claims made on the 'reasons' why various modal logics are computationally well-behaved.

Introduction

Independence-friendly (IF) first-order logic [START_REF] Hintikka | Informational independence as a semantical phenomenon[END_REF][START_REF] Hintikka | Principles of Mathematics Revisited[END_REF] results from first-order logic by dissociating the notions of syntactic and semantic scope in the following sense: formulas of IF first-order logic are like those of first-order logic, except that in place of plain existential quantifiers, expressions of the form (∃x/∀y 1 , . . . , ∀y n ) may appear in a sentence φ, provided that in φ this expression is syntactically subordinate to (in the syntactic scope of) each of the universal quantifiers ∀y 1 , . . . , ∀y n . The semantic effect of such independence indications '/∀y 1 , . . . , ∀y n ' is taken to be that in order for φ to be true, the witness of ∃x may not depend on the values corresponding to the universal quantifiers ∀y 1 , . . . , ∀y n , that is, this value must be provided by a (Skolem) function not having the values chosen for those quantifiers among its arguments. Thereby ∀x(∃y/∀x)Rxy is true iff ∃y∀xRxy is true, and ∀x∀y(∃z/∀y)(∃v/∀x)Sxyzv is true iff the Henkin-quantifier sentence ∀x ∃z ∀x ∃v Sxyzv is true. Expressed in terms of two-player evaluation games among players E and A, the truth of an IF first-order sentence, hence defined, amounts to the existence of a winning strategy for E in the correlated evaluation game -supposing that strategy functions of a given player only take as arguments moves made by his or her adversary. However, this is not how strategies are typically understood in game theory: generally a strategy for a player in a two-player game can perfectly well make use of the previous choices of either player, his or her own ones included. [START_REF] Hodges | Logics of Imperfect Information: Why Sets of Assignments?[END_REF] points out that in the literature some authors discussing IF first-order logic have opted for formulating the semantics as Hintikka does while others have utilized strategy functions in the standard game-theoretic sense in their semantics. Hodges (1997a) had adopted the notational convention of writing (∃x/y) where Hintikka writes (∃x/∀y), hence marking the difference between semantic games formulated in terms of arbitrary strategy functions and those whose strategy functions are in effect Skolem functions. The variable y in (∃x/y) might in Hodges's syntax be 'bound' even by a syntactically precedent existential quantifier, whereas such independence of existential quantifiers cannot be syntactically marked in Hintikka's formulation. Hodges (2007, p. 119) writes:

[W]e refer to the logic with my notation and the general game semantics as slash logic. During recent years many writers in this area (but never Hintikka himself) have transferred the name 'IF logic' to slash logic, often without realising the difference. Until the terminology settles down, we have to beware of examples and proofs that don't make clear which semantics they intend.

The terminology has not shown much tendency of settling down; for instance the recent monograph by [START_REF] Mann | Independence-Friendly Logic: A Game-Theoretic Approach[END_REF] discusses in fact first-order slash logic but calls its object of study nevertheless Independence friendly first-order logic.

In the present paper we discuss a modal-like logic which in fact relates to first-order slash logic (FOsL) in the same way as basic modal logic (ML) relates to first-order logic (FOL): just like ML can be translated into FOL, also our modal-like logic -to be referred to as modal slash logic (MsL) -semantically corresponds to a certain fragment of FOsL, as will be explained in Section 3. Different variants of modal slash logic can be discerned by restricting, or liberalizing, the sorts of independence indications allowed; see [START_REF] Tulenheimo | On IF modal logic and its expressive power[END_REF][START_REF] Tulenheimo | Independence-Friendly Modal Logic: Studies in its Expressive Power and Theoretical Relevance[END_REF][START_REF] Hyttinen | Decidability of IF modal logic of perfect recall[END_REF][START_REF] Tulenheimo | On modal logic, IF logic and IF modal logic[END_REF][START_REF] Sevenster | Branches of Imperfect Information[END_REF][START_REF] Tulenheimo | Approaches to independence friendly modal logic[END_REF][START_REF] Tulenheimo | Equivalence criteria for compositional IF modal logics[END_REF][START_REF] Tulenheimo | Hybrid logic meets IF modal logic[END_REF][START_REF] Sevenster | Decidability of Independence Friendly Modal Logic[END_REF]. The first formulation of a logic termed 'IF modal logic' was due to [START_REF] Bradfield | Independence-friendly modal logic and true concurrency[END_REF], who developed further the framework of Bradfield's Henkin modal logic [START_REF] Bradfield | Independence: logics and concurrency[END_REF]. The key idea in their research was to use the analysis of quantifier independence in studying transition systems with concurrency; for comparison it should be noted that the semantics of MsL is relative to standard modal structures (Kripke models). Recently Väänänen has considered accommodating the framework of his dependence logic [START_REF] Väänänen | Dependence Logic: A New Approach to Independence Friendly Logic[END_REF] to the case of modal logic, cf. [START_REF] Väänänen | Modal Dependence Logic[END_REF][START_REF] Sevenster | Model-Theoretic and Computational Properties of Modal Dependence Logic[END_REF]. The logics emerging from the works of Bradfield and Väänänen are not studied in the present paper.

Basic definitions

We need to lay down some definitions.

1.1.1. Logics. Throughout the paper, prop will be a fixed countably infinite set of propositional atoms, denoted p, q, r etc. The syntax of basic modal logic (or ML) is generated by the grammar φ ::

= ⊤ | ⊥ | p | ∼p | (φ ∨ φ) | (φ ∧ φ) | φ | φ,
where p ∈ prop. The semantics of ML is defined relative to models and their states, i.e., tuples M = (M, R, V ) and elements w ∈ M , where M is a non-empty domain, R is a binary relation on M termed accessibility relation, and V : prop → Pow (M ) is a valuation function. If M is a model and w ∈ M , (M, w) is a pointed model. We assume the reader is familiar with the relation M, w |= φ, or truth of an ML formula φ in M at w; see, e.g., (Blackburn et al., 2002, Def. 1.20). The symbols ⊤ and ⊥ stand for verum and falsum, respectively: they have a fixed semantics, with M, w |= ⊤ and M, w |= ⊥ for all pointed models (M, w). The modal depth of an ML formula φ is the maximum number of nested modal operator tokens in φ.

Fix a vocabulary τ (i.e., a countable set of constant, relation, and function symbols). We write FOL[τ ] for first-order logic of vocabulary τ ; ESO[τ ] stands for existential second-order logic of vocabulary τ , and FOsL[τ ] is first-order slash logic of vocabulary τ . Formulas of ESO[τ ] are strings ∃f 1 . . . ∃f n φ, where the f i are function symbols and φ is an FOL formula of vocabulary τ ∪ {f 1 , . . . , f n }. The syntax of FOsL[τ ] is Tero Tulenheimo produced by the grammar φ ::= α | (φ ∨ φ) | (φ ∧ φ) | ∀xφ | (∃x/W )φ, where α is an atomic or negated atomic formula of FOL[τ ] and W ∪ {x} is a finite set of variables, with x / ∈ W . We agree to write ∃x for (∃x/∅). If x 1 , . . . , x n are pairwise distinct variables, we allow writing (∃x/x 1 , . . . , x n ) for (∃x/{x 1 , . . . , x n }). Expressions produced by the grammar are termed FOsL[τ ] strings. We may wish to distinguish two kinds of free variables in an FOsL string φ: those appearing in atomic formulas (Free 1 [φ]) and those appearing independence indications (Free 2 [φ]). The former sets are recursively defined as in the case of first-order logic, the independence indications playing no role. To define the latter sets, put Free 2 [(∃x/W )φ] = W ∪ (Free

2 [φ] \ {x}), Free 2 [∀xφ] = Free 2 [φ], Free 2 [φ ⋆ ψ] = Free 2 [φ] ∪ Free 2 [ψ]
for junctions ⋆, and Free 2 [α] = ∅ for (negated) atoms α. A string φ is a formula if the set Free 2 [φ] is empty. If even the union Free 1 [φ]∪Free 2 [φ] is empty, φ is a sentence. For example, ∃x∃y(∃z/x)Rxyz is a sentence (and a fortiori a formula). The string ∃x(∃z/x)Rxyz is not a sentence but is a formula. And ∃y(∃z/x)Syz not even a formula. In the present paper we will assume, for simplicity, that in an FOsL string there will never appear two quantifiers carrying the same variable so that one would be syntactically subordinate to the other: hence, e.g., ∀x∃y∀x(∃z/x)Rxyz is not a string. Thanks to this stipulation, if (∃x/W ) appears in a formula, the variables in the set W refer to uniquely determined syntactically preceding quantifiers. To simplify further, we also suppose that if a variable belongs to Free 1 [φ], then no quantifier carrying this variable occurs in φ. The notion of syntactic tree is defined in the expected way for all logics discussed in the present paper: the nodes of a syntactic tree of φ are the operator tokens and tokens of atomic formulas occurring in φ, and they are ordered by the relation of syntactic precedence given by the syntax of the logic in question.

To distinguish τ -structures from modal structures, we use calligraphic symbols such as M and N for the former. If M is such a structure, M stands for its domain. For the semantics of ESO[τ ], see e.g. [START_REF] Ebbinghaus | Finite Model Theory[END_REF][START_REF] Väänänen | Dependence Logic: A New Approach to Independence Friendly Logic[END_REF]. As to FOsL[τ ], given any FOsL[τ ] formula φ with Free 1 [φ] = {x 1 , . . . , x k }, τ -structure M, and a variable assignment x i → c i , there will be an evaluation game G(φ, M, c 1 • • • c k ) between two players, A and E. There are two kinds of moves: model moves (an element of M is chosen) and junction moves (a term 0 or 1 of a junction is chosen). The positions in the game are triples ( a, i, ψ), where a is a tuple keeping track of model moves made in the course of a play, i being a tuple keeping track of junction moves made in the course of a play. The initial position of the game is (c 1 • • • c k , ∅, φ). If a position ( a, i, ψ) has been reached, the continuation of the play depends on the form of ψ. If ψ = (χ 0 ∨ χ 1 ), player E selects j ∈ {0, 1} and the play continues with the position ( a, ij, χ j ). It is the player A who chooses if ψ = (χ 0 ∧ χ 1 ). If, again, ψ = (∃x/W )χ, player E selects b ∈ M and the play continues with the position ( ab, i, χ); note that the rule in no way utilizes the independence indication. If ψ = ∀xχ, player A selects an element b ∈ M . Finally, if ψ is (negated) atomic, E wins and A loses if ψ is satisfied in M by the variable assignment induced by the tuple a, else the players receive the reversed payoffs. Note that indeed we may think of a as a variable assignment: thanks to our syntactic assumptions, the same variable is never re-interpreted in the course of a play, and therefore the tuples a and i together uniquely determine an assignment of type Free 1 [ψ] → M from the input formula φ. We could have avoided encoding information about the junction moves in the description of positions, provided that we would have considered the formulas mentioned in positions as formula tokens. It serves clarity, however, to explicitly list the junction moves made, since a tuple of junction moves together with a formula type uniquely determines which formula token is meant.

Consider the positions ( a, i, (∃x/W )ψ) and ( b, i, (∃x/W )ψ) of one and the same game; note that necessarily the tuples a and b are of the same length. We say that these positions are W-equivalent, given that the following holds: whenever a i = b i , then a i and b i are both model moves made for some quantifier Qy with y ∈ W . A strategy of player E in game G(φ, M) is uniform if for any W -equivalent positions ( a, i, (∃x/W )ψ) and ( b, i, (∃x/W )ψ), the strategy yields the same move. By definition, an FOsL formula φ is satisfied (dissatisfied) in M under assignment x → c if there is a winning strategy for player E (player A respectively) in game G(φ, M, c). If there is no winning strategy for either player, the formula φ is said to be non-determined in M under the assignment x → c. If φ is a sentence, we say that φ is true (false, non-determined) in M when φ is satisfied (respectively false, nondetermined) in M by ∅. For instance, as the reader may readily check, the sentence ∀x(∃y/x) x = y is neither true nor false in any model of size at least 2. We say that sentences φ and ψ are truth equivalent if they are true in precisely the same structures. Since non-truth does not in general amount to falsity, truth-equivalence does not imply that φ and ψ are also false in precisely the same structures. More generally, if φ and ψ are formulas, it is said that they are satisfaction equivalent if they are satisfied by exactly the same structures and the same suitable variable assignments. For FOsL, see (Hodges, 1997a;[START_REF] Hodges | Logics of Imperfect Information: Why Sets of Assignments?[END_REF] and cf. [START_REF] Väänänen | Dependence Logic: A New Approach to Independence Friendly Logic[END_REF][START_REF] Mann | Independence-Friendly Logic: A Game-Theoretic Approach[END_REF].

Tero Tulenheimo

Model-theoretic notions.

If R is a binary relation, write R + for the transitive closure of R and R * for the reflexive transitive closure of R. A modal structure is treelike if its accessibility relation R satisfies: (i) there is a unique element r ∈ M , the root of the model, such that for all x ∈ M , R * rx; (ii) every element of M distinct from r has a unique R-predecessor; and (iii) R is acyclic, i.e., there is no x such that R + xx. The unraveling of a pointed model (M, R, V, w) is a pointed model (M ′ , R ′ , V ′ , w) such that the domain M ′ = {(x 0 , x 1 , . . . , x n ) ∈ M n+1 : x 0 = w and n < ω and Rx i x i+1 for all 0 ≤ i < n}, the accessibility relation R ′ satisfies (w, x 1 , . . . , x n ), (w, y 1 , . . . , y m ) ∈ R ′ iff (m = n + 1 and x i = y i for all 1 ≤ i ≤ n and Rx n y m ), and the valuation

V ′ satisfies (w, x 1 , . . . , x n ) ∈ V ′ (p) iff x n ∈ V (p)
, for all propositional atoms p. Evidently for any pointed model (M, R, V, w) we have that (M ′ , R ′ , V ′ ) is tree-like and w is its root. (We identify unit tuples and elements.)

Model (N, S, U ) is a submodel of model (M, R, V ) if N ⊆ M , S is a restriction of R to N and U is a restriction of V to N . Further, (N, S, U ) is a generated submodel of (M, R, V ) if it is a submodel of (M, R, V
) and satisfies the following closure condition: if w ∈ N and R(w, v), then v ∈ N . Submodel of (M, R, V ) generated by S ⊆ M is by definition the smallest generated submodel whose domain contains S. The notion of substructure is defined similarly for first-order structures of vocabularies containing only one binary but any number of unary relation symbols. A modal logic L evaluated over pointed models is said to be invariant under generated submodels provided that the following holds: if N is a generated submodel of M, and w ∈ N , then M, w |= ψ iff N, w |= ψ, for all formulas ψ of L. The notion of invariance under generated substructures extends in an obvious way to abstract logics, in particular FOL. Given a pointed model (M, R, V, w), define a partial map h : M ⇀ ω as follows: put h(w) = 0, and if h(u) = n and Ruv and v has not yet been assigned a value, put h(v) = n + 1. This recursive definition assigns a natural number h(v) -the height of v -to every state v in M for which there exists a path from w to v along R. That is, the map h is defined on all and only states in the domain of the submodel of (M, R, V, w) generated by the singleton set {w}. The height of a state v in a tree-like model M equals the height of v in the pointed model (M, w), where w is the root of M. If the set {h(v) : v ∈ M } has a maximum, we say that (M, w) is of finite height and take this quantity to be the height of the pointed model (M, w).

Else (M, w) is said to be of infinite height. If M = (M, R, V ) is tree-like and k < ω, the restriction of M to height k, denoted (M ↾ k), is the model (M ′ , R ′ , V ′ )
, where M ′ consists of the states of M of height at most k, and R ′ (respectively V ′ ) is the restriction of R (respectively V ) to M ′ . If v is a state having a finite number, n, of successors along the accessibility relation, we say that the out-degree of v is n; if the number of successors has no finite bound, the out-degree of v is said to be infinite. 1.1.3. Expressivity and bisimulations. Suppose the semantics of logics L and L ′ are defined relative to pointed models. Logic L is translatable into logic L ′ (in symbols L ≤ L ′ ) if for every φ ∈ L there is ψ φ ∈ L ′ such that for all M and w, we have:

M, w |= φ iff M, w |= ψ φ . And L ′ is strictly more expressive than L (in symbols L < L ′ ) if L ≤ L ′ but L ′ ≤ L.
We say that logic L is closed under complementation -or: closed under contradictory negationif for every formula φ of L there is a formula neg(φ) likewise of L such that for all pointed models (M, w), we have: M, w |= neg(φ) iff M, w |= φ. Pointed models (M, w) and (M ′ , w ′ ) are L equivalent if for every φ ∈ L, the following holds: M, w |= φ iff M ′ , w ′ |= φ. For later purposes we recall the notions of bisimulation and n-bisimulation; for more details, see e.g. (Blackburn et al., 2002, Sect. 2.2)

. Suppose M = (M, R, V ) and M ′ = (M ′ , R ′ , V ′ ) are pointed models, w ∈ M and w ′ ∈ M ′ . A relation Z ⊆ M × M ′
is a bisimulation between the pointed models (M, w) and (M ′ , w ′ ), if the following four conditions hold: (0) Initial coordination: wZw ′ ; (1) Atomic harmony: for all states u and u ′ , if uZu ′ , then for all atoms p ∈ prop we have that u ∈ V (p) iff u ′ ∈ V ′ (p); (2) Zig: for all states u, u ′ and t, if uZu ′ and R(u, t), then there is t ′ such that R ′ (u ′ , t ′ ) and tZt ′ ; (3) Zag: for all states u, u ′ and t ′ , if uZu ′ and R ′ (u ′ , t ′ ), then there is t such that R(u, t) and tZt ′ . It is well known and easy to prove that bisimulations offer a criterion for ML equivalence. Indeed, if there is bisimulation between (M, w) and (M ′ , w ′ ), then these pointed models are ML equivalent, i.e., they cannot be distinguished by any ML formula. A sequence Z 0 ⊇ . . . ⊇ Z n of relations with Z i ⊆ M × M ′ is an n-bisimulation between (M, w) and (M ′ , w ′ ) if we have: (0) Initial coordination: wZ n w ′ ; (1) Atomic harmony: for all states u and u ′ , if uZ 0 u ′ , then for all atoms p ∈ prop we have that u ∈ V (p) iff u ′ ∈ V ′ (p); (2) Zig: for all i < n and for all states u, u ′ and t, if uZ i+1 u ′ and R(u, t), then there is t ′ such that R ′ (u ′ , t ′ ) and tZ i t ′ ; (3) Zag: for all i < n and for all states u, u ′ and t ′ , if uZ i+1 u ′ and R ′ (u ′ , t ′ ), then there is t such that R(u, t) and tZ i t ′ . Using n-bisimulations a criterion for ML equivalence of pointed models up to a modal depth is obtained: if there is an n-bisimulation between (M, w) and (M ′ , w ′ ), these pointed models cannot be distinguished by any ML formula of modal depth at most n.

Plan of the paper

Section 2.1 introduces modal slash logic (MsL); the expressive power of this logic is discussed in Section 3. In Section 4 we discern a fragment of MsL, to be denoted MsL 0 , and formulate a criterion which serves to tell when a formula of MsL 0 is not truth-equivalent to any formula of basic modal logic (ML). In Section 5 the game-theoretic property of 'bounded quasi-positionality' of MsL 0 is studied in detail. An alternative syntax for MsL 0 is presented in Section 6; the logic obtained is shown to enjoy the property of quasi-locality which is a generalization of the notion of locality familiar from ML. In Section 7 modal slash logic is compared for its expressive power with first-order logic, finite-variable fragments of first-order logic and loosely guarded fragment of first-order logic. Section 8 introduces the notion of breadth of an MsL 0 formula; and it is shown that while the number of non-equivalent MsL 0 formulas of a fixed modal depth is infinite, the number of non-equivalent MsL 0 formulas of a fixed modal depth and a fixed breadth is finite. We define an asymmetric bisimulation concept in Section 9 and employ this notion to prove that MsL 0 is not closed under complementation. Section 10 closes the paper by making some general observations about claims made in the literature on the 'reasons' why various modal logics are computationally well-behaved.

The logic MsL

We begin by defining modal slash logic (MsL). It is a syntactic extension of basic modal logic (ML). As a matter of fact, MsL is strictly more expressive than ML.

Syntax of MsL

We need to choose a syntax suitable for indicating the sorts of independence relations we are interested in. Having fixed a set prop of propositional atoms, we take as our point of departure basic modal logic in negation normal form (or ML): its formulas are obtained from literals (i.e., formulas of the forms p and ∼p with p ∈ prop) by finitely many applications of the unary operators , and the binary operators ∧, ∨. We wish to study constraints on finding a witness when interested in the truth of formulas. This leads us, for reasons that will become clear in the sequel, to allow slashed diamonds in the syntax of modal slash logic. By means of a syntactic slashing device ( / . . .) we will be able to mark diamonds as independent of a selection of syntactically preceding boxes and diamonds (referred to by suitable identifiers written in place of the dots). What this means is that syntactic scope and semantic scope are dissociated: here 'independent of' means 'not in the semantic scope of.' Generalizations of this syntax could be considered, where not only diamonds but also boxes and even conjunction and disjunction symbols could be slashed. These further options will not be explored in the present paper.

In first-order slash logic independence indications are expressed using variables with the aid of suitable further stipulations. If an existential quantifier ∃y is followed by the independence indication '/x,' its witness must not depend on the closest syntactically precedent quantifier carrying the variable x. (In fact, thanks to our stipulations concerning the syntax, there cannot be more than one quantifier token with the variable x preceding a given quantifier ∃y.) Since the syntax of modal logic involves no variables, here we may not use anything like variables to mark independence relations. Several choices are conceivable, one of which would be to employ explicit indexing of tokens of modal operators within a formula (for example by numerals standing for natural numbers) and using those indices in independence indications. This would lead to formulas such as 1 2 ( 3 /2)p. Since the use of indices would mark a difference compared with ML (whose formulas do not carry indexed modal operator tokens), we allow as the only difference between the syntaxes of ML and MsL that diamonds may carry independence indications of the form '/i 1 , . . . , i k ,' where the i j are pairwise distinct positive integers. Semantically these numbers are construed as relative de Bruijn indices (to be explained in Definition 2.1); they identify those syntactically preceding modal operator tokens of which the relevant diamond symbol is declared to be independent. For example, we will have formulas such as ( /1)p and (p ∨ ( /1, 2)q).

In the first formula, the numeral '1' refers back to the box token which is the immediate syntactic predecessor of the unique diamond symbol.

In the second formula, the numeral '1' serves to identify the diamond symbol in whose syntactic scope we find (p ∨ ( /1, 2)q), while the numeral '2' refers back to the unique box token in the formula. The syntax of MsL -or modal slash logic -is obtained from that of ML by the following rules:

1. If φ ∈ ML and φ ′ results from replacing in φ all tokens of by the symbol ( /∅), then φ ′ is a formula.

2. If φ is a formula, i 1 , . . . , i k is a non-empty strictly increasing tuple of (numerals standing for) positive integers, and α is a token of ( /∅) that lies in φ in the syntactic scope of at least max{i 1 , . . . , i k } = i k modal operators, then the result of replacing α in φ by the symbol ( /i 1 , . . . , i k ) is also a formula.

According to the above syntax, all diamond tokens in MsL formulas are of the form ( /i 1 , . . . , i k ) for some tuple i 1 , . . . , i k . If k = 0, the tuple is empty. We abbreviate diamond tokens ( /∅) by . We observe that on the basis of this notational convention, all ML formulas are, syntactically, MsL formulas. Examples of further formulas are ( /1)p and ( /1, 2)q, as well as (( /1)p ∨ ( /2)q), ( /1)( /1)p and ( /1)( /3)p.

By contrast, the strings ( /5, 27)p and ( /1)q cannot be produced by the above rules. In the former case this is because there are fewer than 27 modal operator tokens syntactically preceding the diamond symbol in the string ( /5, 27)p; and in the latter case because the syntax does not allow slashing boxes.

As already hinted at, the numerals i 1 , . . . , i k appearing in independence indications '/i 1 , . . . , i k ' are interpreted as referring to certain preceding modal operator tokens. The semantics will impose as a condition for finding a witness for the diamond token ( /i 1 , . . . , i k ) that the witness must not depend on the values chosen for the operators to which the numerals i 1 , . . . , i k refer. In order to specify which preceding operator is identified by which numeral, we adopt the convention of interpreting them as de Bruijn indices. DEFINITION 2.1 (Relative de Bruijn index). Let α and β be modal operator tokens appearing in a given MsL formula. We say that β immediately precedes α if β syntactically precedes α and in the relevant formula there is no modal operator token that syntactically precedes α but is syntactically preceded by β. If β immediately precedes α, de Bruijn index of β relative to α is 1. And if de Bruijn index of β relative to α is n and γ immediately precedes β, de Bruijn index of γ relative to α is n + 1.

For instance, the unique box token in (( /1)p ∨ ( /1, 2)q) has de Bruijn index 1 relative to ( /1), which is why the numeral '1' in ( /1) by definition refers to that box token. The very same box token has de Bruijn index 2 relative to ( /1, 2). As this example illustrates, in distinct slashed diamond tokens distinct numerals may refer to the same preceding modal operator token. The numeral '1' in ( /1, 2) refers to the diamond token immediately preceding ( /1, 2). By the syntax, for any modal operator token ( /i 1 , . . . , i k ) appearing in an MsL formula, there are in that formula preceding modal operator tokens to which the numerals i 1 , . . . , i k refer.

Semantics of MsL

The semantics of MsL -like that of ML -is defined relative to models and their states. For later purposes we adopt the following convention: if M = (M, R, V ) is a model with prop = {p 1 , p 2 , . . .}, then M is the corresponding first-order structure, i.e., the structure (M, R M , P M 1 , P M 2 , . . .), with R M = R and

P M i = V (p i ). EXAMPLE 2.2.
On what condition should the formula ( /1)p be true in model M at state w? Recalling that the independence indication '/1' is to express that in order for the formula to be true, it must be possible to select a witness for independently of the state chosen to interpret , we see that ( /1)p is true in M at w iff (1) the basic modal formula p is true in M at w, and

(2) the witness of in p can be chosen uniformly with respect to the state interpreting .

To illustrate, consider two pointed models (M, a) and (M ′ , a ′ ) which both satisfy condition (1), i.e., render p true:

a ′ b ′ 1 [ [ c ′ 2 C C p c ′ 1 [ [ b ′ 2 C C [ [ c ′ 3 C C a b 1 Z Z c 2 C C c 1 p [ [ b 2 D D [ [ c 3 p C C M M ′
The former fails to satisfy the additional condition (2). For, when p is being evaluated on (M, a), the possible states interpreting are b 1 and b 2 . In the former case the accessible states are c 1 and c 2 , in the latter c 2 and c 3 . If the witness for is to be chosen uniformly, it must be a state accessible both from b 1 and from b 2 and so it must actually be c 2 . But if it is also to render the atom p true, it must be either c 1 or c 3 . Since no state satisfies both conditions, the formula ( /1)p is not true in M at a. On the other hand, this formula is true in M ′ at a ′ . Here the diamond token may be witnessed by the state c ′ 2 , which renders the atom p true. Indeed, the formula ( /1)p claims of its state of evaluation w that there exists a state u that is a common successor to all states v accessible from w, and that u makes p true.

For every triple (φ, M, w), where φ is an MsL formula and (M, w) is a pointed model, we associate a game between two players, E and A, denoted G(φ, M, w). Player A will make choices corresponding to tokens of and ∧ -operators with universal force 1 -while E will make choices corresponding to the tokens of and ∨ -operators with existential force. In order to get an idea of how such games are played, let us take examples of games played relative to the pointed model (M, a) of Example 2.2. EXAMPLE 2.3. Let us begin by considering an ML formula. How is the game for the formula p played on (M, a)? A 'terminal play' (a, x, y) consists of some state x accessible from state a, chosen by A corresponding to , followed by some state y accessible from state x, chosen by E and corresponding to . E wins the play if the state y makes the atom p true, otherwise A wins. There are four possible terminal plays: (a, b 1 , c 1 ) and (a, b 1 , c 2 ) and (a, b 2 , c 2 ) and (a, b 2 , c 3 ). There exists a winning strategy for player

E: choose c 1 if A chose b 1 , and choose c 3 if A chose b 2 .
What about the game played on the same pointed model but with the MsL formula ( /1)p? The set of possible terminal plays is the same as in the case of the ML formula p. Also the winning conditions for terminal plays are the same. The difference is that here a restriction is imposed on available winning strategies: a strategy is winning for player E only if it is uniform in the sense of assigning the same state to ( /1) regardless of the state chosen for . No uniform winning strategy exists: the only strategy which yields corresponding to ( /1) a state that is available at both states b 1 and b 2 consists of choosing the state c 2 in both cases. But p is false at c 2 .

We introduce the set of positions of game G(φ, M, w) by laying down the relevant game rules. At each position at most one player has to make a move. Depending on the position, he or she must either make a model move or a junction move. In the former case the player must choose from the domain a state meeting a certain additional condition. In the latter case the choice is syntactic: one of the terms of a junction is chosen. Sequences of positions generated according to the game rules are plays. Plays that cannot be further extended are called terminal plays. For terminal plays we define conditions under which a player comes out as the winner. By stipulation G(φ, M, w) is a zero-sum game: who does not win, loses. DEFINITION 2.4 (Positions). The positions of game G(φ, M, w) are generated thus:

1 Recall that the negation sign may only appear before an atom.

Insights into Modal Slash Logic and Modal Decidability

13

• The initial position is (φ, ∅, w).

• If the position ((ψ ∨ χ), b, a) has been reached, also (ψ, b0, a) and (χ, b1, a) are positions.2 Player E chooses one of them.

• If the position ((ψ ∧ χ), b, a) has been reached, also (ψ, b0, a) and (χ, b1, a) are positions. Player A chooses one of them. • If ℓ is a literal and the position (ℓ, b, a) has been reached, then E wins the play that led to this position if ℓ is true at a according to the valuation function of the model, else A wins.

A position encodes the information about which subformula token has been reached, as well as what the most recent model move has been. Observe that the independence indications play no role whatsoever in the clause for strings of the form ( /i 1 , . . . , i k )ψ: the rule for the slashed diamond is perfectly symmetric to that of the box. The independence indications will have an effect elsewhere: they regulate winning strategies available to player E. For future use, we stipulate that substrings of formula φ are those expressions that appear as leftmost components of a position of a game G(φ, M, w). We call a string of symbols an MsL string if it is a substring of some MsL formula. Not all MsL strings are MsL formulas; e.g., ( /27)q is not one. If (ψ, b, a) is a position, the pair (ψ, b) identifies a specific token of the substring type ψ; indeed the rationale for including the binary tuples b in the positions is precisely to keep track of substring tokens (which is important, as we will see, in MsL). The third component of a position (ψ, b, a) is either a state belonging to the domain of the relevant model or the symbol fail.

Let us move on to define the notion of strategy and explain what it takes for a strategy to be 'uniform' and 'winning.' DEFINITION 2.5 (Strategy, extension of a strategy). If φ ∈ MsL and α 1 , . . . , α n is a list of all diamond and disjunction tokens appearing in Tero Tulenheimo φ, a strategy of player E in game G(φ, M, w) is a tuple (f 1 , . . . , f n ) of functions, called strategy functions. For each i and every position at which a move corresponding to α i must be made, the strategy function f i provides a move that respects the game rules, depending on the previous moves made in the play leading to that position. (Additional requirements imposed on a strategy may, in general, cancel out some of those dependencies; the uniformity requirement discussed below is a case in point.)

By fixing a strategy f , player E leaves open certain plays and excludes others: precisely those are left open that player A can realize by making suitable moves, given that E follows the strategy f . Call the set of plays left open by the choice of f the extension of f , denoted Ext(f ).

We generalize the notion of strategy as follows. If

(f i 1 , . . . , f i k ) is the restriction of a strategy f = (f 1 , . . . , f n ) to the set Ext(f ) -that is, if (f i 1 , . . . , f i k )
is the list of all functions among f 1 , . . . , f n whose all arguments are plays in Ext(f ) -then also the tuple

(f i 1 , . . . , f i k ) is a strategy.
We note that a strategy f in the narrower sense may include strategy functions that never need be used, since the plays in which they would be used lie outside the extension of f . This is what motivates the more general notion of strategy.

Strategy functions are functions that map non-terminal plays to positions. Often it will be more convenient to consider functions which take simply tuples of states as their arguments and which return as values states (case of boxes and diamonds) or objects encoding junction moves (case of junctions). We recall that 0 encodes the choice of the left term of a junction and 1 the choice of its right term. From a suitable function of the latter type it will be straightforward to define a strategy function proper. When no confusion threatens, we will simply take the latter types of functions to be strategy functions.

A strategy f of player E is uniform, if for every diamond token ( /i 1 , . . . , i k ) in φ, the strategy satisfies the following: whenever two plays that belong to the extension of f lead to a position where a move for this token must be made, and those plays differ at most in the choices made for the preceding modal operator tokens identified by the numerals i 1 , . . . , i k , then the strategy yields the same choice in both cases. For instance, E's strategy f in the game associated with ( /1)p, played relative to the state w, is uniform if there is a state u such that f yields the choice u for ( /1) no matter which state v accessible from w is chosen by player A for .

In order for a strategy of player E to be winning, it must satisfy: (1) all terminal plays in the extension of f are won by E, and (2) f is uniform. The notion of winning strategy of player A is otherwise similar but involves no requirement of uniformity. This is because the syntax precludes boxes with independence indications. DEFINITION 2.6 (Truth,falsity). Let φ be an MsL formula. We say that φ is true in M at w, if there exists a winning strategy for E in game G(φ, M, w). And we say that φ is false in M at w, if there exists a winning strategy for A in game G(φ, M, w). We write M, w |= φ to indicate that φ is true in M at w.

As the following example illustrates, the formula φ and the pointed model (M, w) can be so chosen that there exists no winning strategy for either player in game G(φ, M, w), i.e., the game is non-determined in the sense of game theory. In such a case we will derivatively say that φ is non-determined in M at w. Observe that the non-determinacy of a formula in M at w amounts to its being neither true nor false in M at w, given that 'true' and 'false' are understood in the sense of Definition 2.6. It follows from the existence of such formulas that the non-truth of a formula in a pointed model does not guarantee its falsity therein. EXAMPLE 2.7. Let us return to the formula φ := ( /1)p and the pointed model (M, a) of Example 2.3. We already saw that φ is not true in M at a. We will establish that it is not false in M at state a either. Note that there are exactly two possible strategies for A in the game G(φ, M, a), namely choosing b 1 or choosing b 2 to interpret the box. In the former case E may choose c 1 and win, while in the latter case she may choose c 3 and win. Therefore no strategy of A is winning and φ is not false in M at a. We note that since there are formulas non-determined in some pointed models, truth-equivalence of φ and ψ does not in general guarantee that these formulas are also false in precisely the same models: there can be models in which one is false and the other is nondeterminate. Let us take still further examples of evaluating MsL formulas. These examples will utilize the models M 1 and M 2 :

w v 1 X X v 2 F F u 2 M M u 3 Q Q u 1 V V u 4 H H x 1 O O x 3 O O x 2 q J J T T M 1 w v 1 Y Y u 1 u 2 p p v 4 E E v 3 K K v 2 S S T TM M J J Q Q M 2
EXAMPLE 2.8. Consider evaluating the formula ( /1, 2)q in the model M 1 at state w. Let us first note that the following pair f := (f 1 , f 2 ) yields a strategy for E in the relevant game, leading against both possible moves by A to a terminal play won by E:

-f 1 (v 1 ) = u 2 and f 1 (v 2 ) = u 3 . -f 2 (v 1 , u 2 ) = x 2 = f 1 (v 2 , u 3 ).
The functions f 1 and f 2 provide moves that indeed are available according to the game rules, and both terminal plays in the extension of the strategy f are won by E. Second, we may observe that this strategy is uniform: the plays in the extension of f at which a choice for ( /1, 2) is made are (w, v 1 , u 2 ) and (w, v 2 , u 3 ), and the strategy f indeed maps them both to the same state, viz. x 2 . We may conclude that M 1 , w |= ( /1, 2)q.

EXAMPLE 2.9. Consider the model M 2 depicted above. Obviously the formula ( /1)p considered in Examples 2.3 and 2.7 is not true in M 2 at w: that would require that there be a common successor to all the states v 1 , v 2 , v 3 , v 4 making p true, and this is not the case. However -and here we see a rather unusual feature of MsL -the formula (( /1)p∨( /1)p) is true in M 2 at w: replacing the string ( /1)p by the string (( /1)p∨( /1)p) produces a true formula out of a non-true one. Let us see what is behind this phenomenon.

Here is a winning strategy f := (f 1 , f 2 , f 3 ) for E in the game corresponding to the latter formula, played on the pointed model (M 2 , w).

-

f 1 (w, v 1 ) = 0 = f 1 (w, v 2 ) and f 1 (w, v 3 ) = 1 = f 1 (w, v 4 ) -f 2 (w, v 1 , 0) = u 1 = f 2 (w, v 2 , 0) -f 3 (w, v 3 , 1) = u 2 = f 3 (w, v 4 , 1).
Not only do the functions f 1 , f 2 and f 3 yield a strategy for E such that all plays in its extension are won by E, but also the strategy is uniform. For, consider the plays in the extension of f at which a move must be made corresponding to the leftmost token of ( /1), i.e., the plays (w, v 1 , 0) and (w, v 2 , 0). Evidently f maps these plays to the same state, viz. u 1 . Similarly, the plays (w, v 3 , 1) and (w, v 4 , 1) in the extension of f at which a move is to be made for the rightmost token of ( /1) are likewise mapped to the same state, that is, to u 2 . When player E is making her move for the slashed diamond, she is so to say aware of which one of the two tokens of the slashed diamond she is reacting to, and nothing prevents her from acting differently in the two cases. Considering the totality of the plays, using her preceding disjunctive choice, E has been able to partition the set of immediate successors of the state w in two pieces: those states associated with 0 and those associated with 1. When it is E's turn to move for a diamond token, she only needs to be able to provide a common successor to those states which have been associated with the same number, 0 or 1.

Example 2.9 shows that if α is a substring of an MsL formula, substituting (α ∨ α) for α in that formula is not in general a truthvalue preserving operation. However, it is not difficult to see that the phenomenon may only occur if α is not an MsL formula, i.e., only if α is a substring of a formula which cannot itself be produced by the syntax of MsL.

The expressivity of MsL

Many properties of MsL are known from the literature. Since we will be interested in a fragment of MsL -the logic MsL 0 to be introduced in Section 4 -and as we wish to contrast this fragment with various logics, among them the logic MsL itself, it is in order to register here some of these properties, notably those concerning to the relative expressive power of MsL.

FACT 3.1 [START_REF] Tulenheimo | On IF modal logic and its expressive power[END_REF]. MsL is more expressive than ML.

Proof. First, ML is a syntactic fragment of MsL and so the gametheoretic semantics of MsL yields in particular a certain truth condition for each formula of ML. Assuming the Axiom of Choice, the standard semantics of ML and its game-theoretic semantics coincide. The assumption is needed in the direction from the ML semantics to the game-theoretical semantics on models having states with an infinite out-degree: the truth of φ in the standard sense only guarantees the existence of a non-deterministic strategy in the corresponding game, and for the possibility of turning a non-determinisitc strategy into a deterministic one (as required by the MsL semantics), we need the Axiom of Choice. 3 We conclude that ML ≤ MsL. In order to see that MsL ≤ ML, consider the pointed models (M, a) and (M ′ , a ′ ) of Example 2.2. They are plainly bisimilar and therefore ML equivalent. Yet, as noted in Example 2.2, we have M, a |= ( /1)p but M ′ , a ′ |= ( /1)p.

Tero Tulenheimo

It is well-known that ML enjoys the tree-model property: every satisfiable ML formula is true at the root of a tree-like model. The logic MsL, again, lacks this property. FACT 3.2. MsL does not have the tree-model property.

Proof. Consider the MsL formula φ := (( p ∧ ∼p) ∧ ( /1)⊤). It is satisfiable: e.g., the pointed model (M, a) makes it true:

a b 1 p Z Z c D D b 2 ∼p D D Z Z M
No pointed model (N, v) making φ true is tree-like: the out-degree of v is at least 2 and the successors of v have a common successor.

Just like there exists a well-known straightforward translation of ML into FOL -for this so-called standard translation, see e.g. (Blackburn et al., 2002, Def. 2.45) -there exists a straightforward translation of MsL into FOsL. The following examples suffice for seeing how the translation works.

MsL formula its standard translation

( /1)p ∀x(Rx 0 x → (∃y/x)(Rxy ∧ Py)) (( /1)q ∨ ( /1)q) ∀x(Rx 0 x → ((∃y/x)(Rxy ∧ Qy) ∨ (∃z/x)(Rxz ∧ Qz))) ( /1)( /1, 3)p ∀x(Rx 0 x → ∀y(Rxy → (∃z/y)(Ryz ∧ (∃v/x, z)(Rzv ∧ Pv))))
For every φ ∈ MsL, let ST x 0 (φ) be its standard translation in FOsL obtained in this way, with x 0 as its sole free variable. By the semantics of the two logics, it is evident that M, w |= φ iff M, w |= ST x 0 (φ). FACT 3.3. MsL ≤ ESO. That is, for every φ ∈ MsL there is an ESO formula ψ φ (x) of one free variable such that for every pointed model (M, w), the following holds:

M, w |= φ iff M, w |= ψ φ .
Proof. It is well known that FOsL ≤ ESO; cf., e.g., (Väänänen, 2007, Subsect. 6.1). Since MsL ≤ FOsL, the statement follows.

It is quite obvious that Fact 3.3 can be improved: MsL < ESO. Actually already for the fragment FOL of ESO we have that FOL ≤ MsL. We will obtain a strict proof of this fact in Section 9 (Corollary 9.8).

Alternatively, this could be proven for example by observing that MsL, like ML, is invariant under generated submodels whereas FOL is not.

Basic modal logic is translatable into FOL. Could we perhaps improve Fact 3.3 to the point of showing that actually MsL is translatable already into FOL? The answer is in the negative. PROPOSITION 3.4 [START_REF] Tulenheimo | Approaches to independence friendly modal logic[END_REF]. MsL ≤ FOL.

The idea of proof used in [START_REF] Tulenheimo | Approaches to independence friendly modal logic[END_REF] was as follows. A certain MsL formula χ and a family {(M n , a) : n ≥ 2} of pointed models were discerned. Then it was shown (1) that M n , a |= χ iff n is even, and (2) that for every n ≥ 0 there is a number k n ≥ 2 such that the structures (M kn , a) and (M kn+1 , a) are elementarily equivalent up to quantifier rank n. It then follows that χ has no translation into FOL. For suppose it had one, say φ χ (x), and let r be the quantifier rank of φ χ (x). Then (M kr , a) and (M kr+1 , a) would be elementarily equivalent up to quantifier rank r and in particular not distinguished by φ χ (x). But exactly one of the numbers k r and k r + 1 is even, so (M kr , a) and (M kr+1 , a) are distinguished by χ. Therefore (M kr , a) and (M kr+1 , a) are distinguished by the translation φ χ (x) of χ. This is a contradiction. In the proof χ was chosen to be the MsL formula

( ( /1)( /1, 3)⊤ ∨ ( /1)( /1, 3)⊤).
The following result concerning contradictory negation follows from Proposition 3.4. In Section 9 this negative result will be improved. COROLLARY 3.5. MsL is not closed under contradictory negation. That is, it is not the case that for every φ ∈ MsL there is ψ φ ∈ MsL such that for all pointed models (M, w), we have:

M, w |= ψ φ iff M, w |= φ.
Proof. It is well known that contradictory negation is inexpressible in ESO in the following strong sense: if ξ and ζ are two ESO formulas such that for all models M and all variable assignments γ, we have M, γ |= ξ iff M, γ |= ζ, then actually each of ξ and ζ is logically equivalent to an FOL formula; for a proof, see e.g. (Barwise, 1979, pp. 56, 73-74). Now, the MsL formula χ used in the proof of Proposition 3.4 can be translated into ESO but not into FOL. By the fact just mentioned, its contradictory negation has no translation into ESO, and so a fortiori not into MsL.

Tero Tulenheimo

The fragment MsL 0

We discern a certain simple fragment of MsL, to be dubbed MsL 0 . The syntax of MsL 0 is obtained from that of MsL by allowing only formulas containing diamond symbols of the forms ( /∅) or ( /1), where '1' identifies a syntactically preceding box token. Accordingly, for example ( /1)p and (p ∨ ( ( /1)q ∧ ( /1)r)) are formulas, while ( /1)p and ( /1, 2)q are not. The logic MsL 0 is a notational variant of the logic L SD that was formulated and studied in [START_REF] Tulenheimo | On modal logic, IF logic and IF modal logic[END_REF].

In the present and the five following sections we study the expressive power of MsL 0 . In particular, we obtain a model-theoretic criterion for telling when an MsL 0 formula cannot be translated into basic modal logic (the present section); we offer a normal form result for E's winning straregies in MsL 0 games (Section 5); we prove that the semantics of MsL 0 is 'quasi-local' in a sense to be specified (Section 6); we will see that MsL 0 is translatable into FOL but neither to any finite variable fragment of FOL nor to the loosely guarded fragment of FOL (Section 7); it is observed that up to truth-equivalence there are infinitely many MsL 0 formulas of a given modal depth, but only finitely many MsL 0 formulas with a fixed modal depth and a fixed so-called breadth (Section 8); finally, we show that -in a very strong sense -MsL 0 fails to be closed under contradictory negation (Section 9).

Syntax recursively defined

Consider the following grammars A (the former) and B (the latter); note that A is defined with reference to B:4

α ::= p | ∼p | (α ∨ α) | (α ∧ α) | α | α | β β ::= ( /1)α | (α ⋆ β) | (β ⋆ α) | (β ⋆ β),
with ⋆ ∈ {∨, ∧} and p ∈ prop. The formulas of MsL 0 are recursively generated -as a moment's reflection reveals -by the grammar A. The strings (sequences of symbols) generated by the grammar B are not formulas of MsL. However, they are available as building blocks when producing formulas. Indeed, they are substrings of formulas in the sense explained in Section 2.2. Note that for any string β there is a tuple (s 1 , . . . , s n+1 ) of terms such that β is obtained from those terms -using them, say, in the order from s 1 up to s n+1 -by n applications of ∧ and ∨, each term s i being either an MsL 0 formula or a string of the form ( /1)α, where α is an MsL 0 formula. We say that terms of the former kind are formula terms and those of the latter kind non-formula terms. For later purposes, let us introduce the syntactic notions of degree and breadth of a formula. DEFINITION 4.1 (Degree, breadth). If β is a string produced by the grammar B, its degree, denoted deg(β), is the number of its nonformula terms. In other words, deg(β) is the number of those tokens of the symbol ( /1) in β that are not syntactically subordinate to a token of in β. Given a formula φ of MsL 0 , let S φ be the set of its subformulas (subformula types) generated by the grammar B. By definition, the breadth of φ, denoted bre(φ), equals max{deg(β) : β ∈ S φ }.

We will call diamond symbols basic diamonds and diamond symbols ( /1) slashed diamonds. When reasoning about E's strategies in MsL 0 games, we will make use of the following further definitions. DEFINITION 4.2 (Contextual vs. basic disjunction tokens). Suppose φ ∈ MsL 0 . If (χ 1 ∨ χ 2 ) is a substring of φ and both of its terms χ 1 and χ 2 are formulas, then the token of ∨ is basic. If, again, at least one of its terms is a non-formula, the token of ∨ is contextual. That is, the token of ∨ is contextual if there is in (χ 1 ∨ χ 2 ) a token of slashed diamond not preceded in (χ 1 ∨ χ 2 ) by a box token.

For example, consider the formula (p ∨ ((q ∨ (r ∧ ( /1)p ′ )) ∧ (q ′ ∨ r ′ ))). Counting from left to right, the first token of ∨ is basic: p and ((q ∨ (r ∧ ( /1)p ′ )) ∧ (q ′ ∨ r ′ )) are formulas. Also the third token of ∨ is basic: q ′ and r ′ are formulas. However, the second token is contextual: the substring (r ∧ ( /1)p ′ ) is not a formula.

Criterion for non-properness

A formula of MsL 0 is proper if it is not truth-equivalent to any ML formula. We establish a model-theoretic criterion enabling us to tell when a formula is not proper. This result will be of use in Section 9. DEFINITION 4.4 (Global duplication). Let (M, w) be a pointed treelike model of finite height. Write n for its height.

(a) Let I be any subset of M . For each i ∈ I, fix a set K i of indices; the set K i may have any cardinality. For every i ∈ I, suppose that J i = {(M i j , w i j ) : j ∈ K i } is a set of pointed tree-like models having no states in common with M and having pairwise disjoint domains. Write F for the family {J i : i ∈ I}. We define the sum of (M, w) and the family F, denoted (M, w) I F, to be the treelike model whose root is w, whose domain is M ∪ i∈I j∈K i M i j , whose accessibility relation is R ∪ i∈I j∈J i R i j ∪ {(i, w i j ) : j ∈ K i and i ∈ I} and whose valuation assigns to every atom p the set

V (p) ∪ i∈I j∈J i V i j (p).
(b) Let 0 ≤ m < n and let L m be the set of states of M of layer m (i.e., the set of states of height m). For every state v in L m and every R-successor u of v, let (M v,u , u ′ ) be an isomorphic copy of the submodel of M generated by u, having no nodes in common with M. Write J v for the set {(M v,u , u ′ ) : R(v, u)} and F for the family {J v : v ∈ L m }. By definition the duplication of M at layer m equals (M, w) Lm F. (There is nothing to duplicate at layer n -leaves have no successors -hence we only consider values of m smaller than n.) (c) Let S 0 be the duplication of (M, w) at layer 0. Further, if 1 ≤ r < n -1, then let S r+1 be the duplication of S r at layer r + 1. By definition the global duplication of (M, w) equals S n-1 .

Let (N, w) be the global duplication of a tree-like pointed model (M, w) of finite height, and let R be the accessibility relation of N. Suppose u is an R-successor of v. Then, due to the way in which N was constructed, there is a state u ′ with u = u ′ such that R(v, u ′ ) and the submodel of N generated by u is isomorphic to the submodel of N generated by u ′ . Further, suppose K is a class of pointed models closed under global duplications. Let k be any positive integer. If (M, w) ∈ K is tree-like and of finite height, there is a pointed model (N, w) ∈ K with the following property: if v and u are states in N , u accessible from v, there are 2 k -1 further states in N , likewise accessible from v, such that the submodel of N generated by any of these 2 k -1 states is isomorphic to the submodel generated by u. Such a pointed model -to be termed the k-fold duplication of (M, w) -is obtained by applying k times successively the operation of global duplication starting from (M, w).

To facilitate discussion, we stipulate that if a pointed model of finite height is not tree-like, it is its own global duplication. In this way the operation of global duplication is defined for all pointed models of finite height. We write Mod (φ) for the class of all pointed models in which φ is true and the height of which is at most md (φ). Nothing of interest is left outside the class Mod (φ): the class of all pointed models of φ is evidently the class of those pointed models whose restriction to height md (φ) belongs to Mod (φ). The n-unraveling of a pointed model is the restriction of its unraveling to height n. Proof. Let k be a positive integer such that 2 k ≥ bre(φ)+1. Suppose Mod (φ) is closed under md (φ)-unraveling and global duplication. If Mod (φ) is empty, trivially φ is not proper. So suppose there is a pointed model (M, w) in Mod (φ). By assumption the md (φ)-unraveling (M ′ , w) of (M, w) belongs to Mod (φ) as well. Now, the md (φ)-unraveling is of finite height, so there is in Mod (φ) also the k-fold duplication (N, w) of (M ′ , w).

Let f be E's winning strategy in game G(φ, N, w). Since φ is a formula of MsL 0 , whenever a position of the form (( /1)ψ, c, a) occurs in a play of this game, its recollection ( β, d, b) occurs in that play as well. Without loss of generality, we may assume that the strategy f avoids positions (( /1)ψ, c, a) whenever possible. What this means can be explained in other words as follows: if the strategy nevertheless leads to such a position against some sequence of moves by A, then all formula terms χ of the corresponding Boolean combination β are nontrue at a. Now, given that f is a winning strategy and avoids positions of the form (( /1)ψ, c, a) whenever possible, it actually follows that no position of the form (( /1)ψ, c, a) is reached in the first place. In order to prove this we make essential use of the fact that (N, w) is a k-fold duplication of a tree-like pointed model of φ.

Suppose for contradiction that following f against some sequence of moves by A leads to a position (( /1)ψ 0 , c 0 , a 0 ). If ( β, d, b) is the recollection of the token of ( /1), we know that no formula term of β is true at a 0 . By the construction of N, there are at least bre(φ) further states a 1 , . . . , a bre(φ) , all accessible from b, such that each of them generates a submodel of N isomorphic to the submodel of N generated by a 0 . Due to isomorphism, we may conclude that no formula term of β is true at any of those further states either. Therefore, the winning strategy f must lead against any moves by A to such disjunctive choices that for each of those further states a i , a position (( /1)ψ i , c i , a i ) is reached, where ( /1)ψ i is a non-formula term of β. Since there are at most bre(φ) such non-formula terms to assign to the bre(φ) + 1 states a 0 , a 1 , . . . , a bre(φ) , one of those non-formula terms must be utilized twice. That is, there are i and j with a i = a j such that ψ i = ψ j (meaning that ψ i and ψ j are the same string token). Since f is a winning strategy, it will map a i and a j to their common successor. But N is tree-like, so no two states a i , a j with R(b, a i ) and R(b, a j ) have a common successor. This is a contradiction. We have just shown that no winning strategy of E in game G(φ, N, w) will yield any position of the form (( /1)ψ, c, a). Now, let φ ′ be the formula obtained from φ by replacing by ⊥ its all substrings of the form ( /1)ψ which do not lie in φ in the syntactic scope of a further diamond symbol ( /1). Note that by syntactic criteria, φ ′ is a formula of ML. It remains to show that φ and φ ′ are truth-equivalent. Trivially, whenever φ ′ is true in M at w, also φ is true in M at w. Namely, the formula φ ′ determines a certain subtree of the syntactic tree of φ. The existence of a winning strategy for E corresponding to φ ′ guarantees that she can remain within that subtree when playing the game corresponding to φ. For any sequence of moves by A in game G(φ, M, w), player E may respond by the move that her winning strategy yields for the same sequence of moves in game G(φ ′ , M, w); in this way E will in particular never end up in a position involving a slashed diamond in game G(φ, M, w). In order to see that conversely, the truth of φ in M at w suffices for the truth of φ ′ in M at w, we may reason as follows. Suppose M, w |= φ. Construct from M a model N as above. Given that Mod (φ) is closed under md (φ)-unraveling and global duplication, we have N, w |= φ. Since E's winning strategy in G(φ, N, w) does not yield any positions of the form (( /1)ψ, c, a), evidently φ ′ is true in N at w. Now, observe that (M, w) and (N, w) are md (φ)-bisimilar. Since md (φ ′ ) ≤ md (φ), we may conclude that φ ′ is true in M at w.

MsL 0 and bounded quasi-positionality

We will next prove a result which serves to deepen our understanding of the semantics of MsL 0 . We show that the value of a winning strategy for player E at a given play only depends on certain earlier positions -in fact it depends on at most two earlier positions. In what follows, if π and σ are any sequences, π ⌢ σ stands for the sequence obtained by concatenating π and σ (in this order). We need to agree on some further terminology. DEFINITION 5.1 (Bounded quasi-positionality). Let φ ∈ MsL 0 and let α be a diamond or disjunction token in φ. (b) A sequence of strategy functions (in particular, an entire strategy) of player E has bounded quasi-positionality if its strategy functions for basic diamonds and basic disjunctions are positional, its strategy functions for slashed diamonds are quasi-positional, and its strategy functions for contextual disjunctions have bounded quasi-positionality.

(c) Derivatively, a fragment L of MsL 0 is said to have bounded quasipositionality, if the following condition holds: for all formulas φ ∈ L and pointed models (M, w), if there exists a winning strategy for E in G(φ, M, w), then in this game there exists a winning strategy for E which has bounded quasi-positionality.

As the following example illustrates, in MsL 0 we cannot generally hope that the value of a winning strategy for E on a play would depend only on one single model move therein. EXAMPLE 5.2. Consider the MsL 0 formula φ := (( /1)p ∨ ( /1) ∼p) and the model M depicted below.

w v 1 ] ] v 2 A A u 4 A A ] ] u 6 A A u 7 7 7 u 5 O O u 2 ] ] u 1 g g u 3 O O t 3 p t 2 ∼p t 4 ∼p t 1 p X X H H F F V V J J V V H H T T M (1)
We note that M, w |= φ. Indeed, define the functions f , g and h as follows:

f (v 1 , u 1 ) = f (v 1 , u 2 ) = f (v 2 , u 4 ) = f (v 2 , u 5 ) = 0, f (v 1 , u 3 ) = f (v 1 , u 4 ) = f (v 2 , u 6 ) = f (v 2 , u 7 ) = 1, g(v 1 ) = t 1 , g(v 2 ) = t 3 , h(v 1 ) = t 2 , h(v 2 ) = t 4 .
The functions f , g and h induce strategy functions for the disjunction, the left slashed diamond and the right slashed diamond, respectively; obviously these strategy functions constitute a winning strategy for E in game G(φ, M, w). We note that the function f yielding the strategy function for the disjunction uses two arguments.

(2) We proceed to prove that if d is a strategy function for the disjunction in G(φ, M, w) and the value of d at a play depends (i) only on A's move for the first occurrence of or (ii) only on A's move for the second occurrence of , then d is not E's strategy function for the disjunction in any winning strategy.

Suppose d, g, h are functions inducing a winning strategy for E in G(φ, M, w), with g and h of type {v 1 , v 2 } → {t 1 , t 2 , t 3 , t 4 }, corresponding to the left and the right slashed diamond respectively. Case (i): suppose d is a function of type {v 1 , v 2 } → {0, 1}. If d(v 1 ) = 0, the function g maps in particular both plays (w, v 1 , u 2 ) and (w, v 1 , u 3 ) to the state g(v 1 ). Since g belongs to a winning strategy, the state g(v 1 ) is accessible from u 2 and from u 3 , which is impossible. Similar reasoning applies if d(v 1 ) = 1, this time using the function h. Case (ii): suppose d is a function of type {u 1 , . . . , u 7 } → {0, 1}, i.e., suppose d is positional. Suppose d(u 4 ) = 0. Since g yields a strategy function for the left slashed diamond and g belongs to a winning strategy, g must map each of the plays (w, v 1 , u 4 ) and (w, v 2 , u 4 ) to a state at which p is true -not because of the uniformity requirement, but because the state chosen must make p true. Hence in fact g(v 1 ) = t 3 = g(v 2 ). Now, the state t 3 is not accessible from any of the states u 1 , u 2 , u 3 , u 6 , u 7 . So d cannot map any of these five states to 0. Thus, in particular d(u 1 ) = d(u 3 ) = 1. But then h maps both of the plays (w, v 1 , u 1 ) and (w, v 1 , u 3 ) to the state h(v 1 ). Since h yields a strategy function for the right slashed diamond and h belongs to a winning strategy, h(v 1 ) is accessible from both u 1 and u 3 , which is impossible as the two states do not have a common successor. Similar reasoning applies if d(u 4 ) = 1. We conclude that any strategy function for the disjunction in φ belonging to a winning strategy must be a function of two arguments.

Directly by the definition of bounded quasi-positionality, we have: FACT 5.3. Let φ, ψ ∈ MsL 0 and suppose f is a winning strategy for player E in game G(φ, M, w) such that f has bounded quasi-positionality. If the position (ψ, c, v) appears in a play belonging to the extension of f , then there is a winning strategy for E in game G(ψ, M, v), in fact a winning strategy having bounded quasi-positionality.

We prove that the whole MsL 0 has bounded quasi-positionality in the sense of Definition 5.1(c). By Example 5.2 this is an optimal result: we could not always find a winning strategy whose all strategy functions are functions of one argument only. For a less transparent proof of a more general result, see [START_REF] Tulenheimo | Hybrid logic meets IF modal logic[END_REF], Appendix §3, Lemma 3. THEOREM 5.4. MsL 0 has bounded quasi-positionality.

Proof. Suppose there is a winning strategy for E in game G(φ, M, w), call it f . We will define a certain function g and show that it is a winning strategy for E in G(φ, M, w) with bounded quasi-positionality.

Let Π be the set of all plays of G(φ, M, w) at which it is E's turn to move. Before doing anything else, with each play π in Π we associate a tuple P π of moves in π as follows. (Depending on how the last position of π looks like, this tuple will contain either one or two members.) Suppose the last position of π is (ψ, c, a).

-If ψ = χ, or ψ = (χ 1 ∨ χ 2 ) with ∨ basic, then P π := (a).

-If ψ = ( /1)χ and b is the recollection state of this token of ( /1), then P π := (b).

-If ψ = (χ 1 ∨ χ 2 ), with ∨ contextual, and b is the recollection of this token of ∨, then P π := (b, a).

Then define an equivalence relation ≈ on Π by setting π ≈ π ′ iff (π and π ′ are of the same length, involve the same junction moves, and satisfy P π = P π ′ ). With these definitions at our disposal, let us proceed to define the function g. We wish to define g in such a way that whenever σ, σ ′ ∈ Ext(g) and σ ≈ σ ′ , there is a play π ∈ Ext(f

) with σ ≈ π ≈ σ ′ such that g(σ) = f (π) = g(σ ′
). We must of course check that a play π ∈ Ext(f ) with σ ≈ π ≈ σ ′ can always be found. We define g together with an auxiliary function h : Ext(g) ∩ Π → Ext(f ) which indeed provides such a play: for any σ on which h is defined, σ ≈ h(σ) and h(σ) = h(σ ′ ) for any σ ≈ σ ′ . Once the function g with the desired properties is defined, we show that it is actually a winning strategy for E; its quasi-positionality follows automatically from its definition. First, if S ∈ Π/≈ and all plays in S contain only moves by A, select arbitrarily a play π ∈ S and set h(σ) := π for all σ ∈ S. Trivially π belongs to the extension of f . Define g(σ

) := (f • h)(σ), for all σ ∈ S. Next suppose σ = τ ⌢ g(τ ) ⌢ ρ
is a play in the set Π and constructed using g, where ρ contains only moves by A and there is π ∈ Ext(f ) such that for all τ ′ constructed using g and satisfying τ ′ ≈ τ , we have: τ ′ ≈ π and h(τ ′ ) = π and g(τ ′ ) = (f • h)(τ ′ ). We wish to find π 0 ∈ Ext(f ) such that for all plays Tero Tulenheimo σ ′ constructed using g with σ ′ ≈ σ, we have π 0 ≈ σ ′ . Once such a play is found we define h(σ ′ ) := π 0 and we set g(σ ′ ) := (f • h)(σ ′ ) for all σ ′ constructed using g with σ ′ ≈ σ. We will consider cases according to the form of the string ψ at the last position (ψ, c, a) of the sequence g(τ ) ⌢ ρ. (Note that ρ may be empty.) Now, by assumption τ ≈ h(τ

). Since h(τ ) is in Ext(f ), also h(τ ) ⌢ (f • h)(τ ) ⌢ ρ = h(τ ) ⌢ g(τ ) ⌢ ρ is in Ext(f ). Write π * := h(τ ) ⌢ g(τ ) ⌢ ρ.
We will show that actually σ ≈ π * .

1. The case ψ := χ or ψ := (χ 1 ∨ χ 2 ) with basic ∨: Since the plays σ and π * share their last member, we have that σ ≈ π * .

2. The case: ψ := ( /1)χ. We consider two subcases according to whether the recollection of the slashed diamond token occurs in the sequence τ or in the sequence g(τ Let us now proceed to show that the function g is a winning strategy for player E. First we observe that for every play σ ∈ Π on which g is defined, the move g(σ) respects the game rules, i.e., the sequence σ ⌢ g(σ) is a play. In the case that the last position of σ carries a disjunction (whether basic or contextual) this is trivial, and in the case its last position carries a diamond (whether basic or slashed) this follows immediately from the definition of g. Second, if τ ⌢ g(τ ) ⌢ ρ is a terminal play in the extension of g, where ρ contains only moves by A,

) ⌢ ρ. (2.1) If it occurs in the sequence g(τ ) ⌢ ρ, then it is immediate σ ≈ π * . (2.2) If,

Insights into Modal Slash Logic and Modal Decidability

29

this play is won by E because the play h(τ ) ⌢ g(τ ) ⌢ ρ in the extension of f is won by E (the condition of winning depends only on the last position of a terminal play). Third, we note that g respects the required uniformity conditions. Actually, if σ ≈ σ, the function g agrees on these plays. This is more than enough for respecting the corresponding uniformity constraint: the latter would allow the value of the strategy on σ to depend on any model move preceding the earliest model move on which the value of g on σ depends. (That is, the choice made for basic and contextual disjunctions and basic diamonds could depend on any earlier moves, and the choice made for slashed diamonds could depend, in addition to its recollection, on any model move preceding the recollection.)

Let us still introduce some more terminology.

DEFINITION 5.5 (Forwards-looking truth-condition). Let φ be a formula of MsL (not necessarily a formula of MsL 0 ).

(1) Suppose f is a strategy for E in game G(φ, M, w) and S is a set of positions at which it is E's turn to move and which appear in the extension of f . We say the set S is forwards-looking for f provided that we have: if σ := π ⌢ (ψ, c, v) ⌢ ρ is any play in Ext(f ) on which f is defined and for which (ψ, c, v) ∈ S, the value of f on σ does not depend on any position in π.

(2) We say that φ has a strongly (respectively, weakly) forwards-looking truth-condition, if for all M and w ∈ M , the following holds: if M, w |= φ, there exists a winning strategy g for E in G(φ, M, w) such that the set P M,w g (respectively S M,w g

) is forwards-looking for g, where P M,w g is the set of all positions in Ext(g) at which it is E's turn to move, and S M,w g is the subset of P M,w g consisting of positions (ψ, c, v) in which ψ is a formula (and not merely a substring).

OBSERVATION 5.6. By Theorem 5.4, all formulas of MsL 0 have a weakly forwards-looking truth-condition, though not in general a strongly forwards-looking one. The formulas of ML indeed have a strongly forwards-looking truth-condition.

When discussing the possibility for a language to have a compositional semantics, Hintikka has stressed the property of semantic contextindependence: semantic attributes of a complex expression depend only on the semantic attributes of its constituent expressions, plus its structure -not on the sentential context in which the expression is embedded [START_REF] Hintikka | The Game of Language: Studies in Game-Theoretical Semantics and Its Applications[END_REF][START_REF] Hintikka | Principles of Mathematics Revisited[END_REF]. As subsequent work Tero Tulenheimo by Hodges in effect highlights, a language -Hodges discusses precisely first-order slash logic -may enjoy semantic context-independence relative to one type of semantic attribute while failing to enjoy this property relative to another type of semantic attribute. He (Hodges, 1997a;Hodges, 1997b) showed that first-order slash logic actually does admit of a compositional semantics, given that formulas are evaluated relative to sets of variable assignments, instead of being evaluated relative to one assignment only. On the other hand, Cameron and Hodges (2001, Cor. 6.2) proved that no 'Tarskian' compositional semantics exists for first-order slash logic, interpreting a string φ(x) by a subset of M n for some n < ω rather than by a subset of Pow (M ). That is, any compositional semantics of first-order slash logic is bound to employ sets of assignments rather than single assignments. Hintikka used to take it for granted that context-independence unavoidably fails for first-order slash logic (IF first-order logic). This is, then, correct if attention is confined to the semantic attribute satisfaction under an assignment, but not if the attribute satisfaction under a set of assignments is considered. Even without resorting to the non-trivial result of Cameron and Hodges, it is plain that at least there is no obvious way in which the semantics of expressions such as (∃x/∀y)φ could have a context-independent semantics in the 'Tarskian' sense. Actually, from the viewpoint of game-theoretical semantics, such strings do not by themselves have any satisfaction conditions at all, so in particular not satisfaction conditions that could be used for determining whether a larger formula is satisfied. For a discussion on compositionality and first-order slash logic (IF first-order logic), see [START_REF] Sandu | Aspects of compositionality[END_REF].

In connection with the semantic attribute of truth, the above notion of strongly forwards-looking truth-condition provides a formulation of the notion of semantic context-independence utilizing the notion of strategy. The fact that MsL 0 formulas have a weakly forwards-looking truth-condition suggests that through a suitable syntactic reformulation we might be able to turn MsL 0 into an equivalent language whose formulas have a strongly forwards-looking truth-condition and indeed manifest semantic context-independence. Such a language will actually be generated by the grammar C, which we now move on to introduce.

Grammar C and the quasi-locality of the semantics

Grammar C

Let us take another look at strings β generated by the grammar B introduced in Subsection 4.1. There are n 2 • (n -1)! trees with n nodes of out-degree 2, the rest being of out-degree 0, such that every node of out-degree 2 is labeled either with ∨ or with ∧. We may call such trees binary syntactic structures of size n. In such a tree the number of leaves is n + 1. We may take the nodes to be binary strings, the root of the tree being the empty string and the successors of a node b of outdegree 2 being b0 and b1. The leaves may be enumerated by stipulating that b 1 precedes b 2 iff in the first position in which these strings differ, b 1 carries 0 while b 2 carries 1. Binary syntactic structures of size n can be understood as (n + 1)-ary connectives. When such a connective C n is applied to a tuple of n + 1 syntactic objects ξ 1 , . . . , ξ n+1 , the result is one syntactic object, namely the binary syntactic structure of size n whose leaf ℓ i is labeled with ξ i for every 1 ≤ i ≤ n + 1. We may write C n (ξ 1 , . . . , ξ n+1 ) for the resulting syntactic object. If for example ξ 1 , ξ 2 , ξ 3 , ξ 4 are formulas of propositional logic and C 3 is a binary syntactic structure of size 3, then C 3 (ξ 1 , ξ 2 , ξ 3 , ξ 4 ) is the syntactic tree of a formula of propositional logic obtained from ξ 1 , ξ 2 , ξ 3 , ξ 4 by exactly 3 applications of connectives from the set {∨, ∧}. Now, for every string β produced by grammar B there is a positive interger n, a set S ⊆ {1, . . . , n + 1} and a binary syntactic structure C n,S of size n such that C n,S (ξ 1 , . . . , ξ n+1 ) is the syntactic tree of β, given that for all 1 ≤ i ≤ n + 1, we have: ξ i ∈ MsL 0 if i / ∈ S, while ξ i is a string of the form ( /1)φ i with φ i ∈ MsL 0 if i ∈ S.

If φ 1 , . . . , φ n+1 are formulas of MsL 0 , define D n,S (φ 1 , . . . , φ n+1 ) := C n,S (ξ 1 , . . . , ξ n+1 ), where ξ i := φ i if i / ∈ S and ξ i := ( /1)φ i if i ∈ S. For example, D 2,{1,3} (p, q, r) = C 2,{1,3} (( /1)p, q, ( /1)r). That is, D n,S is a binary syntactic structure of size n which, when applied to an (n + 1)-tuple of MsL 0 formulas, returns a syntactic tree whose leaves with an order position in S are labeled with strings of the form ( /1)φ, while leaves having their order position outside S are labeled with MsL 0 formulas. Labeled trees such as those denoted by expressions D n,S (φ 1 , . . . , φ n+1 ) can be identified with the corresponding MsL 0 strings. Let us define E n,S (φ 1 , . . . , φ n+1 ) := D n,S (φ 1 , . . . , φ n+1 ). Any MsL 0 formula of the form β, with β generated by grammar B, has as its notational variant an expression of the form E n,S (φ 1 , . . . , φ n+1 ), the φ i being MsL 0 formulas. The following grammar C yields an alternative notation for the syntax of MsL 0 :

φ ::= p | ∼p | (φ ∨ φ) | (φ ∧ φ) | φ | φ | E n,S (φ 1 , . . . , φ n+1 ).
Here p ∈ prop and E n,S = D n,S , with D n,S a binary syntactic structure of size n for some n ≥ 1 and S ⊆ {1, . . . , n+1}. The notion of immediate subformula of a formula generated by the grammar C is defined in the obvious way. Syntactically formulas generated by C can be considered in their own right, but at the same time they serve as a metalogical notation denoting MsL 0 formulas. Continuing with the above example, the formula E 2,{1,3} (p, q, r) equals by definition D 2,{1,3} (p, q, r) which equals by definition C 2,{1,3} (( /1)p, q, ( /1)r). While the immediate subformulas of E 2,{1,3} (p, q, r) are p, q and r, it stands for an MsL 0 formula which is syntactically composed of expressions not all of which are MsL 0 formulas. In particular the Boolean combination denoted by C 2,{1,3} (( /1)p, q, ( /1)r) is not an MsL 0 formula.

Quasi-locality

Let φ be a formula generated by grammar C. The semantics of φ is said to be quasi-local provided that the following condition holds. If M = (M, R, V ) is any model and w ∈ M , then in order to determine whether φ is true in M at w, it is sufficient to consider the set {x : x = v or R(v, x) or (R • R)(v, x)} of states and to know for every immediate subformula ψ of φ and all states u in that set whether ψ is true in M at u. Quasi-locality amounts to semantic context-independence relative to the semantic attribute of truth at states at most 2 steps away from the current state along the relevant accessibility relation. If it is actually enough to consider the smaller set {x : x = v or R(v, x)} of states, the semantics of φ is local. This is the case with formulas φ of ML. The following result is a consequence of Theorem 5.4. COROLLARY 6.1. The semantics of all formulas generated by grammar C is quasi-local.

Proof. Suppose there is a map F such that for all immediate subformulas ψ of φ and all states u in the set {x :

x = v or R(v, x) or (R • R)(v, x)}, we have F (ψ, u) = 1 if M, u |= ψ
and F (ψ, u) = 0 otherwise. We show that the map F allows us to determine whether M, w |= φ. If (ψ, b, u) is a position of game G(φ, M, w) belonging to the extension of E's strategy g, we say (ψ, b, u) is a g-winning position for E, if player E wins all terminal plays in Ext(g) containing this position. (We note that a strategy f is winning iff the initial position of the game is an f -winning position, but a position may be g-winning without g being a winning strategy.)

Let us consider different cases according to the form of φ. The case of literals is trivial, and so is the case of junctions. If φ := χ, then M, w |= φ iff for some winning strategy g of E in G(φ, M, w) having bounded quasi-positionality we have that for all u with (w, u) ∈ R, the position (χ, ∅, u) is a g-winning position for E iff F (χ, u) = 1 for all u with (w, u) ∈ R. In the first equivalence, the direction from left to right holds by Theorem 5.4, while in the second equivalence, the direction from left to right holds because the truth-condition of φ is weakly forwards-looking and φ is a formula. The case of φ := χ is perfectly analogous. Finally, consider the case φ := E n,S (χ 1 , . . . , χ n+1 ) = D n,S (χ 1 , . . . , χ n+1 ). Recall how the binary syntactic structure D n,S was defined from a certain binary syntactic structure C n,S , the latter being applied to an (n + 1)-tuple of strings such that the strings in places i ∈ S are of the form ( /1)χ i and those in places i / ∈ S are of the form χ i . Write m for the number of conjunction symbols in the binary syntactic structure C n,S . Now, M, w |= φ iff for some winning strategy g of E in G(φ, M, w) having bounded quasi-positionality, there are states t 1 , . . . , t |S| such that for all u with R(v, u) and every tuple c ∈ {0, 1} m of choices for conjunctions, there are choices for disjunctions d such that the substring token χ i corresponding to the tuple b determined by these binary choices c, d satisfies: if i / ∈ S, then (χ i , b, u) is a g-winning position for E -whereas if i ∈ S, we have that R(u, t i ) and (χ i , b, t i ) is a g-winning position for E iff there are states t 1 , . . . , t |S| such that for all u with R(v, u) and every tuple c ∈ {0, 1} m of choices for conjunctions, there are choices for disjunctions d such that the substring token χ i corresponding to these binary choices c, d satisfies: if i / ∈ S, then F (χ i , u) = 1 -whereas if i ∈ S, we have R(u, t i ) and F (χ i , t i ) = 1. Again, Theorem 5.4 grants the left-to-right direction of the first equivalence; in the second equivalence, the direction from left to right uses the fact that the truth-condition of φ is weakly forwards-looking and the χ i are formulas.

Note that Corollary 6.1 is not literally about MsL 0 ; it is about formulas generated by grammar C. Thanks to this result we may, derivatively, say that the semantics of MsL 0 itself is quasi-local. What this really means is that when MsL 0 formulas are suitably syntactically analyzed -when they are considered as generated by grammar C -suitable subformulas can be identified so that in terms of the semantic values of those subformulas (truth or non-truth relative to certain nearby states), the semantic value of a given formula at a given state can be determined. EXAMPLE 7.1. Consider the MsL 0 formula ( /1)p. Its standard translation is θ 1 := ∀x(Rx 0 x → (∃y/x)(Rxy ∧ P y)). This FOsL formula is satisfaction-equivalent to the FOL formula θ 2 := ∃y∀x(Rx 0 x → (Rxy ∧ P y)), obtained from θ 1 by erasing the expression (∃y/x) and placing the quantifier ∃y in front of ∀x.

In order to see that θ 1 and θ 2 are indeed satisfaction-equivalent, suppose first that (f, g) is E's winning strategy in game G(θ 1 , M, w). Then in particular g can be taken to be a function of type M → M which is uniform in its sole argument. If the constant value of g equals c, it is obvious that (f, c) is E's winning strategy in game G(θ 2 , M, w). Conversely, if (f, c) is E's winning strategy in game G(θ 2 , M, w), letting a map g be defined by putting g(a) = c = g(a ′ ) for all a, a ′ ∈ M , we have that (f, g) is E's winning strategy in game G(θ 1 , M, w).

Similarly it is seen that the MsL 0 formula (( /1)p ∨ ( /1)p) admits of an FOL translation: its standard translation ∀x(Rx 0 x → ((∃y/x)(Rxy ∧ P y) ∨ (∃z/x)(Rxz ∧ P z)) is satisfaction-equivalent to the FOL formula ∃y∃z∀x(Rx 0 x → ((Rxy ∧ P y) ∨ (Rxz ∧ P z)).

It was proven in [START_REF] Tulenheimo | On modal logic, IF logic and IF modal logic[END_REF]) that MsL 0 is translatable into FOL, by utilizing a suitable skolemization procedure; in the outputs of the procedure all function symbols were nullary, i.e., the outputs were notational variants FOL formulas not using function symbols. We prove the fact here by more direct means. THEOREM 7.2 [START_REF] Tulenheimo | On modal logic, IF logic and IF modal logic[END_REF]. MsL 0 ≤ FOL.

Proof. Let us define a map T x 0 : MsL 0 → FOL recursively, relative to the syntax given by grammar C discerned in Section 6. If y is a variable and the map T x 0 is defined on φ, we write T x 0 /y (ϕ) for the result of having first changed, if necessary, variables in T x 0 (φ) so that in the resulting formula, x 0 does not appear free in the syntactic scope of any quantifier Qy, and having then substituted y for x 0 in that resulting formula. For literals, disjunctions, conjunctions and formulas with the prefix or , let the map T be defined in the same way as the standard translation of basic modal logic. Finally, let

T x 0 [E n,S (φ 1 , . . . , φ n+1 )] := ∃x i 1 . . . ∃x i |S| ∀x(Rx 0 x → C n,S (ξ 1 , . . . , ξ n+1 )),
where ξ j = (Rxx j ∧ T x 0 /x j [φ j ]) if j ∈ S, and ξ j = T x 0 /x [φ j ] if j / ∈ S, given that the map j → i j is an enumeration of the elements of S. We claim: for all MsL 0 formulas φ, models M and states a of M , there is a winning strategy for player

E in game G(φ, M, a) iff M, a |= T x 0 [φ].
The claim holds evidently for literals. It is also clear that it holds for formulas of the forms ∧, ∨, , if it holds for their immediate subformulas. (For reasons mentioned in the proof of Fact 3.1 above, we need to assume the Axiom of Choice in the direction from right to left.) As to the remaining case, let ψ := E n,S (φ 1 , . . . , φ n+1 ). Let (M, a) be an arbitrary pointed model and assume inductively that the claim holds for the formulas φ i . Suppose first that there is a winning strategy f for E in game G(ψ, M, a). The strategy f induces a map ♯ such that for any state b with R(a, b) and any tuple d ∈ {0, 1} m of left/right choices for conjunctions in the tree C n,S , a certain substring token Letting c i with R(b, c i ) be the state that the strategy f yields at the position (( /1)φ i , e, b) of game G(ψ, M, a), we may by Observation 5.6 infer that there is a winning strategy for E in G(φ i , M, c i ) and so by the inductive hypothesis that M, ∈ S, by the inductive hypothesis there is a winning strategy h j for E in game G(ξ j , M, b). If, again, j ∈ S, there is by the inductive hypothesis a winning strategy h j for E in game G(ξ j , M, c j ). Define a strategy g for E in G(ψ, M, a) as follows: if A chooses b for and he produces the string c of conjunctive choices, let E respond in such a way that the string (ξ j , e j ) is reached with j = ♯ (f, d, b). If E arrives at a position (φ j , e j , b) with j / ∈ S, let E continue by applying strategy h j ; if again she arrives at a position (( /1)φ j , e j , b) with j ∈ S, let her pick the state c j and then continue by applying the corresponding strategy h j . Clearly g is winning for E in G(ψ, M, a).

(ζ i , e i ) is determined with i = ♯(f, d, b) and 1 ≤ i ≤ n + 1 such that ζ i = φ i if i / ∈ S and ζ i = ( /1)φ i if i ∈ S. Now, if indeed i / ∈ S, then ζ i is itself a formula of
c i |= T x 0 [φ i ]. It follows that M, a |= T x 0 [ψ], since M, γ |= (Rx 0 x → C n,S (ξ 1 , . . . , ξ n+1 )) with γ(x 0 ) = a and γ(x i ) = c i for i ∈ S.
It was noted in connection with Fact 3.3 that FOL cannot be translated into MsL, though we postponed the proof (we will obtain one via Corollary 9.8). A fortiori, then, FOL cannot be translated into the

Non-translatability into FOL n

It is well known that ML can be translated into the two-variable frament FOL 2 of FOL. Now, MsL 0 can be translated into FOL; does perhaps some finite number of variables suffice for carrying out this translation? As it happens, the answer is in the negative. THEOREM 7.4 [START_REF] Tulenheimo | On modal logic, IF logic and IF modal logic[END_REF]. For all positive integers n, we have:

MsL 0 ≤ FOL n .
Proof. Let m ≥ 2 be arbitrary and write φ m for the formula

(( /1)⊤ ∨ . . . ∨ ( /1)⊤ m-1 times ).
The formula φ m can be translated into FOL m+1 by the formula χ m :=

∃z 1 . . . ∃z m-1 ∀y(Rx 0 y → (Ryz 1 ∨ . . . ∨ Ryz m-1 )). If k ≥ 1, define a structure N k = (N k , R N k ) by putting N k = {w, v 1 . . . , v 2k , u 1 , . . . , u k } and R N k = {(w, v i ) : 1 ≤ i ≤ 2k} ∪ 1≤i≤k {(v i , u i ), (v k+i , u i )}.
The structure N k consists of three mutually disjoint layers: the root w, a layer of 2k elements and a layer of k elements. The second layer can be partitioned into cells of size two such that the elements of each cell have a common successor on the third layer. We observe that N k , w |= φ m iff 1 ≤ k < m. We proceed to prove that χ m is not equivalent to any formula of FOL m . To this end, we claim that the structures (N m-1 , w) and (N m , w) are FOL m equivalent. From this we will be able to conclude that χ m is not equivalent to any formula of FOL m , since N m-1 , w |= χ m but N m , w |= χ m . The proof uses a pebble game argument. For using pebble games G n m (M, a, N, b) to characterize equivalence of structures up to quantifier rank ≤ r relative to FOL r , see, e.g., [START_REF] Ebbinghaus | Finite Model Theory[END_REF][START_REF] Väänänen | A Short Course on Finite Model Theory[END_REF].

The claim follows if we show that there is a winning strategy for Duplicator in the pebble game G m (N m-1 , w, N m , w). Let the relevant m pairs of pebbles be (α 0 , β 0 ), . . . , (α m-1 , β m-1 ), with α 0 placed initially on the root of N m-1 and β 0 on the root of N m . Clearly an optimal strategy for Duplicator would consist of considering successively some m-1 elements of the third layer from N m , say u 1 , . . . , u m-1 , and placing the pebble β i on u i ; Duplicator may respond to these moves by placing the pebble α i on the element u i of N m-1 . Should the players be granted one extra pair of pebbles, (α m , β m ), Spoiler could place β m on the second-layer element v 2m of N m , and to this Duplicator would have no response, since the third layer successor u m of v 2m would have no pebble placed on it, but all third layer elements of N m-1 would already carry a pebble. We conclude that the structures (N m-1 , w) and (N m , w) are FOL m equivalent.

Non-translatability into LGF

Consider the result of translating ML into FOL. In the fragment in question any existential quantifier appears in a context ∃y(Rxy ∧ψ(y)). We may say that the atomic formula Rxy is the guard of the quantifier ∃y. Similarly all universal quantifiers in the fragment are guarded by an atomic formula: they all appear in contexts of the form ∀y(Rxy → ψ(y)). The guards have a double function. On the one hand they render the quantifiers of the relevant fragment relativized: they impose a condition that the value of the quantified variable must satisfy. On the other hand, they dictate a syntactic property that the matrix formula ψ must satisfy: its only free variable y appears free in the guard as well. In the guarded fragment (GF) this setting is generalized. In GF quantifiers may only appear in contexts of the form Q y(G ⋆ ψ), where G is atomic and the free variables of ψ are among those of G. Let τ be a relational vocabulary. The syntax of GF[τ ] is specified by the following grammar:

ψ ::= x 1 = x 2 | R x | ¬ψ | (ψ ∧ ψ) | (ψ ∨ ψ) | Q x(G ⋆ ψ),
where R ∈ τ is an n-ary relation symbol from τ , Q ∈ {∀, ∃}, the relativizer G is an atomic formula, (Q, ⋆) ∈ {(∀, →), (∃, ∧)}, x 1 , x 2 are variables, x is a finite tuple of variables, and Free(ψ) ⊆ Free(G). Let us mention also a generalization of GF due to van Benthem(1997), called the loosely guarded fragment (LGF). Also here it is required that all quantifiers have relativizers, but the relativizers need not be atomic. Further, a syntactic condition on the distribution of the variables of the tuple y over the relativizer G is imposed. The syntax of LGF is obtained from that of GF by keeping the definition otherwise intact but requiring only that G be a conjunction of atomic formulas (not necessarily a single atomic formula as in GF), and, moreover, stipulating that for every y i in the tuple y and every z ∈ Free(G), at least one conjunct of G contains both y i and z.

As is obvious and well known, ML can be translated into the guarded fragment of first-order logic (GF). [START_REF] Andréka | Modal languages and bounded fragments of predicate logic[END_REF] famously suggested that the distinguishing feature of 'modal fragments' of FOL is that quantifiers appear guarded in them. Notably, they proposed that this fact provides an 'explanation' of the decidability of basic modal logic. Indeed GF is decidable. The loosely guarded fragment (LGF) extends GF but remains decidable (van [START_REF] Van Benthem | Dynamic bits and pieces[END_REF]Grädel, 1999a). So it is potentially capable of 'explaining' even a larger variety of modal decidability results than GF. Postponing comments on the computational properties of MsL 0 to Section 10, we proceed to prove that MsL 0 cannot be translated into LGF and consequently not into GF.

We need some definitions. If the α i with 1 ≤ i ≤ m are atomic first-order formulas of some vocabulary τ and (x 1 , . . . , x s ) is a tuple of variables, the conjunction α 1 ∧ . . . ∧ α m is said to guard the tuple (x 1 , . . . , x s ) if for all 1 ≤ i, i ′ ≤ s there is 1 ≤ j ≤ m such that x i and x i ′ appear both in α j . Given that N is a τ -structure, a subset X of N is said to be loosely k-guarded in N, if for some s ≤ k there is an assignment γ : {x 1 , . . . , x s } → N such that X ⊆ Im(γ), and there are atomic formulas α i with 1 ≤ i ≤ m of vocabulary τ , such that N, γ |= α 1 ∧ . . . ∧ α m and the conjunction α 1 ∧ . . . ∧ α m guards the tuple (x 1 , . . . , x s ). A set is loosely guarded if it is loosely k-guarded for some k. In order to formulate the notion of loosely guarded k-bisimulation, we adopt the following notation. If F is a set of finite partial τ -isomorphisms between τ -structures M and N, and if f : X → Y is a map in the set F such that X ⊆ M and Y ⊆ N are loosely k-guarded sets, we write Zig(f, X) for the claim "for every loosely k-guarded set X ′ ⊆ M there is in the set F a partial isomorphism g : X ′ → Y ′ such that f and g agree on X ∩ X ′ ." Similarly, we write Zag(f, Y ) for the claim "for every loosely k-guarded set Y ′ ⊆ N there is in the set F a partial isomorphism g : X ′ → Y ′ such that f -1 and g -1 agree on Y ∩ Y ′ ." A loosely guarded k-bisimulation between M and N is any non-empty set F of finite partial isomorphisms between M and N such that for all f : X → Y in F with X, Y loosely k-guarded sets, we have Zig(f, X) and Zag(f, Y ). The width of an LGF formula is the maximum number of free variables (variable types) in its subformulas.

The notion of loosely guarded k-bisimulation offers, in particular, a criterion for equivalence of two structures (M, a) and (N, b) with respect to LGF formulas of one free variable and width at most k: if there is a loosely guarded k-bisimulation F between M and N with {(a, b)} ∈ F, then for all LGF formulas ψ of width at most k and with exactly one free variable, x, we have: M, a |= ψ iff N, b |= ψ. For this criterion and the requisite definitions presented above, cf. (Grädel, 1999b, Sect. 3). THEOREM 7.5. MsL 0 ≤ LGF.

Proof. Let R be a binary relation symbol. Consider the structures M = ({a, b, c}, R M ) and

M ′ = ({a ′ , b ′ 1 , b ′ 2 , c ′ 1 , c ′ 2 }, R M ′ ) depicted below: a ′ b ′ 1 Z Z b ′ 2 D D c ′ 1 O O c ′ 2 O O a b O O c O O M M ′
We show that the structures (M, a) and (M ′ , a ′ ) are LGF-equivalent by showing that for every positive integer k ≥ 2, there exists a loosely guarded k-bisimulation between (M, a) and (M ′ , a ′ ). Now, for all k ≥ 2, there are 6 loosely k-guarded subsets of M , namely ∅, {a}, {b}, {c}, {a, b} and {b, c}; and there are 10 loosely k-guarded

subsets of M ′ , that is, ∅, {a ′ }, {b ′ 1 }, {b ′ 2 }, {c ′ 1 }, {c ′ 2 }, {a ′ , b ′ 1 }, {a ′ , b ′ 2 }, {b ′ 1 , c ′ 1 } and {b ′ 2 , c ′ 2 }. Let F be the set consisting of the following maps of type M → M ′ : ∅, {(a, a ′ )}, {(b, b ′ 1 )}, {(c, c ′ 1 )}, {(b, b ′ 2 )}, {(c, c ′ 2 )}, {(a, a ′ ), (b, b ′ 1 )}, {(a, a ′ ), (b, b ′ 2 )}, {(b, b ′ 1 ), (c, c ′ 1 )} and {(b, b ′ 2 ), (c, c ′ 2 )}.
These maps are partial isomorpisms. Further, clearly for every f : X → Y in F we have both Zig(f, X) and Zag(f, Y ). For all k ≥ 2, the set F is, then, a loosely guarded k-bisimulation between M and M ′ containing the map {(a, a ′ )}. It follows that the {R}-structures (M, a) and (M ′ , a ′ ) satisfy the same LGF[{R}]-formulas of exactly one free variable. On the other hand, we note that the MsL 0 -formula ( /1)⊤ is true in M at a but not true in M ′ at a ′ . Therefore there cannot exist a map T from MsL 0 to the formulas of LGF[{R}] of exactly one free variable such that for all formulas φ ∈ MsL 0 and all pointed models (N, w), we would have N, w |= φ iff N, w |= T (φ).

Finite modal depth and finite breadth

Restricting attention to a finite set of propositional atoms, the number of pairwise non-equivalent ML formulas of a given modal depth is finite; for a proof, see, e.g., (Blackburn et al., 2002, Prop. 2.29). Not so for the logic MsL 0 . FACT 8.1 [START_REF] Tulenheimo | On modal logic, IF logic and IF modal logic[END_REF]. Suppose the set prop of available propositional atoms is finite. For any m ≥ 2, the set of pairwise non-truth-equivalent MsL 0 formulas of modal depth m is infinite.

Proof. If k ≥ 0 and m ≥ 2, let φ k m := . . . φ m , where φ m is defined as in the proof of Theorem 7.4, and the number of boxes preceding φ m is k. Let r ≥ 2 be arbitrary, and consider the set of formulas {φ r-2 m : m < ω}. All formulas in this set are of modal depth r. Yet whenever m 1 < m 2 , the formulas φ r-2 m 1 and φ r-2 m 2 fail to be truth-equivalent. This follows from Theorem 7.4: the former formula can be translated into FOL m 1 +r-1 but the latter cannot.

There is, however, a way to restore an analogy with basic modal logic. This requires taking into consideration an additional parameter which plays no role in ML but does play a role here: the breadth of an MsL 0 formula (see Definition 4.1). THEOREM 8.2. Suppose the set prop is finite. Let m, k < ω. The set of pairwise non-truth-equivalent MsL 0 formulas of modal depth m and breadth k is finite.

Proof. We prove the claim by double induction on the parameters m and k. The base case of literals (which are both of modal depth and of breadth zero) holds by the assumption that prop is finite. We proceed in two steps. (1) First observe that if φ is a formula of modal depth ≤ m + 1 and breadth ≤ k, it is obtained by some finite number (possibly zero) of applications of ∨ and ∧ from formulas of the forms φ or φ or φ or E n,S (φ 1 , . . . , φ n ) satisfying the following conditions:

-md (φ) ≤ m, |S| ≤ k, bre(φ) ≤ k -md (φ i ) ≤ m if i / ∈ S, md (φ i ) ≤ m -1 if i ∈ S, bre(φ i ) ≤ k.
Now, let k be fixed and assume that there are (up to truth-equivalence) only finitely many formulas of modal depth m and breadth k. We prove that in that case there are (up to truth-equivalence) likewise only finitely many formulas of modal depth m + 1 and breadth k. From the assumption it immediately follows that there are only finitely many formulas of each of the forms φ or φ or φ or E n,S (φ 1 , . . . , φ n ), where φ and the φ i satisfy the relevant syntactic conditions. But the rest of the formulas of modal depth ≤ m + 1 and breadth ≤ k are truth-functions of these formulas. And out of finitely many formulas only finitely many truth-functions can be formed. The claim follows.

(2) Next, note that if φ is a formula of modal depth ≤ m and breadth ≤ k + 1, it is obtained by some finite number (possibly zero) of applications of ∨ and ∧ from formulas of the forms φ or E n,S (φ 1 , . . . , φ n ) with |S| ≤ k + 1, where

-md (φ) ≤ m, md (φ i ) ≤ m -1 if i / ∈ S, md (φ i ) ≤ m -2 if i ∈ S -bre(φ), bre(φ i ) ≤ k.
Let m be fixed. Assume there are (up to truth-equivalence) only finitely many formulas of modal depth m and breadth k. We show that in that case there are (up to truth-equivalence) only finitely many formulas of modal depth m and breadth k + 1. Directly by assumption there are only finitely many formulas of the forms φ or E n,S (φ 1 , . . . , φ n ), where φ and the φ i satisfy the appropriate syntactic conditions. Since the other formulas of modal depth ≤ m and breadth ≤ k + 1 are truth-functions of these formulas, the claim follows.

Inexpressibility of contradictory negation

In Corollary 3.5 it was seen that MsL is not closed under contradictory negation; the proof turned on the fact that some MsL formulas cannot be translated into FOL. Since the fragment MsL 0 is so translatable, we do not know on the basis of the mentioned corollary whether also MsL 0 fails to be closed under contradictory negation. We proceed to prove that as a matter of fact this is the case. Let us first introduce a generalization of the notion of ML bisimulation.

DEFINITION 9.1 (Asymmetric MsL 0 bisimulation). Let (M, w) and (M ′ , w ′ ) be pointed models, with M = (M, R, V ) and 4) of an ML bisimulation and the following additional condition holds:

M ′ = (M ′ , R ′ , V ′ ). A relation Z ⊆ M × M ′ is an asymmetric MsL 0 bisimulation from the pointed model (M, w) to the pointed model (M ′ , w ′ ), symbolically Z : (M, w) (M ′ , w ′ ), if Z satisfies the conditions (0) to (
(5) Suppose k < ω and vZv ′ and (v,

t i ) ∈ (R • R) for all 1 ≤ i ≤ k.
Then there are t ′ 1 , . . . , t ′ k such that (a) and (b) both hold:

(a) t i Zt ′ i and (v ′ , t ′ i ) ∈ (R ′ • R ′ ); (b) If I is a subset of {1, . . . , k} and (v ′ , u ′ ) ∈ R ′ and (u ′ , t ′ i ) / ∈ R ′ for all i ∈ I, there is u with uZu ′ such that (v, u) ∈ R and (u, t i ) / ∈ R for all i ∈ I.
We write (M, w)

(M ′ , w ′ ) to indicate that there is a relation Z with Z : (M, w) (M ′ , w ′ ).
Some comments are in order. Subclause (5b) allows us to select any index set I and to consider the corresponding states t i with i ∈ I from the fixed tuple (t 1 , . . . , t k ), and it asserts that if there is in M ′ a successor of v ′ which is not among the predecessors of any of the states t ′ i with i ∈ I, then there is likewise a successor of v in M which is not among the predecessors of any of the states t i with i ∈ I. Positively this condition means that if all successors of v in M have at least one of the t i among their successors, then likewise all successors of v ′ in M ′ have at least one of the t ′ i among their successors. Clause ( 5) is manifestly asymmetric. Subclause (5a) asserts the existence of a certain tuple of states in M ′ provided that a certain tuple of states exist in M; there is no clause expressing the analogous condition in the direction from M ′ to M. And subclause (5b) asserts the existence of a certain state in M given that a certain state exists in M ′ ; no clause expresses the analogous condition in the direction from M to M ′ . EXAMPLE 9.2. Let us consider the models M, M ′ , N and N ′ :

w u 2 O O t 1 u 3 = = t 2 u 1 a a F F Z Z O O M w ′ t ′ u ′ 2 A A u ′ 1 ] ] ? ? _ _ M ′ a ′ b ′ 2 Y Y c ′ 1 c ′ 2 c ′ 3 b ′ 5 E E b ′ 4 K K b ′ 3 S S b ′ 1 a a b ′ 6 = = H H Q Q J J T T M M V V N ′ a b 1 Y Y c 1 c 2 c 3 b 4 E E b 3 K K b 2 S S Q Q X X C C J J M MF F N (a) Let Z be the following relation: {(w, w ′ ), (u 1 , u ′ 1 ), (u 2 , u ′ 1 ), (u 3 , u ′
2 ), (t 1 , t ′ ), (t 2 , t ′ )}. Evidently Z is a bisimulation. Does Z satisfy clause (5)? Given that wZw ′ and (w, t 1 ), (w, t 2 ) ∈ (R • R), we may take as an input of rule (5) one of these three tuples of states: (t 1 ), (t 2 ), (t 1 , t 2 ). In each case subclause (a) is satisfied: all states of the relevant set are related via Z to t ′ . Subclause (b) is trivially met as there is in M ′ no successor of w which would not have t ′ as its successor. We conclude that Z : (M, w) (M ′ , w ′ ).

(b) Conversely, we do not have (M ′ , w ′ ) (M, w). For, taking (t ′ ) as an input of the rule (5), the state t ′ would have to be correlated either with t 1 or with t 2 . In neither case would subclause (b) be satisfied. Note that the MsL 0 formula ( /1)⊤ is true in M ′ at w ′ but not in M at w.

(c) We also do not have (N, a)

(N ′ , a ′ ). To see this, observe first that for the input (c 1 , c 3 ) of rule (5), we must choose a pair (x 1 , x 2 ) of states from the set {c

′ 1 , c ′ 2 , c ′ 3 }. At least one of the states c ′ 1 , c ′ 2 , c ′ 3
does not appear in this pair. Hence there is a state b ′ j in N ′ having no successor among x 1 and x 2 (actually there are exactly two such that R ′ (v ′ , u ′ ) and R ′ (u ′ , t ′ j ) for some j ∈ I. Thus, there would be x such that t ′ j Z 1 x and R(u, x); indeed t ′ j is a certain finite path along R and x is its last member. Since there is only one state from M correlated with t ′ j via Z 1 , it follows that we would have x = t j . Yet x is R-accessible from u, but t j is not. This is a contradiction. We conclude that Z 1 : (M ′ , w) (M, w). To complete the proof, we define a relation Z 2 ⊆ N × M ′ . By the construction of (N, w), there are models T 0 , . . . , T h•m with the following properties: T 0 = M ′ ; T h•m = N; each T i is a tree of height m; and there is a map f i : T i → Pow (T i+1 ) mapping distinct states to disjoint sets of states such that for every state x ∈ T i and every state y ∈ f i (x), the submodel of T i generated by x is isomorphic to the submodel of T i+1 generated by y, and for every state z ∈ T i+1 there is x ∈ T i such that z ∈ f i (x). We set vZ 2 v ′ iff there are states x 0 , . . . , x h•m with x 0 = v ′ and x h•m = v such that for all 0 ≤ i < h • m, we have:

x i+1 ∈ f i (x i ).
That is, we have vZ 2 v ′ iff v is one of the 'copies' of v ′ created by the process of h-fold duplication of (M ′ , w). Trivially Z 2 is a bisimulation between (N, w) and (M ′ , w). Suppose vZ 2 v ′ and let the tuple (s 1 , . . . , s k ) of elements of N be the input of clause (5). For every s i there is a uniquely determined s ′ i such that s i Z 2 s ′ i and indeed (R ′ •R ′ )(v ′ , s ′ i ). Now, suppose there is I ⊆ {1, . . . , k} and u ′ with R ′ (v ′ , u ′ ) such that no s ′ i with i ∈ I is R ′ -accessible from u ′ . Then there is u with S(v, u) such that uZ 2 u ′ and no t i with i ∈ I is S-accessible from u. Namely, for contradiction suppose there is u with uZ 2 u ′ and S(u, s j ) for some j ∈ I. Then there is x with s j Z 2 x and R ′ (u ′ , x). But there is exactly one state in N to which s j is related via Z 2 , so x = s ′ j . This is a contradiction and we may conclude that Z 2 : (N, w) (M ′ , w).

Inspecting the proof of Lemma 9.4, we obtain the following:5 COROLLARY 9.5. Suppose Z is a bisimulation from (N, v) to (M, w).

If Z is a surjective function, then in fact Z is an asymmetric MsL 0 bisimulation from (N, v) to (M, w).

We proceed to prove that there is no proper MsL 0 formula whose contradictory negation is expressible in MsL 0 . THEOREM 9.6 (Strong inexpressibility of contradictory negation). If φ and ψ are MsL 0 formulas such that for all pointed models (M, w) we have M, w |= ψ iff M, w |= φ, then φ is not proper.

Proof. Assume φ is a proper formula of MsL 0 . By Lemma 4.5 the class Mod (φ) is either not closed under md (φ)-unraveling or else it is not closed under global duplication. That is, there is a pointed model (M, w) of height at most md (φ) such that M, w |= φ while M ′ , w |= φ, where the pointed model (M ′ , w) is either (i) the unraveling of (M, w), or else (ii) the global duplication of (M, w). Now, suppose for contradiction that there is an MsL 0 formula neg(φ) which is true in a pointed model iff φ is not true therein. We note that M ′ , w |= neg(φ). Let us consider the two cases separately. Case (i): In passing note that in this case (M, w) cannot be tree-like, for otherwise (M, w) would be isomorphic to its own md (φ)-unraveling. Now, by Lemma 9.4 (setting h := 0), we have (M ′ , w) (M, w). Therefore, by Theorem 9.3, we may conclude that M, w |= neg(φ). This is a contradiction. Case (ii): First note that (M, w) must be tree-like, for otherwise it would be its own global duplication. But if (M, w) is tree-like, again Lemma 9.4 applies (this time setting h := 1) and we have (M ′ , w) (M, w). This yields a contradiction, since by Theorem 9.3 we have again M, w |= neg(φ).

Theorem 9.6 states a very strong inexpressibility result for the fragment MsL 0 of MsL. Now, by any reasonable criterion ( /1)⊤ is the syntactically simplest proper MsL formula. As a consequence of what just proven, we may observe the following fact concerning the larger language MsL, thereby vindicating the claim we made in Section 3 to the effect that Corollary 3.5 (according to which MsL is not closed under contradictory negation) can be improved. COROLLARY 9.7. Any fragment of MsL which contains the formula ( /1)⊤ fails to be closed under contradictory negation.

Proof. Consider the pointed models (M, a) and (M ′ , a ′ ) discussed in the proof of Theorem 7.5. The formula ( /1)⊤ is true in the former but not in the latter. On the other hand, these pointed models are evidently bisimilar. Thus, ( /1)⊤ is a proper MsL 0 formula. By Theorem 9.6, then, there is no MsL 0 formula that can express the contradictory negation of ( /1)⊤. Observe that any MsL formula of modal depth at most 2 is by syntactic criteria a formula of MsL 0 . It follows that no MsL formula of modal depth at most 2 can express the contradictory negation of ( /1)⊤. Suppose, then, for contradiction that there is φ ∈ MsL with md (φ) ≥ 3 such that φ is true in a pointed model iff ( /1)⊤ is not true therein. Now, clearly any MsL formula of modal depth at most 2 is true at v in N iff it is true at v in the restriction of N to the height 2. It is also clear that any MsL formula χ of modal depth at least 3 is truth-equivalent over models of height at most 2 to an MsL formula θ χ of modal depth at most 2. It follows that for all pointed models (N, v) we have:

N, v |= φ iff (N ↾ 2), v |= φ iff (N ↾ 2), v |= θ φ iff N, v |= θ φ ,
where md (θ φ ) ≤ 2. But then θ φ is a formula of MsL 0 expressing the contradictory negation of ( /1)⊤. This is a contradiction. We conclude that there is no MsL formula which would express the contradictory negation of ( /1)⊤.

As a by-product of what just established, we obtain a proof of the rather obvious fact that FOL cannot be translated into MsL; in Sections 3 and 7 we promised to exhibit such a proof. COROLLARY 9.8. FOL ≤ MsL.

Proof. The formula ( /1)⊤ can be translated into FOL. Therefore also its contradictory negation can. So if we had FOL ≤ MsL, the contradictory negation of ( /1)⊤ could be translated into MsL, contrary to Corollary 9.7.

The robust decidability of modal logic revisited

We proceed to draw some general morals from the properties of MsL 0 that we have detected. Let us first note a couple of relevant facts about this logic.

Computational properties of MsL 0

Let us say that logic L is strongly closed under complementation if there exists a PTIME-computable function f such that for every φ ∈ L we have that f (φ) is true in a model iff φ is not true therein. If L is strongly closed under complementation, the satisfiability problem of L is decidable iff its validity problem is decidable. Moreover, if one of the problems is C-complete for some complexity class C, the other is coC-complete. If in particular C happens to be a deterministic complexity class, both problems are C-complete if one of them is: in this case coC = C. Now, many commonly encountered logics are strongly closed under complementation. Among them are the following: the logic S5 (i.e., ML evaluated over models whose accessibility relation is an equivalence relation), the (poly)modal logics K4 n (i.e., the extension of ML with n modalities, each associated with a transitive accessibility relation), the hybrid logic H(@), the logic of until and since (US), the finite-variable fragments FOL n of first-order logic, the guarded fragment (GF) and the loosely guarded fragment (LGF) of first-order logic, the fixed point extensions µML (µ-calculus), µGF and µLGF of ML, GF and LGF, respectively. All these logics have available a syntactic sign for the contradictory negation, so in each of these cases there is a constant time computable function yielding the contradictory negation of a given input formula. Observe that in logics like MsL which are not closed under complementation to begin with (cf. Theorem 9.6), the satisfiability and validity problems need to be discussed separatelyor at least there is no obvious way to reduce one to the other.

The following results are immediate consequences of results proven in [START_REF] Tulenheimo | On modal logic, IF logic and IF modal logic[END_REF] about the logic L SD (see ibid., Theorems 15,17 and 19). Logic L SD is a notational variant of MsL; more specifically there exist obvious linear-time computable truth-preserving translations from L SD to MsL and from MsL to L SD . The fact that basic modal logic has many 'good' properties that firstorder logic lacks has generated a remarkable literature. The modelchecking problem and the validity and satisfiability problems of ML are decidable. More specifically, the combined complexity of the modelchecking problem for ML is PTIME-complete [START_REF] Grädel | On logics with two variables[END_REF], while its satisfiability problem is PSPACE-complete [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF]. Now, ML is semantically speaking a fragment of first-order logic. Via its translation, then, ML determines a decidable fragment of FOL. This has been considered interesting because in the relevant fragment no limit is imposed on the allowed quantifier alternations -while historically, known decidable fragments of FOL had been obtained by restricting patterns of allowed quantifier alternations; see, e.g., [START_REF] Börger | The Classical Decision Problem[END_REF]. We may note that MsL 0 is not less interesting in this respect. OBSERVATION 10.2. Also MsL 0 is semantically a decidable fragment of FOL with unbounded quantifier alternation (Theorem 7.2). In particular, it is strictly more expressive than ML (Fact 3.1).

Basic modal logic has been hailed not only because it is decidable (and decidable using an algorithm of a relatively reasonable complexity), but because it is 'robustly decidable': it has a host of independently interesting extensions or variants which are likewise (elementarily) decidable. Examples abound. The satisfiability problem of S5 is NPcomplete [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF], while that of K4 n is PSPACE-complete for all n ≥ 1; for hardness, see [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF] and for inclusion cf., e.g., (Horrocks et al., 2007, Thm. 21). The satisfiability of the hybrid logic H(@) is PSPACE-complete [START_REF] Areces | A road-map on complexity for hybrid logics[END_REF]. It was noted in [START_REF] Burgess | Axioms for tense logic I. 'Since' and 'Until[END_REF] that the decidability of the logic of until and since (US) evaluated over arbitrary linear orders immediately follows from the results of [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF]. Actually the satisfiability problem of US over arbitrary linear orders is PSPACE-complete: inclusion has been proven in [START_REF] Reynolds | The complexity of decision problems for linear temporal logics[END_REF][START_REF] Rabinovich | Temporal logics over linear time domains are in PSPACE[END_REF]; hardness follows from the main result of [START_REF] Reynolds | The complexity of the temporal logic with 'until' over general linear time[END_REF]. The satisfiability problem of the µ-calculus is EXPTIME-complete [START_REF] Emerson | The complexity of tree automata and logics of programs[END_REF].

OBSERVATION 10.3. Modal slash logic provides yet another confirmation of the robust decidability of ML -in a strikingly strong way.

(a) Extending ML by performing slashing in the way permitted by the syntax of MsL 0 yields a logic with a decidable satisfiable problem.6 Even better, insofar as the satisfiability problem is concerned, nothing is lost in terms of computational complexity in the transition from ML to MsL 0 : the satisfiability problem of both logics is PSPACE-complete. Unless PTIME = NP, the difficulty of solving the model-checking problem is increased, though (cf. Proposition 10.1).

(b) Consider the full logic MsL -which, as we recall, is not translatable into FOL. It was proven in (Sevenster, 2010, Thm. 4.9) that the satisfiability problem of a certain polymodal extension of (a notational variant of ) MsL is decidable, actually in 2NEXPTIME. Therefore, in particular, MsL singles out a decidable fragment of ESO lying beyond FOL. And we obtain a host of new decidable fragments of FOL: a fortiori every first-order translatable fragment of MsL has a decidable satisfiability problem.

Explaining the robust decidability of ML

It is natural to ask -and has indeed been asked by several peoplewhat it is in ML that is responsible for its good computational behavior, and especially for its robust decidability. Looking at different ways of translating ML into FOL, one may reflect upon syntactic properties of the translations, and endeavor to identify, from the viewpoint of FOL, syntactic features that would throw light on the relevant properties of ML. One may expect this to lead to a generalization: a fragment of FOL more expressive than ML, or at least syntactically an extension of the translation of ML, yet exhibiting appropriate 'nice' properties. The authors discussing the issue have phrased it as a quest for an explanation; cf. (Vardi, 1998, pp. 8, 22), (Andréka et al., 1998, pp. 243, 261), (Grädel, 2001, pp. 8, 12). If any sort of explanation is sought for, it cannot simply consist of a description applying to ML and to nothing else -any more than the question 'Why does Moon revolve around the Earth?' could be answered by saying 'Because it is Moon.' At the very least, we need to pinpoint a more general phenomenon which subsumes the case of ML. Concretely, at least three features have been proposed to have an explanatory role: the translatability of ML into the 2-variable fragment of first-order logic (FOL 2 ), its translatability into the guarded fragment of first-order logic (GF), as well as the tree-model property that ML enjoys. The first two involve syntactic conditions imposed on the relevant fragment of FOL, whereas the third one is a purely semantic condition. The relevance of these proposals comes from the good computational behavior of the logics FOL 2 and GF as well as from the fact that the decidability of logics having the tree model property can be approached using very widely applicable automata-theoretic tools. The combined complexity of the model-checking problem of FOL 2 is PTIME-complete [START_REF] Grädel | On logics with two variables[END_REF]. The logic FOL 2 without equality is decidable [START_REF] Scott | A decision method for validity of sentences in two variables[END_REF]. This is enough to conclude that ML is decidable, since equality is not needed to translate (in polynomial time) ML into FOL 2 . The complexity of the satisfiability problem of FOL 2 is NEXPTIME-complete; hardness follows from a result of [START_REF] Fürer | Alternation and the Ackermann case of the decision problem[END_REF] while inclusion was proven in [START_REF] Grädel | Undecidability results on two-variable logics[END_REF]. What about the logic GF? Like with FOL 2 , also the combined complexity of the model-checking problem of GF is PTIME-complete [START_REF] Berwanger | Games and model checking for guarded logics[END_REF]. The decidability of GF was proven in [START_REF] Andréka | Modal languages and bounded fragments of predicate logic[END_REF]. The satisfiability problem of GF is 2EXPTIME-complete (Grädel, 1999a).

Let us restrict attention to syntactically phrased explanationssuch as FOL 2 and GF. Even when an automata-theoretic account of the decidability of a modal logic is available, we would still wish to understand of what its decidability consists from the syntactic viewpoint. Now, it makes sense to ask which syntactic features of the translation of ML into FOL are responsible for its decidability -except that of course there is no unique translation, instead there are syntactically innumerable translations which might lead to different assessments of what it is that is responsible for the properties considered. Relative to a given translation, what does it, then, mean to figure out which syntactic features are responsible for the decidability of the fragment. Well, it can only mean detecting irrelevant syntactic features and showing that generalizing with respect to those features still results to a fragment with sufficiently nice features. Of course even relative to a fixed translation there might be several ways of effecting such a generalization. When one poses questions such as 'Why is ML so robustly decidable?' or looks for an explanation of the decidability of ML, what one is doing is at least searching for such generalizations. One's search is typically guided by some preexisting idea as to what modal logic is. Then one aims to single out modal fragments of first-order logic and perhaps to understand in first-order terms of what the modal nature of a fragment consists.

How should we evaluate whether a proposed syntax-based explanation of the robust decidability of ML is correct or illuminating or credible? We may distinguish a strong and a weak criterion. In what follows, the options are, for simplicity, expressed in terms of the satisfiability problem, even though we might wish to consider also further computational problems. From now on, when we say without qualification that logic L ′ is translatable into L, we mean that there exists a polynomial time computable truth-preserving translation of L ′ into L (thereby deviating from the terminology introduced in Subsect. 1.1).

(1) We say that the decidability of an extension or variant of ML is strongly explained by the translatability of ML into logic L, if L is decidable (using an algorithm of such-and-such complexity). Logic L strongly explains the robust decidability of ML if it strongly explains the decidability of all relevant extensions or variants of ML. For example, one manifestation of the robust decidability of ML is that the satisfiability problem of the modal logic T (or the result of restricting the evaluation of ML to models with a reflexive accessibility relation) is also decidable, in fact PSPACE-complete [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF]. This fact is strongly explained by the translatability of ML into FOL 2 , since T can be translated into FOL 2 : to find out whether a formula φ of T is satisfiable, apply a decision algorithm of FOL 2 to the formula (ψ φ ∧ ∀xRxx), where ψ φ is a translation of φ into FOL 2 using only the variables x and y. Also basic tense logic is decidable and indeed translatable into FOL 2 . For explanations in this sense, cf. (Vardi, 1998, p. 11). Note that it might be tempting to liberalize the definition of the notion of strong explanation by saying that it suffices that the satisfiability problem of M can be reduced to that of L. Here one should be careful, though. Since for example the satisfiability problem of FOL 2 is NEXPTIME-complete, we could according to such a definition trivially 'explain' the decidability of any extension or variant M of ML whose satisfiability problem happens to lie in NEXPTIME. For, for such a logic M, there would trivially exist a PTIME-reduction t : M → L such that for any formula φ of M, we would have that φ is satisfiable iff t(φ) is satisfiable. The more complex the satisfiability of the explanans, the more we would purportedly get explanatory power! We are well-advised to stay with reductions phrased in terms of truth-preserving (PTIME-computable) translations.

(2) If logic L is decidable (using an algorithm of such-and-such complexity), the translatability of ML into L weakly explains the decidability of an extension M of ML, if the result L ′ of extending L in the same way as M extends ML has a decidable satisfiability problem. For example, the translatability of ML into GF offers a weak explanation of the fact that the satisfiability problem of µML is decidable; actually this problem is EXPTIME-complete [START_REF] Emerson | The complexity of tree automata and logics of programs[END_REF]. Namely, the satisfiability problem of the fixed point extension µGF of GF is decidable, in fact 2EXPTIME-complete [START_REF] Grädel | Positional determinacy of games with infinitely many priorities[END_REF]. Incidentally, the same fact is not weakly explained by the translatability of ML into FOL 2 , because the fixed point extension of FOL 2 is highly undecidable [START_REF] Grädel | Undecidability results on two-variable logics[END_REF].

If M is a variant of ML obtained by imposing a restriction on its models, the fact of translatability weakly explains the decidability of the variant if the result of restricting the models of L in an analogous way is decidable as well. In connection with such model restrictions, several 'analogous' restrictions on the side of L may present themselves. If, say, ML is considered relative to models whose accessibility relation is required to be transitive (i.e., when considering the logic K4), according to the generalization chosen we must see how L behaves over structures which interpret exactly one/at least one/every binary predicate by a transitive relation; even further options are conceivable as will be noted below, cf. [START_REF] Szwast | The guarded fragment with transitive guards[END_REF]. Logic L weakly explains the robust decidability of ML, then, if it weakly explains the decidability of all relevant extensions and variants of ML.

The above terminology proves useful for systematic purposes, but one should not be misled by it. The existence of a strong explanation does not guarantee the existence of a weak explanation. To see this, write X for the result of translating µML into monadic second-order logic. Let Y := FOL 2 ∪ X. We assume for simplicity that FOL 2 utilizes the variables x, y but no formula of X uses these individual variables. Then we can check in PTIME whether a formula of Y is from X or not, and Y is decidable because FOL 2 and X are. Now, by the above criterion the translatability of ML into Y provides a strong explanation for the decidability of µML, since (trivially) µML ≤ Y and Y is decidable. Yet this fact does not provide a weak explanation for the decidability of µML: the fixed point extension of Y contains the fixed point extension of FOL 2 which is highly undecidable. (It does not matter in which particular way we define the fixed point extension of X.) Conversely, the existence of a weak explanation does not guarantee the existence of a strong one. For example the translatability of ML into GF weakly explains the decidability of because µGF is decidable, but it does not strongly explain the decidability of µML, because µML cannot be translated into FOL to begin with and so a fortiori not into GF. 10.4. How do the proposed explanations fare?

Let us look at the proposed explanations of the robust decidability of ML in some more detail. In the literature, the observation that ML is translatable into FOL 2 is often attributed to [START_REF] Gabbay | Expressive functional completeness in tense logic[END_REF]. So is the general proposal that there is an intimate relation between the finitevariable fragments of FOL and modal logics; cf., e.g., [START_REF] Vardi | Why is modal logic so robustly decidable?" In Descriptive complexity and finite models[END_REF][START_REF] Van Benthem | Temporal logic[END_REF][START_REF] Andréka | Modal languages and bounded fragments of predicate logic[END_REF]. In reality Gabbay did not even mention the fact that basic modal or basic tense logic can be translated into FOL 2 ; neither did he 'identify' modal fragments of FOL with its finite-variable fragments. What he did, though, is to establish a lemma, namely Lemma 57 in [START_REF] Gabbay | Expressive functional completeness in tense logic[END_REF], stating that a k-dimensional modal/temporal logic with a finite number of connectives ♯ i -the semantics of each connective being defined by some first-order formula of k free variables, called the table of the connective -can be translated into FOL max i n(i)+k , using at most max i n(i) bound and k free variables, where for every relevant i, the number of bound variables used in the table of the connective ♯ i equals n(i). The proof does not make use of properties of any specific class of models, so the result applies generally. Now, if one takes k-dimensional modal logics in the sense of Gabbay as exhausting the possible modal fragments of FOL and if one decides to restrict attention modal logics with only finitely many connectives, then indeed Gabbay's lemma implies that any such modal fragment can be translated into FOL n for some n < ω. Pointing to this doubly conditional consequence of the lemma is the best that can be said by way of justifying the attributions mentioned in the beginning of this paragraph. Inspecting, then, the appropriate tables, it is seen, e.g., that ML is translatable into FOL 2 and US into FOL 3 . (Both logics are onedimensional; the tables of the former use 1 and the tables of the latter 2 bound variables.) Returning to FOL 2 and the robust decidability of ML, the explanatory value of the embeddability of ML into FOL 2 is limited. This fact does not strongly explain the decidability of µML, simply because µML ≤ FOL 2 . For a further example, the logic US evaluated over arbitrary linear orders is a decidable variant of ML whose decidability is not strongly explained by the translatability of ML into FOL 2 . For, 3 variables are actually needed to express the tables of until and since and therefore US cannot be translated into FOL 2 (relative to the class of all linear orders). In passing, note that in connection with a logic such as US there is no clear meaning to the notion of weak explanation: how should we extend FOL 2 , say, in order to extend it as US extends ML?

In [START_REF] Vardi | Why is modal logic so robustly decidable?" In Descriptive complexity and finite models[END_REF], the logic S5 is discussed as a counterexample to the explanatory role of FOL 2 . It is a fact that in order to express transitivity in FOL, 3 variables are needed. Because any translation of an S5 formula, evaluated over arbitrary models, must express that the interpretation of its binary relation symbol is transitive, the translation cannot be in FOL 2 . No strong explanation of the decidability of S5 is offered by the fact that ML ≤ FOL 2 . Note that translatability into FOL 3 cannot be used to formulate an alternative strong explanation, since FOL n with n ≥ 3 (even without equality) is undecidable; this follows from the simple fact that already FOL 3 harbors the prefix class AEA which is undecidable; see, e.g., [START_REF] Börger | The Classical Decision Problem[END_REF]. It could be argued, however, that it is unfair to require that transitivity should be expressible in a logic L in order for L to be able to explain the decidability of S5. After all, S5 itself is nothing but ML evaluated on a specific class of models, so we should rather ask whether FOL 2 [{R, P 1 , . . .}] is decidable when evaluated over structures interpreting the binary relation symbol 'R' by an equivalence relation. That is, we should rather ask whether we can have a weak explanation here. As a matter of fact, it was proven in (Kieroński and Otto, 2005) that the satisfiability problem of FOL 2 with a single equivalence relation is decidable, in fact NEXPTIMEcomplete. So arguably S5 does not provide a counterexample to the explanatory role of FOL 2 in the weak sense. Yet, other examples suffice for showing that FOL 2 cannot function even as a weak explanation. It was already noted in Subsection 10.3 that the translatability of ML into FOL 2 does not weakly explain the decidability of the µ-calculus: the fixed point extension of FOL 2 is highly undecidable.

At the end of Subsection 10.3 we mentioned that the translatability of ML into GF explains weakly but not strongly the decidability of the µ-calculus. Another case in which strong explanation fails -a case in which, as noted, the question of weak explanation cannot even be formulated in a natural way -is that of the logic US evaluated over the arbitrary linear orders. Take for example the formula until (p, q) which this would provide a weak explanation of the decidability of K4. And actually it was proven in [START_REF] Szwast | The guarded fragment with transitive guards[END_REF] that the former problem is indeed decidable, in fact 2EXPTIME-complete. The discussion above shows that it is not obvious how to choose the specific first-order decision problem that would function as a weak explanation of a given modal decision problem. Though at first sight [GF + TG] looks promising, it would be more in line with the modal case to find a direct model restriction to be imposed on models of GF than forcing such a restriction with expressions like Trans[R 1 , . . . , R k ] not inherently belonging to our language. Unfortunately for those who would like to see GF as a universal explanation in modal decidability matters, no such model restriction is forthcoming in the case of [GF + TG]. The best we could do is the following 'hybrid' formulation. Every formula ϕ of GF[τ ] has some finite number n(ϕ) of binary guards, so from ϕ we can select a set of binary guards in 2 n(ϕ) ways. For every 0 ≤ i ≤ 2 n(ϕ) , define C i ϕ := {(ϕ, M) : M is a τ -structure interpreting by a transitive relation every each binary guard belonging to the selection i}. We stipulate that the case i := 0 corresponds to the selection of the empty set of guards. Note that C 0 ϕ = {(ϕ, M) : M is a τ -structure}. Finally, put C := {C i ϕ : ϕ ∈ GF[τ ] and 0 ≤ i ≤ m(ϕ)}. Now, the satisfiability problem of [GF + TG] can be reduced to the following problem: given a class C i ϕ ∈ C, find out whether there is a model M with (ϕ, M) ∈ C i ϕ such that M |= ϕ. This formulation makes use of model restrictions, but they are relative to the syntax of a given formula. That is, if we say that a weak explanation of the decidability of K4 consists of the decidability of the latter decision problem, also this suggestion appears rather artificial.

10.5. Lessons from MsL 0

By the results discussed earlier in this paper, the logic MsL 0 is an extension of ML that appears to provide a rather strong counterexample to each of the explanations offered in the literature as being relevant to the robust decidability of ML. First, as noted in Observation 10.3, on the one hand MsL 0 , and even the full MsL, are decidable extensions of ML, but on the other hand, insofar as the satisfiability and validity problems are concerned, the logic MsL 0 behaves algorithmically exactly as well as ML itself. Second, however, we have seen that the following negative facts hold:

1. The logic MsL 0 is able to state that certain paths of the same length in a pointed model converge (have a common successor), so this logic lacks the tree-model property (Fact 3.2).

question is clear: its connectives are the two modal operators , and the propositional connectives. The slash symbol '/' is not an operator -but, as (Hintikka, 1997, p. 523) puts it, a punctuation device, which helps to complete the job of parentheses as scope-indicators. However, it is plain that the tables of these connectives only yield the semantics of ML, not that of MsL 0 . If we wish to attempt forcing MsL 0 into the format in which the semantics of a modal language is defined via tables associated with its connectives, it appears advisable to treat the expression ( /1) as if it was an operator of its own. Then we can assign the following table to this pretended operator: (∃y/x)(Rxy ∧ P y). Supposing the remaining connectives , , ∧, ∨, ¬ have their usual tables, we end up having a way to assign to every MsL 0 formula φ a formula T [ψ] of FOsL expressing the truth condition of φ. Such a formula T [ψ] is simply computed from atomic subformulas of φ by making use of the tables; incidentally, we may arrange that the formulas T [ψ] only use the variables x and y. Construed in this way, MsL 0 is a one-dimensional modal logic with finitely many connectives. The tables of these connectives are strings of FOsL; the truth conditions of MsL 0 formulas are defined by formulas of FOsL obtained via the tables. Yet MsL 0 is not translatable into any finite-variable fragment of FOL. That is, Gabbay's lemma cannot be generalized by allowing the tables of connectives to be even very simple FOsL formulas. The interest of this observation is reinforced by the fact that still the truth condition of each single MsL 0 formula can be expressed even in FOL. However, if we wanted to use tables written in FOL to express the semantics of MsL 0 , we would need to introduce infinitely many connectives: essentially the connectives C n,S of grammar C. While the table of ( /1) can be translated into FOL, there is no n such that every 'substitution instance' of the table can be translated into FOL n .

Let us then note how MsL as a semantic fragment of FOL behaves from the viewpoint of guards. In the guarded fragment, quantifiers are both (syntactically) relativized and (semantically) guarded: quantifiers only appear relativized, i.e., in contexts of the form Q x(G ⋆ ψ) with (Q, ⋆) ∈ {(∀, →), (∃, ∧)}, and furthermore the relativizer G is a guard in the sense that it imposes an explicit condition relating the variables in the tuple x to the free variables of ψ. We might conceive of separating the two functions of guards. A formula might serve to impose the relevant sort of semantic condition without being syntactically a relativizer of the quantifier. For example in the formula ∃z∀y(Rxy → (Ryz ∧ P z)) the atomic formula Ryz in this sense guards the quantifier ∃z without being, syntactically speaking, its relativizer.

Indeed, in the standard first-order translation of MsL 0 the two functions of guards are separated. Let us state in a precise way how MsL 0 in

•

  If the position (( /i 1 , . . . , i k )ψ, b, a) has been reached and R(a, c), then (ψ, b, c) is a position. If a is R-maximal, (ψ, b, fail) is a position. E makes the choice. If (ψ, b, fail) is chosen, A wins the resulting play. • If the position ( ψ, b, a) has been reached and R(a, c), then (ψ, b, c) is a position. If a is R-maximal, (ψ, b, fail) is a position. It is player A who chooses. If (ψ, b, fail) is chosen, E wins the resulting play.

  DEFINITION 4.3 (Recollection, recollection state). Let φ ∈ MsL 0 . If (( /1)χ, c, a) is the last position of a play π of game G(φ, M, w), there is in π a unique earlier position of the form ( β, d, b) with R(b, a) such that ( /1)χ is a term of β. Similarly, if ((χ 1 ∨ χ 2 ), c, a) is the last position of a play π with ∨ contextual, there is in π a unique earlier position of the form ( β, d, b) with R(b, a) such that χ 1 and χ 2 are Boolean combinations of terms of β. We say that the position ( β, d, b) is the recollection of the slashed diamond token ( /1) in π and the element b of M its recollection state in π; respectively we say that ( β, d, b) is the recollection of the relevant contextual disjunction token in π and b its recollection state in π.

  THEOREM 4.5. Let φ ∈ MsL 0 . If the class Mod (φ) is closed under md (φ)-unraveling and global duplication, then φ is not proper.

  (a) A strategy function for α is positional if its value on a play π depends only on the last model move in π. If α is a slashed diamond, a strategy function for α is quasi-positional if its value on π depends only on the recollection state of α in π. And if α is a contextual disjunction token, a strategy function for α has bounded quasipositionality if its value depends only on the following two positions: the last model move of π and the recollection state of α in π.

  again, the recollection( β, d, b) of ( /1) with R(b, a) occurs in the sequence τ , then we may observe that the substring component of the last position of τ must be a contextual diamond. But then, since τ ≈ h(π), the plays τ and h(τ ) share the position( β, d, b), and it follows that also the plays σ and h(τ) ⌢ g(τ ) ⌢ τ share the position ( β, d, b). That is, σ ≈ π * .3. The case ψ := (χ 1 ∨ χ 2 ) with contextual ∨: Again we consider two subcases, according to where the recollection ( β, d, b) of the slashed disjunction token lies; note that here R(b, a). (3.1) If it occurs in the sequence g(τ ) ⌢ ρ, then the plays π * and σ share both the position ( β, d, b) and their last model moves, namely the position (β, d, a) and we have σ ≈ π * . (3.2) If, again, the recollection ( β, d, b) of the diamond token occurs in the sequence τ , we may observe that also the substring component of the last position of τ must be a contextual diamond. But then, since τ ≈ h(π), the plays τ and h(τ ) share both the position ( β, d, b) and the position (β, d, a), and it follows that also the plays σ and π * share these positions. That is, σ ≈ π * .

  MsL 0 compared with FOL 7.1. Translatability into FOL Trivially MsL 0 ≤ MsL. Unlike MsL itself, MsL 0 can actually be translated into FOL. Let us first take an example.

  MsL 0 and by Observation 5.6, there is a winning strategy for player E in game G(ζ i , M, b). Then, by the inductive hypothesis we have M, b |= T x 0 [ζ i ]. If, again, we have i ∈ S, then ζ i is a non-formula.

  Conversely, suppose M, a |= T x 0 [ψ]. Then there are witnesses c i 1 , . . . , c i |S| such that for all b with R(a, b) we have M, γ |= C n,S (ξ 1 , . . . , ξ n ), with γ(x) = b and γ(x i k ) = c i k . Let d ∈ {0, 1} m be a tuple of conjunctive choices in the tree C n,S . Then there is a corresponding substring token (ξ j , e j ) such that M, γ |= ξ j . If j /

fragment

  MsL 0 of MsL. It follows by Theorem 7.2 that MsL 0 < FOL. As to the relation of MsL 0 and MsL, we have: COROLLARY 7.3. MsL 0 < MsL. Proof. Trivially MsL 0 ≤ MsL. By Theorems 3.4 and 7.2, MsL cannot be translated into FOL but MsL 0 can. So MsL ≤ MsL 0 .

  PROPOSITION 10.1. (a) The model-checking problem for MsL 0 is NP-complete in combined complexity (i.e., measured in terms of the combined length of both inputs); (b) the validity problem of MsL 0 is PSPACE-complete; (c) MsL 0 has the strong finite model property (i.e., there is a recursive upper bound to the size of every satisfiable MsL 0 formula); and (d) the satisfiability problem of MsL 0 is PSPACE-complete. 10.2. ML and MsL 0 as fragments of FOL

We assume that 0 and 1 are objects not belonging to the set M .

It was observed in(Hodges, 1983, p. 94) and in(Hintikka and Kulas, 1985, pp. 6- 7) that one must assume the Axiom of Choice in order to prove the equivalence of the standard Tarskian semantics of first-order logic and its game-theoretical semantics.[START_REF] Hodges | Logic and Games[END_REF] noted that if the weaker notion of strategy is applied -namely that of non-deterministic strategy -we obtain an unconditional correspondence between the Tarskian and the game-theoretical semantics for first-order logic.

Recall that abbreviates ( /∅).

The author is grateful to Antti Kuusisto who observed that Lemma 9.4 has this corollary.

To employ an imprecise turn of phrase of a kind common in the literature, ML remains decidable even when it is subjected to some slashing. Of course in reality ML is not the subject of change here -there is no subject of change -rather one logic gives rise to another and a certain property is preserved.

such states). But this violates subclause (5b), since all states among b 1 , b 2 , b 3 , b 4 have one of the states c 1 and c 3 as their successor in N. We note that the formula (( /1)⊤ ∨ ( /1)⊤) is true in N at a but not in N ′ at a ′ . 2 ), (c 2 , c ′ 1 ), (c 3 , c ′ 3 )}. Now, Z is a bisimulation. Further, for any tuple x ∈ ∪ 1≤m≤3 {c ′ 1 , c ′ 2 , c ′ 3 } m , the corresponding tuple y ∈ ∪ 1≤m≤3 {c 1 , c 2 , c 3 } m (uniquely) determined by the relation Z clearly satisfies clause (5).

Using the notion of asymmetric bisimulation just defined, we obtain a criterion for the preservation of truth of an MsL 0 formula when moving from a given pointed model to another. The criterion precisely does not guarantee the preservation of truth also in the direction from the latter to the former pointed model. This asymmetry is crucial when proving that MsL 0 is not closed under contradictory negation. For proofs of this kind, cf., e.g., (Immerman, 1999, Ch. 8).

We will use the following terminology. If R is a binary relation, (U 1 , . . . , U m ) is a partition of the set {u : R(v, u)} and there are pairwise distinct states s 1 , . . . , s n with n ∈ {m, m -1} such that s i is a common R-successor to all states in U i , we say that the partition is indexed by the tuple (s 1 , . . . , s n ). If n = m -1, the partition is with remainder and the cell U m is a remainder cell. If n = m, it is without remainder. If (t 1 , . . . , t k ) is any tuple of states (not necessarily pairwise distinct), let (s 1 , . . . , s n ) be a tuple of states such that {s 1 , . . . , s n } = {t 1 , . . . , t k }, the states s i are pairwise distinct (hence n ≤ k), and s i precedes s j iff there are i ′ , j ′ with i ′ < j ′ such that s i = t i ′ and s j = t j ′ . We say derivatively that a partition (U 1 , . . . , U m ) is indexed by the tuple (t 1 , . . . , t k ) if it is indexed by the tuple (s 1 , . . . , s n ). Note that there may in general be many ways of partitioning the set of successors of a state v in such a way as to be indexed by a tuple: this is the case when u 1 , u 2 , u 3 are successors of v, t is a successor of u 1 , u 2 and t ′ is a successor of u 2 , u 3 .

We may consider MsL 0 formulas as generated by the grammar C. It is evident that the claim holds for atoms, and that it can be inductively proven to hold for formulas of the forms Tero Tulenheimo ∨, ∧, , ; for the cases of and we will be able to use the inductive hypothesis thanks to the fact that Z has the properties of usual bisimulation between (M, w) to (M ′ , w ′ ). What remains to be checked are the formulas of the form D n,S (ξ 1 , . . . , ξ n+1 ). Without loss of generality we may assume that there is 1 ≤ k ≤ n + 1 such that S = {1, . . . , k}. Let T x 0 be the translation of MsL 0 into FOL discussed in the proof of Theorem 7.2. Now, instead of φ := D n,S (ξ 1 , . . . , ξ n+1 ), we may just as well consider its FOL translation θ := ∃x 1 . . . ∃x k ∀y(Rx 0 y → D n,S (ξ ′ 1 , . . . , ξ ′ n+1 )), where

We may note that among the formulas ξ ′ 1 , . . . , ξ ′ n+1 , there is for every variable x i with 1 ≤ i ≤ k exactly one formula ξ ′ j in which this variable occurs free. Now, there are positive integers m and r 1 , . . . , r m such that θ is logically equivalent to an FOL formula χ of the form

where each ζ ij is one of the formulas ξ ′ 1 , . . . , ξ ′ n+1 . Here one and the same variable x i with 1 ≤ i ≤ k may well occur free in several conjuncts.

Assume inductively that for any states r and r ′ , if rZr ′ and M, r |= ζ ij , then M ′ , r ′ |= ζ ij . Now, suppose that vZv ′ and that for fixed (but not necessarily pairwise distinct) states t 1 , . . . , t k and for all 1 ≤ i ≤ m, we have:

By the fact that Z : (M, w) (M ′ , w ′ ), if we take the tuple (t 1 , . . . , t k ) as the input of rule (5), a certain tuple (t ′ 1 , . . . , t ′ k ) is obtained with t l Zt ′ l for all 1 ≤ l ≤ k. We proceed to prove that for every 1

Let i be fixed. Since ∀y(Rx 0 y → 1≤j≤r i ζ ij ) is satisfied in (M, v, t 1 , . . . , t k ), there is I ⊆ {1, . . . , k} such that the set {u : R(v, u)} has a partition P indexed by the tuple t i : i ∈ I . The partition P has at most r i ≤ k + 1 cells. By subclause (5a) in the definition of asymmetric MsL 0 bisimulation, there is, then, a partition P ′ of the set {u ′ : R ′ (v ′ , u ′ )} indexed by the tuple t ′ i : i ∈ I . Let l ∈ I be arbitrary. Then there is j such that the state t l satisfies the formula T x 0 /x l [φ j ] in M. On the other hand, t l Zt ′ l . Thus, by the inductive hypothesis t ′

If, again, the partition P is with remainder, P ′ may or may not be itself with remainder. If it is without remainder, the claim follows immediately by the inductive hypothesis. If it is with remainder, we need to check that every state in the remainder cell of P ′ satisfies in M ′ some formula ξ ′ l with l / ∈ S. Let u ′ be any state with R ′ (v ′ , u ′ ) in the remainder cell of P ′ . By clause (5a) we find, then, a state u with R(v, u) in the remainder cell of P such that uZu

. By the inductive hypothesis we may conclude that M ′ , u ′ |= ξ ′ l , and again the claim follows.

In the above proof it was crucial that the states t ′ 1 , . . . , t ′ k provided by the asymmetric MsL 0 bisimulation Z were obtained once and for all as witnesses for certain slashed diamonds, and that it was possible to repeatedly choose a selection I of those states when considering the relevant different conjuncts. Indeed it would have led to too weak a condition if subclause (5b) had been imposed directly on the states t ′ 1 , . . . , t ′ k and not to a separately chosen selection thereof; that would have corresponded to choosing separate witnesses for each conjunct.

We use the following lemma in proving the main result of the present section, i.e., that MsL 0 is not closed under complementation.

Proof. First note that the following clearly holds. If

(M 3 , w 3 ). Let (M, w) be a pointed model, (M ′ , w) its m-unraveling and (N, w) the h-fold duplication of (M ′ , w). By what just noted, in order to prove the lemma, it suffices to show that (N, w) (M ′ , w) and (M ′ , w)

We define a relation Z 1 ⊆ M ′ × M by using the fact that there is a natural correlation of the states of the models M ′ and M, given the way in which M ′ is produced from M. For every state v

Plainly Z 1 is a bisimulation between (M ′ , w) and (M, w). We claim that Z 1 also satisfies clause (5) of an asymmetric bisimulation. So suppose v ′ Z 1 v and let the tuple (t ′ 1 , . . . , t ′ k ) of elements of M ′ be the input of clause (5). For every t ′ i there is a uniquely determined

Suppose, then, that there is I ⊆ {1, . . . , k} and u with R(v, u) such that no t i with i ∈ I is Raccessible from u. We must show that there is an R ′ -successor u ′ of v ′ from which no state t ′ i with i ∈ I is R ′ -accessible and which satisfies u ′ Z 1 u. Now, if there was no such state, there would be u ′ with u ′ Z 1 u Tero Tulenheimo can be translated into FOL by the formula ∃y(x < y ∧ P y ∧ ∀z([x < z ∧ z < y] → Qz)). This formula is not in GF: the quantifier ∀z is not guarded in a suitable way. Actually it can be shown that this formula does not even have a translation into GF. While US over arbitrary linear orders is decidable, this cannot, then, be strongly explained with reference to the translatability of ML into GF. This observation need not yet discourage those who see in something like the guarded fragment the key to the explanation of robust modal decidability. For, we may reformulate the strong explanation thesis in terms of LGF instead of GF. Why should this be relevant? As an aside it can be mentioned that LGF over arbitrary models is decidable -a proof sketch was presented in (van Benthem, 1997) -in fact its satisfiability problem is 2EXPTIME-complete (Grädel, 1999a). But this fact is irrelevant here. Write τ = {<, P 1 , . . . , P n }, with < binary and the P j unary. We can only proceed if the logic LGF[τ ] is decidable over structures interpreting '<' as a linear order. But this is the case: actually the full FOL[τ ] is decidable over such structures [START_REF] Ehrenfeucht | Decidability of the theory of the linear ordering relation[END_REF]. Therefore, indeed we may take LGF as strongly explaining the decidability of US over the class of all linear orders. What about the logics K4 n ? Transitivity is not expressible in LGF (Grädel, 1999a), so the translatability of ML into LGF cannot strongly explain the decidability of K4 n for any n ≥ 1. Can the decidability of K4 n be weakly explained with reference to GF or LGF? Let τ k be a vocabulary containing (among other items) the relation symbols R 1 , . . . , R k and write T k for the class of all τstructures that interpret the relation symbols R 1 , . . . , R k by transitive relations. If S 1 , . . . , S k are binary relations, let Trans[S 1 , . . . , S k ] be the statement (not expressible in LGF) that the interpretations of 'S 1 ', 'S 2 ', etc. are transitive. If we take the weak explanation to mean that the satisfiability problem of GF[τ k ] (or that of LGF[τ k ]) is decidable over T k , the answer is in the negative for all k ≥ 2. For, a GF[τ k ] formula ϕ is satisfiable over T k if and only if the statement ϕ ∧ Trans[R 1 , R 2 ] is satisfiable simpliciter. But Grädel has shown that the latter question is undecidable for formulas ϕ ∈ GF[τ 2 ]; see (Grädel, 1999a, proof of Theorem 5.10). In the case of LGF, the answer is known to be negative already for k = 1 (even when there is no equality in the language); see [START_REF] Ganzinger | The two-variable guarded fragment with transitive relations[END_REF]. Let us finally consider giving the following meaning to the notion of weak explanation. Define the guarded fragment with transitive guards, denoted [GF + TG], to be the extension of GF (of a vocabulary without constant symbols) which allows even formulas of the form ϕ ∧ Trans[R 1 , . . . , R k ], provided that in ϕ the binary relation symbols R 1 , . . . , R k occur in guards. Clearly there is a truth-preserving translation of type K4 → [GF + TG]. So it might be suggested that if the satisfiability problem of [GF + TG] is decidable, Tero Tulenheimo 2. Not only is MsL 0 not translatable into FOL 2 , but it cannot be translated into any finite-variable fragment of FOL (Theorem 7.4).

3. There is no truth-preserving translation of MsL 0 into LGF (Theorem 7.5). That is, the translatability of ML into LGF does not strongly explain the decidability of MsL 0 .

On the basis of these three negative properties, it can be said that MsL 0 rather convincingly resists features commonly associated with decidable extensions of ML. This is worth noting, even if it remains quite possible that the translatability of ML into LGF weakly explains the decidability of MsL 0 : the relevance of LGF for the decidability of MsL 0 could still be saved by showing the decidability of the result of extending LGF in the same way as MsL 0 extends ML; cf. the discussion in [START_REF] Tulenheimo | On modal logic, IF logic and IF modal logic[END_REF]. Different formulations of such a 'slashed LGF' (or sLGF) could be proposed, but the most immediate formulation would be as follows. All LGF formulas are formulas of sLGF. Further, suppose a formula φ of sLGF has a subformula φ ′ of the form ∀ x(G → ψ). If here ψ contains a subformula ψ ′ := ∃ y(G ′ ∧ χ) such that in ψ no quantifier syntactically precedes ∃ y, the result of replacing in φ the subformula ψ ′ by the string (∃ y/ x)(G ′ ∧χ) is likewise a formula of sLGF. The semantics of sLGF is obtained from that of FOsL by taking Qx 1 . . . x n to be a shorthand notation for Qx 1 . . . Qx n when Q ∈ {∀, ∃}, and (∃y 1 . . . y m /x 1 . . . x n ) to be an abbreviation of (∃y 1 /x 1 , . . . , x n ) . . . (∃y m /x 1 , . . . , x n ). We leave it as an open question whether the satisfiability problem of sLGF is decidable.

Given that semantically MsL 0 liberalizes certain restrictions inherent in ML, and that it is even most conveniently defined precisely as a result of such liberalization, it does not appear far-fetched to view it as a modal logic, or if more general term is needed, as a modal-like logic. In any case it is obviously an extension of ML. Since it furthermore behaves computationally very well indeed, any proposal purporting to clarify the computational properties of ML and its extensions should also prove to have explanatory power here. However, as just reiterated, none of the suggestions routinely resorted to in the literature in connection with modal logics is applicable (with the possible exception of LGF in the sense of weak explanation).

We conclude by some comments about the negative results ( 2) and (3) listed above. As to finite-variable fragments, we have mentioned Gabbay's lemma to the effect that any finite-dimensional modal logic with finitely many connectives, each with a first-order table, can be translated into FOL n for some n < ω. How does MsL 0 look like from this perspective? Does it have finitely many connectives? Which are its connectives? From the viewpoint of slash logic, the answer to the last Tero Tulenheimo this respect differs from ML on the one hand and GF on the other. Let us say that an atomic formula (or a quantifier) appearing in a formula ψ is ungoverned if in ψ this atom (respectively this quantifier) does not itself appear in the scope of any quantifier in ψ. First note that one way to express the locality of ML is to say that in its standard firstorder translation, (1) any token of a quantifier Qx is associated with a unique formula (G ⋆ ψ) where G is the guard of Qx, (2) the guard is the relativizer of the quantifier, i.e., Qx is actually prefixed to the formula (G ⋆ ψ), and there are strict syntactic restrictions on where the variable x introduced by the quantifier Qx may appear in the formula ψ: (3) x is the only free variable of ψ, and (4) in ψ the variable x may only appear in an ungoverned atomic formula or in the guard of an ungoverned quantifier. Now, if we allow the use of binary syntactic structures in the syntax of first-order logic, then by inspecting the translation explained in the proof of Theorem 7.2, it is readily seen that MsL 0 deviates from ML only in giving up restriction (2) for existential quantifiers. For, in such a translation existential quantifiers may occur in contexts ∃x i 1 . . . ∃x i |S| ∀x(Rx 0 x → C n,S (ξ 1 , . . . , ξ n+1 )), where each ξ i j is of the form (G i j ∧ψ i j ) and the context (G i j ∧ψ i j ) satisfies restrictions (1), ( 3) and ( 4).

The case of MsL 0 suggests, then, that being a relativizer may not be essential for being a guard, insofar as one wishes to consider being guarded as a feature of quantifiers which would explain decidability. On the other hand, MsL 0 retains also the locality properties (3) and (4) of ML, so it is not clear that its decidability can be predicated on its being guarded even in this weaker sense. We may note that from the firstorder perspective, formulas of MsL 0 , like those of ML, serve to impose relational tests on variables introduced by quantifiers, but unlike in the case of ML, in MsL 0 such a test is carried out so to say with a delay: not immediately when a value corresponding to an existentially quantified variable is introduced, but only later it is checked whether this value stands in a suitable relation to a value introduced by the subsequent evaluation of a universal quantifier. For comparison we note that in GF requirements (1) and (2) are retained but constraints (3) and ( 4) are given up in favor of allowing the variable x to appear anywhere in the scope of Qx, as long as G serves to impose an explicit relational condition on x and the free variables of ψ; indeed instead of a single variable x a tuple x of variables is allowed. Logic sLGF, again, results from GF by allowing limited deviations of restriction (2). Should sLGF turn out to be decidable, suitable non-relativizing guards might gain some credibility as features weakly explaining decidability in the realm of modal-like logics.