Contextual Negations and Reasoning with Contradictions

1 Introduction

In some previous work we have defended the idea that any system which tries to formalise reasoning should be able to treat the question of contradiction ( cf. (Carnielli and Lima Marques, 1990] and [Carnielli, 1990]).

A similar point has been raised (more or less indepen­ dently) by several authors, and some solutions involving simple many-valued logics and non-monotonic logics, for example, have already been proposed.

Such solutions, however, fail to consider the difference between local (or contextuaQ inconsistencies, and global inconsistencies.

This is an important point, first because this distinc­ tion is apparently very familiar to real reasoners, and second because by failing to consider these points the existing solutions try to reestablish consistency as soon as contradictions appear, and are thus obliged to main­ tain a costly and cumbersome process of revision.

It is then very natural to consider the possibility of approaching this problem by means of some logic which can support local inconsistencies.

In modal logics, for instance, simultaneous utterances of A is possible and -,A is possible are perfectly accept- Mamede LIMA MARQUES *

·supported by the Alexander von Humboldt Foundation (FRG) and CNPq (Brasil).

fSupported by BRA: (MEDLAR).

*Supported by CAPES (Brasil) and BRA: (MEDLAR).

Universitt! Paul Sabatier-IRIT 118, Route de Narbonne 31062 Toulouse - France

mamedeOirit .fr

able, if we understand possibility as a contextual notion: in this case we are just not referring to the same world.

We want to propose that trueness in certain cases can be interpreted in a similar way: so if our theory has to analyse A is true and -,A is true and the theory is sufficiently prepared, it may regard that discrepancy as an intrinsic difference of context between the two as­ sertions, thus avoiding collapsing and at the same time gaining more information while recognising that differ­ ence of context.

The objectives of this paper are:

1. To propose a new definition of semantics of transla­ tions, in order to give a formal approach to the prob­ lem of characterizing the notion of distinct contexts or situations that affect the truth of a sentence, and
2. In particular, to illustrate how semantics of this sort can be obtained for a certain logic which supports contradictions in the process of reasoning.

In the particular application, we will be using as underlying logics certain three-valued logics (see, e.g. [Ginsberg, 1988], and [Delahaye and Thibau, 1988] for related uses of many-valued logics) .

The method introduced here is general, and can be used for instance in connection to other logics (many­ valued or not). The restriction to three-valued logics, however, is interesting because of the connection with paraconsistent logic.

Paraconsistent logic, in particular the propositional systems C.. (1 :$ n < w) and Cw and their first-order counterparts make it possible to separate inconsistency from triviality in formal systems. The importance of this point in terms of reasoning strategy is discussed in [Carnielli and Lima Marques, 1990].

Although all such paraconsistent systems are known to be sound and complete with respect to semantics of two-valued functions (see e.g. [da Costa, 1974] and [Alves, 1984]) some non-intuitive aspects of those se­ mantics have prevented their applications in automated reasoning.

We show how to obtain a new semantic interpretation for paraconsistent logics in such a way that negation in those logics could be seen as a kind of contextual nega­ tion.

In this way, as we argue, it is possible to obtain a logical framework which gives a quite natural account of the idea of reasoning under contradiction.

2 Translation Semantics

The idea of translation semantics and its applications was introduced in elsewhere ( cf. [Carnielli, 1990]). In this section we give a more general treatment to this notion, refining the appropriate concepts.

Let L be a logic whose language C.(L) has connec­ tives (V, A,-+,--,) and quantifiers ('v', 3). Let also M be another logic whose language C.(M) contains sets of cor­ responding connectives and quantifiers, that is, C.(M) contains sets

We suppose that C.(M) and C.(L) contain all the fa­ miliar logical symbols and that all the usual syntactic definitions hold for them. A situation such as that oc­ curs naturally when M is a many-valued logic, for exam­ ple, where several connectives can be defined. It is usual to classify them as conjunctions, disjunctions, etc., and we use this classification here, assuming only that the sets Sa (where# is in {V,A,--,,-+,3,'v'}) are non-empty if the corresponding {V, A,--,,-+, 3, 'v'} are present in L. Of course each connective and quantifier can be seen as a distinct logical symbol.

We define a translation from L to M as a function T : C.(L) ...-. C.(M) such that:

satisfying the following properties:

where T(A) = {T(X) :X E A} and f:L, FM denote the respective satisfiability relations in L and M.

The indices it to i6 above are fixed in advances or can vary according to prescribed conditions.

For example, the well-known Gentzen translation from classical propositional calculus (PC) to intuitionistic logic (!NT) is given by:

where

In this case there are no quantifiers, and the sets Sa in I NT are all singletons (consequently, the indices it to i6 are all fixed) .

It is clear that our definition includes many distinct translations depending upon the cardinalities of S 1 .

Other properties and examples of translations are given in [Epstein, 1990] .

The cases when M is a many-valued logic are of es­ pecial interest because those logics have semantics de­ scribed by simple algebraic conditions (through logic ma­ trices).

We shall concentrate on the particular case of three­ valued logics, showing that there exists a semantics of translations between the paraconsistent calculus Ct and the three-valued logic LCD containing two negations (all other connectives and quantifiers appearing just one time). In order to render the analysis more intuitive, we can consider two different logics, LD and CD, instead of one single logic LCD containing two negations.

3 Three-valued Logics, Continous and Local Default

Let us consider a fixed language L containing the follow­ ing symbols (as the usual language for first-order theo­ ries):

• (a) primitive connectives: ..., (negation), V (disjunc­ tion), A (conjunction), -+ (implication),
• (b) quantifiers: 'v' (universal), 3 (existential)
• (c) a denumerable stock of variables, constants, func­ tions symbols and predicate symbols.

We denote the collection of all well-formed formulas by Wff and a well-formed formula by wff.

All the usual syntactic definitions such as substitution, etc. (with their usual proviso on variables) hold also here.

We define now the calculus of continuous truth-default CD and the calculus of local truth default LD as three­ valued systems in the language L, whose interpretation is given by the following logical matrices:

1. Logic values: T, F, I, of which T and I are desig­ nated;
2. The connectives A, V, and -+ are interpreted by the following tables:

and the two negations, respectively, in CD and LD are interpreted by the negation of continuous default ...,C, and by the negation of local default ...,l:

and

where T <I< F.

These conditions are sufficient to characterize com­ pletely a many valued logic in terms of syntactic rules for which these tables are sound and complete (see [Carnielli, 1987]).

In order to make clear that we are referring to CD or LD we underline the connectives and quantifiers, and write .,C or .,l for the negations.

We want to argue that the logic values and the matri­ ces for CD and LD can be viewed as a basis for a model of reasoning by default, inspired by suggestions of Ep­ stein in [Epstein, 1990]. For this purpose consider the following interpretation of the logic values:

1. F means definitely false, and thus a sentence A re­ ceives values F only when there is positive evidence of falsehood;
2. Dubie negations are reducible, that is, A and -.-,A receive the same logic value.
3. There cannot be positive evidence of falsehood for both A and -.A.
4. We assume that Tis assigned to A (resp., to -.A) when there is positive evidence of falsehood for -.A (resp., to A) and in this case -,A (resp., to A) re­ ceives value F .
5. We further assume that positive evidence of trueness is not possible; so this implies that a sentence of the form A or -.A receives value T by default when there is positive evidence of the falsehood of the other one; that is, T is the default value, which is assumed to hold if there is no other indication.
6. If it happens that neither A nor -.A have positive evidence of falsehood, we accept that in principle A is not yet determined, thus assigning to it the value I.

We call a 9-valuation for CD (respectively, for lD) any function extended from the atomic sentences to all sentences by these tables. We assume that the reader is familiar with the usual definitions of many-valued struc­ tures A; it is sufficient to know that the routine syntactic and semantic notions can be defined for those logics. In particular, .C(A) stands for the extended language ob­ tained from A by adding new constants as names for all elements of the universe I A I of A. For both systems, the valuations for the quantified case are extended as follows:

if v is 3-valuation then

1. As a final assumption, we agree that positive in­ formation for falsehood of negated sentences may be obtained in the future, but not for positive sen­ tences, i.e. ones not beginning with T (this can be justified, for example, imagining a process of lim­ ited resources, where after a first attempt to find evidence for the positive sentences, we concentrate our efforts on the negative ones).

If we are careful reasoners we should keep track of our deductions made on the basis of I values; we thus assume that any valuation which relates to I is assigned I unless it is granted by some value F: this is clearly guaranteed by the tables for V, 1\ and-+ above, and by the interpretation of the quantifiers.

This explains why we do not define, in the tables for "V" and "-+" TV I = T, IV T = T, I -+ T = T, F -+ I= T. The intuitive idea is that I is the indeterminated value, which can be turned into Tor F in the presence of further information, but also that we want to be able to keep track of all wff's which somehow involve I values.

The reader will notice that, defining TV I= IVT = T, for example (which incidentally would give the relevant system RM3 of relevant logic [Anderson and Belnap, 1975]) would make we too loose this property of keeping track of I values.

As a consequence of our assumptions, it follows that neither T nor F can be changed, but the value I can be changed in the light of future information. There are two possibilities for the course of events of a given sentence A having value I:

• case (a) This situation continues forever, and thus -.A is also evaluated as I; this explains the table for -,C and justifies calling CD a logic for continuous default.
• case (b) As a consequence of assumption (7) above, in a given moment A stops being regarded as I, but gains the status ofT, because new positive information on the falsehood of -.A has been obtained. Thus -.A has to be evaluated as F, and this explains the table for -,l and justifies calling LD a logic for local default.

We want to remark that while LD is a three-valued version of classical logic, CD is a genuinely new system: it does not coincide with any of the well-known three­ valued systems.

We can regard the union (in the obvious sense as sim­ ply a logic in .C(-.L, .,c,V, /\, -+)) LCD of CD and LD as a three-valued logic also, and all the definitions (like 3-valuations, etc.) extend to LCD.

4 Paraconsistent Backgrounds

Paraconsistent logics are formal systems designed to serve as the basis for inconsistent but non-trivial the­ ories, with the additional characteristic of being as con­ servative as possible with respect to the l'ostulates of classical logic. We refer to [da Costa, 1974j and [Alves, 1984] for the axiomatics of cl and its first-order exten­ sion cr.

We are using here the version of [Alves, 1984] where (-.-.A +-+ A) is an axiom.

The semantic interpretation of Cf is described as fol­ lows: if Lis a language of Cf (i.e., the basic alphabet plus a class of function symbols, predicate symbols, variables and constants), we define a structure in the usual way as a nonempty domain I A I plus the interpretations for the elements of L. C(A) as explained above, denotes the extended language. Here i and j denote names.

A paraconsistent valuation based on the structure A is a function ·v from a wff to {t,f} such that:

1. if p* = pa1 ···an then v(p*) = t iff P.A(A( at), ·· ·, A(an)) for p a predicate, P.A its interpretation, ai variable-free terms and A(ai) their interpretations;

where X 0 is defined as -.(X 1\ -.X) for any wff X .

1. if v(N) = v(B 0 ) = t then v((A # B) 0 ) = t for # in {V,A,-}
2. v('v'xA) = t iff v(A.,[i]) = t for all i in .C(A)

1. v(A) = v(A') if A and A' are variants obtained by renaming variables .

Note that from (6) and (7) it follows that v(A) =f. v( -.A) iff v(A 0 ) = t. Thus, in the cases where v(A 0 ) = f we do have v(A) = v( -.A) = t , since clause (6) forbids v(A) = v(-.A) =f.

The proof of completeness given in [Alves, 1984] for Cf (i.e. Cf plus the predicate = for equality) can be modified in minor details to show that Cf is correct and complete with respect to the paraconsistent valuations.

Theorem 4.1 The systems Ct and Cf are not finite many-valued logics.

• Proof : It is sufficient to show that the propositional system C1 is not finite many-valued.

The proof is an adaptation of the proof by GOdel [Godel, 1932] about the non-characterizability of the intuitionistic propositional calculus by many-valued logics, using the following logic matrix M, whose logic values are the ordinals in w + 1 and w the set of distinguished logic values and whose operations V, /\, -., --+ are defined by:

D

The previous theorem shows that paraconsistent logic (at least the systems Ct and Cf and their cognates) can­ not be interpreted as a finite many-valued logic. The relationship between paraconsistent and many-valued logics is, however, much more subtle: we prove that paraconsistent semantics can be characterized by classes of translations involving simultaneously more than one many-valued systems, as explained in section (5).

5 Contradictions and Contextual Negation

A translation between Cf and LCD= CD U LD is a func­ tion T from the language of Cf into the union of the languages of CD and LD such that the following condi­ tions hold (underlined symbols belong to the common language of CD and LD) :

1. For p* an atomic formula:
2. (a) T(p*) = 1?.*· where E.* is an atomic sentence in .C(LCD)

1. For non-atomic formulas

A translation T is called a Cf-translation if it is sub­ jected to the following conditions:

In intuitive terms, the above definitions mean:

• (a) translations of double neighbour negations cannot mix, and
• (b) for the sentences of the form A 0 , if the internal nega­ tion is regarded as continuous default then the ex­ ternal one has to be local default.

Note that a translation will not be determined by the atomic level: thus, for example, all the following formulas can be obtained by distinct translations of -.(-.AV B): ...,c(...,cA VB), ...,c(...,L AV B), -.L(-.cAV B) and ...,L (-....,LA VB) for A, B atomic.

All the above clauses which treat negation make clear that the negation in q is being translated into two dis­ tinct contexts (namely, the distinct negations in LD and CD).

Given a ct-translation T and a 3-valuation v m LCD, we say that (T, v) satisfies a Cf-sentence X iff v(T(X)) E {T, I}; this is denoted in symbols as

The sentence X is said to be valid in the translation T (respectively, valid in the valuation v) if there exists a valuation v (respectively, a translation T) such that (T, v) f= X ; and X is a tautology if it is valid for all translations T and valuations v.

The following theorem can be proved:

Theorem 5.1 Let T be a ct -translation. Then each model (T, v) determines a paraconsistent valuation v such that (T, v) f= A iff v(A) = t, for all wff's A. 0

Now it remains to prove that we can define a 3valuation and an appropriate translation based on para­ consistent valuations.

Theorem 5.2 Each paraconsistent valuation v {based on the structure A) determines a ct-translation model (T,v) such that v(A) = t iff (T,v) f= A, for all sen­ tences A .

• Proof : Let l(A) and v be the given structure and paraconsistent valuation; the proof is carried out by constructing simultaneously a 3-valuation v and a Cf-translation T having the desired property, by induction on the length of formulas:
• For atomic sentences p*, define

and set T(p*) = K_. Then clearly the result holds.

1. For non-atomic cases the proof involves a de­ tailed analyses by cases, defining inductively (on the length of formulas) the required val­ uation v and q-translation T .

0

Theorems (5.1) and (5.2) establish then the proposed translation semantics for ct. This offers a meaning for the negation in ct as a contextual negation: each in­ stance of negation in this logic is interpreted differently according to which logic scenario the reasoner is accept­ ing for this particular instance (namely, CD or LD).

6 Applications

The deep significance of this idea is that we can use the two usual logic values t and f, and almost all the usual logic laws (as guaranteed by the axioms of en.

When contradiction ofthe form v(A) = t and v(...,A) = t occurs, this is interpreted by the system (by virtue of the translation semantics) as a situation where A and ...,A would take the value I, interpreted as a situation caused by each of information. The system is prepared, then, not only to support such a situation, but also to correct it in the light of further information.

We believe that our analysis gives a precise and intu­ itively acceptable account of a theory ofreasoning which supports local inconsistency, with both theoretical and practical interest. As for applications, in [Carnielli and Lima Marques, 1990] we give examples of automated rea­ soners who can, for example, discover a liar in a group interview, or who can handle paradoxes like the Barber's Paradox.

An application of our analysis consists in obtaining a clear account of the method of analysis of contradictions which we have developed in [Carnielli and Lima Mar­ ques, 1990]. We give here a example (the same given in the mentioned paper) of how such ideas can be applied to a controversial investigation:

Suppose that in the course of an investigation there is some information concerning three persons a, {3, -y; the system has to answer who, among a, {3, -y, are the men and who the women, based on the following knowledge, which is possibly incomplete and contradictory:

1. All men are using hats.
2. All persons using earrings are women.
3. Each person is either a man or a woman.
4. "Y is sure not to be using a hat.
5. "Y is using an earring.
6. Either f3 is using an earring or "Y is a man.
7. If "Y is using an earring, then f3 is not.
8. It is sure that no two of a, {3, "Y are women

Note that, according to the analysis of section (3), clauses ( 4) and (8) are the only to be prefixed with F; the remaining clauses are assumed to be true by default.

Using the tableau version of ct developed in [Carnielli and Lima Marques, 1990], where the prefixes T and F are interpreted as it is true that and it is false that re­ spectively, these conditions are formalized as follows:

1. T(Vx(M(x)-+ H(x))
2. T(Vx(E(x)-+ W(x))
3. T(Vx(M(x) V W(x))
4. F(H(-y))
5. T(E(-y))
6. T(E(/3) V M(-y))
7. T(E(-y)-+ -,E(/3))
8. F(W(a) A W(,B)) V (W(a) A W(-y)) V (W(,B) A W(l))

Analysing this set of formulas using the tableau method referred to above, we obtain as a solution the following information:

meaning that:

1. a and f3 are men

2. "Y is a woman and the extra information T(E({J)) and F(E({3) 0 ) convey that {3 is using an earring, but this has to be revised.

These examples show that the system can identify the critical points where contradictions appear, and give a solution taking the critical points into consideration, in accordance with the clauses of the problem.

Problems of this sort and their solutions show the real applicability of the systems supporting contradic­ tion when they are based on an intuitively clear and well founded semantics. Since such semantics, in the way we have studied, are based on the idea of translations, it also suggests the interest about investigating other log­ ics from this point of view.