Transitively Relational Partial Meet Horn Contraction

1 Introduction

The theory of belief change deals with the dynamics of beliefs represented as logical formulas, usually under classical propositional logic (PL). The change often involves removal of existing beliefs-the contraction operation-and incorporation of newly acquired beliefs-the revision operation. The AGM [Alchourr´on et al., 1985] framework is generally held to be the most compelling account of belief change and provides a common point of reference and comparison.

The nature of belief change where the underlying logic is restricted to the Horn fragment of classical PL (Horn logic) has recently attracted significant attention [Delgrande, 2008; Booth et al., 2009; 2010; Delgrande and Wassermann, 2010; Zhuang and Pagnucco, 2010a; 2010b]. The topic is interesting for several reasons. Horn logic is an important subset of PL which has found use in many artificial intelligence and database applications. The study of belief change under Horn logic broadens the spectrum of the AGM framework and in particular it provides a key step towards applying the AGM framework to non-classical logics with less expressive and reasoning power than PL.

In the AGM framework beliefs are characterised by belief sets which are sets of formulas closed under logical deduction. Once we work under a less expressive logic such as Horn logic there are various restrictions on how beliefs can be represented. Under Horn logic a belief set contains only Horn formulas, thus it is referred to as a Horn belief set. The main challenge is therefore to define change operations satisfying the principles of the AGM framework while their resultant belief sets are still representable as Horn belief sets.

The aim of this paper is to consider a fundamental construction for the contraction operation-transitively relational partial meet contraction-in the context of Horn logic. The representation theorem we prove establishes a tight connection between a construction method and a set of rationality postulates. It guarantees soundness-contractions constructed by the method satisfy the postulates-and completeness-all contractions that satisfy the postulates can be constructed by the method. In the AGM framework construction methods often make use of a reasoner's belief preference information represented by orderings over formulas, maximal non-implying subsets (commonly known as remainder sets), or possible worlds (i.e., propositional interpretations). The contraction we construct extends an existing one in which preference information over a notion of remainder sets, namely weak remainder sets, are used for guiding the operation.

2 Technical Preliminaries

We assume a fixed propositional language L over a finite set of atoms P = {p, q, . . .}. Lower case Greek characters φ, ψ, . . . denote formulas and upper case Roman characters X, Y, . . . denote sets of formulas. Classical logical consequence and logical equivalence are denoted by ⊢ and ≡ respectively. Cn is the Tarskian consequence operator such that Cn(X) = {φ : X ⊢ φ}. An interpretation of L is a function from P to {true, false}. Truth and falsity of a formula in L is determined by standard rules of PL. An interpretation I is a model of a formula φ, written I |= φ, if φ is true in I. An interpretation I is a model of a set of formulas X, written I |= X if for each formula φ in X, I |= φ. Given a set of formulas X, [X] denotes the set of models of X. To denote the set of models of a formula φ, we write [φ] instead of [{φ}]. An interpretation is identified by the set of atoms assigned true, e.g., the interpretation bc indicates atoms b, c are assigned true and the others are assigned false. 1

A Horn clause is a clause that contains at most one positive atom, e.g., ¬p ∨ ¬q ∨ r. A Horn formula is a conjunction of Horn clauses. The Horn language LH is the subset of L that contains only Horn formulas. The Horn logic generated from LH is just PL acting on Horn formulas. A Horn theory is a set of Horn formulas. We add the suffix h to logical operators under Horn logic. For example, Cnh is the Horn consequence operator such that Cnh (X) = {φ : X ⊢ φ, φ ∈ LH}. Horn : 2L → 2LH is a function such that Horn(X) = {φ : φ ∈ X and φ ∈ LH}. Negation is not always available in Horn logic. For example, the negation of ¬p∧¬q (i.e., p∨q) is not a Horn formula. However, we denote by [¬φ] the set of interpretations in which φ is false.

1 Here bc is a shorthand for {b, c} for the sake of simplicity.

The intersection of a pair of interpretations is the interpretation that assigns true to those atoms that are assigned true by both of the interpretations. We denote the intersection of interpretations m1 and m2 by m1 ∩ m2, e.g., ab ∩ bc = b, ab ∩ cd = ∅. Given a set of interpretations M, the closure of M under intersection is denoted as Cl∩(M). Models of any Horn theory are closed under intersection, that is for a Horn theory H, if m1,m2 ∈ [H] then m1 ∩m2 ∈ [H]. Conversely any set of interpretations that are closed under intersections can be represented by a Horn theory. This closure property plays a crucial role in this paper.

3 Background: AGMContraction

The operation of contraction in the AGM framework concerns giving up beliefs from a belief set K which is closed under Cn. A set of rationality postulates is formalised for capturing the intuitive ideas behind the operation, in which (K .-1)-(K .-6) are regarded as the basic postulates and (K .-7)-(K .-8) as supplementary postulates.

• (K .-2) K .-φ ⊆K.
• (K .-1) K .-φ = Cn(K .-φ).
• (K .-3) If φ ̸∈ K, then K .-φ =K.
• (K .-5) K ⊆ (K .-φ) +ϕ.
• (K .-4) If ̸⊢ φ, then φ ̸∈ K .-φ.
• (K .-6) If φ ≡ ψ, then K .-φ =K .-ψ.
• (K .-8) If φ ̸∈ K .-φ ∧ψ then K .-φ ∧ψ ⊆K .-φ.
• (K .-7) K .-φ ∩K .-ψ ⊆K .-φ ∧ψ.

A widely used construction of AGM contraction is that based on the notion of remainder sets. If K is a set of formulas and φ a formula, we write K ↓ φ for the set of all maximal subsets X of K such that φ ̸∈ Cn(X). If K is a belief set, then elements of K ↓ φ are called remainder sets of K with respect to φ. As noted in [Alchourr´on et al., 1985], K ↓ φ is non-empty iff φ ̸∈ Cn(∅). A selection function γ for a belief set K is one such that γ(K ↓ φ) returns a nonempty subset of K ↓ φ whenever K ↓ φ is non-empty and returns K otherwise. Let γ be a selection function for a belief set K, then the partial meet contraction (PMC) .- over K is defined as K .-φ = ⋂ γ(K ↓ φ). As limiting cases, for all φ ̸∈ Cn(∅), if γ(K ↓ φ) = K ↓ φ, then .- is a full meet contraction; and if γ(K ↓ φ) is a singleton set, then .- is a maxichoice contraction. A contraction is a PMC iff it satisfies the basic postulates. A PMC does not in general satisfy both the supplementary postulates unless it is transitively relational which requires that further restrictions be imposed on the selection function. We say that γ is transitively relational over K iff a transitive relation ⩽ over remainder sets of K is used to generate γ via the marking off identity:

The relation ⩽ is intended to capture the intuition that X ⩽ Y iff Y is at least as plausible as X. X < Y means X ⩽ Y and Y ̸⩽ X. A PMC is transitively relational, referred to as a transitively relational partial meet contraction (TRPMC), if it is determined by a transitively relational selection function. A contraction is a TRPMC iff it satisfies the full set of postulates.

In the next section we study the operation of contraction under Horn logic. Obviously, a Horn belief set H is closed under Horn consequence, that is H = Cnh (H). A Horn contraction is a function over a Horn belief set that, given a Horn formula, returns another Horn belief set. In particular, we develop the Horn analogue of TRPMC.

4 Belief Contraction Under Horn Logic

4.1 Partial Meet Horn Contraction

The Horn analogue of TRPMC has been studied in [Zhuang and Pagnucco, 2010b] where the relationship with the epistemic entrenchment based Horn contraction (EEHC) [Zhuang and Pagnucco, 2010a] is investigated but no representation result is considered. That contraction is defined as an extension of the partial meet Horn contraction (PMHC) studied in [Delgrande and Wassermann, 2010] where the notion of weak remainder sets is proposed.

Definition 1 Let H be a Horn belief set and φ be a Horn formula. The set of weak remainder sets of H with respect to φ, denoted by H ↓w φ, is such that X ∈ H ↓w φ iff X = Cnh (X) and there is an m ∈ [¬φ] such that [X] = Cl∩([H] ∪ {m}).

Remainder sets of a belief set K with respect to a formula φ can be obtained semantically by adding counter-models of φ to the models of K (i.e., Cn(X) ∈ K ↓ φ iff [X] = [K] ∪ {m} for some m ∈ [¬φ]). Essentially, the number of remainder sets is identical to the number of counter-models of φ. Weak remainder sets of a Horn belief set with respect to a Horn formula are obtained similarly but by also taking into account the closure property of Horn theories.

Example 1 Let P = {a, b, c} and H = Cnh (a ∧ b). Consider H ↓w (a ∧ b). As [H] = {ab, abc} and [¬(a ∧ b)] = {ac, a, bc, b, c, ∅}, we have H ↓w (a ∧ b) = {X1, . . . ,X6} such that [X1] = Cl∩([H] ∪ {ac}) = {ab, abc, ac, a} and X1 = Cnh ({a}); [X2] = Cl∩([H] ∪ {a}) = {ab, abc, a} and X2 = Cnh ({a, ¬c ∨ b}); [X3] = Cl∩([H] ∪ {bc}) = {ab, abc, bc, b} and X3 = Cnh ({b}); [X4] = Cl∩([H] ∪ {b}) = {ab, abc, b} and X4 = Cnh ({b, ¬c ∨ a}); [X5] = Cl∩([H] ∪ {c}) = {ab, abc, c, ∅} and X5 = Cnh ({¬a ∨ b, ¬b ∨ a}); [X6] = Cl∩([H] ∪ {∅}) = {ab, abc, ∅} and X6 = Cnh ({¬a ∨ b, ¬b ∨ a, ¬c ∨ a, ¬c ∨ b}). Note that X1 ⊂ X2, X3 ⊂ X4, and X5 ⊂ X6.

We first prove some new results concerning weak remainder sets which stem from the model-theoretic definition and the closure property.

Lemma 1 Let K be a belief set and H be a Horn belief set such that φ, ψ ∈ H then

1. If X ∈ H ↓w φ and X ̸⊢ ψ then X ∈ H ↓w ψ.
2. H ↓w φ ∧ ψ = (H ↓w φ) ∪ (H ↓w ψ).
3. Horn(X) ∈ Horn(K) ↓w φ iff X ∈ K ↓ φ.

Proof: 1. Suppose X ∈ H ↓w φ and X ̸⊢ ψ we need to show X ∈ H ↓w ψ. From Definition 1 it follows that X = Cnh (X) and [X] = Cl∩([H] ∪ {u}) for some u ∈ [¬φ]. Assume X ̸∈ H ↓w ψ, then u ∈ [ψ] for otherwise it follows from Definition 1 and u ∈ [¬ψ] that X ∈ H ↓w ψ contradicting the assumption. ψ ∈ H implies [H] ⊆ [ψ]. From [H] ⊆ [ψ] and u ∈ [ψ] it follows that [H] ∪ {u} ⊆ [ψ], hence Cl∩([H] ∪ {u}) ⊆ Cl∩[ψ]. Since X ̸⊢ ψ, there is v ∈ [X] such that v ̸∈ [ψ]. Since [X] ⊆ Cl∩[ψ], we have v ∈ Cl∩[ψ]. From v ∈ Cl∩[ψ] and v ̸∈ [ψ] we can conclude, by the closure property, that ψ ̸∈ LH, contradicting ψ ∈ [H]. 2. Let X ∈ H ↓w φ ∧ ψ then X ̸⊢ φ or X ̸⊢ ψ, so by part 1, X ∈ H ↓w φ or X ∈ H ↓w ψ. Conversely, if X ∈ H ↓w φ or X ∈ H ↓w ψ then X ̸⊢ φ ∧ ψ so, by part 1 again, X ∈ H ↓w φ ∧ ψ.

3. For one direction (⇒) suppose Y ∈ Horn(K) ↓w φ then by Definition 1, there is m ∈ [¬φ] such that [Y ] = Cl∩([Horn(K)] ∪ {m}) = Cl∩(Cl∩([K]) ∪ {m}) = Cl∩([K] ∪ {m}). By a property of standard remainder sets, there is X ∈ K ↓ φ such that [X] = [K] ∪ {m}, that is Cl∩([K] ∪ {m}) = Cl∩([X]) = [Horn(X)] which implies Y =Horn(X).

For the other direction (⇐), suppose X ∈ K ↓w φ, then [X] = [K] ∪ {u} for some u ∈ [¬φ]. [Horn(X)] = Cl∩[X] = Cl∩([K] ∪ {u}) = Cl∩(Cl∩[K] ∪ {u}) = Cl∩([Horn(K)] ∪ {u}). Then by Definition 1, we have Horn(X) ∈ Horn(K) ↓w φ.

✷

Part 1 says that if a weak remainder set of H does not contain ψ then it is a weak remainder set of H with respect to ψ, provided that ψ is an element of H. Part 2 says that weak remainder sets with respect to conjunctions are comprised of the union of the remainder sets with respect to each conjunct. Part 3 says that there is a one-to-one correspondence between the remainder sets of K and the weak remainder sets of Horn(K).

PMHC is defined similarly to PMC:

Definition 2 [Delgrande and Wassermann, 2010] Let γ be a selection function for H, then the PMHC .- over H is given by: H .-φ = ⋂ γ(H ↓w φ).

The representation result for PMHC is as follows:

(H .-1)-(H .-4) and (H .-6) are Horn analogues of the corresponding AGM postulates. (H .-f) captures the failure property which states that the contraction of a tautology leaves the belief set unchanged. The property is derivable from (K .-2) and (K .-5). Since (K .-5) is not compatible with Horn logic [Flouris, 2006], (H .-f) is needed here to take care of a special case. (H .-wr) is a weaker version of the relevance postulate [Hansson, 1999] for Horn logic.

In the subsequent section we investigate PMHCs whose determining selection functions are constrained by transitivity and relationality.

4.2 Transitively Relational PMHC

A PMHC is transitively relational and referred to as a transitively relational partial meet Horn contraction (TRPMHC) if it is determined by a transitively relational selection function.

Definition 3 Let γ be a transitively relational selection function for a Horn belief set H. Then .- is a TRPMHC over H iff H .-φ = ⋂ γ(H ↓w φ) for all φ ∈ LH.

TRPMHC is more sophisticated than PMHC as it brings in more order via the transitively relational selection function. As with TRPMC, the additional order makes TRPMHC satisfy some extra postulates regarding the contraction of conjunctive formulas.

Lemma 2 Let H be a Horn belief set and .- be a PMHC over H determined by a transitively relational selection function γ, then .- satisfies the following postulates:

• (H .-8) If φ ̸∈ H .-φ ∧ ψ then H .-φ ∧ ψ ⊆ H .-φ.
• (H .-7) H .-φ ∩H .-ψ ⊆H .-φ ∧ψ.
• (H .-ct) If ψ ∈ H .-φ ∧ψ then ψ ∈ H .-φ ∧ψ ∧ δ
• (H .-pa) (H .-φ) ∩Cnh (φ) ⊆H .-φ ∧ψ.
• (H .-c) H .-φ ∧ψ ⊆H .-φ or H .-φ ∧ψ ⊆H .-ψ.

Proof: We only show the proof for (H .-pa) as proofs for the others are very similar to those in [Alchourr´on et al., 1985]. If ⊢ φ, ⊢ ψ, φ ̸∈ H or ψ ̸∈ H then (H .-pa) is trivially satisfied, so suppose ̸⊢ φ, ̸⊢ ψ, φ ∈ H and ψ ∈ H. By the construction of TRPMHC and Part 2 of Lemma 1, it suffices to show ⋂ γ(H ↓w φ) ∩Cnh (φ) ⊆ ⋂ γ(H ↓w φ∪H ↓w ψ) that is, by model theory, to show [⋂ γ(H ↓w φ∪H ↓w ψ)] ⊆ [⋂ γ(H ↓w φ)∩Cnh (φ)]. Since [⋂ γ(H ↓w φ∪H ↓w ψ)] = [X1] ∪ · · · ∪ [Xn] for X1, . . . ,Xn ∈ γ(H ↓w φ ∪H ↓w ψ) and [⋂ γ(H ↓w φ) ∩ Cnh (φ)] = [Y1] ∪ · · · ∪ [Ym] ∪ [φ] for Y1, . . . , Ym ∈ γ(H ↓w φ). It remains to show for each X ∈ {X1, . . . ,Xn}, [X] ⊆ [Y1] ∪ · · · ∪ [Ym] ∪ [φ].

First case, X ∈ H ↓w φ. It follows from relationality of γ and X ∈ γ(H ↓w φ ∪ H ↓w ψ) that X ∈ γ(H ↓w φ). Thus there is a Y ∈ {Y1, . . . , Ym} such that [X] = [Y ].

Second case, X ̸∈ H ↓w φ. It follows from X ∈ (H ↓w φ ∪ H ↓w ψ) and X ̸∈ H ↓w φ that X ∈ H ↓w ψ. Assume X ̸⊢ φ then by Part 1 of Lemma 1 we have X ∈ H ↓w φ thus contradicting the assumption, so X ⊢ φ which implies [X] ⊆ [φ].

✷

(H .-7) and (H .-8) are Horn analogues of (K .-7) and (K .-8). Some conjunctive postulates are derivable from (K .-7) and (K .-8) such as partial antitony, conjunctive trisection, and covering. Let .- be a PMC for K, we have that .- satisfies (K .-7) iff it satisfies partial antitony [Alchourr´on et al., 1985]; .- satisfies partial antitony iff it satisfies conjunctive trisection [Rott, 1992]; and .- satisfies (K .-8) only if it satisfies covering [Alchourr´on et al., 1985]. (H .-pa), (H .-ct) and (H .-c) are Horn analogues of partial antitony, conjunctive trisection, and covering respectively. The connection between (H .-7) and (H .-8) and Horn analogues of the derived postulates are also preserved except for (H .-pa) which is is not related to (H .-7). It is for this reason that (H .-pa) is able to stand alone, capturing properties exclusive to (H .-7).

The following notion of completed selection function [Alchourr´on et al., 1985] is useful in proving completeness of TRPMHC with respect to its set of characterising postulates.

Definition 4 Let γ be a selection function for a Horn belief set H. The completion of γ is a function ˆ γ such that: ˆ γ(H ↓w φ) = {X : ⋂ γ(H ↓w φ) ⊆ X ∈ H ↓w φ} if H ↓w φ is non-empty and ˆ γ(H ↓w φ) = γ(H ↓w φ) = {H} otherwise. γ is completed iff γ = ˆ γ.

Clearly, ˆ γ is also a selection function. Let γ be a selection function for a belief set K. We have ⋂ ˆ γ(K ↓ φ) = ⋂ γ(K ↓ φ) for all φ [Alchourr´on et al., 1985], thus ˆ γ determines the same PMC as γ does. Selection functions for Horn belief sets exhibit a similar property. The proof is identical to the PL case.

Lemma 3 Let γ be a selection function for a Horn belief set H. Then ⋂ γ(H ↓w φ) = ⋂ ˆ γ(H ↓w φ) for all φ ∈ LH.

All selection functions for determining PMCs are completed 2 [Alchourr´on et al., 1985], however, this is not the case for PMHC. In Example 1, if γ is such that γ(H ↓w (a ∧ b)) = {X1}, then ˆ γ(H ↓w (a ∧ b)) = {X1, X2} as X1 ⊂ X2.

Given a PMHC determined by a selection function γ, the following lemma shows that (H .-pa) and (H .-8) are sufficient conditions for ˆ γ to be transitively relational.

Lemma 4 Let H be a Horn belief set and .- be a PMHC over H determined by a selection function γ. If .- satisfies (H .-pa) and (H .-8), then ˆ γ is transitively relational.

Proof: Let ⩽ be the relation over all weak remainder sets of H such that X ⩽ Y iff either:

(i) Y = H or both of the following hold:

• (iib) for all φ, if X, Y ∈ H ↓w φ and H .-φ ⊆ X, then H .-φ ⊆ Y .
• (iia) there is some φ ∈ H such that H .-φ ⊆ Y ∈ H ↓w φ.

We need to show that (1) ⩽ generates the completion ˆ γ of γ via the marking off identity, and (2) ⩽ is transitive.

(1) Suppose for the principal case that H ↓w φ ̸= ∅. We need to show ˆ γ(H ↓w φ) = {Y ∈ H ↓w φ |X ⩽ Y for all X ∈ H ↓w φ}.

For one direction, suppose Z ̸∈ ˆ γ(H ↓w φ). We need to show Z ̸∈ {Y ∈ H ↓w φ : X ⩽ Y for all X ∈ H ↓w φ}.

First case, φ ̸∈ H. By Definition 1, φ ̸∈ H implies H ↓w φ = {H} hence ˆ γ(H ↓w φ) = {H}. So it follows from Z ̸∈ ˆ γ(H ↓w φ) that Z ̸∈ H ↓w φ.

Second case, φ ∈ H. If Z ̸∈ H ↓w φ, then Z ̸∈ {Y ∈ H ↓w φ |X ⩽ Y for all X ∈ H ↓w φ} holds trivially. So suppose Z ∈ H ↓w φ. Since H ↓w φ ̸= ∅, we have by definition of γ, ˆ γ(H ↓w φ) ̸= ∅. By Lemma 3, H .-φ = ⋂ γ(H ↓w φ) = ⋂ ˆ γ(H ↓w φ). Let N ∈ ˆ γ(H ↓w φ), then H .-φ = ⋂ ˆ γ(H ↓w φ) ⊆ N. By the completion property of

2 The result only holds for belief sets that are finite modulo Cn. As we assume a finite language, this is always the case.

ˆ γ, Z ̸∈ ˆ γ(H ↓w φ) implies H .-φ ̸⊆ Z. Then from condition (iib) it follows that N ̸⩽ Z which implies Z ̸∈ {Y ∈ H ↓w φ | X ⩽ Y for all X ∈ H ↓w φ}.

For the other direction suppose Z ∈ ˆ γ(H ↓w φ). We need to show Z ∈ {Y ∈ H ↓w φ : X ⩽ Y for all X ∈ H ↓w φ}. Let N ∈ H ↓w φ. It remains to show N ⩽ Z.

First case, φ ̸∈ H. By Definition 1, φ ̸∈ H implies H ↓w φ = {H}. It then follows from N ∈ H ↓w φ, Z ∈ H ↓w φ and H ↓w φ = {H} that N = Z = H. Hence by condition (i) we have N ⩽ Z.

Second case, φ ∈ H. We will show conditions (iia)- (iib) for deriving N ⩽ Z are satisfied. It follows from Z ∈ ˆ γ(H ↓w φ) and the construction of PMHC that H .-φ ⊆ Z ∈ H ↓w φ. So condition (iia) is satisfied. For condition (iib), suppose ψ ∈ LH, N ∈ H ↓w ψ, Z ∈ H ↓w ψ and H .-ψ ⊆ N. It remains to show H .-ψ ⊆ Z. It follows from (H .-c) which follows from (H .-8) that either H .-φ ∧ ψ ⊆ H .-φ or H .-φ ∧ ψ ⊆ H .-ψ. In the latter case H .-φ ∧ ψ ⊆ H .-ψ ⊆ N ∈ H ↓w φ, so φ ̸∈ H .-φ ∧ ψ; then by (H .-8) we have H .-φ ∧ ψ ⊆ H .-φ. Thus in either case H .-φ∧ψ ⊆ H .-φ. Let μ ∈ H .-ψ then [H .-ψ] ⊆ [μ]. We are going to show μ ∈ Z. By (H .-pa) we have H .-ψ∩Cn(ψ) ⊆ H .-φ ∧ ψ ⊆ H .-φ ⊆ Z. So by model theory we have [Z] ⊆ [H .-φ] ⊆ [H .-φ∧ψ] ⊆ [H .-ψ ∩Cn(ψ)] ⊆ [μ] ∪ [ψ]. Z ∈ H ↓w ψ implies Z ̸⊢ ψ, hence [Z] ̸⊆ [ψ]. By (H .-2), μ ∈ H .-ψ ⊆ H, so [H] ⊆ [μ]. By Definition 1 we have Z = Cnh (Z) and [Z] = Cl∩([H]∪{u}) for some u ∈ [¬ψ]. It follows from u ∈ [Z] ⊆ [ψ] ∪ [μ] and u ∈ [¬ψ] that u ∈ [μ]. It then follows from μ ∈ LH (i.e., its models are closed under intersection), [H] ⊆ [μ] and u ∈ [μ] that [Z] = Cl∩([H] ∪ {u}) ⊆ [μ] which implies Z ⊢ μ. Since Z = Cnh (Z), Z ⊢ μ implies μ ∈ Z.

(2). Let X, Y and Z be weak remainder sets of H and suppose X ⩽ Y and Y ⩽ Z. We need to show X ⩽ Z. In the case that Z = H, X ⩽ Z follows from condition (i). In the case that Z ̸= H, we have to show conditions (iia)-(iib) for deriving X ⩽ Z are satisfied. Condition (iia) follows from the definition of Y ⩽ Z and Z ̸= H. For condition (iib), suppose ψ ∈ LH, X, Z ∈ H ↓w ψ, and H .-ψ ⊆ X. It remains to verify H .-ψ ⊆ Z. It follows from Y ⩽ Z, Z ̸= H and the definition of ⩽ that Y ̸= H. It follows from Y ̸= H, X ⩽ Y and condition (iia) that there is some φ ∈ H such that H .-φ ⊆ Y ∈ H ↓w φ. By part 2 of Lemma 1, we have H ↓w φ ∧ ψ = (H ↓w φ) ∪ (H ↓w ψ) from which it follows that X, Y,Z are all elements of H ↓w φ ∧ ψ. By (H .-c), either H .-φ ∧ ψ ⊆ H .-φ or H .-φ ∧ ψ ⊆ H .-ψ.

Second case, H .-φ ∧ ψ ⊆ H .-ψ. Since H .-ψ ⊆ X, we have H .-φ ∧ ψ ⊆ X. It then follows from condition (iib) and X ⩽ Y that H .-φ ∧ ψ ⊆ Y . Similarly, it follows from condition (iib) and Y ⩽ Z that H .-φ ∧ ψ ⊆ Z.

First case, H .-φ ∧ ψ ⊆ H .-φ. Since H .-φ ⊆ Y , we have H .-φ ∧ ψ ⊆ Y . It then follows from condition (iib) and Y ⩽ Z that H .-φ ∧ ψ ⊆ Z.

So in both cases H .-φ ∧ ψ ⊆ Z. Let μ ∈ H .-ψ. We are going to show μ ∈ Z. μ ∈ H .-ψ implies [H .-ψ] ⊆ [μ]. By (H .-pa) we have H .-ψ ∩ Cn(ψ) ⊆ H .-φ ∧ ψ ⊆ Z. So by model theory [Z] ⊆ [H .-φ ∧ ψ] ⊆ [H .-ψ ∩ Cn(ψ)] ⊆ [ψ] ∪ [μ]. Z ̸⊢ ψ follows from Z ∈ H ↓w ψ, and it implies [Z] ̸⊆ [ψ]. By (H .-2), μ ∈ H .-ψ ⊆ H, which implies

[H] ⊆ [μ]. It follows from Definition 1 and Z ∈ H ↓w ψ that Z = Cnh (Z) and [Z] = Cl∩([H]∪{u}) for some u ∈ [¬ψ]. It then follows from u ∈ [Z] ⊆ [ψ] ∪ [μ] and u ∈ [¬ψ] that u ∈ [μ]. Finally from μ ∈ LH (i.e. its models are closed under intersection), [H] ⊆ [μ] and u ∈ [μ] we have Z = Cl∩([H]∪{u}) ⊆ [μ] that is [Z] ⊆ [μ] which implies μ ∈ Z. ✷

Let a PMHC .- for H be determined by a selection function γ. If .- satisfies (H .-pa) and (H .-8), then by Lemma 4, ˆ γ is transitively relational. Lemma 3 guarantees that ˆ γ determines the same PMHC as γ does, so .- is also determined by ˆ γ, and since ˆ γ is transitively relational, .- is a transitively relational PMHC. Combining Theorem 1, Lemma 2 and Lemma 4 we obtain the representation theorem for TRPMHC.

Theorem 2 Let H be a Horn belief set. .- is a TRPMHC for H iff .- satisfies (H .-1)-(H .-4), (H .-f), (H .-6), (H .-wr), (H .-pa) and (H .-8).

In subsequent sections we investigate PMHCs whose determining selection functions are constrained by-in addition to transitivity and relationality-connectivity and maximality.

4.3 Connectively TRPMHC

As mentioned in Section 3, the relation ⩽ is intended to capture the intuition that X ⩽ Y iff Y is at least as plausible as X. It is reasonable to enforce connectivity on the relation ⩽ so that all pairs of X, Y are comparable by ⩽. A selection function γ is connectively relational over a belief set K if it is generated from a connected relation of K via the marking off identity. We call such a γ a connected selection function.

Connectivity is shown in [Alchourr´on et al., 1985] to be a redundant requirement for selection functions that are transitively relational. For each transitively relational PMC .-, there is a transitively and connectively relational PMC that is identical to .-, and vice versa. This is also the case for TRPMHC.

Theorem 3 Let H be a Horn belief set and .- be a PMHC over H, then .- is transitively relational over H iff it is transitively and connectively relational over H.

In fact, all selection functions for determining TRPMC are connected [Alchourr´on et al., 1985] 3 . This is easy to verify. Assume the transitively relational selection function γ for a belief set K is not connected thus the transitive relation ⩽ for generating γ is not connected. Let X, Y be the only remainder sets of K with respect to φ 4 such that neither X ⩽ Y nor Y ⩽ X. If .- is the TRPMC determined by γ then K .-φ = ⋂ γ(H ↓ φ) = ⋂ γ(X, Y ) is undefined, thus violates the definition of selection function.

However, as illustrated in Example 2, selection functions for determining TRPMHC need not be connected. Let X, Y be a pair of weak remainder sets for a Horn belief H. Due to the closure property, we may not have a Horn formula φ with respect to which X, Y are the only weak remainder sets i.e., H ↓w φ = {X, Y }. So, without knowing the relation between X and Y , the transitive relation for H can still determine a selection function that covers all Horn formulas.

3 The result only hold for belief set that are finite modulo Cn, as we assume a finite propositional language, this is always the case.

4 By property of remainder set such φ always exists.

Example 2 Let P = {p, q}, and let Horn belief set H = Cnh (p ∧ ¬q), then [H] = {p} and [¬(p ∧ ¬q)] = {pq, q, ∅}. Suppose [X] = Cl∩([H] ∪ {pq}), [Y ] = Cl∩([H] ∪ {q}), [Z] = Cl∩([H] ∪ {∅}) such that X, Y and Z are closed under Cnh , then X, Y and Z are weak remainder sets of H. Assume H ↓w φ = {X,Z}, then [¬φ] = [pq, ∅] and [φ] = {p, q}. It follows from p ∩ q = ∅ and ∅ ̸∈ [φ] that [φ] ̸= Cl∩([φ]) which implies φ ̸∈ LH. Thus there is no Horn formula φ with respect to which X and Z are the only weak remainder sets of H.

4.4 Maximisingly TRPMHC

As a fundamental principle of the AGM framework, loss of previous beliefs should be kept to a minimum whenever possible. Therefore, preference relations such as those used in TRPMHC should put more value on a set than any of its proper subsets. We then say that a relation ⩽ for K is maximised if for all remainder sets X, Y of K, X ⊂ Y implies X < Y ; it is weak maximised if X ⊂ Y implies X ⩽ Y [Hansson, 1999]. A selection function is called maximisingly relational (weak maximisingly relational) iff it is generated from a maximised (weak maximised) relation via the marking off identity. Under propositional logic, if X, Y are remainder sets of K, then neither X ⊆ Y nor Y ⊆ X. Therefore the relation over remainder sets of K is always maximised, leaving (weak) maximality as a vacuous requirement on TRPMCs. We no longer have this neat property with weak remainder sets. As illustrated in Example 1, weak remainder sets can be proper subsets of one another. The relation over weak remainder sets may not be maximised.

It is easy to see that for any selection function that is not weak maximised, its completion is weak maximised. By Lemma 3, we have, for each pair of selection function and its completion, that the PMHCs they determine are identical. So for any selection function γ that is not weak maximised there is a weak maximised one that determines the same PMHC as γ does, and vice versa. Thus weak maximality is redundant for TRPMHC as well. Unlike weak maximality, maximality does have some effect on TRPMHC. In Example 1, if the non-maximised selection function γ is such that γ(H ↓w (a ∧ b)) = {X1}, then due to the fact that X1 ⊂ X2, there is no maximised selection function that determines an identical PMHC as γ does. A PMHC determined by a maximisingly and transitively relational selection function is abbreviated as MTRPMHC. A MTRPMHC satisfies the Horn analogue of the relevance postulate, which implies (H .-wr).

Theorem 4 Let H be a Horn belief set. .- is a maximised TRPMHC for H iff .- satisfies (H .-1)-(H .-4), (H .-f), (H .-6), (H .-pa), (H .-8), and the following postulate: (H .-r) If ψ ∈ H \ (H .-φ), then there is some H′ such that H .-φ ⊆ H′ ⊆ H and φ ̸∈ Cnh (H′ ) but φ ∈ Cnh (H′ ∪ {ψ}).

Sketch of proof: By maximality of selection function, weak remainder sets selected have the maximal property such that for φ, ψ in H, if X ∈ γ(H ↓w φ) and ψ ̸∈ Cnh (X), then φ ∈ Cnh (X ∪ {ψ}), which handles satisfaction of (H .-r). In turn (H .-r) implies maximality of the selection function. Clearly, if .- is a MTRPMHC, then it is a TRPMHC, but the converse is not true.

4.5 Connections with AGMContraction

Given a transitive and connected relation ⩽ for a Horn belief set H, we define a relation ⪯⩽ for belief set Cn(H) as X ⪯⩽ Y iff Horn(X) ⩽ Horn(Y ) for X, Y remainder sets of Cn(H). By Part 1 of Lemma 1, X, Y are remainder sets of Cn(H) iff Horn(X) and Horn(Y ) are weak remainder sets of H, so that ⪯⩽ is well defined. Clearly, ⪯⩽ is a relation over remainder sets of belief set Cn(H). As ⩽ is transitive and connected, so is ⪯⩽. We require ⩽ to be connected as all selection functions for determining TRPMCs are connected.

Now we establish the explicit relationship between TRPMHCs and AGM contraction, in particular TRPMC.

Theorem 5 Let .-be a connected TRPMHC for aHorn belief set H based on ⩽. Let ∼ be a TRPMC for Cn(H) based on ⪯⩽. Then H .-φ = (Cn(H) ∼ φ) ∩ H.

Proof: By the construction of ∼, we have Cn(H) ∼ φ = ⋂(X1, . . . ,Xn) for X1, . . . ,Xn ∈ Cn(H) ↓ φ. It then follows from Part 3 of Lemma 1 and the definition of ⪯⩽ that H .-φ = ⋂(Horn(X1), . . . ,Horn(Xn)) = Horn(⋂(X1, . . . ,Xn)) = Horn(Cn(H) ∼ φ) = (Cn(H) ∼ φ) ∩ H.

✷

The theorem highlights the appropriateness of the Horn contraction constructed as a connected TRPMHC. A formula is retained in the Horn contraction iff it is an element of the Horn belief set and it is retained in the corresponding AGM contraction. As clarified earlier, for each non-connected TRPMHC .- there is a connected TRPMHC that performs identically to .-. Thus we can omit the connectivity requirement in Theorem 5, and conclude that TRPMHC retains as many Horn formulas as its corresponding TRPMC does.

4.6 Loss of Uniqueness

It is shown in [Alchourr´on et al., 1985] that all selection functions for determining PMC are completed. Firstly, due to the following lemma, different selection functions determine different PMCs.

Lemma 5 [Alchourr´on et al., 1985] Let K be any belief set finite modulo Cn, and let γ and γ ′ be selection functions for K. If γ(K ↓ φ) ̸= γ ′ (K ↓ φ), then ⋂ γ(K ↓ φ) ̸= ⋂ γ ′ (K ↓ φ).

But we know a selection function determines the same PMC as its completion does, so, for this to hold it must be that the selection function is identical to its completion, that is it is itself completed. As shown in the following example, Lemma 5 no longer holds for selection functions that determine PMHCs, so that, they may not be completed.

Example 3 Continuing with Example 1, let a selection function γ for H be such that γ(H ↓w (a ∧ b)) = {X1,X5}. Then ⋂ γ(H ↓w (a ∧ b)) = X1 ∩ X5. Since X1 ⊂ X2 and X5 ⊂ X6, we have ⋂ γ(H ↓w (a ∧ b)) ⊆ X2 and

⋂ γ(H ↓w (a ∧ b)) ⊆ X6. Thus the completion ˆ γ is such that ˆ γ(H ↓w (a ∧ b)) = {X1,X2,X5,X6} and ⋂ ˆ γ(H ↓w (a ∧ b)) = X1 ∩ X5. Note that γ is different from ˆ γ, yet ⋂ γ(H ↓w (a ∧ b)) = ⋂ ˆ γ(H ↓w (a ∧ b)).

The observation implies that different selection functions may yield identical TRPMHCs. This is counterintuitive. As the relation ⩽ (and the selection function generated from ⩽) of a belief set represents an agent's perspective on what beliefs are more plausible, ideally each perspective would have different effects on the way the contraction is performed. That is, each relation yields a unique contraction. This uniqueness property is lost by turning to Horn logic. This is also evidenced by connectively and maximisingly relational TRPMHCs since for each non-connected (non-maximised) selection selection function, there exists a connected (maximised) one that determines an identical TRPMHC as the non-connected (non-maixmised) one does, and vice versa.

5 RelatedWork

Existing work on Horn contraction falls roughly into two groups: those focussing on the basic postulates [Booth et al., 2009; 2010; Delgrande and Wassermann, 2010] and those focussing on the full set of postulates by taking into account preference information over remainder sets [Delgrande, 2008; Zhuang and Pagnucco, 2010b] or over formulas [Zhuang and Pagnucco, 2010a]. Contractions of the second group are more sophisticated as we can now make use of the preference information when they have been made available in certain forms.

The construction of PMHC does not assume any explicit preference information. In this respect, PMHC is similar to the Horn e-Contraction (HEC) studied in [Booth et al., 2009]. Instead of weak remainder sets, HEC is based on infra remainder sets. Both notions of Horn remainder set try to stick to the behaviour of standard remainder sets but they have different emphases. Weak remainder sets unify their model theoretic behaviour to that of standard remainder sets. Infra remainder sets unify themselves to the convexity property of PMC. This property states that every belief set that is, by set inclusion, in between the ones obtained by the two limiting cases of PMC-maxichoice contraction and full meet contraction-is obtainable by intersection of some of the remainder sets. As shown in [Delgrande and Wassermann, 2010] neither notion is more expressive or more suitable than the other in terms of constructing Horn contractions. However we find that the notion of weak remainder set is more adaptable for including preference information to the construction of Horn contraction. In order to characterise HEC, we need (H .-1)-(H .-4), (H .-f) and (H .-cr):

H .-φ ⊆ H′ and φ ̸∈ Cnh (H′ ) but φ ∈ Cnh (H′ ∪ {ψ}). (H .-cr) is the Horn analogue of the core-retainment postulate [Hansson, 1999]. Clearly (H .-cr) follows from (H .-r), and since MTRPMHC also satisfies the remaining charaterising postulates of HEC, if .- is a MTRPMHCs, then it is a HEC.

If ψ ∈ H \ (H .-φ), then there is some H′ such that

The maxichoice e-contraction (MEC) studied in [Delgrande, 2008] is essentailly the Horn analogue of a special case of TRPMC, in which the relation over remainder sets (for generating a selection function which in turn determines the TRPMC) is required to be, in addition to transitive, antisymmetric. Such contractions might be regarded as orderly maxichoice PMCs. The definition of the Horn remainder set used in MEC is the same as standard remainder sets but restricted to Horn formulas and Horn derivability. This notion of Horn remainder set is not as expressive as that of weak remainder set and infra remainder set [Delgrande and Wassermann, 2010]. Every such Horn remainder set is a weak remainder set as well as an infra remainder set, but the converse is not true. Due to this nature of MEC, each MEC is a PMHC as well as a HEC. In order to characterise MEC we need (H .-1)-(H .-4), (H .-f), and (H .-8e):

If ψ ̸∈ H .-(φ ∧ ψ) then H .-(φ ∧ ψ) = H .-ψ.

The EEHC of [Zhuang and Pagnucco, 2010a] is the Horn analogue of the epistemic entrenchment based contraction [G¨ardenfors and Makinson, 1988] which assumes an ordering over formulas of the belief set. Our TRPMHC supersedes EEHC in the sense that for each EEHC .-, there is a TRPMHC that behaves identically to .- [Zhuang and Pagnucco, 2010b] implying that if .- is an EEHC, then it is a TRPMHC. In order to characterise EEHC we need (H .-1)- (H .-4), (H .-f), (H .-ct), (H .-9) and (H .-10). The combination of (H .-9) and (H .-10) gives the Horn analogue of the condition φ ∨ ψ ∈ K .-φ iff ψ ∈ K .-φ [G¨ardenfors and Makinson, 1988].

The representation results for Horn contractions are summarised in Figure 1 where the arrows are pointing to the more general contractions.

6 Conclusion and FutureWork

In this paper we proposed a fully characterised construction of the contraction operation under Horn logic, namely TRPMHC. TRPMHC extends the PMHC in [Delgrande and Wassermann, 2010] by taking into account preference information in the form of an ordering over remainder sets. Several variants of TRPMHC are studied, however, only the TRPMHCs constrained by maximality, that is MTRPMHC, are distinguishable from TRPMHC. The plausibility of TRPMHC is investigated against AGM contractions where the results demonstrate that TRPMHCs perform identically to their corresponding AGM contractions in terms of Horn formulas.

Existing work on constructing Horn contractions have utilised preference information represented as orderings over various notions of remainder sets as in TRPMHC and MEC, and orderings over formulas as in EEHC. Another classic approach in defining AGM contractions is based on preference information as an ordering over possible worlds [Grove, 1988; Katsuno and Mendelzon, 1992]. So for future work, we aim to give a model theoretic account of Horn contraction, in particular for TPMHC. Such model based Horn contraction would give a semantics for the TRPMHC in the same way as the model based contraction in [Grove, 1988; Katsuno and Mendelzon, 1992] does to TRPMC.