Stéphane Demri
email: demri@imag.fr

Rajeev Goré

An O((n.log n) 3 )-time transformation from Grz into decidable fragments of classical first-order logic

The provability logic Grz is characterized by a class of modal frames that is not first-order definable. We present a simple embedding of Grz into decidable fragments of classical first-order logic such as FO 2 and the guarded fragment. The embedding is an O((n.log n) 3 )-time transformation that neither involves first principles about Turing machines (and therefore is easy to implement), nor the semantical characterization of Grz (and therefore does not use any second-order machinery). Instead, we use the syntactic relationships between cut-free sequent-style calculi for Grz, S4 and T. We first translate Grz into T, and then we use the relational translation from T into FO 2 .

Introduction

Propositional modal logics have proved useful in many areas of computer science because they capture interesting properties of binary relations (Kripke frames) whilst retaining decidability (see e.g. [START_REF] Vardi | Why is modal logic so robustly decidable? In Descriptive complexity and finite models[END_REF][START_REF] Van Benthem | The Range of Modal Logic -An Essay in Memory of George Gargov[END_REF]). By far the most popular method for automating deduction in these logics has been the method of analytic tableaux (see e.g. [START_REF] Fitting | Proof methods for modal and intuitionistic logics[END_REF][START_REF] Rautenberg | Modal tableau calculi and interpolation[END_REF][START_REF] Goré | Tableaux methods for modal and temporal logics[END_REF]), particularly because of the close connection between tableaux calculi and known cut-free Gentzen systems for these logics.

An alternative approach is to translate propositional modal logics into classical first-order logic since this allows us to use the wealth of knowledge in first-order theorem proving to mechanize modal deduction (see e.g. [START_REF] Ch | Methods for automated theorem proving in non classical logics[END_REF][START_REF] Ohlbach | A resolution calculus for modal logics[END_REF][START_REF] Herzig | Raisonnement automatique en logique modale et algorithmes d'unification[END_REF][START_REF] Agostino | A set-theoretical translation method for polymodal logics[END_REF][START_REF] Nonnengart | Resolution-based calculi for modal and temporal logics[END_REF][START_REF] Ohlbach | Combining Hilbert style and semantic reasoning in a resolution framework[END_REF]). Let FO n be the fragment of classical first-order logic using at most n individual variables and no function symbols. Any modal logic characterized by a firstorder definable class of modal frames can be translated into FO n for some fixed n ≥ 2. The decidable modal logic K4, for example, is characterised by transitive frames, definable using the first-order formula (∀x, y, z)(R(x, y) ∧ R(y, z) ⇒ R(x, z)) containing 3 variables. Since FO3 is undecidable and FO 2 is decidable, translating K4 into first-order logic does not automatically retain decidability. Of course, the exact fragment delineated by the translation is decidable. The only known first-order decision procedure for that particular fragment except the one that mimicks the rules for K4 is the one recently published in [START_REF] Ganzinger | A resolution-based decision procedure for extensions of K4[END_REF]. Therefore, blind translation is not useful if this means giving up decidability.

Moreover, it is well-known that many decidable propositional modal logics are characterised by classes of Kripke frames which are not firstorder definable, and that the "standard" relational translation (see e.g. [START_REF] Ch | Methods for automated theorem proving in non classical logics[END_REF][START_REF] Van Benthem | Modal logic and classical logic[END_REF]) is unable to deal with such logics. The class of such "second order" modal logics includes logics like G and Grz which have been shown to have "arithmetical" interpretations as well as logics like S4.3.1 which have interpretations as logics of linear time (without a next-time operator) [START_REF] Goré | Cut-free sequent and tableau systems for propositional Diodorian modal logics[END_REF].

Somewhat surprisingly, faithful translations into classical logic (usually augmented with theories) have been found for some propositional modal logics even when these logics are characterized by classes of frames that are not first-order definable. For instance, the modal logic K augmented with the McKinsey axiom is captured by the framework presented in [START_REF] Ohlbach | Optimized translation of multi modal logic into predicate logic[END_REF]. Similarly, the provability logic G 3 that admits arithmetical interpretations [START_REF] Solovay | Provability interpretations of modal logics[END_REF] is treated within the set-theoretical framework defined in [START_REF] Agostino | A set-theoretical translation method for polymodal logics[END_REF]. Both techniques in [START_REF] Ohlbach | Optimized translation of multi modal logic into predicate logic[END_REF][START_REF] Agostino | A set-theoretical translation method for polymodal logics[END_REF] use a version of classical logic augmented with a theory. Alternatively, G can also be translated into classical logic by first using the translation into K4 defined in [START_REF] Ph | A translation from the modal logic of provability into K4[END_REF] and then a translation from K4 into classical logic (see e.g. [START_REF] Van Benthem | Modal logic and classical logic[END_REF]).

The fact that G can be translated into a decidable fragment of classical logic follows from a purely complexity theory viewpoint, as shown next. Take a modal logic L that is in the complexity class C and let C be another complexity class. Here a logic is to be understood as a set of formulae and therefore a logic is exactly a (decision) problem in the usual sense in complexity theory. That is, as a language viewed as a set of strings built upon a given alphabet. By definition (see e.g. [START_REF] Ch | Computational Complexity[END_REF]), for any fragment of classical logic that is C-hard with respect to C many-one reductions4 , there is a mapping f in C such that any modal formula φ ∈ L iff f (φ) is valid in such a first-order fragment. From the facts that G is in PSPACE (see e.g. [START_REF] Ph | A translation from the modal logic of provability into K4[END_REF][START_REF] Ladner | The computational complexity of provability in systems of modal propositional logic[END_REF]), validity in FO 2 is NEXPTIME-hard [START_REF] Fürer | The computational complexity of the unconstrained limited domino problem (with implications for logical decision problems)[END_REF] (see also [START_REF] Lewis | Complexity results for classes of quantificational formulas[END_REF]) and PSPACE ⊆ NEXPTIME, it is easy to conclude that there exists a polynomial-time transformation from G into validity in FO 2 .

As is well-known, this illustrates the difference between the fact that a propositional modal logic K + φ is characterised by a class of frames which is not first-order definable, and the existence of a translation from K + φ into first-order logic. The weak point with this theoretical result is that the definition of f might require the use of first principles about Turing machines. If this is so, then realising the map f requires cumbersome machinery since we must first completely define a Turing machine that solves the problem. This is why the translations in [START_REF] Ohlbach | Optimized translation of multi modal logic into predicate logic[END_REF][START_REF] Ph | A translation from the modal logic of provability into K4[END_REF][START_REF] Agostino | A set-theoretical translation method for polymodal logics[END_REF] are much more refined and practical (apart from the fact that they allow to mechanise the modal logics under study).

Another well-known modal logic that is characterized by a class of modal frames that is not first-order definable is the provability logic Grz (for Grzegorczyk). The main contribution of this paper is the definition of an O(n.log n)-time transformation from Grz into S4, using cut-free sequent-style calculi for these respective logics. Renaming techniques from [START_REF] Mints | Gentzen-type and resolution rules part I: propositional logic[END_REF] are used in order to get the O(n.log n)-time bound. Then, we present a cubic-time transformation from S4 into T, again using the cutfree sequent-style calculi for these respective logics. Both reductions proceed via an analysis of the proofs in cut-free sequent calculi from the literature. The second reduction is a slight variant of the one presented in [START_REF] Cerrito | A polynomial translation of S4 into T and contraction-free tableaux for S4[END_REF] (see also [START_REF] Fitting | First-order modal tableaux[END_REF]). The reduction announced in the title can be obtained by translating T into FO 2 , which is known to be decidable (see e.g. [START_REF] Mortimer | On language with two variables[END_REF]). Furthermore, the formula obtained by reduction belongs to the decidable guarded fragment of classical logic (see e.g. [START_REF] Andreka | Modal languages and bounded fragments of predicate logic[END_REF]) for which a resolution decision procedure has been defined in [START_REF] De Nivelle | A resolution decision procedure for the guarded fragment[END_REF].

In [START_REF] Boolos | The Logic of Provability[END_REF] Chapter 12], a (non polynomial-time) transformation from Grz into G is defined. By using renamings of subformulae, it is easy to extract from that transformation, an O(n.log n)-time transformation from Grz into G [Boo93, Chapter 12]. There exists an O(n)-time transformation from G into K4 [START_REF] Ph | A translation from the modal logic of provability into K4[END_REF]. There exists an O(n 4 .log n)-time transformation from K4 into K using [START_REF] Cerrito | A polynomial translation of S4 into T and contraction-free tableaux for S4[END_REF] and renamings of subformulae. Finally, there exists an O(n)-time transformation from K into FO 2 [START_REF] Van Benthem | Modal logic and classical logic[END_REF].

Combining these results gives an O(n 4 .(log n) 5 )-time transformation from Grz into FO 2 , a decidable fragment of first-order logic.

The translation proposed in this paper is therefore a more refined alternative since it requires only time in O((n.log n) 3 ). As a side-effect, we obtain an O(n.log n)-time transformation from Grz into S4 and an O((n.log n) 3 )-time transformation from Grz into T. Using the space upper bound for S4-validity from [START_REF] Hudelmaier | Improved decision procedures for the modal logics K, T and S4[END_REF], we obtain that Grz requires only space in O(n 2 .(log n) 3 ). We are not aware of any tighter bound for Grz in the literature. Furthermore, our purely proof-theoretical analyses of the cut-free sequent-style calculi, and sometimes of the Hilbert-style proof systems, gives a simple framework to unify the transformations involved in [START_REF] Boolos | The Logic of Provability[END_REF][START_REF] Ph | A translation from the modal logic of provability into K4[END_REF][START_REF] Cerrito | A polynomial translation of S4 into T and contraction-free tableaux for S4[END_REF]. As we intend to report in a longer paper, it is also possible to generalise our method to handle other "second order" propositional modal logics like S4.3.1 using the calculi from [START_REF] Goré | Cut-free sequent and tableau systems for propositional Diodorian modal logics[END_REF] (see also [START_REF] Demri | Theoremhood preserving maps as a characterisation of cut elimination for provability logics[END_REF] for a generalisation and extension in the Display Logic framework [START_REF] Belnap | Display logic[END_REF]). This paper is a completed version of [START_REF] Demri | An O((n.log n) 3 )-time transformation from Grz into decidable fragments of classical first-order logic[END_REF].

Basic Notions

In the present paper, we assume that the modal formulae are built from a countably infinite set For 0 def = {p i,j : i, j ∈ ω} of atomic propositions using the usual connectives 2, ¬, ⇒, ∧. Other standard abbreviations include ∨, ⇔, 3. The set of modal formulae is denoted For. An occurrence of the subformula ψ in φ is positive [resp. negative] iff it is in the scope of an even [resp. odd] number of negations, where as usual, every occurrence of φ 1 ⇒ φ 2 is treated as an occurence of ¬(φ 1 ∧ ¬φ 2 ). For instance 2p 0,0 [resp. 2p 0,1 ] has a positive [resp. negative] occurrence in (22p 0,1 ) ⇒ (p 0,1 ∧ 2p 0,0 ). We write mwp(φ) [resp. mwn(φ)] to denote the number of positive [resp. negative] occurrences of 2 in φ. We write |φ| to denote the size of the formula φ, that is the number of symbols occurring in φ. φ is also represented as a string of characters.

We recall that the standard Hilbert system K is composed of the following axiom schemes: the tautologies of the Propositional Calculus (PC) and 2p ⇒ (2(p ⇒ q) ⇒ 2q). The inference rules of K are modus ponens ( from p and p ⇒ q infer q) and necessitation (from p infer 2p). By abusing our notation, we may identify the system K with its set of theorems, allowing us to write φ ∈ K to denote that φ is a theorem of K. Analogous notation is used for the following well-known extensions of K:

T def = K + 2p ⇒ p, K4 def = K + 2p ⇒ 22p, S4 def = K4 + 2p ⇒ p and Grz def = S4 + 2(2(p ⇒ 2p) ⇒ p) ⇒ 2p.
Numerous variants of the system Grz (having the same set of theorems) can be found in the literature (see for instance [START_REF] Goré | Relations between propositional normal modal logics: an overview[END_REF]).

We call GT , GS4 and GGrz the cut-free versions of the Gentzen-style calculi defined in [START_REF] Ohnishi | Gentzen method in modal calculi[END_REF][START_REF] Avron | On modal systems having arithmetical interpretations[END_REF] where the sequents are built from finite sets of formulae. Moreover, the weakening rule is absorbed in the initial sequents. For instance, the initial sequents of all the Gentzen-style calculi used in the paper are of the form Γ, φ ∆, φ where "," denotes set union. The common core of rules for the systems GT , GS4 and GGrz are presented in Figure 1. The introduction rules for 2 on the right-hand side are the following:

Γ φ Σ, 2Γ 2φ, ∆ ( 2) T 2Γ φ Σ, 2Γ 2φ, ∆ ( 2) S4 2Γ, 2(φ ⇒ 2φ) φ Σ, 2Γ 2φ, ∆ ( 2) Grz
where 2Γ def = {2ψ : ψ ∈ Γ }. Moreover, we assume that in Σ, there is no formula of the form 2ψ. This restriction is not essential for completeness (and for soundness) but it is used in the proof of Lemma 5. Each rule ( 2) T , ( 2) S4 and ( 2) Grz belongs respectively to GT , GS4 and GGrz. For each L ∈ {T, S4, Grz}, we know that for any sequent Γ ∆, the formula

( φ∈Γ φ) ⇒ ( φ∈∆ φ) ∈ L iff 5 the sequent Γ ∆ is derivable in GL (see e.g. [OM57,Avr84,Gor99]). Consequently, if Γ ∆ is derivable in GL, then so is Γ, Γ ∆, ∆ .

A transformation from Grz into S4

Let f : For × {0, 1} → For be the following map:

for any p ∈ For 0 , f (p, 0)

def = f (p, 1) def = p -f (¬φ, i) def = ¬f (φ, 1 -i) for i ∈ {0, 1} -f (φ 1 ∧ φ 2 , i) def = f (φ 1 , i) ∧ f (φ 2 , i) for i ∈ {0, 1} -f (φ 1 ⇒ φ 2 , i) def = f (φ 1 , 1 -i) ⇒ f (φ 2 , i) for i ∈ {0, 1} -f (2φ, 1) def = 2(2(f (φ, 1) ⇒ 2f (φ, 0)) ⇒ f (φ, 1)) f (2φ, 0) def = 2f (φ, 0).
In f (φ, i), the index i should be seen as information about the polarity of φ in the translation process as is done in [START_REF] Ph | A translation from the modal logic of provability into K4[END_REF] for the translation from G into K4. Observe that if we replace the definition of f (2φ, 1) above by f (2φ, 1)

def = 2(f (2(φ ⇒ 2φ) ⇒ φ, 1
)), we get the same map. Since the rule of replacement of equivalents is admissible in Grz, one can show by induction on the length of φ that for any φ ∈ For and for

any i ∈ {0, 1}, φ ⇔ f (φ, i) ∈ Grz. Moreover, Lemma 1. For any φ ∈ For, φ ⇒ f (φ, 1) ∈ K ⊆ S4 and f (φ, 0) ⇒ φ ∈ K ⊆ S4.
Proof. The proof is by simultaneous induction on the structure of φ. The base case when φ is an atomic proposition is immediate. By way of example, let us treat the cases below in the induction step:

(1)

φ 1 ∧ φ 2 ⇒ f (φ 1 ∧ φ 2 , 1) ∈ K (2) 2φ 1 ⇒ f (2φ 1 , 1) ∈ K (3) f (¬φ 1 , 0) ⇒ ¬φ 1 ∈ K (4) f (2φ 1 , 0) ⇒ 2φ 1 ∈ K.
(1) By the induction hypothesis, φ 1 ⇒ f (φ 1 , 1) ∈ K and φ 2 ⇒ f (φ 2 , 1) ∈ K. By easy manipulation at the propositional level,

φ 1 ∧ φ 2 ⇒ f (φ 1 , 1) ∧ f (φ 2 , 1) ∈ K. By definition of f , φ 1 ∧ φ 2 ⇒ f (φ 1 ∧ φ 2 , 1) ∈ K.
(2) By the induction hypothesis, φ 1 ⇒ f (φ 1 , 1) ∈ K. By easy manipulation at the propositional level,

φ 1 ⇒ (2(f (φ, 1) ⇒ 2f (φ, 0)) ⇒ f (φ 1 , 1)) ∈ K. It is known that the regular rule (from ψ 1 ⇒ ψ 2 infer 2ψ 1 ⇒ 2ψ 2 ) is admissible in K. So, 2φ 1 ⇒ 2(2(f (φ, 1) ⇒ 2f (φ, 0)) ⇒ f (φ 1 , 1)) ∈ K. By the definition of f , 2φ 1 ⇒ f (2φ 1 , 1) ∈ K.
(3) By the induction hypothesis, φ 1 ⇒ f (φ 1 , 1) ∈ K. By easy manipulation at the propositional level, ¬f

(φ 1 , 1) ⇒ ¬φ 1 ∈ K. By definition of f , f (¬φ 1 , 0) ⇒ ¬φ 1 ∈ K. (4) By the induction hypothesis, f (φ 1 , 0) ⇒ φ 1 ∈ K. Since the regular rule is admissible in K, 2f (φ 1 , 0) ⇒ 2φ 1 ∈ K. By the definition of f , f (2φ 1 , 0) ⇒ 2φ 1 ∈ K. Theorem 1. A formula φ ∈ Grz iff f (φ, 1) ∈ S4.
Proof. If f (φ, 1) ∈ S4, then a fortiori f (φ, 1) ∈ Grz, and since φ ⇔ f (φ, 1) ∈ Grz, we then obtain φ ∈ Grz. Now assume φ ∈ Grz, hence the sequent φ has a cut-free proof in GGrz. We can show that in the given cut-free proof of φ, for every sequent Γ ∆ with cut-free proof Π , the sequent f (Γ, 0) f (∆, 1) admits a cut-free proof in GS4. Here, f is extended to sets of formulae in the natural way. So, we shall conclude that f (φ, 1) is derivable in GS4 and therefore f (φ, 1) ∈ S4. The proof is by induction on the structure of the derivations.

Base case: When Γ ∆ is an initial sequent Γ , ψ ψ, ∆ , we can show that f (Γ , 0), f (ψ, 0) f (ψ, 1), f (∆ , 1) has a cut-free proof in GS4 since f (ψ, 0) ⇒ f (ψ, 1) ∈ S4. By completeness of GS4, f (ψ, 0) f (ψ, 1) has a proof in GS4. Induction step: The structural rules pose no difficulties because by definition f is homomorphic with respect to the comma. By way of example, the proof step (in GGrz)

. . . . 2Γ , 2(ψ ⇒ 2ψ) ψ Γ, 2Γ 2ψ, ∆ ( 2)
Grz is transformed into the proof steps (in GS4)

. . . .

2f (Γ , 0), 2(f (ψ, 1) ⇒ 2f (ψ, 0)) f (ψ, 1) 2f (Γ , 0) 2(f (ψ, 1) ⇒ 2f (ψ, 0)) ⇒ f (ψ, 1) ( ⇒) f (Γ, 0), 2f (Γ , 0) 2(2(f (ψ, 1) ⇒ 2f (ψ, 0)) ⇒ f (ψ, 1)), f (∆, 1) ( 2) S4
The induction hypothesis is used here since 2f (Γ , 0), 2(f (ψ, 1) ⇒ 2f (ψ, 0)) f (ψ, 1) has a (cut-free) proof in GS4. Furthermore, by definition,

-f (2Γ , 0) = 2f (Γ , 0); f (2ψ, 1) = 2(2(f (ψ, 1) ⇒ 2f (ψ, 0)) ⇒ f (ψ, 1)); -f (2(ψ ⇒ 2ψ), 0) = 2(2(f (ψ, 1) ⇒ 2f (ψ, 0))).
Observe that f (Γ, 0) does not contain any formula of the form 2ψ . The proof (in GGrz) . . . .

Γ, 2ψ, ψ ∆ Γ, 2ψ ∆ (2 )
is transformed into the proof (in GS4)

. . . .

f (Γ, 0), 2f (ψ, 0), f (ψ, 0) f (∆, 1) f (Γ, 0), 2f (ψ, 0) f (∆, 1) (2 )
Indeed, f (2ψ, 0) = 2f (ψ, 0). The other cases are not difficult to obtain and they are omitted here.

A close examination of f shows that f is not computable in O(n.log n)time. Indeed, the right-hand side in the definition of f (2φ, 1) requires several recursive calls to f and the computation of f is therefore exponentialtime. However, we can use a slight variant of f that uses renamings as done in [START_REF] Mints | Gentzen-type and resolution rules part I: propositional logic[END_REF]. Specifically, we have, (Renaming) φ ∈ S4 iff 2(p new ⇔ ψ) ⇒ φ ∈ S4 where φ is obtained from φ by replacing every occurrence of ψ in φ by the atomic proposition p new not occurring in φ.

Let φ be a modal formula we wish to translate from Grz into S4. Let φ 1 , . . . , φ m be an enumeration (without repetition) of all the subformulae of φ in increasing order with respect to the size such that the n first formulae are all the atomic propositions occurring in φ. We shall build a formula g(φ) using {p i,j : 1 ≤ i ≤ m, j ∈ {0, 1}} such that g(φ) ∈ S4 iff f (φ, 1) ∈ S4. Moreover, g(φ) can be computed in time O(|φ|.log |φ|). For i ∈ {1, . . . , m}, we associate a formula ψ i as shown in Figure 2 and let g(φ

) def = ( m i=1 ψ i ) ⇒ p m,1 . Form of φi ψi p 2(p i,0 ⇔ p i,1 ) ¬φj 2(p i,1 ⇔ ¬p j,0 ) ∧ 2(p i,0 ⇔ ¬p j,1 ) φi 1 ∧ φi 2 2(p i,1 ⇔ (p i 1 ,1 ∧ p i 2 ,1 )) ∧ 2(p i,0 ⇔ (p i 1 ,0 ∧ p i 2 ,0 )) φi 1 ⇒ φi 2 2(p i,1 ⇔ (p i 1 ,0 ⇒ p i 2 ,1 )) ∧ 2(p i,0 ⇔ (p i 1 ,1 ⇒ p i 2 ,0 )) 2φj 2(p i,1 ⇔ 2(2(p j,1 ⇒ 2p j,0 )) ⇒ p j,1 )) ∧ 2(p i,0 ⇔ 2p j,0 ) Fig. 2. Definition of ψi Lemma 2. (1) f (φ, 1) ∈ S4 iff g(φ) ∈ S4 (2) computing g(φ) requires time in O(|φ|.log |φ|) (3) |g(φ)| is in O(|φ|.log |φ|) (4) mwp(g(φ)) + mwn(g(φ)) is in O(|φ|).
Proof.

(2)-( 4) is by simple inspection of the definition of g(φ). The idea of the proof of (1) is to effectively build g(φ) from f (φ, 1) by successively applying transformations based on (Renaming). Such a process requires exponential-time in φ (since |f (φ, 1)| can be exponential in |φ|). However, we can build g(φ) in a tractable way (see (2)-( 4)) since g translates and renames simultaneously.

(1) Let us build g(φ) from f (φ, 1) by successively applying transformations based on (Renaming). For any atomic proposition q = φ i occurring in f (φ, 1), replace the positive [resp. negative] occurrences of q by p i,1 [resp. p i,0 ]. Let us say that we obtain the formula ψ (this shall be our current working formula). The constraint formula, say C, is defined as

C def = n i=1 2(p i,1 ⇔ p i,0
). Along the steps, we shall have that f (φ, 1) ∈ S4 iff C ⇒ ψ ∈ S4. The next steps consist of replacing subformulae ψ in ψ by their renaming equivalent and then to update C appropriately until ψ = p m,1 . For instance, take a subformula ψ = p i,1 ∧ p j,1 in ψ. Replace every occurrence of p i,1 ∧p j,1 in ψ by p k,1 with φ k = φ i ∧φ j . The constraint formula C is updated as follows: C := C ∧ 2(p k,1 ⇔ (p i,1 ∧ p j,1 )). The other cases are omitted and they use the decomposition from Figure 2

. So, when ψ is equal to p m,1 , f (φ, 1) ∈ S4 iff C ⇒ p m,1 ∈ S4. It is easy to see that ( m i=1 ψ i ) ⇒ p m,1 ∈ S4 iff C ⇒ p m,1 . Indeed, the set of conjuncts of C is a subset of the set of conjuncts of m i=1 ψ i . So, if C ⇒ p m,1 ∈ S4, then g(φ) ∈ S4.
In order to show that the converse also holds, let us define the binary relation DEP between atomic propositions. Let p i 1 ,j 1 and p i 2 ,j 2 be atomic propositions occurring in m i=1 ψ i . We write p i 1 ,j 1 DEP p i 2 ,j 2 to denote that there is a conjunct of m i=1 ψ i of the form 2(ψ 1 ⇔ ψ 2 ) such that either p i 1 ,j 1 occurs in ψ 1 and p i 2 ,j 2 occurs in ψ 2 or p i 1 ,j 1 occurs in ψ 2 and p i 2 ,j 2 occurs in ψ 1 . Let DEP * be the smallest equivalence relation including DEP . It is easy to see that if g(φ) ∈ S4, then C ⇒ p m,1 ∈ S4 since for all the atomic propositions q occurring in m i=1 ψ i but not in C, not qDEP * p m,1 .

Theorem 2. Grz requires space in O(n 2 .(log n) 3 ).

An equivalent statement is that there exists a deterministic Turing machine in SPACE(O(n 2 .(log n) 3 )) that solves the Grz-provability problem. This follows from the facts that S4 requires space in O(n 2 .log n) [START_REF] Hudelmaier | Improved decision procedures for the modal logics K, T and S4[END_REF], computing g(φ) requires space in O(|φ|.log |φ|), and |g(φ)| is in O(|φ|.log |φ|). Putting these together gives that checking whether g(φ) is an S4-theorem requires space in O((|φ|.log |φ|) 2 .log(|φ|.log |φ|)), that is space in O(|φ| 2 .(log |φ|) 3 ). By the way, one can show that Grz is PSPACE-hard by using mappings from propositional intuitionistic logic into Grz (see e.g. [START_REF] Chagrov | Modal Logic[END_REF]).

A transformation from Sinto T

Let h : For × ω × {0, 1} → For be the following map (n ∈ ω, i ∈ {0, 1}):

for any p ∈ For 0 , h(p, n, 0)

def = h(p, n, 1) def = p -h(¬φ, n, i) def = ¬h(φ, n, 1 -i) -h(φ 1 ∧ φ 2 , n, i) def = h(φ 1 , n, i) ∧ h(φ 2 , n, i) -h(φ 1 ⇒ φ 2 , n, i) def = h(φ 1 , n, 1 -i) ⇒ h(φ 2 , n, i) -h(2φ, n, 1) def = 2h(φ, n, 1) -h(2φ, n, 0) def = 2 n h(φ, n, 0) if n ≥ 1 2h(φ, n, 0) otherwise
The map h is a slight variant of the map M S4,T defined in [CCM97] which itself is a variant of a map defined in [START_REF] Fitting | First-order modal tableaux[END_REF]. The main difference is that we do not assume that the formulae are in negative normal form (which is why a third argument dealing with polarity is introduced here). In that sense, we follow [Fit88, Section 3]. Furthermore, since we are dealing here with validity instead of inconsistency, the treatment of the modal operators is dual. Lemma 3. For any formula φ ∈ For and for any 0 ≤ m ≤ n,

(1) φ ⇔ h(φ, n, 0) ∈ S4 and φ ⇔ h(φ, n, 1) ∈ S4.

(2) h(φ, n, 0) ⇒ h(φ, m, 0) ∈ T and h(φ, m, 1) ⇒ h(φ, n, 1) ∈ T .

(3) h(φ, n, 0) ⇒ h(φ, n, 1) ∈ T .

Proof. The proof of (1) uses the facts that the rule of replacement of equivalents is admissible in S4 and 2 n ψ ⇔ 2ψ ∈ S4 for any n ≥ 1 and for any ψ ∈ For. The proof of (2) is by simultaneous induction on the size of the formula. By way of example, let us show in the induction step that h(2φ, n, 0) ⇒ h(2φ, m, 0) ∈ T . By induction hypothesis, h(φ, n, 0) ⇒ h(φ, m, 0) ∈ T . It is known that the regular rule is admissible for T. So, by applying this rule n times on h(φ, n, 0) ⇒ h(φ, m, 0), we get that

2 n h(φ, n, 0) ⇒ 2 n h(φ, m, 0) ∈ T . Since 2 n h(φ, m, 0) ⇒ 2 m h(φ, m, 0) ∈ T (remember m ≤ n and 2ψ ⇒ ψ ∈ T ), then 2 n h(φ, n, 0) ⇒ 2 m h(φ, m, 0) ∈ T . (3) If n = 0, then h(φ, n, 0) = h(φ, n, 1) = φ. Now assume n ≥ 1.
The proof is by induction on the structure of φ. The base case when φ is an atomic proposition is immediate. Let us treat the cases φ = ¬φ and φ = 2φ in the induction step. By Induction Hypothesis, h(φ , n, 0) ⇒ h(φ , n, 1) ∈ T . By manipulation at the propositional level, ¬h(φ , n, 1) ⇒ ¬h(φ , n, 0) ∈ T . By definition of h, h(¬φ , n, 0) ⇒ h(¬φ , n, 1) ∈ T . Moreover, by applying n times the regular rule (admissible in T) on h(φ , n, 0) ⇒ h(φ , n, 1), we get 2 n h(φ , n, 0) ⇒ 2 n h(φ , n, 1) ∈ T . Moreover,

-2 n h(φ , n, 1) ⇒ 2h(φ , n, 1) ∈ T ; -2 n h(φ , n, 0) = h(2φ , n, 0); -2h(φ , n, 1) = h(2φ , n, 1). So, h(2φ , n, 0) ⇒ h(2φ , n, 1) ∈ T .
The map h is extended to sets of formulae in the most natural way.

Lemma 4. Let Γ ∆ be a sequent that has a (cut-free) proof Π in GS4 such that the maximum number of ( 2) S4 -rule inferences in any branch is at most n. Then, h(Γ, n, 0) h(∆, n, 1) has a (cut-free) proof in GT.

Lemma 4 is an extension of Lemma 2.2 in [START_REF] Cerrito | A polynomial translation of S4 into T and contraction-free tableaux for S4[END_REF].

Proof. The proof is by double induction on n and then on the length of the proof Π of Γ ∆. The length of Π is just the number of nodes of the proof tree. Base case (i): n = 0. By definition, h(Γ, 0, 0) = Γ and h(∆, 0, 1) = ∆. Any proof of Γ ∆ in GS4 with no applications of ( 2) S4 is also a proof of Γ ∆ in GT . Induction step (i): assume that for any sequent Γ ∆ having a (cut-free) proof in GS4 such that the maximum number of ( 2) S4 -rule inferences in any branch is at most n -1 ≥ 0, h(Γ, n -1, 0) h(∆, n -1, 1) has a (cut-free) proof in GT. Now, let Γ ∆ be a sequent that has a (cut-free) proof Π in GS4 such that the maximum number of ( 2) S4 -rule inferences in any branch is at most n. We use an induction on the length of Π. Base case (ii): Γ ∆ is an initial sequent Γ , φ ∆ , φ. By Lemma 3(3), h(φ, n, 0) ⇒ h(φ, n, 1) ∈ T . So, h(φ, n, 0) h(φ, n, 1) has a cut-free proof in GT by completeness of GT with respect to T. Hence, h(Γ , n, 0), h(φ, n, 0) h(∆ , n, 1), h(φ, n, 1) has a cut-free proof in GT . Induction step (ii): assume that for any sequent Γ ∆ having a (cutfree) proof Π of length at most n -1 ≥ 1 in GS4 such that the maximum number of ( 2) S4 -rule inferences in any branch is at most n, h(Γ, n, 0) h(∆, n, 1) has a (cut-free) proof in GT. Now, let Γ ∆ be a sequent that has a (cut-free) proof Π in GS4 of length n such that the maximum number of ( 2) S4 -rule inferences in any branch is at most n. Among the Boolean connectives, we only treat here the case for the conjunction since the cases for ¬ and ⇒ are similar. The proof Π below (in GS4) . . . .

Γ , φ 1 , φ 2 ∆ Γ , φ 1 ∧ φ 2 ∆ (∧ )
is transformed into the proof below (in GT ) using the induction hypothesis (ii) . . . .

h(Γ , n, 0), h(φ 1 , n, 0), h(φ 2 , n, 0) h(∆ , n, 1) h(Γ , n, 0), h(φ 1 ∧ φ 2 , n, 0) h(∆ , n, 1) (∧ )
The proof Π below (in GS4) . . . .

Γ ∆ , φ 1 Γ ∆ , φ 2 Γ ∆ , φ 1 ∧ φ 2 ( ∧)
is transformed into the proof below (in GT ) using the induction hypothesis (ii) . . . . h(Γ , n, 0) h(∆ , n, 1), h(φ 1 , n, 1) h(Γ , n, 0) h(∆ , n, 1), h(φ 2 , n, 1) h(Γ , n, 0) h(∆ , n, 1), h(φ 1 ∧ φ 2 , n, 1) ( ∧)

Consider the proof Π below:

Π . . . . 2Γ φ Γ , 2Γ 2φ, ∆ ( 2) S4
In the proof Π of 2Γ φ in GS4, the maximum number of ( 2) S4 -rule inferences in any branch is less than n -1. By induction hypothesis (i), h(2Γ , n -1, 0) h(φ, n -1, 1) has a cut-free proof, say Π , in GT . So, the proof below is obtained in GT : Π . . . .

2 n-1 h(Γ , n -1, 0) h(φ, n -1, 1) h(Γ , n, 0), 2 n h(Γ , n -1, 0) 2h(φ, n -1, 1), h(∆ , n, 1)
( 2) T For ψ ∈ Γ , h(ψ, n, 0) ⇒ h(ψ, n -1, 0) ∈ T by Lemma 3(2). By using n applications of the regular rule, for ψ ∈ Γ , 2 n h(ψ, n, 0) ⇒ 2 n h(ψ, n -1, 0) ∈ T . Similarly, by Lemma 3(2) h(2φ, n -1, 1) ⇒ h(2φ, n, 1) ∈ T . By soundness of GT , the formula ϕ ∈ T where:

ϕ def = (( ψ∈Γ h(ψ, n, 0))∧( ψ∈Γ 2 n h(ψ, n-1, 0))) ⇒ (h(2φ, n-1, 1)∨ ψ∈∆ h(ψ, n, 1)).
For ψ ∈ Γ , 2 n h(ψ, n-1, 0) occurs negatively in ϕ and h(2φ, n-1, 1) occurs positively in ϕ. By the Monotonicity of Entailment Lemma [AM86],

((

ψ∈Γ h(ψ, n, 0))∧( ψ∈Γ 2 n h(ψ, n, 0))) ⇒ (h(2φ, n, 1)∨ ψ∈∆ h(ψ, n, 1)) ∈ T
By completeness of GT , we get that h(Γ , n, 0), h(2Γ , n, 0) h(2φ, n, 1), h(∆ , n, 1) has a cut-free proof in GT . In order to conclude the proof, let us treat the last case. Consider the proof Π below in GS4: . . . .

Γ , 2φ, φ ∆ Γ , 2φ ∆ (2 )
By induction hypothesis (ii), h(Γ , n, 0), 2 n h(φ, n, 0), h(φ, n, 0) h(∆ , n, 1) has a cut-free proof in GT . So,

s 1 def = h(Γ , n, 0), 2 n h(φ, n, 0), 2 n-1 h(φ, n, 0), . . . , 2h(φ, n, 0), h(φ, n, 0) h(∆ , n, 1)
has also a cut-free proof in GT . The above proof is transformed into (in GT ) . . . .

s 1 h(Γ , n, 0), 2 n h(φ, n, 0), 2 n-1 h(φ, n, 0), . . . , 2h(φ, n, 0) h(∆ , n, 1) (2 ) h(Γ , n, 0), 2 n h(φ, n, 0), 2 n-1 h(φ, n, 0), . . . , 2 2 h(φ, n, 0) h(∆ , n, 1) (2 ) . . . . h(Γ , n, 0), 2 n h(φ, n, 0), 2 n-1 h(φ, n, 0) h(∆ , n, 1) h(Γ , n, 0), h(2φ, n, 0) h(∆ , n, 1) (2 )
Lemma 5. Let Γ ∆ be a sequent such that the number of negative occurrences of 2 in φ∈Γ φ ⇒ ψ∈∆ ψ is n. If Γ ∆ has a (cut-free) proof in GS4, then Γ ∆ has a (cut-free) proof in GS4 such that the ( 2) S4 -rule is applied at most n + 1 times to the same formula in every branch.

Lemma 5 is also an extension of Lemma 2.4 in [START_REF] Cerrito | A polynomial translation of S4 into T and contraction-free tableaux for S4[END_REF]. However, its proof mainly relies on the analysis of the proof of [CCM97, Lemma 2.4]. So it is included here in order to make the paper self-contained.

Proof. First, observe that if Γ ∆ is derivable in GS4 and if ψ has a negative [resp. positive] occurrence in ( φ∈Γ φ) ⇒ ( φ∈∆ φ), then for any cut-free proof Π of Γ ∆, every occurrence of ψ in Π can only occur in the left-hand side [resp. in the right-hand side] of sequents. So if the inference below

2Γ φ Γ , 2Γ 2φ, ∆ ( 2) S4
occurs in a proof Π of Γ ∆, then any 2ψ ∈ 2Γ occurs with negative polarity in ( φ∈Γ φ) ⇒ ( φ∈∆ φ). Moreover, consider the following ( 2) S4 inferences in a proof Π of Γ ∆:

2Γ 2 φ 2 Γ 2 , 2Γ 2 2φ 2 , ∆ 2 ( 2) S4 . . . . 2Γ 1 φ 1 Γ 1 , 2Γ 1 2φ 1 , ∆ 1 ( 2) S4 . . . . Then Γ 1 ⊆ Γ 2 . Let Π be a (cut-free) proof of Γ ∆ in GS4.
Assume there is a branch in Π containing n + 1 + k (k ≥ 1) ( 2) S4 inferences introducing the same formula 2ψ. Let us eliminate at least one ( 2) S4 inference on that branch as done in [START_REF] Cerrito | A polynomial translation of S4 into T and contraction-free tableaux for S4[END_REF]. Consider the sequence inf 1 , . . . , inf n+1+k of inferences of the form (1 ≤ i ≤ n + 1 + k),

2Γ i ψ Γ i , 2Γ i 2ψ, ∆ i ( 2) S4
We assume that if i < j, then inf j occurs above inf i . Let Γ be the set of the formulae of the form 2ψ where 2ψ has a negative occurrence in ( φ∈Γ φ) ⇒ ( φ∈∆ φ). Since Γ 1 ⊆ . . . ⊆ Γ n+1+k and card(Γ ) = n, there exist i 0 ∈ {1, . . . , n + 1} and j 0 ∈ {i 0 , . . . , n + 2} such that Γ i 0 = Γ j 0 . So, in that branch of Π, we can replace the sequence shown below left by the sequence shown below right: Π . . . . 2Γ j 0 ψ Γ j 0 , 2Γ j 0 2ψ, ∆ j 0 ( 2) S4 . . . .

2Γ i 0 ψ Γ i 0 , 2Γ i 0 2ψ, ∆ i 0
( 2) S4 Π . . . .

2Γ j 0 ψ Γ j 0 , 2Γ j 0 2ψ, ∆ j 0 ( 2) S4
Theorem 3. A formula φ ∈ S4 iff h(φ, (mwn(φ) + 1).mwp(φ), 1) ∈ T .

Theorem 3 is a mere consequence of Lemma 4 and Lemma 5. Its proof uses the sequent calculi GS4 and GT whereas in [START_REF] Cerrito | A polynomial translation of S4 into T and contraction-free tableaux for S4[END_REF] the proofs manipulate Fitting's non prefixed calculi for S4 and T [START_REF] Fitting | Proof methods for modal and intuitionistic logics[END_REF]. Observe the map h is a variant of a map defined in [START_REF] Fitting | First-order modal tableaux[END_REF]. Let us write h (φ) to denote the formula h(φ, (mwn(φ) + 1).mwp(φ), 1).

By close examination of the definition of h (φ), The relational translation from T into FO 2 (see e.g. [START_REF] Van Benthem | Modal logic and classical logic[END_REF]) with a smart recycling of the variables requires only linear-time and the size of the translated formula is also linear in the size of the initial formula. We warn the reader that in various places in the literature it is stated that the relational translation exponentially increases the size of formulae; this is erroneous. Using this "smart" relational transformation, the composition of various transformations in the paper provides an O((n.log n) 3 )-time transformation from Grz into the decidable fragment FO 2 of classical logic. It is easy to see that the resulting formula is in the guarded fragment of classical logic (see e.g. [START_REF] Andreka | Modal languages and bounded fragments of predicate logic[END_REF]), for which a proof procedure based on resolution is proposed in [START_REF] De Nivelle | A resolution decision procedure for the guarded fragment[END_REF]. Alternatively, after translating Grz into T, the techniques from [START_REF] Schmidt | Optimised Modal Translation and Resolution[END_REF] could also be used to translate T into classical logic. These are possibilities to obtain a decision procedure for Grz using theorem provers for classical logic.

Fig. 1 .

 1 Fig. 1. Common core of rules

1

  . computing h (φ) requires time in O(|φ| 3 ); 2. |h (φ)| is in O(|φ| 3 ). So a formula φ ∈ Grz iff h (g(φ)) ∈ T .1. Computing h (g(φ)) requires time in O((|φ|.log |φ|) 3 ) (remember mwp(g(φ))+ mwn(g(φ)) is in O(|φ|); 2. |h (g(φ))| is in O((|φ|.log |φ|) 3 ).

Also called GL (for Gödel and Löb), KW, K4W, PrL.

Also called "transformation", see e.g.[START_REF] Ch | Computational Complexity[END_REF].

Γ, φ ∆, φ (initial sequents)Γ ∆, φ Γ, ¬φ ∆ (¬ ) Γ, φ ∆ Γ ∆, ¬φ ( ¬) Γ, φ1, φ2 ∆ Γ, φ1 ∧ φ2 ∆ (∧ ) Γ ∆, φ1 Γ ∆, φ2 Γ ∆, φ1 ∧ φ2 ( ∧) Γ ∆, φ1 Γ, φ2 ∆ Γ, φ1 ⇒ φ2 ∆ (⇒ ) Γ, φ1 ∆, φ2 Γ ∆, φ1 ⇒ φ2 ( ⇒) Γ, 2φ, φ ∆ Γ, 2φ ∆(2 )

As is usual, the empty conjunction is understood as the verum logical constant (or simply p 0,0 ∨ ¬p 0,0 ) and the empty disjunction is understood as the falsum logical constant ⊥ (or simply p 0,0 ∧ ¬p 0,0 ).

We are currently investigating whether this translation can be extended to first-order Grz (FOGrz). But the set of valid formulae for first-order Gödel-Löb logic, a close cousin of FOGrz, is not recursively enumerable [Boo93, Chapt. 17], and we suspect that this result also holds for FOGrz.

Supported by an Australian Research Council Queen Elizabeth II Fellowship.


Tayeb Zaoui

Mansour Debdab
email: mansour.debdab@univ-tiaret.dz

Boumediene Haddad

El Habib Belarbi

Yassine Chaker

Mustapha Rahmouni

Serge Bresson

Vincent Baeten

Synthesis, vibrational and thermal properties of new functionalized 1-(2-hydroxyethyl) -3-methylimidazolium dihydrogenophosphate ionic liquid

Keywords: Hydroxyl-functionalized ionic liquids, dihydrogenophosphate anion, NMR spectra, IR spectra, RAMAN spectra, thermal stability

Very recently, the hydroxyl-functionalized ionic liquids have gained immense interest and were developed for a number of interesting applications.In this work and for the first time new hydroxyl-functionalized

was synthesized in our laboratory. The synthesis is based on an alkylation reaction of 1-methylimidazole followed by anion exchange. The obtained IL is characterized by 1 H-NMR, 13 C-NMR spectroscopy. This experimental vibrational spectroscopy have been investigated using Infrared and Raman spectroscopy, based on the infrared (IR) and Raman spectroscopies results, complete vibrational assignments have been performed. Besides, thermal properties of this hydroxyl-functionalized IL were investigated by using following techniques, (i) Thermogravimetric Analysis (TGA) and Derivative Thermogravimetry (DTG) in the temperature range from 20 to 600 C°, (ii) differential scanning calorimetry (DSC) from-100 °C to 200 °C. The thermogravimetry analysis was coupled with mass spectrometry in order to assess the influence of anion on the measured property.

Introduction:

In the early 1990's, for the vast majority of chemists, the term ionic liquid was obscure and little known.

Since 2000, the research in this area has been focused and greatly expanded. Indeed, their physicochemical properties are very interesting and varied, and the multiple possibly applications in organic chemistry make these entities the compounds of choice as substitute solvents for catalysis [START_REF] Betz | Recent advances in oxidation catalysis using ionic liquids as solvents[END_REF][START_REF] Haddad | Synthesis of palladium-bidentate complex and its application in Sonogashira and Suzuki coupling reactions[END_REF] and supported synthesis [START_REF] Fraga-Dubreuil | Grafted ionic liquid-phase-supported synthesis of small organic molecules[END_REF][START_REF] Debdab | Ionic-liquid-supported synthesis of amines and derivatives[END_REF]. In addition, the physical and chemical properties of the Ionic Liquids (ILs) are modifiable by varying the anion / cation combinations. This enabled the design of systems adaptable to various applications (electrochemistry, organic, inorganic and enzymatic synthesis, catalysis ...) but also to adjust the physicochemical properties of these organic salts according to needs.

In this area, several works focused on the synthesis and application of new class of ionic liquids, namely; hydroxyl functionalized ionic liquids containing, bromide, chloride, iodide, tetrafluoroborate,picrate, hexafluorophosphate,bis(trifluoromethylsulfonyl)imide, nitrate, alkyl sulfates, dicyanamide, thiocynate, and trifluoromethanesulfate anions [START_REF] Nie | Thermodynamic properties of the water+ 1-(2hydroxylethyl)-3-methylimidazolium chloride system[END_REF][START_REF] Qu | Efficient dehydration of glucose to 5hydroxymethylfurfural catalyzed by the ionic liquid, 1-hydroxyethyl-3-methylimidazolium tetrafluoroborate[END_REF][START_REF] Najdanovic-Visak | Co-solvent effects in LLE of 1-hydroxyethyl-3-methylimidazolium based ionic liquids+ 2-propanol+ dichloromethane or 1, 2-dichloroethane[END_REF][START_REF] Jalili | Solubility of CO2 in 1-(2-hydroxyethyl)-3-methylimidazolium ionic liquids with different anions[END_REF][START_REF] Zhang | Investigation of cation-anion interaction in 1-(2-hydroxyethyl)-3-methylimidazolium-based ion pairs by density functional theory calculations and experiments[END_REF][START_REF] Sakhaeinia | Solubility of H2S in 1-(2-hydroxyethyl)-3-methylimidazolium ionic liquids with different anions[END_REF][START_REF] Panja | Clusters of the Ionic Liquid 1-Hydroxyethyl-3-methylimidazolium Picrate: From Theoretical Prediction in the Gas Phase to Experimental Evidence in the Solid State[END_REF][12][START_REF] Panja | Cluster formation through hydrogen bond bridges across chloride anions in a hydroxyl-functionalized ionic liquid[END_REF].Compared to the traditional ILs, this class of ILs have received much attention in many applications, especially in the fields of catalysis [START_REF] Sun | Hydroxyl-functionalized ionic liquid: a novel efficient catalyst for chemical fixation of CO2 to cyclic carbonate[END_REF], biotechnology [START_REF] Reslan | Ionic liquids as biocompatible stabilizers of proteins[END_REF], sonochemistry [START_REF] Merouani | Acoustic cavitation in 1-butyl-3-methylimidazolium bis (triflluoromethyl-sulfonyl) imide based ionic liquid[END_REF]andorganic synthesis [START_REF] Fan | Lipase-catalyzed synthesis of biodiesel in a hydroxyl-functionalized ionic liquid[END_REF].

In this respect and at spectroscopic point of view, there are extensive works published in this area (see Ref. [START_REF] Paschoal | Vibrational spectroscopy of ionic liquids[END_REF] and references therein), However, compared to the hydroxyl functionalized ionic liquids already synthesized and published and to the best of our knowledge, there are no reports in the literature dealing the synthesis, thermal and vibrational spectroscopy of 1-(hydroxyethyl)-3methylimidazoliumdihydrogenophosphate [EtOHMIM + ][ H 2 ]. This inorganic anion used in numerous analytical methods andis one of the anions in the dissociation equilibrium of phosphoric acid dissolved in water [START_REF] Perez-Olivan | Determination of grepafloxacin in plasma samples by HPLC: Application to clinical pharmacokinetic studies[END_REF][START_REF] Lamrini | Evaluation of hydroxyl radicals production using 13CO2 gas chromatography-isotope ratio mass spectrometry[END_REF].

Very recently, we have investigated the vibrational and thermal properties of1-(hydroxyethyl)-3methylimidazolium cation coupled with sulphate and chloride anion [START_REF] Chaker | Synthesis and characterization of 1-(hydroxyethyl)-3-methylimidazolium sulfate and chloride ionic liquids[END_REF]by using IR /Raman spectroscopic and thermal analysis. In this work, we thought to synthesize this functionalized ionic liquid but with dihydrogenophosphate [H 2 ] anion there are no reports in the spectroscopic literature dealing to the vibrational spectroscopy of1-(hydroxyethyl)-3-methylimidazolium with this anion.

On the other hand and contrary to that published with this cation, the synthesis, vibrational spectroscopy and the thermal properties of this ionic liquid coupled with dihydrogenophosphate are not covered yet by the literature. In this framework, we have set out to prepare 1-(hydroxyéthyl)-3-methylimidazolium dihydrogeno phosphate. This new functionalized ionic liquid has been structurally identified using Nuclear magnetic resonance (NMR). Furthermore, infrared and Raman spectroscopy have been adopted to evaluate their vibrational spectroscopy properties. Finally; their thermal properties have been investigated by thermogravimetric analysis TGA, DTG and DSC.

In order to study the impact of the anion on the thermal and vibrational behavior, we show an example of recent study [START_REF] Chaker | Synthesis and characterization of 1-(hydroxyethyl)-3-methylimidazolium sulfate and chloride ionic liquids[END_REF]. For the metathesis reaction a mixture of 1-(2-hydroxyethyl) -3-methylimidazolium chloride (5 g, 0.0252 mol) and ortho-phosphoric acid (08 ml, 0.062 mol) was carried out at room temperature for 24h with vigorous magnetic stirring in 30 ml acetonitrile. The crude was washed with diethyl ether (3 x 80 ml) after elimination of acetonitrile and then concentrated on a rotary evaporator under reduced pressureyielding a pale viscous yellow liquid. Finally, in order to obtain high purity and to remove any possible water contamination before their use, our obtained ionic liquid was dried under vacuum (10 3- bar). The yield of this reaction was(98%). The general procedure for the synthesis of 1-(hydroxyethyl)-3-

methylimidazoliumdihydrogenophosphate[EtOHMIM + ][H 2 PO 4 - ] is summarized in Scheme 1. Scheme 1. Synthetic route of [EtOHMIM + ][H 2 PO 4 - ].

NMR spectroscopy analysis:

The structure and purity of our investigated functionalized ILs were confirmed by spectral analysis: 1 H and

FTIR/ATR measurements

The samples measurements were performed in the Walloon Agricultural Research Center (CRA-W)

Belgium. Fourier Transform mid-infrared All attenuated total reflectance (FTIR /ATR) measurements were acquired on a Bruker Vertex II-70 RAM Spectrometer (Bruker Analytical, Madison, WI) operating with a Golden Gate diamond ATR accessory TM (Specac Ltd, Slough, United Kingdom). FTIR/ATR spectra [4000-600 cm -1 ] were collected with a resolution of 1cm -1 by co-adding 64 scans for each spectrum. The OPUS Software 6.0 was used for the management of the instrument.

FT-Raman measurements

These measurements were also carried out in the Walloon Agricultural Research Center (CRA-W) in Belgium. The FT-Raman spectra were acquired on a Vertex 70-RAM II Bruker FT-Raman spectrometer.

This instrument is equipped with a Nd:YAG laser (yttrium aluminum garnet crystal doped with triply ionized neodymium)with a wavelength of 1064 nm and a maximum power of 1.5 W. The measurement accessory is pre-aligned: only the Z-axis of the scattered light is adjusted to set the sample in the appropriate position regarding the local measurement point. The RAM II spectrometer is equipped with a liquid nitrogen cooled Gedetector.FT-Raman spectra [4000-45 cm -1 ] were collected with a resolution of 1 cm -1 by co-adding 128 scans for each spectrumat room temperature. The OPUS 6.0 software was used for the spectral acquisition, manipulation and transformation.

Thermal measurements

Thermal gravimetric (TGA) and DTG measurements were performed using a NETZSCH STA 449 C (TGA-DSC) (20 °C to 1500 °C)apparatus coupled to a mass spectrometer for analyzing the gas, with a heating rate of 5°C/min in a temperature range of 20°C to 400 °C under Argon. The characterization by DSC was carried out with a Differential calorimetry system (NETZSCH DSC 204 F1) with a speed of heating and cooling of 5°C /min, by performing two heating and cooling cycles to remove traces of water and solvent in a temperature range of (-100°C to 200 °C) under Argon. The experimental procedure is as follows:

-Cooling from 25 °C to -100 °C, leaving the sample at this temperature for 5 minutes -Heating from -100 °C to 120 °C -Cooling from120°C to -100 °C leaving the sample at this temperature for 5 minutes -Heating from -100 °C to 200 °C

Results and discussion

3.1.NMR spectroscopy characterization

In order to identify and confirmed the structures of obtained ILs, the ionic liquids skeletons

[EtOHMIM + ][Cl -] and [EtOHMIM + ][H 2 PO 4 -
] have been characterized structurally using Nuclear magnetic

Experimental vibrational spectroscopy analysis

In order to evaluate the effect of anions on the vibrational spectroscopic properties, FTIR/ATR and Raman spectra of this ionic liquid compared to 1-(hydroxyethyl)-3-methylimidazolium chloride [EtOHMIM + ][Cl - ]were measured and investigated in the wavenumber range 600-4000 cm -1 and from 45 to 3500 cm -1 , ] in the spectral range 1300-600 cm -1 .

3.

3.2.3.Region 1800-1300 cm -1

In this spectral zone (Figure .5) we observe a spectrum with high density for the Cl -anion than for the H 2 PO 4 anion. We notice the mode in 1347 cm -1 for the Cl -anion which is transformed for the H 2 PO 4 -anion to 1360 and 1338 cm -1 modes (Imidazolium ring: C-N, C=N str, CH 2 (N) str, CH 3 (N) CN Str, ν (C-C)) [START_REF] Chaker | Synthesis and characterization of 1-(hydroxyethyl)-3-methylimidazolium sulfate and chloride ionic liquids[END_REF][START_REF] Boumediene | Synthesis, thermal stability, vibrational spectra and conformational studies of novel dicationic metaxylyl linked bis-1-methylimidazolium ionic liquids[END_REF][START_REF] Kausteklis | Effect of cation-anion interactions on the structural and vibrational properties of 1-buthyl-3-methyl imidazolium nitrate ionic liquid[END_REF][START_REF] Drai | Synthesis, experimental and theoretical vibrational studies of 1-methyl and 1, 2-dimethyl, 3-propyl imidazoliumbis (trifluoromethanesulfonyl) imide[END_REF].We also observe in 1338 cm -1 the presence of the stretching mode P=O forH 2 PO 4 -anion [START_REF] Okura | Properties and vibrational spectra of magnesium phosphate glasses for nuclear waste immobilization[END_REF].The spectral zone of the CH 2 rockingof the cation [EtOHMIM + ]1500-1400also seems to be influenced by the choice of the anion in a less important way. In the spectral zone 1800-1500 cm -1 , we observe a shift in frequency of the vibrational mode attributed to the ring C=C and =C-H stretching [START_REF] Chaker | Synthesis and characterization of 1-(hydroxyethyl)-3-methylimidazolium sulfate and chloride ionic liquids[END_REF][START_REF] Moumene | Study of imidazoliumdicationic ionic liquids by Raman and FTIR spectroscopies: The effect of the nature of the anion[END_REF]. The shift is from 1572 cm -1 for the anion Cl -to a shoulder at 1566 cm -1 for H ] in the spectral range 1800-1300 cm -1 .

Region 3500-2400 cm -1

In this spectral region (Figure .6), we observe more peaks for the Cl -anion than for the H 2 PO 4 -anion. In the spectral range 3000-2600 cm -1 , we observe the vibrational mode attributed to the symmetric and antisymmetric (CH 2 ) of the cation [EtOHMIM + ] [START_REF] Chaker | Synthesis and characterization of 1-(hydroxyethyl)-3-methylimidazolium sulfate and chloride ionic liquids[END_REF][START_REF] Kausteklis | Effect of cation-anion interactions on the structural and vibrational properties of 1-buthyl-3-methyl imidazolium nitrate ionic liquid[END_REF]. The C-H ring stretching occurs in the regions 3100-3000 cm -1 which is the characteristic region of the ready identification of the C-H stretching vibrations [START_REF] Guidara | Molecular structure, NLO, MEP, NBO analysis and spectroscopic characterization of 2, 5-dimethylanilinium dihydrogen phosphate with experimental (FT-IR and FT-Raman) techniques and DFT calculations[END_REF].The vibrational mode of the(C-H)is observed in the spectral range: 2993, 3035, 3051, 3097 cm -1 and 3140 cm -1 for the anion Cl -and at 3111 and 3157 cm -1 for the anion H 2 PO 4 -.We notice the mode in 3140 cm -1 for the Cl -anion which is transformed for the H 2 PO 4 -anion to 3111 and 3157 cm -1 modes (H-C-C-H asym str, ν as (C-H), CH 3 (N), = C-H stretching) [START_REF] Chaker | Synthesis and characterization of 1-(hydroxyethyl)-3-methylimidazolium sulfate and chloride ionic liquids[END_REF][START_REF] Boumediene | Synthesis, thermal stability, vibrational spectra and conformational studies of novel dicationic metaxylyl linked bis-1-methylimidazolium ionic liquids[END_REF][START_REF] Kausteklis | Effect of cation-anion interactions on the structural and vibrational properties of 1-buthyl-3-methyl imidazolium nitrate ionic liquid[END_REF][START_REF] Drai | Synthesis, experimental and theoretical vibrational studies of 1-methyl and 1, 2-dimethyl, 3-propyl imidazoliumbis (trifluoromethanesulfonyl) imide[END_REF][START_REF] Guidara | Molecular structure, NLO, MEP, NBO analysis and spectroscopic characterization of 2, 5-dimethylanilinium dihydrogen phosphate with experimental (FT-IR and FT-Raman) techniques and DFT calculations[END_REF].Note that the presence of a shoulder intensity predicted at 3311 cm -1 can be assigned to the corresponding vibrational mode OH (alcohol function of the cation) and possibly OH of H 2 PO 4 -anion [START_REF] Emmanuel | FTIR spectroscopy of woods: A new approach to study the weathering of the carving face of a sculpture[END_REF]. ] in the spectral range 3500-45 cm -1 .

Table 2

Observed FT-Raman bands and their assignment of 1-(hydroxyethyl)-3-methylimidazoliumwith chloride and dihydrogenophosphateanions (vw = very weak, w = weak, m = medium, s = strong, sh = shoulder, str = stretch, d = deformation, bend = bending deformation, ω = wagging, ρ = rocking, τ = torsions = symmetric, as = antisymmetric). ] in the spectral range 1000-45 cm -1 .

Region 1700-1000 cm -1

In this region (Figure. between 1072 and 1194 cm -1 , P-O stretching in 1072 cm -1 and P=O symmetric stretching in 1340 cm -1 [START_REF] Ahmed | Crystal structure, vibrational spectra and theoretical studies of L-histidiniumdihydrogen phosphate-phosphoric acid[END_REF][START_REF] Okura | Properties and vibrational spectra of magnesium phosphate glasses for nuclear waste immobilization[END_REF][START_REF] Frost | Vibrational spectroscopy of the phosphate mineral lazulite-(Mg, Fe) Al2 (PO4) 2•(OH) 2 found in the Minas Gerais, Brazil[END_REF][START_REF] Stutman | Vibrational spectra and structure of the phosphate ion in some calcium phosphates[END_REF].The Raman modes at 1347 cm -1 can be assigned to (N)CH 2 CN stretching vibrations for the Cl - anion which is transformed for the H 2 PO 4 -anion to 1340 and 1356 cm -1 modes [START_REF] Paschoal | Vibrational spectroscopy of ionic liquids[END_REF][START_REF] Heimer | Vibrational spectra of imidazoliumtetrafluoroborate ionic liquids[END_REF][START_REF] Kadari | Comparative study between 1-Propyl-3-methylimidazolium bromide and trimethylenebis-methylimidazolium bromide ionic liquids by FTIR/ATR and FT-RAMAN spectroscopies[END_REF].The bands appearing in the zone 1435-1389cm ] in the spectral range 1700-1000 cm -1 .

Region 3500-2700 cm -1

It should be noted that in this region, the only vibrational mode of the cation is observed(Figure.

Thermal properties

The peak at 117°C that corresponds probably to the melting point of a second morphology of the same sample [START_REF] Haddad | The interplay between molecular structure and dielectric properties in ionic liquids: A comparative study[END_REF][START_REF] Haddad | Bis-methyl imidazoliummethylidenebis (trifluoromethanesulfonyl) imide, crystal structure, thermal and dielectric studies[END_REF]. The temperatures of decomposition and total decomposition are indicated in Table 3.

4.2.Thermal Stability

According to the TGA and DTG curves in (Figure .12.a), the thermal stability of [EtOHMIM + ][Cl -] covers a large domain of temperature between -100°C and 250°C. A mass loss started in two steps between 20 ° C and 400°C. For the first step, a mass loss of 2.30% begins at nearly 67 °C and ends at a temperature of 253°C. This loss corresponding to the release of the H 2 O gas identified from the mass spectrometry curve.

The second step (from 253°C to about 334°C), a loss of 89.46%, corresponding to the release of CH 3 and OH and other fragments identified as gas from the mass spectrometry curve.

Conclusion

In this study, we synthesized a new hydroxyl-functionalized ionic liquid based on 1-(hydroxyethyl)-3methylimidazolium dihydrogenophosphate with a yield of98% in two-steps of synthesis where the anion Cl -

resonance 1 H

 1 and 13 C-NMR spectroscopy, which confirms the absence of any impurities. The resulting spectra are presented in Figures 1-2, in the 1 H-NMR spectra of [EtOHMIM + ][Cl -] and [EtOHMIM + ][H 2 PO 4 -],the signals at δ H = 9.36 ppm and at δ H = 9.21 ppm corresponds to the C2-H of imidazolium ring protons, respectively. For the proton of imidazolium ring: C 4 -H and C 5 -H were displayed at δ H = 7.82 / 7.79 ppm for [EtOHMIM + ][Cl -] and at δ H = 7.75 / 7.71 ppm for [EtOHMIM + ][H 2 PO 4 -]. Signatures of (N-CH 2 -) protons found at δ H =4.25 ppm in [EtOHMIM + ][Cl -], while it's appeared at δ H = 4.23 ppm in [EtOHMIM + ][H 2 characteristic peak for N-methyl protons (N-CH 3 ) appeared at δ H = 3.88/3.86 ppm in [EtOHMIM + ][Cl -] and [EtOHMIM + ][H 2 PO 4 -] respectively. Moreover,the resonance of the methylene protons (-CH 2 -OH)is observed at δ H = 3.69 ppm for both of ILs.As shown in Figures 1a and 2a, the chemical shift O-H groups was observed at 9.08 ppm for [EtOHMIM + ][Cl -] and 6.70ppm for[EtOHMIM + ][H 2 PO 4 -].This behavior related to the impact of electronegativity of each anion and also the charge transfer between 1-(hydroxyéthyl)-3-methylimidazoliumcation and both chloride and dihydrogenophosphate anions who plays a crucial role in the interionic interactions[22-25]. Additionally; two hydrogen's atoms are attached with [PO 4 -] their signatures can only be found in[EtOHMIM + ][H 2 PO 4 -], this is observed in the area of the OH peak in [EtOHMIM + ][H 2 PO 4 -]which shows a greater amplitude than that of OH in [EtOHMIM + ][Cl -]. On the other hand, the 13 C-NMR spectra of [EtOHMIM + ][Cl -] and [EtOHMIM + ][H 2 PO 4 -]show very clearly six signals between δ C = 36.12 and 137.33 ppm. Therefore, these spectral results confirm a high-purity of our investigated ILs.

Figure. 1 :

 1 Figure.1: 1 H-NMR (600 MHz) (a) and 13 CNMR (600 MHz) (b), spectra of [EtOHMIM + ][Cl -].

Figure. 2 .

 2 Figure.2. 1 H-NMR (300 MHz) (a) and 13 CNMR (300 MHz) (b), spectra of [EtOHMIM + ][H 2 PO 4 -].

Figure. 6 . 4 -FT- 7 .

 647 Figure.6. FTIR/ATR spectra of [EtOHMIM + ][Cl -] and [EtOHMIM + ][H 2 PO 4 -]in the spectral range 3500-

  9), both of ILs have almost similar intensities without having a big shift in frequency of the vibrational mode. In the range 1300 -1000 cm -1 , we observe the vibrational mode attributed to C-C of the cation and the vibrations of the H 2 PO 4 anion. Two PO 2 symmetric stretching modes are expected

Figure. 10 . 4 -]

 104 Figure.10. Raman spectra of [EtOHMIM + ][Cl -] and[EtOHMIM + ][H 2 PO 4 -] in the spectral range 3500-2700 cm -1 .

4 -]Figure. 12 . 4 -] are presented in Figure. 13 .

 412413 Figure.12. The mass spectrometric diagram of gas escaped from ionic liquid [EtOHMIM + ][Cl -] and [EtOHMIM + ][H 2 PO 4 -] are presented in Figure.13. The thermal gravimetric parameters extracted from these curves are presented in Table3.

Figure. 11 . 4 -Figure. 12 . 4 -]( 20

 11412420 Figure.11. DSC thermograms of ionic liquids from -100 °C to 200 °C [EtOHMIM + ][Cl -] (a) and [EtOHMIM + ][ H 2 PO 4 -](b)

Figure. 13 .

 13 Figure.13. Mass spectrometric diagram of gas escaped from [EtOHMIM + ][Cl -](20 °C to 400 °C) (a) and [EtOHMIM + ][H 2 PO 4 -]ionic liquids(20 °C to 600 °C) (b).

For

  the TGA and DTG thermograms (Figure12.b) show that this compound is steady below 50°C and undergo change from this temperature in three steps, leaving a reddish residue of 26.19% from the initial mass at 600°C. The first step begins at almost 50°C with a mass loss of 14.81% and ends at a temperature of 200°C corresponding to the release of H 2 O as a gas identified by the mass spectrometry curve. The second step begins at 200°C and ends at approximately360°C with a loss of 37.08% corresponding to the release of H 2 O, CH 3 , OH and other fragments identified as gases from the mass spectrometry curve, and the third step between 360 and 600°C with a loss of 21.92%.

was exchanged by H 2 PO 4 -. 1 H 4 -]

 414 and 13 C-NMR spectroscopy measurements confirm the geometry and purity of the targeted ILs. Also, both compounds were characterized by FTIR/ATR, FT Raman and TGA / DTA/ DSC thermal measurements DSC. The anion seems to play an important role in the thermal stability of the compound as well as on its vibrational behaviour. The results of vibrational spectroscopy and DSC are compared with those obtained on the same intermediate compound [EtOHMIM + ][Cl -]. The final compound i.e. [EtOHMIM + ][H 2 PO shows more interesting vibrational and thermal properties due the type of anion.

2.2.1. 1-(hydroxyethyl)-3-methylimidazoliumchloride [EtOHMIM + ][Cl -] 1 H-NMR (600 MHz, D 2 O) : δ

	= 9.36 (s, 1H, H-2);9.08 (sl, 1H, OH); 7.82 (s, 1H, H-4or H-5); 7.79 (s, 1H,
	H-4or H-5); 4.25 (t, 2H, NCH 2 ); 3.88 (s, 3H, NCH 3 ); 3.69(t, 2H, CH 2 OH) (
	probe at 600 and 300 MHz, respectively. Chemical shifts () are given in ppm and referenced to the internal
	signal solvent D 2 O and DMSO. The spectroscopic data are given below.

C NMR spectra were recorded on a Bruker Biospin Avance III spectrometer equipped with a 5 mm TXI

see Figure.1.a). 13 C-NMR (600 MHz, D 2 O): δ

	= 137.33 (C-2); 123.70 and 123.10(C-4 and C-5); 59.71 (NCH 2 ); 51.94 (CH 2 O); 36.12
	(NCH 3 ) (seeFigure.1.b).
	2.2

.2. 1-(hydroxyethyl)-3-methylimidazolium dihydrogenophosphate [EtOHMIM + ][H 2 PO 4 - ] 1 H-NMR (300 MHz, DMSO): δ

	= 9.21 (s, 1H, H-2); 7.75 (s, 1H, H-4 or H-5); 7.71 (s, 1H, H-4 or H-5);
	6.70 (sl, 1H, OH); 4.23 (t, 2H, NCH 2 ); 3.86 (s, 3H, NCH 3 ); 3.69 (t, 2H, CH 2 OH) (

see Figure.2.a). 13 C- NMR (300 MHz, DMSO): δ

	= 137.23 (C-2); 123.7 and 123.08 (C-4 and C-5); 59.74 (NCH 2 ); 51.96
	(CH 2 O); 36.12 (NCH 3 ) (seeFigure.2.b).

2.1. The comparison between FTIR/ATR spectra of ionic liquids: 1-(hydroxyethyl)-3- methylimidazolium chloride [EtOHMIM + ][Cl -] and 1-(hydroxyethyl)-3-methylimidazolium dihydrogenophosphate [EtOHMIM + ][H 2 PO 4 -].

  FTIR / ATR spectra [4000-600 cm -1 ] of the two ILs are illustrated in Figure.3. The observed IR bands and their detailed assignments are listed in

Table 1 .

 1 We distinguish three well defined spectral regions: 3500-2700, 1700-1300 and 1300-600 cm -1 .

					[EtOHMIM
					[EtOHMIM	+ ][H 2 PO 4	-]
	(a.u)
	intensity
	IR
	4000	3500	3000	2500	2000	1500	1000
				Wavenumber (cm -1 )
	Figure.3. FTIR/ATR spectra of [EtOHMIM + ][Cl -] and[EtOHMIM + ][H 2 PO 4 -]in the spectral range 4000-600
				cm -1 .

+ ][Cl -]

Table 1 :

 1 Observed FTIR/ATR bands and their assignment of 1-(hydroxyethyl)-3-methylimidazolium with chloride and dihydrogenophosphate anions (vw = very weak, w = weak, m = medium, s = strong, sh = shoulder, str = stretch, d = deformation, bend = bending deformation, ω = wagging, ρ = rocking, s = symmetric, as = antisymmetric).For the Cl -anion, this spectral zone (Figure.4) is more intense than for [EtOHMIM + ][H 2PO 4

	[EtOHMIM + ]			Assignment			Refs
	[Cl -]	[ H 2 PO 4 -]
	621(s)	619(w)	ω(N-H),νC=C, CH 3 (N) CN str, τCH(imidazolium)		[21,26,27,28]
	652(s)	648(w)	ω(N-H), CH 2 (N) str, CH 3 (N) CN str, νN-CH 3 ,ɤ(N-C)		[21,26,29,30]
	687 (s)		ω(C-H), δCC				[21,28,31]
	706(m)	702(vw)	CH 2 (N), CH 3 (N)CN str				[18,21,22]
		746 (w)	ω(C-H), ring HCCH sym bend, CH 3 (N) bend, CH 2 (N) bend	[21,25,26,27]
	797(s)		ring HCCH asym bend, CS str			[21,23,24]
		831(sh)	ring HCCH asym bend, NC(H)N bend, ɤ(C-H)		[29,32]
	870 (s)	870 (w)	ρ as (CH 2 ), NC(H) N bend, P-OH str, ν 1 (PO 4 )		[21,26,32,33]
	943 (vw)		ρ as (CH 2 )				[21,34,35]
		974 (s)	(P-O) stretch, ν 3 (PO 4 )				[33,36]
	1037 (m)		ring sym str, CH 3 (N) str, CH 2 (N) str, νC-C		[21,37]
	1063 (sh)	1060 (w)	Ring ip asym str, CC str, CH 3 (N) twist, SNS asym str, ν (C-O),	[21,26,33]
			P-O str, ν 3 (PO 4 )
	1074 (s)		Ring ip asym str, CC str, CH 3 (N) twist, SNS asym str		[21,26,38]
	1100 (vw)		CC str, ν (C-C)				[21,28]
	1120 (vw)		δCH, ring HCCH sym bend, CC str, ρ(CH 3 )		[21,26,29]
	1175 (m)	1163 (w)	ring asym str CH 2 (N), CH 3 (N) CN str, CCstr, νN-C		[26,28,29]
	1198 (m)		ring s CH 2 (N), CH 3 (N)CN str, ν(C-C), ω(C-H, τ(C-H)		[21,26,39]
	1254 (w)		ρCH(imidazolium)				[30]
		1338 (vw)	Imidazolium ring: C-N, C=N str, CC str, CH 2 (N) str, CH 3 (N), ν	[21,26,36]
			(C-C), P=O str
	1347 (m)	1360 (vw)	Imidazolium ring: C-N, C=N str, CH 2 (N) str, CH 3 (N) CN str, ν	[21,26,29,40]
			(C-C), ω(C-H 2 )
	1371 (w)		δ(CH), δ s (CH 3 )				[21]
	1387 (sh)	1387 (vw)	ρ(CH 2 ), ρ(CH), δ(CH 2 ) [op], ω(CH), ring ip asym str, CH 2 (N)	[21,26,28]
			bend, CC str, CH 2 (N) str, CH 3 (N) CN str, ρ(N-H)
	1425 (m)	1427 (vw)	Imidazoliumring:C-N,	C=N	strband,δs(CH 2 ),	C-H	[21,26,28]
			deformation,ρ(N-H)
	1447 (m)	1450 (w)	δ(CH 2 ), CCH HCH as bend,ring ip asym str, CH 3 (N)	[21,26,29]
			str,δ a (CH 3 )
	1464 (sh)		δ a (CH 3 ), δ(CH 2 ), CH 3 (N) HCH sym bend, CH 3 (N) CN str		[21,29,40]
	1479 (w)		δ(CH 2 ), CCH HCH as bend			[21,26]
	1572 (s)	1566 (sh)	Imidazolium ring ν(N=C), ring ip sym/asym str, CH 2 (N),	[21,26,28]
			CH 3 (N) CN str
		1630 (sh)	ν (C=C)				[25]
	1687 (w)		ν (C=C), ring C=C, N=C-N str			[21,25]
	1751 (w)		overtone =C-H str				[21]
		2316 (vw)
	2486 (vw)		ν (C=C)				[21]
	2600 (vw)		ν s (CH 2 )				[21]
	2673 (vw)		ν s (CH 2 )				[21]

-

]. Conversely we notice new strong intense peak in 974 cm -1 which is assigned to the symmetric stretching ν 3 mode of dihydrogenophosphate anion not available for [EtOHMIM + ][Cl -].The presence of this new intense is assigned to (P-O) stretching mode

[START_REF] Ahmed | Crystal structure, vibrational spectra and theoretical studies of L-histidiniumdihydrogen phosphate-phosphoric acid[END_REF][START_REF] Okura | Properties and vibrational spectra of magnesium phosphate glasses for nuclear waste immobilization[END_REF]

. The modes at 619, 648 and 706 cm -1 are assigned to (N-H) wagging and CH 3 (N)CN stretching. The band due to (CH 2 ) rocking antisymmetric of the cation [EtOHMIM + ] and NC(H) N bending occurs at 870 cm -1 for the two ILs and is of weak to strong intensity. Figure.4. FTIR/ATR spectra of [EtOHMIM + ][Cl -] and [EtOHMIM + ][H 2 PO 4 -

Table 2 .

 2 We distinguish three well defined spectral regions: 3500-2700, 1700-1000 and 1000-45 cm -1 .

					[EtOHMIM	+ ][Cl	-]
					[EtOHMIM	+ ][H 2 PO 4	-]
	(a.u)
	intensity
	IR
	3400	3200	3000	2800	2600	2400
			Wavenumber (cm	-1 )

Figure.7. Raman spectra of [EtOHMIM + ][Cl -] and [EtOHMIM + ][H 2 PO 4 -

  Raman spectra of [EtOHMIM + ][Cl -] and [EtOHMIM + ][H 2 PO 4 -

			[EtOHMIM	+ ][Cl	-]
	(a.u)
	Raman intensity		[EtOHMIM	+ ][H 2 PO 4	-]
	1000	900	800	700	600	500	400	300	200	100
						Wavenumber (cm -1 )
	Figure.9.
			-1 assigned to imidazolium ring: C-N, C=N stretching banding. For
	[EtOHMIM + ][Cl -] we observe four modes in 1435, 1445, 1466 and 1568 cm -1 assigned to NCH 3 CN
	stretching while for [EtOHMIM + ][H 2 PO 4	-]this mode was observed at 1453 and 1567 cm -1 .

Table 3 . 4.1.DSC Thermogram

 3

	Concerning [EtOHMIM + ][Cl -] we can see from Figure.11.aand Table 3that while heating from lower
	temperature (-100°) we observe a glass transitions Tg = -58 °C, then an exothermic peak onset at -36.2°C
	with an enthalpy of 24.21 J/g that corresponds to the crystallization of the sample and then an endothermic
	peak onset at 64 °C in the heating phase corresponding to the melting point of [EtOHMIM + ][Cl -] with an
	enthalpy of 79.44 J/g.
	In the DSC curve (Figure.11.b), [EtOHMIM + ][H 2 PO 4	-] has not showed a glass transition on heating scan,
	then an exothermic peak onset at 77°C.An endothermic peak onset at 84 °C was observed in the heating
	phase corresponding to the melting point of [EtOHMIM + ][H 2 PO 4	-].We observe also another endothermic

+ ][Cl -]

  Table 3Thermal properties of [EtOHMIM + ][Cl -] and [EtOHMIM + ][H 2 PO 4

							-].
			Tg(°C) Tc (°C) Tf (°C) Td(°C)	Td T (°C)
	Ionic Liquids
	[EtOHMIM + ][Cl -]		-58	-36.2	64	250	317
	[EtOHMIM + ][H 2 PO 4	-]	-	77	84	264	365

Acknowledgment

The authors thank the ATRST-DGRSDT (Algeria) for the financial support and the Walloon Agricultural Research Center (CRA-W), who participated to FT-RAMAN and FTIR/ATR measurements.

873(w) 899(vw) 942(w) 1027(m) 1065(w) 1078(w) 1121(w) 1194(w) 1251(w) 1303(w) 1347(m) 1389(w) 1420(m) 1435(w) 1445(w) 1466(w) 1480(w) 1568(w) 2829(w) 2874(w) 2930(w) 2957(sh) 2966(m) 3003(w) 3037(sh) 3054(w) 3104(w) 3143(vw) 875(sh) 901(m) 945(vw) 1023(m) 1072(vw) 1110(vw) 1194(vw) 1257(vw) 1340(w) 1356(vw) 1389(w) 1418(m) 1453(w) 1567(vw) 2835(vw) 2893(vw) 2964(m)

Region 1000-45 cm -1

In this region (Figure .8), we observe the characteristic modes of H 2 PO 4 -anion. The bands appearing in the zone 200 -50 cm -1 assigned to intermolecular vibrations [START_REF] Paschoal | Vibrational spectroscopy of ionic liquids[END_REF][START_REF] Haddad | Effects of C (2) methylation on thermal behavior and interionic interactions in imidazolium-based ionic liquids with highly symmetric anions[END_REF]. The modes between 230 and 655 cm -1 are assigned to NCH 3 for both of ILs [START_REF] Paschoal | Vibrational spectroscopy of ionic liquids[END_REF][START_REF] Haddad | Para-xylyl linked bis-imidazolium ionic liquids: A study of the conformers of the cation and of the anion-cation hydrogen bonding[END_REF][START_REF] Boumediene | Synthesis, thermal stability, vibrational spectra and conformational studies of novel dicationic metaxylyl linked bis-1-methylimidazolium ionic liquids[END_REF][START_REF] Heimer | Vibrational spectra of imidazoliumtetrafluoroborate ionic liquids[END_REF][START_REF] Kadari | Comparative study between 1-Propyl-3-methylimidazolium bromide and trimethylenebis-methylimidazolium bromide ionic liquids by FTIR/ATR and FT-RAMAN spectroscopies[END_REF] . The symmetric bending modeν 2 of dihydrogenophosphate anion is observed at 417 cm -1 .The bending vibration of the P-O group gives a very weak to weak band in the region 600-400 cm -1 for the H 2 PO 4 -anion [START_REF] Ahmed | Crystal structure, vibrational spectra and theoretical studies of L-histidiniumdihydrogen phosphate-phosphoric acid[END_REF]. In addition, we notice the presence of the following vibrational modes: 705, 875, 901 and 945cm -1 assigned to PO 2 symmetricstretching, POH symmetric and antisymmetric stretching respectively.