Lost in Translation: Language Independence in Propositional Logic - Application to Belief Revision and Belief Merging

1 Introduction

In propositional logic, propositional symbols are the formal counterparts of propositions which are not analyzed (i.e., decomposed) within the language of the logic but can be arbitrarily sophisticated nevertheless. For instance, an (informal) proposition like "John's house is located northern to the station" can be represented by a propositional symbol like p. This symbol p is atomic in the logic, which implies that, from p alone, one cannot infer that concepts like "John", "house", "station", "being northern to" are used to define its actual meaning. Alternatively, the same informal proposition can be represented by slightly more complex formulae, like r ⊕ s where r means "John's house is located northern and western to the station" and s means "John's house is located northern and eastern to the station".

The problem of which informal propositions of interest should be associated with propositional symbols is not ruled by logic since this is mainly a domain-dependent modeling issue. What is important from a logical point of view is to

Nicolas Schwind

CRIL-CNRS, Universit´e d'Artois Lens, France schwind@cril.univ-artois.fr

make a representation choice so that every proposition of interest can be represented as a formula based on the chosen propositional symbols (otherwise the corresponding propositional language is not expressive enough w.r.t. the propositions of interest.) Several choices for propositional symbols are usually possible without questioning such an expressiveness issue.

In artificial intelligence, propositional formulae are used to build propositional structures which represent propositional information. In applications where propositional logic is enough from a representation perspective, information processing can be modeled as a combination of queries (e.g., deducing some facts from the available beliefs or inferring some plausible conclusions from them) and transformations (e.g., forgetting some facts, revising some beliefs.) Propositional queries and propositional transformations can be formalized as propositional operators, which are mappings from propositional structures to propositional structures.

In this paper, we address the language independence issue for propositional operators. Intuitively, a propositional operator Ω is language-independent iff whenever the representation language is modified in such a way that symbols in the original language correspond to formulae in the target language, if the input of Ω is modified so as to reflect the language change, then the output of Ω should be modified accordingly. Thus, language change can be modeled by symbol translations (i.e., substitutions), and language independence for a propositional operator is the faculty for it to be robust w.r.t. symbol translations.

For instance, assume that t represents the fact that "Mary's house is located northern to the station". If it is known that "John's house is located northern to the station" (p) and that "John's house is located northern to the station" if and only if "Mary's house is located northern to the station" (p ⇔ t) since Mary and John live together, then one can deduce that "Mary's house is located northern to the station": t holds. If we consider another representation choice, where "John's house is located northern to the station" is represented by r ⊕ s, then the same conclusion follows: from r⊕s and (r⊕s) ⇔ t, t can still be deduced. Accordingly, the deduction operator is robust when the symbol translation σ such that σ(p) = r⊕s is applied to the given belief base.

Clearly, such a notion of language independence should not be confused with notions of syntax independence, which reflects the ability to be robust w.r.t. substitution of formulae (or sets of formulae) by equivalent formulae (or sets), a topic which got much attention in artificial intelligence. Quite surprisingly, the language independence issue in propositional logic did not receive so far a systematic investigation, despite the fundamental nature of the issue and the significance of propositional languages in artificial intelligence.

This paper is intended to fill the gap. After some formal preliminaries (Section 2), we point out the notion of symbol translation, define the notion of language independence as robustness w.r.t. symbol translations, and present several refinements of it in Section 3. We provide some complexity results in Section 4. As a case study, in Section 5, we put some belief revision/merging operators in the setting and identify the level of language independence achieved by those operators. We discuss some related work in Section 6, before concluding. An extended version (including proofs) is available at http://www.cril.fr/∼marquis/ijcai11b.pdf

2 Formal Preliminaries

We consider a countably infinite set PS of propositional symbols. For any finite subset X of PS, PROPX denotes the propositional language over X defined in the usual way. For every formula α, α0 is equivalent to α and α1 is equivalent to ¬α. For every formula α, Var(α) is the set of propositional symbols occurring in α.

An interpretation ω over X is a mapping from X to {0, 1}, an associated canonical term is a term over X (i.e., a conjunction of literals over X) such that for each x ∈ X, x occurs in it if ω(x) = 1, else ¬x occurs in it. The notion of satisfaction of a formula is the usual one. |= denotes logical entailment and ≡ denotes logical equivalence.

A formula α is said to be generated from a set C of connectives and a set Σ of formulae iff α ∈ Σ or there exists a connective c ∈ C of arity n > 0 such that α ≡ c(α1, . . . , αn) where each αi (i ∈ 1, . . . , n) is generated from C and Σ. A set C of connectives is said to be functionally complete w.r.t. a set of variables X given a set Σ of formulae iff for every propositional formula α generated from C and X, there exists a propositional formula β generated from C and Σ such that β ≡ α.

In the following, we are interested in the robustness to symbol translations offered by propositional operators over propositional structures:

Definition 1 (propositional structure) A propositional structure Σ over a finite set X of propositional symbols is a vector of sets of propositional formulae from PROPX (only finite vectors and finite sets are considered.) If n is the dimension of the vector, Σ is an n-propositional structure.

Sets are interpreted conjunctively, so that two sets of formulae α and β are equivalent, noted α ≡ β, when the conjunction of formulae of α is equivalent to the conjunction of formulae of β.

Two n-propositional structures Σ = 〈α1, . . . , αn〉 and Σ′ = 〈α′1 , . . . , α′n 〉 are equivalent, noted Σ ≡ Σ′ iff ∀i ∈ 1, . . . , n, we have αi ≡ α′i .

Definition 2 (propositional operator) A propositional operator Ω is a mapping associating an m-propositional structure with an n-propositional structure.

Many propositional queries and transformations can be viewed as propositional operators; here are a few examples:

Example 1

• DED (deduction) : 〈{α1, . . . , αn}, {β}〉 ↦→ 〈{⊤}〉 if β is a logical consequence of {α1, . . . , αn}, and 〈{⊥}〉 otherwise;
• ◦ (belief revision) : 〈{α1, . . . , αn}, {β}〉 ↦→ 〈{β1, . . . , βm}〉 where {β1, . . . , βm} is the belief base resulting from revising {α1, . . . , αn} by β using the belief revision operator ◦;
• Δ (belief merging) : 〈{α1 1 , . . . , α1n(1) }, . . . , {αp 1 , . . . , αpn(p)}, {μ}〉 ↦→ 〈{β1, . . . , βm}〉 where {β1, . . . , βm} is the belief base resulting from merging the profile 〈{α1 1 , . . . , α1n(1) }, . . . , {αp 1 , . . . , αpn(p) }〉 using the belief merging operator Δ when μ is the integrity constraint.

3 On Language Independence

3.1 Translations

The key notion for defining notions of language independence is that of translation; let X and Y be two finite subsets of PS:

Definition 3 (translation) A (symbol) translation σ is a mapping from X to PROPY , which is extended to a morphism (also noted σ) from propositional structures over X to propositional structures over Y , defined inductively by (for any n):

• for every connective c of arity k, σ(c(α1, . . . , αk)) = c(σ(α1), . . . , σ(αk)),
• σ({α1, . . . , αn}) = {σ(α1), . . . , σ(αn)},
• σ(〈α1, . . . , αn〉) = 〈σ(α1), . . . , σ(αn)〉.

There is no need to assume any connection between X and Y , i.e., we may have X ∩ Y = ∅, but, conversely, this is not forbidden (e.g., we may have X = Y .) For instance, if σ : {x, y} → PROP{y,z} such that σ(x) = y and σ(y) = ¬y ∨ z, 1 we have σ(x ∧ ¬y) = y ∧ ¬(¬y ∨ z) ≡ y ∧ ¬z.

A fundamental result in propositional logic when dealing with such symbol translations is the well-known substitution theorem:

Proposition 1 (substitution theorem) Let α, β be formulae from PROPX. If α ≡ β then for every symbol translation σ from X to PROPY , we have σ(α) ≡ σ(β).

The following properties are direct consequences of this theorem:

Corollary 1

1. Let {α1, . . . , αn} be a finite set of formulae from PROPX, and let β be a formula from PROPX. We have {α1, . . . , αn} |= β if and only if for every symbol translation σ from X to PROPY , we have σ({α1, . . . , αn}) |= σ(β).

1 We also note σ : x ↦→y; y ↦→ ¬ y ∨ z.

1. |= α if and only if for every symbol translation σ from X to PROPY , we have |= σ(α). Similarly, |= ¬α if and only if for every symbol translation σ from X to PROPY , we have |= ¬σ(α).

Let us illustrate point 1. of Corollary 1 by considering the example provided in the introduction. We have p ∧ (p ⇔ t) |= t. Let σ : p ↦→ (r ⊕ s). Then σ(p ∧ (p ⇔ t)) = (r ⊕ s) ∧ ((r ⊕ s) ⇔ t) implies σ(t) = t.

Obviously enough, in the general case, there is no direct logical connections between a formula α and the associated translated formula σ(α). They can be logically independent, like α = p and σ(α) = q when σ : p ↦→ q is considered. It can also be the case that one of them implies the other one (consider α = p, σ1 : p ↦→ p ∧ q and σ2 : p ↦→ p ∨ q) or that the formulae are jointly inconsistent (consider α = p and σ : p ↦→ ¬p.) Actually, the only direct logical connections between α and σ(α) are obtained in the specific case α is valid or α is contradictory (and are given by point 2. of Corollary 1.) See also the forthcoming Proposition 3.

Nevertheless, some indirect logical connections between α and σ(α) exist, as stated by the following proposition:

Proposition 2 Let α be a formula from PROPX. Let σ be a symbol translation from X to PROPY . We have ∧x∈X (x ⇔ σ(x)) |= α⇔ σ(α).

This proposition shows that α and σ(α) are equivalent modulo the theory where each symbol in X is equivalent to its image by σ.

3.2 Language independence based on translations

We are now ready to define language independence as robustness w.r.t. symbol translations satisfying some properties:

Definition 4 (language independence) Let P be a property on translations. A propositional operator Ω associating an m-propositional structure with an n-propositional structure is P-language independent if and only if for every translation σ satisfying P, for every n-propositional structure Σ, for every m-propositional structure Σ′ such that Ω(Σ) ≡ Σ′ , we have Ω(σ(Σ)) ≡ σ(Σ′ ).

P characterizes what should be preserved (or dually what can be lost) when a symbol translation is applied. Indeed, replacing in a uniform way propositional symbols by formulae may lead to question a number of properties which hold for propositional symbols but can be lost when formulae are considered. For instance, unlike formulae, propositional symbols are neither inconsistent nor valid, conjunction of possibly negated but distinct propositional symbols are always consistent, propositional symbols are enough to generate a full propositional language over them whenever a functionally complete set of connectives is considered.

Formally, we focus on the following properties:

Definition 5 (properties on symbol translations) A symbol translation σ from X = {x1, . . . , xn} to PROPY satisfies:

• UNI (universality);
• SIN (symbol insensitivity) if and only if σ is a bijection from X to Y ;
• TPR (triviality prevention) if and only if ∀x ∈ X, σ(x) is consistent but not valid;
• AIP (atom independence preservation) if and only if ∀s1, . . . , sn ∈ {0, 1}, ∧xi∈X σ(xi)si is consistent;
• FCP (functional completeness preservation) if and only if {¬, ∧} is functionally complete w.r.t. ⋃x∈X Var(σ(x)) given {σ(x) | x ∈ X};
• REV (reversibility) if and only if there exists a symbol translation θ such that ∀x ∈ X, θ(σ(x)) ≡ x.

UNI (universality) is when no constraints at all are imposed on the admissible translations. UNI -language independence is hard to be satisfied since it leads to consider as admissible translations which do not preserve anything from the input propositional structure, except trivialities (tautologies and contradictions) which are always kept. Indeed, we have the following result:

Proposition 3 Let α be a formula of PROPX and β a formula of PROPY . If α is neither valid nor inconsistent, then there exists a symbol substitution σ such that σ(α) ≡ β.

This motivates the need to restrict the set of admissible translations.

SIN-language independence asks the choice of the symbols names to be non-significant. This independence property is highly expected. However, as we will see in the following, it is not always guaranteed for revision/merging operators.

The rationale for TPR is to set aside translations which leads to replace a symbol, which is in essence neither valid nor inconsistent, by a formula which would be valid or inconsistent.

The rationale for AIP-language independence is as follows: at start (i.e., in the language PROPX), all the symbols of X are logically independent, which means that ∀s1, . . . , sn ∈ {0, 1}, ∧xi∈X xsi i is consistent; if another representation choice is made, such an independence should be preserved. Thus, for instance, x ↦→ p ∨ q; y ↦→ ¬p ∨ q does not satisfy AIP since ¬(p ∨ q) ∧ ¬(¬p ∨ q) is inconsistent; contrastingly, x ↦→ p ⇔ q; y ↦→ p satisfies AIP.

FCP-language independence asks for the preservation of functional completeness. In the language PROPX considered at start taking any fully expressive set of connectives (like {¬, ∧}) proves enough to represent every Boolean function over X. In the target language PROPY , it is expected that any functionally complete set of connectives proves enough to represent every Boolean function over Y given that the set of "atoms" is now {σ(x) | x ∈ X}. As an example, consider again x ↦→ p∨q; y ↦→ ¬p∨q; this symbol translation does not satisfy FCP since p cannot be defined using {¬, ∧} when the set of "atoms" is {p∨q, ¬p∨q}; on the other hand, x ↦→ p ⇔ q; y ↦→ p satisfies FCP: both p and q can be defined using {¬, ∧} when the set of atoms is {p ⇔ q, p}; this is obvious for p, and for q, we have q ≡ (p ⇔ q) ⇔ p.

Finally, the idea underlying REV-language independence is the one of reversibility. The intuition is that nothing important is lost in a symbol translation when the translation can be reversed. For instance, x ↦→ p ∨ q; y ↦→ ¬p ∨ q does not satisfy REV since {p ∨ q ≡ x, ¬p ∨ q ≡ y} with variables p and q has no solution over PROP{x,y}. Contrastingly, σ : x ↦→ p ⇔ q; y ↦→ p satisfies REV since θ : p ↦→ y, q ↦→ y ⇔ x is such that θ(σ(x)) ≡ x and θ(σ(y)) ≡ y.

3.3 Connections between notions of language independence

Clearly enough, none of the properties above is trivial in the sense that it would be satisfied by every (or by no) symbol translation when the choice of Y is free. Thus, the identity translation σ : X → PROPX such that σ : x ↦→ x satisfies all the properties above, while σ : {x, y} → PROP{p,q} such that σ : x ↦→ ⊥; y ↦→ p ∨ q satisfies none of them (except UNI of course.)

FCP appears as logically independent of all the properties, except SIN (which implies FCP, and UNI which is obviously implied by FCP):

• SIN implies FCP since any set of connectives which is functionally complete w.r.t. X given X is functionally complete w.r.t. any set of variables Y given Y ;
• x ↦→ ⊥ satisfies FCP (since ⋃x∈X Var(σ(x)) is empty) but does not satisfy TPR;
• x ↦→ x ∨ y satisfies TPR and REV but does not satisfy FCP .

While based on quite different intuitions, it turns out that REV and AIP are the same property:

Proposition 4 REV and AIP are equivalent.

The remaining properties are not logically independent, but connected as follows:

• SIN implies REV : when σ is a bijection from X to Y , θ = σ-1 from Y to X such that for any y ∈ Y , θ(y) = x iff σ(x) = y is such that for all x ∈ X, θ(σ(x)) ≡ x. The implication is strict: let X = {x, y}, Y = {p, q}, σ : x ↦→ p; y ↦→ p ⇔ q. Clearly, σ does not satisfy SIN. However, it satisfies REV : θ such that θ : p ↦→ x; q ↦→ x ⇔ y satisfies θ(σ(x)) ≡ x and θ(σ(y)) ≡ y.
• AIP implies TPR: it is obvious that if there is an xi such that σ(xi) is valid or inconsistent, then there is also a ∧xi∈X σ(xi)si that is inconsistent. The implication is strict: let X = {x, y}, Y = {p}, σ : x ↦→ p; y ↦→ ¬p. σ satisfies TPR but does not satisfy AIP.
• TPR implies UNI since UNI is always satisfied. The implication is strict: let X = {x}, Y = {}, σ : x ↦→ ⊥. σ satisfies UNI but does not satisfy TPR.

The logical dependencies between properties of language independence are given by the implication graph at Figure 1.

Finally, it is easy to check that language independence (whatever P among the choices we considered) is logically independent from syntax independence, where a propositional operator Ω which associates a m-propositional structure with a given n-propositional structure is said to be syntax-independent iff whenever 〈α1, . . . , αn〉 ≡ 〈α′1 , . . . , α′n 〉, we also have Ω(〈α1, . . . , αn〉) ≡ Ω(〈α′1 , . . . , α′n 〉).

4 The Complexity of Recognizing Translations

In this section, we consider the problem of determining whether a given symbol translation is admissible, where admissible means that it satisfies one of the properties considered in the previous section. Such an issue has to be addressed each time a representation change is expected, given a propositional operator which is known as P -language independent. Indeed, a symbol translation is acceptable in this case only if it satisfies P.

First, we show that FCP amounts to a definability issue (see [Lang and Marquis, 2008] for details):

Proposition 5 σ : {x1, . . . , xn} → PROPY satisfies FCP if and only if ∧ni=1 (zi ⇔ σ(xi)) defines ⋃x∈X Var(σ(x)) in terms of {z1, . . . , zn}, where {z1, . . . , zn} ∩ Y = ∅.

We have also derived the following results (symbol translations σ : X → PROPY are supposed to be represented extensionally as {(x, σ(x)) | x ∈ X}):

Proposition 6

1. Determining whether a given symbol translation σ : X →PROPY satisfies SIN is in P.
2. Determining whether a given symbol translation σ : X →PROPY satisfies TRP is NP-complete.
3. Determining whether a given symbol translation σ : X → PROPY satisfies FCP is coNP-complete.
4. Determining whether a given symbol translation σ : X → PROPY satisfies REV (or, equivalently, AIP) is Πp2 -complete.

Interestingly, the problem of determining whether a given symbol translation σ : X → PROPY satisfies REV is a specific case of the following problem of propositional matching (given 2n formulae α1, β1, . . ., αn, βn, determining whether there exists a substitution θ from X = ⋃ni=1 Var(αi) to PROPY with Y = ⋃ni=1 Var(βi) such that for i ∈ 1, . . . , n, θ(αi) ≡ βi.) Hence, Point 4. of Proposition 6 shows that the problem of propositional matching is at least as hard as problem of Boolean unification with constants [Baader, 1998], which was an open problem issue, as far as we know.

5 Language Independence for Belief Merging and Belief Revision

As a case study, we have investigated how some belief revision/merging operators from the literature are languageindependent. Belief merging operators aim at defining a belief base (the merged base) which represents the beliefs of a group of agents given their individual belief bases, and some integrity constraints. Formally, a base K denotes the set of beliefs of an agent, it is a finite set of propositional formulae, interpreted conjunctively. A profile E = 〈K1, . . . ,Kn〉 is a vector of consistent bases representing the beliefs from the group of n agents involved in the merging process. A merging operator Δ is a mapping associating a formula μ (representing the integrity constraints) and a profile E with a new base Δμ(E).

KP rationality postulates [Konieczny and Pino P´erez, 2002] are expected properties for belief merging operators. For space reasons, we only recall two of them:

(IC1) If μ is consistent, then Δμ(E) is consistent;

Distance-based merging operators are characterized by a distance 2 between worlds and an aggregation function f (a mapping associating with a tuple of non-negative real numbers a non-negative real number) [Konieczny et al., 2004]:

Definition 6 (Distance-based merging operator) Let d be a distance between worlds and f be an aggregation function. The merging operator Δd,f is defined for every profile E and every formula μ by mod(Δd,f μ (E)) = min(mod(μ),≤E) where the total preorder ≤E over worlds induced by E is defined by:

• ω ≤E ω′ if and only if d(ω,E) ≤ d(ω′ ,E),
• d(ω,E) = fK∈E(d(ω,K)),
• d(ω,K) =minω′ |=Kd(ω, ω′ ).

Usual distances are dD, the drastic distance (dD(ω, ω′ ) = 0 if ω = ω′ and 1 otherwise), and dH the Hamming distance (dD(ω, ω′ ) = n if ω and ω′ differ on n variables.)

Belief revision operators can be viewed as belief merging operators restricted to singleton profiles, so that AGM/KM postulates [Alchourr´on et al., 1985; Katsuno and Mendelzon, 1991] for belief revision are direct counterparts of KP postulates for singleton profiles; for instance, the KM postulate (R2) (resp. (R3)) for belief revision corresponds to the KP postulate (IC2) (resp. (IC1).)

As Proposition 3 suggests it, UNI -language independence is hardly achieved by operators which have to deal with jointly inconsistent (but typically individually consistent) propositional information, while avoiding trivialization. Actually, focusing on translations satisfying TPR or FCP is not enough as well, since rational belief revision/merging operators (in the sense of AGM/KM postulates for belief revision and KP postulates for belief merging) are neither TPRlanguage independent, nor FCP-language independent; more precisely:

Proposition 7 No belief revision operator ◦ satisfying (R2) and (R3) and no belief merging operator Δ satisfying (IC1) and (IC2) is TPR-language independent or FCP-language independent.

2 Actually, a pseudo-distance is enough, i.e., triangular inequality is not mandatory.

Hence, one needs to consider less restricted forms of language independence, especially REV . It turns out that existing belief revision/merging operators are not equally REVlanguage independent. Unsurprisingly, the distance choice is of tremendous significance in this respect:

Proposition 8 Let f be any aggregation function.

• Every distance-based belief merging operator ΔdD,f based on the drastic distance dD is REV -language independent.
• No distance-based belief merging operatorΔdH,f based on the Hamming distance dH is REV-language independent.

The situation is worse for SIN-language independence since it is not always guaranteed by rational operators:

Proposition 9 There exist belief revision (resp. belief merging) operators which satisfy all AGM/KM postulates (resp. all KP postulates) but are not SIN -language independent.

Indeed, every AGM/KM operator ◦ can be characterized in terms of a faithful assignment associating with every formula α a total preorder ≤α over interpretations, so that the models of α ◦ β are exactly the models of β which are minimal w.r.t. ≤α [Katsuno and Mendelzon, 1991]. The point is that nothing ensures that the faithful assignment associates with σ(α) a total ordering corresponding to ≤σ(α) even when σ is a bijective symbol translation. For instance, let X = Y = {a, b}. Consider a belief revision operator associated with a faithful assignment such that:

Let σ : a ↦→ b; b ↦→ a. Let α = a∧¬b and β = b. We have α◦β ≡ ¬a∧b. Now, σ(α) ≡ ¬a∧b and σ(β) ≡ a. We have σ(α) ◦ σ(β) ≡ a ∧ b, which is not equivalent to σ(α ◦ β).

This calls for two further axioms expressing such a form of language independence ((SIN-R) for belief revision and (SIN-M) for belief merging), stating respectively that for every bijection σ from X to Y :

Those axioms complement the ones related to syntax independence ((R4) for belief revision, and (IC3) for belief merging) and seem highly desirable. Actually, the distancebased belief revision and belief merging operators, based on "standard distances" (like the drastic distance and the Hamming one), satisfy those axioms. More generally, when X = {x1, . . . , xn} contains n atoms, let a distance d over interpretations over X be decomposable when there exists a mapping fd : Rn → R symmetric in each argument and a symmetric mapping gd : {0, 1} × {0, 1} → R such that d(ω1, ω2) = fd(gd(ω1(x1), ω2(x1)), . . . , gd(ω1(xn), ω2(xn)). We have:

Proposition 10 Every belief revision/merging operator based on a decomposable distance is SIN-language independent.

For the drastic distance dD, we have fdD = max and gdD (x, y) = 0 if x = y, = 1 otherwise. For the Hamming distance dH, we have fdH = Σ and gdH = gdD .

6 Other RelatedWork

Independence is well-known as a key notion in many domains within artificial intelligence, especially graphical models for representing beliefs (e.g., Bayes nets) or preferences (e.g., CP-nets or GAI-nets.) In propositional logic, since Belnap's work about relevance logic in the sixties, a number of concepts of independence (also referred to as irrelevance, separability, etc.) has been pointed out in the literature (see [Lang et al., 2002; 2003] for a survey.) Various forms of syntax-independence for belief bases have also been investigated so far [Dalal, 1988; Nebel, 1991; Benferhat et al., 1997; Hansson, 2002]. Qualitative independence, i.e., how the fact of learning a new piece of evidence individually affects previous beliefs, has been studied as well for a while [Dubois et al., 1997]. It turns out that none of these notions of independence in propositional logic coincides with a form of language independence (in all the works cited above, independence is defined as a relation over a language over a fixed set of propositional symbols.)

More recently, Makinson [Makinson, 2009] studied a notion of relevance (canonical relevance) which is expected to be respected in belief change (roughly, contracting a belief base/set K with some piece of information α should preserve every consequence β of K when α is irrelevant to β.) While canonical relevance is syntax-independent in the usual sense, Makinson shows that it is not language-independent; revisiting Makinson's counter-example in the light of our work, we can state more precisely that canonical relevance is SINlanguage independent, but is neither REV -language independent nor FCP-language independent.

7 Conclusion

This paper is centered on the concept of language independence in propositional logic. The main contributions are mainly as follows:

• We have defined language independence as robustness w.r.t. symbol translations.
• We have motivated the need to focus on symbol translations of different types, i.e., satisfying some additional properties, which leads to several notions of language independence. We have shown how they are logically connected.
• We have identified the complexity of recognizing symbol translations satisfying properties of interest.
• As a case study, we have investigated the robustness of belief revision and belief merging operators w.r.t. translations of different types. Only limited forms of language independence are satisfied in the general case for belief change operators. Especially, even SIN-language independence is not guaranteed for the AGM/KM belief revision operators.

This work paves the way for three main directions for further research. A first one concerns belief change; pointing out other operators satisfying SIN-language independence would be useful. A second direction consists in investigating the "degree" of language independence of other propositional operators from the literature (for instance, abduction, circumscription and other forms of closed-world reasoning.) A third one consists in determining how our results can be lifted to other propositional settings where a substitution theorem holds (for instance, this is the case for a number of multi-valued paraconsistent logics.)