# Preservative Translations between Logical Systems

Yuming Shen, Yue Ma, Cungen Cao, Yuefei Sui, Ju Wang

► To cite this version:

Yuming Shen, Yue Ma, Cungen Cao, Yuefei Sui, Ju Wang. Preservative Translations between Logical Systems. 6th IFIP TC 12 International Conference on Intelligent Information Processing (IIP), Oct 2010, Manchester, United Kingdom. pp.55-63, 10.1007/978-3-642-16327-2_10. hal-01060356

HAL Id: hal-01060356

https://inria.hal.science/hal-01060356

Submitted on 5 Dec 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Preservative translations between logical systems

Yuming Shen¹,², Yue Ma¹,², Cungen Cao¹, Yuefei Sui¹, and Ju Wang³

¹ Key Laboratory of Intelligent Information Processing, Institute of Computing Technology, Chinese Academy of Sciences 100190, China, shenyuming@ict.ac.cn,

² Graduate University of Chinese Academy of Sciences, 100049, China,

³ School of Computer Science and Information Engineering, Guangxi Normal University 541004, China

**Abstract.** This paper investigates a subclass of translations between logical systems, called the preservative translations, which preserve the satisfiability and the unsatisfiability of formulas. The definition of preservative translation is given and connections between the preservative translation and other definitions of translations in the literature are discussed. Some properties of logical systems, such as the compactness and the decidability, which are characterized by the existence of preservative translations between logical systems are also studied.

**Keywords:** Translation, Faithfulness, Fullness, Preservative translation

# 1 Introduction

The method of studying relations between logical systems by analyzing translations between them was originally introduced by Kolmogorov [7]. Translating or encoding one logical system (the *source logical system*) into another logical system (the *target logical system*) gives us a powerful tool for understanding logical systems from a logical, algorithmical, and computational point of view. Translating a source logical system into a target logical system have several advantages, and some of these are given below [10]:

* To grasp the expressive power, both of the source logical system and of the target logical system.

* To export any proof procedures and tools that we may have for the target logical system to the source logical system.

* To grasp the computational costs of various reasoning tasks, again both for the source logical system and for the target logical system.

* To combine two logical systems, sometimes the most natural solution is to translate both into the same target logical system, and to work inside the target logical system.

Many translations found in the literature (see, e.g., [6, 8, 12]) satisfy the following logical properties:
* Soundness: for every formula $\varphi$ of the source logical system, if $\varphi$ is satisfiable then $\varphi$ is translated to a satisfiable formula of the target logical system;

* Completeness: for every formula $\varphi$ of the source logical system, if the translated formula for $\varphi$ is satisfiable, then $\varphi$ is satisfiable.

By the definitions of soundness and completeness, we have that the satisfiability of formulas is preserved. However, translating in a satisfiability-preserving way does not immediately lead to the preservation of the unsatisfiability, if the translation between models is taken into account and the class of models of a source logical system is translated to a proper subclass of the class of models of a target logical system. For example, Fara and Williamson[3] showed that the translations from first-order modal logic into the counterpart theory given by Lewis[9], Forbes[5] and Ramachandran[14] may translate an unsatisfiable formula to a satisfiable formula.

Inspired by the observation, in [13], we give the following logical properties to describe a translation $\sigma$.

* Faithfulness: for every formula $\varphi$ of a source logical system, $\varphi$ is satisfied in a model $\mathfrak{M}$ and a valuation $v$ of the source logical system if and only if $\sigma(\varphi)$ is satisfied in the translated model $\sigma(\mathfrak{M})$ and valuation $\sigma(v)$, that is,

$$ (\mathfrak{M}, v) \models \varphi \text{ if and only if } (\sigma(\mathfrak{M}), \sigma(v)) \models \sigma(\varphi). $$

* Fullness: for any formula $\varphi$ of a source logical system, any model $\mathfrak{M}'$ and any valuation $v'$ of a target logical system, if $(\mathfrak{M}', v') \models \sigma(\varphi)$, then there exists a model $\mathfrak{M}$ and a valuation $v$ of the source logical system such that $(\mathfrak{M}, v) \models \varphi$ and $\sigma(\mathfrak{M}) = \mathfrak{M}', \sigma(v) = v'$.

The faithfulness is the soundness and completeness of a translation. The fullness says that every model and every valuation which satisfies $\sigma(\varphi)$ has a corresponding model and valuation in the source logical system. By the definitions of faithfulness and fullness, we have that the satisfiability and unsatisfiability of formulas are both preserved.

In this paper, a translation is called a preservative translation if it is faithful and full. The aim of this paper is to investigate a subclass of translations, the preservative translations, which preserve the satisfiability and the unsatisfiability.

The paper is organized as follows. In section 2, we give the definition of preservative translation, and show that the satisfiability and unsatisfiability of formulas are preserved under the preservative translations. Two translation examples are also given in the section, the first example is the standard relational translation from propositional modal logic into first-order logic, the second is the identity translation from intuitionistic propositional logic into classical propositional logic. In section 3, we discuss connections between the definition of preservative translation and several definitions of translation given in the literature. In section 4, we study some properties of logical systems, such as the decidability and the compactness, which are characterized by the existence of preservative translations between them, and section 5 is the conclusion.
## 2 The concept of preservative translation

In this section, we firstly present the definitions of logical system and translation between logical systems introduced in [1, 4], and then give the definition of preservative translation. Next, we show that the satisfiability and the unsatisfiability of formulas are preserved under the preservative translations. Finally, we give the following examples: the standard relational translation from modal propositional logic(PML) into first-order logic(FOL) and the identity translation from intuitionistic propositional logic (IPL) into classical propositional logic (CPL). We show that the former is a preservative translation, whereas the latter is not.

In [1, 4], logical systems are characterized as sets with consequence relation and translation between logical systems as consequence relation preserving maps.

**Definition 1.** A logical system $\mathcal{L}$ is a pair $(\mathcal{L}, C)$ such that $\mathcal{L}$ is a formal language and $C$ is a consequence operator in the free algebra $Form(A)$ of the formulas of $\mathcal{L}$, that is, $C : 2^{Form(A)} \to 2^{Form(A)}$ is a function that satisfies, for $X, Y \subseteq Form(A)$, the following conditions:

(i) $X \subseteq C(X)$;

(ii) If $X \subseteq Y$, then $C(X) \subseteq C(Y)$;

(iii) $C(C(X)) \subseteq C(X)$.

It is clear that the non-monotonic logics do not match the above definition.

**Definition 2.** A translation from a logical system $\mathcal{L}$ into a logical system $\mathcal{L}'$ is a mapping $\sigma : \mathcal{L} \to \mathcal{L}'$ such that $\sigma(C_{\mathcal{L}}(X)) \subseteq C_{\mathcal{L}'}(\sigma(X))$ for any $X \subseteq Form(\mathcal{L})$.

By the definition 2, it clear that if the syntactical consequence relations $\vdash_{\mathcal{L}}$ and $\vdash_{\mathcal{L}'}$ are associated with $C_{\mathcal{L}}$ and $C_{\mathcal{L}'}$, respectively, then a function $\sigma : \mathcal{L} \to \mathcal{L}'$ is a translation if and only if for every $\Phi \subseteq Form(\mathcal{L})$, $\varphi \in Form(\mathcal{L})$, if $\Phi \vdash_{\mathcal{L}} \varphi$, then $\sigma(\Phi) \vdash_{\mathcal{L}'} \sigma(\varphi)$.

In the following discussion, we suppose that a translation $\sigma$ is extended by translating every model and every valuation of $\mathcal{L}$ to a model and a valuation of $\mathcal{L}'$, respectively. Then, we give the definition of preservative translation as follows:

**Definition 3.** Let $\mathcal{L}$ and $\mathcal{L}'$ be logical systems. A translation $\sigma$ is called a preservative translation from $\mathcal{L}$ into $\mathcal{L}'$ if the following conditions holds:

(1) For any formula $\varphi$, any model $\mathfrak{M}$ and any valuation $v$ of $\mathcal{L}$,

$$ (\mathfrak{M}, v) \models_{\mathcal{L}} \varphi \text{ if and only if } (\sigma(\mathfrak{M}), \sigma(v)) \models_{\mathcal{L}'} \sigma(\varphi). $$

(2) For any formula $\varphi$ of $\mathcal{L}$, any model $\mathfrak{M}'$ and any valuation $v'$ of $\mathcal{L}'$, if $(\mathfrak{M}', v') \models_{\mathcal{L}'} \sigma(\varphi)$, then there exists a model $\mathfrak{M}$ and a valuation $v$ of $\mathcal{L}$ such that $(\mathfrak{M}, v) \models_{\mathcal{L}} \varphi$ and $\sigma(\mathfrak{M}) = \mathfrak{M}', \sigma(v) = v'$.
**Remark.** In some cases, a logical system does not contain valuations, for example, propositional logic and propositional modal logic. If both $\mathcal{L}$ and $\mathcal{L}'$ do not contain valuations, then there is no corresponding relation between valuations of $\mathcal{L}$ and valuations of $\mathcal{L}'$, for example, the translation between classical propositional logic and intuitionistic propositional logic. If one of them contains valuations, then the mapping $\sigma$ may be considered as a partial function, for example, the standard relational translation from propositional modal logic into first-order logic.

□

By the definition of preservative translation, we have that the satisfiability and unsatisfiability of formulas are preserved.

**Proposition 1.** If $\sigma$ is a preservative translation from $\mathcal{L}$ into $\mathcal{L}'$, then for any formula $\varphi$ of $\mathcal{L}$, $\varphi$ is a satisfiable formula if and only if $\sigma(\varphi)$ is a satisfiable formula.

□

**Proposition 2.** If $\sigma$ is a preservative translation from $\mathcal{L}$ into $\mathcal{L}'$, then for any formula $\varphi$ of $\mathcal{L}$, $\varphi$ is an unsatisfiable formula if and only if $\sigma(\varphi)$ is an unsatisfiable formula.

*Proof.* For any formula $\varphi$, if $\varphi$ is an unsatisfiable formula but $\sigma(\varphi)$ is a satisfiable formula, then there exists a model $\mathfrak{M}'$ and valuation $v'$ of $\mathcal{L}'$ such that $(\mathfrak{M}', v') \models_{\mathcal{L}'} \sigma(\varphi)$. By the definition of preservative translation, we have that there exists a model $\mathfrak{M}$ and valuation $v$ such that $(\mathfrak{M}, v) \models_{\mathcal{L}} \varphi$. Contradicting the fact $\varphi$ is an unsatisfiable formula. On the other hand, if $\sigma(\varphi)$ is an unsatisfiable formula but $\varphi$ is a satisfiable formula, then there exists a model $\mathfrak{M}$ and valuation $v$ of $\mathcal{L}$ such that $(\mathfrak{M}, v) \models_{\mathcal{L}} \varphi$. By the definition of preservative translation, we have that $(\sigma(\mathfrak{M}), \sigma(v)) \models_{\mathcal{L}'} \sigma(\varphi)$. Contradicting the fact $\sigma(\varphi)$ is unsatisfiable.

□

The following example shows that the standard relational translation from **PML** into **FOL** is a preservative translation.

*Example 1.* Suppose that **PML** and **FOL** both are contain the connectives $\neg$, $\rightarrow$ and the vocabulary of **FOL** consists of a binary predicate **R** to represent the accessibility relation and unary predicate symbols to represent proposition letters, the standard relational translation $\sigma$ is given as follows:

$$ \sigma(\varphi, w) = \begin{cases} p(w) & \text{if } \varphi = p \\ \neg\sigma(\psi, w) & \text{if } \varphi = \neg\psi \\ \sigma(\psi, w) \rightarrow \sigma(\theta, w) & \text{if } \varphi = \psi \rightarrow \theta \\ \forall w'(\mathbf{R}(w, w') \rightarrow \sigma(\psi, w')) & \text{if } \varphi = \Box\psi. \end{cases} $$

On the semantic side, for any **PML** model $\mathfrak{M} = (W, R, \mathfrak{J})$, we construct a **FOL** model $\sigma(\mathfrak{M}) = \mathfrak{M}' = (U', \mathfrak{J}')$ as follows:

$\bullet U' = W;$
• $\mathfrak{J}'(\mathbf{R}) = R$;

• $\mathfrak{J}'(p) = \{w \in W : \mathfrak{J}(p, w) = 1\}$;

• $v'(w) = w$.

By induction on $\varphi$, we have that for any formula $\varphi$ and any model $\mathfrak{M}$ of PML,

$$ (\mathfrak{M}, w) \models_{\text{PML}} \varphi \text{ if and only if } (\sigma(\mathfrak{M}), v') \models_{\text{FOL}} \sigma(\varphi, w). $$

For any FOL model $\mathfrak{M}' = (U', \mathfrak{J}')$, we construct a corresponding PML model $\mathfrak{M} = (W, R, \mathfrak{J})$ as follows:

• $W = U'$;

• $R = \mathfrak{J}'(\mathbf{R})$;

• $\mathfrak{J}(p, w) = 1$ if and only if $w \in \mathfrak{J}'(p)$.

By induction on $\varphi$, we have that for any formula $\varphi$ of PML, and any model $\mathfrak{M}'$ and valuation $v'$ of FOL, if $(\mathfrak{M}', v') \models_{\text{FOL}} \sigma(\varphi, w)$ then there exists a model $\mathfrak{M}$ of PML such that $(\mathfrak{M}, w) \models_{\text{PML}} \varphi$, $\sigma(\mathfrak{M}) = \mathfrak{M}'$. By the definition of preservative translation, we have that the standard relational translation is preservative.

The next example is the identity translation from IPL into CPL. we show that the translation is not preservative, since the law of excluded middle holds for CPL, not for IPL.

*Example 2.* Suppose that IPL and CPL both are contain the connectives $\neg$, $\wedge$, $\vee$, $\rightarrow$. The identity function $\sigma$ from IPL into CPL is a translation. Since the formula $p \wedge \neg p$ is a valid formula in CPL but it is invalid in IPL, the identity translation $\sigma$ is not a preservative translation.

# 3 Connections with several definitions of translations

In this section, we present several definitions of translations in the literature and analyze connections between the definition of preservative translation and them.

## 3.1 Translations for Epstein and Krajewski

In [2], Epstein and krajewski present a validity mapping of a propositional logic $\mathcal{L}$ into a propositional logic $\mathcal{L}'$ as a map $\sigma$ from the language of $\mathcal{L}$ into the language of $\mathcal{L}'$ such that, for every formula $\varphi$,

$$ \models_{\mathcal{L}} \varphi \text{ if and only if } \models_{\mathcal{L}'} \sigma(\varphi). $$

A translation is a validity mapping $\sigma$ such that, for every set $\Phi$ of formulas and every formula $\varphi$ of $\mathcal{L}$,

$$ \Phi \models_{\mathcal{L}} \varphi \text{ if and only if } \sigma(\Phi) \models_{\mathcal{L}'} \sigma(\varphi). $$

The following proposition show that if $\sigma$ is a preservative translation and satisfies the following conditions:
(1) $\sigma$ is injective at models level, that is, for any models $\mathfrak{M}_1, \mathfrak{M}_2$ of $\mathcal{L}$, if $\mathfrak{M}_1 \neq \mathfrak{M}_2$, then $\sigma(\mathfrak{M}_1) \neq \sigma(\mathfrak{M}_2)$.

(2) $\sigma$ is injective at valuations level, that is, for any given model $\mathfrak{M}$ of $\mathcal{L}$ and any valuations $v_1, v_2$ in $\mathfrak{M}$, if $v_1 \neq v_2$, then $\sigma(v_1) \neq \sigma(v_2)$.

Then Epsten's definition of translation coincides with our definition of preservative translation.

**Proposition 3.** Let $\mathcal{L}$ and $\mathcal{L}'$ be logical systems. If $\sigma$ is a preservative translation from $\mathcal{L}$ into $\mathcal{L}'$ and satisfies the above conditions (1) and (2), then for every formula set $\Phi$ and every formula $\varphi$ of $\mathcal{L}$, $\Phi \models_{\mathcal{L}} \varphi$ if and only if $\sigma(\Phi) \models_{\mathcal{L}'} \sigma(\varphi)$.

*Proof.* Suppose that $\Phi \models_{\mathcal{L}} \varphi$. For any model $\mathfrak{M}'$ and any valuation $v'$ of $\mathcal{L}'$, if $(\mathfrak{M}', v') \models_{\mathcal{L}'} \sigma(\Phi)$, then by $\sigma$ is a preservative translation, there exists a model $\mathfrak{M}$ and valuation $v$ of $\mathcal{L}$ such that $(\mathfrak{M}, v) \models_{\mathcal{L}} \Phi$, $\sigma(\mathfrak{M}) = \mathfrak{M}', \sigma(v) = v'$. Since $\Phi \models_{\mathcal{L}} \varphi$, we have that $(\mathfrak{M}, v) \models_{\mathcal{L}} \varphi$. By $\sigma$ is a preservative translation, we have that $(\mathfrak{M}', v') \models_{\mathcal{L}'} \sigma(\varphi)$, i.e., $\sigma(\Phi) \models_{\mathcal{L}'} \sigma(\varphi)$.

On the other hand, Suppose that $\sigma(\Phi) \models_{\mathcal{L}'} \sigma(\varphi)$. For any model $\mathfrak{M}$ and any valuation $v$ of $\mathcal{L}$, if $(\mathfrak{M}, v) \models_{\mathcal{L}} \Phi$, then by $\sigma$ is a preservative translation, we have that $(\sigma(\mathfrak{M}), \sigma(v)) \models_{\mathcal{L}'} \sigma(\Phi)$. Since $\sigma(\Phi) \models_{\mathcal{L}'} \sigma(\varphi)$, we have that $(\sigma(\mathfrak{M}), \sigma(v)) \models_{\mathcal{L}'} \sigma(\varphi)$. Since $\sigma$ is a preservative translation and satisfies the conditions (1) and (2), we get that $(\mathfrak{M}, v) \models_{\mathcal{L}} \varphi$, i.e., $\Phi \models_{\mathcal{L}} \varphi$. $\square$

## 3.2 Translations for Prawitz and Malmnäs

In [11], Prawitz and Malmnäs define that a translation from $\mathcal{L}$ into $\mathcal{L}'$ via a function $\sigma$ such that, for every formula of $\varphi$ of $\mathcal{L}$,

$$ \vdash_{\mathcal{L}} \varphi \text{ if and only if } \vdash_{\mathcal{L}'} \sigma(\varphi). $$

The following proposition shows that if $\mathcal{L}$ and $\mathcal{L}'$ are logical systems whose languages have the negation $\neg$ and $\sigma$ is a preservative translation which satisfies that for any formula $\varphi$ of $\mathcal{L}$, $\sigma(\neg\varphi) = \neg\sigma(\varphi)$, then the definition of translation given by Prawitz and Malmnäs coincides with our definition of preservative translation.

**Proposition 4.** Let $\mathcal{L}$ and $\mathcal{L}'$ be logical systems whose languages have the negation $\neg$ and $\sigma$ is a preservative translation which satisfies that for any formula $\varphi$ of $\mathcal{L}$, $\sigma(\neg\varphi) = \neg\sigma(\varphi)$, then

$$ \vdash_{\mathcal{L}} \varphi \text{ if and only if } \vdash_{\mathcal{L}'} \sigma(\varphi). $$

*Proof.* For any formula $\varphi$ of $\mathcal{L}$, if $\vdash_{\varphi} \varphi$ but $\vdash_{\mathcal{L}'} \sigma(\varphi)$, then there exists a model $\mathfrak{M}'$ and a valuation $v'$ of $\mathcal{L}'$ such that $(\mathfrak{M}', v') \models_{\mathcal{L}'} \neg\sigma(\varphi)$. Since $\sigma(\neg\sigma) = \neg\sigma(\varphi)$ and $\sigma$ is preservative, there exists a model $\mathfrak{M}$ and a valuation $v$ of $\mathcal{L}$ such that $(\mathfrak{M}, v) \models_{\mathcal{L}} \neg\varphi$. Contradicting the fact $\vdash_{\mathcal{L}} \varphi$. On the other hand, if $\vdash_{\mathcal{L}'} \sigma(\varphi)$ but $\vdash_{\mathcal{L}'} \varphi$, then there exists a model $\mathfrak{M}$ and a valuation $v$ such that $(\mathfrak{M}, v) \models_{\mathcal{L}'} \neg\varphi$.
By $\sigma(\neg\varphi) = \neg\sigma(\varphi)$ and $\sigma$ is preservative, we have that $(\sigma(\mathfrak{M}), \sigma(v)) \models_{\mathcal{L}'} \neg\sigma(\varphi)$. Contradicting the fact $\vdash_{\mathcal{L}'} \sigma(\varphi)$.

□

Feitosa and Ottaviano[4] define that a conservative mapping from $\mathcal{L} = (A, C)$ into $\mathcal{L}' = (A', C')$ as a function $\sigma$ such that, for every $x \in A$,

$$x \in C(\emptyset) \text{ if and only if } \sigma(x) \in C'(\emptyset),$$

where $A$ is a set and $C$ is a consequence operator. If we restrict $A, A'$ to formal languages and the syntactical consequence relations $\vdash_{\mathcal{L}}$ and $\vdash_{\mathcal{L}'}$ are associated with $C$ and $C'$, respectively, then by the proposition 4, we have that the conservative mapping coincides with our definition of preservative translation.

# 4 General properties characterized by the preservative translations

In this section, we give some general properties of logical logics, such as the compactness and the decidability, which are characterized by the existence of preservative translations between logical logics.

The compactness theorem of a logical system $\mathcal{L}$ is that any formulas set $\Phi$ of $\mathcal{L}$, if every finite subset of $\Phi$ is satisfiable then $\Phi$ is satisfiable. The following proposition shows that if there is a preservative translation from $\mathcal{L}$ into $\mathcal{L}'$ then the compactness theorem holds for $\mathcal{L}'$ implies that it holds for $\mathcal{L}$.

**Proposition 5.** Let $\sigma$ be a preservative translation from $\mathcal{L}$ into $\mathcal{L}'$. If the compactness theorem holds for $\mathcal{L}'$, then the compactness theorem holds for $\mathcal{L}$.

*Proof.* For any given formulas set $\Phi$ of $\mathcal{L}$ and for every finite $\Psi_0$ of $\sigma(\Phi)$, there exists a finite subset $\Phi_0$ of $\Phi$ such that $\sigma(\Phi_0) = \Psi_0$. By $\sigma$ is preservative, we have that if $\Phi_0$ is a satisfiable then $\Psi_0$ is satisfiable. As the compactness theorem holds for $\mathcal{L}'$, we have that $\sigma(\Phi)$ is satisfiable, and by $\sigma$ is preservative we have that $\Phi$ is satisfiable, i.e., the compactness theorem holds for $\mathcal{L}'$.

□

Since the compactness theorem holds for first-order logic, not for second-order logic, we have the following corollary.

**Corollary 1.** There is no preservative translation from second-order logic into first-order logic.

□

The decidability of a logical system $\mathcal{L}$ is that there exists an effective procedure that, given any formula $\varphi$, will decide whether or not it is a theorem of $\mathcal{L}$. Let $\mathcal{L}, \mathcal{L}'$ be logics whose languages have negation $\neg$, the following proposition shows that if there is a preservative translation $\sigma$ from $\mathcal{L}$ into $\mathcal{L}'$ and $\sigma$ also satisfies the following conditions:

* $\sigma$ is a recursive function at formulas level, that is, for any formula $\varphi$ of $\mathcal{L}$, we can determine $\sigma(\varphi)$ is a formula of $\mathcal{L}'$.
• $\sigma$ is distributive with negation, that is, for any formula $\varphi$ of $\mathcal{L}$, $\sigma(\neg\varphi) = \neg\sigma(\varphi)$.

Then the decidability of $\mathcal{L}'$ implies that $\mathcal{L}$ is decidable.

**Proposition 6.** Let $\mathcal{L}, \mathcal{L}'$ be logics whose languages have negation $\neg$. If there is a preservative translation from $\mathcal{L}$ into a decidable $\mathcal{L}'$ and $\sigma$ is recursive at formulas level and distributive with negation, then $\mathcal{L}$ is decidable.

*Proof.* For any formula $\varphi$ of $\mathcal{L}$, as $\sigma$ is recursive at formulas level, we can determine $\sigma(\varphi)$. Since $\mathcal{L}'$ is decidable, it is possible to verify that $\sigma(\varphi)$ is or is not a theorem of $\mathcal{L}'$. Hence, if $\sigma(\varphi)$ is a theorem of $\mathcal{L}'$ but $\varphi$ is not a theorem of $\mathcal{L}$ then there exists a model $\mathfrak{M}$ and a valuation $v$ of $\mathcal{L}$ such that $(\mathfrak{M}, v) \models_{\mathcal{L}} \neg\varphi$. By $\sigma$ is preservative and distributive with negation, we have that $(\sigma(\mathfrak{M}), \sigma(v)) \models_{\mathcal{L}'} \neg\sigma(\varphi)$. Contradicting the fact $\sigma(\varphi)$ is a theorem of $\mathcal{L}'$, i.e., $\varphi$ is a theorem of $\mathcal{L}$. If $\sigma(\varphi)$ is not a theorem of $\mathcal{L}'$, then there exists a model $\mathfrak{M}'$ and a valuation $v$ such that $(\mathfrak{M}', v') \models_{\mathcal{L}'} \neg\sigma(\varphi)$. By $\sigma$ is preservative and distributive with negation, there exists a model $\mathfrak{M}$ and a valuation $v$ such that $(\mathfrak{M}, v) \models_{\mathcal{L}} \neg\varphi$, i.e., $\varphi$ is not a theorem of $\mathcal{L}$.

Since propositional modal logics K, D, T, S4, S5 are decidable but first-order logic is not, we have the following corollary.

**Corollary 2.** There is no recursive, distributive and preservative translation from first-order logic into propositional modal logics K, D, T, S4, S5.

# 5 Conclusion

In this paper, we investigate a subclass of translations, the preservative translations, which preserve the satisfiability and unsatisfiability of formulas. We give the definition of preservative translation, and show that the satisfiability and unsatisfiability of formulas are preserved under such translations. Also, we show that the standard relational translation from propositional modal logic into first-order logic is a preservative translation and the identity translation from intuitionistic propositional logic into classical propositional logic is not. Connections between our definition of preservative translations and other definitions of translations in the literature are given. Finally, the preservation of general properties of logical systems, such as the compactness and the decidability, is also discussed.

# Acknowledgements

The work was supported by the National Natural Science Foundation of China under Grant Nos.60496326, 60573063, 60573064, 60773059 and the National High-Tech Research and Development Plan of China under Grant No.2007AA01Z325.
References

1. Carnielli, W. A., Coniglio, M. E., D'Ottaviano, I. M. L.: New dimensions on translation between logics. Logica Universalis. **3**(2009) 1–18

2. Epstein, R. L.: The Semantic Foundations of Logics, vol.1. Propositional Logics. LKluwer, Dordrecht, 1990.

3. Fara, M., Williamson, T.: Counterparts and actuality. Mind. **114** (2005) 1–30

4. Feitosa, H. A., D'Ottaviano, I. M. L.: Conservative translations. Annals of Pure and Applied Logic. **108** (2001) 205–227

5. Forbes, G.: Canonical counterpart theory. Analysis. **42** (1982) 33–37

6. Hustadt, U., Schmidt, R. A., Georgieva, L.: A survey of decidable first-order fragments and description logics. Journal of Relational Methods in Computer Science. **1** (2004) 251–276

7. Kolmogorov, A. N.: On the principle of excluded middle (1925). In: Heijenoort, J., (ed.) From Frege to Gödel: a Source Book in mathematical logic 1879–1931. Cambridge: Harvard University Press. (1977) 414–437

8. Kurtonina, N., de Rijke, M.: Expressive of concept expression in first-order description logics. Artificial Intelligence. **107** (1999) 303–333

9. Lewis, D.: Counterpart theory and quantified modal logic. Journal of Philosophy. **65** (1968) 113–126

10. Ohlbach, H., Nonnengart, A., de Rijke, M., Gabbay, D.: Encoding two-valued non-classical logics in classical logic. In: Robinson A., Voronkov A., (eds.) Handbook of Automated Reasoning. Amsterdam Netherland: Elsevier. (2001) 1403–1486

11. Prawitz, D., Malmnäs, P. E.: A survey of some connections between classical, intuitionistic and minimal logic. In: Schmidt, H. et al. (eds.) Contributions to Mathematical Logic. North-Holland, Amsterdam. (1968) 215–229

12. Schmidt, R., Hustadt, U.: The axiomatic translation principle for modal logic. ACM Transactions on Computational Logic. **8** (2007) 1–55

13. Shen, Y., Ma, Y., Cao, C., Sui, Y., Wang, J.: Logical properties on translations between logics. Chinese Journal of Computers. **32** (2009) 2091–2098

14. Ramachandran, M.: An alternative translation scheme for counterpart theory. Analysis. **49** (1989) 131–141