Preservation Properties in Deductive Data Bases

Marek A. Suchenek
California State University - Dominguez Hills
Carson, CA 90747 U.S.A.
e-mail addr: Suchenek@csudh.edu

1992

lht[thm]Lyndon Theorem

Key words: circumscription, closed-world assumption, default assumptions, domain-closure axiom, unique-names assumption, model theory for non-monotonic logics, preference relations.

AMS classification: 68G99, 03C40, 03C52.

Abstract

Given set of premises S, assume j if and only if, for every g Î G, SÈ{j} does not entail g unless S does,

1  Introduction

In this paper, we investigate instances of the following scheme D of default reasoning:

If the assumption j doesn't introduce unwanted consequences to the set of premises S then assume j.

G0 È{ M( jÙØg1) , ... , M( jÙØgk) } j

(1)

where G₀ ranges over consistent subsets of G, and g₁ , ... , g_k are all elements of G\G₀. For instance, if formula false is the only unwanted consequence then (1) may be reduced to a single normal default:

{ M( j) } j .

To express D in the general case of infinite G, one must admit infinitary default rules of inference. For this reason, we will utilize a different way of formalizing default schemes of this kind.

Using the default scheme D in the context of reasoning from an arbitrary set of premises of S involves a subtlety. If S itself entails consequences that are unwanted, then the requirement ``j doesn't introduce unwanted consequences" should be understood as ``j doesn't entail any unwanted consequence, unless this unwanted consequence is already entailed in S". This observation, given the set G of all unwanted consequences, leads to the formalization of D by the following postulate:

Assume j if and only if, for every g Î G, SÈ{j} does not entail g unless S does.

The consistency of DA_G(S) seems to be a serious problem that is reportedly common to all kinds of default rules. In particular, it may happen that each of a pair j, y of inconsistent sentences separately does not add any unwanted consequences to S, and then both of them are included in DA_G(S), making DA_G(S) inconsistent. In this paper, we have managed to avoid this problem by restricting both S and DA_G(S) to sentences which do not reveal such pathological behavior. Most notably, clauses, or universally quantified sentences, do not cause this type of a problem for appropriately chosen G. As a result of this precaution, the instances of the G-default assumption which are studied here may be treated as rules of inference and used whenever applicable, without contradicting the other uses of the same instance of G-default assumption. This desirable proof-theoretic property frees us from fixed-point equations which seem inevitable for the default rules that do not possess this feature.

Consistency of DA_G(S) creates the possibility of characterizing it in terms of its models, which is an object of our primary concern. A question which we will attempt to address to the fullest extent possible is:

Given G, what semantics assigns to every S from the domain of DA_G the class of first-order models of DA_G(S)?

j Î DA_G(S) if and only if every finest model of S is a model of j.

2  Prerequisites from Logic and Algebra

We apply the standard terminology and notation of first-order model theory, a good account of which can be found in [], Chap. A2. We restrict ourselves to a first-order language L with logical connectives Ù (and ), Ú (or ), Ø (not ), " (for all ) and $ (there exists), and treat all other connectives as abbreviations. In addition to predicates, L contains constants and the equality symbol =¹, and may contain function symbols. We identify L with the set of its all formulas. To avoid confusion with connectives of L, we apply beyond L the informal quantifiers Ù and Ú as abbreviations for for all and there exists. For instance,

Ù j Î L  "x j Î L

means:

For every formula j of L, "x j is a formula of L.

A formula j is atomic if and only if no logical connective appears in j. For example, x = f(d) is an atomic formula. A "-formula is a formula of the form "x₁ "x₂ ..."x_n j (abbreviated as "[] j), where j is quantifier-free. Similarly, an $-formula is a formula of the form $x₁ $x₂ ... $x_n j (abbreviated as $[] j), where j is quantifier-free. A sentence is a formula without free (i.e., unquantified) variables. Atom denotes the set of all atomic sentences of L; QF denotes the set of all quantifier-free sentences of L; and " and $, when used in appropriate context, denote the set of all "-sentences and the set of all $-sentences of L, respectively.

"-sentences seem to play a very important role in artificial intelligence. In particular, every clause is logically equivalent to a "-sentence. Also, every "-sentence is logically equivalent to a finite set of clauses. Therefore, in this paper "-sentences are given special attention. Moreover, we identify sets of clauses with subsets of ", and sets of ground clauses with subsets of QF. Obviously, this can be done without loss of generality.

S_L denotes the class of all first-order structures for L. We usually denote its elements by A, B, M, N, ..., and their respective domains by A, B, M, N, ...,. If F is a function symbol of L then F^M denotes the corresponding function in M. Analogously, R^M denotes the relation in M corresponding to the predicate R. The satisfaction relation is denoted by , so that M j[s] means that formula j is satisfied in structure M by assignment s on its free variables (formally, s is a function from variables of L into the domain M of M). If j is satisfied in M by every assignment s then M j is used instead of M j[s]. In such a case we say that j is true in M. If j is a sentence of L then for every assignment s in M, M j[s] is synonymous with M j. We use M Í N, to mean that M is a substructure of N, if and only if M Í N, and for every predicate or function symbol F of L, F^M = F^N | \` M, where `` | \` " means ``restricted to".

A theory S in L is a set of sentences of L. Here we usually denote formulas by lower-case Greek letters, and theories by upper-case Greek letters. We write M S to express that for every j Î S,  M j. M S means that all elements of S are true in M, that is, the structure M is a model of S. We denote the class of all models of S by Mod(S). We make an implicit use of the completeness theorem of first-order logic by applying Sj in the sense Mod(S) Í Mod(j), so that Sj means that j is true in every model of S. If f is a function from subclasses of S_L into subclasses of S_L then _f is a relation defined by:

Ù S Í L  Ù j Î L  Sf j if and only if Mod(S)  Çf(Mod(S)) Í Mod(j).

(2)

S_f j means that j is true in all models of S that are in f(Mod(S)), but not necessarily in all models of S. Relations and _f are called entailments.

We use Cn(S) to denote the set { j | Sj} of all first-order consequences of S within the language L. We say that S₁ is logically equivalent to S₂ if and only if Cn(S₁) = Cn(S₂), or equivalently, if and only if Mod(S₁) = Mod(S₂). Moreover if G is a set of sentences of L then we use S_G to denote the set Cn(S) ÇG. In particular, S_L coincides with Cn(S).

The notion of relative positiveness and negativeness are the key concepts which allow for proper articulation of default assumptions that are "-complete with respect to various versions of minimal semantics.

Let  be a set of predicates of L. Our intention is that  contains all predicates which are being minimized, while the predicates not in  remain constant. A formula is positive in a symbol R if and only if it does not contain an appearance of R in a scope of a negation². It is positive if and only if it is positive in every predicate in  and in the equality symbol =. A formula is negative in R if and only if it is a negation of a formula which is positive in R. In this paper, Pos _{{ = } ¢} denotes the set of all "-sentences which are positive in all predicates in  (symbol ``¢" in Pos _{{ = } ¢} indicates that = is excluded from the requirement of positiveness), Pos _{{ = }} denotes the set of all "-sentences which are positive in =, Pos (the intersection of Pos _{{ = } ¢} and Pos _{{ = }} ) denotes the set of all positive "-sentences, and Neg _{{ = }} denotes the set of all "-sentences which are negative in =. Let us note that elements of Pos may contain negative occurrences of predicates from beyond Â.

A conservative homomorphism on M into N is a mapping f : M® N such that for each atomic formula j without an occurrence of the symbol =, and assignment s in M,

M j[s] iff N j[s °f],

and for each term t and assignment s in M,

f(tM(s)) = tN(s °f),

where ° is the composition operator. Conservative homomorphism f on M defines unambiguously the structure N such that f : M [ on || (® )] N. We denote such a structure by fM. Structure M is isomorphic with structure N if and only if there is a one-to-one conservative homomorphism from M onto N. Isomorphic structures are indistinguishable in the sense that thy possess the same mathematical properties. In particular, they satisfy exactly the same formulas of L. For these reasons we treat any pair of isomorphic structures as if they were equal.

If µ is a binary relation on a class S then a subclass K of S is called upward µ -closed if and only if M Î K and M µ N imply N Î K. The upward µ -closure Clo^­ _µ (K) of K is defined as the least upward µ -closed class containing K as a subset. If µ is a reflexive and transitive relation then

Clo­ µ (K) = { N Î S | Ú M Î K  M µ N } .

(3)

Class K is called µ -dense in class J if and only if

Ù M Î J  Ú N Î K ÇJ  N µ M.

(4)

If µ is a reflexive and transitive relation then class K is µ -dense in class J if and only if J Í Clo^­ _µ (K ÇJ). If K is µ -dense in J and K ÇJ is µ -dense in I then K is µ -dense in I, also.

Transitive and reflexive closure of a relation µ is denoted by µ ^*. If µ ₁ and µ ₂ are binary relations on S then µ ₁ ° µ ₂ denotes their composition, and µ ₁ + µ ₂ denotes their combination, that is, the relation ( µ ₁ È µ ₂)^*. If µ ₁ and µ ₂ are reflexive and transitive then µ ₁ + µ ₂ = ( µ ₁ ° µ ₂)^*. Let us note that µ ₁ ° µ ₂ is not necessarily a transitive relation, even though µ ₁ and µ ₂ are. However, if µ ₁, µ ₂ and µ ₁ ° µ ₂ are reflexive and transitive then µ ₁ + µ ₂ = µ ₁ ° µ ₂; the converse is true as well. We call µ a partial order if, in addition to being reflexive and transitive, it is antisymmetric, that is, it satisfies the following postulate:

Ù N,M Î S  N µ M and M µ N implies N = M.

(5)

3  Model Refinements

It turns out that appropriately chosen preference relations, which we call here refinements, constitute semantical counterpart of G-default assumption. The purpose of a refinement is to modify a model M of a set of sentences S to another model N of S, which satisfies more consequences of an instance of G-default assumption in question and, in effect, better approximates the reality that S under this default assumption is supposed to describe. Consequently, the mostly preferred models of S which cannot be further refined will provide DA_G(S) with adequate semantics. In Sections and we will determine which refinements are appropriate matches for selected instances of the G-default assumption. Here, we define refinements as binary relations between first-order structures of S_L, and state their basic properties.

A refinement, usually denoted by µ (possibly with subscripts), is a partial order on the class S_L of first-order structures for L. N µ M expresses the fact that N is a refinement of M. Given K Í S_L, the class fin _µ (K) of µ -finest structures in K is defined by

fin µ (K) = {M Î K | Ù N Î K  (N µ M É M = N)}.

(6)

The entailment is incomplete with respect to the µ -finest semantics. Indeed, a sentence j that is not provable from S by means of , or in other words, is false in some elements of Mod (S), may be true in all elements of fin _µ (Mod (S)). This fact motivates our interest in the entailment_{fin µ} , denoted for simplicity by _µ , which by definition (2) is complete with respect to the µ -finest semantics. Since fin _µ (K) always is a subset of K, _µ is characterized by the following instance of (2):

S µ j iff fin µ (Mod (S) ) Í Mod (j).

(7)

S _µ j means that j is true in all µ -finest models of S. We call _µ a refined entailment. Of course, if S j then S _µ j, but the converse is not necessarily true.

A subclass K of S_L is called µ -flat if and only if,

Ù M, N Î K  M µ N implies M = N.

(8)

Obviously, by (6), every class of the form fin _µ (K) is flat, but not vice versa.

We focus on the following instances of the refinement µ . It is a matter of routine inspection to check that all these instances are partial orders.

3.1  Predicate Minimization

(M £ N) if and only if (M = N, and for every function symbol F of L,  F^M = F^N, and for every predicate symbol P not in Â, P^M = P^N, and for every predicate symbol R in Â, R^M Í R^N).

Following generally accepted convention, we call £ -finest models predicate-minimal models.

3.2  Domain Minimization

The very relation Í between first-order structures comprises our second instance of refinement. It formalizes the Ockham's razor principle in this sense, that the domains of Í -finest structures consist only of necessary individua, namely of interpretations of constant³ terms of the language L. We call Í -finest structures domain-minimal structures. Not every consistent set of sentences has a model being a domain-minimal structure. For example, { $xP(x) } È{ ØP(t) | t is a constant term of L } has not. However, for every theory S Í ", each domain-minimal substructure of a model of S is a model of S.

Domain-minimal structures are also known under the name domain-closed structures.

3.3  Gluing

M N iff there exists a conservative homomorphism f such that M = fN.

The nature of the refinement lies in gluing together certain elements of the domain of a model if they satisfy the same atomic and negated atomic sentences of L. Therefore, may be used to minimize the domains of first-order structures, albeit, in a different sense than Í . For instance, in a language with one unary predicate P and three constants a, b, and c, each -finest model of { P(a), ØP(b), ØP(c) } has the domain consisting of two elements: one to interpret a and another to interpret b and c.

3.4  Discrimination

Oddly enough, something quite converse to gluing , namely discrimination, seems to be a matter of interest in deductive databases and logic programming. Discrimination may be defined as the inverse of gluing restricted to elements of the domain which are values of the constant terms of L. We denote the relation of discrimination by . M N means that there is a conservative homomorphism f of M onto N, such that f(m₁) = f(m₂) holds only if, for some constant terms t₁ and t₂ of L, m₁ = t₁^M, and m₂ = t₂^M. In particular,

M N implies Ú A Í M  A M.

(9)

Models which are -finest are called discriminant, or, in the extreme case, when every two non-identical constant terms are assigned different values, they are called strongly discriminant. For instance, if f is a function symbol and c is a constant of L then each strongly discriminant structure satisfies Ø(f(c) = c). Discriminant models constitute a semantic counterpart of the so called unique-names assumption.

The restriction to strongly discriminant semantics is necessary for the validity of many published completeness proofs of negation-as-failure and similar procedures. This is most likely the reason of popularity of discriminant models. Of course, if S contains occurrences of the equality symbol, for instance, a sentence a = b, there may be no strongly discriminant models of S. However, we will show in subsection that for every consistent S Í ", there are always discriminant models of S, which are strongly discriminant if = does not occur in S.

3.5  Combinations

It turns out that the most interesting in applications are certain combinations of the above instances of µ . For example, the combination of Í and leads to the concept of the Herbrand (i.e., domain-minimal and discriminant) structure, or, in the extreme case to strongly Herbrand (i.e., domain-minimal and strongly discriminant) structure. The combination of the three refinements: Í , , and £ yields in the extreme case the concept of a minimal strongly Herbrand structure. This notion plays a fundamental role in model theory for deductive databases and logic programming.

Combinations of refinements are the central point of our interest. They are the subject of systematic study in Section .

3.6  Densly Founded Theories

If certain theories have models which cannot be refined to µ -finest models than the entailment _µ may reveal an irregular behavior. In particular, if a consistent theory S has no µ -finest models at all (e.g., in the language with a unary predicate symbol N, the usual inductive definition of natural numbers with the postulate ``N(0)" being replaced by ``$x N(x)", has no predicate-minimal models) then S entails false, which is decidedly an unwanted consequence. This troubled situation cannot happen if every S Í " is µ -densly founded, that is, if class fin _µ (Mod (S)) is µ -dense in Mod (S). Fortunately, this is the case for all the refinements considered in this paper.

Lemma 1

For every S Í ",

1. fin _£ (Mod (S)) is £ -dense in Mod (S).
2. fin _Í (Mod (S)) is Í -dense in Mod (S).
3. fin(Mod (S)) is -dense in Mod (S).
4. fin(Mod (S)) is -dense in Mod (S).

Lemma 3.6 is surprisingly strong. For instance, 3.6 implies the compactness theorem of "-fragment of first-order logic. In Section we will generalize Lemma 3.6 over combinations of refinements.

4  Simple Preservation Properties

Let G be a set of "-sentences of L. The G-default assumption DA_G introduced in Section 1 is formally defined as a consequence operation from subsets of " into subsets of ", given by:

Ù S Í "  Ù j Î L  j Î DAG (S) iff j Î " and (SÈ{ j} ) G = SG .

(10)

DA_G assumes, by default, a clause j if and only if j does not introduce new G-consequences to S. For j Î ", scheme (10) generalizes (1) over infinite G's; one can check that if G is finite then a working instance of (1) can be obtained by putting G₀ = S_G.

It turns out that those G's, whose elements' truthfulness is upward µ -preserved, yield instances of G-default assumption which are "-complete with respect to the refined entailments _µ .

Definition 1 We call a set G of sentences of L a complete preservation property with respect to the refinement µ , in abbreviation: CPP(G, a), if and only if,

Ù S Í "  Mod(SG) = Clo­ µ (Mod (S)).

(11)

^[¯]

In other words, CPP(G, µ ) means that for every S Í ", Mod (S_G) is the least upward µ -closed class containing Mod (S) as a subset. Because we assumed that refinements are partial orders, in particular reflexive and transitive, CPP(G, µ ) holds if and only if for every S Í " and every A Î S_L,

A SG iff Ú M µ A  M S.

(12)

CPP(G, µ ) implies that any "-axiomatizable subclass of S_L is upward µ -closed if and only if it is axiomatizable by a subset of G. In particular, for every j Î G, if M j and M µ N then N j. Thus µ preserves the truthfulness of sentences of G. Moreover, for every sentence j of L whose truthfulness is preserved under µ there is a finite G₀ Í G with j º ÙG₀. In this sense G is a complete preservation property.

The notion of complete preservation property constitutes a fundamental concept which allows us to establish the "-completeness of the G-default assumption with respect to refined entailment _µ .

The Completeness Theorem 2 Assume that CPP(G, µ ) holds. For every µ -densly founded S Í " and j Î ",

S µ j iff j Î DAG ( S).

Proof. We show that under these assumptions, S _µ j if and only if (SÈ{ j})_G = S_G. Indeed, S _µ j iff [by definition (7) of _µ ] fin _µ (Mod (S)) Í Mod(j) iff Mod(j) is µ -dense in fin _µ (Mod (S)) iff [by µ -densly foundedness of S, that is by µ -density of fin _µ (Mod(S)) in Mod(S)] Mod(j) is µ -dense in Mod(S) iff [by (3) and reflexiveness and transitivity of µ ] Mod(S) Í Clo^­ _µ (Mod(S) ÇMod(j)) iff Mod(S) Í Clo^­ _µ (Mod(SÈ{ j} )) iff [by CPP(G, µ ) and (11)] Mod(S) Í Mod((SÈ{ j} )_G). Observation that S_G Í (SÈ{ j})_G always holds completes the proof. ^[¯]

We demonstrated in Section 3 (Lemma 3.6) that all the instances of µ discussed there satisfied the requirement that "-theories are µ -densly founded. Here, we establish their complete preservation properties.

Lemma 3

The following complete preservation properties hold:

1. CPP(Pos _{{ = } ¢} , £ ),
2. CPP(QF , Í ),
3. CPP(Neg _{{ = }} , ),
4. CPP(Pos _{{ = }} , ),

Now, Theorem 4 yields automatically the appropriate "-completeness results.

Theorem 4 For every S Í " and every j Î ",

1. S_£ j iff j Î DA_{Pos { = } ¢} ( S)
2. S _Í j iff j Î DA_QF ( S)
3. S j iff j Î DA_{Neg { = }} ( S)
4. Sj iff j Î DA_{Pos { = }} ( S)

The above theorem makes it clear that the Pos _{{ = }¢}-default assumption expresses the predicate circumscription, the QF-default assumption expresses the domain closure axiom, and the Pos _{{ = }} -default assumption expresses the unique-names assumption.

DA_{Pos { = }¢} was first introduced as an instance of operation cwa_S, and proven complete with respect to entailment _£ in [].

5  Composed Preservation Properties

In this section, we investigate combinations of refinements. We prove that the resulting "-complete default assumptions are straightforward combinations of the simple ones.

We start with technical lemmas (Lemmas - ) which yield a handy tool for surgically clean analysis of the following combinations of instances of µ that were introduced in Sections 3 and 4:

• simultaneous predicate minimization and domain minimization (we call it a total minimization),
• predicate minimization with discrimination,
• domain minimization with discrimination, and
• total minimization with discrimination.

Lemma 1

Assume that µ ₁ ° µ ₂ is transitive. Then for every K Í S_L,

Clo µ 2­(Clo µ 1­(K)) = Clo µ 1­(Clo µ 2­(Clo µ 1­(K))) .

(13)

Proof. It suffices to show that Clo _{µ 2}^­(Clo _{µ 1}^­(K)) is upward µ ₁-closed. Let M Î Clo _{µ 2}^­(Clo _{µ 1}^­(K)), and M µ ₁ N. By the reflexiveness of µ ₂ we get M µ ₁ ° µ ₂ N. By (3) we obtain Ú_{A,B Î K}A µ ₁ B µ ₂ M, that is, Ú_{A Î K}A µ ₁ ° µ ₂ M. The transitivity of µ ₁ ° µ ₂ yields Ú_{A Î K}A µ ₁ ° µ ₂ N, that is, by (3) again, N Î Clo _{µ 2}^­(Clo _{µ 1}^­(K)). Thus Clo _{µ 2}^­(Clo _{µ 1}^­(K)) is upward µ ₁-closed. ^[¯]

We say that sets G₁ and G₂ possess the intersection property if and only if every subset of G₁ logically equivalent to a subset of G₂ is logically equivalent to a subset of G₁ ÇG₂. For instance, one can show that the sets " and $ possess the intersection property (note that "Ç$ = QF).

The following lemma is interesting in its own right since it generalizes classic results of Craig [] and Lyndon [].

Interpolation Lemma 2

Assume that CPP(G₁ , µ ₁) and CPP(G₂ , µ ₂) hold, µ ₁ ° µ ₂ is a partial order, and G₁ and G₂ posses the intersection property. Then

Ù S Í "  Mod(SG1 ÇG2) = Mod((SG1)G2).

(14)

Proof. S_{G1 ÇG2} = Cn(S) ÇG₁ÇG₂ Í Cn(Cn(S) ÇG₁) ÇG₂ = (S_G1)_G2. Hence, Mod((S_G1)_G2) Í Mod(S_{G1 ÇG2}). Therefore, it suffices to prove that Mod(S_{G1 ÇG2}) Í Mod((S_G1)_G2). Indeed, Mod((S_G1)_G2) = [by CPP(G₂, µ ₂) and (3)] Clo^­ _{µ 2}(Mod(S_G1)) = [by CPP(G₁, µ ₁) and (3)] Clo^­ _{µ 2}(Clo^­ _{µ 1}(Mod(S))) = [by Lemma 5] Clo^­ _{µ 1}(Clo^­ _{µ 2}(Clo^­ _{µ 1}(Mod(S)))) = [by similar argument] Mod(((S_G1)_G2)_G1). Because ((S_G1)_G2)_G1 Í G₁ and (S_G1)_G2 Í G₁, the intersection property of G₁ and G₂ yields P Í G₁ ÇG₂ with Mod((S_G1)_G2) = Mod(P). Since Mod(S) Í Mod((S_G1)_G2), we have Mod(S) Í Mod(P), therefore P Í S_{G1 ÇG2}. Hence, Mod(S_{G1 ÇG2}) Í Mod(P). Thus Mod(S_{G1 ÇG2}) Í Mod((S_G1)_G2). ^[¯]

To see the ``interpolation" in Lemma 5 let us note that (14) can be equivalently expressed by:

Ù P Í G1  Ù j Î G2  (P j implies Ú Q Í G1 ÇG2  (P Q and Q j)),

where P Q is an abbreviation for Ù_{J Î Q} P J.

Now, we prove that CPP is preserved under combinations of refinements.

Lemma 3

Assume that CPP(G₁ , µ ₁) and CPP(G₂ , µ ₂) hold, µ ₁ ° µ ₂ is a partial order, and G₁ and G₂ have the intersection property. Then CPP(G₁ ÇG₂, µ ₁ + µ ₂) holds.

Proof. We must prove that

Ù S Í "  Mod(SG1 ÇG2) = Clo­ µ 1 + µ 2(Mod(S)).

(15)

Because µ ₁ + µ ₂ is reflexive and transitive, it suffices to demonstrate that for every S Í " and A Î S_L,

A SG1 ÇG2 iff Ú M µ 1 + µ 2 A  M S.

(16)

By Lemma 5, Mod(S_{G1 ÇG2)} = Mod((S_G1)_G2). Therefore, A S_{G1 ÇG2} iff A(S_G1)_G2 iff [because of CPP(G₁, µ ₁, CPP(G₂, µ ₂, and (3)] A Î Clo^­ _{µ 2}(Clo^­ _{µ 1}(Mod(S))) iff [because of reflexiveness and transitivity of µ ₂] Ú_{N µ 2 A} N Î Clo^­ _{µ 1}(Mod(S)) iff [because of transitivity of µ ₁] Ú_{N µ 2 A} Ú_{M µ 1 N} M S iff Ú_{M µ 1 ° µ 2 A}M S iff [because of transitivity of µ ₁ ° µ ₂, µ ₁ + µ ₂    =    µ ₁ ° µ ₂] Ú_{M µ 1 + µ 2 A} M S. Hence (16). ^[¯]

Here are the rest of the technicalities.

Lemma 4

For every upward µ ₁ + µ ₂-closed class K Í S_L,

fin µ 1 + µ 2 (K) = fin µ 1 (K) Çfin µ 2 (K).

(17)

Proof. The case of ( Í ) follows from fin _µ (K) Í K.

( Ê ) Assume M Î fin _{µ 1} (K) Çfin _{µ 2} (K). Let N Î K satisfy N µ ₁ + µ ₂ M, with N ¹ M. There is A Î S_L, A ¹ M, with N µ ₁ + µ ₂ A µ _i M, where i Î { 1 , 2 }. By upward µ ₁ + µ ₂-closedness of K, A Î K. Hence, M Î fin _{µ i} (K), a contradiction. ^[¯]

Lemma 5

For every K Í S_L,

fin µ (K) = fin µ (Clo µ ­(K)).

(18)

Proof. ( Í ) Assume M Î fin _µ (K) and N Î Clo _µ ^­ (K), with N µ M. There is A Î K with A µ N. The transitivity of M yields A µ M. µ -finestness of M gives A = M. Therefore, both N µ M and M µ N hold. Because µ is a partial order, (5) yields N = M. Hence, M Î fin _µ (Clo _µ ^­ (K)).

( Ê ) Assume M Î fin _µ (Clo _µ ^­ (K)) and N Î K, with N µ M. In particular, N Î Clo _µ ^­ (K), therefore µ -finestness of M yields N = M. Hence, M Î K, and M Î fin _µ (K). ^[¯]

Lemma 6

For every K Í S_L, fin _µ (K) is µ -dense in K iff fin _µ (K) is µ -dense in Clo _µ ^­(K).

Proof follows from fin _µ (K) Í K Í Clo _µ ^­(K) and µ -density of K in Clo _µ ^­(K). ^[¯]

Lemma 7

For every K Ì S_L, fin _µ (K) is µ -dense in K iff fin _µ (Clo _µ ^­(K)) is µ -dense in Clo _µ ^­(K).

Proof by direct application of Lemmas 5 and 5. ^[¯]

To show that the dense foundedness of "-theories is preserved under combinations of refinements we need the following property of antipreservation. Refinement µ ₂ is said to be antipreserving for refinement µ ₁ if and only if

Ù A,B,C Î SL  A µ 2 B µ 1 C and A µ 1 C imply A = B.

(19)

(To see the above concept from a better perspective, one can equivalently start from this definition: µ ₂ is preserving for µ ₁ iff µ ₂ ° µ ₁ Í µ ₁, that is,

Ù A,B,C Î SL  A µ 2 B µ 1 C implies A µ 1 C,

and then use the prefix ``anti", as in the definition (5) of ``antisymmetric".)

Lemma 8

Assume that µ ₂ is antipreserving for µ ₁, µ ₁ ° µ ₂ is a partial order, fin _{µ 1}(K) is µ ₁-dense in K, and fin _{µ 2}(K) is µ ₂-dense in K. Then fin _{µ 1 + µ 2}(K) is µ ₁ + µ ₂-dense in K.

Proof. By Lemma 5, we may assume that K is upward µ ₁ + µ ₂-closed. Therefore, by Lemma 5, it suffices to show that

fin µ 1 (K) Çfin µ 2 (K) is µ 1 + µ 2 -dense in K.

(20)

Let M Î K, A Î fin _{µ 2}(K) with A µ ₂ M [it exists since fin _{µ 2}(K) is µ ₂-dense in K], B Î fin _{µ 1}(K) with B µ ₁ A [it exists because fin _{µ 1}(K) is µ ₁-dense in K], and N Î K with N µ ₂ B. Because µ ₁ + µ ₂ = µ ₁ ° µ ₂, N µ ₂ B µ ₁ A yields C Î S_L, with N µ ₁ C µ ₂ A. Since K is upward µ ₁-closed and N Î K, we see that C Î K. Therefore, by A Î fin _{µ 2}(K), (6) yields C = A. Hence, N µ ₁ A. Since N µ ₂ B µ ₁ A holds and µ ₂ is antipreserving for µ ₁, (19) gives N = B. Hence, B Î fin _{µ 2}(K), that is, B Î fin _{µ 1}(K) Çfin _{µ 2}(K), which gives (20). ^[¯]

None of the assumptions of Lemma 5 may be dropped. If fin _{µ i}(K) is not µ _i-dense in K then fin _{µ i + µ i}(K) is not µ _i + µ _i-dense in K. If µ ₁ + µ ₂ is not a partial order then letting µ = µ ₁ + µ ₂^-1 will produce fin _µ (K) which may not be µ -dense in K. If µ ₂ is not antipreserving for µ ₁ then Fig. depicts a counterexample to the lemma's thesis.

Figure 1                      A counterexample.

The relation µ ₁ is represented in Fig. 5 by solid arrows, that is, M µ ₁ N holds if and only if there is a solid directed path from N to M (this is not a misprint). Similarly, the relation µ ₂ is represented by dotted arrows. Put K = { A_i | i Î w} È { B_i | i Î w}. We have fin _{µ 1}(K) = { B_i | i Î w}, and fin _{µ 2}(K) = { A_i | i Î w}. One can easily check that all the assumptions of Lemma 5 are met, except that µ ₂ is preserving for µ ₁, that is, µ ₂ is not antipreserving for µ ₁ ( µ ₁ is antipreserving for µ ₂, though). Because fin _{µ 1 + µ 2}(K) is empty, it cannot be µ ₁ + µ ₂-dense in nonempty K.

After all this, the proof of the following fundamental result becomes an easy exercise.

The Completeness Theorem 9

Assume that CPP(G₁ , µ ₁) and CPP(G₂ , µ ₂) hold, µ ₁ ° µ ₂ is a partial order, µ ₂ is antipreserving for µ ₁, and G₁ and G₂ have the intersection property. Then for every µ ₁- and µ ₂-densly founded S Í " and for every j Î ",

Sµ 1 + µ 2 j iff j Î DAG1 ÇG2 ( S) .

(21)

Proof. Lemma 5 yields CPP(G₁ ÇG₂, µ ₁ + µ ₂). Lemma 5 gives µ ₁ + µ ₂-densly foundedness of every µ ₁- and µ ₂-densly founded S Í ". Application of Theorem 4 completes the proof.                      ^[¯]

Now, we return to instances of refinements. We will make Theorem 5 applicable to the combinations of refinements that were mentioned at the beginning of this section. One can easily check that the following compositions are partial orders:

£ ° Í ,    £ °,   ° Í ,    and ( £ °) ° Í .

Routine inspection shows that the second refinement of each of these compositions is antipreserving for the first one. We need to show that their CPP's possess the intersection property.

Let W be the set of all seven intersections of sets

Pos { = } ¢, Pos { = } , and QF.

(22)

Lemma 10

Every pair of elements of the set W has the intersection property.

Proof. We prove that Pos_{{ = }¢} and QF have the intersection property. (The cases of Pos_{{ = }} and QF, and Pos_{{ = }¢} and Pos_{{ = }} have similar proofs; the cases involving their intersections are straightforward).

Let S Í QF be logically equivalent to a subset of Pos_{{ = }¢}. We may assume without loss of generality that all elements of S are minimal disjunctions of atomic and negated atomic sentences. It follows from CPP(Pos_{{ = }¢}, £ ) that £ preserves the truthfulness of elements of S. Therefore, by the minimality of its elements, S does not contain occurrences of predicates from  in a scope of negation, that is, S Í Pos_{{ = }¢}. Therefore, S Í Pos_{{ = }¢} ÇQF.                      ^[¯]

Here are the previously announced "-complete characterizations of combined entailments by combined default assumption.

Main Theorem 11

For every S Í ", and every j Î ",

1. S _{£ + Í} j iff j Î DA_{Pos{ = }¢ ÇQF} ( S)

2. S _{£ +} j iff j Î DA_Pos ( S)

3. S_{Í +} j iff j Î DA_{Pos{ = } ÇQF} ( S)

4. S _{£ + Í +} j iff j Î DA_{Pos ÇQF} ( S)

Note. Because every "-sentence is logically equivalent to a conjunction of clauses, all instances of G used in Theorem 5 can be restricted to clauses, that is, QF may be understood as the set of ground clauses, Pos as the set of clauses positive in every symbol in  and in equality symbol =, and so on.

We end this section with a brief account of some more important consequences of Theorem 5.

• the Pos_{{ = }¢} ÇQF-default assumption is clause-complete with respect to totally minimal (i.e., predicate-minimal and domain-minimal) semantics. It syntactically characterizes simultaneous application of predicate and domain minimization.
• the Pos-default assumption is clause-complete with respect to predicate-minimal discriminant semantics. For those S Í " which do not contain positive appearances of =, the Pos-default assumption is clause-complete with respect to predicate-minimal strongly discriminant semantics (if S contains sentences of the form ``a = b", where a is not identical with b, then S does not have strongly discriminant models).
• The Pos ÇQF-default assumption is clause-complete with respect to minimal Herbrand (i.e., totally minimal and discriminant) semantics. For those S Í " which do not contain positive occurrences of =, the Pos ÇQF-default assumption is clause-complete with respect to minimal strongly Herbrand semantics (if S contains sentences of the form ``a = b", where a is not identical with b, then S does not have any strongly Herbrand models). Therefore, the Pos ÇQF-default assumption may be recognized as the "-complete version of generalized closed-world assumption GCWA (cf. [] and []) and extended closed-world assumption ECWA (cf. []).
• The Pos_{{ = }} ÇQF-default assumption is clause-complete with respect to Herbrand (i.e., domain-minimal and discriminant) semantics. For those S Í " which do not contain positive occurrences of =, the Pos_{{ = }} ÇQF-default assumption is clause-complete with respect to strongly Herbrand semantics.

6  Languages without Equality

What if L does not include the equality symbol? Since the class of strongly Herbrand models, or its subclass, has been widely accepted as the standard semantics for deductive data bases and logic programs, exclusion of = from L was perhaps the simplest way to ensure that a consistent set of clauses has a strongly Herbrand model. In this Section, we use the results of Section 5 to determine how the lack of the equality symbol in L affects the the "-completeness of the G-default assumption.

First, let us note that if M is a structure for language L with the equality symbol = then M is also a structure for language L¢ being a result of removal of = from L. Because the satisfaction relation does not depend on whether the sentence in question is embedded in L or L¢, it follows that for every set of sentences S Í L¢, the class of models of S is the same as if S was understood as a set of sentences of L. Of course, the set Cn_L¢(S) of consequences of S in L¢ is a proper subset of the set Cn_L(S) of consequences of S in L. Nevertheless, a sentence j Î L¢ is a consequence of S within L¢ if and only if it is a consequence of S in L. Therefore, we have the following fact.

Fact 1

For every S Í L¢,

CnL¢(S) = CnL(S) ÇL¢.

                     ^[¯]

This preservation property of the consequence operation with respect to removing the equality symbol from the underlying language extends over refined entailments. More specifically, for each refinement µ , each S Í L¢, and each j Î L¢, S _µ j holds independently of whether one embeds S and j in L or in L¢. We state this observation in the following form.

Fact 2

For every refinement µ and every S Í L¢,

{j Î L¢| S µ j} = {j Î L|S µ j} ÇL¢.

                     ^[¯]

Unfortunately, the same cannot be said about the G-default assumption, for there exists S Í "ÇL¢ and j Î "ÇL¢ such that (SÈ{j})_GÇL¢ = S_GÇL¢, but (SÈ{j})_G ¹ S_G.

Example 3

Let S = {P(c) ÚP(d)}, j = ØP(c) ÚØP(d), and G = Pos_{{ = }¢}. We have (SÈ{j})_GÇL¢ = S_GÇL¢, but because Ø(c = d) Î (SÈ{j})_G \S_G, (SÈ{j})_G ¹ S_G.                      ^[¯]

Therefore, in general, one cannot restrict G to GÇL¢ while switching from L to L¢ without putting the "-completeness of the G-default assumption at risk. For some G's it is possible, though. To show this we need the following technical lemmas.

Lemma 4

For each S Í "ÇL¢ and j Î Pos _{{ = }} ,

Sj iff Sj.

Proof. Sj iff [by Theorem 4.4] (SÈ{ j} )_{Pos { = }} = S_{Pos { = }} iff [since j Î (SÈ{ j} )_{Pos { = }} ] j Î S_{Pos { = }} iff S j.                      ^[¯]

Definition 5

Operation ¢ on "-formulas of L and sets of "-formulas of L is defined by induction as follows.

1. for every term t of L,

   
   

   ( t = t )¢ = true

2. for every pair t, s of non-identical terms of L,

   
   

   ( t = s )¢ = false

3. for every "-formula j of " without occurrences of =,

   
   

   j¢ = j

4. for all quantifier-free formulas j, y of L,

   
   

   (Øj) ¢ = Øj¢

   
   

   (jÙy) ¢ = j¢Ùy¢

5. for every quantifier-free formula j of L,

   
   

   (" ® x   j)¢ = " ® x   j¢

6. for every G Í L,

   
   

   G¢ = { j¢ | j Î G} .

                        ^[¯]

Lemma 6

For each strongly discriminant structure M for L, and each j Î QF,

M j iff M j¢.

Proof by routine induction, using Definition 6, 6 - 6.                      ^[¯]

Lemma 7

For every S Í "ÇL¢ and j Î QF,

Sj iff Sj¢.

Proof. Sj iff [because S does not contain occurrences of =] j is true in all strongly discriminant models of S iff [by Lemma 6] j¢ is true in all strongly discriminant models of S iff Sj¢.                      ^[¯]

Lemma 8 Assume that G Í G¢ÈPos _{{ = }} . For every S, P Í "ÇL¢,

SG = PG iff SG¢ = PG¢ .

(23)

Proof. Assume j Î G. We are going to show that Sj iff S j¢, and P j iff P j¢. This will prove (23).

Case 1: j Î G¢, is obvious since [by Definition 6.6] j = j¢ in this case.

Case 2: j Î Pos _{{ = }} ÇQF. S j iff [by Lemma 6] Sj iff [by Lemma 6] Sj¢ iff [by Lemma 6; note that by Definition 6, j¢ Î Pos _{{ = }} ] Sj¢. Similarly, P j iff P j¢.

Case 3: j Î Pos _{{ = }} \QF. Let j = "[] y([]), where y([]) is quantifier-free. S "[] y([]) iff Sy([c]), where [c] is a sequence of constants not in S with [] and [c] having the same pattern of repetitions, iff [using the same argument as in Case 2] S y([c])¢ iff S "[] y([])¢ iff [by Definition 6.6] S ("[] y([]))¢. Similarly, P j iff P j¢.                      ^[¯].

Now, we are ready to prove the "-completeness of the following instances the G-default assumption with respect to instances of entailment _µ .

Theorem 9

For every S Í "ÇL¢ and every j Î "ÇL¢,

1. S_{£ +} j iff j Î DA_PosÇL¢ ( S)

2. S_{Í +} j iff j Î DA_{QF ÇL¢} ( S)

3. S_{£ + Í +} j iff j Î DA_{Pos ÇQF ÇL¢} ( S)

DA_{Pos ÇL¢} was first introduced in [] as an instance of cwa_S, and proven complete with respect to entailment _{£ +} in [].

As noted at the end of Section 5, QF in Theorem 6 may be replaced with the set of ground clauses, Pos with the set of clauses positive in every symbol in Â, and Pos ÇQF with the set of ground clauses positive in every symbol in Â.

We conclude this Section with the application of Theorem 6 to the evaluation of the degree of completeness of published in [] extended version GCWA^* of Minker's GCWA.

Let us note that the condition involved in the definition of G-default assumption, namely

(SÈ{ j} )G = SG

(24)

is equivalent to

Ù g Î G  S ØjÚg implies S g,

(25)

which constitutes the familiar scheme whose instances occur in definitions of Minker style closed-world assumptions. For G = Pos ÇQF ÇL¢ (the set of ground positive clauses without occurrences of =), and j restricted to QF ÇL¢, (25) expresses the GCWA^*(S), that is, by (10),

Ù S Í "  GCWA*(S) = DAPos ÇQF ÇL¢ (S) ÇQF ÇL¢.

(26)

Therefore, by Theorem 6.6, GCWA^* is ground-complete with respect to minimal strongly Herbrand entailment (cf. [] for an early proof of this fact).

One should note, however, that although for some refinements µ that do not involve Í (and consequently, respective µ -finest semantics are not restricted to domain-minimal semantics), their complete preservation properties G satisfy

Ù "x j(x) Î "  "x j(x) Î DAG ( S) iff j(c) Î DAG ( S),

(for example, take µ    =    £ , and G = Pos_{{ = }¢}), where c is a new constant symbol from beyond L, the same is not true for £ + Í + . Therefore, the ground completeness (26) of GCWA^* does not imply its "-completeness. Indeed, GCWA^* is not "-complete with respect to minimal strongly Herbrand semantics, except of course, for those S's which admit elimination of universal quantifiers. Here is a counterexample.

Example 10

Put S = {P(a) ÚQ(b)}. One can check that GCWA^*(S)ØP(c) . On the other hand, "x ØP(x) is inconsistent with S. Hence, j(c) cannot be used as a valid replacement for ("x)(j(x)) when GCWA^* is used. Consequently, GCWA^* (S) ("x)(ØP(x) ÚØQ(x)), even though S _{£ + Í +} ("x)(ØP(x) ÚØQ(x)). Of course, by Theorem 6.6, ("x)(ØP(x) ÚØQ(x)) Î DA_{Pos ÇQF ÇL¢} (S).                      ^[¯]

This fact makes GCWA^* strictly weaker than DA_{Pos ÇQF ÇL¢}. Similar argument shows that also ECWA of [] is strictly weaker than DA_{Pos ÇQF ÇL¢}; it turns out that the published in [] proof of "-completeness of ECWA works only for cases of S which admit elimination of quantifiers.

7  Few Words about the Roots

Default rules of inference were introduced by Reiter in [], also the inventor of the closed-world assumption ([]), and quickly became a very fashionable subject of research. At the same time, McCarthy in his famous paper [] about circumscription initiated investigations of first-order minimal models. Second-order variant of circumscription was proven complete with respect to minimal-model semantics by Lifschitz in []. A restricted form of scheme (25) was first used by Minker in [], with subsequent ground-complete extensions by Yahya and Henschen ([]), and Gelfond, Przymusi\'nska and Przymusi\'nski ([]). Credit for the first proof of dense foundedness is due to Bossu and Siegel ([]).

Marczewski in [] and Lyndon in [] (followed by []) were first to study preservations of positive sentences. The consequence operation defined by

(SÈ{ j} )" = S"

(27)

was first used by Kaiser in [] and later by Henrard, who proved in [] that certain iterative use of (27) completely characterizes the generic-model semantics of Robinson's model-theoretic forcing of []. A generalization (24) of scheme (27) was first applied to analysis of the closed-world assumption in [], with its "-completeness proven in [].

8  Acknowledgements

I would like to thank Klaus Kaiser for his kind invitation to write this paper, Barbara Tillman for her patience when I ruined our vacation plans, Ehren Evans and Henrietta Okeke for turning the hieroglyphic manuscript into a neat L^AT_EX document, Ken Ganezer for his improvements of my ESL, and Anonymous Referee for his favorable comments and helpful suggestions.

References

[]

Jon Barwise, editor. Handbook of Mathematical Logic. North-Holland, Amsterdam, second edition, 1978.

[]

Genviéve Bossu and Pierre Siegel. Saturation, nonmonotonic reasoning, and the closed world assumption. Artificial Intelligence, 25(1):13-64, 1984.

[]

W. Craig. Three uses of Herbrand - Gentzen theorem in relating model theory and proof theory. J. Symbolic Logic, 22:269-285, 1957.

[]

Michael Gelfond, Halina Przymusi\'nska, and Teodor C. Przymusi\'nski. The extended closed world assumption and its relationship to parallel circumscription. In Proceedings ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, pages 133-139, Cambridge, MA, 1986. ACM.

[]

Paul Henrard. Le `forcing-compagnon' sans `forcing'. C. R. Acad. Sc. Paris, 276(Ser. A):821-822, 1973.

[]

Thomas J. Jech. About the axiom of choice. In [], chapter B.2, pages 345-370. 1978.

[]

Klaus Kaiser. Über eine verallgemeinerung der Robinsonschen Modellvervollstaändigung. Zeitschrift für Mathematik Logik und Grundlagen der Mathematik, 15:37-48, 1969.

[]

H. Jerome Keisler. Fundamentals of model theory. In [], chapter A.2, pages 47-104. 1978.

[]

Vladimir Lifschitz. Closed-world databases and circumscription. Artificial Intelligence, 27:229-235, 1985.

[]

Roger C. Lyndon. Review of paper by A. Horn. Journal of Symbolic Logic, 16:216, 1951.

[]

Roger C. Lyndon. An interpolation theorem in the predicate calculus. Pacific J. Math., 9:129-142, 1959.

[]

Roger C. Lyndon. Properties preserved under homomorphism. Pacific J. Math., 9:143-154, 1959.

[]

Edward Marczewski. Sur les congruences et les proprietés positives d'algèbres abstraites. Colloquium Mathematicum, 2:220, 1951.

[]

John McCarthy. Circumscription - a form of non-monotonic reasoning. Artificial Intelligence, 13(1-2):27-39, 1980.

[]

Jack Minker. On indefinite databases and closed world assumption. In Proceedings of 6-th Conference on Automated Deduction, Lecture Notes in Computer Science 138, pages 292-308, Berlin, New York, 1982. Springer Verlag.

[]

Raymond Reiter. On closed world data bases. In Hervé Gallaire and Jack Minker, editors, Logic and Data Bases, pages 55-76. Plenum Press, 1978.

[]

Raymond Reiter. A logic for default reasoning. Artificial Intelligence, 13(1-2):81-132, 1980.

[]

Abraham Robinson. Forcing in model theory. In Proc. Simp. Mat., pages 64-80. Institute Nationale di Alta Matematica, 1971.

[]

Marek. A. Suchenek. Forcing versus closed world assumption. In Zbigniew W. Ra\'s and Maria Zemankova, editors, Methodologies for Intelligent Systems, pages 453-460. North-Holland, 1987.

[]

Marek A. Suchenek. Incremental models of updating data bases. In C. H. Bergman, R. D. Maddux, and D. L. Pigozzi, editors, Algebraic Logic and Universal Algebra in Computer Science, Lecture Notes in Computer Science 425, pages 243-271, Ames, June 1-4 1988. Springer-Verlag.

[]

Marek A. Suchenek. A syntactic characterization of minimal entailment. In Ewing L. Lusk and Ross A. Overbeek, editors, Logic Programming, North American Conference 1989, pages 81-91, Cambridge, MA, October 16-20 1989. MIT Press.

[]

Marek A. Suchenek. First-order syntactic characterizations of minimal entailment, domain minimal entailment, and Herbrand entailment. Journal of Automated Reasoning, 10:237-263, 1993.

[]

A. Yahya and L. Henschen. Deduction in non-Horn databases. Journal of Automated Reasoning, 1:141-160, 1985.

Footnotes:

¹The case of L without = is addressed in Section .

²The concept of positiveness is purely syntactic, so that a non-positive formula may be logically equivalent to a positive one; similarly, a non-atomic formula may be logically equivalent to an atomic formula.

³i.e., with no occurrences of variables