General Approach to Nonmonotonic Logics

1. Language

The language under consideration con­ tains: the set of proposition letters de­ noted by p,q,p1,q1, ·· ; the connectives I'V (not), ::> (if ··· then); the modal opera­ tor M (it is consistent that); the brack­ ets ( , ) · A formula is either a proposi­ tion letter, an expression ( "'cx:.) , where 0(, is a formula, or an expression (ex:. ::J ~), where ex. and ~ are formulas. 0ther connec­ tives are defined as usual. The modal op­ erator L (it is provable that) is an ab­ breviation for "'M"'oc. The brackets can be omitted if convenient.

2. The monotonic component

Each nonmonotonic theory is identified with a set of formulas, the proper axioms of the theory. A deductive structure of the theory is given in two steps, first specifying a set of logical axioms and monotonic inference rules, common to all theories, and then de1!nlng a theorem of the theory by means of special algebraic operator. We start with the first part of the above specification.

Logical axioms

A1. ot::>(pO(.)

A2. tec. ::> l ~::> 't)) ::> ( (ex:,:>~):> (c£.:> f))

A3. ( .. ~he>L)::>(("P=>"')=> J)

A4. L(DL::~ ¥) .:> (Lt::>L~)

A5. loc ::>or.

A6. Ma<..:>I..M«. Monotonic inference rules

R1. From ot::> ~ and oc. to infer

R2. From ' r:L to infer Lor..

The axioms A1-A3 and the rule R1 form a possible axiomatization of classical propositional logic. The axioms A4-A6 and t he rule R2 are minimal conditions which should be valid if modal operators are to meet their interpretation as consistency and provability. It is difficult to dis­ cuss such conditions without a reference to an inference system. For a time being, however, we can assume that we have some abstract operator Y mapping theories into sets of formulas regarded as theorems of the theories. Assuming that for each the­ ory A the set Y(A) contains all proposi­ tional tautolo6ies and is closed under the rule R1, there are two further conditions which should be fulfilled:

(L)

oc EY(Al iff lix:EY(A)

• (M) "'oc ~ Y (A) iff M~EY( A) , assuming that ~ tY (A) for some formula ~ ·

Now the rule R2 is the only-if half of ( L) . A4 is the modus ponens rule R1 stated in the object language. A5 states the ob­ vious fact that whatever is provable is true. A6 follows from (L) and (M) (note that it is equivalent to L"'«vLM~, take any theory A and consider two cases: (i) "-'EY{A); (ii) "'o:~Y(A) ). Observe that R2, and A5 together with R1 guarantee ( L) . The if half of ( M) is also satisfied ( as­ sume that MC(.EY (A) and .f>fY (A) for some~ ; thus ~MC(.fY(A); but ~M«aL~~, and hence ~~~Y (A) by R2 ). It should be remarked that the only-if half of (M) is not as­ sured. We shall discuss this problem later.

We write S 1- oc. iff ex. is provable in the usual sense from the set of formulas S and instances of A1-A6 by re?eated application of R1-R2. We define Th( S J =tC~.: S roO<.}.

Formally, A1-A6 and R1-R2 form an axi­ omatization of traditional propositional S5 modal logic (see [1]).

3. Kripke models

We review Kripke semantics for proposi­ tional S5 modal logic. It will play an important role in further development.

A~ is a system K· tW,m), where W is a non-empty set of possible worlds, and m is ·a mapping from proposition let-t_!rs into 2w.

The value of formula o: in K·(W,m) with reslnct to wEV: denoted by -v (K, w, <i) , ~ def ed as follows: (i) V(K,w,p)·1 iff wEm(p) , where p is any propositional let­ ter; (11) V(K,w,"'<i) ·1-V (K,w,o:); (iii) V (K,w,cx.:)~) ·1 iff V(K,w,«) ~ or V (K,w,~) ·1; ( iv) V(K,w,M..:)·1 iff V(K,u,«) ·1 for some u(W.

A formula oc is true in K ( K 1= oe.) , iff V(K,w,~>-1 for each Wiw. A set s of for­ ~ is true.!!:! K, and we say that Irl's ·!liiOdelfor S, iff K ,_ «. for each Q(.ES.

4. Generalized nonmonotonic operator

We noted that the specified monotonic component guarantees ( L) and the if half of (M) . There still remains the problem of the only-if half of (M), which we denote by ( M~ ) . McDermott tries to resolve the problem by means of a special operator NMA defined f or each theory A as NMA(S) = Th(AvAsA(S)), where AsA \S) , the set of assumptions from S is given by As A ( m- ... { 1\k: "'"' ~ S f-="'1'h( A) ·

Let S be a fixed point of NMA. It can be regarded as a set of formulas obtain­ able from A by means of monotonic rules augmented by lM~), and thus satisfies all conditions required from the set of the­ orems nonmonotonically derivable from A. Unfortunately, for a given theory A there are, in general, many fixed points under that operator. Moreover, each of them is minimal in the following sense: if S1, S2 are fixed points of NMA, then S1 ~ S2 im-

plies S1·S2 (see [3]). Hence, the only plausible solution is to identify the set of theorems nonmonotonically derivable from A with the intersection of all fixed points of NM · Unfortunately, the re­ sulting logi~ is the monotonic S5 modal logic (see [2] ) .

To resolve the problem we propose to change the conceptual emphasis in our ap­ proach. Instead of formalizing the notion of consistency, and treating the nonmono­ tonicity as some kind of side effect of a resulting system, we shall look at non­ monotonic logic as at a formalization of beliefs based on the concept of consis­ tency. To fix some ideas, consider a the­ ory A. From the strictly logical point of view, the whole of valid information about A is contain~d in Th(A). Now if this in­ formation is insufficient and, moreover, no new axioms can be added, there is only one possibility: to extend the theory on a heuristic basis. Of course, if S is such a heuristic extension of A, then for­ mulas from the set Th(S) - Th(A) should be regarded as beliefs.

There still is the problem how such an extension is to be specified. We think that the syntactic form of axioms can give us some hints. Consider, for instance, the theory A ·{Mp::~q}. Although A has infin­ itely many extensions, one feels that ex­ tensions containing Mp, and hence q, should be preferred to all others. It is due to the fact that we are tempted to re­ gard Mp as the logical truth. Of _course, Mp is not valid. The problem is that to decide whether something is consistent one has to answer the crucial question: consistent with what? The simplest an­ swer: with the theory itself, is unaccept­ able. Note that p and ~q are both con­ sistent with A, yet regarding Mp and MNq , as simultaneuosly valid leads to inconsis­ tency. The correct interpretation of con­ sistency is to view it with respect to the theory itself together with all be­ liefs. Having this in mind, it is clear that the truth value of Mp depends on beliefs we hold about the theory, Never­ theless, Mp can consistently be added to A and, moreover, it seems to be the only candidate for such an addition.

The above discussion suggest that the set of theorems nonmonotonically derivable from a theory should be identified with the set of theorems monotonically deriv­ able from some extension of the theory. We propose to specify such an extension by choosing a set of preferable assumltions, i.e., a set of assumptions one wou d like to add to the theory. To make this idea workable we generalize the operator NMA as follows.

Let A be a theory, S and T sets of for­ mulas. We define the ~eneralized nonmono­ ~ operator NMA,T y

NMA T(S) · Th(AvAsA T{S)), where AsA T(S), ' ' ' the ~ £! assumptions ~ S ~ respect to T is given by AsA T(S) = {McC.: cx.ET and ..... ts}- Th(A).

futui tively, . the set {Met: o{. ~T J forms the set of preferable assumptions for a theory A.

We propose the following general de­ finition of nonmonotonic logic. By n2n­ monotonic logic we understand any function f from sets of formulas into sets of for­ mulas. Intuitively, f should be regarded as a mappin~ which assigns to each theory A a set f(AJ such that the set { Ma.: oc.~f(A)J is the set of preferable assumptions of ~.

If f is a nonmonotonic logic and A is a theory, then the set of theorems non­ monotonically derivabLe from A, denoted by TH(A), is the intersection of all fixed points of NMA,f(A)'

There still remains the problem what nonmonotonic logic f should be chosen to meet intuitive expectations, We shall pro­ pose a solution to this problem for a specific class of theories. But first we give a semantics of nonmonotonic logic.

5. Semantics of nonmonotonic logic

The semantics of nonmonotonic logic is based on the notion of model of S5 modal logic.

Let K be a model, T a set of formulas. By M(K,T) we denote the set {M«.: «. ET and K I= M«.J,

A model K for a theory A is said to be M-maximal with resRect to T iff for each model K1 fOrA, M ( , T) £M (K1 , T) implies M(K,T) = M(K1,T) .

The following completeness theorem holds:

Theorem 5.1. Let f be a nonmonotonic logic. : or each ·t,her·,··:· A anrl formula ac., o:'-'l 'H(.A; iff · ·-~-- ·~ t·ue in e2.ch ; _ -· · . ~· ;;'~al model for A with respect t.o 7 ·.· ·

We have a detailed proof of the a uove theorem but we are not able to give it in this brief paper.

6, Default theories

The problem of choosing the appropriate nonmonotonic logic is, in general, very complex. In this paper we limit ourselves to a specific class of theories. Following Reiter's terminology (see [4]) we call them default theories.

We denote by PC the classical proposi­ tional calculus. A theory A is said to be a default theory iff each axiom of A be­ longs to PC or is of the form

Letcx. be an axiom of a default theory. By P(oc) we denote the set of formulas giv­ en by

If A is a default theory, then by P(A) we denote the set U P(~) · o(.liA

P(oc.) = ifoe.~:.PC then the empty set else t~1'' .. '~n}·

For default theories the problem of choosing the appropriate nonmonotonic log­ ic is simple. The only reasonable candi­ date seems to be the function which assigns to a theory A the set P(A). ·

From the Theorem 5.1 we thus obtain the following completeness theorem for default theories:

Theorem 6.1. Let A be a default theory. For each formula cc., ou:TH (A) iff a. is true in every M-maximal model for A with re­ spect to P(A).