Reasoning under inconsistency: the forgotten connective

1 Introduction

There are many different situations that can lead to reason with sets of (mutually) inconsistent formulae (see e.g. [Bloch and Hunter, 2001] for a classi�cation).

When dealing with an inconsistent belief base, a rational agent must refrain from using classical entailment to exploit her belief base, since from an inconsistent belief base, every formula is a logical consequence.

Many approaches have been proposed so far to address the paraconsistency issue, i.e., the problem of designing inference relations that do not necessarily trivialize when the belief base is inconsistent, but preserve many expected consequences nevertheless. Among them, many approaches to avoid trivialization in presence of a contradiction consist in weakening the inconsistent belief base by inhibiting some formulae in it. To be more precise, the key idea of such approaches is to select some consistent subsets of the belief base B, then to reason deductively from some of them.

Clearly enough, such approaches require a belief base to be a set of formulae, not a single formula (inhibition consists in removing formulae from the set). As a consequence, a (�nite) inconsistent set of formulae cannot be considered as equivalent to the conjunction of its elements (and this contrasts with what happens when consistent sets are considered). For instance, the set of consequences of {ϕ, ¬ϕ, ψ} typically differs from the set of consequences of {ϕ ∧ ¬ϕ ∧ ψ}.

Pierre Marquis CRIL - Universit·e d'Artois 62307 Lens, France marquis@cril.univ-artois.fr

Handling in a different way conjunctions of formulae and sets of formulae when they are classically inconsistent is an idea which underlies many paraconsistent logics for decades. Such logics are called non-adjunctive logics, which just means that the inference rule which consists in considering the conjunctive formula φ ∧ ψ as derivable from the set {ϕ, ψ} fails. For instance, Ja·skowski's discursive logic [Ja·skowski, 1969], one of the �rst paraconsistent logic pointed out so far, is non-adjunctive: in this logic, a propositional formula ϕ is considered as a consequence of a set of formulae {ϕ1, . . . , ϕn} if and only if ⋄ϕ is a consequence of {⋄ϕ1, . . . , ⋄ϕn} in epistemic logic S5; this amounts to say that ϕ is a consequence of {ϕ1, . . . , ϕn} in Ja·skowski's logic if and only if ϕ is a classical consequence of one of the ϕi's. This approach has been further re�ned by Rescher and Manor [Rescher and Manor, 1970], who suggest to conjoin up to maximal consistency, and then by many AI researchers who introduce conjoining policies that can take advantage of additional information about the relative certainty of pieces of belief.

Nevertheless, as far as we know and apart of the recent work [Mengin, 2004] discussed in Section 8, considering comma as a plain connective has never been overstepped up to now, in particular the languages of previous paraconsistent logics do not enable sets of formulae to be nested. De�ning and investigating a logical framework in which such a �comma connective� is used is the main purpose of this paper, which is organized as follows. After some formal preliminaries, we present both the syntactical and the semantical aspects of the �comma logic� in Section 3. Some properties of the corresponding inference relation are given in Section 4. The generality of the proposed framework is discussed in Section 5. Some translatability results and some complexity results are given in Section 6. An alternative semantics for the comma connective based on cardinality is brie�y discussed in Section 7. Due to space limitations, most proofs are only sketched. Section 8 concludes the paper.

2 Preliminaries

Let PS be a �nite set of propositional variables: a, b, c, etc. LPS is the propositional language built from PS, the constants ⊤ (verum) and ⊥ (falsum) and the standard connectives {∧, ∨, ¬,→} in the usual way. Formulae of LPS are noted with small Greek letters ϕ, ψ, etc. An interpretation (world) M is a total function fromPS to {0, 1}, typically represented as the set of all the variables of PS it satis�es. MPS denotes the set of interpretations built over PS. M is a model of a formula ϕ, denotedM |= ϕ, if and only if it makes it true (in the usual truth-functional way). Mod(ϕ) denotes the set of models of ϕ. |= denotes classical entailment and ≡ denotes equivalence between formulae from LPS .

Let ⊂ denotes strict inclusion. Let B = {ϕ1, . . . , ϕn} be a �nite set of formulae of LPS, and let B′ ⊆ B, we note ∧ B′ = ∧{ϕi |ϕi ∈ B′}. B′ is a consistent subset of B if and only if ∧ B′ is consistent. B′ is a maximal consistent subset (or maxcons) of B if and only if B′ is consistent and there is no consistent B′′ such that B′ ⊂ B′′ ⊆ B. MaxCons(B) denotes the set of the maximal consistent subsets of B.

3 The �comma logic�

Let us start with the de�nition of the language of our comma logic.

De�nition 1 The language LCPS of the propositional comma logic is de�ned inductively as follows:

• PS ∪ {⊤,⊥} ⊆ LCPS ;
• If ϕ ∈ LCPS and ψ ∈ LCPS then (¬ϕ), (ϕ∧ψ), (ϕ∨ψ), (ϕ → ψ) belong to LCPS ;
• If n ≥ 0 and {ϕ1, . . . , ϕn} ⊆ LCPS then 〈ϕ1, . . . , ϕn〉 belongs to LCPS .

Parentheses can be omitted when no ambiguity is possible.

Clearly enough, LCPS is a superset of LPS: nonclassical formulae obtained by taking advantage of the comma connective can be formed. Here, we abuse words slightly: comma is actually considered as a set constructor, hence formally comma denotes a family of connectives, one per possible arity. Especially, comma is not always binary: one can apply the comma connective to no formula at all (the empty set), one formula (singletons), or more than two formulae. This forces us to introduce additional separators (the chevrons 〈 and 〉 � which must not be confused with parentheses) but enables to keep the notations not too heavy.

It proves also interesting to de�ne the depth of a formula of LCPS , and the languages {LC[n] PS , n ∈ IN} as:

De�nition 2 The depth of a formula ϕ from LCPS is de�ned inductively as follows:

• If ϕ ∈ PS ∪ {⊤,⊥} then depth(ϕ) = 0 ;
• depth(¬ϕ) = depth(ϕ) ;
• depth(ϕ ∧ ψ) = depth(ϕ ∨ ψ) = depth(ϕ → ψ) = max(depth(ϕ), depth(ψ)) ;
• depth(〈ϕ1, . . . , ϕn〉) = maxi=1...n depth(ϕi) + 1. 1

For n ∈ IN, LC[n] PS is the set of all formulae of LCPS whose depth is less or equal to n.

One can easily check that LCPS = ⋃n∈INLC[n] PS and LC[0] PS = LPS. Finally, for all n ≥ 1, we de�ne the language LC[s,n] PS (set of simple formulae of depth n) as the subset of LC[n] PS containing all formulae 〈ϕ1, . . . , ϕk〉, where ϕ1, . . . , ϕk are formulae of LC[n-1] PS , i.e., the set of formulae of depth n where comma is the main functor. Here are some examples of formulae of LCPS , where PS = {a, b, c}:

1 By convention depth(〈 〉) = 1.

• ϕ1 = a ∧ b ∧ (¬b ∨ c) ∧¬c;
• ϕ2 = 〈a ∧ b, ¬b ∨ c, ¬c〉;
• ϕ3 = 〈a ∧ (b ∨ 〈c, a ∨ b, ¬c〉), 〈¬b ∨ c, ¬c〉 ∧ 〈a, ⊤〉〉;
• ϕ4 = 〈 〉.

We have depth(ϕ1) = 0; depth(ϕ2) = 1; depth(ϕ3) = 3. Note also that ϕ2 ∈ LC[s,1] PS (as ϕ4) and that ϕ3 ∈ LC[s,3] PS . Let us now present the semantics of our new language:

De�nition 3 The notion of satisfaction of a formula of LCPS by an interpretationM is given by the relation |=c onMPS× LCPS de�ned inductively as:

• M|=c⊤;
• M ̸|=c⊥;
• If a ∈ PS, M|=ca if and only if a ∈M;
• M|=c¬ϕ if and only if M ̸|=cϕ;
• M|=c ϕ ∧ ψ if and only if M|=cϕ and M|=cψ;
• M|=c ϕ ∨ ψ if and only if M|=cϕ or M|=cψ;
• M|=c ϕ → ψ if and only if M|=c ¬ϕ or M|=c ψ;
• M|=c 〈ϕ1, . . . , ϕn〉 if and only if there is no interpretation M ′ ∈ MPS such that {i | M ′ |=cϕi} strictly contains {i | M|=cϕi}.

We now extend several standard notions (and the corresponding notations) from classical logic to comma logic. Let ModC(ϕ) = {M ∈ MPS | M|=cϕ}. A formula of LCPS is said to be consistent (or satis�able) if and only if ModC(ϕ) ̸= ∅, and valid if and only if ModC(ϕ) =MPS. If ϕ and ψ are two formulae of LCPS , ψ is said to be a consequence of ϕ (denoted ϕ|=cψ) if and only if ModC(ϕ) ⊆ ModC(ψ). When ϕ = ⊤, we simply write |=cψ instead of ⊤|=cψ. Two formulae ϕ and ψ of LCPS are said to be equivalent, noted ϕ≡cψ, if and only if ϕ|=cψ and ψ|=cϕ.

4 Some logical properties

It is easy to show that, in contrast to the other connectives in the logic, the comma connective is not truth-functional: in the general case, the truth value of 〈ϕ1, . . . , ϕn〉 from LCPS in interpretation M cannot be determined from the truth values of each ϕi (i ∈ 1 . . . n) in M only. For instance, let PS = {a, b}, M = {a}, ϕ1 = 〈a, b〉, ϕ2 = 〈a ∧ ¬b, b〉: M satis�es the ��rst� element of ϕ1 and ϕ2, but does not satisfy the �second� one; while M is a model of ϕ2, it is not a model of ϕ1. This lack of truth-functionality explains why the comma connective is really genuine in the logic. (It cannot be de�ned by just combining connectives of classical logic).

Actually, the discrepancy between classical logic and comma logic lies only in the comma connective, since:

Proposition 1 Comma logic is a conservative extension of classical logic: for every pair of formulae ϕ, ψ in which the comma connective does not occur, then ϕ|=cψ if and only if ϕ |= ψ.

Obviously, new valid formulae are obtained in comma logic, like 〈ϕ, ¬ϕ〉, because the language of propositional logic has been enriched, but in any case classical theorems are preserved.

Furthermore, the replacement metatheorem of classical logic can be extended to comma logic:

Proposition 2 Let ϕ be a valid formula from LCPS and let x ∈ PS. Let ψ be any formula from LCPS . The formula obtained by replacing in ϕ every occurrence of x by an occurrence of ψ is valid as well.

Let us now make precise some properties of the inference relation |=c . First, a direct consequence of its de�nition is that |=c is a Tarskian consequence relation (since it is de�ned as model containment); from this observation, a number of immediate properties follows, especially the fact that |=c is re�exive and transitive. By the way, note that while in classical logic the basic entailment relation |= on LPS ×LPS can be easily extended to a relation on 2LPS × LPS by de�ning the models of a set of formulae as the interpretations satisfying every formula from the set, the similar construction would not be meaningful here; indeed, in comma logic, sets of formulae are interpreted in a nonstandard way. This renders the usual characterization of Tarskian consequence relations inadequate in our setting since |=c does satisfy neither strong re�exivity nor monotonicity:

• 〈a, ¬a〉 ̸|=ca;
• 〈a〉|=ca but 〈a, ¬a〉 ̸|=ca.

Here are some other valuable properties:

Proposition 3

1. If ϕ1|=cϕ2 and 〈ϕ1, ϕ2〉|=cψ, then ϕ1|=cψ.
2. If 〈ϕ1, ϕ2〉|=cψ, then ϕ1|=c (ϕ2 →ψ).
3. If ϕ1≡cϕ2 and ϕ1 is a subformula of ψ, then any formula obtained by replacing in ψ occurrences of ϕ1 by ϕ2 is equivalent to ψ.
4. ϕ|=cψ1 ∧ψ2 if and only if ϕ|=cψ1 and ϕ|=cψ2.
5. If 〈ϕ, ϕ1〉|=cψ and 〈ϕ, ϕ2〉|=cψ, then 〈ϕ, (ϕ1 ∨ ϕ2)〉|=c ψ.

Item (1) is a form of the cut rule. Item (2) is a form of the deduction metatheorem. Item (3) is the substitution metatheorem for the �comma logic�. In particular, it shows that ∀k if ∀i ∈ 1 . . . k ϕi ≡c ϕ′i then 〈ϕ1, . . . , ϕk, . . . , ϕn〉 ≡c 〈ϕ′1, . . . , ϕ′k , . . . , ϕn〉. Item (4) is a form of the �and rule�. Item (5) is a form of proof by cases (or �or rule�).

Other standard metatheorems of classical logic fails in the general case for full comma logic, i.e., when sets of formulae are considered. For instance, modus ponens fails (〈a, (a → ¬a)〉 ̸|=c¬a), and-elimination and or-introduction as well (〈⊥, ϕ〉 ̸|=c⊥ and 〈⊥〉 ̸|=c⊥∨ϕ); reduction ad absurdum fails (ϕ|=cϕ while 〈ϕ, ¬ϕ〉 ̸|=c⊥).

Let us now present additional properties which state how the comma connective interacts with the other connectives (and itself).

Proposition 4

1. For any permutation σ of {1, . . . , n}, 〈ϕ1, . . . , ϕn〉 is equivalent to 〈ϕσ(1), . . . , ϕσ(n)〉.
2. 〈ϕ1, . . . , ϕ1, ϕ2, . . . , ϕn〉 ≡c 〈ϕ1, . . . , ϕn〉.
3. ∀n ≥ 0 〈ϕ1, . . . , ϕn〉 ̸|=c⊥.
4. 〈ϕ1, ϕ2, . . . , ϕn〉 ≡c 〈ϕ2, . . . , ϕn〉 if ϕ1 is inconsistent or (∃i ∈ 2 . . . n, ϕi is consistent and ∀i ∈ 2 . . . n, ϕi |= ϕ1).
5. ϕ1 ∧ . . . ∧ ϕn|=c 〈ϕ1, . . . , ϕn〉.
6. 〈ϕ1, . . . , ϕn〉∧〈ψ1, . . . , ψm〉|=c 〈ϕ1∧ψ1, . . . , ϕ1∧ψm, . . . , ϕn ∧ ψ1, . . . , ϕn ∧ ψm〉.
7. 〈ϕ1, . . . , ϕn〉 ∧ 〈ψ1, . . . , ψm〉|=c 〈ϕ1, . . . , ϕn, ψ1, . . . , ψm〉.
8. If ϕi is consistent (for at least one i ∈ 1 . . . n), then 〈ϕ1, . . . , ϕn〉|=cϕ1 ∨ . . . ∨ ϕn.
9. If ϕ is consistent, then 〈ϕ1 ∨ ϕ, . . . , ϕn ∨ ϕ〉 ≡c (ϕ1 ∧ . . . ∧ ϕn) ∨ ϕ.
10. ¬(¬ϕ) ≡c ϕ.

Item (6) shows that the �comma connective� is symmetric in every argument. Item (7) shows that the �comma connective� is idempotent.

Item (8) shows that for every n > 0, every formula from LC[s,n] PS is consistent (obviously, this cannot be extended to the full language LCPS ). This is suf�cient to ensure that |=c achieves a form of paraconsistency when starting from a set of formulae.

Item (9) gives a suf�cient condition to simplify a set of formulae (note that in contrast to classical logic, it is not possible in general to remove a formula from a set as soon as it is entailed by another formula; for instance, while a ∧ b|=c a ∨ b, we do not have 〈a ∧ b, ¬a, a ∨ b〉 equivalent to 〈a ∧ b, ¬a〉).

Items (10), (11), (12) make precise the connection between the comma connective and conjunction. None of the converse relation holds in the general case (for (10), ϕ1 ∧ . . . ∧ ϕn should be consistent; the converse of (11) does not hold even in the restricted case m = 1 and 〈ϕ1, . . . , ϕn〉 ∧ ψ1 is consistent: 〈a∧¬b, ¬a∧¬b, ¬a∧¬b〉 ̸|=c 〈a, ¬a∨ b, ¬a〉 ∧¬b; the converse of (12) fails since for instance 〈a, ¬a〉 ̸|=c 〈a〉 ∧ 〈¬a〉). Note also that there is in general no deductive connections between a formula where nested commas occur and its �unfold� counterpart. Especially, in general, we have:

Item (13) and (14) make precise the connection between the comma connective and disjunction. No other signi�cant properties involving disjunction hold; for instance 〈a, b, ¬b〉∨ ¬a ̸|=c 〈a ∨ ¬a, b ∨ ¬a, ¬b ∨ ¬a〉. Together with the previous properties concerning conjunction, it shows that we can consider the comma connective as a �weak� conjunction connective, since it is equivalent to it when the conjunction is consistent, but gives a consistent result even when it is not. Furthermore, when all the formulae are pairwise contradictory but one of them is consistent, comma is equivalent to the disjunction connective. Thus, if we specialize it to the case two formulae ϕ and ψ are considered, we get the easy corollary:

Item (15) �nally states that negation is involutive for the full logic (in particular, ¬(¬〈ϕ1, . . . , ϕn〉) ≡c 〈ϕ1, . . . , ϕn〉). No other link between negation and the comma connective can be established in the general case (for instance, ¬ does not distribute over the �comma connective�; for instance, ¬〈⊥〉 ≡c ⊥ while 〈¬⊥〉 ≡c ⊤).

5 Generality of the framework

Let us now show how several approaches for dealing with inconsistency can be encoded in this logic.

5.1 Skeptical inference

One of the most common method for reasoning from an inconsistent set of formulae consists in selecting the maximal (w.r.t. set inclusion) consistent subsets (also called maxcons) of formulae (see [Rescher and Manor, 1970] for example). Consequences w.r.t. skeptical inference (also called �universal� inference) are then de�ned as classical consequences of every maxcons:

Such an inference relation can be easily recovered in our comma logic:

5.2 Credulous inference

From a set of maxcons, one can also consider credulous inference (also called �existential� inference), that allows to infer a formula if at least one maxcons classically entails it.

Again, such an inference relation can be easily recovered in our comma logic:

Proposition 6

5.3 Supernormal defaults

Assumption-based theories and supernormal default logic [Poole, 1988; Brewka, 1989] can be described in the following way. Let 〈B, Bd〉 be a pair, where B and Bd are two �nite sets of formulae. B is the set of facts (or hard constraints), that is supposed to be consistent. Bd is a set of defaults, i.e., a set of formulae that one wishes to add to facts if it does not result in an inconsistency. Bd is often not consistent with B.

An extension is a subset of formulae of B∪Bd that contains all the formulae of B and a maximum (w.r.t. set inclusion) of formulae of Bd. So, the set of all the extensions is de�ned as: Extens(〈B, Bd〉) = {E | E ⊆ B∪Bd and B ⊆ E and E ̸|= ⊥ and ∀E′ s.t. E ⊂ E′ ⊆ B ∪Bd,E′ |= ⊥}.

Inference from such a supernormal default theory 〈B, Bd〉 is de�ned as:

This can be also easily expressed within the comma logic framework (note that since the set B of facts is consistent, it can be considered conjunctively):

∧ B, . . . , ϕn ∧ ∧ B〉 ∧ ∧ B|=cϕ. Finally, note that since circumscription can be encoded as skeptical inference from supernormal defaults (see e.g., [Etherington, 1987]), it can also be encoded in the comma logic framework.

5.4 Belief revision

The basic revision operator proposed by Nebel [Nebel, 1991; 1998; Fagin et al., 1983] is de�ned as follows:

In comma logic, this can be expressed as follows:

5.5 Belief merging

Suppose that one wants to merge several belief (or goal) bases while allowing some of those bases to be inconsistent. If one wants to take into account inconsistent belief bases in the merging process, one can �rst perform an intra-source merging in order to extract useful information from those bases, before making the proper inter-source merging.

Let E = {B1, . . . ,Bn} be a set of (possibly inconsistent) belief bases s.t. for all i ∈ 1 . . . n, we have Bi = {ϕi1, . . . , ϕiki }. Then, we can de�ne the merging of those

This operator is not de�nable as a two aggregation steps merging operator (as de�ned in [Konieczny et al., 2002]). Conversely, considering an alternative semantics for the comma connective (see Section 7), we can capture some of the two aggregation steps merging operators in comma logic.

6 Computational aspects

Let us investigate both translatability issues and complexity issues for comma logic. First of all, one can prove that the expressiveness of the comma logic is exactly the same as the expressiveness of classical logic (every piece of information which can be encoded in one of the logics can also be encoded in the other one):

Proposition 9 For any formula ϕ of LCPS , there is a formula ψ of LC[0] PS = LPS that is equivalent to ϕ.

A simple induction on the depth of the formulae shows how each formula ϕ of LCPS can be equivalently (for |=c ) rewritten into a classical formula C(ϕ). Let ϕ be a formula of LCPS of depth k. A translation of it into a classical formula can be obtained as follows. First, replace every subformula of ϕ

that is in LC[s,1] PS by an equivalent formula from LC[0] PS (the substitution theorem for the �comma logic� makes it sound); one gets then a formula of depth n - 1, so we can iterate the process until a formula of depth 0 is obtained. For example, let ϕ = 〈a, b, 〈¬b∨c, ¬c〉〉; we start by translating 〈¬b∨c, ¬c〉 in ¬b ∧ ¬c: after one iteration, we get the formula 〈a, b, ¬b ∧ ¬c〉, and a second iteration gives (a ∧ b) ∨ (a ∧ ¬b ∧ ¬c), that is equivalent to a ∧ (b ∨ ¬c). The problem with such a translation is that the size of C(ϕ) is generally exponentially larger than the size of ϕ. Can we do better? Actually, the answer is negative:

Proposition 10 Under the usual assumptions of complexity theory, 2 there is no polysize function that maps any formula from LCPS (and even from LC[1] PS ) to

• an equivalent classical formula.
• an equivalent formula from LCPS in which the �comma connective� is binary (i.e., whenever it is used, it may connect at most two formulae).

The �rst item is a direct consequence of the noncompilability of circumscription [Cadoli et al., 1997]. The second is a consequence of the �rst one, given that every formula ϕ from LCPS in which the comma connective is at most binary can be turned into a classical formula whose size in bounded by |ϕ| (the proof is easy by structural induction given Corollary 1).

Let us now turn to the inference issue. From De�nition 3, it is easy to show that ϕ|=cψ if and only if ϕ ∧ ¬ψ is inconsistent. Hence it is suf�cient to focus on the satis�ability issue. The satis�ability problem in LCPS is, of course, at least as hard than for classical logic (so it is NP-hard). Can we say more than that? Let us begin with LC[1] PS .

Proposition 11 The satis�ability problem in LC[1] PS is Σp2 - complete.

Membership to Σp2 comes from the fact that the corresponding model checking problem is in coNP: for any simple subformula ψ = 〈α1, . . . , αn〉 of ϕ from LC[s,1] PS , deciding whether M ̸|=cψ simply consists in guessing an interpretation M ′ and to check in polynomial time that the set of αi satis�ed by M ′ is a proper superset of the set of αi satis�ed by M. Actually, the truth values of all such ψ in M can be established in nondeterministic polynomial time (guess in parallel several M ′ , one for each simple subformula ψ of depth 1 which is not satis�ed by M). Once this has been done, the truth value of ϕ in M can be computed in deterministic polynomial time. Hardness comes fromΣp2 -hardness of credulous inference from maximal consistent subbases [Nebel, 1998; Cayrol and Lagasquie-Schiex, 1995].

Now, what about the satisfaction problem when commas are nested? An iterated use of the proof of the preceding result (membership part) easily leads to the following:

Proposition 12

• The satis�ability problem in LC[n] PS is in Σpn+1 .
• The satis�ability problem in LCPS is in PSPACE.

2 Especially, the fact that the polynomial hierarchy does not collapse.

We do not have hardness proofs but we conjecture them. 3 Thus, we do not know how to perform comma elimination (for the nested occurrences) in polynomial time (and we conjecture that it is not possible to do it); especially, introducing new symbols would not necessarily preserve equivalence over the original language; for instance, 〈a, 〈¬a, b〉〉 ̸≡c 〈a, new〉 ∧ (new ⇔ 〈¬a, b〉).

Let us now give a few comments about those complexity results. First, the fact that satis�ability in LC[1] PS is at the second level of the polynomial hierarchy, and not higher are good news. We know (from Section 5) that the universal and existential inference problems can be reduced, in polynomial time, to satisfaction or validity problems of formulae of LC[1] PS . Given complexity results from [Cayrol et al., 1998; Nebel, 1998], it follows that the satis�ability problem in LC[1] PS cannot be lower than the second level of the polynomial hierarchy. The fact that it is not higher shows that the gain of �exibility we get does not result in a complexity shift.

7 Variation on the �comma semantics�

Among others, another semantics for the comma connective is obtained by considering as models of 〈ϕ1, . . . , ϕn〉, the interpretations that maximize the number of satis�ed formulae ϕi. Formally, this amounts to replacing in De�nition 3, the itemM|=c 〈ϕ1, . . . , ϕn〉 by the following one:

• M|=Cc 〈ϕ1, . . . , ϕn〉 if and only if there is no interpretation M ′ ∈ MPS such that |{i | M ′ |=cϕi}| > |{i | M|=cϕi}|.

Properties reported in Section 4 are typically preserved by this modi�cation, but idempotence: 〈ϕ1, ϕ1, ϕ2, . . . , ϕn〉 is (generally) not equivalent to 〈ϕ1, ϕ2, . . . , ϕn〉. For example, 〈a, a, ¬a〉 is not equivalent to 〈a, ¬a〉 under the cardinality maximality semantics.

Contrariwise to the |=c case, we can show that:

Proposition 13 For every �xed n, there is a polysize function that maps any formula of LC[n] PS into a query-equivalent formula of LPS when we appeal to the |=Cc semantics.

The proof is a constructive one and relies on a translation function C similar to the one given in Section 6: we �rst replace each occurrence of the formulae ψ = 〈α1, . . . , αn〉 of LC[s,1] PS in ϕ by the cardinality formulae [= kψ] : 〈α1, . . . , αn〉, meaning that exactly kψ formulae among the n formulae α1, . . . , αn must be satis�ed (see e.g. [Benhamou et al., 1994]); such cardinality formulae can be translated in polynomial space as classical query-equivalent formulae. Such a translatability result is helpful in the objective of compiling formulae from LC[n] PS into classical formulae so as to improve inference.

Proposition 14 The satis�ability problem in LCPS for |=Cc is in ∆p2 .

3 That the comma nesting level goes seemingly pairwise with a complexity increase is not surprising (a similar phenomenon happens when conditionals are nested, see e.g. [Eiter and Gottlob, 1993]).

Membership to ∆p2 comes from the fact that one can associate to any simple subformula ψ = 〈α1, . . . , αn〉 of ϕ ∈ LCPS the maximal number kψ of αi which can be jointly satis�ed. Simple subformulae of ϕ are processed by increasing depth: for any ψ of depth 1, the αi are classical formulae, and using binary search, logarithmically many calls to an NP oracle are suf�cient to compute the corresponding kψ. For any ψ of depth 2, again using binary search, logarithmically many calls to an NP oracle are suf�cient to compute the corresponding kψ: the key observation is that the model checking issue for ψ can be done in polynomial time once the kψ′ for each simple subformula ψ′ of ψ have been computed (M|=Cc ψ′ if and only if M satis�es kψ′ elements in ψ′ ), and so on. Since ϕ does not contain more than |ϕ| simple subformulae, linearly many calls to an NP oracle are suf�cient to compute all the kψ; since model checking is in P once they have been computed, a last call to an NP oracle is suf�cient to determine whether ϕ is satis�able. We conjecture that the problem is ∆p2 -complete but have only a proof of Θp2 - hardness at that time.

One has to note that the complexity gap (between the �rst and the second level of the polynomial hierarchy) highlighted by [Cayrol et al., 1998] when one goes from the cardinality criterion to the set-inclusion one, becomes here an amazing gap (from at most ∆p2 to PSPACE) � under the assumption of completeness for PSPACE, of course.

8 Conclusion

In this paper, we have given a �logic� for paraconsistent reasoning where comma is considered as a genuine connective. We have presented some properties of this logic, and we have shown that it allows to express, in a uni�ed language, several problems of reasoning with inconsistent belief bases, nonmonotonic inference, belief revision and belief merging. We have also provided some translatability results and some complexity results. Finally, we have given an alternative semantics for the comma connective.

A distinction between a �nite set of formulas and the conjunction of them is also made in many substructural logics, i.e. logics weaker than the classical one because of the absence of some structural rules [Restall, 1999]. The �comma connective� in such logics is not necessarily commutative or idempotent. Unlike in our comma logic, it is binary and cannot be in the scope of every other connective under consideration in the language.

Another closely related work is [Mengin, 2004], which de�ned a more general framework than ours: it can be shown indeed that any formula of our language can be translated in a formula of his (which is a consequence of the equivalence given in his Section 3.3 for formulas of depth one together with our Proposition 2). Therefore, our logical properties and complexity results carry on to the framework of [Mengin, 2004].

Acknowledgements

The authors would like to thank the anonymous reviewers for their comments. This work has been supported by the Universit·e d'Artois, the IRCICA Consortium, the R·egion Nord/Pasde-Calais and the European Community FEDER program.