Modal Interpretations of Default Logic

1 Introduction

The default logic of Reiter [1980] is a nonmonotonic for­ malism based on the paradigm of "negation as failure to prove" and is defined by means of a certain fixed-point construction. It is a formalism in the language of propo­ sitional calculus (or, in a more general variant, in the lan­ guage of first-order logic). In 1982, McDermott [1982], building on the joint work with Doyle [1980], introduced a large class of modal nonmonotonic logics. He proposed a general scheme which, also using "negation as failure to prove" and a fixed-point construction, assigns to each monotone modal logic its nonmonotonic variant. The au­ toepistemic logic of Moore [1985], an important modal formalism, belongs to the McDermott-Doyle's family of logics (see [Shvarts, 1990]). In recent years there have been numerous attempts to explain and exploit the na­ ture of the relationship between the default logic and The default logic was first embedded into a variant of autoepistemic logic by Konolige [1988]. Marek and Truszczynski [1989; 1990] proposed to embed default logic into the nonmonotonic variant of the logic of neces­ sitation N - the modal logic that does not contain any modal axiom schemata and uses modus ponens and ne­ cessitation as inference rules. Recently, Lin and Shoham [1990] defined yet another, this time bimodal, nonmono­ tonic logic, which they called the logic of grounded knowl­ edge (denoted GK), and provided an interpretation of the default logic within logic GK.

*This work Was partially supported by Army Research Of­ fice under grant DAAL03-89-K-0124, and by National Science Foundation and the Commonwealth of Kentucky EPSCoR program under grant RII 8610671.

Each of these approaches has some disadvantages. We discuss them briefly in the next section. In this paper we consider another interpretation of defaults in the modal languae;e. It is somewhat related to the approach of Siegel [1990] to modal nonmonotonic logic 1 · We argue that our translation avoids the problems of the trans­ lations used in the earlier approaches. We show that under this new interpretation, default logic can be faith­ fully embedded into any of the whole range of modal nonmonotonic logics. As a consequence, possible-worlds semantics for these modal logics yield possible-worlds semantics for default logic, and their automated proof methods (whenever exist) can be applied to default the­ ories. For example, in Section 4, we choose logic S4F, that has a particularly well-structured possible-world se­ mantics, to obtain possible-world semantics for default logic.

An important feature of the new translation is that it easily lends itself to an extension suitable for default reasonings with indefinite information in the form of dis­ junction, and generalizes the formalism for such reason­ ings introduced recently by Gelfond [1990]. In Section 5, we introduce this extension, relate it to an earlier work of [Gelfond, 1990] and [Gelfond et al. , 1991], and apply our formalism to discuss the "broken hand" example of Poole [1989].

1 I would like to thank Vladimir Lifschitz who informed me about the work of Siegel after seeing the preliminary version of my paper.

Our results bring up the following general question: how essential in explaining default reasonings are those aspects of modal logics that are specifically concerned with properties of the modality? Earlier investiga­ tions lKonolige, 1988], [Marek and Truszczynski, 1990], [Siegel, 1990], implicitly suggested that there may be some relationship between the properties of the modal­ ity and default logic by centering around the question of what is the right modal logic for the embedding to work (logics K45 [Konolige, 1988], N [Marek and Truszczynski, 1990] and T [Siegel, 1990] were consid­ ered) . But there seem to be no reason for any connection between default reasonings and modal axioms to exist. Default reasonings first use a certain mechanism ( "nega­ tion as failure to prove") to establish defaults applicable in a given situation and then proceed like in a classical first-order case. In the whole process there is no place where properties of the modality (like standard modal axiom schemata) might intervene.

Our results supp'ort this view by showing that there is a significant degree of freedom in the choice of the "host" modal nonmonotonic logic -any out of the whole family of (drastically different) modal nonmonotonic logics will do. An analysis of the translation proposed by Konolige reveals the same "insensitivity" to the choice of modal logic (see [Truszczynski, 1991a]), and Lin and Shoham [1990] make a similar observation in the case of their approach.

2 Previous approaches to the problem of representing default logic as a modal system

Theories in default logic are pairs (D, W), where W is a collection of formulas in some propositional language .C, and D is a collection of nonstandard inference rules, called defaults, that are of the form

To apply default (1) and conclude -y, as in the case of standard inference rules, one first has to establish all its premises. The premises of defaults are of two types. Premise a is treated in a standard way - a has to be proved before the default can be applied. Premises M f3i are treated differently. This is the place when we depart from standard monotone systems. We interpret M f3i as "f3i is possible" (which is emphasized by the use of the modal operator M) and define this as consistency of f3i with some theory S (the potential collection of conse­ quences of a default theory). Thus, M f3i is established if s If -,f3i·

Such treatment of the premises of defaults leads to a nonstandard consequence operator, fv,w(S) [Reiter,

1980]. For a theory W ~ .C, r D,w(S) consists of all facts that can be proven from W by means of propositional calculus and defaults in D, applied as explained above (with S used in consistency checking) . If theory S coin­ cides with the set fv,w(S) of such consequences of W, that is, if

then Sis called an extension of a default theory (D, W) and is regarded as a candidate (many theories S may satisfy (2)) for the set of nonmonotonic consequences of (D,W) .

A similar approach to nonmonotonicity but within the language of modal logic .C L - an extensio~ of .C by a modal operator L interpreted as "is known" - was pro­ posed by McDermott and Doyle [1980] and McDermott l1982]. The operator M, mentioned earlier, is simply an abbreviation for...,£..., . The idea was that modal formulas would play the role of defaults, and the standard conse­ quence operator Cns for a selected modal logic S would replace the nonstandard consequence operator fv,(S). To achieve nonmonotonicity, the theory I encoding the knowledge of a reasoning agent was extended by the for­ mulas expressing "negation as failure to prove" that is, by the formulas ...,£/{) for /{) ¢ T . Theory T (playing the same role as S for default logic) is potentially the col­ lection of nonmonotonic consequences of I. If T agrees exactly with consequences in logic S of IU { -,£/{): /{) ~ T} that is, if

then Tis called an S-expansion of I, and is regarded as a candidate (equation (3) may have multiple solutions) for the set of nonmonotonic S-consequences of I.

A variant of nonmonotonic modal logic was recently introduced by Kaminski [1991] and further studied in [Truszczynski, 1991b] (see also [Konolige, 1988]) . In­ stead of extending I by all formulas given by "negation as failure to prove", I is extended only by the results of application of this rule to modal-free formulas of T. Formally, theory Tis a groundS-expansion of I if

This approach, by restricting the applicability of the "negation as failure to prove" rule to modal-free formu­ las, results in nonmonotonic formalisms more robust to updates in the initial theory I. In addition, since modal nonmonotonic logics based on ( 4) apply "negation as fail­ ure" only to modal-free formulas- all that is required in default logic - they seem especially suitable for study­ ing default reasonings.

Before we continue, let us recall one more important notion. A theory T ~ .CL is stable if it is closed un­ der propositional consequence and necessitation, and if for every /{) ~ T, -,£1{) E T. It is well-known that S­ expansions and ground S-expansions are stable (for the latter to hold, we require that S be normal) . Stable sets are uniquely determined by their objective part [Moore, 1985; Konolige, 1988]. That is, for each S ~ .C there is exactly one stable set T such that Tn .C = Cn( S), where Cn stands for the consequence operator of propositional calculus. We will denote this unique stable set by St(S) .

There have been several attempts to embed default logic into a modal nonmonotonic logic.

(1) Konolige [Konolige, 1988] proposed to interpret a default d given by (1) by the formula

This translation can be extended to a default theory (D, W) by setting

Under this interpretation no modal nonmonotone logic is known to faithfully capture default reasoning. An addi­ tional modification of embK(D, W) is needed. This mod­ ification, involving a stable theory T, yields a subtheory of embK(D, W) referred to as the reduct of embK(D, W) with respect toT. Konolige proved that a consistent and closed under provability theory S is an extension of a default theory (D, W) if and only if St(S) is a ground K45-expansion of the reduct of embK(D, W) with re­ spect to St( S). For the same interpretation, Marek and Truszczynski [1989] showed a similar result: a consistent and closed under provability theory S is an extension of a default theory (D, W) if and only if St(S) is an N­ expansion of the reduct of embK(D, W) with respect to St(S).

The problem with the approach of Konolige is that the concept of reduct is representation dependent - logically equivalent theories may have reducts that are not logically equivalent. Consequently, in modal systems using the concept of reduct, syntactically different but logically equivalent theories may have different conse­ quences. Moreover, as we will argue later, this transla­ tion cannot be used to handle reasonings with disjunc­ tion.

(2) In another paper Marek and Truszczynski [1990] in­ troduced a different translation of the default (1):

Under this interpretation · consistent extensions of ( D, W) correspond exactly to N -expansions of the trans­ lation of (D, W). This was the first result which embed­ ded default logic into a modal nonmonotonic logic in McDermott-Doyle's family. The main disadvantage of this approach is that the interpretation used does not have a natural, intuitive justification.

(3) Lin and Shoham [Lin and Shoham, 1990] do not use the scheme of McDermott and Doyle. They introduce a modal nonmonotonic logic with two modalities. They define semantics of this logic by modifying the concept of preference semantics and faithfully embed default logic into their logic. The solution is elegant but requires two modalities, which introduces an extra degree of complex­ ity.

3 New modal representation of default logic

The translation we propose is based on the most natu­ ral interpretation of a default d = a,Mt!t .... ,M/3,. : if o:, ., M {31 , ... , M f3n are known to an agent then the agent knows 'Y· Such interpretation treats defaults in the same way as standard inference rules are treated - all premises must be known - the only difference is that premises are of two types. This new interpretation can be encoded faithfully in the language of modal logic by the formula

We extend now this definition to the case of default theories. Let (D, W) be a default theory. A modal the­ ory representing (D, W) is defined by

In the rest of the paper, we assume familiarity with ba­ sic concepts of (monotone) modal logic. For all undefined concepts the reader is referred to H uges and Cresswell [1984]. All modal logics considered in this paper con­ tain propositional calculus and use necessitation ( <p / L<p) as an additional inference rule. Besides standard modal logic systems like K, T, S4, S5 and K45, we will con­ sider the following two logics:

1. T- -the logic containing only axiom schema T,
2. S4F - the logic determined by the class of Kripke frames with the accessibility relation of the form (Mt x Mt)U(Mt x M2)U(M2 x M2), where Mt and M2 are disjoint (M1 may be empty) and contain all the worlds of the model. Logic S4F contains logic S4 and is included in logic S5. It can be axioma­ tized by the axiom schemata of S4 and the followng additional axiom F: <p A M L,P => L( M <p V 'if;) (see [Segerberg, 1971]).

Our first theorem contains the main result of the pa­ per.

Theorem 3.1 Let (D, W) be a default theory and let S ~ .C be consistent and closed under propositional con­ sequence. The following conditions are equivalent:

1. S is an extension of (D, W);

2. St(S) = CnT_(emb(D, W) u {-.L<p:<p ft St(S)});

3. St(S) = Cns(emb(D, W) u {-.L<p:<p ft St(S)}), for any modal logicS such that T- ~ S ~ S4F;

4. St(S) = Cns 4 F(emb(D, W) U { -.L<p: <p ft St(S)} ).

Thus, under the translation (7) - (8) for any of a big range of modal logics (T- - S4F) its nonmono­ tonic variant (exactly as introduced in [McDermott and Doyle, 1980; McDermott, 1982]) can be used to express default reasonings, without the need for representation­ dependent concepts like reduct.

Let us now consider representing default reasoning in ground modal nonmonotonic logics. We will again use our new translation of defaults. A similar result to the previous one holds: there is a whole range of logics that can be used for an embedding.

Theorem 3.2 Let S be any logic such that T ~ S ~ S4F. A consistent and closed under propositional prov­ ability theory S is an extension of a default theory (D, W) if and only if St(S) is a groundS-expansion of emb(D, W) .

This theorem will be used in the next section in a def­ inition of a possible-words semantics for default logic, where logic S4F, which has a relatively simple Kripke­ model characterization is selected as a modal counter­ part of default logic.

Even larger range of equivalent logics, in the sense of faithful representation of default reasoning, can be found if the concept of ground expansion is combined with the concept of the reduct of emb(D, W) In such case any of the logics from the range T - S5 can be used. Similarly, for the original approach of Konolige [1988] (translation embK combined with the concept of reduct), we can prove that any of the modal logics in the range K - S5, and not only logic K45 used in [Konolige, 1988], allows us to faithfully encode default logic (see [Truszczynski, 1991a] for details) .

4 Possible-worlds semantics for default logic

In the previous section we have presented two results embedding default logic into nonmonotonic modal logics of McDermott and their ground variants. In each case we have a significant degree of freedom in choosing the underlying monotone logic. In this section, we make use of this freedom. Our approach is based on· Theorem 3.2, and for logic S we choose S4F.

A (default) model is a triple M = (M1 , M2, V}, where M1 and M2 are sets such that M1 nM2 = 0 and M2 :f. 0, and V is a function assigning to each m E M a proposi­ tional valuation V(m).

We say that a formula I{) is true (holds) in a world m of Mt U M2 if I{) is true in the valuation V(m) (in symbols: (M, m) I= 1{)). We say that a pair (M, m), where m E M1, satisfies default (1) (in symbols, (M, m) I= d) if whenever a is true in all worlds in M1 U M2 and each f3i holds in at least one world of M2 , then 'Y holds in all worlds in M~ U M2 . We say that a pair (M, m), where mE M2, satisfies default (1) ((M, m) I= d) if whenever a is true in all worlds in M2 and each f3i holds in at least one of the worlds in M2 , then 'Y holds in all worlds in M2. In a standard way, we define now satisfiability of a default by a model. Namely, M f= d, if ( M, m) f= d for each m E M1 U M2 . In a similar fashion, we define ~atis~ability of a formula by a model: for I{) E .C, M f= I{) If I{) IS true in all worlds from M1 U M2.

Note that for each model M there is an equivalent model M' = (M{, M~, V') (that is, for each default d, M I= d if and only if M' I= d) such that valuations assigned to worlds in Mf, i = 1, 2, are distinct. Conse­ quently, if .C has only finitely many propositional vari­ ables, then each model has an equivalent finite model.

In commonsense reasoning we often restrict the class of models by imposing additional conditions. For example, Moore's autoepistemic interpretations of the language .CL [Moore, 1985] are defined with respect to a theory T ~ .CL, called the modal index of an interpretation. A valuation v of .CL is autoepistemic with respect to T if v(LI{)) = 1 if and only if I{) E T. The class of autoepis­ temic interpretation has been used by Moore to define the concept of stable expansion and the nonmonotonic formalism called autoepistemic logic.

In this paper, we proceed similarly. Let S ~ .C. A

model M is called strongly consistent with S

Let (D, W) be a default theory. We say that (D, W) S-entails a, where a stands for a default or for a formula from .C, if a is satisfied in all models strongly consis­ tent with S in which (D, W) is satisfied. We denote the relation of S-entailment by l=s. We have the follow­ ing theorem providing a characterization of extensions analogous to Moore's definition of stable expansions by means of autoepistemic interpretations.

Theorem 4.1 Let (D, W) be a default theory. LetS~ .C. Theory S is an extension of (D, W) if and only if

that is, if S is exactly the set of all formulas true in all S-models of(D, W).

5 Effective disjunction

One of the problems of nonmonotonic formalisms often is that the semantics of the disjunction operator does not accurately capture the intuitive understanding of disjunction [Poole, 1989; Gelfond, 1990]. We will show that our embedding of defaults can be used to handle disjunction. In commonsense reasoning we often use a "constru_ctive" or "effective" disjunction- knowing aVb, each behef set an agent will construct will contain a or b - instead of the classical, nonconstructive interpreta­ tion in which we may know aV b without knowing which of the two disjuncts is true. The distinction between the two can easily be achieved in the modal language. The "constructive" disjunction can be expressed as La v Lb and the "noneffective" one by L(a V b).

Let us consider the following example due to Poole [~oole, 1989]. Suppose that normally people's left (resp. nght) arms are usable and people with broken left (resp. right) arms are exceptions. Suppose also that we remem­ ber seeing a friend with a broken arm, but we cannot re­ member which. Intuitively, we should not conclude that both his arms are usable. A straightforward default en­ coding of this situation by a default theory (D, W) is as follows:

and

Clearly, this default theory has exactly one extension and it contains the formula u,A Ur, contrary to the intuition.

The reason for the inadequacy of the default logic to handle such situations is that default logic does not have a mechanism to deal with effective disjunction. Recently an extension of default logic was proposed in [Gelfond et al., 1991] which commonsense disjunction is expressed by means of a new connective. In this extension of default logic the abovementioned paradox disappears.

Let us now consider the encoding of the above situa­ tion using modal disjunctive defaults of the form:

Using such formulas, the Poole's example can be encoded as follows (recall that M = -,£-,):

Consider now logic 54. In [Shvarts, 1990; Marek et al., 1990] 54-expansions are characterized and algorithms to compute them described. Using these results, one can find that the above theory has two 54-expansions: one generated by { ab,, b,, Ur} and the other generated by { abr, br, u,}, which coincides with the intuition. The same result can be obtained for any logic from the range T-- 54F.

In fact, more can be shown. Namely, each nonmono­ tonic logicS, for logics S such that T- ~ S ~ 54, and each ground nonmonotonic logicS, for logics S such that T ~ S ~ 54F, can be used as a nonmonotonic system capable of distinguishing between "effective" and "non­ effective" disjunction. These issues will be discussed in detail in the full version of the paper.

Let us briefly mention here that formulas used to rep­ resent default proposed by Konolige [1988] and Marek and Truszczynski [1990] cannot be extended to handle disjunction, because they use modal-free formulas to rep­ resent consequents of defaults and, thus, cannot distin­ guish between the "effective" and "noneffective" inter­ pretations of disjunction.

6 Conclusions

In the paper we presented a new and natural interpre­ tation of defaults as modal formulas. We have shown that under this interpretation there are whole families of modal nonmonotonic logics that accurately represent default reasoning. We proposed a semantics for default logic based on the embedding we found.

We also have shown that the disjunctive information can easily be handled within our modal system. disjunc­ tive defaults.

A very important conclusion of this research is that there is no single, distinguished modal logic for describ­ ing default reasoning. On the contrary, there exist whole ranges of modal logics, each of which can be used in the embedding as a "host" logic. This shows that, in agreement with the intuition, in order to capture default reasoning the most important step is to translate into a nonmonotonic modal system the principle of "negation as failure to prove". Once this is made, then the choice of particular modal axiom schemata is of secondary im­ portance, in fact, there is a large degree of freedom in which of them to choose.

7 Proof of Theorem 3.1

Let us define in a precise way the operator r D,w(S) . To this end, let us introduce a formal system PC+ (D, S) as the formal system containing propositional calculus and an additional set Ds of inference rules, where Ds = { !!.: a,Mt!t, ... ,Mp,. E D and S I./ ..,a. 1 < i < n}. By 'Y 'Y '/ 1-'·· - - fD,w(S) we denote the set of all formulas that have a proof from W in the system PC+ (D, S) . It is well­ known that fD,w(S) can alternatively be defined as the minimal set closed under provability in PC+(D, S) that is, the minimal set closed under propositional provability and the rules in Ds (this is the original definition of fD,w(S) given in [Reiter, 1980)).

Throughout the proof we use the following abbrevia­ tions: T = St(S) and I = emb(D, W). The reduct of emb(D, W) with respect to St(S) (in symbols: In) is the theory containing {Lcp: cp E W} and formulas La=> L1, such that for some Pt, ... pn, a,Mfh, ... ,M/3,. ED and for ..., all i, -,pi fl. S. In= R(emb(D, W), St(S)). We will also use the following facts listed below:

Pl: For a normal mqdal logic S, and for S ~ .C, if S ~ Cns(I u { -,£cp: cp, E .C \ St(S)} ), then St(S) ~ Cns(I U { -,£cp: cp E .C \ St(S)}) ([Truszczynski, 1991b]). For any modal logic S containing necessitation, and for S ~ .C, if S ~ Cn5 (Iu{-,Lcp:cp fi St(S)}), then St(S) ~ Cns(I U { -,£cp: cp fi St(S)}) ([Marek and Truszczynski, 1990]);

P2: If S ~ T ~ 55 are two modal logics with necessi­ tation, then each S-expansion of I is aT-expansion of I ([McDermott, 1982]);

P3: Logic 55 is complete with respect to the class of universal Kripke models that is, models with a universal accessibility relation ([Hughes and Cresswell, 1984]);

P4: Each consistent stable set is of the form { cp: M F cp}, for some universal Kripke model M [Moore, 1984]; P5: Stable sets are closed under provability in 55 ([Mc­ Dermott, 1982]);

P6: A theory S ~ .C closed under propositional con­ sequence, is closed under rules in Ds if and only if emb( D, W) ~ St( S) if and only if In ~ St( S) (straight­ forward to prove) .

1 => 2. Assume that S = fD,w(S) . Then, if cp E S , cp has a proof cp1 , ... , IPn ( = cp) from W in the system PC+ Ds. We will show, by induction on the length of the proof, that cp E CnT- ( emb(D, W) U { -,£cp: cp fi T} ). Assume that the claim holds for all formulas in S with proofs of length < n . If IPn(= cp) is a tautology or is a member of W, then cp E CnT_(emb(D, W) U {-,Lcp:cp fi T}). If IPn is obtained from l;?i, l;?j, where i,j < n, by means of modus ponenes, then the induction hypothesis appliesandcpi,l;?j E CnT_(emb(D, W)u{-,Lcp:cp fiT}) . Consequently, cp E CnT_(emb(D, W) U {-,Lcp: cp fl. T}).

The last possibility is that IPn is obtained from l;?i, i < n, by means of a rule !£..i.. E Ds . Then, "'" there is a default d = <p ; ,Mfb,····MPm E D such "'" that all -,pi fi S . Consequently, all £-,£-,pi E CnT_(emb(D, W) U {-,Lcp:cp fl. T}). By the induction hypothesis, ~Pi E CnT_(emb(D, W) u {-,Lcp:cp fl. T}) . Thus, Lcpi E CnT_(emb(D, W)u{-,Lcp: cp fl. T}). More­ over, emb(d) = Lcpi 1\ £-,£-,pl 1\ ... 1\ £-,£-,Pm => Lcpn is a member of Cn'J'_ (emb(D, W) U {-,Lcp: cp fl. T}) (re­ call that M = -,£...,) . Thus, Lcpn E CnT- (emb(D, W) U { -,£cp: cp fi T} ). Applying axiom T, we get that ~Pn( = cp) E CnT_(emb(D, W) U {...,Lcp: cp fl. T}).

By P1, it follows that St(S) ~ CnT- (emb(D, W) U { -,£cp: cp fi T} ). To prove the converse inclusion, observe that St(S) is closed under provability in T- (by P5), St(S);;;;? emb(D, W) (since S is an extension of (D, W) , Sis closed under rules from Ds and P6 applies) . Finally, since T = St(S) and St(S) is stable, { -.Lt,o: <p rl. T} ~ St(S) .

2 => 3 and 3 => 4. These implications follow by P2. 4 => 1. The definition of the reduct yields

Cns4F(Iu{-.L<p:<p rt T}) = Cns4F(IRU{-.L<p: <p rt T}).

Thus, St(S) = Cns4F(IR U {-.L<p: <,0 rt St(T)}). Next, we will show that

St(S) = Cn55(IR U {-.L<p: <,0 E .C \ T} ).

Since T is stable, T is closed under provability in S5 (by P5). In addition, { -.L<p: <p E .C \ T} ~ T. Thus, Cnss(IRU{ -.L<p: <p E .C\T}) ~ T. To prove the converse inclusion it suffices, by P1, to show that

S ~ Cnss(IR U { -.L<p : <,0 E .C \ T} ).

Consider <p E S and any universal Kripke model M = (M,R, V} such that M f= lRU {-.L<p:<p E .C\ T}. Let M' = (M', R', V'}, M n M' = 0, be a universal Kripke model such that T = {'rP: M' f= 1/1} (apply P4) . De­ fine .N = (M", R", V"}, by letting M" = M u M', R" = R U (M x M') U R' and V" = V U V'. It follows from the definition of .N that .N, m' F= { -.L<p: <p rl. T}, for every m' E M'. Thus, also for every m E M, .N, m f= { -.L<p: <p rl. T}. Next, it is easy to see that if 1/1 E .C then .N, m f= 1/1 if and only if M, m f= 1/1, and .N, m f= L,P if and only if M, m f= L,P. Thus, for ev­ ery mE M, .N,m f= JR. Since IR ~ T, M',m f= IR, for every m E M'. Consequently, .N, m f= IR, for ev­ ery m E M'. Summarizing, .N f= lR U {-.L<p : <p rl. T}. By the definitions of the model .N and of the logic S4F, it follows that .N f= <p . Thus, M f= <p and, by P3, <,0 E Cnss(IR U {-.L<p: <,0 E .C \ T}).

Now, St(S) is a ground 55-expansion of IR and, by a result of Kaminski [Kaminski, 1991], St(S) is a min­ imal stable theory containing lR. Consequently, S is a minimal set closed under rules from Ds . Hence, Sis an extension of ( D, W) . D