What Is an Ideal Logic for Reasoning with Inconsistency?

1 Introduction

Handling contradictory data is one of the most complex and important problems in reasoning under uncertainty. To handle inconsistent information one needs a logic that, unlike classical logic, allows contradictory yet non-trivial theories. Logics of this sort are called paraconsistent [da Costa, 1974]. There are many AI applications that are based, in one way or another, on some paraconsistent logic. For instance, the inconsistency measurements in [Oller, 2004] are based on Priest's three-valued paraconsistent logic LP [Priest, 1989], the database mediator system in [de Amo et al., 2002] is based on the logic of formal inconsistency LFI1 [Carnielli et al., 2007], and the preference modeling approach in [Perny and Tsouki`as, 1998] is based on Belnap's four-valued logic [Belnap, 1977]. In many of these applications, however, it is not clear what are the criteria for choosing a certain paraconsistent logic for the application at hand, and - what is more - whether such a logic can be extended or modified (say, to accommodate beliefs, certainty factors, and so forth) without affecting its basic properties regarding the inconsistency maintenance. This is also realized in light of the fact that already in the early stages of investigating reasoning with inconsistency it has been acknowledged that paraconsistency by itself is not sufficient for a plausible handling of contradictory data. This implies that other considerations should be taken into account in the choice of a proper paraconsistent logic.

In this paper we identify the following properties as desirable for a 'decent' logic for reasoning with inconsistency:

1. Paraconsistency. The rejection of the principle of explosion, according to which any proposition can be in-
2. ferred from an inconsistent set of assumptions, is a primary condition for properly handling contradictory data.
3. Sufficient expressive power. Clearly, a logical system is useless unless it can express non-trivial, meaningful assertions. In our framework, a corresponding language should contain at least a negation connective, which is needed for defining paraconsistency, and an implication connective, admitting the deduction theorem.
4. Faithfulness to classical logic. As observed by Newton da Costa, one of the founders of paraconsistent reasoning, a useful paraconsistent logic should be faithful to classical logic as much as possible. This implies, in particular, that entailments of a paraconsistent logic should also be valid in classical logic.
5. Maximality. The aspiration to "retain as much of classical logic as possible, while still allowing non-trivial inconsistent theories" is reflected by the property of maximal paraconsistency, according to which any extension of the underlying consequence relation yields a logic that is not paraconsistent anymore.

We call logics that satisfy all the properties above ideal (for reasoning with inconsistency). In what follows we define in exact terms the above properties of ideal logics, investigate known logics in light of these properties, and provide a systematic way of constructing ideal n-valued logics for any natural number n greater than two.

2 Preliminaries

In the sequel, L denotes a propositional language with a set AL of atomic formulas and a set WL of well-formed formulas. We denote the elements of AL by p, q, r (possibly with subscripted indexes), and the elements of WL by ψ, φ, σ. Given a unary connective ⋄ of L, we denote ⋄0ψ = ψ and ⋄iψ = ⋄(⋄i-1ψ) (for i ≥ 1). Sets of formulas in WL are called theories and are denoted by Γ or Δ. Following the usual convention, we shall abbreviate Γ ∪ {ψ} by Γ, ψ. More generally, we shall write Γ, Δ instead of Γ ∪ Δ.

Definition 2.1 A (Tarskian) consequence relation for a language L (a tcr, for short) is a binary relation ⊢ between theories inWL and formulas inWL, satisfying the following three conditions:

Reflexivity :

if ψ ∈ Γ then Γ ⊢ ψ.

Monotonicity :

if Γ ⊢ ψ and Γ ⊆ Γ′ , then Γ′ ⊢ ψ.

Transitivity :

Let ⊢ be a tcr for L.

• ⊢ is structural, if for every uniform L-substitution θ it holds that Γ ⊢ ψ implies θ(Γ) ⊢ θ(ψ). 1
• ⊢ is non-trivial, if there exist some non-empty theory Γ and some formula ψ such that Γ ̸⊢ ψ.
• ⊢ is finitary, if whenever Γ ⊢ ψ, there is a finite theory Γ′ ⊆ Γ such that Γ′ ⊢ ψ.

Definition 2.2 A (propositional) logic is a pair 〈L, ⊢〉, so that L is a propositional language, and ⊢ is a structural, nontrivial, and finitary consequence relation for L.

The most standard semantic way of defining logics is by using the following structures (see, e.g., [Urquhart, 2001]).

Definition 2.3 A (multi-valued) matrix for a language L is a triple M = 〈V, D, O〉, where

• V is a non-empty set of truth values,
• D is a non-empty proper subset of V, consisting of the designated elements of V, 2 and
• O includes an n-ary function ˜⋄M : V n → V for every n-ary connective ⋄ of L.

Let M = 〈V,D,O〉 be a matrix for L. An M-valuation for L is a function ν : WL → V such that for every n-ary connective ⋄ of L and every formulas ψ1, . . . , ψn ∈ WL, ν(⋄(ψ1, . . . , ψn)) = ˜⋄M(ν(ψ1), . . . , ν(ψn)). We denote the set of all the M-valuations by ΛM. A valuation ν ∈ΛM is an M-model of a formula ψ if it belongs to the set modM(ψ) = {ν ∈ ΛM | ν(ψ) ∈ D}. The M-models of a theory Γ are the elements of the set modM(Γ) = ∩ψ∈Γ modM(ψ). A formula ψ is M-satisfiable if modM(ψ) ̸= ∅. A theory Γ is M-satisfiable (or M-consistent) if modM(Γ) ̸= ∅.

Definition 2.4 Given a matrix M, the relation ⊢M that is induced by M, is: Γ ⊢M ψ if modM(Γ) ⊆ modM(ψ). We denote LM = 〈L, ⊢M〉, where M is a matrix for L and ⊢M is the relation induced byM.

Example 2.5

1. Propositional classical logic is induced, e.g., by the twovalued matrix M2 = 〈{t, f}, {t}, {˜∨, ˜∧, ˜¬}〉 with the standard two-valued interpretations for ∨, ∧ and ¬.
2. Priest's LP [Priest, 1989] is induced by the matrix LP = 〈{t, f, ⊤}, {t, ⊤}, {˜∨, ˜∧, ˜¬}〉, where:

Proposition 2.6 [Shoesmith and Smiley, 1971] For every propositional language L and every finite matrix M for L, LM = 〈L, ⊢M〉 is a propositional logic. 3

1 Where θ(Γ) = {θ(γ) | γ ∈ Γ}.

2 We shall denote D = V\D.

3 The non-trivial part in this result is that ⊢M is finitary; It is easy to see that for every matrixM (not necessarily finite), ⊢M is a structural and consistent tcr.

3 Ideal Paraconsistent Logics

We now consider the properties of 'robust' logics for reasoning with inconsistency. First, we define paraconsistency.

Definition 3.1 A logic 〈L, ⊢〉, where L is a language with a unary connective ¬, and ⊢ is a tcr for L, is ¬-paraconsistent, if there are formulas ψ, φ in WL, such that ψ, ¬ψ ̸⊢ φ.

Note 3.2 As ⊢ is structural, it is enough to require in Definition 3.1 that there are atoms p, q such that p, ¬p ̸⊢ q.

3.1 Maximal Paraconsistency

The requirement that a logic will not only be paraconsistent, but also maximal with respect to paraconsistency, is widely considered in the literature and motivated by the aspiration to tolerate inconsistencies but at the same time retain from classical logic as much as possible (see, e.g., [Karpenko, 2000; Marcos, 2005; Carnielli et al., 2007]). This property is defined in [Arieli et al., 2011] as follows:

Definition 3.3 Let L = 〈L, ⊢〉 be a ¬-paraconsistent logic. Then L is maximally paraconsistent, if every logic 〈L, ⊩〉 that properly extends L without changing the language (i.e., ⊢ ⊂ ⊩), is not ¬-paraconsistent.

In what follows we shall say that a matrix M is (maximally) paraconsistent, if so is the logic LM that it induces.

Note 3.4 The notion of maximal paraconsistency given in Definition 3.3 is a strengthening of a weaker notion, according to which L is maximally paraconsistent in the weak sense, if every logic 〈L,⊩〉 that extends L without changing the language (i.e., ⊢ ⊆ ⊩), and whose set of theorems properly includes that of L, is not ¬-paraconsistent. This alternative definition of maximal paraconsistency refers to extending the set of theorems of the underlying logic rather than extending its consequence relation, as in Definition 3.3. Clearly, maximal paraconsistency implies maximal paraconsistency in the weak sense. As shown in [Arieli et al., 2011], the converse does not hold.

3.2 Expressivity

A useful logic must have a reasonable expressive power. As it turns out, maximal paraconsistency by itself is not enough for assuring this. Indeed, as shown in [Arieli et al., 2011], there are maximally paraconsistent logics with a very weak expressive power, such as the three-valued one, whose only connective is Sette's negation [Sette, 1973]. To avoid this, we require a negation connective (with respect to which paraconsistency is defined) that is classically closed, and an implication connective that allows to reduce entailments to theoremhood.

First, we make sure that the negation connective resembles, as much as possible, the one of classical logic.

Definition 3.5 Let L = 〈L, ⊢〉 be a propositional logic for a language L with a unary connective ¬.

• A bivalent ¬-interpretation for L is a function F that associates a two-valued truth-table with each connective of L, such that F(¬) is the classical truth table for negation. We denote by MF the two-valued matrix for L induced by F.

• Given a bivalent ¬-interpretation F for L, we say that L is F-contained in classical logic, if ϕ1, . . . , ϕn ⊢L ψ implies ϕ1, . . . , ϕn ⊢MF ψ.
• L is ¬-contained in classical logic, if it is F-contained in classical logic for some F.

We say that a matrix M is F-contained (¬-contained) in classical logic if so is the logic it induces, LM.

Proposition 3.6 No two-valued paraconsistent matrix is ¬- contained in classical logic.

Proof. Let M = 〈V, D, O〉 be a paraconsistent matrix and let F be a bivalent ¬-interpretation, such that LM is F-contained in classical logic. Since p ̸⊢MF ¬p, also p ̸⊢M ¬p, so there is some t ∈ D, such that ˜¬t ̸∈ D. SinceM is paraconsistent, p, ¬p ̸⊢M q, and so there is some ⊤ ∈ D, such that ˜¬⊤ ∈ D. It follows that there are at least two different elements (t and ⊤) in D. Since D ⊂ V, V must contain at least three truthvalues. ✷

By Definition 3.5, ¬ indeed acts as a negation connective:

Proposition 3.7 Let 〈L, ⊢〉 be a logic that is ¬-contained in classical logic. For every formula ψ: ψ ̸⊢ ¬ψ and ¬ψ ̸⊢ ψ.

We now turn to the other connective:

Definition 3.8 A (primitive or defined) binary connective ⊃ is a proper implication for L = 〈L, ⊢〉, if the classical deduction theorem holds for ⊃ and ⊢ : Γ, ψ ⊢ ϕ iff Γ ⊢ ψ ⊃ ϕ.

By the definition of a bivalent ¬-interpretation F, F(¬) is the classical truth-table. The next proposition shows that this is the case also for a proper implication:

Proposition 3.9 Let L be a logic that is F-contained in classical logic for some F. If ⊃ is a proper implication for L, then F(⊃) is the classical interpretation for implication.

Proof. Let F be a bivalent ¬-interpretation such that L is a logic F-contained in classical logic. Since p ⊢L p and ⊃ is a proper implication, ⊢L p ⊃ p, thus ⊢MF p ⊃ p. HenceMF satisfies t ⊃ t = f ⊃ f = t. Next, also q ⊢L p ⊃ p and so ⊢L q ⊃ (p ⊃ p), thus ⊢MF q ⊃ (p ⊃ p). It follows that MF satisfiers f ⊃ t = t. Finally, p ⊃ q ⊢L p ⊃ q, and again since ⊃ is a proper implication, p ⊃ q, p ⊢L q. Hence, also p ⊃ q, p ⊢MF q, and soMF must satisfy t ⊃ f = f (otherwise, v(p) = t and v(q) = f would be a counter-example). ✷

Definition 3.10 A ¬-paraconsistent logic L is called normal, if it is ¬-contained in classical logic and ⊃ is a proper implication for L.

3.3 Maximal Containment in Classical Logic

As noted in [Avron et al., 2010], maximal paraconsistency of n-valued logics may be easily achieved when all the n values are definable in the language:

Proposition 3.11 Any logic LM of an n-valued matrix M for a language L in which all the n values are definable 4 , is maximal in the strongest possible sense: it has no non-trivial extensions.

4 That is, for every truth value x there is a formula ψx in L, such that for every valuation ν, ν(ψx) = x.

Corollary 3.12 Let LM = 〈L, ⊢M〉 be an n-valued paraconsistent logic, where L is functionally complete for M. 5 Then LM is maximally paraconsistent.

Clearly, the languages of the logics considered in the last proposition and corollary depend on the many-valuedness of the logic, and so these logics are not ¬-contained in classical logic. This shows that maximal paraconsistency can be easily achieved, but on the expense of the aspiration to preserve as much as possible from classical logic. To avoid this, we consider below languages that can be interpreted classically.

Definition 3.13 Let L be a language with a unary connective ¬, and let F be a bivalent ¬-interpretation for L.

• We say that a L-formula ψ is a classical F-tautology, if every two-valued valuation, which for every connective ⋄ of L respects the truth-table F(⋄), satisfies ψ.
• We say that a logic L = 〈L, ⊢〉 is F-complete, if its set of theorems includes all the classical F-tautologies.

Definition 3.14 Let F be a bivalent ¬-interpretation. A logic L = 〈L, ⊢〉 is F-maximal relative to classical logic, if the following conditions hold:

• L is F-contained in classical logic.
• If ψ is a classical F-tautology not provable in L, then by adding ψ to L as a new axiom schema, an F-complete logic is obtained.

We say that L is maximal relative to classical logic, if for some bivalent ¬-interpretation F it holds that L is F-maximal relative to classical logic.

Note 3.15 One could define a stronger notion of maximality relative to classical logic, taking into account extensions of the consequence relation rather than extending only the set of axioms (just as we did in the case of maximal paraconsistency; cf. Definition 3.3 and Note 3.4). That is, it is possible to define a logic L as maximal relative to classical logic in the strong sense, if there is some bivalent ¬-interpretation F for which the following properties hold:

• L is F-contained in classical logic for some bivalent ¬- interpretation F, and
• If Γ ̸⊢L ψ and Γ ⊢MF ψ, then the minimal extension L′ = 〈L, ⊢L′ 〉 of L, so that Γ ⊢L′ ψ, is LF = 〈L, ⊢MF 〉.

However, as the next result shows, as we are interested in normal paraconsistent logics, there is no point in considering this stronger definition of containment in classical logic:

Proposition 3.16 No paraconsistent normal logic is maximal relative to classical logic in the strong sense.

We are now ready to define what we consider to be optimal logics for reasoning with inconsistency.

Definition 3.17 A ¬-paraconsistent logic L is called ideal, if it is normal (i.e., ¬-contained in classical logic and has a proper implication), maximal relative to classical logic, and maximally paraconsistent.

5 That is, every function g : V k →V is representable in L: There is a formula ψg (whose atoms are in {p1, . . . , pk}), such that for every valuation ν it holds that ν(ψg) = g(ν(p1), . . . , ν(pk)).

4 A Systematic Construction of Ideal Logics

A natural question to ask at this point is whether ideal logics do exist. In this section we not only give a positive answer to this question, but also show that for every n > 2 there is an extensive family of n-valued ideal logics, each of which is not equivalent to any k-valued logic with k < n. 6

Proposition 4.1 Let LM = 〈L, ⊢M〉 be a ¬-paraconsistent logic for a language L that includes a unary connective ⋄. Suppose that LM is ¬-contained in classical logic and that for some n > 2 the following conditions are satisfied:

1. p, ¬p ⊢M ⋄n-2p,
2. p, ¬p, ⋄k p ⊢M q, for 1 ≤ k ≤ n-3,
3. p, ¬p, ¬⋄k p ⊢M q, for 1 ≤ k ≤ n-3,
4. p ⊢M ¬¬p.

ThenMhas at least n elements, including at least n-2 nondesignated elements.

Proof. By the proof of Proposition 3.6, there should be at least one element t ∈ D, such that f = ˜¬t ̸∈ D and at least one element ⊤ ∈ D, such that ˜¬⊤ ∈ D. Let ⊥k = ˜⋄k⊤ for 1 ≤ k ≤ n-3. Then ⊥k ∈ D for 1 ≤ k ≤ n-3 (i.e, ⊥k ∈ V\D; otherwise p, ¬p, ⋄k p ̸⊢M q). Moreover, ⊥1, . . . , ⊥n-3 are different from each other, because otherwise we would get that ˜⋄i⊤ ∈ D for every i > 0, and this violates the condition that p, ¬p ⊢M ⋄n-2p. It follows that t,⊤,⊥1, . . . ,⊥n-3 are all different from each other. Now, by Rule (3) above, ˜¬⊥k ∈ D (otherwise the assignment v(p) = ⊤ would contradict this rule). On the other hand, Rule (4) implies that ˜¬f ∈ D. Hence, f is different from ⊥1, . . . ,⊥n-3. Obviously, f is also different from t and ⊤ (since it is in D). It follows that t,⊤, f,⊥1, . . . ,⊥n-3 are all different from each other. ✷

Now we can construct the promised family of ideal nvalued logics:

Theorem 4.2 Let M = 〈V, D, O〉 be an n-valued matrix for a language containing the unary connectives ¬ and ⋄, a binary connective ⊃, and a propositional constant f. Suppose that n > 3, and that the following conditions hold inM:

1. V = {t, f,⊤,⊥1, . . . ,⊥n-3} and D = {t,⊤},
2. the interpretation of the constant f is the element f,
3. ˜¬t = f, ˜¬f = t, and ˜¬x = x otherwise,
4. ˜⋄t = f, ˜⋄f = t, ˜⋄⊤ = ⊥1, ˜⋄⊥i = ⊥i+1 for i < n-3, and ˜⋄⊥n-3 = ⊤,
5. a ˜⊃ b = t if a ̸∈ D and a ˜⊃ b = b otherwise,
6. for every other n-ary connective ⋆ of L, ˜⋆ is classically closed, i.e., whenever a1, . . . , an ∈ {t, f}, also ˜⋆(a1, . . . , an) ∈ {t, f}.

Then LM = 〈L, ⊢M〉 is an ideal n-valued paraconsistent logic that is not equivalent to any k-valued logic with k < n.

Proof. It can be easily checked that all the conditions in Proposition 4.1 are satisfied, so by that proposition, for every matrix M′ with less than n elements, ⊢M ̸= ⊢M′ .

6 By Proposition 3.6 there are no ideal logics for n = 2.

We divide the rest of the proof to several lemmas, showing that LM satisfies all the properties of an ideal paraconsistent logic. In the sequel we shall assume that M is an n-valued matrix satisfying the conditions in the theorem.

Lemma 4.3 LM is a normal ¬-paraconsistent logic.

Proof. Clearly, LM is ¬-paraconsistent. By the definitions of the connectives in L, M is ¬-contained in classical logic. It is also easy to verify that the classical deduction theorem obtains for ⊃ and ⊢M, and so ⊃ is a proper implication. Thus LM is normal. ✷

Lemma 4.4 M is maximally ¬-paraconsistent.

Proof. Note first that for any a ∈ V \ {t, f} there is 0 ≤ ja ≤ n-2, such that a valuation v is a model inMof {⋄ja p, ¬⋄jap} iff v(p) = a (j⊤ = 0 or j⊤ = n-2, and j⊥i = n-2 - i). Let L = 〈L, ⊢L〉 be any proper extension of LM. Then there are some ψ1, . . . , ψk and ϕ, such that ψ1, . . . , ψk ⊢L ϕ, but ψ1, . . . , ψk ̸⊢M ϕ. From the latter it follows that there is a valuation v, such that v(ψi) ∈ D for every 1 ≤ i ≤ k, and v(ϕ) ∈ D. Let p1, . . . , pm be the atoms occurring in {ψ1, . . . , ψk, ϕ}. Since we can substitute the propositional constant f for any p such that v(p) = f, and ¬f for any p such that v(p) = t, we may assume that v(p) is in V \ {t, f} for any atom p. Accordingly, let ji = jv(pi) for 1 ≤ i ≤ m. By the observations above, v is the only model of the set Ψ = ⋃1≤i≤m{⋄ji pi , ¬⋄ji pi}. It follows that Ψ ⊢M ψi for every 1 ≤ i ≤ k, and Ψ ∪ {ϕ} ⊢M q (where q is a new variable). Hence Ψ ⊢L q. Now, by substituting ⋄n-ji-2p for pi (where p is different from q), we can unify Ψ to {⋄n-2p, ¬⋄n-2 p}. But in LM both elements of this set follow from {p, ¬p}. Thus, p, ¬p ⊢L q, and so L is not paraconsistent. ✷

Lemma 4.5 M is maximal relative to classical logic.

Proof outline. Let ϕ be a formula that is not M-valid, and let Δ be the set of instances of ϕ. Suppose for contradiction that there is a classical tautology θ such that Δ ̸⊢M θ. Let Γ be a maximal theory extending Δ, such that Γ ̸⊢M θ. Then for every formula ψ, either ψ ∈ Γ, or Γ, ψ ⊢M θ and so Γ ⊢M ψ ⊃ θ. Now, for any truth value a ∈ V and formula ψ ∈ WL, define formulas φa1 (ψ) and φa2 (ψ) as follows:

Define a valuation ν by: ν(ψ) = a if φa1 (ψ) ∈ Γ and φa2 (ψ) ∈ Γ. It can be verified that ν is a well-defined classical valuation that is a model of Γ but is not a model of θ. Now, since θ is a classical tautology and ν is a classical valuation, necessarily ν(θ) = t, contradicting the fact that ν is not a model of θ. ✷

This concludes the proof of Theorem 4.2.

✷

Example 4.6 Let M = 〈{t, f,⊤,⊥}, {t,⊤},O〉 be a fourvalued matrix for a language L that consists of a propositional constant f, an implication connective ⊃ , defined by:

and the following two unary connectives:

1. Belnap's negation [Belnap, 1977], denoted ¬, in which ˜¬t = f, ˜¬f = t, ˜¬⊤ = ⊤ and ˜¬⊥ = ⊥.

It is east to verify that the connective ⋄ from Theorem 4.2 can be defined by a composition of the two unary connectives above: for all x ∈ {t, f, ⊤, ⊥}, ˜⋄a = ˜¬ ˜-a = ˜- ˜¬a. By Theorem 4.2, LM is an ideal four-valued paraconsistent logic, and it is equivalent to no three-valued logic. Note that the extensions of this logic by the standard (Belnap/Fitting) four-valued conjunction and disjunction, defined by:

are still ideal logics. As shown already in [Arieli and Avron, 1998], these logics provide a very natural framework for reasoning with inconsistent information, and have corresponding cut-free, sound and complete Hilbert-type and Gentzen-type proof systems.

5 The Three-Valued Case

Three-valued semantics is the most popular framework for reasoning with inconsistency. Among other reasons, this is because it is the minimal framework adhering paraconsistent reasoning (recall Proposition 3.6). Below, we study in greater detail ideal logics in this context.

Proposition 5.1 Let M = 〈V, D, O〉 be a three-valued paraconsistent matrix that is ¬-contained in classical logic. Then M is isomorphic to a matrix M′ = 〈{t, f, ⊤}, {t, ⊤}, O〉, in which ˜¬t = f , ˜¬f = t and ˜¬⊤ ∈ {t, ⊤}.

Proof . Let F be a bivalent ¬-interpretation, such that LM is F-contained in classical logic. By the proof of Proposition 3.6, there are t, ⊤ ∈ D, such that f = ˜¬t ̸∈ D and ˜¬⊤ ∈ D. Since |V| = 3, necessarily V = {t, f, ⊤} and D = {t, ⊤}. Now, since p, ¬¬p ̸⊢MF ¬p, also p, ¬¬p ̸⊢M ¬p. Thus, there is a model ν of {p, ¬¬p} that does not satisfy ¬p. For this ν, it holds that ν(p) ∈ D and ν(¬p) ̸∈ D, thus ν(p) = t. Since also ν(¬¬p) ∈ D, we get that ˜¬f = ˜¬ ˜¬t ∈ D, and so ˜¬f ∈ {t,⊤}. Let us now show that ˜¬ ˜¬ ˜¬⊤ ∈ D. If ˜¬⊤ = t, then ˜¬ ˜¬⊤ = ˜¬t = f and ˜¬ ˜¬ ˜¬⊤ = ˜¬f ∈ D. If ˜¬⊤ = ⊤, then ˜¬ ˜¬ ˜¬⊤ = ⊤. Hence ˜¬ ˜¬ ˜¬⊤ ∈ D. Now, since p ̸⊢M ¬¬¬p, necessarily ˜¬ ˜¬ ˜¬t = ˜¬ ˜¬f ̸∈ D, and so ˜¬f ̸= ⊤. It follows that ˜¬f = t. ✷

Interestingly, in the three-valued case, maximal paraconsistency implies maximality relative to classical logic.

Theorem 5.2 Let M be a three-valued matrix that is ¬- contained in classical logic. If LM is maximally paraconsistent then LM is maximally paraconsistent relative to classical logic.

Proof . First, we need the following lemmas:

Lemma 5.3 Let Mbe a three-valued maximally paraconsistent matrix, for which there is some classical ¬-interpretation F, such that LM is F-contained in classical logic, but LM is not F-maximal relative to classical logic. Then the operations of M are classically closed. 7

Lemma 5.4 Let M = 〈V,D,O〉 be a three-valued matrix for L. If M is classically closed, then LM is ¬-contained in classical logic.

Proof of Lemma 5.4. Suppose that M is classically closed. Consider the ¬-interpretation FM(⋄) = ˜⋄M/{t, f}, where ˜⋄M/{t, f} is the reduction of ˜⋄M to {t, f}. Now, let ϕ1, . . . , ϕn, ψ ∈ WL, such that ϕ1, . . . , ϕn ̸⊢MFM ψ. Then there is someMFM -valuation ν, such that ν(ϕi) ∈ D for all 1 ≤ i ≤ n and ν(ψ) ̸∈ D. By the definition of MFM , ν is also an M-valuation, and so ϕ1, . . . , ϕn ̸⊢M ψ. Hence LM is FM-contained in classical logic. ✷

To prove Theorem 5.2, let M be a three-valued matrix that is ¬-contained in classical logic and such that LM is maximally paraconsistent. Then in particular LM is paraconsistent and is F-contained in classical logic for some F.

If LM is F-complete, or if for every classical F-tautology ψ0 not provable in LM, the addition of ψ0 to LM as an axiom results in an F-complete logic, then we are done. Otherwise, by Lemma 5.3, M is classically closed, and by Proposition 5.1, ˜¬t = f and ˜¬f = t. Thus, by Lemma 5.4, LM is FM-contained in classical logic.

We end by showing that LM is FM-maximal relative to classical logic. Let ψ′ be a classical FM-tautology not provable in LM and let Δ′∗ be the set of all of its substitution instances. Let L′∗ be the logic obtained by adding ψ′ as a new axiom to LM. Then for every theory Γ we have that Γ ⊢L′∗ φ iff Γ,Δ′∗ ⊢M φ. In particular, since M is maximally paraconsistent,

Suppose for contradiction that there is some classical FMtautology σ not provable in L′∗ . Since ̸⊢L′∗ σ, also Δ′∗ ̸⊢M σ. Hence, there is a valuation ν ∈ ΛM which is a model of Δ′∗ , but ν(σ) = f. Note that sinceM is a ¬-paraconsistent three-valued matrix, by Proposition 5.1, ⊤ ∈ D and ˜¬⊤∈D. If there is some ψ such that ν(ψ) = ⊤, then since ν is a model of Δ′∗ , it is also a model of Δ′∗ ∪ {ψ, ¬ψ}, and so by (1) above, it is a model of σ, in contradiction to the fact that ν(σ) = f . Otherwise, ν(ψ) ∈ {t, f} for all ψ, and so ν is anMFM -valuation, assigning f to σ, in contradiction to the fact that ⊢MFM σ. Hence, all the classical FM-tautologies are provable in L′∗ , and so LM is FM-maximal relative to classical logic, which implies that it is also maximally paraconsistent relative to classical logic. ✷

Corollary 5.5 Every normal and maximally paraconsistent three-valued logic is ideal.

In order to identify three-valued ideal logics, then, one may incorporate the following criterion, given in [Arieli et al., 2011], for checking maximal paraconsistency.

7 That is, for every n-ary connective, if a1, . . . , an ∈ {t, f}, then also ˜⋄(a1, . . . , an) ∈ {t, f}.

Proposition 5.6 Let M be a three-valued paraconsistent matrix that is ¬-contained in classical logic. Suppose that there is a formula Ψ(p, q) in L such that for all ν ∈ ΛM, ν(Ψ) = t if either ν(p) ̸= ⊤ or ν(q) ̸= ⊤. Then M is maximally ¬-paraconsistent for L.

By Corollary 5.5 and Proposition 5.6, we have, therefore, the following result.

Proposition 5.7 Let M be a three-valued normal paraconsistent matrix. Suppose that there is a formula Ψ(p, q) in L such that for all ν ∈ ΛM, ν(Ψ) = t if either ν(p) ̸= ⊤ or ν(q) ̸= ⊤. Then 〈L, ⊢M〉 is an ideal logic.

Example 5.8 Among the three-valued logics that meet the conditions of Proposition 5.7 (and so they are ideal) are Sette's logic P1 [Sette, 1973] (and all of its fragments containing Sette's negation), the logic PAC [Batens, 1980; Avron, 1991], J3 [D'Ottaviano, 1985], and all the 220 three-valued logics considered in [Arieli et al., 2011] (including the 213 LFIs introduced in [Carnielli et al., 2007]).

The three-valued logic LP [Priest, 1989], considered in Example 2.5, is nevertheless not ideal, since it lacks a proper implication connective. Note that by Proposition 5.6 and by Theorem 5.2 (respectively), LP is both maximally paraconsistent and maximal relative to classical logic. It follows that these two properties (the former of which was investigated in [Avron et al., 2010; Arieli et al., 2011] and the latter is realized in [Carnielli et al., 2007]) are not enuogh for getting an ideal paraconsistent logic.

6 Conclusion

The contribution of this paper is threefold: first, setting up a desiderata list of the properties of useful logics for reasoning with inconsistency, second: identifying known logics (in particular, three-valued ones) that meet these requirements, and third: showing that for any n > 2 there are ideal n-valued logics (and providing a constructive way of defining them).

The diversity of ideal logics for paraconsistent reasoning leaves a lot of room for further considerations in the choice of an appropriate paraconsistent logic for specific needs. Our framework should be regarded, then, as a directive approach on how to choose such a logic, rather than a definite one.

Acknowledgement

This research was supported by The Israel Science Foundation (grant number 280-10).