Journal of Logic, Language, and Information 5: 25-63,1996. @ 1996 Kluwer Academic Publishers. Printed in the Netherlands.
25
Reasoning with Logical Bilattices OFER ARIELI and ARNON AVRON Department of Computer Science,Schoolof Mathematical Sciences,Tel-AvivUniversity, Ramat-Aviv69978, Israel Email: (ofera,aa)@nath.tau.ac.il (Received 31 May 1994; in final form 23 October 1995) The notion of bilattice was introduced by Ginsberg, and further examined by Fitting, as a general framework for many applications. In the present paper we develop proof systems,which correspondto bilattices in an essentialway. For this goal we introduce the notion of logical bilattices. We also show how they can be used for efficient inferences from possibly inconsistentdata. For this we incorporate certain ideas of Kifer and Lozinskii, which happen to suit well the context of our work. The outcome are paraconsistentlogics with a lot of desirableproperties.*
Abstract.
Key words: Substructural logics, relevance logic, many-valued logics, hypersequents
1. Introduction When using multiple-valued logics, it is usual to orderthe truth values in a lattice structure.In most casessuch a partial order intuitively reflects differencesin the “measureof truth” that the lattice elementsare supposedto represent.There exist, however, other intuitive criteria of ordering that might be useful. Another reasonable ordering might reflect, for example, differencesin the amount of knowledge or in the amount of information that each of theseelementsexhibits. Obviously, therefore,theremight be casesin which two partial orders,eachreflecting a different intuitive concept,might be useful. This, for example, has beenthe casewith Bemap’s famousfour-valuedlogic (Belnap, 1977a;Behrap,1977b).Bemap’s logic was generalizedin Ginsberg(1988),whereGinsbergintroducedthenotion of bihttices, which are algebraicstructuresthat containtwo partial orderssimultaneously (seeDefinition 2.1). His motivation was to presenta generalframework for many applications, like truth maintenancesystems and default inferences.The notion was further investigatedand applied for logic programming and otherpurposesby Fitting (1989, 1990a,1990b,1991, 1993, 1994). In all of their applications so far, the role of bilattices was algebraic in nature. In this paper we try to carry bilattices to a new stage in their development by constructingZogics (i.e.: consequencerelations) which are basedon bilattices, as well as correspondingproof systems.For this purposewe have found it useful to introduceandinvestigatethe notion of a logical bilattice. (All the known bilattices which were actually proposed for applications in the literature fall under this * A preliminary version of this paper appearsin Arieli and Avron (1994).
26
OFERARIELIANDARNONAVRON
category). The general logic of these bilattices turned out to have a very nice proof theory. We also show how to use logical bilattices in a more specific way for non-monotonic reasoningand for efficient inferencesfrom inconsistentdata (thesewere, respectively,the original purposesof Belnap and Ginsberg).For this we incorporatecertain ideas from Kifer and Lozinskii (1992). We show (so we believe)that bilattices provide a betterframework for applying theseideasthan the one usedin the original paper. The paperis organizedas follows: In the next sectionwe introduceand investigate the notion of logical bilattice. In Section 3 we investigate(from semantical and proof-theoreticalpoints of view) the generallogic that is naturally associated with them. This logic is monotonic and paraconsistent.In Section 4 we considera refinedconsequencerelation which is shownto be non-monotonic,andvery useful for reasoningin the presenceof inconsistency. 2. Logical 2.1.
Bilattices
BILATTICES-GENERALBACKGROUND
DEFINITION 2.1. A bilattice is a structureB = (B, St, $, 1) such that B is a non empty set containing at least two elements; (B, St), (B, Sk) are complete* lattices; and 1 is a unary operationon B that has the following properties: 1. if a St b, then ya >t yb, 2. if a & b, then la & lb, 3. -la=a.
Following Fitting, we shall use A and V for the lattice operationswhich correspondto
REASONINGWITH LOGICAL BILATI-ICES
27
k
k
Fig. 1. FOUR and NINE
We will denoteby f andby t the leastelementandthe greatestelement(respectively) of B w.r.t It, while I and T will denotethe least elementand the greatest element of B w.r.t Sk.* f, t, I, and T are all different by Lemma 2.5(a) below, and by the fact that a bilattice containsat least two elements. DEFINITION 2.2. A bilattice is called distributive (Ginsberg, 1988) if all the twelve possible distributive laws concerning A, V, 8, and @ hold.** It is called interlaced (Fitting, 1990a)if eachone of A, V, @,and $ is monotonic with respect to both St and I~c. LEMMA 2.3. (Fitting, 1990a)Every distributive bilattice is interlaced. EXAMPLE 2.4. Figures 1 and 2 contain double Hassediagrams of some useful bilattices. In thesediagrams y is an immediate It-successor of z iff y is on the right side of 5, and there is an edgebetween them; similarly, y is an immediate $-successor of 1ciffy is abovez, and thereis an edgebetweenthem. Belnap’sFOUR (Belnap 1977a,1977b),drawn in Figure 1, is the smallestbilattice. It easy to check that FOUR is distributive. Ginsberg’sDEFAULT (Figure 2) was introduced in Ginsberg (1988) as a tool for non-monotonic reasoning.The truth values that have a prefix “d” in their namesare supposedto representvalues of default assumptions(dt = true by default; etc.). It easyto verify that -df = dt; -dt = df; YdT = dT. The negationsof T, t, f, I are identical to that of FOUR (see * I and T could be thought of as representing no information and inconsistent knowledge, re*s*pectively. Znjinitmy laws have also been consideredin the literature (see,e.g., Fitting, 1993, Definition 3.3). In this paper we do not use such laws. They might be more useful when we enter more deeply to quantification theory in the future.
28
OFER
ARIELI
AND
ARNON
AVRON
t Fig. 2.
DEFAULT
Lemma 2.5(a) below). This bilattice is not even interlaced;* NINE (Figure l), on the other hand, is distributive, and it containsthe default values of DEFAULT. In addition,NINE hastwo more truth values,ot andof, where ~of = ot andlot = of. LEMMA 2.5. Let B = (B, it, Sk, -) be a bilattice, and let a, bE B. a) (Ginsberg,1988)l(aAb) = TCLV~; ~(aVb) = -raA~b; ~(u@b) l(U@b)
=
=
TZ@Y~;
la@+.
T-I-ET. Also, lf = t; --it=f; yL=I; b) (Fitting, 1991)If B is interlaced,then: IAT = f;
IVT
=
t; f @L= I; f CD!= T.
DEFINITION 2.6. (Ginsberg,1988)Let (L,I) be a completelattice. The structure L@L=(L x L&,&Y) is definedas follows: (y1,y2)
>t
(a92)
iffy1
2x1
mdY2Im
(YI,Y~)
>l~
(a,x2)
iffy1
2~1
andYAm
LEMMA 2.7. Let (L,<) be a complete lattice. Then: a) (Fitting, 1990a)L@L is an interlacedbilattice. b) (Ginsberg,1988)If L is distributive, then so is LO L. LO L was introduced in Ginsberg (1988), and later examined by Fitting as a general method for constructing bilattices. A truth value (z, y) E L 0 L may intuitively be understoodso that z representsthe amountof belieffor an assertion, and y is the degreeof belief against it.
EXAMPLE 2.8. Denote the standardtwo valued structure {O,l} by TWO. Then FOUR is isomorphic to TWOOlWO. Similarly, NINE is isomorphic to { - 1, 0, 1}
o(-l,O,
1).
t For example, f
>t df=df@
dT.
REASONING
WITH
LOGICAL
29
BILAl-lXES
We conclude this introductory part by consideringanotherbilattice operation, and a correspondingfamily of bilattices: DEFINITION 2.9. (Fitting, 1990b) A con$!&ion, -, is a unary operation on a bilattice B that hasthe following properties: l.ifak-b, 2.ifa&bthen-a&-b, 3. --a=a, 4. -7a=7-
a.*
LEMMA 2.10. (Fitting, 1990b) Let B = (B, St,
= -aA-b;
Also,-f=f;
-t=t;
-(aVb)
= -aV-b;
-l=T;
-(a@b)
= -a@-b;
-(a@b)
= -a@-b.
-T=l.
DEFINITION 2.11. (Fitting, 1994)A bilattice with a conflation is called classical, if for every bE B, bv-Tb=t.* EXAMPLE 2.12. FOUR is a classicalbilattice (where“-” is definedaccordingto Lemma 2.10). Classicalbilattices werepresentedis order to allow analoguesof classicaltautologies. In particular, in classical bilattices it is really the combination -7 that plays the role of classical negation. 2.2.
BIFILTERS AND LOGICALITY
One of the most important componentin a many-valuedlogic is the subsetof the designated truth values.This subsetis usedfor defining validity of formulae and a consequencerelation. Frequently,in analgebraictreatmentof the subject,the setof the designatedvalues forms a filter, or even a prime (ultra-) filter, relative to some naturalorderingof the truth values.Natural analoguesfor bilattices of filters, prime filters, ultrafilters, and set of designatedvalues in general,arethe following: DEFINITION 2.13. a) A bi$Zter of a bilattice B = (B,
c
B, F # B,
* This requirement is not part of Fitting’s original definition. Nevertheless, it is usually assumed when dealing with bilattices that have conflation, and useful for our purposes. ** In the original definition of classical bilattice, Fitting requires that the bilattice would be distributive. This requirement is not essential for the present treatment of such bilattices.
OFECR ARIJ3LI
I
AND
ARNON
AVRON
F
Fig. 3. FIVE
cLVbE3iffUE3Oor bE3 a@bE3iff aE3oorbE3 c) Let B be a bilattice with a conflation. bifilter, and b E 3 iff --b @3.
3 is an uZtrabi.Zter in B, if it is a prime
EXAMPLE 2.14. FOUR and DEFAULT contain exactly one bifilter: {T, t}, which is prime in both, and an ultrabifilter in FOUR. {T, t} is also the only bifilter of FZVE (Figure 3), but it is not prime there: dT V I = t, while dT $3, and I $! 3. NINE contains two bifilters: {T, ot, t}, as well as {T, ot, t, of, dT, dt}; both are prime, but neither is an ultrabifilter. PROPOSITION 2.15. (Basic properties of bihlters) Let 3 be a bifilter of f3; Then: a) 3 is upward-closed w.r.t both It and
REASONING
WITH
LOGICAL
BILATTICES
31
usedin classicallogic. The role which TWO hasamongBooleanalgebrasis taken hereby FOUR: THEOREM 2.17. Let (f?,3) be a logical bilattice. Then there exists a unique homomorphism h : B -+ FOUR, suchthat h(b) E {T, t} iff bci3. Proof. It is immediate that the only function h : a --t FOUR that satisfiesthe condition, and is also an homomorphism w.r.t negation,is the following one: if bE3and TbE3 if bE3and Tb#3
T h(b) Ef
;
ifbqJ3andlbE3
if b$3and lb@3
i I
This entails uniqueness.For existence,note first that h is obviously an homomorphism w.r.t 1. It remainsto showthat it is alsoa homomorphismw.r.t A, V, @, and @. a) The case of A:
1. Supposethat a A b E 3 and -(a A b) E 3. Then a E 3 and b E 3. In addition, T(aAb) ~3, henceTaVlb E 3, and so la E 3 or -b E 3 (since 3 is prime). It follows that {a la C3or{b,lb}E3,henceeitherh(a)=Torh(b)=T. Since both h(a) and a(b) arein{T,t},andTAT=TAt=T,itfollowsthat h(a)Ah(b)=T=h(aAb). 2. If aAbE3but l(aAb) $3, then aE3and bE3, but laVlb@3, and so neither la nor lb are in 3. It follows that h(a) = h(b) = t, so this time h(a)Ah(b)=t=h(aAb).
3. Supposethat aAb$3 andl(aAb) E 3. Then either la E 3 or lb E 3. Assume, e.g.,that laE3. If aq3then h(a)=f and so h(a)Ah(b)=f=h(aAb). If, on the other hand, a E 3, then h(a) = T. In addition b $3 (otherwisewe would haveaAbE3), and so h(b) E {f, I). Since in FOUR TAf = TAI = f, in this caseh(a)Ah(b)=f=h(aAb). 4. Supposethat a A b @3 and -(a Ab) $Z3. Then la $2 3, lb $! 3 and either a @3 or b 6 3. It follows that either h(a) = I or h(b) = 1. Assume, e.g., the former. Since lb # 3, then h(b) E {t, I}. But since IA t = I Al = I, h(a)Ah(b)=l=h(aAb) inthiscase. b) The case of V:
Since aVb=-r(laAlb),
this casefollows from the previous
one. c) The case of @: 1. If a@b E 3 and l(a@b) E 3, then since l(a@b) = la@lb, we have that a, b, la, lb E 3, hence h(a) = h(b) = T, and so h(a)@h(b) = T@T = T = h(a@b).
2. Ifa~bb3~d~(a~b)ft’3,thena~3,b~3,andeither~a~3or~b~3. It follows that both h(a) and h(b) are in {T, t}, and at least one of them is t. hence,h(a)@h(b)=t=h(a@b).
32
OFJ3R ARELI
AND
ARNON
AVRON
3. The casethat a @b@3 and 1 (a @b) E 3 is similar to the previous one. 4. If a@b @3 and l(a@ b) @3 then either a # 3 or b # 3, and also either -G $3 or -tb @3. Assume, e.g., that a $!3. If also wz 4 3, then h(a) = I, and so h(a)~h(b)=I=h(a~b).If,ontheotherhand,~a~3,then~b~3,andso wegetthath(a)=f,andh(b)E{t,I}.SinceinFOURf@t=f@-L=J-, we have againthat h(u)@h(b)=l=h(u@b). d) The case
of B:
1. Assume that a@b E 3 and l(uCE b) E 3. Then a E 3 or b E 3. Assume, e.g., that a E 3, then h(u) E {T, t}. If in addition la E 3, then h(u) = T, and so h(u)@h(b)=T=h(u@b). Otherwise,~bE3,andsoh(b)E{T,f}.Sincein FOUR,T~T=T~~=T~f=t~f=T,wehavethath(a)~h(b)=T=h(a~b). 2, Ifu~b~3and~(u~b)~3,thenu~3orb~3,andneither~unor~bare in 3. It follows that h(u), h(b) are both in (t, I}, and at least on of then is t. Hence,h(u)@h(b)=t=h(a@b). 3. The casethat a@b @3 and -(a@ b) E 3 is similar to the previous one. 4. If a@ b $ 3 and -(a@ b) @3, then a, -KZ,b, -b are all not in 3, and so h(u)=h(b)=I. It follows that h(u)@h(b)=l=h(u@b). q Note: For Boolean algebraswe have, in fact, a weaker theorem:given 2 from a Boolean algebra B, and a filter F C B s.t. 2 $ZF, we have an homomorphism h, : B -tZWO w.r.t 1, A, V s-t. h,(z) $!F( TWO), and h,(y) E F( TWO) for every y E F. In ourcase,the sameh is goodfor all 2. On theotherhand,in Booleanalgebras we have the property that if 2, y E B and z # y, then there is an homomorphism h : B +TWO which separatesthem. This further implies that equalitieswhich hold in TWO arevalid in any Booleanalgebra.Logical bilattices andFOUR, in contrast, do not enjoy this property.Thus,the distributive law ur\( bVc) = (ur\b)v(ur\c) is valid in FOUR, but not in every logical bilattice in general(take, e.g.,DEFAULT). DEFINITION 2.18. An ultralogical bilattice is a pair (D, 3), whereD is a bilattice with a conflation, and 3 is an ultrabifilter on L3. As it follows from Proposition 2.15(c),ultralogical bilattices arenatural extensionsof Fitting’s notion of classicalbilattices.Also, they haveseveralsimilar properties to those of logical bilattices. The next proposition is one such an instance (cf. Theorem 2.17): PROPOSITION 2.19. Let (D, 3) be an ultralogical bilattice. Then there exists a uniquehomomorphism h : x3+FOUR,suchthath(b)~{T,t}iffb~3. Proof. Similar to that of Theorem 2.17. The only extra thing that we need to check is thecaseof conflation.Again, we shall examinethefour possiblecases: 1. h(b)=T+bE3,~bE3+-~b$!3,-~~b@3’~-b#3,-b$3+ h(-b)=I=-h(b).
33
REASONINGWITH LOGICALBILAlTICES
2. h(b)=t+bc3,~b$!3+-~b@3,-~~bE3=k--,-b@3,-bE3=+ h(-b)=t=-h(b). 3. h(b)=f ~b$!3,~b~3~--~b~3,-~~bS;I3+~--b~3,-b~3~ h(-b)=f=-h(b). 4. h(b)=1 + b$.T,lb@3+ -7bE3, -llbE3+ h(-b)=T=-h(b).
l--bE3,
-be3+ q
Since ultralogical bilattices seems to be quite rare,* we shall concentrate in what follows on logical bilattices. Next we discuss the existence of bifilters and prime bifilters, concentrating on an important special case: DEFINITION 2.20. Let B be a bilattice. Define: 0 z&(O) dzf {z 1z rlc t } (designated values of B w.r.t Sk) l Q(B) kf { z 1z >t T } (designated values of B w.r.t
u Dt(S> C 3.
Proof. The first part concerning Z& (0) o f ( a) is obvious. To see that f @DDI,(B) , assume the countrary. Then f & t and so also -f >k 4, which means that t & f, hence f = t. This entails that D contains just one element, but this contradicts the definition of a bilattice. An even simpler argumenet holds for 1. Claim (b) follows immediately from Proposition 2.15. 0 PROPOSITION 2.23. If Q(O) =2&(D), then D,(a) is the smallest bifilter (i.e: it is contained in any other bifilter). Proof. Foreverya,bEB,aAbEDt(D)iffaAb>tT,iffa>tTandb>tT,iff a E Z&(a) and b E DDt(B). Similarly, a@b E Z&(O) iff a E Dk(Z3) and b E Dh(B). Hence, if Z& (a) = Dt(B) then D)~c(a) is a bifilter of f?. That Z& (B) is the srrdest bifilter in this case follows from Proposition 2.22(b). 0 * Even NINE with either one of its two prime bifilters is not ultralogical bilattice.
34
OFJ3R ARIELI
AND
ARNON
AVRON
PROPOSITION 2.25. Let a be an interlacedbilattice. Then: a) Dk(Q =WB>. b) {b, 4) &D(B) iff b = T. Proof. Supposethat B is interlaced.Then: a) bztT =s bAT=T + bAT>kt =$ bV(bAT)>kbVt + bkkt. Similarly, b>kt + b@t=t + b@t>tT +- b@(b@t)>tb@T + b>tT.Hence Dk(a>=Dt(@
If b = T, then b = lb = T >k t, hence {b, Tb} E ?&(a). The other direction: if {b,~b}E~k(~),thenbLktand~b~kt,hanceb~r,tandb=~~b~k~t=f,and so b >k:t@,f = T (seeLemma 2.5(b)). But T is the greatestelementw.r.t Sk, hence b=T. 0
b)
COROLLARY 2.26. For every interlacedbilattice D, (f3) is defined(In particular, (L OL) is definedfor every completelattice L). Proof. Follows from section (a) of the last proposition, and from Proposition 2.23. cl From the last corollary it follows that if B is interlaced, then (a) is a logical bilattice iff D(a) is prime. In fact, (23)is logical bilattice in all the exampleswhich were actually usedin the literature for constructivepurposes.This is true even for (DEFA ULT), although it is not interlaced. (FfTrE), in contrast,is not a logical bilattice. We next provide a sufficient andnecessaryconditionsfor ZJ(B) to beprime in a particularly important case.It will follow that logical bilattices are very common, andeasily constructed: PROPOSITION 2.27. If L is a complete lattice, then (LO L) is a logical bilattice iff sup(L) is joinirreducible (i.e.: if d/b = sup(L), then a=sup(L) or b=sup(L)). Proof. Denotethe suprimum of L by VL. Then: (+=) Assumethat VL is join irreducible.Since L@L is interlaced,thenby Corollary 2.26, D(L@L) is a bifilter. It remainsto show that it is also aprime bifilter. Indeed, (zl,z2)V(yl,yz)EZ)(LOLL)
~~~(~~VLY~,Z~ALY~)E~(LOL)
iffhV~w)=V~
(see Example 2.21(e)), iff ~1 = VL or y1 = VL, iff (~1,22) E D(L 0 L) or (~~,TJ~)ED(L@L). Theproofinthe caseof @is similar. (+) Assume that LO L is prime, and that XV y = VL for x, y E L. Take arbitrary z EL. Then, (x, z)V(y, z) = (xVy, z) = (VL, z) E D(LOL), hence(x, x) E D(L@L) or (y, z) E D(L@L). It follows that z = VL or y = VL (by Example 2.21(e)again). q
COROLLARY 2.28. a) (FOUR) (= ({O,l}O{O, 1))) and (NINE) (= ({-l,O, l}@{-l,O,l)>) both logical bilattices.
are
35
REASONINGWITHLOGICALBILATITCES
b) More generally, if L is a chain, or if sup(L) has a unique predecessor, then (LO L) is a logical bilattice. 3. The Basic Logic of Logical 3.1.
Bilattices
SYNTAXAND~EMANTICS
We shall first treat the propositional
case.
DEFINITION 3.1. a) The language BL (Bilattice-based Language) is the standard propositional language over {A, V, l,@, CD}. b) BL- is BL together with a unary connective, -, for conflation. c) BL(4) (BL-(4)) is BL (BL-) enriched with the propositional constants {f, t, J-9 T). d) Let (D, F) be a logical bilattice. BL(B) is BL enriched with a propositional constant for each element in B. We shall usually employ the same symbol and name for each b E B and its corresponding propositional constant. Given a bilattice 23 = (B, Lt, Sk, -), perhaps with conflation, the semantic notion of a valuation in B for sentences in BL(B) is defined in the obvious way. The associated logics are also defined in the most natural way: DEFINITION 3.2. a) Let (a, F) be a logical bilattice. F +BL(B,F) A (where I’, A are finite sets of formulae in BL(B)) iff for every valuation u such that v($J) E F for every $ E l?, there exists some C$E A such that V( 4) E F as well. b) Suppose that all the sentences in I’UA are in the language BL (resp. in BL(4)). Then r +BL A (rev. r h(4) A>, iff r ~=BL(B,F) A for every (6 F). Two important
properties of +BL are given in the following
proposition:
PROPOSITION 3.3. a) ~BL has no tautologies. b) ~BL is paraconsistent: p, up ~BL Q. Proof. a) Let $ be any sentence in BL, and suppose that v is a valuation (in FOUR, say) that assigns all the propositional variables in +!Jthe value 1. Then Y($) = I as well, so $ is not valid. 0 b) Set, e.g., v(p) = T and v(q) = f. Note that the first part of the last proposition fails in BL(4), since both t and T are valid. Our next theorem is an easy consequence of Theorem 2.17. It shows that in order to check consequence in any logical bilattice, it is sufficient to check it in (FOUR).
36
OFER
ARIELI
AND
ARNON
AVRON
THEOREM 3.4. Let P and A be finite sets of formulae in BL (in BL(4)). Then r I=ELA t?’h(4) A> iff r I==(FouR) A.* Proof. One direction is trivial. For the other, supposethat for some logical bilattice (B, 3), I’ pBL(B,7) A, where I, A in BL(4). Let v be an assignmentin B such that v($J)E 3 if $ E P, and .v($) @3 if $JE A. Then hov, where h is the homomorphism definedin Theorem2.17, is easily seento be a valuation in FOUR with the sameproperties,hencel? ptFoUR) A. cl The next proposition,which provides a semi-CNF for formulae, will be needed later. PROPOSITION 3.5. Let (B, 3) be a logical bilattice. For every sentence+ in BL(f3) one can construct a sentence$J’, so that $’ is a A-conjunction of Vdisjunction of literals, and for every v over B, v($) E 3 iff v(@) E 3. If 1c,is in BL(4) then the same$J’is good for every logical bilattice (f3,3). Proof. From the propertiesof negationit is obvious that for every sentence$J we can find a sentenceJ/J’in a negationnormal form (i.e. in $’ the negationprecedes only propositional variables), s.t. v($J)= v($‘) for every valuation u. It suffices, therefore,to prove the proposition for sentencesin a negationnormal form. This is doneby an induction on the numberof operationsin $ (negationexcluded):the case where$Jis literal is obvious. If G = $1Ar,l~zor + = $1@B/Q,take $J’= ${ A$& Then for every V, v($J)E 3 iff ~($1) E 3 and ~($2) E 3, iff v($J{)E 3 andv(&) E 3, iff v($~{r\&)E3, iff ~(@)~3.Finally, supposethat$=+rV& or+=&@&.Let $i = ?+b’iA$‘TA. . .A$‘;” and $I2 = @‘~A@~/\. . .A?,b’F (where $J’:are V-disjunction of literals). Let $J’= l\15i5n,l
1. $ and $J’ above are not equivalent, i.e: there may be some valuation Y, s.t. v($J)# v($‘). All the proposition claims is that y!~and $’ aretrue with respect to the samevaluations.* 2. We could, of course,use@and @(or @and V, etc.) insteadof A and V, without any changein the proof.
* There is a related, weaker theorem (10.5) in Fitting (1994). ** The situation is in some senseanalogous to that of Skolemizing and satisfiability in first order classicallogic; The Skolemized version of a sentenceis satisfiable iff the original sentenceis satisfiable, but the two sentencesare not equivalent.
REASONING
3.2.
WITH
PROOF
LOGICAL
BILAlTICES
37
THEORY
Since +BL doesnot have valid formulae, it cannothave a Hilbert-type representation. However, there is a nice Gentzen-typeformulation, which we shall call GBL (GBL(4)):
The System GBL: Axioms: r,ti *$,A Rules: Exchange,Contraction,andthe following logical rules:
[” *I
r,?J=+a
r,q5*n
r,ti”4=+A
In GBL(4) the following axioms arealso included:
38
OFER
r,-L+-n
ARIELI
AND
ARNON
AVRON
r+A,T
The positive rules for A and @are identical. Both behaveas classicalconjunction. The difference is with respect to the negations of p A q and p@ q. Unlike the conjunction of classical logic, the negation of p@q is equivalent to up@ -4. This follows from the fact that p & q iff up & 14. The differencebetweenV and @ is similar. DEFINITION 3.6. A follows provablein GBL.
from I in GBL (notation: I t-G& A) if I + A is
THEOREM 3.7. a) (soundness und completeness)r +BL A iff r kGBLA. b)(CutEZimination)Ifrl~~~~Al,~andr2,~ ~~~~A2,thenrl,r2~~~~Al,A2. Proof. The soundnesspart is easy,andis left to the reader.We prove completenessand cut-elimination togetherby showing that if l?+ A hasno cut-free proof then l? FBL A. The proof is by an induction on the complexity of the sequent
r+n: The basestep: Supposethat I’ + A consists only of literals. If l? and A have a literal in common then I + A is obviously valid (and is provable without cut), while if I’ andA haveno literal in common, then considerthe following assignment
l
v in FOUR: T
v(p) dzf It i f
ifbothpandTpa.reinI ifbothpandlpareinA if(pEI’and~p$T)or(p$?Aand~pEA) if(p$ZI’andlpEI’)or(pEAandYp@A)
Obviously, this is a well defined valuation, which gives all the literals in I’ values in {T, t}, and all the literals in A values in {I, f }. Hence v refutes l? + A in (FOUR). Hence,I’ ~BLA. l The induction step: The crucial observationis that all the rules of the systemGBL arereversible,both semantically andproof-theoretically(a direct demonstrationin the proof-theoreticalcaserequires cuts). There are many casesto considerhere. We shall treat in detail only the casein which a sentenceof the form $ A 4 is in I’ U A. Before doing so we note that the casein which a sentenceof the form -T+!J belongsto l? U A should be split into the subcases$ = ~4, $ = 41A&, etc. (The casein which $ = up wherep is atomic was alreadytakencareof in the basestep). (i) Supposethat $JA 4 E I, i.e.: I = I”, T/JA 4. Considerthe sequentI”, $, 4 + A.
REASONING
WITH
LOGICAL
BILA-ITCES
39
By induction hypothesis,either I”, $J,4 + A is provable without a cut (and then I”, $A$ + A is provable without cut, using [A +I), or elsethereis a valuation that refutesI”, +, #J+ A. In the latter casethe samevaluation refutes I”, $ A 4 + A as well. (ii) Supposethat ?,!J A 4 E A, i.e.: A = A’, $A@ Consider the sequentsr + A’, ~,J.J and I’ + A’, 4. Again, either both have cut-freeproofs, and then l?+ A’, $A#Jalso hasa proof without a cut (using [=x A]), or thereis an assignmentthat refuteseither 0 sequent,and the sameassignmentrefutesl?+ A’, $)r\d as well. Notes:
1. It is obvious from the proof that we can delete contraction from the list of the rules, and restrict the axioms to the casethat l?, A, V/J,and 4 contains only literals. 2. The {A, V, -} fragment of GBL was called “the basic {A, V, -} system” in Avron (1991a), and was introduced there following a different motivation. It had generally been known as the system of “first degreeentailments” in relevancelogic (seeAnderson, 1975;Dunn, 1986),sinceit is well known that ) &, is provable in it, iff $1A . . . /\$I~ + c#qV . . . V& is @l,..,&I. *ch,*-* provablein the systemR (or E) of AndersonandBelnap, iff v(QqA. . . A&) It v(qlqv... V&) for every valuation v in FOUR. It is not difficult to show that this fragment of GBL is valid in any distributive lattice with an involution (“valid” - in the sensethat $1, . . . , gin + 41, . . . ) & is provable in GBL if +,h)A ..- A+h.> It @I) V . . . V ~(4~) for every valuation v). Hence we have an alternative soundnessand completenesstheorem relative to these structures. 3. In Avron (1991b)it is shown that if we add r, -$J, $ + A as an axiom to the h v, -1 (or {A, V, 1) f, t}) fragment of GBL, we get a soundand complete system for Kleene 3-valued logic, while if we add l? + A, +, -$ we get one of the basic three-valuedparaconsistentlogics (Also known as basic J3 - see,e.g., ChapterIX of Epstein (1990) as well as d’ottaviano and da-Costa (1970), d’ottaviano (1985), Avron (1986) and Rozoner (1989)). By adding both axioms, we get classical logic. 4. In order to add a conflation to GBS oneneedsto expandit with additional rules for the left and right combination of - with A, V, 63, ~33and - (10 new rules altogether).These rules are the duals of the correspondingrules of negation. For example, IT,-?)+A r,-+=+-a -+, -A * A [--A4 r,r,-($ [-@=+-I A 4) * A r, -($ @ $1 * A In addition, one should add four more rules for the combination of negation and conflation:
OFER
ARIELI
AND
ARNON
AVRON
Using Theorem 2.19 it is straightforwardto extendthe proof of Theorem 3.7 to the caseof ultralogical bilattices and the resulting systems.Note that in the presenceof conflation we do have provable sequentsof the form r =+ and
=+-A. 5. In orderto get a soundand completesystemfor EL(B) for any logical bilattice Z3,we have to add axioms to GBL for every b E B, accordingto the homomorphism h of Theorem 2.17. For example, if for some b E B h(b) = t, then we addI’+A,bandl?,lb+A. For the single-conclusionedfragment of ~BL we have a strongerresult: DEFINITION 3.8. GBLr (In&&on&k G&C) is the systemobtainedfrom GBL by allowing a sequentto haveexactly oozeformula to the r.h.sof +, and by replacing the rules which have more than one formula on their r.h.s (or empty r.h.s) by the correspondingintuitionistic rules. GBL1(4) is definedsimilarly.* For example,in GBLI, [+
V]
is replacedwith the following two rules:
In caseof BL(4), all the axioms of the form b + (where b E u, ‘6 J-, -1 replacedby b + T/Jfor arbitrary $J.
-1)are
THEOREM 3.9. l?+B& iff l?k GBL~$. A similar result holds for BL(4). Proof. We startwith two lemmas: LEMMA 3.9a: Supposethat I-GBL??+ A, where A is not empty, and r consists only of literals. Then ~-GBL~ I’ + 7L,for some $Jin A (note that if A is empty, then I-GBL~r =+Q for every +). ProofofLemma 3.9~ By an easyinduction on the length of a cut-freeproof of I’ + A in GBL: It is trivial in the casewhere l?+ A is an axiom. For the induction stepwe usethe fact that since l? consistsof literals, all the rules employed arer.h.s rules. We will prove the caseof the rules for V as an example: l Supposethat A = A', 4Vr and l?+ A was inferred from r + A’, 4,~. By induction hypothesiseither ~GBL~l? + 4, or I-GBL~l? +- 7, or ~GBL~l? + $, for some 11,E A’. In the third casewe aredone,while in the first two we infer I-GBL~l’ + 4~7 * Note that 1-G + 11,obtains in both new systems,so the analogy with intuitionistic logic is not perfect.
REASONING
WITH
LOGICAL
BILATTICES
41
using the intuitionistic rules for introduction of V. and r + A was inferred from l? + A’, 14 and l Supposethat A = A’, T(c$VT) r =%A’, 77. By induction hypothesis either i-GBLr r =$ r,!~,for some $JE A’, in which casewe are done, or both t-G&’ r + -4 and J-GEL1 r + -v. In this case, l?=+--( 4 v r) follows immediately by [=+--VI. LEMMA 3.9b: For every l? there exist setsl?; (i = 1 . . . n) s.t: 1. For every i, r; consistsof literals. 2. For every A, ~GBLr + A iff for every i, t-GBLri + A. 3. For every A thereis a cut-freeproof of r + A from I’i + A (i = 1. . . n), where A is the r.h.sof all the sequentsinvolved, and the only rules usedare1.h.srules. Proof of Lemma 3.9b: By induction on the complexity of I’, using the fact that all the 1.h.srules of GBL are reversible, and their active formulae belong to the 1.h.sof the premises. Proof of Theorem 3.9: Assume that ~-GBL r * 7).Then !-GBLri * + for the ri's given in Lemma 3.9b. Lemma 3.9aimplies, then, that kGj3Lrri + 11,(i = 1 . . . n). Thethirdpropertyofrt,... r, in Lemma 3.9b implies that t-GBL1r a T/J,since GBLI and GBL have the same1.h.srules. 0 Notice that the last theorem is still true if we add r, $, -t/j + A to the axioms of GBL, and r, $, + + (pto the axioms of GBLI. In contrast,the theoremfails if we add l? + A, +, 1tJ as an axiom, or the classical introduction rules of 7, or implication with the classicalrules.That is why classicallogic is not a conservative extension of intuition&tic logic. This is also the reason why the theorem fails for the conservativeextension of GBL with the implication we introduce in the forthcoming sections. We end this subsectionwith two other fundamentalpropertiesof ~BL: THEOREM 3.10. (Monotonicity and Compactness) Let I’, A be arbitrary setsof formulae in BL (possibly infinite). Define I’ ~=BLA exactly as in the finite case. Then l? +BL A iff there exist firtite sets I”, A' such that I” 2 l?, A’ C_A, and r'bBLA' (iff t-GnLr'+A'). Proof. Supposethat I’, A are sets for which no such I”, A’ exist. Construct a refuting v in FOUR as follows: first, extend the pair (I, A) to a maximal pair (I’*, A*) with the same property. Then, for any V/J,either 11,E I’* or $J E A* (Otherwise, (I’* U {$J}, A*) and (l?*, A* U {V/J})do not have the property, and so there are finite l?’ C l?*, and A’ c A* suchthat I”, ?I,~BL A’ and there are finite I?’ c I’*, and A” C A* suchthat r” kBL $J,A”. It follows that l?uP kBL A’uA”, contradicting the definition of (I’*, A*)). Define v from the set of all sentencesto FOUR as follows:
42
OFER
T
v($Q dAf ; i
I
if +GI’* if$EE* if $EA* if$EA*
ARIELI
AND
ARNON
AVRON
and+GE* and+EA* and +,I’* and+EA*
Obviously, v($) E D(FOUR) for all $ E I’*, while v(G) $!D(FOUR) if $ E A*. It remains to show that v is indeeda valuation (i.e. it respectsthe operations).We will prove the caseof A, leaving the other casesto the reader.For this, we first note the following facts: 1. If1C,EA*or4EA*,then+A4EA* (SinCe$r\$~BL?J!Jand$JA$+BL$,$‘A#cannotbeinF*) 2. If$Er*,then$A+Er* (~A*)iffb~I’@ (~A*).Similarly,If4~I’*,then + A ~EI? @A*) iff @X’*(EA*). (Supposethat G E I’*. If also 4 E I*, then $ A 4 cannot be in A*, since ?,!J, 4 +BL v,!JA~, So $JA~ E I?* as well. If, on the other hand, 4 E A*, then also @Ad E A*, by UN. 3. If +EI’* or +EI’*, then -($J’Ac$)E~* (similarto(1)). 4. If -$J E A* then -($Ad) E A* iff -4 E A* (similar to (2)). Using (l)-(4), it is straightforwardto check that v($A+) = v($J)Av($) for every $,, 4. For example, if v($J) = f then $ E A* and -$ E I’*, thus, by (1) and (3), ?+!JAc$EA*and-(+A4)EI’*. Hencev($A4)=f=v(+)Av(4) inthiscase.The 0 other casesarehandledsimilarly. THEOREM 3.11, (Interpolation) Supposethat II, I2 =+ A,, A2 is provable in BL(4). Then thereexistsa sentence$ suchthat both l?l + Al, + and$, l?z =+ A2 areprovable in BL (4)) and $Jcontainsonly atomic formulae which are common to rl +- A, andto r2 =F AZ. In particular, $J+ $ iff $ and 4 have an interpolant. Proof. By Maehera’smethod (seeTaukeuti, 1975,Chapter1). 0
3.3. THE SYMMETRIC CONSEQUENCE RELATION The consequencerelation, /=BL, as definedabove,meetsthe symmetry conditions for 1, A, V as defined in Avron (1991b).It follows from the discussiontherethat it is possible to define an associatedsymmetric consequencerelation, +LL, for which Proposition 3.13 below will be valid: DEFINITION 3.12. The symmetric version, &, $Jl,***
of FBL, is defined as follows:
,hJ=~L~l,...,~mif:
a)foreVery1~j
b)foreveryl
PROPOSITION 3.13. &
~m~~7&~BL7$%~
hasthe following properties:
REASONING
WITH
LOGICAL
BILA’ITICES
43
a) & is a consequencerelation in the extendedsenseof Avron (1991a, 1991b). In otherwords: $ & $ for everyformula $, and if I?1k&Al, ?I,andl?2,II, & A2 (where rt , l?2,A, and A2 are multisets of formulae) then rt, I?2+kL At, AZ.
b)If r +;L6 thenr +BL$. c) -, is an internal negationwith respectto +gL, i.e.: r /=& $+ A iff r, -ti I=& A, and I’, $ & A iff II’ & +, A.
d) EL
is the maximal single-conclusionedconsequencerelation having properties
W-W. e) A and V are, respectively, combining conjunction and disjunction for &: I? & $ A c$,A iff I? & $, A and I? & 4, A. Similarly, r, $ v 4 +gL A iff Wd=~LAanWd4=~LA. f) +BL and F&L havethe samelogical theorems.In otherwords,for any +, +BL $ iff &Q’.* g) From II, & 4 and4 &$ it follows that G(q) b.sjLG(4) andG(4) & for every scheme0 (The proof is by induction on the complexity of 0).
G($>
Notes: 1. Similar symmetric versions, with similar properties,can be given, of course, to the other consequencerelations definedin the previous section. 2. The converse of property (b) above does not hold (unless r is empty, as in property (f)). Thus, p, Q +BL p but p, Q kgL p (which shows also that is non-monotonic).Hence the single-conclusionedfragment of F&L is EL strictly weaker then that of +BL. Thus, /=kL can be used to expressstronger connectionsthan thoseallowed by +BL. 3. Both weakeningandcontractionfail for &. We havealreadyseenanexample for the failure of weakening.As for contraction,we notethat kgL -$ Vq, -qb V This demonstratesgreat similarity with linear logic $7 but l+kL 3 v $.” (Girard, 1987). In fact, 1 behavesexactly as linear negation,while A and V correspondsto the “additives” of linear logic. In the next subsectionwe will introduceconnectiveswhich correspondto the “multiplicatives” of linear logic as well. On the other hand, thereis nothing in linear logic which corresponds to either @ or @.$ * For the case of ~BL, but not FBL(~), this holds in fact vacuously. The situation is different, though, for the stronger language introduced below. ** This can directly be seenfrom the definition of b”BL. It can also be inferred from 3.13(b), using only the fact that ~BL +V+. z Clearly not the connectiveswhich have the same notations in Girard (1987)!
44 4.
OFER
ARIELI
AND
ARNON
AVRON
Property (g) above fails for km. Thus, pVq +BLp@q, and pC%q +~3..pVq, but +p@q) ~BL+W& M oreover, for the implication > we introduce in the next section, we have that p > p /=BL q > q and q > q kBL p > p, while ~(p > p) ~BL -(q > q). For the fragment of (1, A, V} we do have (g) as an admissible rule. In other words, if $ and C$are in this fragment, and it is actually the case that $ +BL 4 and 4 kBL +, then O($) +BL O(4). This follows (using induction on the complexity of 0) from the fact that for such$ and 4, if $ +BL 4 then T$ +BL -$. However, this rule is not derivable: from 1c,+ q5and I$+ Q one cannotinfer in GBL T$ + -4.
3.4. 3.4.1.
IMPLICATION
Comcrwm
Weak Implication
As we have noted, +.BL and k&L correspondto different degreesof entailment betweenpremisesandconclusions.Being consequencerelationsthey can be used, however,only as separatedframeworksfor making conclusions.It would be much more convenientto be able to treat them within one framework. For this we need appropriateimplication connectives, which would correspondto thoseconsequence relations. In general,the existenceof an appropriateimplication connective is a major requirement for a logic. First of all, it allows us to reduce questions of deducibility to questionsof theoremhood,and to expressthe various consequence relations among sentencesby other sentencesof the language.Moreover, higher order rules (like: “if ?I,entails 4 then not-4 entails that not-$“) can be expressed only if we have a correspondingimplication in our disposal. If more than one consequencerelation is relevant,the useof correspondingimplication connectives allow us also to expresshigher-orderconnectionsamong thoserelations. Unfortunately, the language BL, rich as it is, lacks an appropriate general implication connectives(this is clear from the fact that it has no tautologies).We can try to use -$ V 4 as expressingimplication of 4 by II, (henceforthwe shall useu for this connective),but this is not adequate,sinceboth modus ponensand the deductiontheorem fail for this connective.The natural thing to do, therefore, is to enrich the languageof BL so that this problem will be eliminated. Again, Avron (1991b) provides a clue how to get implication connectivesthat correspond to both +BL and +kL, by adding only one connective. What we need is an internal implication, 1, for +BL, which satisfies the symmetry conditions for implication: -
~,$'+BL$,A~~~+BL$'>~,A. Ifr,~,,l~~BLAthenr,l(~>~)~~~A.
-
Ifr~BL~',Aandr~BL~~,A,thenr~BLl(~'>),A.
These conditions can easily be translatedinto rules of a sequentialcalculus. Therefore,it is easierto startby extendingthe languageandthe proof system,then to look for an appropriatesemantics.
REASONING
WITH
LOGICAL
45
BILATTTCES
DEFINITION 3.14. are the extensions of the various languagesdefined abovewith the connective >. is obtained from GBL (GBL(4)) by the additions of the b) GBb G=,(4)) following rules:
a) BL3, G(4),
B&(B)
c) l?FGBL, A iff I =$ A is provable in GBL,. We turn now to the semanticsof >: DEFINITION 3.15. a) Given a logical bilatice (8,3), the operation> is definedas follows:* b t
a>b%f
ifaE3 if a@3
b) Using part (a), the consequencerelation ~BL (kBL14)) is extendedto ~BL, ( +.BL, c4))in the languageBL, (BL, (4)) in the obvious way. PROPOSITION 3.16. Both modus ponensandthe deductiontheoremarevalid for 1
in
k=BL>
(i=BL,(4))*
Proof. Easy, andis left to the reader.
0
3.17. Theorem 2.17 is still valid when > is allowed: if (23,3) is a logical bilattice, then there exists a unique homomorphism (relative to 1, A, V, I%,@,and 1) h : B + FOUR, s.t. h(b) E {T, t} iff bE3. Proof. Almost identical to that of Theorem 2.17. We only haveto check that h as defined there is an homomorphism w.r.t > also. Well, if a E 3, then a > b = b, so h(a > b) = h(b) = h(a) > h(b), since h(a) E {T, t} when a E 3. On the other hand, if a @3, then a > b = t and so h(a > b) = h(t) = t. But since in this case h(a) E {I, f}, then h(a) > h(b) is also t, no matter what h(b) is. 0 PROPOSITION
3.18. Let I’ and A be finite sets of formulae in BL (in BL(4)).
PROPOSITION menrkBL3
A
#BL3(4)A>
iff+(FOUR)
A.
Proof. Identical to the proof of Theorem 3.4, using the previous proposition
insteadof Theorem 2.17. * Note that unlike the operations we delt with so far, > is defined onZy for Zogicul bilattices.
cl
46
OFERARIELI AND ARNONAVRON
Note: In contrastto Theorem 3.4, Proposition 3.5 fails for BL,. Thus, p > p is always valid (i.e.: always hasa value in 3), while the languageof (1, A, V, 18, CD} containsno such formula. The sameargumentshows also the following proposition:
PROPOSITION 3.19. BL3 is a proper extensionof BL. THEOREM 3.20. a) (Soundness, Completeness) I’ ~BL> A iff I FGBL, A (similarly for GBL, (4)).* b) The Cut Elimination Theorem is valid for GBL, and for GBL,(4). ProoJ Soundnessis easy,and is again left to the reader.The combined proof of completenessand cut-elimination is identical to that in the caseof +EL (Theorem 3.7). We only have to check that all the rules of > are again reversible,both proof theoretically and semantically.We do this herefor the caseof [l >+I: First, we observethat it is easyto show that $,, -4 + -($ > 4) is provable, and so it is valid (by soundness).Hence, if I’, l(+ > 4) + A is valid (provable),then a cut (which is a valid rule) with $J,-q5=+--($J > 4) gives that I’, $J,-4=%-A is alsovalid (provable). 0 COROLLARY 3.21e a) GBL, is a conservativeextensionof GBL. b) GBL, is still paraconsistent. c) The {A, V, >}-part of ~BL, is identical of that of classical logic. Proof.
a) This is direct implication of cut-elimination. It also a corollary of the soundness and completenessresults for both. b) We still have that p, up ~GBL, q. c) The {A, V, >}-part of GBL, is identical to that of theusualGentzen-typesystem of classical logic. By cut-elimination, this part of the system is complete for the correspondingfragment of t==BL,.* q Other propertiesof +BL which can be generalizedto +BL, are compactness and interpolation: THEOREM 3.22. + BL, enjoys compactness,monotonicity, and interpolation. Proof. Identical to theseof Theorems3.10 and 3.11. The only necessaryaddition to the proof of 3.10 is showing that v as definedthereis a valuation also with respectto > (i.e.: v($ > 4) = V(G) > ~(4)). We leave this to the reader(compare to the proof of Proposition 3.17). 0 * It is not difficult to check that in FOUR our definition of > is the only possible definition for which this is true. ** From part (c) of the corollary it follows that the critical connective of GBL is negation.
REASONINGWITH LOGICAL BILATTICES
47
On the other hand,Theorem 3.9 cannot be extendedto bg~, . This is obvious from the fact that the {A, V, > )-fragment of GEL, is identical to the classicalone, andso it is strictly strongerthanits intuitionistic version (Thus, (II,> 4) > q!~I-G~L, ‘$9but ($1 d 1 ti YGBLI Tb We have alreadynotedthat unlike ~BL, +BL, doeshave valid formulae. This fact, togetherwith the existenceof an internal implication, indicate that for +BL, it might be possible to provide a sound and complete Hilbert-type representation. This indeedis the case:t The System HBL Defined Connective: $ = 4 gf w 14) A (4 1 $J> Inference Rule: $
$14
f In the formulae below the associationof nested implications should be taken to the right.
48
OFER
ARIELI
AND
ARNON
AVRON
[-x3] +mqq =+c3+ [-631-($eqq = +cB-(b [-II +04)-W-~ b-1 77TjcI?Jl Note: Again we note the critical role of negation in this system. THEOREM 3.23. GBL, and HBL are equivalent. In particular: abfh.. ,7LSn~GBL,~l,...,~rnifft-HBL~lA,...,A~~ 1 hv~..-7v~m(or.bst Vf$,incasethatn=O).
hV,..*,
b) Let l? be any set of sentences, and $ - a sentence. Then I’ I-HBL $ iff every valuation v in FOUR, which gives all the sentences in I’ designated values, does the same to $. Proof. It is possible to prove (a) purely proof theoretically. This is easy but tedious (the well-known fact that every {A, V, >}-classical tautology is provable from the corresponding fragment of HBL can shorten things a lot, though). Part (b) follows then from the completeness and the compactness of GBL, . Alternatively, one can prove (b) first (and then (a) is an immediate corollary). For this, assume that I’ YHBL $J. Extend I’ to a maximal theory I’*, such that l?* YHBL $. By the deduction theorem for > (which obviously obtains here), and from the maximality of l?*, r* (+ff~L q5iff r* t-HBL 4 > $. Hence, if 7 is any sentence, then if I’* YHBL $J > 7, then I* ~-HBL ($J > r) > 111and so I’* I-HBL $J by [> 31; a contradiction. It follows that I’* ~HBL $ > 7 for every i, and so for every 4 and 7: (*) if
r* YHBL C$ then r* I-HBL 4 3 7.
Define now a valuation v as follows: T u@)
dzf
I
t
i f
if I* !-HBL 4 and I’* I-HBL 14 ifI'*
YHBL
$andr*
YHBL
14
if I’* J-HBL Q, and I’* YHBL -c$ if I’* I~HBL 4 and I* I-HBL -4
Obviously, ~(4) is designated whenever I’* ~HBL 4, while v($) is not. It remains to show that u is actually a valuation. We shall show that ~(4 > r) = ~(4) > v(r), 1eaving the other cases for the reader. and that v(q5V~) =v(qb)Vv(~), To show that v(q5V~) = v(4)V v ( r ) , we note first that axioms [I V] and [V I], together with the above characterization (*) of the non-theorems of I*, imply that I’* ~HBL #VT iff either I* I- HBL 4, or I’* ~HBL 7. Axiom [TV], on the other hand, entails that I* ~HBL l( q5V7) iff both I’* k HBL 14, and r* tHBL 7. From these facts the desired equation easily follows. In showing that V(C$> T) = ~(4) > v ( r ) , we distinguish between two cases: case I: u(4) E {f, I}. Th is means, on the one hand, that ~(4) > V(T) = t. On the
REASONINGWITH LOGICAL BILATI-ICES
49
other hand, it is equivalent to I’* ~~HBL4. By (*) above,and by axiom [- >] this entailsthatr*~HEL~>~butr*YHBLl(~>7).Hencev(~>7)=t=y(~)>v(7). case 2: ~(4) E {t,T}. Then ~(4) > V(T) = V(T). In addition, it means that I* I-HBL4, and so (by axioms [> l] and [- >I), I’* ~HBL4 > T iff I’* ~HBLT, and 0 r* kHBL +$ > 7) iff r* t-HBL17. It follows that ~(4 > 7) = V(T) too. COROLLARY 3.24. HBL is well-axiomatized: a complete and sound axiomatization of every fragment of +BL,, which includes >, is given by the axioms of HBL which mention only the connectivesof that fragment. Proof. The aboveproof shows, as it is, the completenessof the axioms which mention only {V, >, -} for the correspondingfragment. All the other casesin which 1 is included are similar. If 1 is not included, thenthe systemis identical to the system for positive classical logic, which is known to have this property.* q Note: The (1, A, V, >}-fragment of GBL, and HBL were called in Avron (1991b)the “basic systems”.Again, it is shown therethat by addingI’ + A, $, +J to GBL,, and either -$V?+!J or ($J > 4) > (-+ > q5)> C$to HBL, we get complete proof systemsfor the full three-valuedlogic of {t, f, I}. This logic is an extension of Kleene three-valuedlogic, which is equivalent to the logic of LPF (Barringer, 1984; Jones, 1986). If, on the other hand, we add I, 7(1,-T+Q =S A to GBL, and -T/J > (+ > 4) to HBL, we get complete proof systemsfor the three-valuedlogic of {t, f, T} (also known as J3 - seenote (3) after Theorem 3.7). 3.4.2.
Strong Implication
The implication connective> hastwo drawbacks:the main one is that evenin case are both valid, $Jand 4 might not be equivalent(in the sensethat W>andO+ onecan be substitutedfor the other in any context). For example,if II, = $7 > p) and 4 = r A lp, then both $ > 4 and 4 > $ are valid, but + > -4 is not. The seconddisadvantageis that $ > 4 may be true, its conclusion false, without this entailing that the premise is also false (for example: I > f = t). This drawbacksof > are,in fact, drawbacksof kg~, , the consequencerelation on which it is based.What we can do, however, using the generaltheory developed in Avron (1991b), is to define in ~BL, an implication connective, which correspondsto k&L> and doesnot suffer from thesedisadvantages. DEFINITION 3.25. (strong implication)* l
$
+
4
+,sf
w
>44
.
$
*
4
esf
(Ic,
+
4)
A
C-4
A
(4
>-Icl> +
$9
* Without 7 there is no difference between A and 8, and no difference between V and @. ** In this definition too, the role of negation is critical.
50
OFER
ARIElLI
AND
ARNON
AVRON
has all the properties stated for & in ProposiPROPOSITION 3.26. &> tion 3.13. In addition, + is an internal implication for it: I’, $ &, 4 iff r l=SL, ti + 4 (in pa.rticulw YA$ -+ 4 k%L3 4). Proof. These are all immediate consequencesof the generaltheory in Avron (1991b), and the fact that 1, A and > satisfy in +BL, their correspondingsymmetry conditions as defined there (basically this meansthat the relevant rules of GBL, are valid). 0 PROPOSITION 3.27. Let $, 4, r be formulae in BL,, and v - any evaluation in FOUR. Then:
4 v($ + 4) E D(FOUR), iffv($) It v(4). b) v($ - 4) E D(FOUR), iff v($) = ~(4). Proof. Left to the reader.
0
COROLLARY 3.28. $ f-t 4 j=BL, O(q) tf O(4) for every scheme0. In other words, tf is a congruence connective. Proof. Immediate from part (b) of the last proposition, and from the fact that +BL,
is the Sameas ~(FOUR).
0
Proposition 3.27 provides us with an easy method of checking validity or invalidity of sentencescontaining +. Using this method it is straightforward to checkthe next two propositions:
REASONING
WITH
LOGICAL
BILA’ITICES
51
PROPOSITION 3.30. The following are not valid in ~=BL, (~BL,(~)):
Notes: 1. If we comparethe list above with the usual formal system for the relevance logic R (Andersonand Behrap,1975;Dunn, 1986),we seethat the only axiom of R which is not valid for this interpretationof -+ is the contraction axiom: ($J--t $ --f #) + $ -+ c$.It is worth noting that the omission of this axiom is also the main difference between the linear logic of Girard (see Girard, 1987) and the usual relevancelogics. In fact, the last two propositions are true for linear logic as well (with the exceptionof the converseof contraction, the distributive schemes,and the parts concerning @ and CB,of course), if we interprate1 and 4 as linear negationand implication (respectively),and A, V as the “additives”. Note, however, that the ‘“mix” (or “mingle”) axiom $*++lc, is valid. 2. On {t, f, I}, + is exactly Lukasiewicz implication (Lukasiewicz, 1967; Urquhart, 1984), while on (t, f, T) it is Sobocinski implication (Sobocinski, 1952),which is the implication of RM3 - the strongestlogic in the family of relevancelogics.
52
OFER
ARIELI
AND
ARNON
AVRON
3. By using +, we can sometimestranslate“annotatedatomic formulae” from Subrahmanian’sannotatedlogic (seeSubrahmanian,1990a,1990b;da-Costa et al., 1990; Kifer and Lozinskii, 1992;Kifer and Subrahmanian,1992):The translation of II, : b to BL(4) when b E FOUR, and when the partial order in the (semi)lattice is St, is simply b + $J. PROPOSITION 3.31. + EL> ww +4vw-w-+-t~) Proof. This can easily be checkedin FOUR.
0
The last proposition means that it is possible to choose--t rather than > as the primitive implication of the language.We prefer the latter, though, since the intuitive meaning of both is then clearer.Also, the correspondingproof systems are much simpler if we follow this choice. Using +, on the other hand, is more convenientfor relating our logic to other known logics, as we havejust seen. Our next proposition brings us back to the relations between our logic and relevancelogic: PROPOSITION 3.32. Let $ and 4 be in the languageof (1, A, V}; then the following assertionsare equivalent: a)II)bBL($ b) tit=&&
was noted alreadyafter Theorem 3.7. That ~BL $J14 iff $J+BL 4 is an instanceof the deductiontheorem for 1. Similarly, the equivalenceof +BL $J+ 4 and $ F&L 4 follows from the deductiontheorem for + relative to bgL, and the fact that +nL ?+!J iff +kL ?,/.J. Finally, +BL $ + $!)iff or every valuation u in FOUR, and it is well known (seeAnderson 444 It 48 f and Belnap, 1975;Dunn, 1986)that if $Jand 4 arein the (1, A, V}-language,then kR$ + 4 underexactly the samecircumstances. 0 PrOOf. That ?+b+BL (b iff +R $ + 4
We endthis subsectionwith a shortdemonstrationof the potential use of kBL, as well as of its various implication connectives.Recall that we are using w to denotethe implication of the classical calculus (i.e: $ cu 4 = -$J V 4). EXAMPLE 3.33. Considerthe following knowledge-base: bird( tweety ) -
fEy (tweety )
penguin( tweety) > bird( tweety) penguin(
tweety) + -?fly( tweety)
REASONING
WITH
LOGICAL
BILATTICES
53
bird (tweety )
Note that we are using different implication connectives according to the strength we attach to each entailment: Penguins lzever fly. This is a characteristic feature of penguins, and there are no exceptions to that, hence we use the strongestimplication (t) in the third assertionin order to expressthis fact. The secondassertionstatesthat every penguinis a bird. Again, thereare no exceptions to that fact. Still, penguinsarenot typical birds, thus they should not inherit all the propertieswe expectbirds to have. The useof a weakerimplication (1) forcesus, indeed,to infer that something is a bird wheneverwe know that it is a penguin, but it doesnot forces us to infer that it has every property of a bird. Finally, the first assertionstatesonly a default feature of birds, hencewe attach the weakest implication (u) to it. Indeed,sincefrom $ and T/.J Q 4 we cannotinfer 4 (by +BL) without more information, the first assertiondoesnot causeautomaticinferenceof flying abilities just from the fact that something is a bird. It doesgive, however, strongconnectionbetweenthe two facts. The above knowledge-basedoes not allow us to infer whether tweety is a penguin or not (as it should be), and if it can fly or not (which is less satisfactory; we shall return to it in the next section). However, if we add to the knowledgebaseanextra assumption,penguin( tweety), we can infer lfly(tweety) but we still cannot infer fiy( tweety), as should be expected. 3.5.
ADDING QUANTIFIERS
So far we have concentratedon propositional languagesand systems.The justification for this is that the main ideasandinnovationsareall on this level. Extending our notions and results to first order languagescan be done in a rather standard way. We can take V, for example, as a generalizationof A. Having then an appropriate structureD, and an assignmentu of valuesto variables and truth values to atomic formula, we let v(Vm+b(z)) be inf~~(~($~(d) ( d f D}. Here we are using, of course,the fact that we assume2? to be a complete lattice relative to St. The correspondingGentzen-typerules are then:
In theserules we assume,as usual, that the variable y doesnot appearfree in l? or in A. Correspondingsoundnessand completenessas well as cut elimination theoremscan be proved relative to FOUR with no great difficulties. We omit here the details.We just notethat onecan introducealso, in the obvious way, quantifiers which correspondto @Iand @.
54
4. A More Subtle Consequence
OFER ARIELI AND ARNON AVRON
Relation
+BL should be taken as a first approximation of what can be safely inferred when we have a classically inconsistent knowledge-base; this safety is its main advantage. The disadvantage is that +BL is somewhat “over cautious”. Thus, in Example 3.33 we would have liked to be able to infer jIy (tweety) from the original knowledge-base, before the new information, penguin( tweety ), is added to it. We cannot do this, of course, since +BL is monotonic. There is more than one way of introducing other consequence relations, which are less cautious, and enjoy non-monotonic&y; we present here one example. The idea is taken from a paper of Kifer and Lozinskii (1992). Their idea, basically, is to order models of a given knowledge-base in a way that somehow reflects their degree of consistency, and then take into account only the models which are maximal w.r.t this order. The main difference is that they were using just ordinary (semi)lattices, in which the partial order relation corresponds, intuitively, to our Sk. Hence, no direct interpretation of the standard logical cormectives (A, V) was available to them. They were forced, therefore, to use an unnatural language, in which the atomic formulae are of the form p : b (where p is an atomic formula of the basic language, and b - a value from the semilattice). $J : b is meaningless, however, for nonatomic $J. The use of bilattices allows us to give the standard logical language a direct interpretation, and so gives a meaning to every annotated formula. On the other hand, by using 3 we can dispense with annotated formulae altogether, as we do below.* DEFINITION 4.1. Let B = (B, It, Sk, 1) be a logical bilattice. A subset Z of B is called an inconsistency set, if it has the following properties: a)bEZifflbEZ. Notes: 1. From (b), always T EZ. Also, from (b), t $!Z, and so, from (a), f $!I. 2. As for I, both Z U {I} and Z \ {I} are inconsistency sets in case Z is. Now, on one hand, in every bilattice, 71 = I (Proposition 2.5), so 1. has some features that may be associated with inconsistent elements. On the other hand, I intuitively reflects no knowledge at all about the assertions it represents; in particular, one might not take such assertions to be inconsistent. We shall usually prefer, therefore, to take I as consistent (see also the note after Proposition 4.13). EXAMPLE 4.2. The following a)Zt={bIbE3and~bE3}.
are all inconsistency
sets:
* Despite the fact that this method of using “annotated” atomic formulae is quite common, it is still artificial from a logical point of view, since semantic notions interfere within the syntax. ** In Kifer and Lozinskii (1992) the inconsistent values are defined quite differently; see there for the details.
REASONING
WITH
LOGICAL
55
BILA’ITICES
b)&={b 1 b = lb}. c)I&={bIb=-.b, b#I}. Zl is the minimal possible inconsistency set in every in every (B, 3). In case that B in interlaced, and F = 27(B), Zl is just {T} (see Proposition 2.25). Z2 and Zs are always inconsistency sets in case B is interlaced, and F = D(B). There are, however, other cases in which they are inconsistency sets, for example in DEFAULT.
We fix henceforth some logical bilattice (B, 3), and an inconsistency subset Z of it. Unless otherwise stated, all the definitions below will be relative to (17, F) and 1. We will refer to the members of Z (the members of B \Z) as the inconsistent (consistent) truth values of B. NOTATION 4.3. a) A(I) denotes the set of the atomic formulae that appear in some formula of I. b) For a valuation M of I, denote: IM(I’) = {pi A(I’) 1M(p) ET}. DEFINITION 4.4. Let l? and A be two sets of formulae, and M, N - models of I. a) M is more consistent model of I than N, if the set of the atomic formulae in AA(I’) that are assigned under M values from Z, is properly contained in the corresponding set of N (i.e: IM(r) c IN(I)). b) M is a most consistent model of I (mcm, in short), if there is no other model of I’ which is more consistent than M. d r bon A if every mcm of I is a model of some formula of A. EXAMPLE 4.5. Let us return to the knowledge-base K. of Example 3.33. Take F = {t, T} and B - any bilattice in which this 3 is a prime bifilter (e.g: FOUR, DEFAULT). Let Z be any inconsistency set in B (obviously, FnZ = {T}). Relative to (B, F) and 1, this knowledge-base has exactly one mcm, and it takes values in {t, f }. Hence, if $ is in the language { 1, A, V, >}, then KB b,,, 11,iff $ follows classically from KB. Thus (unlike in the case of +BL!): KB f==,,, bird (tweety ), KB k,,, lpenguin(tweety), KB t#=,,, lbird(tweety), KB /&,,penguin(tweety),
KB +confly(tweety), KB ~Con~Jty(tweety).
Now, consider again what happens when we add penguin(tweety) new knowledge-base, KB’, has two mcms, Ml and M2, where: Ml (bird (tweety)) Mz(bird(tweety))
= t, Ml (penWn(tweety)) = T, M2(penguin(tweety))
to KB: The
= T, Ml(fEy(tweety))
= T,
= t, N@y(tweety))
= f-
This time, therefore,
KB’ km
bird(tweety),
KB’ k=,,, penguin(tweety),
KB’ b:,,,
l,%y(tweety),
56
OFER
KB’ km
1 bird (tweety),
KB’ /&,,
lpenguin(tweety),
ARIELI
AND
ARNON
AVRON
KB’ PC,, fEy(tweety).
It follows that /==,,, is a non-monotonicconsequencerelation, which seemsto behaveaccordingto our expectations. 0 Some important propertiesof k,,, aresummarizedbelow: PROPOSITION 4.6. If I’ ~=BLA then l? k,,lt A. Proof. If every model of l? satisfiessome formula of A, then obviously every 0 mcm of P doesso. PROPOSITION 4.7. kcon is non-monotonic. Proof. Consider,e.g., I’ = {p, 1pV q}. In every mcm, M, p and Qmust have consistentvalues (since the valuation that assignst to each one of them, is an mcm of I’). Also, M(p) E 3, since M is a model of I. If M(lp) E 3 also, then M(p) E 3’nZ(from Definition 4.1(b)),so M(p) is inconsistent.HenceM(lp) 523. But M( lp V q) E 3, henceM(Q) E 3. So, l? k,,, Qin every (f3,3) and Z. Obviq ously,however, I, up pc,,q (take,e.g., M s.t. M(p) = T, and M(q) =f). PROPOSITION 4.8. k,,, is paraconsistent: P, --P bGon q, and even pvq,
-(PO>
b%
q.
Proof. Consider any valuation that assignsp the value T, and assignsq the value f . 0 PROPOSITION 4.9. If l? and $ are in the language of (1, A, V, 1, f, t}, and v+!J, then $ classically follows from r. Proof. The crucial property of the languagehere is that if all the atomic formulae get valuesin {f, t}, then so doesany formula in the language.Now, if I’ is classically consistent,then it hasa model in {t, f}, and so all its mcms assignthe members of AA(I’) consistentvalues. Hence, if I b,,, $, then every model of l? that assignsthe membersof A(I) consistentvalues,is a model of +. In particular, every model of I’ that assignsthe members of A({I’, $}) classical values (i.e.: {t, f}), is a model of $, and so $ follows classically from l?. If I is classically inconsistent,then any # follows from it classically (in particular $). 0.
r +,,,
A partial conversefor consistenttheoriesis given in the next proposition: PROPOSITION 4.10. Let I be a classically consistentset in the languageof (7, A, V, f, t}, andlet $Jbe a sentencein the samelanguage,which classically follows from I. Then thereexist sentences4 and7, suchthat: 1) $Jis classically equivalentto 4, 2) 7 is a tautology,
REASONING
WITH
LOGICAL
BILATI’ICES
57
Proof. Let $’ be a sentencelike in Proposition3.5. T/J,’ canbe written in the form 4 A T, where T is the conjunction of all the conjuncts in $’ which are tautologies (i.e.: contains some atomic formula and its negation as disjuncts), and 4 is the conjunction of the other conjunctsof $J’(if either setof conjunctsis empty, we take it to be t). 4 and T obviously satisfy properties(2) and (3). Since classical logic is an extensionof ~BL(~) w.r.t. the languageunder consideration,+ is classically equivalent to EAT, and so to 4 (since 7 is a tautology). It remains to prove (4). It is easy to seethat l?+=,,, f$iA. . .A& iff F b,,, & for every i = 1. . .n. Hence, (4) follows from the following lemma:
LEMMA 4.11. Let I be a classically consistentset in the languageof { 1, A, V , f , t } , and1c,- a clausethat doesnot containany pair of an atomic formula and its negation.If $ follows classically from l?, then l? k:,,, $. Proof. We will show that if l? PC,, $, then there is a classical model of l?, which is not a model of $. Indeed,let M be an mcm of l? s.t. M($) 63. Consider the valuation M’, definedas follows: if M(p)E3, andpEA@‘,+). if M(y~)~F,andp~A(l?,y!~). if M(p) $!3, M (1~) $3, and lp appearsas a literal in $. if M(p) @3, M (1~) $!3, andp appearsas a literal in $J. otherwise Exactly asin the proof of Proposition4.9, thefact that I is classically consistent entails that M(p) is consistentfor everyp in A(F). Hencetherecannotbe any p in A(P) s.t. both M(p) and M(lp) are in 3 (otherwise,from (b) in Definition 4.1, M(p) E Z). On the other hand, if p E A($) then either p or up is a disjunct of $. Since M ($) @3, this implies that either M(p) 6 3, or M(lp) e 3. These two facts and our explicit assumptionon T/Jimply that M’ above is well defined. Obviously, M’ is a classical valuation. Now, by Proposition 3.5, there is a set of clausesr’, s.t.A(r) = A(r’), every model of F is also a model of I”, and viceversa.Since M is a model of I, it is also a model of I”. Hence, for every clause 4 E r-1with literals Zi (i = 1 . . . n), there is at least one literal, li, s.t. M (li) E 3. From the definition of M’, M’(Zi) E 3 as well, thus M’ is a model of I”. Hence M’ is a model of l? as well. On the other hand, M’($J) = f, since for every literal Zi that appearsin T/J,M’(Zi) = f. Indeed,without a loss of generality,supposethat Zi= lp. Since M ($J)$!3, also M (-p) $z’3. If M(p) E 3, then M’(p) = t, and so M’(4) = M’(lp) = -M’(p) = -t = f. If M(p) @3, then since up appearsas a literal in $J,M’(p) = t in this caseaswell, and againM’(Zi) = f. M’ is, therefore,a classicalmodel of l?,which is not a model of T/J.Hence1c,doesnot follow classically from r. 0 Note: The crucial Lemma 4.11 doesnot hold under strongerassumptions: a) If we allow the appearanceof > in F, then consider (FOUR) with Z = {T},
58
OFER
ARIELI
AND
ARNON
AVRON
and I’ = {p > q,p > TQ}, $ = up. $ follows classically from l?, but the valuation M, where M(p) = I, and M(q) =t, is an exampleof an mcm of I’, which is not a model of $. b) If 1c,contains a literal and its negation, then consider again (FOUR) with Z = {T}. This time, pV up follows classically from q, but q kI,,, pV up (consider, e.g., M(q)=t, M(p)=I).* As we have already shown, k=,,, is non-monotonic. We next show that in addition it satisfiessome propertiesthat one might like a non-monotoniclogic to have: DEFINITION 4.12. (Lehmann, 1992): A plausibility the following conditions (for finite l?, A): Inclusion:
logic is a logic that satisfies
r, T)* $.
Right Monotonicity:
If l? + A, then I +- $, A.
Cautious Left Monotonicity: Cautious Cut: If
If I’ =+r,l~and I + A, then I, $J+ A.*
r , $q,. . . ,$~+AandI’+&,Afori=l...n,thenI’+A.
PROPOSITION 4.13. + co71 satisfiesInclusion, Right Monotonicity, and Cautious Left Monotonicity. k,,, also satisfies Cautious Cut iff there exists ,B E B s.t. /3pJFU{b 1dEF}, and the languageis BL(4) (Hence b=,,-,,is a plausibility logic under theseconditions).t Proof. Inclusion and Right Monotonicity follow immediately from the definition of k,,,. Proof of Cautious Lef Monotonicity: Assume that I k,,, r/j, I kc,, A, and let M be any mcm of {I’, $J}. We will show that M is also a mcm of I. Since l?kcon A, this will imply that M satisfiessomeformula in A, and so I, r,l~kcon A. Now, M is certainly a model of I. Assume that it is not an mcm of I. Then there is a model of I’ that is strictly more consistentthan M. Since l? is finite, there is an mcm iV of l?, which is strictly more consistent than M; and so IN(r) C IM(I’). Consider the valuation N’ that is defined as follows: N’(p) = N(p) for every p E A(r) and N’(p) = b otherwise, where b is any consistenttruth value. Obviously, N’ is an mcm of I. Since I’ k,,, $, N’ is a model of {I’, $}. Now, INf(r,~)=IN’(r)=IN(r)cIIM(r)~I1M(r,~).HenceN’isamodelof(r,~}, which is more consistentthan M. This contradictsthe fact that M is an mcm of v, $1. * One can replace here {q} by {q, qVp}, if one wishes A(+) to be a subsetof d(r). ** This rule was first proposed in Gabbay (1985). $ In Proposition 4.10 of Arieli and Avron (1994) the bilattice under consideration should have been interlaced, and p = I (these assumptionswere used there for the proof of the Cautious Cut). Here we prove the proposition for any logical bilattice, and for ,Bas defined above, which may be different from 1.
REASONING
WITH
LOGICAL
59
BILATTICES
Proof of Cautious Cut under the speci$ed conditions: Assume that I, $1, . . . , n. Let M be an mcm of I’. We will show ~‘n~=conAandr~=,,,Ili,Afori=l... that M is a model of some formula of A. For this, define another valuation, M’, by. Ml@)
d”=f{ T(P)
f;eEm-~~’
Obviously, M’(d) = M(4) for every 4 s.t. A(d) GA(I). Hence M’ is also an mcm of I. Thus, M’ is either a model of some 4 E A, or M’ is a model of $1, . . . , &. Since M’(p) E Z implies that p E A(I), and since M’ is an mcm of l?, M’ is necessarily an mcm of {r, $1,. . . , $,,,} in the second case. Hence, again, M’ is a model of some 4 E A. It follows that in either cases M’(4) E F for some 4 E A. It remains to show that M (4) E F whenever M’(4) E F. Indeed, by Proposition 3.5 there exists a formula #‘, which is a conjunction of disjunctions of literals, s.t. for every valuation u, ~(4) E F iff ~(4’) E 3. If M’(4) E 3, then M’(#) E F also, so M’(D) E 3 for every conjunct D of qS. Now, M’(D) E F iff there is a literal 1 E D s.t. M’(Z) E J’=. But since I is a literal, it is obvious that M’(Z) E F only if M’(Z)#Pand M’(lZ)#p, so M(Z)=M’(Z). Hence M(Z) ~3as well. It follows that M(D) EF also, and so M($‘) EF, implying that M(4) ~3. To show the necessity of the conditions we note that: 1) If > is in the language, then for every B, 3, and Z: q k,-0, q V p, and Q,4VP km. (P 1 -q> V (1~ 3 lq), but q PC,, (P 3 -q> V (T 3 -q> We a valuation M, s.t. M(q) =t and M(p) =T). 1 7bE 3}, then q kc,, qVp and q,qVp /=conpV~p, but 2) If B=ZU3U{b q pconpVlp (consider M, s.t.M(q) = t and M(p) = I). 0 Note: If I $!Z (see note 2 after Definition Cut is satisfied for p = 1.
4.1) then the condition
for Cautious
The crucial point in the counterexamples given in the last proof, is that the cut formula contain atomic formula that does not appear in A(I). In fact, it is easy to show that otherwise the rule is valid with no extra assumption: DEFINITION 4.14. (Analytic Cautious Cut) If I, $1, . . . , v+!J~ kO, A and I t==,,, &, A for i = 1 . . . n, and if A({$l, . . . , $n}) C AA(I’), then I’ +=,,, A. PROPOSITION 4.15. Analytic Cautious Cut is valid rule for kO,. Proof. Let M be any mcm of I’. We will show that M is a model of some formula in A. If not, then M is a model of $~i (i = 1 . . . n), since P k,,, $;, A. Hence M is a model of {I’, $1,. . . $J~}. It is obviously an mcm of this set, since any model which is more consistent than M w.r.t {I’, $1,. . . $J~}, is also a more consistent model than M w.r.t I (using the fact that n({$l,. . . , $I~}) G A(r)). Sincel7,7+$,... , $m k,,, A, M is a model of some formula of A after all. 0
60
OFER
ARIELI
AND
ARNON
AVRON
PROPOSITION 4.16. All the rules of GBLarevalid for b=,,,. Proof. The validity of Exchangeand Contraction is immediate from the definition of bcon. The introduction rules on the right, as well as their inverses,are valid for exactly the same reasonsthat they are valid in +BL. The rules [A +-I and [@=+-Iare valid, since the models of {I’,$, 4}, {I’,$A$}, and {I’,$J@~}, are the same,hencethe mcms of these sets are also the same. Similar argument works for [ll +I. The rules [V +] and [C;a +] areproved in Lehmann (1992)to be valid in every plausibility logic, which satisfies[a V], [+ @],and their converses. The proof there doesnot use in fact the full power of Cautious Cut, but only that of Analytic Cautious Cut. For the readerconvenience,we repeatthe arguments, adjustedto our logic, for the caseof [@+]: Inclusion andRight Monotonicity. (1) r,ll, * $74 w-4~4 (l), [*@I. Hypothesis. (3) r,ti * A (2), (3), Left CautiousMonotonicity. (4) r,w.b @?4 * A (5) I, $, $ $4 + 4, A (4), Right Monotonicity. (6) I, + @ 4 =%?1,@4 Inclusion. (6), Inverserule of [+ e]. (7) r, ti e 4 + ti, 4 (8) I, $J@ 4 =+ $, 4, A (7), Right Monotonicity. (5), (8), Analytic CautiousCut. (9) r, ?il@ 4 * 4, A Provedlike (4), exchangingthe roles of $Jand 4. (10) r, 4, $ @ 4 * A (9), (lo), Analytic CautiousCut. (11) r,ea+A Finally, [+ +I, [TV =s], [w% +-I, and [-@ +] all follow from Lemma 2.5(a), togetherwith the previous observations. 0 (2)
Someothernice propertiesthataretruein everyplausibility logic which satisfies [+@],andth eir converses,arelisted in the next proposition (seeLehmann, 1992): [*VI,
PROPOSITION 4.17. Let l?, A be setsof formulae, and $J,4, r - formulae in BL. Then: Left Equivalence:
Right equivalence:
r, + kc,, 4 r, 4 i=con$ r, @bon A I?,4 kconA r, + kco, 4 r, 4 kcon + r b r bon 4, A
$TA
REASONING
WITH
LOGICAL
61
BILA-ITICES
4 v ?-l=m4 + v 4 l=con $ + v 7 l=con ti
4a3?-l=ccm 4 + @4 hm $ ti a37-I==,*, ?I
As we have shown, kcon has a lot of desirable properties. We should mention, however, that k c0n is not closed under substitutions. In other words: it is sensitive to the choice of the atomic formulae. Thus, although up, pV q /==,,, q, when p and q are atomic, it is not true in general that T/J, $V 4 kc,,, qh(take, e.g., 23= FOUR, +==(-pAp),and4=q).Th is ,h owever, is unavoidable when one wants to achieve both Lemma 4.11 and Proposition 4.8 above. 5. Conclusion
and Further
Work
Bilattices have had an extensive use in several areas, most notably in logic programming, but their role so far was mainly semantic in nature. We develop a real notion of logic based on bilattices, giving associated consequence relations and corresponding proof systems. These consequence relations are strongly related to non-monotonic reasoning, and especially to reasoning in the presence of inconsistent data. This, however, is not the end of the work. The basic languages mentioned here are, as their name suggests, only basic. It seems that additional connectives are required in order to get more expressive languages. Such languages should be able to describe more precisely the specific bilattice under consideration. One would like, for example, to express in a knowledge-base over DEFAULT that a certain formula is considered to be true by default, or that the result of f @ t should be considered as dT rather than 1. This can be achieved, e.g., by defining a connective that reflects equivalences in formula assignments, or by defining some kind of analogue to the “:” -connective of annotated logic. The guard connective, investigated in Fitting (1994), might also be considered. The consequence relations are also a matter for further examination. As we have shown (Theorem 3.4), the basic consequence relation, ~BL, is no more than the logic of FOUR. Nevertheless, it is obviously desirable to take advantage of the availability of other values in the bilattice under consideration, for example the default values {df, dt} of DEFAULT. Considering b=,,, was a first step, since we take into account not just the designated elements of the bilattice, but also those that were considered as inconsistent. For b,,, FOUR is no longer a single representative of all the logical bilattices. For example, by taking B to be FOUR with the inconsistency set Z = {b E 0 1 b = lb}, we have that q, p > lq k,,,, -up, ~pVp, while if we take i? to be DEFAULT with the same definition aWw+con of inconsistency set, these consequences are no longer valid. k=,,, seems to be, however, somewhat too crude, since it treats uniformly the whole set of atoms that are assigned inconsistent values under a given valuation. As a result, the preferences
OFERARJELIAND ARNONAVRON
62
among the valuations are due to “global” considerations rather than pointwise ones. A future work should seek for a refinment of this relation, which might as well reflect the specific structure of the bilattice (especially its partial orders). Another natural issue for a further research is to investigate how the resulting logics are affected by the choice of the bilattice under consideration, the truth values that are taken to be designated, and the choice of the inconsistency subsets. References Arieli, 0. and Avron, A., 1994 “Logical bilattices and inconsistent data,” in Proc. 9th IEEE Annual Symp. on Logic in Computer Science, IEEE Press,pp. 468-476. Anderson, A.R. and Belnap, N.D., 1975, Entailment. Vol. 1, Princeton, NJ: Princeton University Press. Avron, A., 1986, “On an implication connective of RM,” Notre Dame Journal of Formal Logic 27, 201-209. Avron, A., 1991a, “Simple consequencerelations,” Information and Computation 92, 105-139. Avron, A., 1991b, “Natural 3-valued logics: characterizationand proof theory,” Journal of Symbolic Logic 56(l), 276-294. Barringer, H., Chang, J.H., and Jones, C.B., 1984, “A logic covering undefinedness in program proofs,” Acta Informatica 22,25 l-269. Belnap, N.D., 1977a, “A useful four-valued logic,” in Modern Uses of Multiple-Valued Logic, G. Epstein and J.M. Dunn, eds., Dordrecht: Reidel, pp. 7-37. Belnap, N.D., 1977b, “How a computer should think,” in Contemporary Aspects of Philosophy, G. Ryle, ed., Stocksfield, Engknd: Oriel Press,pp. 3&56. da-Costa, N.C.A., 1974, “On the theory of inconsistent formal systems,” Notre Dame Journal of Formal Logic 15 497-510. da-Costa, N.C.A., Henschen, L.J., Lu, J.J., and Subrahmanian, V.S., 1990, “Automatic theorem proving in paraconsistentlogics, theory and implementation.” in IOth Int. Con$ on Automated Deduction, M.E. Stichel, ed., pp. 72-86. Dunn, J.M., 1986, “Relevant logic and entailment,” in Handbook of Philosophical Logic, Vol. III, D. Gabbay and F. Guenthner, eds., Dordrecht: Reidel, pp. 117-224. Epstein, R.L., 1990, The Semantic Foundation of Logic. Vol. I: Propositional Logics, Dordrecht: Kluwer Academic Publisher. Fitting, M., 1989, “Negation asrefutation,” in Proc. 4th Annual Symp. on Logic in Computer Science, IEEE Press,pp. 63-70. Fitting, M., 1990a, “Bilattices in logic programming,” in The 20th Int. Symp. on Multiple-Valued Logic, G. Epstein, ed., IEEE Press,pp. 238-246. Fitting, M., 1990b, “Kleene’s logic, generalized,” .Journal of Logic and Computation 1,797-810. Fitting, M., 1991, “Bilattices and the semanticsof logic programming,” Journal of Logic Programming 11(2), 91-116. Fitting, M., 1993, “The family of stable models,” Journal of Logic Programming 17, 197-225. Fitting, M., 1994, “Kleene’s three-valued logics and their children,” Fundamenta Informaticae 20, 113-131. Gabbay, D.M., 1985, “Theoretical foundation for non-monotonic reasoning in expert systems,” in Proc. of the NATO Advanced Study Inst. on Logic and Models of Concurent Systems, K.P. Apt, ed., La Collesur-Loup, France: Springer-Verlag,439-457. Ginsberg, M.L., 1988, “Multivalued logics: A uniform approach to reasoning in AI,” Computer Intelligence
4,256-3
16.
Girard, J.Y., 1987, “Linear logic,” Theoretical Computer Science 50, l-101. Jones,C.B., 1986, Systematic Sojiware Development Using VDM, Englewood Cliffs, NJ: PrenticeHall. Kifer, M. and Lozindcii, EL., 1992, “A Iogic for reasoningwith inconsistency,”Journal ofAutomated Reasoning 9(2), 179-215.
REASONINGWITH LOGICAL BILAl-l-ICES
63
Kifer, M. and Subrahmanian, VS., 1992, “Theory of generalized annotated programming and its applications,” Journal of Logic Programming 12,335-367. Lehmamr, D., 1992, “Plausibility logic,” in Proc. of.5th Workshop on Computer Science Logic, Berlin Springer-Verlag,pp. 227-241. Lukasiewicz, J., 1967, “On 3-valued logic,“Ruch Filosoficzny 5, 169-171, 1920. English translation: Polish Logic 1920-1939, S. McCall, ed., Oxford: Oxford University Press,pp. 15-18. d’ottaviano, I.M.L. and da-Costa, N.C.A., 1970, “Sur un problbme de Jaskowski,” Comptes Rendus Hebdomadaires
des Seances de I’dcademie
des Sciences. Serie A 270, 1349-1353.
d’Ottaviano, I.M.L., 1985, “The completenessand compactnessof a three-valued First Order Logic,” Revista colombiana de matematicas X1X( l-2), 3 l-42. Rozoner, L.I., 1989, “On interpretation of inconsistent theories,” Information Sciences 47,243-266. Sobocinski, R., 1952, “Axiomatization of a partial system of three-value calculus of propositions,” Journal of Computing
Systems 1,23-55.
Subrahmanian, VS., 1990a, “Mechanical proof procedures for many valued lattice-based Logic programming,” Journal of Non-Classical Logic 7, pp. 7-41. Subrahmanian, VS., 199Ob, “Paraconsistent disjunctive deductive databases,” in ZEEE.2Oth Znf. Symp. on Multiple Logic, pp. 339-345. Takeuti, G., 1975, Proof Theory, Amsterdam: North-Holland. Urquhart, A., 1984, “Many-valued logics”, in Handbook of Philosophical Logic, Vol. III, D. Gabbay and F. Guenther, eds., Dordrecht: Reidel, pp. 71-116.