Definability of Horn Revision from Horn Contraction

1 Introduction

AGM revision 1 can be constructed directly, as in [Grove, 1988; Katsuno and Mendelzon, 1992], through systems of spheres (i.e., total preorders of interpretations) or, as in [G¨ardenfors and Makinson, 1988], through epistemic entrenchment (i.e., total preorders of sentences) as well as several other methods. Alternatively, a revision can be constructed indirectly through a contraction via the Levi identity [Levi, 1991]. 2 The idea is that to revise a belief set K by a formula φ, we first contract by the negation of φ then expand by φ. Formally, let - be a contraction function for K and + the expansion function, then a revision function ∗ for K can be defined as

1 AGM revision (contraction) refers to a revision (contraction) that satisfies the full set of AGM revision (contraction) postulates.

2 Commonly, the belief revision community understands a revision, through the so-called Levi identity, as a contraction followed by an expansion. However, this is a simplification of Levi's original idea [Levi, 1991] as expressed by his Commensurability Thesis (p. 65) which essentially states that one can get from one state of belief to another through a sequence of expansions and contractions.

for all formulas φ. The purpose of the contraction step is to remove all formulas that are inconsistent with the revising formula. As a result, the belief set obtained after the expansion step is guaranteed to be consistent. The revision operation thus defined is an AGM revision if and only if the contraction is an AGM one [Alchourr´on and Makinson, 1985]. Also, there is a bijection between the contraction functions and the obtained revision functions. Each AGM revision function is definable from an AGM contraction function and each revision function defined from an AGM contraction function is an AGM revision function.

Recent years have seen significant effort in defining AGM style contraction and revision that operate under Horn logic (i.e., Horn contraction and Horn revision) [Delgrande, 2008; Delgrande and Wassermann, 2010; Booth et al., 2009; 2010; 2011; Delgrande and Peppas, 2011; Zhuang and Pagnucco, 2010; 2011; 2012]. However, none of these have explored the interdefinability of Horn contraction and Horn revision. In this paper, we fill this gap by giving an indirect construction of Horn revision via a variant of the Levi identity. Specifically, we obtain a model-based Horn revision from the modelbased Horn contraction (MHC) of [Zhuang and Pagnucco, 2012].

The only Horn revision studied so far is the model-based Horn revision (MHR) of [Delgrande and Peppas, 2011] which is a direct construction that adapts the approach of [Katsuno and Mendelzon, 1992]. Thus, focusing on a modelbased approach makes it easier to compare with this direct approach. Also, MHC subsumes all the Horn contractions studied so far that assume explicit preference information. It is equivalent to the transitively relational partial meet Horn contraction (TRPMHC) in [Zhuang and Pagnucco, 2011] and more general than the epistemic entrenchment Horn contraction (EEHC) in [Zhuang and Pagnucco, 2010]. MHC and MHR are reviewed in Section 3.

The main difficulty in obtaining such revision is the lack of negation in Horn logic. In the contraction step of obtaining a revision function via the Levi identity, we need to contract by the negation of the revising formula. However the negation of a Horn formula may be non-Horn and Horn contraction functions do not operate on non-Horn formulas. We overcome this difficulty by using the notion of Horn strengthening [Kautz and Selman, 1996] which is introduced in Section 4. Horn strengthenings for a non-Horn formula φ are logically the weakest Horn formulas that entail φ. The contraction of a non-Horn negation is then replaced by contractions of its Horn strengthenings. This replacement, however, brings in another difficulty.

Since a non-Horn formula has at least two Horn strengthenings and each Horn strengthening is logically stronger than the non-Horn formula, to thoroughly remove a nonHorn negation (so that the later expansion operation will not cause any inconsistency) all its Horn strengthenings have to be removed. This means we need a sequence of contractions such that each contraction removes one Horn strengthening. MHC as well as AGM contraction are single-step contractions which means certain iteration schemes are required for carrying out a sequence of such contractions. Recently, [Ramachandran et al., 2012] discussed three main iteration schemes for contraction. As we will argue, the scheme of conservative contraction is most suitable here which is adapted to iterated Horn contraction in Section 4.

It is shown in Section 5 that, with the above procedure, MHC might generate Horn revisions that behave counterintuitively. To avoid this, MHC has to be properly restricted. For this purpose, we introduce the condition of strict Horn compliance which restricts the allowable preorders for determining MHC. As it turns out, strict Horn compliance is a sufficient condition for avoiding the counterintuitive case. Moreover, with such condition, the generated Horn revision is a restricted form of MHR. The result suggests that, under the restriction of strict Horn compliance, Horn revision is definable through Horn contraction.

2 Technical Preliminaries

We assume a propositional language L over a finite set of atoms P which is closed under the usual truth-functional connectives and contains the propositional constants ⊤ (truth) and ⊥ (falsum). Atoms are denoted by lower case Roman letters (p, q, . . .). Formulas are denoted by lower case Greek letters (φ, ψ, . . .). Sets of formulas are denoted by upper case Roman letters (V,X, . . .). A clause is a disjunction of positive and negative atoms. A Horn clause is a clause with at most one positive atom. A Horn formula is a conjunction of Horn clauses.

The logic generated from L is specified by the standard Tarskian consequence operator Cn. For any set of formulas X, Cn(X) denotes the set of formulas following logically from X. For any formula φ, Cn(φ) abbreviates Cn({φ}). We sometimes write X ⊢ φ to denote φ ∈ Cn(X), φ ≡ ψ to denote Cn(φ) = Cn(ψ), and ⊢ φ to denote φ ∈ Cn(∅). The letter K is reserved to represent a theory or a belief set which is a set of formulas such that K = Cn(K).

Standard two-valued model-theoretic semantics is assumed. The set of all interpretations is denoted by Ω. An interpretation µ is a model of a formula φ if φ is true in µ, written µ |= φ. For any set of formulas X, |X| denotes the set of models of X. For any formula φ, |φ| abbreviates |{φ}|. For P = {a, b, c, . . .}, we write an interpretation as a bit vector; for example, 011 . . . to indicate that a is assigned false, b is assigned true, c is assigned true, etc. The theory operator T : 2Ω → 2L is such that, given a set of interpretations M, T (M) is the set of formulas that are true in all interpretations of M. Formally, T (M) = {φ ∈ L : µ |= φ for every µ ∈ M}.

The Horn language LH is the subset of L containing only Horn formulas. The Horn logic generated from LH is specified by the consequence operator CnH such that for any set of Horn formulas X, CnH(X) = Cn(X) ∩ LH. The letter H is reserved to represent a Horn theory or a Horn belief set which is a set of Horn formulas such that H = CnH(H). The Horn theory operator TH : 2Ω → 2LH is such that, given a set of interpretations M, TH(M) is the set of Horn formulas that are true in all interpretations of M. Formally, TH(M) = {φ ∈ LH : µ |= φ for every µ ∈M}.

The intersection of two interpretations is the interpretation that assigns true to those atoms that are assigned true by both interpretations. We denote the intersection of interpretations µ and ν by µ ∩ ν, e.g., 001 ∩ 101 = 001. If µ ∩ ν = ω then we say µ and ν induce ω. Given a set of interpretations M, the closure of M under intersection is denoted by Cl∩(M). Formally, Cl∩(M) = {ω : ω ∈ M or ∃µ, ν ∈ M such that µ ∩ ν = ω}. For any Horn formula, its set of models is closed under Cl∩, and we call it Horn closed. Conversely, any Horn closed set of models corresponds to an unique Horn formula. Moreover, intersections of Horn closed sets of models are also Horn closed.

3 Model Based Horn Revision andModel Based Horn Contraction

In the account of [Katsuno and Mendelzon, 1992], a preorder ⪯ is a reflexive and transitive binary relation over Ω. The strict relation ≺ is defined as µ ≺ ν iff µ ⪯ ν and ν ̸⪯ µ. The equivalence relation =⪯ is defined as µ =⪯ ν iff µ ⪯ ν and ν ⪯ µ. A preorder is total if for every pair of µ, ν ∈ Ω, either µ ⪯ ν or ν ⪯ µ. Let M be a set of interpretations, min⪯(M) represents the minimal models of M:

We abbreviate min⪯(|φ|) as min⪯|φ|. A preorder ⪯ is faithful with respect to K iff min⪯(Ω) = |K|. If a revision function ∗ for K is defined as K ∗ φ = T (min⪯ |φ|) for all φ ∈ L then ∗ is an AGM revision function iff ⪯ is a faithful total preorder. The preorder ⪯ is referred to as the determining preorder for ∗ and we say ∗ is determined by ⪯.

The model theoretic account can also be applied to contraction through the Harper Identity. In this account, a contraction function - for K is defined as K - φ = T (|K| ∪ min⪯ |¬φ|) for all φ. The contraction thus defined is an AGM contraction function iff ⪯ is a faithful total preorder.

In accordance with [Katsuno and Mendelzon, 1992], Delgrande and Peppas [Delgrande and Peppas, 2011] studied model-based revision under Horn logic. Apart from total and faithful, the preorders that determine their Horn revision functions have to be Horn compliant. A preorder ⪯ is Horn compliant iff for every φ ∈ LH, min⪯|φ| = Cl∩(min⪯|φ|). It is noted in [Zhuang and Pagnucco, 2012] that a preorder ⪯ is Horn compliant iff it satisfies the following condition:

A MHR function ∗ for H is defined as

for all φ ∈ LH, where ⪯ is a faithful total and Horn compliant preorder for H. A function ∗ is a MHR function iff it satisfies the following postulates [Delgrande and Peppas, 2011].

(H∗1)-(H∗8) are obtained simply by recasting the standard AGM revision postulates to Horn logic. Thus they carry the same meaning as the AGM postulates except that they operate under Horn logic. Preorders are acyclic, however, in some cases, cyclic orders of interpretations can determine Horn revision functions that satisfiy (H∗1)-(H∗8). (H∗a) rules out such functions by enforcing transitivity on the orderings of interpretations. Due to HC, min⪯|φ| is Horn closed for all φ ∈ LH, thus for any MHR function ∗, |H ∗φ| = min⪯|φ|. If ⪯ does not satisfy HC then min⪯|φ| may contain µ, ν such that µ ∩ ν = ω and ω ̸∈ min⪯|φ|. As shown in [Delgrande and Peppas, 2011], the Horn revision function determined by such a preorder violates (H∗7) and (H∗8) and the culprits are the induced models like ω. So, informally speaking, the key for the satisfaction of (H∗7) and (H∗8) is to assure the models of H ∗ φ coincide with the minimal models of φ.

As a complement to [Delgrande and Peppas, 2011], Zhuang and Pagnucco [Zhuang and Pagnucco, 2012] studied model-based contraction under Horn logic. The preorder used for determining the Horn contraction is faithful and total but not necessarily Horn compliant. A MHC - for H is defined as:

for all φ ∈ LH, where ⪯ is a faithful total preorder for H. It is shown in [Zhuang and Pagnucco, 2012] that there is no condition that guarantees the Horn closeness of |H| ∪min⪯|¬φ| for all φ ∈ LH. Thus we may have ω ∈ |H - φ| but ω ̸∈ |H| ∪ min⪯|¬φ|. As evidenced by the representation result of MHC, induced models like ω do not prohibit MHC from satisfying the supplementary postulates for contraction.

From the study of MHR and MHC, Horn compliance is mandatory for generating meaningful Horn revision, but not for Horn contraction. It will be clear from Section 5 that if Horn contraction functions are used as an intermediate step for generating Horn revision functions then a stricter condition is required.

4 DealingWith Non-Horn Negations

An obvious obstacle in generating Horn revision from Horn contraction is the lack of negation in Horn logic. For example, in the revision of ¬p ∧ ¬q via the Levi identity, we need to first contract by the negation of ¬p∧¬q, however the negation (i.e., p ∨ q) is not a Horn formula. In this case, we can not apply MHC functions in the contraction step as they only take Horn formulas as input. One natural way to get around this problem is to contract by the Horn approximations of the nonHorn negation. The notion of Horn strengthening [Kautz and Selman, 1996] has proved to be useful in this situation which is used as the Horn approximations of non-Horn formulas in constructing EEHC.

A Horn strengthening of a formula φ is, logically, the weakest Horn formula that entails φ.

Definition 1 [Kautz and Selman, 1996] Let φ be a formula. The set of Horn strengthenings of φ, denoted as HS(φ), is such that χ ∈ HS(φ) iff

1. |χ| ⊆ |φ|,

The following lemma concerning the intersection of the models of Horn strengthenings will be used in proving the main results.

Proof: Suppose φ ∈ L and HS(φ) = {χ1, . . . , χn}. We first show that |φ| = |χ1| ∪ · · · ∪ |χn|. |χ1| ∪ · · · ∪ |χn| ⊆ |φ| follows directly from Definition 1. For the other inclusion, assume there is u ∈ |φ| such that u ̸∈ |χ1| ∪ · · · ∪ |χn|. Let ψ be such that |ψ| = {u}, then ψ is a Horn formula and |ψ| ⊆ |φ|. [Kautz and Selman, 1996] showed that if ψ ∈ LH is such that |ψ| ⊆ |φ|, then there is χ ∈ HS(φ) such that |ψ| ⊆ |χ|. It then follows from |ψ| ⊆ |φ| that there is a χ ∈ HS(φ) such that |ψ| ⊆ |χ|. A contradiction ensues. We then have |¬φ| = |¬χ1| ∩ · · · ∩ |¬χn| by De Morgan's law. □

A non-Horn formula has at least two Horn strengthenings and each implies the non-Horn formula. To guarantee consistency after the expansion, all Horn strengthenings of the nonHorn negation have to be removed in the contraction step. The standard approach to remove several items of information simultaneously is to apply a package contraction [Fuhrmann and Hansson, 1994]. AGM contraction and the Horn contractions studied so far are in fact singleton contractions which take as input one formula and return as output a belief set that does not imply the formula. In contrast, package contractions take as input a set of formulas and return as output a belief set that does not imply any formula in the set. However, this approach is not appropriate in the current context, as our goal is to investigate the definability of singleton Horn revision through singleton Horn contraction. Therefore, instead of a package contraction we will apply a sequence of singleton contractions that remove the Horn strengthenings one by one. Importantly, to obtain a revision by performing a sequence of contractions and an expansion is in accordance with Levi's original idea on the nature of the revision operation [Levi, 1991].

The need to perform a sequence of contractions gives rise to another difficulty. Singleton contractions are "one shot" operations that do not specify the posterior preference information associated with the contracted belief set, therefore subsequent contractions are not possible. For instance, a MHC function - for H does not specify the posterior preorder for the contracted Horn belief set H -φ thus no further contraction can be determined for the set H - φ. The standard approach is to apply an iteration scheme. Let - be a model-based contraction for K determined by the preorder ⪯. In contracting φ, an iteration scheme specifies a posterior preorder, written as ⪯-φ , for the posterior belief set K-φ. In this way, a contraction for K - φ can be determined by ⪯-φ .

Several iteration schemes are proposed for contraction such as priority contraction [Nayak et al., 2006], conservative contraction [Rott, 2006], and lexicographic contraction [Nayak et al., 2007]. 3 Roughly speaking, priority contraction gives precedence to new beliefs, conservative contraction gives precedence to old beliefs, and lexicographic contraction treats the old and new beliefs the same. Since the sequence of contractions is intended to replace a single contraction, it makes sense to retain as much as possible the prior preorder in each iteration so that the sequence of contractions better mimics the behaviour of a single contraction. For this reason, conservative contraction is most suitable as it best retains the prior preorder. 4 Conservative contraction is characterised by the following conditions.

In contracting φ, C1 assures that the resulting models are most preferred in the posterior preorder which guarantees its faithfulness, and C2 assures that the rest of the posterior preorder is identical to the prior one.

C1 and C2 have to be modified for iterated Horn contraction. Suppose - is a MHC function for H determined by ⪯. There may be ω ∈ |H - φ| such that ω ̸∈ |H| ∪ min⪯|¬φ|. Since C2 does not guarantee the minimality of ω in ⪯-φ , |H - φ| ̸= min⪯-φ (Ω) which means ⪯-φ is not faithful (with respect to H - φ). As the determining preorders for MHC functions have to be faithful, ⪯-φ can not be used for determining MHC functions for H - φ. We therefore modify C1 such that the induced models like ω are made minimal and to avoid conflicts, we modify C2 such that it does not apply to such models.

3 The schemes are defined specifically for model-based contractions though it is straightforward to recast them to, for example, epistemic entrenchment contraction.

4 In fact, by using the other two schemes we obtain the same Horn revision as the one obtained by using conservative contraction. The reason is that the properties of conservative contraction that are required to show properties of the obtained Horn revision are shared by all schemes.

In subsequent sections, with any contraction sequence ((· · · ((H -1 χ1) -2 χ2) · · ·) -n χn) we assume that HC1 and HC2 are applied throughout the sequence and we take the convention that ⪯-i φi is the preorder specified by HC1 and HC2 after contracting φi through -i (for 1 ≤ i ≤ n) such that -1 is a MHC function determined by the preorder ⪯ for H, and -i (2 ≤ i ≤ n) is a MHC function determined by the preorder ⪯-i-1 φi-1 for ((· · · ((H-1 φ1)-2 φ2) · · ·)-i-1 φi-1).

5 Contraction Generated Horn Revision

By replacing a contraction by a non-Horn negation with sequences of contractions by Horn stengthenings of the nonHorn negation, a Horn revision can be constructed indirectly as follows.

Definition 2 ∗ is a contraction generated Horn revision (CGHR) function for H iff

Notice that once the first contraction -1 is fixed, subsequent contractions are also fixed as their determining preorders are specified by HC1 and HC2 from the preorder for H (which determines -1). Thus a CGHR function for H is fully determined by the preorder for H. In Definition 2 we did not specify the order in which the Horn strengthenings are contracted. The reason will be discussed towards the end of this section.

This construction however does not give us MHR and it leads to counterintuitive results. Consider the Horn language with P = {a, b}. Let |H| = {01}, |φ| = {00, 11, 10}, and the preorder ⪯ for H be 01 ≺ 10 ≺ 11 ≺ 00. For the revision of H by φ, Figure 1 illustrates, in a system of spheres setting, the resulting models (indicated by the shaded area) of the revision through a CGHR function (left diagram) and through a MHR function (right diagram). According to the intuition of model-based revision, the revision by φ should end up with models of φ that are closest to those of H (i.e., the minimal models of φ by means of a preorder). Counterintuitively, the CGHR function in Figure 1 returns 10 and 00 as the resulting model. Given that 11, which is closer to |H| than 00, is not taken as a resulting model, it does not make any sense taking 00 as a resulting model. Notice that enforcing HC does not help, as ⪯ is already Horn compliant. Also the example suffices to show that not all CGHR functions are MHR functions.

Informally, the culprit is the model 00. Since ¬φ is a Horn formula whose only Horn strengthening is itself, we have |H∗φ| = |(H-¬φ)+φ| = Cl∩(|H|∪min⪯ |¬φ|)∩|φ|. 00 is taken as a resulting model of the revision merely because it is induced by 01 of |H| and 10 of min⪯ |¬φ|. This can be avoided by requiring the induced models to be more preferred than one of their inducing models, thus the following condition of strict Horn compliance.

Obviously, HC follows from SHC. Another obvious result is that if ω is induced by some elements of a model set M, then there exists µ of M such that ω ⪯ µ, provide that ⪯ satisfies SHC.

Lemma 2 Let ⪯ be a preorder that satisfies SHC. Let M be a set of models. If ω ∈ Cl∩(M) \ M then there is µ ∈ M such that ω ⪯ µ.

We define a CGHR function with a strict Horn compliant determining preorder as a strict contraction generated Horn revision (SCGHR) function.

Definition 3 ∗ is a SCGHR function for H iff ∗ is a CGHR function for H determined by a strict Horn compliant preorder.

A MHR function is determined by a preorder over all interpretations, however, the result of a particular revision is determined by the ordering between models of the revising formula. For a SCGHR function, the ordering between models of the revising formula is not altered throughout its contraction sequence.

Lemma 3 Let ⪯ be the preorder for H that is strict Horn compliant. Let φ ∈ LH be such that HS(¬φ) = {χ1, χ2, . . . , χn}. For the contraction sequence ((· · · ((H-1 χ1) -2 χ2) · · ·) -n χn), if µ, ν ∈ |φ| then

for 1 ≤ i ≤ n.

Proof: Suppose µ, ν ∈ |φ| and µ ⪯ ν. By Lemma 1, |φ| ⊆ |¬χi| for 1 ≤ i ≤ n. We first show µ ⪯-1 χ1 ν. There are three cases:

Case 1, µ, ν ̸∈ Cl∩(|H| ∪ min⪯|¬χ1|): µ ⪯-1 χ1 ν follows immediately from HC2.

Case 2, µ ∈ Cl∩(|H| ∪min⪯|¬χ1|): It follows from HC1 that µ is minimal in ⪯-1 χ1 . Thus µ ⪯-1 χ1 ν.

Case 3, ν ∈ Cl∩(|H| ∪ min⪯|¬χ1|) and µ ̸∈ Cl∩(|H| ∪ min⪯|¬χ1|): If ν ∈ |H| ∪ min⪯|¬χ1| then µ ⪯ ν implies µ ∈ |H| ∪min⪯|¬χ1|, a contradiction. If ν ̸∈ |H| ∪ min⪯|¬χ1| then by Lemma 2, there is δ ∈ |H|∪min⪯|¬χ1|

such that ν ⪯ δ. It then follows from µ ⪯ ν and the transitivity of ⪯ that µ ⪯ δ which implies µ ∈ |H| ∪ min⪯|¬χ1|, a contradiction.

µ ⪯-i χi ν for 2 ≤ i ≤ n can be proved inductively in the same manner as for ⪯-1 χ1 . The proof for the opposite direction is similar. □

Recall that the key for MHR functions to satisfy (H∗7) and (H∗8) is to ensure that their resulting models coincide with the minimal models of the revising formulas. As shown in Theorem 1, SHC suffices to guarantee this behavior for CGHR functions.

Theorem 1 Let ∗ be a SCGHR function for H that is determined by ⪯. Then

for all φ ∈ LH.

Proof: Suppose ∗ is a SCGHR function for H that is determined by ⪯ and φ ∈ LH, we need to show |H∗φ| = min⪯|φ|. Let ⪯-0 χ0 =⪯. Suppose HS(¬φ) = {χ1, χ2, . . . , χn}, then by the construction of SCGHR, we have |H ∗φ| = |((· · · ((H-1 χ1)-2χ2) · · ·)-nχn)+φ| = Cl∩(|H|∪min⪯-0 χ0 |¬χ1|∪· · ·∪ min⪯-n-1 χn-1 |¬χn|) ∩ |φ|. And it follows from Lemma 1 and HS(¬φ) = {χ1, χ2, . . . , χn} that |φ| ⊆ |¬χi| for 1 ≤ i ≤ n.

⊆: Suppose ω ∈ |H ∗ φ|, we need to show ω ∈ min⪯|φ|

There are three cases:

Case 1, ω ∈ |H|: it follows from the faithfulness of ⪯ that ω ∈ min⪯|φ|.

Case 2, there is χi such that ω ∈ min⪯-i-1 χi-1 |¬χi|: Since ω ∈ |φ| ⊆ |¬χi|, ω ∈ min⪯-i-1 χi-1 |¬χi| implies ω ∈ min⪯-i-1 χi-1 |φ|. Since min⪯|φ| = min⪯-i-1 χi-1 |φ| follows from Lemma 3, we have ω ∈ min⪯|φ|.

Case 3, ω is induced by models in |H| ∪min⪯-0 χ0 |¬χ1| ∪ · · · ∪ min⪯-n-1 χn-1 |¬χn|: Since ⪯ satisfies SHC, it follows from Lemma 2 that there is µ ∈ |H| ∪ min⪯-0 χ0 |¬χ1| ∪ · · · ∪ min⪯-n-1 χn-1 |¬χn| such that ω ⪯ µ. If µ ∈ |H| then it follows from ω ̸∈ |H| and the faithfulness of ⪯ that µ ≺ ω which contradicts ω ⪯ µ. So there is χi such that µ ∈ min⪯-i-1 χi-1 |¬χi|. Due to HC1 and HC2, the rankings for models of φ are not downgraded throughout the contraction sequence. It then follows from ω ∈ |φ| and ω ⪯ µ that ω ⪯-i-1 χi-1 µ. Thus ω ∈ min⪯-i-1 χi-1 |¬χi| which implies, as in Case 2, ω ∈ min⪯|φ|.

⊇: Suppose ω ∈ min⪯|φ|, we need to show ω ∈ |H ∗ φ|. Assume ω ̸∈ |H ∗ φ|. We first show that the assumption implies |H ∗ φ| ∩ |φ| = ∅. Assume there is µ ∈ |φ| such that µ ∈ |H ∗ φ|. There are three cases.

Case 1, µ ∈ |H|: It follows from the faithfulness of ⪯ and ω ⪯ µ that ω ∈ |H|, a contradiction.

Case 2, there is χi such that µ ∈ min⪯-i-1 χi-1 |¬χi|: It follows from Lemma 3 and ω ⪯ µ that ω ∈ min⪯-i-1 χi-1 |¬χi|, a contradiction.

Case 3, µ is induced by models in |H| ∪min⪯-0 χ0 |¬χ1| ∪ · · · ∪ min⪯-n-1 χn-1 |¬χn|: Since ⪯ satisfies SHC, it follows from Lemma 2 that there is ν ∈ |H| ∪ min⪯-0 χ0 |¬χ1| ∪ · · · ∪min⪯-n-1 χn-1 |¬χn| such that µ ⪯ ν. It then follows from ω ⪯ µ and the transitivity of ⪯ that ω ⪯ ν. Then, with the same reasoning as in Case 3 of ⊆, we derive a contradiction. Since all cases lead to contradiction, we have |H∗φ|∩|φ| = ∅. Let µ ∈ min⪯-i-1 χi-1 |¬χi|. Then there is χj such that µ ̸∈ |¬χj| for otherwise it follows from Lemma 1 that µ ∈ |φ|. Let ν ∈ min⪯-j-1 χj-1 |¬χj|. Since µ ∈ |χj|, ν ̸∈ |χj|, and ν ∈ |¬φ|, we have by the definition of Horn strengthening that µ∩ν ∈ |φ|. Since µ, ν ∈ |((· · · ((H-1χ1)-2χ2) · · ·)-n χn)| = Cl∩(|((· · · ((H-1 χ1)-2 χ2) · · ·)-n χn)|), we have µ∩ν ∈ |((· · · ((H-1χ1)-2χ2) · · ·)-nχn)|. Since |H∗φ| = |((· · · ((H -1 χ1)-2 χ2) · · ·)-n χn)| ∩ |φ|, we have µ∩ν ∈ |H ∗ φ| which implies |H ∗ φ| ∩ |φ| ̸= ∅, a contradiction.

□

A SCGHR is a sequence of contractions followed by an expansion. Interestingly, a SCGHR can always be reduced to a single contraction follow by an expansion.

Theorem 2 Let ∗ be a SCGHR function for H that is determined by ⪯. Then for all φ ∈ LH there is χ ∈ HS(¬φ) such that min⪯|¬χ| ∩ |φ| ̸= ∅ and

for - a MHC function for H that is determined by ⪯.

Proof: Let ∗ be a SCGHR function for H that is determined by ⪯. Let φ ∈ LH be such that HS(¬φ) = {χ1, . . . , χn}. Assume for all χ ∈ HS(¬φ), min⪯|¬χ| ∩ |φ| = ∅. Let µ ∈ min⪯|¬χi|. Then there is χj such that µ ̸∈ |¬χj| for otherwise it follows from Lemma 1 that µ ∈ |φ|. Let ν ∈ min⪯|¬χj|. Since µ ∈ |χj|, ν ̸∈ |χj|, and ν ∈ |¬φ|, we have by the definition of Horn strengthening that µ ∩ ν ∈ |φ|. It then follows from Lemma 1 that µ ∩ ν ∈ |¬χi| and µ ∩ ν ∈ |¬χj|. By SHC, we have either µ ∩ ν ⪯ µ or µ∩ν ⪯ ν which implies either µ∩ν ∈ min⪯|¬χi| or µ∩ν ∈ min⪯|¬χi|, a contradiction. Thus there is χ ∈ HS(¬φ) such that min⪯|¬χ| ∩ |φ| ̸= ∅. Without loss of generality, let χ1 ∈ HS(¬φ) be such that min⪯|¬χ1| ∩ |φ| ̸= ∅.

Let - be a MHC function for H that is determined by ⪯. By Theorem 1, |H ∗ φ| = min⪯|φ|. Thus it suffices to show |H - χ1 + φ| = min⪯|φ|.

• ⊆: By the construction of MHC, |H - χ1 + φ| = Cl∩(|H| ∪ min⪯|¬χ1|) ∩ |φ| ⊆ Cl∩(|H| ∪ min⪯|¬χ1| ∪ · · ·∪min⪯-n-1 χn-1 |¬χn|)∩|φ| = |H-χ1 -2 · · ·-n χn+φ| = |H ∗ φ| = min⪯|φ|.

⊇: Let ν ∈ min⪯|¬χ1| ∩ |φ|. If µ ∈ min⪯|φ| then µ ⪯ ν. By Lemma 1, |φ| ⊆ |¬χ1| which implies µ ∈ |¬χ1|. Thus it follows from ν ∈ min⪯|¬χ1| and µ ⪯ ν that µ ∈ min⪯|¬χ1|. Thus min⪯|φ| ⊆ min⪯|¬χ1| ∩ |φ| ⊆ Cl∩(|H| ∪ min⪯|¬χ1|) ∩ |φ| = |H - χ1 + φ|.

□

Theorem 2 suggests that, under the restriction of strict Horn compliance, the generation of Horn revision is exactly the same as the generation of AGM revision. That is, to first perform a contraction which eliminates any potential inconsistencies followed by an expansion.

It is generally accepted that commutativity is not a desirable property of iterated contraction [Hansson, 1999; Hild and Spohn, 2008; Hansson, 2010]. In contracting a set of formulas one by one, the order in which the formulas are contracted is crucial in determining the final result. Notice that we did not specify the ordering of contractions for SCGHR functions. According to Theorem 2, although the contraction part of two SCGHR functions may differ in the ordering, the two contraction sequences are reducible to a contraction by an identical formula. Thus the ordering in which the contractions are performed does not affect the result of SCGHR functions; an initial preorder and an iteration scheme are all we need.

It is immediate from Theorem 1 and the construction of MHR that a SCGHR function is a MHR function. More specifically, it is a MHR function with a strictly Horn compliant determining preorder. As SHC does not follow from HC the converse is not generally true.

Theorem 3 Let ∗ be a SCGHR function for H, then it is a MHR function for H.

We can conclude from Theorem 3 that MHR is definable from MHC under the restriction of strict Horn compliance.

Although we focus on obtaining Horn revision from MHC, the definability result is applicable to other Horn contractions as well. Since TRPMHC is equivalent to MHC [Zhuang and Pagnucco, 2012], it leads to the same Horn revision as MHC does. It is also shown in [Zhuang and Pagnucco, 2012] that EEHC is equivalent to the restricted form of MHC with strict Horn compliant determining preorders. Thus the MHC functions used for generating SCGHR functions are in fact EEHC functions. Thus all existing Horn contractions which assume explicit preference information lead to SCGHR. Unlike TRPMHC, MHC and EEHC, the Horn contractions defined in [Delgrande and Wassermann, 2010; Booth et al., 2011] do not assume any preference information. The generation of Horn revisions from these Horn contractions is left for future work.

6 Conclusion and FutureWork

In conclusion, we studied the definability of Horn revision from Horn contraction via a variant of the Levi identity. Importantly, the variant is in accordance with Levi's original idea on obtaining revision. The main obstacle, which is also encountered in the direct construction of Horn revision and Horn contraction, is the lack of negation for Horn logic. We proved that, under the restriction of strict Horn compliance, MHR functions are definable from MHC functions. Thus, unlike the classic case, Horn contractions have to be properly constrained for the generated Horn revision to be meaningful and not all meaningful Horn revisions can be generated from Horn contractions.

Notice that we only tackled one direction of the definability problem between Horn revision and Horn contraction. In the classic case, contraction is definable from revision via the Harper identity. Thus it remains to study the definability of Horn contraction from Horn revision via some variants of the Harper identity.

Acknowledgments

The first author was supported by An Australian Research Council Discovery Project grant (CDP0988750) when he was working as a post-doc research fellow at University of Western Sydney.