Stéphane Demri
email: demri@imag.fr

The Nondeterministic Information Logic NIL is PSPACE-complete

Keywords: information system, multimodal logic, computational complexity, Ladner-like algorithm

.

Introduction

Information systems. The information logics derived from Pawlak's information systems [START_REF] Pawlak | Information systems theoretical foundations[END_REF] are intended to be able to reason about information systems. An information system can be seen as a structure OB, AT such that OB is a nonempty set of objects, AT is a nonempty set of attributes and each attribute a ∈ AT , is a mapping a : OB → P(V al a ) \ {∅} where V al a is a nonempty set of values. For each object x and for each attribute a, a(x) can be read as the set of possible values of the attribute a for the object x. In that setting, various derived relations between objects can be defined. We recall some of them below from the literature (see e.g. [START_REF] Or | Introduction: What you always wanted to know about rough sets[END_REF]). For any x 1 , x 2 ∈ OB, A ⊆ AT ,

• x 1 ind(A)x 2 def ⇔ for any a ∈ A, a(x 1 ) = a(x 2 ) (indiscernibility) ;

• x 1 comp(A)x 2 def ⇔ for any a ∈ A, a(x 1 ) = V al a \ a(x 2 ) (complementarity);

• x 1 f in(A)x 2 def
⇔ for any a ∈ A, a(x 1 ) ⊆ a(x 2 ) (forward inclusion);

• x 1 bin(A)x 2 def ⇔ for any a ∈ A, a(x 2 ) ⊆ a(x 1 ) (backward inclusion);

• x 1 sim(A)x 2 def ⇔ for any a ∈ A, a(x 1 ) ∩ a(x 2 ) = ∅ (similarity).

x 1 ind(A)x 2 can be read as follows: the objects x 1 and x 2 cannot be distinguished modulo the set of attributes A. Similarly, x 1 sim(A)x 2 iff x 1 and x 2 are similar modulo A. The other relations comp(A), f in(A) and bin(A) admit a reading in the same vein. The polymodal logics obtained from the information systems are multimodal logics such that the relations in the Kripke-style semantical structures correspond to relations between objects in the underlying information systems. The first information logic has been introduced in [START_REF] Or | Expressive power of knowledge representation system[END_REF] and many others appeared later (see e.g. [START_REF] Del Cerro | DAL -A logic for data analysis[END_REF][START_REF] Vakarelov | Modal logics for knowledge representation systems[END_REF]1,[START_REF] Konikowska | A logic for reasoning about relative similarity[END_REF][START_REF] Vakarelov | Information systems, similarity and modal logics[END_REF][START_REF] Demri | Relative similarity logics are decidable: reduction to FO 2 with equality[END_REF]). The information logic NIL (introduced in [START_REF] Or | Representation of nondeterministic information[END_REF]) is remarkable among the class of information logics. Indeed, in 1987, Vakarelov [START_REF] Vakarelov | Abstract characterization of some knowledge representation systems and the logic NIL of nondeterministic information[END_REF] provides the first first-order characterization of structures derived from information systems and this has been done with the semantical structures of NIL. The NIL semantical structures contain not only forward and backward inclusions derived relations but also the similarity relation. More precisely, the NIL frames are all the structures OB, f in(AT ), bin(AT ), sim(AT ) derived from some information system OB, AT . Actually, in [START_REF] Vakarelov | Abstract characterization of some knowledge representation systems and the logic NIL of nondeterministic information[END_REF], it has been shown that in order to define NIL an additional condition (not present in [START_REF] Or | Representation of nondeterministic information[END_REF]) between forward inclusion and similarity needs to be taken into account (the forthcoming condition (N4)).

Our contribution. The main contribution of the paper is to fully characterize the computational complexity of NIL satisfiability. Actually, we show that NIL satisfiability is a PSPACEcomplete problem (see e.g. [START_REF] Ch | Computational Complexity[END_REF] for a thorough introduction to complexity theory). So, NIL satisfiability captures the difficulty of the whole complexity class PSPACE that is the class of (decision) problems that can be solved by a deterministic Turing machine in polynomial space in the length of the input string. PSPACE-hardness with respect to logarithmic space transformations is shown to be an easy consequence of PSPACE-hardness of the well-known modal logic S4 [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF]. The main difficulty is to show that NIL satisfiability is in PSPACE. To do so we present an original construction that extends various previous works in [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF][START_REF] Halpern | A guide to completeness and complexity for modal logics of knowledge and belief[END_REF][START_REF] Spaan | The complexity of propositional tense logics[END_REF]. The technique can be extended to other information logics (and polymodal logics with interdependent modal connectives) and this shall be the topic of forthcoming papers. Moreover, the analysis developed in the paper could be easily plug into a labelled tableaux calculus for NIL. Such a calculus is not difficult to define following for instance [2,[START_REF] Demri | Sequent calculi for nominal tense logics: a step towards mechanization[END_REF][START_REF] Vigano | Labelled Non-Classical Logics[END_REF].

Related work. The procedure designed in this paper has a direct filiation with the works of Ladner [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF], Halpern and Moses [START_REF] Halpern | A guide to completeness and complexity for modal logics of knowledge and belief[END_REF] and Spaan [START_REF] Spaan | The complexity of propositional tense logics[END_REF]. Indeed, we shall use a tableau-based procedure to show that we do not need more than polynomial space to check NIL satisfiability. We cannot take advantage of [START_REF] Hemaspaandra | Complexity transfer for modal logic (extended abstract)[END_REF] where the complexity of join modal logics is characterized (NIL contains interdependent modal connectives). The detection of cycles for S4 modalities in NIL is similar to the proof-theoretical results from [START_REF] Cerrito | A polynomial translation of S4 into T and contractionfree tableaux for S4[END_REF] that is related to the techniques from [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF][START_REF] Fitting | First-order modal tableaux[END_REF]. Other proof-theoretical analysis about complexity issues for modal logics can be found in [START_REF] Massacci | Single steps tableaux for modal logics[END_REF][START_REF] Vigano | Labelled Non-Classical Logics[END_REF].

Definition of NIL and PSPACE-hardness

For any set X, we write X * [resp. X + ] to denote the set of [resp. nonempty] finite strings built from elements of X. For any finite string s, we write |s| [resp. last(s)] to denote its length [resp. the last element of s, if any]. For any s ∈ X * , we write s k to denote the string composed of k copies of s. For instance, (bin

• f in) 2 = bin • f in • bin • f in and |(bin • f in) 2 | = 4.
Given a countably infinite set For 0 = {p 0 , p 1 , p 2 , . . .} of propositional variables the NILformulae φ are inductively defined as follows:

φ ::= p k | φ 1 ∧ φ 2 | ¬φ | [≤]φ | [≥]φ | [σ]φ
for p k ∈ For 0 . We write |φ| to denote the length of the formula φ, that is the length of the string φ ([≥], [≤] and [σ] count here for one symbol). We write md(φ) to denote the modal degree of φ, that is the modal depth of φ. md is naturally extended to finite sets of formulae, understood as conjunctions and by convention md

(∅) = 0. For R ∈ {σ, ≤, ≥}, [R] i φ is inductively defined as follows: [R] 0 φ = φ and [R] i+1 φ = [R][R] i φ for i ≥ 1. For s ∈ {[≤], [≥], [σ]} * , an s-formula is defined as a formula prefixed by s. For instance, [σ][≤][≥]p 0 is a [σ][≤]-formula. A NIL-model M is a structure M = W, R ≤ , R ≥ , R σ ,
m such that W is a nonempty set, m assigns to each propositional variable a subset of W and R ≤ , R ≥ , R σ are binary relations on W such that

(N1) R ≤ = (R ≥ ) -1 , that is R ≤ is the converse of R ≥ ; (N2) R ≤ is reflexive and transitive; (N3) R σ is reflexive and symmetric; (N4) If x, y ∈ R σ , x, x ∈ R ≤ and y, y ∈ R ≤ , then x , y ∈ R σ .
Observe that in any NIL-model, we have (R ≤ ∪R ≥ ) ⊆ R σ . The condition (N4) was not originally in the logic NIL defined in [START_REF] Or | Representation of nondeterministic information[END_REF] but it appeared in [START_REF] Vakarelov | Abstract characterization of some knowledge representation systems and the logic NIL of nondeterministic information[END_REF] for the first-order characterization of the structures OB, f in(AT ), bin(AT ), sim(AT )

where OB, AT is an information system. The condition (N4) is mainly responsible for the difficulty in showing that NIL satisfiability is in PSPACE. Conditions (N2) and (N4) can be equivalently replaced by (N2 ) R ≥ is reflexive and transitive;

(N4 ) If x, y ∈ R σ and y, y ∈ R ≤ , then x, y ∈ R σ .

The condition (N4 ) can be read as a pseudo transitivity condition involving two binary relations. Transitivity of R ≤ and R ≥ requires a specific treatment in order to show that NIL-satisfiability is in PSPACE. We apply a method of detection of cycles known in the literature (see [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF][START_REF] Spaan | The complexity of propositional tense logics[END_REF]).

As is usual for modal logics, the formula φ is satisfied by the world w ∈ W in M def ⇔ M, w |= φ where the satisfaction relation |= is inductively defined as follows:

• M, w |= p def ⇔ w ∈ m(p), for every propositional variable p;

• M, w |= [≤]φ def ⇔ for every w ∈ R ≤ (w), M, w |= φ; • M, w |= [≥]φ def ⇔ for every w ∈ R ≥ (w), M, w |= φ; • M, w |= [σ]φ def ⇔ for every w ∈ R σ (w), M, w |= φ.
We omit the standard conditions for the propositional connectives. A formula φ is said to be NIL-satisfiable def ⇔ there is a NIL-model M = W, R ≤ , R ≥ , R σ , m and w ∈ W such that M, w |= φ. An Hilbert-style system can be easily designed for NIL in which all the modal axiom schemes are Sahlqvist formulae (see e.g. [START_REF] Sahlqvist | Completeness and correspondence in the first and second order semantics for modal logics[END_REF]). Similarly, prefixed tableaux calculi and cut-free display calculi can be defined for NIL using the general results from [START_REF] Kracht | Power and weakness of the modal display calculus[END_REF]2]. Moreover, a linear-time transformation from NIL satisfiability problem into the fragment of first-order logic with three individual variables can be given by using the standard translation from modal logics into classical logic (see e.g. [3]). Although this fragment of classical logic is known to be undecidable, the results in the paper can be viewed as an explanation for the decidability (and indeed PSPACE-completeness) of the exact fragment of first-order logic with three individual variables delineated by the translation from NIL. However, the complexity of NIL satisfiability is really a problematic issue since NIL contains interdependent modal connectives. A complexity lower bound can be easily established since NIL can be viewed as an extension of S4.

Theorem 2.1. NIL satisfiability is logarithmic space hard in PSPACE.

Proof: Let X be the set of NIL satisfiable formulae φ such that neither [σ] nor [≥] occurs in φ. We shall show that X is the set of S4 satisfiable formulae modulo the replacement of [≤] by the standard modal connective []. Since S4 satisfiability is logarithmic space hard in PSPACE [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF], so is NIL satisfiability. If φ ∈ X, then φ is S4 satisfiable since by removing from a NIL-model for φ the components R σ and R ≥ we get an S4-model. Moreover, if φ is S4 satisfiable, then there exist an S4-model

M = W, R, m and w ∈ W verifying M, w |= φ. Let M = W, R ≤ , R ≥ , R σ , m be the NIL-model such that R ≤ def = R, R ≥ def = R -1 (the converse of R) and R σ def = W × W . Obviously M , w |= φ (modulo the replacement of [≤] by []) and M is indeed a NIL-model.
What is done in the proof of Theorem 2.1 at the level of Kripke-style structures can be also interpreted at the level of information systems. Indeed, let S = OB, AT and S = OB, AT be information systems such that

• AT def = {a : a ∈ AT }; • for a ∈ AT , V al a def = V al a ∪ {Dummy} with Dummy ∈ {V al a : a ∈ AT }; • for a ∈ AT and x ∈ OB, a (x) def = a(x) ∪ {Dummy}.
One can easily check that f in(AT ) = f in(AT ) and sim(AT ) = OB × OB, that is the S4-frame OB, f in(AT ) can be extended to the NIL-frame OB, f in(AT ), bin(AT ), sim(AT ) where sim(AT ) is the universal relation OB × OB.

Results from [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF][START_REF] Spaan | The complexity of propositional tense logics[END_REF][START_REF] Chen | The computational complexity of the satisfiability of modal Horn clauses for modal propositional logics[END_REF][START_REF] Marx | Complexity of modal logics of relations[END_REF] easily entail the following: It remains to show that NIL satisfiability with the three modal connectives [≤], [≥] and [σ] living together and interacting, is also in PSPACE. To do so, we shall follow the proof technique from [START_REF] Spaan | The complexity of propositional tense logics[END_REF] and we propose substantial modifications in order to cope with the much more difficult NIL case. It is worth mentioning that interactions between modal connectives can lead to an increase of computational complexity. K-satisfiability and S5-satisfiability are in PSPACE and in NP, respectively [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF]. However, the bimodal logic with an S5 modal connective [1] and with a K modal connective [2] such that [1]φ ⇒ [2]φ is an additional axiom has an EXPTIME-hard satisfiability problem [START_REF] Hemaspaandra | The price of universality[END_REF]. This is well-known that the axiom schema [1]

φ ⇒ [2]φ corresponds to the semantical condition R 2 ⊆ R 1 where R i is the accessibility relation associated to the modal operator [i] (i = 1, 2).

Preliminary results

In Definition 3.1 below, we introduce a closure operator for sets of NIL-formulae as it is done for Propositional Dynamic Logic PDL by Fischer and Ladner in [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF]. Definition 3.1. Let X be a set of NIL-formulae. Let cl(X) be the smallest set of formulae such that:

• X ⊆ cl(X); • if ¬φ ∈ cl(X), then φ ∈ cl(X); • if φ 1 ∧ φ 2 ∈ cl(X), then φ 1 , φ 2 ∈ cl(X); • if [≤]φ ∈ cl(X), then φ ∈ cl(X); • if [≥]φ ∈ cl(X), then φ ∈ cl(X); • if [σ]φ ∈ cl(X), then [≥]φ ∈ cl(X); • if [σ]φ ∈ cl(X) and φ is not a [≤]-formula, then [σ][≤]φ ∈ cl(X); • if [σ][≤]φ ∈ cl(X), then [σ]φ ∈ cl(X). Consequently, if [σ]φ ∈ cl(X) and φ is not a [≤]-formula, then [≤]φ ∈ cl(X) and if [σ]φ ∈ cl(X), then φ ∈ cl(X). A set X of formulae is said to be closed def ⇔ cl(X) = X.
For any finite set X of formulae, we have md(cl(X)) ≤ md(X) + 1. Moreover, for any formula ψ,

md([≤]ψ) = md([≥]ψ) = md(cl({[≤]ψ})) = md(cl({[≥]ψ})).
Lemma 3.1. Let φ be a formula. Then, card(cl({φ})) < 5 × |φ|.

Proof:

Let sub(φ) be the set of subformulae of the formula φ. Obviously, sub(φ) ⊆ cl({φ}). Moreover, cl({φ}) is the union of the following sets:

1. sub(φ); 2. {[≥]ψ : [σ]ψ ∈ sub(φ)}; 3. {[≥]ψ : [σ][≤] n ψ ∈ sub(φ), n ≥ 1}; 4. {[≥][≤]ψ : [σ]ψ ∈ sub(φ), ψ = [≤]ψ }; 5. {[σ][≤]ψ : [σ]ψ ∈ sub(φ), ψ = [≤]ψ }; 6. {[σ]ψ : [σ][≤] n ψ ∈ sub(φ), n ≥ 1}; 7. {[≤]ψ : [σ]ψ ∈ sub(φ), ψ = [≤]ψ }.
Each set above is of the cardinality at most card(sub(φ)) and a formula in sub(φ) can generate at most four formulae in cl({φ}). So card(cl({φ})) < 5 × |φ|, since card(sub(φ)) < |φ|.

In order to determine the NIL satisfiability of some formula φ, we need to handle sets of formulae. All those sets shall be subsets of cl({φ}). In establishing the PSPACE complexity upper bound, the fact that cl({φ}) is finite and its cardinality is linear in the size of φ plays an important role.

In order to check whether φ is NIL-satisfiable, we build sequences of the form

X 0 x 0 X 1 x 1 X 2 x 2 . . .
where φ ∈ X 0 ⊆ cl({φ}) and for i ∈ ω, X i is a consistent subset of cl({φ}) and x i ∈ {σ, ≤, ≥}. We extend a finite sequence X 0 x 0 X 1 x 1 . . . x i-1 X i with x i X i+1 whenever we need a witness of [x i ]ψ ∈ X i for some formula ψ (and ψ ∈ X i+1 ). The intention is to build paths in some NIL model

M = W, R ≤ , R ≥ , R σ , m such that for i ∈ ω, there is w i ∈ W such that M, w i |= ψ iff ψ ∈ X i and w i , w i+1 ∈ R x i .
This roughly corresponds to the exploration of a branch in the depth-first proof search for a tableaux-style calculus. In order to avoid confusion, σ [resp. ≤, ≥] shall be written sim [resp. f in, bin].

In order to establish termination of the proof of building sequences, which is a necessary step to obtain the PSPACE complexity upper bound, we define subsets cl(s, φ) ⊆ cl({φ}) for s ∈ {sim, f in, bin} * such that for i ∈ ω,

X i ⊆ cl(x 0 . . . x i-1 , φ)
For s ∈ {sim, f in, bin} * and x ∈ {sim, f in, bin} cl(s • x, φ) contains all the formulae ψ which we could possibly be put in X i+1 for ψ ∈ cl(x 0 . . . x i-1 , φ).

We will get termination if there is some computable map f : ω → ω such that for |s| ≥ f (|φ|), cl(s, φ) = ∅. To establish the PSPACE complexity upper bound, f should preferably be bounded by a polynomial. Those general principles may look quite attractive but in concrete examples of modal logics they are seldom sufficient to show that the satisfiability problem is in

PSPACE. Since transitivity of R ≤ is required, if [≤]ψ ∈ X i , then M, w i |= [≤]ψ, M, w i |= [≤ ][≤]ψ and therefore one can expect that [≤]ψ ∈ X i+1 if x i = f in. So the formula [≤]ψ ∈ X i
should be propagated for any "fin" transition. However, this does not guarantee termination. Actually, as already known from [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF][START_REF] Spaan | The complexity of propositional tense logics[END_REF][START_REF] Cerrito | A polynomial translation of S4 into T and contractionfree tableaux for S4[END_REF], duplicates can be identified in X 0 x 0 X 1 x 1 X 2 x 2 . . . which corresponds to a cycle detection (see also [START_REF] Fitting | Proof methods for modal and intuitionistic logics[END_REF]). Since card(P(cl({φ}))) is in O(2 |φ| ), a finer analysis is necessary to establish the PSPACE complexity upper bound as done in [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF] (see also [START_REF] Spaan | The complexity of propositional tense logics[END_REF] for the tense extension of Ladner's solution). Things are even worse. since by (N4),

if [σ]ψ ∈ X i , then M, w i |= [σ]ψ and M, w i |= [≥] n [σ][≤] n ψ for n, n ≥ 0. One can expect that [≥] n-1 [σ][≤] n ψ ∈ X i+1 if x i =
bin and n ≥ 1. This is not a good perspective for termination and in this paper we shall also provide a technical answer to this problem. We omit at this stage of the paper, the complications caused by having a symmetric relation in the NIL models.

In order to conclude this introductory part that motivates the existence of the sets of the form cl(s, φ), let us say that once the set X i of formulae is built and x i is chosen, the set X i+1 satisfies:

1. X i+1 is a consistent subset of cl(x 0 . . . x i , φ); 2. X i , X i+1 satisfies a certain condition (to be specified in the sequel) that shall guarantee that M is a NIL model and w i , w i+1 ∈ R x i .

Definition 3.2. Let φ be a formula. For s ∈ {sim, f in, bin} * , let cl(s, φ) be the smallest set such that:

1. cl(λ, φ) = cl({φ}); 2. cl(s, φ) is closed; 3. if [σ][≤]ψ ∈ cl(s, φ), then [≤]ψ ∈ cl(s • sim, φ); 4. if [≤]ψ ∈ cl(s, φ), then [≤]ψ ∈ cl(s • f in, φ); 5. if [≥]ψ ∈ cl(s, φ), then [≥]ψ ∈ cl(s • bin, φ); 6. if [σ][≤]ψ ∈ cl(s, φ), then [σ][≤]ψ ∈ cl(s • bin, φ). Example 3.1. Let φ be the formula [σ]p 0 . We have cl(λ, φ) = cl({φ}) = {[σ]p 0 , p 0 , [≥]p 0 , [σ][≤]p 0 , [≥][≤]p 0 , [≤]p 0 }
Below are some examples of sets of the form cl(s, φ):

• cl(bin, φ) = cl({φ});

• cl(bin • sim, φ) = {p 0 , [≤]p 0 }; • cl(bin • sim • f in, φ) = {p 0 , [≤]p 0 }; • cl(bin • sim • f in • bin, φ) = ∅.
One can check that for any s ∈ {sim, bin, f in} * such that |s| ≥ 4, we have cl(s, φ) = ∅.

Lemma 3.2 contains some basic properties of the sets cl(s, φ).

Lemma 3.2. Let φ be a formula and s, s ∈ {sim, f in, bin} * such that s is a prefix of s . Then, (I) cl(s , φ) ⊆ cl(s, φ);

(II) if [σ]ψ ∈ cl(s, φ), then ψ ∈ cl(s • sim, φ); (III) if [σ]ψ ∈ cl(s, φ), then [σ]ψ ∈ cl(s • bin, φ); (IV) if [≤]ψ ∈ cl(s • bin, φ), then md([≤]ψ) < md(cl(s • bin, φ)).
Proof:

(I) This is immediate by Definition 3.2, since both cl(s, φ) and cl(s , φ) are closed.

(II) Let [σ]ψ ∈ cl(s, φ). If ψ = [≤]ψ , then by definition ψ ∈ cl(s • sim, φ). If ψ = [≤]ψ , then since cl(s, φ) is closed, [σ][≤]ψ ∈ cl(s, φ). By definition, [≤]ψ ∈ cl(s • sim, φ). Since cl(s • sim, φ) is closed, ψ ∈ cl(s • sim, φ). (
[σ][≤]ψ ∈ cl({[≥]ψ }) ⊆ cl(s • bin, φ). Hence, md([≤]ψ) < md(cl(s • bin, φ)). Case 2: [≤]ψ ∈ cl({[σ][≤]ψ }) for some [σ][≤]ψ ∈ cl(s, φ) (see Definition 3.2(6)).
Thus,

• [≤]ψ ∈ cl({[≤]ψ }); and • md([≤]ψ) ≤ md([≤]ψ ) = md(cl({[≤]ψ })). Hence, md([≤]ψ) ≤ md([≤]ψ ) < md([σ][≤]ψ ) ≤ md(cl(s • bin, φ)).
Lemma 3.3 below is crucial to prove forthcoming Theorem 3.1 and this is the cornerstone for termination of the procedure defined in Section 4.1. It states sufficient conditions on the string s to guarantee that the modal degree of cl(s • s , φ) is strictly less than the modal degree of cl(s, φ). Lemma 3.3. Let φ be a formula, s ∈ {sim, f in, bin} * and s ∈ {bin•f in•bin, f in•bin•f in, sim}. Then, md(cl(s • s , φ)) ≤ max(0, md(cl(s, φ)) -1).

Proof:

Assume that md(cl(s, φ)) ≥ 1, otherwise the proof is immediate by Lemma 3.2(I). Let ϕ ∈ cl(s, φ) be such that md(ϕ) = md(cl(s, φ)). Let us show that ϕ ∈ md(cl(s • s , φ)). By Lemma 3.2(I) we are done. We distinguish cases according to the value of s .

Case 1: s = f in • bin • f in Case 1.1: the outermost connective of ϕ is in {∧, ¬}. By Definition 3.2, we have ϕ ∈ cl(s • f in, φ) iff there is [≤]ψ ∈ cl(s, φ) such that ϕ ∈ cl({[≤]ψ}). Suppose ϕ ∈ cl(s • f in, φ). ϕ can only be a proper subformula of [≤]ψ. But then md(ϕ) < md([≤ ]ψ), a contradiction. Hence, ϕ ∈ cl(s • f in, φ) and therefore ϕ ∈ cl(s • s , φ). Case 1.2: ϕ = [σ][≤]ϕ . Suppose ϕ ∈ cl(s•f in, φ) (otherwise ϕ ∈ cl(s•s , φ) by Lemma 3.2(I)). By Definition 3.2(4), there is [≤]ψ ∈ cl(s, φ) such that ϕ ∈ cl({[≤]ψ}). [σ][≤]ϕ cannot be a subformula of [≤]ψ, otherwise md([σ][≤]ϕ ) < md([≤]ψ) (see the point 1. in the proof of Lemma 3.1). Similarly, [σ][≤] n+1 ϕ is not a subformula of [≤]ψ with n ≥ 1 (see the point 3. in the proof of Lemma 3.

2) by maximality of md(ϕ). The only remaining possibility is that

[σ]ϕ is a subformula of [≤]ψ and ϕ is not a [≤]-formula. Hence, md([≤]ψ) = md(ϕ). Now since ϕ ∈ cl(s • f in • bin, φ), md(ϕ) = md(cl(s • f in • bin, φ)). By Lemma 3.2(IV), for any [≤]ψ in cl(s, φ) such that md([≤]ψ ) = md(cl(s, φ)), we have [≤]ψ ∈ cl(s•f in•bin, φ). In particular, [≤]ψ ∈ cl(s•f in•bin, φ). We can now in position to conclude the present case. [σ][≤]ϕ ∈ cl(s • s , φ) iff there is [≤]ψ ∈ cl(s • f in • bin, φ) such that [σ][≤]ϕ ∈ cl({[≤]ψ }) (see Definition 3.

2(4)). Suppose [σ][≤]ϕ ∈ cl(s • s , φ). So md([σ][≤]ϕ ) = md([≤]ψ ) and from the above developments, we can conclude that

[≤]ψ ∈ cl(s • f in • bin, φ), a contradiction. Case 1.3: ϕ = [≤]ϕ . So ϕ ∈ cl(s • f in, φ). Now suppose ϕ ∈ cl(s • f in • bin, φ). By Lemma 3.2(IV), md(ϕ) < md(cl(s • f in • bin, φ)). By Lemma 3.2(I), md(cl(s • f in • bin, φ)) ≤ md(cl(s, φ)) So, md(ϕ) < md(cl(s, φ)), a contradiction. Case 1.4: ϕ = [≥]ϕ . Assume ϕ ∈ cl(s • f in, φ) (otherwise ϕ ∈ cl(s • s , φ) by Lemma 3.2(I)). So, there is [≤]ψ ∈ cl(s, φ) such that ϕ ∈ cl({[≤]ψ}). So md([≤]ψ) = md(ϕ).
Since md(ϕ) = md(cl(s, φ)), ϕ cannot be a subformula of [≤]ψ (see the point 1. in the proof of Lemma 3.1). Similarly, there is no subformula [σ][≤] n ϕ of [≤]ψ for some n ≥ 1 (see the point 3. in the proof of Lemma 3.1) by maximality of md(ϕ). ϕ can only be of the form

[≥][≤]ϕ for some subformula [σ]ϕ of [≤]ψ such that ϕ is not a [≤]-formula. So ϕ ∈ cl(s • f in • bin, φ). By Lemma 3.2(IV), [≤]ψ ∈ cl(s • f in • bin, φ). Otherwise, we have md(ϕ) = md([≤]ψ) = md(cl(s • f in • bin, φ))
Actually, for any formula

[≤]ψ ∈ cl(s, φ) such that md([≤]ψ ) = md(cl(s, φ)), we have [≤]ψ ∈ cl(s • f in • bin, φ). Now, [≥][≤]ϕ ∈ cl(s • f in • bin • f in, φ) iff there is [≤]ψ ∈ cl(s • f in • bin, φ) such that [≥][≤]ϕ ∈ cl({[≤]ψ }) (see Definition 3.2(4)). Analogously, we can conclude that [σ]ϕ is a subformula of [≤]ψ . Suppose [≥][≤]ϕ ∈ cl(s • f in • bin • f in, φ)
. By Lemma 3.2(I), we have cl(s • f in • bin, φ) ⊆ cl(s, φ) and therefore [≤]ψ ∈ cl(s, φ) and md([≤]ψ ) = md(ϕ) which leads to a contradiction from the above developments. Thus, Theorem 3.2. Let f : ω → ω be a computable map, φ be a formula and s ∈ {sim, f in, bin} * be such that neither bin k+1 nor f in k+1 is a substring of

[≥][≤]ϕ ∈ cl(s • f in • bin • f in, φ). Case 2: s = bin • f in • bin Case 2.1: the outermost connective of ϕ is in {∧, ¬}. See the Case 1.1. Case 2.2: either ϕ = [σ][≤]ϕ or ϕ = [≥]ϕ (see Definition 3.2(5-6)). So ϕ ∈ cl(s • bin, φ). Suppose ϕ ∈ cl(s • bin • f in, φ) (otherwise ϕ ∈ cl(s • s , φ)). So there is [≤]ψ ∈ cl(s•bin, φ) such that ϕ ∈ cl({[≤]ψ}) (see Definition 3.2(4)). Since md(ϕ) = md(cl(s, φ)), md([≤]ψ) = md(ϕ). By Lemma 3.2(IV), md(ϕ) < md(cl(s • bin, φ)), a contradiction. Case 2.3: ϕ = [≤]ϕ . Suppose ϕ ∈ cl(s • bin, φ). By Lemma 3.2(IV), md(ϕ) < md(cl(s • bin, φ)) ≤ md(cl(s, φ)), a contradiction. Case 3: s = sim Suppose ϕ ∈ cl(s • sim, φ). By Definition 3.2(3), ϕ ∈ cl(s • sim, φ) iff there is [σ][≤]ψ ∈ cl(s, φ) such that ϕ ∈ cl({[≤]ψ}). Observe that md([≤]ψ) = md(cl({[≤]ψ})) < md([σ][≤]ψ). Hence md(ϕ) < md(cl({[≤]ψ})), a contradiction.
s for k ≥ f (|φ|) and |s| ≥ 3 × |φ| × f (|φ|). Then cl(s, φ) = ∅.
Theorem 3.1 is a particular case of Theorem 3.2 where f is the constant map 1. The proof of Theorem 3.2 also uses the property that cl(s

• bin k , φ) = cl(s • bin, φ) [resp. cl(s • f in k , φ) = cl(s • f in, φ)] for k ≥ 1.
It is legitimate to wonder whether Theorem 3.1 is optimal. We show that we can hardly do better: the factor 3 cannot be replaced by the factor 2. Lemma 3.4. For n ∈ ω, there exist a formula φ n and s n ∈ {sim, bin, f in} * such that

• md(φ n ) = n + 1 and |φ n | = n + 3; • neither bin • bin nor f in • f in occurs in s n ; • |s n | = 3 × n + 1; • cl(s n , φ n ) = ∅. Proof: Let us define φ n def = [≤][σ] n p 0 and s n def = (f in • bin • sim) n • f in. Let us show that cl(s n , φ n ) = ∅.
To do so, we prove that for i ∈ {0, . . . , n},

[≤][σ] i p 0 ∈ cl((f in • bin • sim) n-i , φ n ). Base case: i = n. [≤][σ] n p 0 ∈ cl(λ, φ n ).

Induction step: Let us take as an induction hypothesis that

[≤][σ] i+1 p 0 ∈ cl((f in•bin•sim) n-i-1 , φ n ) for some i ≥ 0. It follows that • [≤][σ] i+1 p 0 ∈ cl((f in • bin • sim) n-i-1 • f in, φ n ); • [σ] i+1 p 0 ∈ cl((f in • bin • sim) n-i-1 • f in, φ n ); • [σ][≤][σ] i p 0 ∈ cl((f in • bin • sim) n-i-1 • f in, φ n ); • [σ][≤][σ] i p 0 ∈ cl((f in • bin • sim) n-i-1 • f in • bin, φ n ); • [≤][σ] i p 0 ∈ cl((f in • bin • sim) n-i-1 • f in • bin • sim, φ n ). Hence, [≤]p 0 ∈ cl((f in • bin • sim) n , φ n ) and [≤]p 0 ∈ cl((f in • bin • sim) n • f in, φ n ).
Definition 3.3. The binary relation ≈ on sets of NIL-formulae is defined as follows: if last(Σ) is not s-consistent, then return false;

X ≈ Y def ⇔ 1. for all [σ]ψ ∈ X, ψ ∈ Y ; 2. for all [σ]ψ ∈ Y , ψ ∈ X.

The binary relation is defined as follows

: X Y def ⇔ 1. for all [≤]ψ ∈ X, [≤]ψ, ψ ∈ Y ; 2. for all [≥]ψ ∈ Y , [≥]ψ, ψ ∈ X; 3. for all [σ]ψ ∈ Y , [σ]ψ ∈ X. Let clos be the set of subsets Y of cl({φ}) such that for R ∈ {σ, ≥, ≤}, [R]ψ ∈ Y implies ψ ∈ Y .
for [σ]ψ ∈ cl(s, φ) \ last(Σ) do for each X ψ ⊆ cl(s • sim, φ) \ {ψ} such that last(Σ) ≈ X ψ , call NIL-WORLD(X ψ , s • sim, φ).
If all these calls return false, then return false;

for [≤]ψ ∈ cl(s, φ) \ last(Σ) do if there is no X ∈ Σ such that ψ ∈ X, last(Σ) X, and last(s) = f in, then for each X ψ ⊆ cl(s • f in, φ) \ {ψ} such that last(Σ) X ψ , if last(s) = f in, then call NIL-WORLD(Σ • X ψ , s, φ), otherwise call NIL-WORLD(X ψ , s • f in, φ
). If all these calls return false, then return false;

for [≥]ψ ∈ cl(s, φ) \ last(Σ) do if there is no X ∈ Σ such that ψ ∈ X, last(Σ) X, and last(s) = bin, then for each X ψ ⊆ cl(s • bin, φ) \ {ψ} such that X ψ last(Σ), if last(s) = bin, then call NIL-WORLD(Σ • X ψ , s, φ), otherwise call NIL-WORLD(X ψ , s • bin, φ).
If all these calls return false, then return false; Return true. The function NIL-WORLD is actually defined on the model of the function K-WORLD in [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF] and it is an extension of the function S4 t -WORLD defined in [START_REF] Spaan | The complexity of propositional tense logics[END_REF] (see also [START_REF] Donini | The complexity of concept languages[END_REF][START_REF] Massacci | Single steps tableaux for modal logics[END_REF][START_REF] Vigano | Labelled Non-Classical Logics[END_REF]). The results given in Section 3 are crucial to guarantee that NIL-WORLD is correct and terminates. By a successful call of NIL-WORLD(Σ, s, φ) we mean that it returns true.

Termination and complexity upper bounds

If NIL-WORLD correct, then for any formula φ, φ is NIL satisfiable iff there is X ⊆ cl({φ}) such that φ ∈ X and NIL-WORLD(X, λ, φ) returns true. Each subset X ⊆ cl({φ}) can be represented as a bitstring of length 5 × |φ| since card(cl(φ)) < 5 × |φ|. At each level of the recursion, we use space in O(|φ|) by implementing Σ as a global stack. For instance, in the parts of NIL-WORLD of the form "'for each X ψ . . . then return false", the implementation uses a bitstring of length 5 × |φ| to encode X ψ and a Boolean indicating whether a call has returned true.

Suppose that in the call of NIL-WORLD(X, λ, φ) at some recursion depth, NIL-WORLD(Σ, s, φ) is called with Σ = X 1 • . . . • X n , n ≥ 2. We treat the case s = s • f in and the case s = s • bin 1. either (a) last(Σ) = X;

(b) NIL-WORLD(Σ, s, φ) calls NIL-WORLD(Σ , s , φ) successfully in the "fin" [resp. "bin"] segment of NIL-WORLD(Σ, s, φ);

(c) last(Σ ) = X .
2. or there is a finite sequence Σ 1 , s 1 , . . . , Σ k , s k such that:

(a) last(Σ k ) = X; last(Σ 1 ) = X ; (b) Σ k = Σ; s k = s; s 1 = s ; (c) for i ∈ {1, . . . , k}, last(Σ i ), s i ∈ W ; (d) for i ∈ {1, . . . , k -1}, NIL-WORLD(Σ i , s i , φ) calls NIL-WORLD(Σ i+1 , s i+1 , φ) in the "fin" [resp. "bin"] segment of NIL-WORLD and both NIL-WORLD(Σ i , s i , φ) and NIL-WORLD(Σ i+1 , s i+1 , φ) return true; (e) the call NIL-WORLD(Σ k , s k , φ) enters in the "'fin" [resp. "bin"] segment of NIL-WORLD, last(s k ) = f in [resp. last(s k ) = bin],
and for some formula

[≤]ψ ∈ cl(s, φ) \ X [resp. [≥]ψ ∈ cl(s, φ) \ X], ψ ∈ X and X X [resp. X X ].
The definition of M can be now completed:

• R ≤ def = (R f in ∪ R -1 bin ) * ; • R ≥ def = (R bin ∪ R -1 f in ) * ; • R σ def = R ≥ • (R sim ∪ R -1 sim ∪ { X, s , X, s : X, s ∈ W }) • R ≤ ; • for p ∈ For 0 , m(p) def = { X, s ∈ W : p ∈ X}.
is easy to see that R ≤ and R ≥ are reflexive and transitive relations and R ≥ is the converse of R ≤ . Moreover, it is easy to show that R σ is reflexive and symmetric and

R ≥ • R σ • R ≤ ⊆ R σ .
So, M is NIL-model and W is of cardinality 2 O(|φ|) . One can show:

(i) X, s (R f in ∪ R -1 bin ) X , s implies X X ; (ii) X, s (R bin ∪ R -1 f in ) X , s implies X X; (iii) X, s (R sim ∪ R -1 sim ∪ { X, s , X, s : X, s ∈ W }) X , s implies X ≈ X .
So, (iv) X, s R ≤ X , s implies for all [≤]ψ ∈ X, ψ ∈ X (by definition of );

(v) X, s R ≥ X , s implies for all [≥]ψ ∈ X, ψ ∈ X (by definition of );

(vi) X, s R σ X , s implies for all [σ]ψ ∈ X, ψ ∈ X (by definition of ≈ and by Lemma 3.6(I)).

By induction on the structure of ψ we shall show that for all X, s ∈ W , for all ψ ∈ cl(s, φ), ψ ∈ X iff M, X, s |= ψ. The case when ψ is a propositional variable is by definition of m. Induction hypothesis: for all ψ ∈ cl({φ}) such that |ψ| ≤ n, for all X, s ∈ W , if ψ ∈ cl(s, φ), then ψ ∈ X iff M, X, s |= ψ.

Let ψ be a formula in cl({φ}) such that |ψ| ≤ n + 1. The cases when the outermost connective of ψ is Boolean is a consequence of the s-consistency of X and the induction hypothesis. Let us treat the other cases.

Case 1: ψ = [≤]ψ . Let X, s ∈ W such that ψ ∈ cl(s, φ). By definition of W , there is a sequence Σ such that last(Σ) = X and NIL-WORLD(Σ, s, φ) returns true. If ψ ∈ X one of the following two cases occurs.

Case 1.1: there is X in Σ such that X X , ψ ∈ X and last(s) = f in. By definition of W , there is a subsequence Σ of Σ and s such that last(Σ ) = X and NIL-WORLD(Σ , s , φ) returns true (see the conditions 3. and 4. defining W ). Hence, we have X, s R f in X , s and therefore X, s R ≤ X , s . Observe that either s = s or s = s • f in. By Lemma 3.9, ψ ∈ cl(s , φ). By induction hypothesis, M, X , s |= ψ and therefore M, X, s |= ψ. Case 1.2: NIL-WORLD(Σ, s, φ) calls successfully NIL-WORLD(Σ , s , φ) in the "fin" segment of NIL-WORLD, last(Σ ) = X , ψ ∈ last(Σ ), X X and X ⊆ cl(s , φ). Moreover, we have either s = s or s = s • f in. This is so since NIL-WORLD(Σ, s, φ) returns true. By definition of R f in , X, s R f in X , s . Furthermore, ψ ∈ cl(s , φ) by Lemma 3.9. By the induction hypothesis, M, X , s |= ψ and therefore M, X, s |= ψ. If ψ ∈ X, then by (iv), for all X , s ∈ R ≤ ( X, s ), ψ ∈ X (and ψ ∈ cl(s , φ) by Lemma 3.9). By the induction hypothesis, M, X , s |= ψ and therefore M, X, s |= ψ. Case 2: ψ = [≥]ψ . This is analogous to the Case 1 and can be proved by using (v) above and Lemma 3.10. Case 3: ψ = [σ]ψ . By definition of W , there is a sequence Σ such that last(Σ) = X and NIL-WORLD(Σ, s, φ) returns true. If ψ ∈ X, then NIL-WORLD(Σ, s, φ) calls NIL-WORLD(X , s • sim, φ) in its "sim" segment, ψ ∈ last(X ), X ≈ X and X ⊆ cl(s , φ). This is so since NIL-WORLD(Σ, s, φ) returns true. By definition of R sim , X, s R sim X , s • sim . By Lemma 3.7, ψ ∈ cl(s • sim, φ). By the induction hypothesis, M, X , s • sim |= ψ and therefore M, X, s |= ψ.

If ψ ∈ X, by (vi), for all X , s ∈ R σ ( X, s ), ψ ∈ X (and ψ ∈ cl(s , φ) by Lemma 3.7 and 3.8). By the induction hypothesis, M, X , s |= ψ and therefore M, X, s |= ψ. As a conclusion, since φ ∈ Y and NIL-WORLD(Y, λ, φ) returns true, M, Y, λ |= φ and therefore φ is NIL-satisfiable.

The proof of Lemma 4.1 can be viewed as a way to transform a successful call of NIL-WORLD(Y, λ, φ) into a quasi NIL-model by analyzing the computation tree of NIL-WORLD(Y, λ, φ). Then, this quasi NIL-model is appropriately completed in order to get a NIL-model. The idea to construct a (standard) model from different coherent pieces is very common to establish decidability and complexity results for modal logics (see e.g. [START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF][START_REF] Pratt | Models of program logics[END_REF][START_REF] Marx | Complexity of modal logics of relations[END_REF]4]).

Lemma 4.2. Let φ be a NIL-formula. If φ is NIL-satisfiable, then there is Y ⊆ cl({φ}) such that φ ∈ Y and NIL-WORLD(Y, λ, φ) returns true.

Proof:

Assume φ is NIL-satisfiable. So, there is a NIL-model M 0 = W 0 , R 0 ≤ , R 0 ≥ , R 0 σ , m 0 and w 0 ∈ W 0 such that M 0 , w 0 |= φ. We shall show that (i) for any s ∈ {sim, f in, bin} * such that neither bin • bin nor f in • f in occurs in s, if Σ is a finite nonempty sequence of subsets of cl(s, φ) that contains no duplicates, last(Σ) = X and there is a NIL-model M = W, R ≤ , R ≥ , R σ , m and w ∈ W satisfying for all ψ ∈ cl(s, φ), M, w |= ψ iff ψ ∈ X, then NIL-WORLD(Σ, s, φ) returns true.

Consequently, by taking s = λ, X = {ψ ∈ cl({φ}) : M 0 , w 0 |= ψ} and Σ = X we get that NIL-WORLD(X, λ, φ) returns true. The proof of (i) is by double induction on the length of s and on the length of Σ.

Base

(Σ) = X. and M be a NIL-model M = W, R ≤ , R ≥ , R σ , m with w ∈ W satisfying for all ψ ∈ cl(s, φ), M, w |= ψ iff ψ ∈ X.
Now we use a second induction on the length of Σ.

Base case 2: |Σ| > 2 card(cl(s,φ)) . Σ contains duplicates and (i) holds. Induction hypothesis 2: for all finite nonempty sequence Σ of subsets of cl(s, φ) that contains no duplicates with last(Σ) = X, |Σ| ≥ n for some n ≥ 1 and there is a NIL-model M = W, R ≤ , R ≥ , R σ , m and w ∈ W satisfying for all ψ ∈ cl(s, φ), M, w |= ψ iff ψ ∈ X, then NIL-WORLD(Σ, s, φ) returns true. Assume Σ is a sequence of subsets of cl(s, φ) that contains no duplicates, last(Σ) = X, |Σ| = n -1 and there is a NIL-model M = W, R ≤ , R ≥ , R σ , m and w ∈ W satisfying for all ψ ∈ cl(s, φ), M, w |= ψ iff ψ ∈ X. Consequently, X is s-consistent by Lemma 3.5. So NIL-WORLD(Σ, s, φ) returns false only because either the segment "sim" or the segment "bin" or the segment "fin" returns false. Case 1:

Consider [≤]ψ ∈ cl(s, φ) \ X such that M, w |= [≤]ψ. There is w ∈ W such that w, w ∈ R ≤ and M, w |= ψ. Let Y be the subset of cl(s • f in, φ) such that for ϕ ∈ cl(s • f in, φ), ϕ ∈ Y def ⇔ M, w |= ϕ. So, ψ ∈ Y and X Y by Lemma 3.12(III).
If Y ∈ Σ and last(s) = f in, then no recursive call to NIL-WORLD needed by definition of NIL-WORLD. In the case when either Y ∈ Σ or last(s) = f in, by induction hypothesis, either NIL-WORLD(Σ • Y, s, φ) returns true (by the induction hypothesis 2) or NIL-WORLD(Y, s • f in, φ) returns true (by the induction hypothesis 1). Therefore, NIL-WORLD(Σ, s, φ) does not return false in the "fin" segment of NIL-WORLD. Similarly, we can show that NIL-WORLD(Σ, s, φ) does not return false in the "bin" segment of NIL-WORLD. Case 2: consider [σ]ψ ∈ cl(s, φ) \ X such that M, w |= [σ]ψ. There is w ∈ W such that w, w ∈ R σ and M, w |= ψ. Let Y be the subset of cl(s • sim, φ) such that for ϕ ∈ cl(s•sim, φ), ϕ ∈ Y def ⇔ M, w |= ϕ. So, ψ ∈ Y and X ≈ Y by Lemma 3.12(II). By the induction hypothesis 1 (remember ψ ∈ cl(s • sim, φ)), NIL-WORLD(Y, s • sim, φ) returns true. Therefore, NIL-WORLD(Σ, s, φ) does not return false in the "sim" segment of NIL-WORLD. The fact that the induction hypothesis 2 is not used in this case should not come as a surprise. Indeed, NIL-WORLD(Σ , s • sim, φ) = NIL-WORLD(last(Σ ), s • sim, for any nonempty finite sequence Σ of elements of P(cl(s • sim, φ)) and s ∈ {sim, f in, bin} * . In other words, for a 'sim' transition, we do not need to keep track of the history of the path. Actually, we only need to check the predecessor which is done with the syntactic relation ≈. Consequently, since neither the segment "sim" nor the segment "bin" nor the segment "fin" returns false, NIL-WORLD(Σ, s, φ) returns true and this completes the proof.

Since NIL-WORLD is correct, the proof of Lemma 4.1 provides the finite model property for NIL and an exponential bound for the size of the models exists. These results could be also obtained via a filtration construction but here we get them as a by-product of the complexity result.

Finally, Theorem 4.2. NIL satisfiability is in PSPACE.

Proof: By Lemma 4.1 and Lemma 4.2, for any formula φ, φ is NIL-satisfiable iff there is X ⊆ cl({φ}) such that NIL-WORLD(X, λ, φ) returns true. By Theorem 4.1, NIL-WORLD(X, λ, φ) requires space in O(|φ| 4 ) and the index necessary to remember which X ⊆ cl({φ}) have been already treated, is in space O(log card(P(cl({φ})))), that is in space O(|φ|).

Concluding remarks

We have shown that the information logic NIL introduced in [START_REF] Or | Representation of nondeterministic information[END_REF] and further studied in [START_REF] Vakarelov | Abstract characterization of some knowledge representation systems and the logic NIL of nondeterministic information[END_REF] has a PSPACE-complete satisfiability problem. This should not come as a real surprise since PSPACE is known to be the complexity class for modal logics. However, it is also known that the satisfiability of polymodal logics can be EXPTIME-hard as soon as the universal modality or the reflexive transitive modality is added to appropriate modal logics [START_REF] Hemaspaandra | The price of universality[END_REF]. For instance, the bimodal logic (say, with modal operators [1] and [2]) characterized by the class of frames W, R 1 , R 2 such that R 1 ⊆ R 2 ⊆ W × W and R 2 is an equivalence relation is EXPTIMEhard [START_REF] Hemaspaandra | The price of universality[END_REF]. Remember that in a NIL model we also have R ≤ ⊆ R σ and R ≥ ⊆ R σ . Furthemore, PSPACE-hardness for satisfiability is not a systematic feature of polymodal information logics (assuming NP = PSPACE). For instance, the bimodal information logic containing a modal operator for indiscernibility and a modal operator for complementarity (see Section 1) has an NP-complete satisfiability problem [START_REF] Demri | Indiscernibility and complementarity relations in Pawlak's information systems[END_REF]. Hence, a further analysis about the PSPACEcompleteness of NIL satisfiability shall certainly help understanding the complexity of other information logics and in a more general setting the computational complexity of numerous polymodal logics with interdependent modal connectives.

Theorem 2 . 2 .

 22 (I) Any fragment of NIL with a single modal connective [R] where R ∈ {≤, ≥ , σ} has a PSPACE-complete satisfiability problem; (II) The fragment of NIL without the modal connective [σ] has a PSPACE-complete satisfiability problem.

  III) Similar to (II). (IV) Let [≤]ψ ∈ cl(s • bin, φ). Two cases are distinguished according to the way the formula [≤]ψ can appear in cl(s • bin, φ). Case 1: [≤]ψ ∈ cl({[≥]ψ }) for some [≥]ψ ∈ cl(s, φ) (see Definition 3.2(5)). We distinguish two cases according to the way [≤]ψ belongs to cl({[≥]ψ }). If [≤]ψ is a subformula of [≥]ψ (see the point 1. in the proof of Lemma 3.1), then md([≤]ψ) < md([≥]ψ ) since [≤]ψ = [≥]ψ and [≥]ψ ∈ cl(s • bin, φ). So md([≤]ψ) < md(cl(s • bin, φ)). If [σ]ψ is a subformula of [≥]ψ and ψ is not a [≤]-formula (see the point 7. in the proof of Lemma 3.1), then

Theorem 3 . 1 .

 31 Let φ be a formula and s ∈ {sim, f in, bin} * be such that neither bin • bin nor f in • f in is a substring of s and |s| ≥ 3 × |φ|. Then cl(s, φ) = ∅.Proof:First observe that for any substring s of length 3 in s, either sim occurs in s or s ∈ {f in • bin • f in, bin • f in • bin}. Since md(φ) + 1 ≤ |φ|, let s be the prefix of s of length 3 × md(φ). By Lemma 3.3, md(cl(s , φ)) = 0 and therefore cl(s , φ) = ∅.What is really important in Theorem 3.1 is that for certain elements s of {sim, f in, bin} * of polynomial length in |φ|, cl(s, φ) is empty. The strings bin • bin and f in • f in do not occur in s, since by (N1) and (N2) we shall identify any element of {bin} + [resp. {f in} + ] with bin [resp. f in]. Theorem 3.1 can be extended in the following way.

  The binary relation ≈ is a reflexive and symmetric relation on clos and is a reflexive and transitive relation on clos. In Definition 3.4 below, for s ∈ {sim, f in, bin} * , we define the set of s-consistent sets which is a subset of clos. function NIL-WORLD(Σ, s, φ)

Figure 1 .

 1 Figure 1. Algorithm NIL-WORLD

  case 1: |s| > 3 × |φ|. Then cl(s, φ) = ∅ and therefore (i) holds. Induction hypothesis 1: for any s ∈ {sim, f in, bin} * such that neither bin • bin nor f in • f in occurs in s , |s | ≥ n for some n ≥ 1, if Σ is a finite nonempty sequence of subsets of cl(s, φ) that contains no duplicates, last(Σ) = X and there is a NIL-model M = W, R ≤ , R ≥ , R

σ , m and w ∈ W satisfying for all ψ ∈ cl(s , φ), M, w |= ψ iff ψ ∈ X, then NIL-WORLD(Σ, s , φ) returns true. Let s ∈ {sim, f in, bin} * such that neither bin • bin nor f in • f in occurs in s, |s| = n -1. Let Σ be a finite nonempty sequence of subsets of cl(s, φ) that contains no duplicates with last

Acknowledgements: The author wish to thank Ewa Or lowska for her numerous suggestions on earlier versions of this work.

Definition 3.4. Let X be a subset of cl(s, φ) for some s ∈ {sim, bin, f in} * and for some formula φ. The set X is said to be s-consistent def ⇔ for ψ ∈ cl(s, φ):

3. if ψ = [R]ϕ for some R ∈ {σ, ≤, ≥} and ψ ∈ X, then ϕ ∈ X;

Roughly speaking, the s-consistency entails the maximal propositional consistency with respect to the set cl(s, φ) of formulae. Furthermore, the modal conditions 3.-6. in Definition 3.4 are added in order to take into account the reflexivity of the relations in the NIL models and the inclusion

The proof of the above lemma is by an easy verification using that cl(s, φ) is closed. Lemma 3.6(II) below roughly states that ⊆≈ which is the syntactic version of R ≤ ⊆ R σ in the NIL models. Similarly, Lemma 3.6(I) below states a syntactic version of

• denote the composition operation for binary relations.

In the forthcoming Lemma 3.7, Lemma 3.8, Lemma 3.9, Lemma 3.10 and Lemma 3.11 we state some basic facts about the sets cl(s, φ). Lemma 3.7. Let s ∈ {sim, bin, f in} * and φ be a formula.

(IV) By Lemma 3.7(IV). Lemma 3.9. Let s ∈ {sim, bin, f in} * and φ be a formula.

Lemma 3.10. Let s ∈ {sim, bin, f in} * and φ be a formula.

(III) This is obvious since cl(s, φ) is closed. Lemma 3.11. Let s ∈ {sim, bin, f in} * and φ be a formula.

(II) See the proof of Lemma 3.8(III). (III) Obvious.

Before defining the main algorithm of the paper, let us conclude by presenting some relationships between the relations and ≈ and the relations from the NIL-models. Lemma 3.12. Let M = W, R σ , R ≤ , R ≥ , m be a NIL-model and w, w ∈ W . Let s ∈ {sim, bin, f in} * , s , s ∈ {λ, sim, f in, bin} and φ be a formula. Let

(II) if s , s ∈ { λ, sim , sim, λ , λ, λ } and w, w ∈ R σ , then X w ≈ X w ;

(III) if s , s ∈ { λ, f in , bin, λ , λ, λ } and w, w ∈ R ≤ , then X w X w .

The proof is by an easy verification using the previous lemmas.

NIL is in PSPACE 4.1. The algorithm

In Figure 1, the function NIL-WORLD(Σ, s, φ) returning a Boolean is defined. Σ is a nonempty finite sequence of subsets of cl({φ}) and s ∈ {sim, f in, bin} * . For any X ⊆ cl({φ}) and for any call NIL-WORLD(Σ, s, φ) in NIL-WORLD(X, λ, φ) (at any recursion depth), we have last(Σ) ⊆ cl(s, φ). In the next section we shall show that

is omitted because it is very similar. Moreover, if s = s • sim, then |Σ| = 1 and hence this case is not relevant, since we assume n ≥ 2. For i ∈ {1, . . . , n -1}, [≤]ψ ∈ X i implies [≤]ψ ∈ X i+1 . Thus, Σ can be written as Σ = Σ 1 • . . . • Σ n where for i, i ∈ {1, . . . , n } • the elements of Σ i contain the same [≤]-formulae;

Since there are less than 5 × |φ| [≤]-formulae in cl({φ}), n ≤ 5 × |φ|. Let i ∈ {1, . . . , n }. Σ i can be written as

where for j, j ∈ {1, . . . , l(i)}, the elements of Σ j i contains the same [≥]-formulae and [σ]-formulae and j < j implies the set of [≥]-formulae and [σ]-formulae of Σ j i is a proper subset of the set of [≥]-formulae and [σ]-formulae of Σ j i .

For i ∈ {1, . . . , n}, let

One can see that l(1) • Any call NIL-WORLD(Σ, s, φ) from NIL-WORLD(X, λ, φ) satisfies that neither bin • bin nor f in • f in is a substring of s;

• Any call NIL-WORLD(Σ, s, φ) with |s| ≥ 3 × |φ| does not call recursively NIL-WORLD. This means that no more recursive calls to NIL-WORLD is executed (see Theorem 3.1).

Consequently, the depth of the recursion is in O(|φ| 3 ). More precisely, the depth is bounded by 75 × |φ| 3 . Since we need space in O(|φ|) at each level of the recursion, the total space to compute NIL-WORLD(X, λ, φ) for X ⊆ cl({φ}) is in O(|φ| 4 ). As a consequence we have, Theorem 4.1. Let X ⊆ cl({φ}).

(I) NIL-WORLD(X, λ, φ) terminates and requires space in O(|φ| 4 );

(II) Let NIL-WORLD(Σ, s, φ) be a call in the computation of NIL-WORLD(X, λ, φ). Then, |Σ| ≤ (III) Let a call NIL-WORLD(Σ , s , φ) be made in NIL-WORLD(Σ, s, φ) in the computation of NIL-WORLD(X, λ, φ). Then,

where < is the standard (well-founded) lexicographical ordering on ω 2 .

Correction

Theorem 4.1 is an important step to prove that NIL satisfiability is in PSPACE but it is not sufficient. Indeed, up to now we have no guarantee that the function NIL-WORLD is correct. This is shown in the next two lemmas. Let S be the set of strings s over {sim, bin, f in} such that |s| ≤ 3 × |φ|. We define W as the set of pairs X, s for which there is a finite sequence Σ 1 , s 1 , . . . , Σ k , s k (k ≥ 1) such that


Stéphane Demri
email: demri@imag.fr

A Simple Modal Encoding of Propositional Finite Many-Valued Logics

Keywords: finite many-valued logic, modal logic of elsewhere, manyone reduction

We present a method for testing the validity for any finite manyvalued logic by using simple transformations into the validity problem for von Wright's logic of elsewhere. The method provides a new original viewpoint on finite many-valuedness. Indeed, we present a uniform modal encoding of any finite many-valued logic that views truth-values as nominals. Improvements of the transformations are discussed and the translation technique is extended to any finite annotated logic. Using similar ideas, we conclude the paper by defining transformations from the validity problem for any finite many-valued logic into TAUT (the validity problem for the classical propositional calculus). As already known, this sharply illustrates that reasoning within a finite many-valued logic can be naturally and easily encoded into a twovalued logic. All the many-one reductions in the paper are tight since they require only time in O(n.log n) and space in O(log n).

Introduction

Background. Many-valued logics devised as formal systems have been extensively studied since [START_REF] Lukasiewicz | O logice trówartościowej[END_REF][START_REF] Post | Introduction to a general theory of elementary propositions[END_REF]. Several applications exist in various areas such as in Mathematical Logic (see e.g. [START_REF] Lukasiewicz | Elements of mathematical logic[END_REF]), in Quantum Physics (see e.g. [START_REF] Reichenbach | Philosophical Foundations of Quantum Mechanics[END_REF]), in Theoretical Computer Science (see e.g. [START_REF] Rasiowa | Many-valued algorithmic logic as a tool to investigate programs[END_REF][START_REF] Fitting | Kleene's logic, generalized[END_REF]) and in Artificial Intelligence (see e.g. [START_REF] Ginsberg | Multivalued logics : A uniform approach to reasoning in artificial intelligence[END_REF]). The proof theory of finite (propositional and first-order) many-valued logics is quite well understood (see e.g. [Tak68, Mor76, Sur77, Car87, Wój88, Zac93, Häh93, Zab93, BF95, Sal96]) and various publicly available running systems exist (see e.g. [START_REF] Beckert | The tableau-based theorem prover 3TAB[END_REF][START_REF]Vienna Group for Multi-Valued Logics. MUltlog 1.0: towards an expert system for many-valued logics[END_REF]).

Our contribution. In this work, we concentrate on the relationships between finite propositional many-valued logics and modal logic, proposing an original approach about the essence of finite many-valuedness. The need for such a comparison is mainly motivated by Urquhart's statement in the survey paper [Urq86, Section 3.1]: "..., the semantical methods involving relational model structures, 'possible worlds' and the like, which [...] have proved so fruitful in areas like modal logic, seem to have no clear connection with traditional many-valued logic."

Our goal here is to clarify such a connection. A relational semantics for finite many-valued logics can be found in [START_REF] Konikowska | A relational formalisation of arbitrary finite valued logic[END_REF] (see also [START_REF] Ch | Kripke and relational-style semantics and associated tableau proof systems for arbitrary finite valued logics[END_REF]). In the present paper, we show that there exists a Sahlqvist modal logic [START_REF] Sahlqvist | Completeness and correspondence in the first and second order semantics for modal logics[END_REF], say L = , such that any finite many-valued logic has a natural embedding into L = . Extensions are also given for finite annotated logics. The result is of interest especially because it can be then argued that any finite many-valued logic (and any finite annotated logic) can be viewed as a modal system. Furthermore, we also define transformations ("many-one reductions", see e.g. [START_REF] Ch | Computational Complexity[END_REF]) from the validity problem for any finite many-valued logic into TAUT (the validity problem for the propositional calculus PC) using similar ideas. This clearly illustrates that reasoning within a finite many-valued logic can be easily and naturally encoded into a two-valued logic. Although this fact has been known at least since [START_REF] Rosser | Many-Valued Logics[END_REF] (see also [START_REF] Zinov'ev | Two-valued and many-valued logic[END_REF]), we also provide evidence here that such an encoding can be effectively done into a modal logic that is enough expressive to allow nominals (atomic propositions that hold true in a unique world of the Kripke-style models) and the truthvalues are viewed as nominals.

When L is a co-NP-hard language, for any finite many-valued logic L, there exists a polynomial-time transformation f from the set of L-valid formulae into L such that for any L-formula φ, φ is L-valid iff f (φ) ∈ L. This is just by definition of co-NP-hardness with respect to polynomialtime many-one reductions (see e.g. [START_REF] Ch | Computational Complexity[END_REF]) since L-validity is in co-NP. However, 1. there is no guarantee that the transformation f is natural (it might be necessary to apply first principles about Turing machines and therefore it is difficult to implement); 2. f is in the complexity class P, that is there is a polynomial p(n) such that computing f (φ) requires time in O(p(|φ|)) where |φ| is the length of φ for some reasonably -unspecified-succinct encoding. However, we ignore the value of p(n) and whether the main exponent of p(n) increases with the number of truth values and/or with the number of connectives;

3. a uniform definition of the transformations for all the finite manyvalued logics is not immediate.

By constrast, herein, the transformations into L = are natural, they require only time in O(n.log n) and L = is precisely co-NP-complete. So even with respect to the worst-case computational complexity, the transformations can be hardly optimized. An interesting potential application of our results is that mechanization of the finite many-valued logics can be done with a unique theorem prover dedicated to the logic L = (or dedicated to PC) and it is guaranteed that the transformations do not introduce any significant complexity blow-up. Experimental analyses are needed, even though the transformations given in the paper are theoretically appealing.

The logic of elsewhere The point here is that the logic L = is not some ad hoc modal logic made up for the purpose of the paper but it is the well-known von Wright's logic of elsewhere [START_REF] Wright | A modal logic of place[END_REF] defined as the smallest normal modal logic (extension of the minimal normal modal logic K -see e.g. [START_REF] Chellas | Modal Logic[END_REF]) containing all instances of the axiom schemes: φ ⇒ 23φ and 33φ ⇒ (φ ∨ 3φ). Hence, L = is an extension of the modal logic K by addition of Sahlqvist axiom schemes. In order to make this paper selfcontained, let us recall some known facts about L = . In [START_REF] Segerberg | A note on the logic of elsewhere[END_REF], it is shown that L = is characterized by the class C = of modal frames W, R such that the binary relation R is the complement of the diagonal relation of W (this was conjectured in [START_REF] Wright | A modal logic of place[END_REF]). This means that for any modal formula φ, φ ∈ L = iff φ is valid in all the frames belonging to C = . In the present paper, we assume that the modal formulae are built from a countably infinite set {q 0 , . . . , q n , . . .} of atomic propositions 1 and closed under 2, ¬, ⇒, ∧ (the standard abbreviations include ∨, ⇔, 3). "2φ" can be read as "everywhere else φ holds". It is known that C = is not modally definable since it is not closed under disjoint union [START_REF] Goldblatt | Axiomatic classes in propositional modal logic[END_REF]. C = -satisfiability (or equivalently L =consistency) is known to be NP-complete [START_REF] Smit | The complexity of the modal difference operator in propositional logic[END_REF] and a formula φ is C =satisfiable iff it has a C = -model of cardinality at most 2.mw(φ) + 1 [START_REF] Demri | A simple tableau system for the logic of elsewhere[END_REF] where mw(φ) is the number of occurrences of the modal operator 2 in φ. Hence, L = is co-NP-complete. L = has been recently equipped with analytic calculi since prefixed tableaux-style proof systems for L = have been defined in [START_REF] Demri | A simple tableau system for the logic of elsewhere[END_REF][START_REF] Ph | Prefixed tableaux systems for modal logics with enriched languages[END_REF] as well as decision procedures building models with the best known model's size [START_REF] Demri | A simple tableau system for the logic of elsewhere[END_REF][START_REF] Ph | Prefixed tableaux systems for modal logics with enriched languages[END_REF]. All those previous facts are evidence that L = is a quite well-understood modal logic.

Related work. The idea of interpreting finite many-valued logics into modal logics is not a new one and even the three-valued logic L of Lukasiewicz had a modal flavour from the beginning [START_REF] Lukasiewicz | O logice trówartościowej[END_REF] (see also [START_REF] Turquette | Modality, minimality and many-valuedness[END_REF] [Urq86, Section 1.2]). In [START_REF] Segerberg | Some modal logics based on a three-valued logic[END_REF], a (poly)modal logic is defined based on a threevalued logic (see also in [START_REF] Thomason | Possible worlds and many truth values[END_REF][START_REF] Morikawa | Some modal logics based on a three-valued logics[END_REF][START_REF] Fitting | Many-valued modal logics, I and II[END_REF] the definition of many-valued modal logics). It is argued in [START_REF] Segerberg | Some modal logics based on a three-valued logic[END_REF] that a generalization to any finite manyvalued logic is possible. Hence, a family of (poly)modal logics can be defined on the basis of a family of finite many-valued logics. However, the main concern in [START_REF] Segerberg | Some modal logics based on a three-valued logic[END_REF] is not to embed many-valued logics into modal logics and a fortiori not into a unique modal logic. In [START_REF] Duffy | Modal interpretations of three valued logics, I and II[END_REF] (see also [START_REF] Woodruff | A modal interpretation of three valued logic[END_REF]), the three-valued logic L of Lukasiewicz is translated into the standard modal logic S5 (eight modal interpretations are explored). The second part of [START_REF] Duffy | Modal interpretations of three valued logics, I and II[END_REF] contains 3042 mappings from S lupecki's functionnally complete version of L into a modified version of S5. Every model of the modified S5 has at least two worlds and the language is augmented with a unique nominal. This is the first work we are aware of that relates a many-valued logic with a nominal modal logic. As known, L = is also a nominal modal logic in disguise and this fact shall be quite useful in what follows. In [Zab93, Chapter 9], Lukasiewicz's logics L n are also translated into modal logics with a minimal models semantics (see e.g. [START_REF] Chellas | Modal Logic[END_REF]). Another way to relate modal logics with finite many-valued logics consists in translating modal logics into finite many-valued logics. For instance, in [CZ90], using similar ideas from [Kri63, Section 5.2], the modal logic S5 is translated into finite many-valued logics. Each S5-formula of size n is translated into a finite many-valued logic having 2 n+1 truth values, which does not necessarily guarantee the best computational behaviour (see [Häh93, Section 7.2.4] for improvements of the method).

2 Propositional finite many-valued logics

In this section, we just recall a few basic notions about finite many-valued logics. A signature Σ is a (non-empty) finite set {c 1 , . . . , c K } of propositional connectives augmented with an arity function ar : {c 1 , . . . , c K } → ω. Given a countably infinite set For 0 = {p 0 , . . . , p n , . . .} of atomic propositions, the Σ-formulae φ ∈ For are inductively defined as follows:

φ ::= p i | c 1 (φ 1 , . . . , φ ar(c 1 ) ) | . . . | c K (φ 1 , . . . , φ ar(c K ) )
where

p i is an atomic proposition. A Σ-logic L is a structure Σ, {1, . . . , N }, N , f c 1 , . . . , f c K such that 1. N ≥ 2; 2. 1 < N ≤ N ({1, . . . , N -1} is the non-empty set of designated values); 3. for i ∈ {1, . . . , K} such that ar(c i ) = 0, f c i is a map f i : {1, . . . , N } ar(c i ) → {1, . . . , N };
4. for i ∈ {1, . . . , K} such that ar(c i ) = 0, f c i is a truth-value, that is a member of {1, . . . , N }. •

I, v |= p i def ⇔ I(p i ) = v; • for i ∈ {1, . . . , K} such that ar(c i ) = 0, I, v |= c i (φ 1 , . . . , φ ar(c i ) ) def ⇔ there exist v 1 , . . . , v ar(c i ) such that for 1 ≤ j ≤ ar(c i ), I, v j |= φ j and f c i (v 1 , . . . , v ar(c i ) ) = v; • for i ∈ {1, . . . , K} such that ar(c i ) = 0, I, v |= c i def ⇔ f c i = v.
We take here some freedom with the usual presentation of the semantics in order to facilitate the presentation of the forthcoming transformations. Indeed, there is a unique truth-value v such that I, v |= φ given an Linterpretation I and a Σ-formula φ. A Σ-formula φ is L-valid def ⇔ for any L-interpretation I, there is a designated truth-value v ∈ {1, . . . , N -1} such that I, v |= φ. A Σ-formula φ is L-satisfiable def ⇔ there exist an Linterpretation I and v ∈ {1, . . . , N -1} such that I, v |= φ. It is easy to see that L-satisfiability is in the complexity class NP (L-satisfiability can be solved by a non-deterministic Turing machine in polynomial-time) whereas L-validity is in co-NP (the set of non L-valid formulae is in NP).

Example 2.1. Let L = Σ, {1, . . . , 3}, 2, {f T , f N , f ⊃ } be S lupecki's functionnally complete version of Lukasiewicz three-valued logic L.

• Σ = {T, N, ⊃}, ar(T) = 0, ar(N) = 1, ar(⊃) = 2;

• 1, 2 and 3 respectively corresponds to the more usual truth-values 1, 1/2 and 0; the unique designated truth-value is 1;

• f T = 2 and f N (v) = 4 -v for v ∈ {1, 2, 3}; • f ⊃ (v, v ) = 1 if v ≤ v; f ⊃ (v, v ) = 2 if v, v = 1, 2 or v, v = 2, 3 ; f ⊃ (v, v ) = 3 if v, v = 1, 3 .

Embeddings

In this section, we assume that L is a finite many-valued logic and we use the notations from Section 2.

Finite many-valued logics into L =

The main idea of the embedding from any finite many-valued logic L into L = is quite simple. Roughly speaking, any L-interpretation can be seen as a partition of cardinality N of the set of Σ-formulae. Indeed, an Linterpretation I : For 0 → {1, . . . , N } can be viewed as a C = -model

M I = {1, . . . , N }, {1, . . . , N } 2 \ { v, v : v ∈ {1, . . . , N }}, m
such that for any atomic proposition p,

I(p) = v iff v ∈ m(p )
where p is an atomic proposition associated to p. In the paper, if p = p i , then p def = q 2.i . Since finite cardinality can be defined in L = [Koy92, Chapter 4], we can enforce that M I is of cardinality N . Indeed, there exists a modal formula φ n (n ≥ 1) such that for any frame W, R ∈ C = , φ n is valid in W, R iff card(W ) = n. Moreover, to each world, say v, of M I we can attach a name, that is an atomic proposition, say q 2.v+1 , that holds true only in the world v. In this way, each world of M I can be viewed as a truthvalue and its name allows to know which one. Observe that p associated to p (see above) also behaves as a name. Until now, we have only treated atomic propositions from L. To each subformula ψ of φ (the formula to be translated), we associate an atomic proposition, say q 2.[ψ]+1 , in L = where [ψ] is a natural number associated to ψ and q 2.[ψ]+1 in L = behaves as ψ in L. We have also to take care that the assignment of the atomic propositions does not interfer with the names or between each other. A similar renaming technique is also used in [START_REF] Hähnle | Short conjunctive normal forms in finitely valued logics[END_REF] to define normal forms for many-valued logics. Our purpose here is different although the renaming technique is a standard tool also used for classical, modal and intuitionistic logics, to quote a few logics.

Let us give now the formal definitions. Let φ be a Σ-formula from the Σlogic L. Let φ 1 , . . . , φ m be an arbitrary enumeration (without repetition) of the subformulae of φ such that the n first formulae are all the atomic propositions occurring in φ. For i ∈ {1, . . . , m}, we write [φ i ] to denote i. Moreover, for i ∈ {n + 1, . . . , m}, we write c(i) to denote the outermost connective of φ i . We shall build a formula g(φ) upon {q 2 , . . . , q 2.N } ∪ {q 3 , . . . , q 2.m+1 } such that

φ is L-valid iff g(φ) ∈ L = .
The atomic propositions from {q 2 , . . . , q 2.N } shall behave as nominals that encodes truth-values whereas the atomic propositions from {q 3 , . . . , q 2.m+1 } shall respectively behave as the subformulae φ 1 , . . . , φ m .

We use the following abbreviations:

U ψ def = 3ψ ∨ ψ [U ]ψ def = 2ψ ∧ ψ [!]ψ def = U (ψ ∧ 2¬ψ) "[U ]
ψ" can be read as "everywhere ψ holds" whereas "[!]ψ" can be read as "there is exactly one world where ψ holds". [U ] is the standard universal modal operator (see e.g. [START_REF] Goranko | Using the universal modality: gains and questions[END_REF]). Let φ = 1 be the formula stating that the C = -model has exactly N worlds and each world is labelled by a different atomic proposition q 2.k for k ∈ {1, . . . , N }:

φ = 1 def = ( N k=1 [!]q 2.k ) ∧ ([U ] N k=1 q 2.k ) ∧ ([U ] 1≤k<k ≤N ¬(q 2.k ∧ q 2.k ))
The size of φ = 1 is constant in |φ| since it does not depend on φ.

Lemma 3.1. Let M = W, R, m be a Kripke-style model based on a frame in C = , that is R = { w, w ∈ W2 : w = w }. Then, there is w ∈ W such that 2 M, w |= φ = 1 iff the conditions below holds:

1. card(W ) = N ;

2. for w ∈ W there is a unique v ∈ {1, . . . , N } such that M, w |= q 2.v .

Let φ = 2 be the formula stating that each atomic proposition in φ is assigned a unique truth value in the interpretation:

φ = 2 def = n k=1 [!]q 2.k+1
The size of φ = 2 is in O(|φ|.log |φ|). As usual in complexity theory, the extra log |φ| factor in the size of φ is due to the fact that we need an index of size O(log |φ|) for these different atomic propositions. The natural numbers are indeed represented in binary writing.

Lemma 3.2. Let M = W, R, m be a Kripke-style model based on a frame in C = . Then, there is w ∈ W such that M, w |= φ = 2 iff for k ∈ {1, . . . , n} there is a unique w ∈ W such that M, w |= q 2.k+1 .

Let φ i = c(i)(ϕ 1 , . . . , ϕ ar(c(i)) ) be a non atomic subformula of φ such that ar(c(i)) = 0. For any v ∈ {1, . . . , N }, we write f -1 c(i) (v) to denote the set

f -1 c(i) (v) def = { v 1 , . . . , v ar(c(i)) ∈ {1, . . . , N } ar(c(i)) : f c(i) (v 1 , . . . , v ar(c(i)) ) = v}
Let φ i,v 3 be the formula stating that q 2.i+1 behaves in L = as φ i in L with respect to the truth value v:

φ i,v 3 def = [U ](q 2.v ⇒ q 2.i+1 ) ⇔ v 1 ,...,v ar(c(i)) ∈f -1 c(i) (v) ar(c(i)) j=1 [U ](q 2.v j ⇒ q 2.[ϕ j ]+1 ) When f -1 c(i) (v) = ∅
, the generalized disjunction should be read as the logical constant ⊥ (falsum). The size of φ i,v 3 is also in O(log |φ|). Remember that N , K, M = max{ar(i) : 1 ≤ i ≤ K} are constants of the logic L. Let φ i = c(i) be such that ar(c(i)) = 0. The formula φ i 3 is defined as follows:

φ i 3 def = [U](q 2.i+1 ⇔ q 2.f c(i) )
Let g(φ) be the formula:

g(φ) def = (φ = 1 ∧φ = 2 ∧( ar(c(i)) =0 i∈{n+1,...,m} v∈X c(i) L φ i,v 3 )∧( ar(c(i))=0 i∈{n+1,...,m} φ i 3 )) ⇒ [U ](q 2.[φ]+1 ⇒ N -1 v=1 q 2.v )
where

X c(i) L def = {v ∈ {1, . . . , N } : f -1 c(i) (v) = ∅} So |g(φ)| is in O(|φ|.
= such that M, w |= φ = 1 ∧ φ = 2 ∧ ( ar(c(i)) =0 i∈{n+1,...,m} v∈X c(i) L φ i,v 3 ) ∧ ar(c(i))=0
i∈{n+1,...,m} φ i 3 . Then, for k ∈ {1, . . . , m} there is a unique w ∈ W such that M, w |= q 2.k+1 .

The proof of Lemma 3.3 is based on the fact that for any i ∈ {1, . . . , K} such that ar(c i ) = 0,

{f -1 c i (v) : v ∈ {1, . . . , N }, f -1 c i (v) = ∅} is a partition of {1, . . . , N } ar(c i ) . Proposition 3.4. φ is L-valid iff g(φ) ∈ L = .
Proof: Let φ be a Σ-formula. For any L-interpretation I, we write M I def = W, R, m (depending also on φ) to denote the C = -model such that

1. W def = {1, . . . , N }; R def = W 2 \ { v, v : v ∈ W }; 2. for v ∈ {1, . . . , N }, m(q 2.v ) def = {v}; 3. for i ∈ {1, . . . , m}, m(q 2.i+1 ) def = {v ∈ W : I, v |= ψ i };
4. the interpretation of the other atomic propositions is not constrained.

One can check that for any

v ∈ W , M I , v |= φ = 1 ∧φ = 2 ∧( ar(c(i)) =0 i∈{n+1,...,m} v∈X c(i) L φ i,v 3 )∧ ar(c(i))=0
i∈{n+1,...,m} φ i 3 . For i ∈ {1, . . . , m}, m(q 2.i+1 ) is also a singleton by Lemma 3.3. Then, one can prove that for any i ∈ {1, . . . , m} and for any v ∈ {1, . . . , N }, I, v |= φ i iff M I , v |= q 2.i+1 (by an induction on the structure of the formulae). Consequently, if g(φ

) ∈ L = , then φ is L-valid. Now, let M def = W, R, m be a C = -model such that for some w ∈ W , M, w |= φ = 1 ∧ φ = 2 ∧ ar(c(i)) =0 i∈{n+1,...,m} v∈X c(i) L φ i,v 3 ∧ ar(c(i))=0
i∈{n+1,...,m} φ i 3 . Let I M be the L-interpretation such that for any i ∈ {1, . . . , n}, I M (φ i ) def = v where v is the unique index in {1, . . . , N } such that there is world w ∈ W verifying M, w |= q 2.v ∧ q 2.i+1 . One can show that for any i ∈ {1, . . . , m} and for any v ∈ {1, . . . , N }, I M , v |= φ i iff M, v |= q 2.i+1 (by an induction on the structure of the formulae). Consequently, if φ is L-valid, then g(φ) ∈ L = . Q.E.D.

Let g (φ) be the formula:

g (φ) def = (φ = 1 ∧φ = 2 ∧( ar(c(i)) =0 i∈{n+1,...,m} v∈X c(i) L φ i,v 3 )∧( ar(c(i))=0 i∈{n+1,...,m} φ i 3 ))∧ U (q 2.[φ]+1 ∧ N -1 v=1 q 2.v ) It is now easy to show that φ is L-satisfiable iff g (φ) is C = -satisfiable (or equivalently, iff g (φ) is L = -consistent). g(φ)
and g (φ) share the same complexity measures described previously. The definition of φ i,v 3 can be improved in order to significantly reduce the size of g(φ). Let i ∈ {1, . . . , K} be such that ar(c i ) = 0 and v ∈ {1, . . . , N }. The set X c i v is defined as a set of strings over {1, . . . , ar

(c i )} × {1, . . . , N } of length at most ar(c i ). l 1 , v 1 . . . . l s , v s ∈ X c i v is understood as a compact representation for "f i (w 1 , . . . , w ar(c i ) ) = v when w l 1 = v 1 , . . . , w ls = v s ".
with the new definition. Although the above improvement is unessential for the soundness of the embeddings, it can considerably reduce the size of the translated formula and therefore it is well-suited for mechanization. By the way, this optimization is comparable, for instance to refinements in the calculi from [START_REF] Carnielli | Systemization of finite many valued logics through the method of tableaux[END_REF][START_REF] Zabel | Nouvelles techniques de déduction automatique en logiques polyvalentes finies et infinies du premier ordre[END_REF][START_REF] Hähnle | Automated Deduction in Multiple-Valued Logics[END_REF][START_REF] Zach | Proof theory of finite-valued logics[END_REF]. This provides another reading for some of those calculi: these are calculi for fragments of von Wright's logic of elsewhere obtained by optimally translating finite many-valued logics. Indeed, every subformula of the form [U ](q 2.v ⇒ q 2.i+1 ) occurring in g(φ) corresponds to the signed formula v : φ i . More importantly, techniques for analysis of a finite many-valued logic at the metalevel can be embedded into the object level (in L = for instance). Finally, the proof of Proposition 3.4 shows that there exists a natural correspondence between C = -models and L-interpretations. This allows the construction of L-interpretations by using proof systems for L = that admit model-building mechanisms, as done in [START_REF] Ph | Prefixed tableaux systems for modal logics with enriched languages[END_REF] for instance.

Example 3.1. (Example 2.1 continued) Let φ be the formula Np 200 ⊃ T. The sets X N j and X ⊃ j for j ∈ {1, 2, 3} takes the following values:

• X N 1 = { 1, 3 } (the unary connective N returns the truth-value 1 with input the truth-value 3); X N 2 = { 1, 2 }; X N 3 = { 1, 1 }; • X ⊃ 1 = { 2, 1 , 1, 2 . 2, 2 , 1, 3 . 2, 2 , 1, 3 . 2, 3 } (for instance the "first" element in X ⊃ 1 means that if the second argument of v ⊃ v is 1 then v ⊃ v is evaluated to 1) ; • X ⊃ 2 = { 1, 1 . 2, 2 , 1, 2 . 2, 3 }; X ⊃ 3 = { 1, 1 . 2, 3 }.
The sequence φ 1 , . . . , φ 4 of subformulae of φ can be for instance p 200 , T, Np 200 , φ.

Let us present the different formulae that constitute the formula g(φ).

φ = 1 def = ( 3 k=1 [!]q 2.k ) ∧ ([U ] 3 k=1 q 2.k ) ∧ ([U ] 1≤k<k ≤3 ¬(q 2.k ∧ q 2.k )) φ = 2 def = [!]q 3 φ 2 3 def = [U ](q 4 ⇔ q 5 ) φ 3,1 3 def = [U ](q 2 ⇒ q 7 ) ⇔ [U ](q 6 ⇒ q 3 ) φ 3,2 3 def = [U ](q 4 ⇒ q 7 ) ⇔ [U ](q 4 ⇒ q 3 ) φ 3,3 3 def = [U ](q 6 ⇒ q 7 ) ⇔ [U ](q 2 ⇒ q 3 ) φ 4,2 3 def = [U ](q 4 ⇒ q 9 ) ⇔ ([U ](q 2 ⇒ q 7 ) ∧ [U ](q 4 ⇒ q 5 )) ∨ ([U ](q 4 ⇒ q 7 ) ∧ [U ](q 6 ⇒ q 5 ))
The values for φ 4,1 3 and φ 4,3 3 can be also easily computed.

Finite annotated logics into L =

The treatment of "truth values as nominals" can be easily carried out to particular paraconsistent logics, namely to the finite annotated logics (see e.g. [Sub87, dCHLS90, LSC91, KL92]) as shown below. First, let us briefly recall some basic definitions. Let {1, . . . , N }, ∩, ∪ be a finite lattice and ∼ be an 1-1 mapping ∼: {1, . . . , N } → {1, . . . , N }. Here, we do not need to require any particular property for ∼.

Example 3.2. The standard complete lattice FOUR (see e.g. [START_REF] Da Costa | Automatic theorem proving in paraconsistent logics: theory and implementation[END_REF]) is composed of the truth values {⊥, , t, f} with the greatest element, ⊥ the lowest element and t and f are not comparable.

Given a countably infinite set For 0 = {p 0 , . . . , p n , . . .} of atomic propositions, the formulae φ are inductively defined as follows:

φ ::= p i , v | ¬ p i , v | ¬φ | φ 1 ∧ φ 2
for p i an atomic proposition and v ∈ {1, . . . , N }. An interpretation I is a map I : For 0 → {1, . . . , N }. The satisfiability relation |= is inductively defined as follows: An annotated logic L can be defined as the structure {1, . . . , N }, ∩, ∪ , ∼ , For 0 . A formula φ is L-valid def ⇔ for all interpretations I (based on {1, . . . , N }, ∩, ∪ and ∼), I |= φ. Without any loss of generality 4 , let φ be a ¬ -free annotated formula. Let φ 1 , . . . , φ m be an arbitrary enumeration (without repetition) of the subformulae of φ such that the n first formulae are all the annotated atomic propositions occurring in φ. For i ∈ {1, . . . , m}, we write [φ i ] to denote i. This time, we build a formula g(φ) upon {q 0 } ∪ {q 2 , . . . , q 2.N , q 3 , . . . , q 2.m+1 }. The atomic proposition q 0 shall also behave as a name and it refers to the world where the (binary) satisfiability relation is encoded.

• I |= p i , v def ⇔ I(p i ) ≥ v (≥ is
Let φ = 1 be the formula stating that the model has exactly N + 1 worlds and names are attached to the worlds:

φ = 1 def = ( N k=0 [!]q 2.k ∧ [U ] N k=0 q 2.k ∧ [U ] 0≤k<k ≤N ¬(q 2.k ∧ q 2.k ))
Let φ = 2 be the formula stating that the atomic propositions are interpreted by a value in {0, . . . , N } \ {0}:

φ = 2 def = n k=1 [!]q 2.k+1 ∧ [U ]( n k=1 (q 2.k+1 ⇒ ¬q 0 ))
For each subformula φ i of φ we associate a formula φ i 3 as shown in Figure 1 and let

g(φ) def = (φ = 1 ∧ φ = 2 ∧ m i=1 φ i 3 ) ⇒ [U ](q 0 ⇒ q 2.[φ]+1 ) Form of φ i φ i 3 p, v [U ](q 0 ⇒ (q 2.i+1 ⇔ U (q 2.i+1 ∧ v ≥ v q 2.v )) ψ ∧ ψ [U ](q 0 ⇒ (q 2.i+1 ⇔ (q 2.[ψ ]+1 ∧ q 2.[ψ ]+1 )) ¬ψ [U ](q 0 ⇒ (q 2.i+1 ⇔ ¬q 2.[ψ ]+1 ))
Figure 1: Definition of φ i 3 Proposition 3.6. φ is L-valid iff g(φ) ∈ L = .

Proof: Similar to the proof of Proposition 3.4. Q.E.D.

Finite many-valued logics into PC

In Section 3.1 and in Section 3.2, we have seen that the concept of "truthvalues as nominals" is essential to define natural translations into L = . However, by close examination of the proof in Section 3.1, it is possible to observe that the names are very useful but they are absolutely not necessary. In what follows, we show how to define natural transformations (in time O(n.log n)) from the validity problem for any finite many-valued logic into TAUT. We assume that the formula of PC are built over the set {q i,j : i, j ∈ ω} of atomic propositions. We could also just consider the set {q i : i ∈ ω} of atomic propositions and use a 1-1 mapping from ω 2 → ω but for the sake of simplicity, the present option is the most convenient.

Let φ be a Σ-formula from the Σ-logic L (we use again the notations of Section 3.1). We shall build a formula g (φ) over {q

i,v : 1 ≤ i ≤ m, 1 ≤ v ≤ N } such that φ is L-valid iff g (φ)
is a tautology. The simple idea of the translation is the following. Since the C = -models involved in the proof of Proposition 3.4 are finite and only a finite amount of atomic propositions are considered for a given formula φ, we introduce atomic propositions such that M I , v |= q 2.i+1 iff q i,v holds true in some interpretation for PC.

Let φ P C 1 be the formula stating that each atomic proposition in φ is assigned a unique truth value in the interpretation:

φ P C 1 def = n i=1 (( N v=1 p i,v ) ∧ 1≤v<v ≤N ¬(p i,v ∧ p i,v ))
The size of φ P C 1 is in O(|φ|.log |φ|). Let φ i = c(i)(ϕ 1 , . . . , ϕ ar(c(i)) ) be a non atomic subformula of φ such that ar(c(i)) = 0. Let φ i,v 2,P C be the formula stating that q i,v behaves in PC as φ i in L with respect to the truth value v: φ i,v 2,P C def = q i,v ⇔ l 1 ,v 1 ..... ls,vs ∈X c(i) v ( s j=1 q [ϕ l j ],v j )

In the case when X c(i) v = {Λ}, φ i,v 2,P C def = q i,v . Now let φ i = c(i) be a subformula of φ such that ar(c(i)) = 0. φ i 2,P C is defined as the atomic formula q i,f c(i) . Let g (φ) be the formula: Proposition 3.7. φ is L-valid iff g (φ) ∈ TAUT.

Proof: Similar to the proof of Proposition 3.4. Q.E.D.

g is a very natural map. It requires only time in O(n.log n) and it is not difficult to see that similar many-one reductions from any finite annotated logic in PC can be defined.

Concluding remarks

In this paper, the modal encoding of propositional finite many-valued logics are based on the notion of transformations ("many-one reductions") used in complexity theory. All the transformations in this paper are tight since they require only time in O(n.log n) and space in O(log n). Futhermore, the target problems (either L = or TAUT) are in co-NP which is an evidence of the efficiency of the transformations since validity for the propositional finite many-valued logics and validity for the propositional annotated logics are also in co-NP. Apart from the modal viewpoint on finite many-valued logics we provided here, it is an open question whether any efficient theorem prover dedicated to either L = or PC could be used to mechanize the propositional finite many-valued logics and the propositional annotated logics. Experimental analyses are needed and this is part of future work.

  An L-interpretation I is a map I : For 0 → {1, . . . , N } and the set of Linterpretations is denoted Int L . The satisfiability relation |= is a ternary relation subset of Int L × {1, . . . , N } × For. (I, v, φ) ∈|= ((I, v, φ) ∈|= shall be written I, v |= φ)) is understood as "the formula φ takes the truth-value v under the interpretation I". The relation |= is inductively defined as follows:

  log |φ|) and computing g(φ) requires time O(|φ|.log |φ|) and space 3 O(log |φ|). Furthermore, the modal depth of g(φ) is only two, that is, two is the maximum number of nested modal operator 2 in g(φ). Lemma 3.3. Let M = W, R, m be a Kripke-style model based on a frame in C

  defined from the lattice structure {1, . . . , N }, ∩, ∪ );• I |= ¬ p i , v def ⇔ I |= p i , ∼ v ; • I |= ¬φ def ⇔ not I |= φ; • I |= φ 1 ∧ φ 2 def ⇔ I |= φ 1 and I |= φ 2 .

q

  [φ],v ) So |g (φ)| is also in O(|φ|.log |φ|) and computing g (φ) requires time O(|φ|.log |φ|) and space O(log |φ|).

The metavariables for atomic propositions are p, q, . . .. When q is subscripted by some natural number, we mean the exact member in the enumeration of the atomic propositions.

We hasten to point out that the symbol |= is being overloaded here. We'll continue this overloading throughout the paper, counting on context to make clear which satisfiability relation we have in mind.

As usual, the space (number of cells) occupied by the input and output tapes of the Turing machine is not counted for the space complexity.

For any annotated formula φ , there is a logically equivalent ¬ -free annotated formula φ computable in time O(|φ |).

Acknowlegments:

The author thanks Ricardo Caferra and Ewa Or lowska for their comments on an earlier version of this work.

The improvement in size is due to the fact that the length s can be less than (or equal to) ar(c i ). Let σ, σ be two strings over {1, . . . , ar(c i )}×{1, . . . , N }. We write σ σ def ⇔ σ can be obtained from σ be deleting some pairs in the sequence σ . For instance,

The empty string is denoted Λ. X c i v should satisfy the properties:

length at most ar(c i ), and for some j, v ∈ {1, . . . , ar

v is uniquely determined.

Lemma 3.5 ensures that the definition of φ i,v 3 below is more compact that the first one. The definition of φ i,v 3 is modified as follows.

In the case when X

3 is replaced by [U ](q 2.i+1 ⇔ q 2.v ) which corresponds exactly to φ j 3 when ar(c(j)) = 0. The worst-case complexity of the new map g remains unchanged since the computation of the X c i v 's for v ∈ {1, . . . , N } and for i ∈ {1, . . . , K} (such that ar(c i ) = 0) can be done once and for all, and therefore its cost is constant in the computation of g. It is also a routine task to check that Proposition 3.4 still holds true