Extending the Harper Identity to Iterated Belief Change

1 Introduction

Since the publication of Darwiche and Pearl's seminal paper on the topic in the mid 90's [Darwiche and Pearl, 1997], a substantial body of research has now accumulated on the problem of iterated belief revision-the problem of how to adjust one's corpus of beliefs in response to a temporal sequence of successive additions to its members [Booth and Meyer, 2006; 2011; Boutilier, 1996; Jin and Thielscher, 2007; Nayak et al., 2003; Peppas, 2014].

In contrast, work on the parallel problem of iterated contraction-the problem of how to adjust one's corpus in response to a sequence of successive retractions-was only initiated far more recently and remains comparatively under-

Jake Chandler

La Trobe University Melbourne, Australia jacob.chandler@latrobe.edu.au

developed [Chopra et al., 2008; Hansson, 2012; Hild and Spohn, 2008; Nayak et al., 2006; 2007; Ramachandran et al., 2012; Rott, 2009].

One obvious way to level out this discrepancy would be to introduce a principle that enables us to derive, from constraints on iterated revision, corresponding constraints on iterated contraction. But while there exists a well known and widely accepted postulate connecting single-shot revision and contraction, the 'Harper Identity' [Harper, 1976], there has been no discussion to date of how to extend this principle to the iterated case. 1 One idea, which we pursue in this paper, is that whereas the Harper Identity says the belief set resulting from contracting sentence A should be formed by combining (i) the initial belief set and (ii) the belief set resulting from revision by ≻A, we look for ways to define the plausibility ordering over worlds resulting from contracting A in terms of (iii) the initial plausibility ordering, and (iv) the plausibility ordering resulting from revision by ≻A.

In the present paper, we first of all show that the simplest extension of the Harper Identity to iterated belief change is too strong a principle, being inconsistent with basic principles of belief dynamics on pains of triviality (Section 3). This leads us to consider a set of collectively weaker principles, which we show to characterise, in our domain of interest, a family of binary combination operators for total preorders that we call TeamQueue combinators (Section 4). After recapitulating a number of existing postulates from both iterated revision and contraction, we show how these two lists of postulates can be linked via the use of any TeamQueue combinator (Section 5). Then we prove some more specific results of this type using a particular TeamQueue combinator that we call Synchronous TeamQueue (Section 6). Finally we conclude and mention some ideas for future work.

Due to space limitations, proofs or proof sketches are only provided for a small subset of the propositions stated. A version of the paper containing full proofs can be accessed online at http://arxiv.org/abs/1604.05419.

1 It should be noted that [Nayak et al., 2006] and Ramachandran et al [Ramachandran et al., 2012] do propose a principle that they call the 'New Harper Identity'. But while this may be suggestive of an attempted extension of the Harper Identity to the iterated case, the New Harper Identity simply appears to be a representation, in terms of plausibility orderings, of a particular set of postulates for iterated contraction.

2 Preliminaries

We represent the beliefs of an agent by a so-called belief state , which we treat as a primitive. determines a belief set [ ], a deductively closed set of sentences, drawn from a finitely generated propositional, truth-functional language L. The set of classical logical consequences of a sentence A 2 L is denoted by Cn(A). The set of propositional worlds is denoted by W, and the set of models of a given sentence A is denoted by [[A]].

The dynamics of belief states are modelled by two operations-contraction and revision, which respectively return the posterior belief states ⇤ A and ÷ A resulting from an adjustment of the prior belief state to accommodate, respectively, the inclusion and exclusion of A.

We assume that these operations satisfy the so-called AGM postulates [Alchourr´on et al., 1985], which enforce a principle of 'minimal mutilation' of the initial belief set in meeting the relevant exclusion or inclusion constraint. Regarding revision, we have:

Regarding contraction:

We also assume that they are linked in the one-step case by the Harper Identity (HI):

We follow a number of authors in making use of a 'semantic' representation of the 'syntactic' one-step revision and contraction dispositions associated with a particular belief state in terms of a total preorder (tpo) ⪯ over the set W of possible worlds. Intuitively ⪯ orders the worlds according to plausibility (with more plausible worlds lower down the ordering). Then the set min(⪯ ↪ [[A]]) := ¶x 2 [[A]] ♣ 8y 2 [[A]]↪ x ⪯ y♦ of minimal A-worlds corresponds to the set of worlds in which all and only the sentences in [ ⇤A] are true, with [[[ ]]] = min(⪯ ↪W) for any (see, for instance, the representation results in [Grove, 1988; Katsuno and Mendelzon, 1991]). Viewed in this way, the question of iterated belief change becomes a question about the dynamics of ⪯ under contraction and revision, with HI translating into the constraint min(⪯ ÷A↪W) =min(⪯ ↪W) [min(⪯ ⇤≻A↪W). We will denote the set of all tpos over W by T(W). The strict part of ⪯ will be denoted by ≺ and its symmetric part by ⇠ .

A tpo ⪯ can also be represented by an ordered partition hS1↪ S2↪ ▷ ▷ ▷ Smi of W, with x ⪯ y iff r(x↪⪯ )  r(y↪⪯ ), where r(x↪⪯ ) denotes the 'rank' of x with respect to ⪯ and is defined by taking Sr(x↪⪯ ) to be the cell in the partition that contains x.

3 A triviality result

What should an agent believe after performing a contraction followed by a revision? We would like to extend the Harper Identity to cover this case.

In syntactic terms, the most straightforward suggestion would be to simply extend HI to cover not just one's beliefs, but also one's commitments to retain or lose various beliefs upon subsequent revisions:

If B ⌘ > then we obtain HI as a special case. Note that under weak assumptions, EHI can equivalently be restated in terms of contraction only:

Proposition 1 EHI entails

and is equivalent to it in the presence of AGM⇤3 and the Levi Identity:

However, as G¨ardenfors' classic triviality result and its subsequent refinements [G¨ardenfors, 1986; Rott, 1989; Etlin, 2009] have taught us, the unqualified extension of principles of belief dynamics to cover conditional beliefs is a risky business. And as it turns out, the above proposal is too strong: it can be shown that, under mild constraints on single shot revision and contraction, it places unacceptable restrictions on the space of permissible belief sets resulting from single revisions:

Proposition 2 In the presence of AGM⇤5, AGM⇤6 and AGM÷3, EHI (and more specifically, HI, alongside its leftto-right half [( ÷ A) ⇤ B] ✓ [ ⇤ B] \ [( ⇤ ≻A) ⇤ B]) entails that there does not exist a belief state such that: (i) [ ] = Cn(p ^ q), (ii) [ ⇤ ≻p] = Cn(≻p ^ q) and (iii) [ ⇤ p $ ≻q] = Cn(p $ ≻q), where p and q are propositional atoms.

Proof: We first show that HI and the left-to-right half of EHI jointly entail that [( ÷A)÷B] ✓ [ ⇤≻B]. Indeed, by HI, [( ÷A)÷B] = [ ÷A]\[( ÷A)⇤≻B] ✓ [( ÷A)⇤≻B]. By the left-to-right half of EHI, we then have [( ÷A)÷B] ✓ [ ⇤ ≻B] \ [( ⇤ ≻A) ⇤ ≻B] ✓ [ ⇤ ≻B] as required.

We now establish that, in the presence of AGM⇤5, AGM⇤6 and AGM÷3, HI and the left-to-right half of EHI jointly entail the following "vacuity" principle:

Indeed, assume that A is consistent and that B 2 [ ⇤ A]. Since A is consistent, so too is [ ⇤A], byAGM⇤5, and hence ≻B ◁2 [ ⇤A]. Since, byHI, we have [ ÷≻A] = [ ]\[ ⇤A] (with help from AGM⇤6), it follows that ≻B ◁2 [ ÷ ≻A]. Given AGM÷3, we then have [( ÷≻A)÷≻B] = [ ÷≻A], and, byHI, [( ÷≻A)÷≻B] = [ ]\[ ⇤A]. By the inclusion [( ÷ ≻A) ÷ ≻B] ✓ [ ⇤ B], which we have shown above to be derivable from HI and the left-to-right half of EHI (plus AGM⇤6), it then follows that [ ] \ [ ⇤ A] ✓ [ ⇤ B], as required.

With this in place, assume VAC and, for reductio, that there exists a belief set satisfying (i) to (iii). It follows from (ii) that p $ ≻q 2 [ ⇤ ≻p]. Given the latter, it then follows from VAC that [ ] \ [ ⇤ ≻p] ✓ [ ⇤ p $≻q]. But by (i) and (ii), [ ]\[ ⇤≻p] = Cn(p^q)\Cn(≻p^q) = Cn(q). Hence, by [ ]\[ ⇤≻p] ✓ [ ⇤p $≻q], we have q 2 [ ⇤p $≻q]. But (iii) tells us that [ ⇤p $≻q] = Cn(p $≻q). Contradiction. QED. 2

The above strategy and its shortcomings can equivalently be recast in semantic terms. Let us call a function ⊕ that takes pairs of tpos as inputs and yields a tpo as an output a tpo combination operator, or a 'combinator'. For convenience, we denote ⪯1⊕⪯2 by '⪯1⊕2'.

In extending the Harper Identity to the iterated case, we are essentially looking for an appropriate combinator ⊕ such that:

Now, just as HI corresponds, given COMBI, to the following semantic principle:

EHI amounts to

What our result above effectively demonstrates is that no combinator ⊕ satisfies ⊕EHI unless we place undesirable restrictions on its domain: ⊕EHI is too much to ask for.

We will continue approaching our issue of interest from a predominantly semantic perspective for the remainder of the paper. In the following section, we retreat from ⊕EHI to offer an altogether weaker set of minimal postulates for ⊕, before taking a look at a concrete family of 'Team Queuing' combinators that satisfy them. We first establish a general characterisation of this family before showing that our set of minimal postulates suffices to characterise it in our restricted domain of interest.

2 The problem that we have just noted for EHI is closely related to the observation that an intersection of two sets of 'rational doxastic conditionals' need not itself be rational, which is familiar from the literature on default reasoning [Lehmann and Magidor, 1992].

4 Combinators: the bottom line

Since we are in the business of extending the Harper Identity, we will begin by requiring satisfaction of ⊕HI. We call combinators that satisfy this property 'basic' combinators.

In addition, even though EHI is too strong, certain weakenings of it do seem to be compelling. Specifically, it seems appropriate to require that our combination method leads to the following weak lower and upper bound principles:

We note that the former corresponds to the half of EHI that was not implicated in our earlier triviality result. Given COMBI, these will be ensured by requiring, respectively, the following upper and lower bounds on min(⪯1⊕2↪ S) for any S ✓ W (note an upper, resp. lower bound on world-sets yields a lower, resp. upper bound on belief sets):

⊕UB and ⊕LB can be repackaged using only binary comparisons:

Proposition 3 ⊕UB and ⊕LB are respectively equivalent to the following:

⊕SPU+ and ⊕WPU+ owe their names to their being respective strengthenings of the following principles of strict and weak preference unanimity, which are analogues of the 'weak Pareto' and 'Pareto weak preference' principles found in the social choice literature:

We now consider a concrete family of basic combinators that satisfy both ⊕SPU+ and ⊕WPU+, and, indeed, can be shown to be characterised by precisely these principles in our domain of interest. We call these 'TeamQueue' combinators.

The basic idea behind this family-and motivation behind the name given to it-can be grasped by means of the following analogy: A number of couples go shopping for groceries. The supermarket that they frequent is equipped with two tills. For each till, we find a sequence of various groups of people queueing to pay for their items. In order to minimise the time spent in the store, each couple operates by "team queueing": each member of the pair joins a group in a different queue and leaves their place to join their partner's group in case this group arrives at the till first. After synchronously processing their first group of customers, the tills may or may not then operate at different and variable speeds. We consider the temporal sequence of sets of couples leaving the store. In our setting, the queues are the two tpos (with lower elements towards the head of the queue) and the couples are pairs of copies of each world.

More formally, we assume, for each ordered pair h⪯1↪ ⪯2i of tpos, a sequence ha⪯1↪⪯2 (i)ii2N such that:

a⪯1↪⪯2 (i) specifies which queue is to be processed at each step. Then (a1) ensures either one or both are processed, and (a2) says both are processed at the initial stage (which will ensure ⊕HI holds for the resulting combinators). Then we construct the ordered partition hT1↪ T2↪ ▷ ▷ ▷ ↪ Tmi corresponding to ⪯1⊕2 inductively as follows:

(where 'T c ' denotes the complement of set T ) and m is minimal such that Sim Ti = W. With this in hand, we can now offer:

Definition 1 ⊕ is a TeamQueue combinator iff, for each ordered pair h⪯1↪⪯2i of tpos there exists a sequence ha⪯1↪⪯2 (i)ii2N satisfying (a1) and (a2) such that ⪯1⊕2 is obtained as above.

It is easily verified that TeamQueue combinators are indeed basic combinators. The following example provides an elementary illustration of the combinator at work:

Example 1 Suppose that W = ¶w↪ x↪ y↪ z♦, that ⪯1 is the tpo represented by the ordered partition h¶z♦↪ ¶w♦↪ ¶x↪ y♦i, and that ⪯2 is represented by h¶x↪ z♦↪ ¶y♦↪ ¶w♦i. Let ⊕ be a TeamQueue combinator such that ha⪯1↪⪯2 (i)ii2N = h¶1↪ 2♦↪ ¶2♦↪ ¶1♦↪ ▷ ▷ ▷i. Then the ordered partition corresponding to ⪯1⊕2 is hT1↪ T2↪ T3i = h¶x↪ z♦↪ ¶y♦↪ ¶w♦i, since

As noted above, TeamQueue combinators satisfy both ⊕SPU+ and ⊕WPU+. In fact, one can show that this family can actually be characterised by these two conditions, in the presence of a third:

Theorem 1 ⊕ is a TeamQueue combinator iff it is a basic combinator that satisfies ⊕SPU+, ⊕WPU+ and the following 'no overtaking' property;

Proof: (Outline of completeness part) From any basic combinator ⊕ satisfying the postulates we can construct, for each ordered pair h⪯1↪⪯2i of tpos, a sequence ha⪯1↪⪯2 (i)ii2N. Assuming ⪯1⊕2 is represented by hS1↪ ▷ ▷ ▷ ↪ Sni, we set

ha⪯1↪⪯2 (i)ii2N satisfies (a1) by property ⊕TRI below and satisfies (a2) from ⊕HI. Let ⊕0 denote the TeamQueue combinator defined by this sequence. Letting hT1↪ ▷ ▷ ▷ ↪ Tmi represent ⪯1⊕0 2, it is then a straightforward inductive proof to show Ti = Si for all i. QED

Taken together, the three postulates ⊕SPU+, ⊕WPU+ and ⊕NO say that in ⪯1⊕2, no world x is allowed to improve its position w.r.t. both input orderings ⪯1 and ⪯2. Indeed each postulate blocks one of the three possible ways in which this 'no double improvement' condition could be violated. We note that this condition can be cashed out in terms of the following remarkable property:

Proposition 4 ⊕ is a TeamQueue combinator iff it is a basic combinator that satisfies the following 'trifurcation' property, for all S ✓ W:

Given COMBI, ⊕TRI yields the claim that [( ÷A) ⇤ B] is equal to either [ ⇤B], [( ⇤≻A)⇤B] or [ ⇤B]\[( ⇤≻A)⇤B].

To wrap up this section, it should be noted that the results so far have been perfectly domain-general, in the sense that they hold for combinators whose domain corresponded to the entire space of pairs of tpos defined over W. Our problem of interest is somewhat narrower in scope, however, since we are interested in the special case in which one of the tpos is obtained from the other by means of a revision. In particular, we assume the first two semantic postulates of [Darwiche and Pearl, 1997].

In other words, ⪯1 and ⪯2 will always be [[A]]-variants for some sentence A, in the following sense:

Definition 2 Given ⪯1↪ ⪯22 T (W) and S ✓ W, we say ⪯1 and ⪯2 are S-variants iff [x ⪯1 y iff x ⪯2 y] holds for all x↪ y 2 (S⇥S)[(Sc ⇥Sc ). We let V (W) denote the set of all h⪯1↪ ⪯2i 2 T (W) ⇥ T (W) such that ⪯1↪ ⪯2 are S-variants for some S ✓ W.

Example 2 Suppose that W = ¶w↪ x↪ y↪ z♦, that ⪯1 is the tpo represented by the ordered partition h¶w♦↪ ¶x♦↪ ¶y♦↪ ¶z♦i, and that ⪯2 is represented by h¶w♦↪ ¶x↪ y♦↪ ¶z♦i. Then ⪯1 and ⪯2 are ¶y↪ z♦-variants, since (i) w ≺1 x and w ≺2 x, as well as (ii) y ≺1 z and y ≺2 z. They are not, however, ¶x↪ y♦-variants, since x ≺1 y but y ⪯2 x.

This leads to the following domain restriction on ⊕:

As it turns out, this constraint allows for a noteworthy simplification of the characterisation of TeamQueue combinators:

Proposition 5 Given ⊕DOM, ⊕ is a TeamQueue combinator iff it is a basic combinator that satisfies ⊕SPU+ and ⊕WPU+.

We also note, in passing, that

Proposition 6 Given ⊕DOM, ⊕ satisfies ⊕SPU+ and ⊕WPU+ iff it satisfies ⊕SPU and ⊕WPU, respectively.

Given Proposition 4, the potentially surprising upshot of Proposition 5 is that, in our domain of interest, satisfaction of ⊕LB and ⊕UB entails satisfaction of ⊕TRI.

5 Iterated Contraction via TeamQueue Combination

A central result of AGM theory says that, under assumption of HI, if ⇤ satisfies the AGM revision postulates, then ÷ automatically satisfies the AGM contraction postulates. In this section we look at some of the postulates for both iterated revision and contraction that have been proposed in the literature. We show that, if ⪯ ÷A is defined from⪯ and ⪯ ⇤≻A using COMBI via a TeamQueue combinator, then satisfaction of some well known sets of postulates for iterated revision leads to satisfaction of other well known sets of postulates for iterated contraction.

The most widely cited postulates for iterated revision are the four DP postulates of [Darwiche and Pearl, 1997]. These, like most of the postulates for iterated belief change, come in two flavours: a semantic one in terms of requirements on the tpo⪯ ⇤A associated to the revised state ⇤A, and a syntactic one in terms of requirements on the belief set [( ⇤ A) ⇤ B] following a sequence of two revisions. Turning first to the semantic versions, we've already encountered the first two of these postulates-CR⇤1 and CR⇤2-in the previous section. The other two are

Each of these has an equivalent corresponding syntactic version as follows:

Chopra et al [2008] proposed a list of 'counterparts' to the DP postulates for the case of ÷A. The semantic versions of these were:

Chopra et al [2008] showed (their Theorem 2) that, in the presence of the AGM postulates (reformulated as in our setting to apply to belief states rather than just belief sets) each of these postulates has an equivalent syntactic version as follows:

As it turns out, the definition of ⪯ ÷A from ⪯ and ⪯ ⇤≻A using COMBI via a TeamQueue combinator allows us to show the precise sense in which Chopra et al's postulates are 'Darwiche-Pearl-like', as they put it:

Proposition 7 Let ⊕ be a TeamQueue combinator, let ⇤ be an AGM revision operator and let ÷ be such that ⪯ ÷A

is defined from ⇤ via COMBI using ⊕. Then, for each i = 1↪ 2↪ 3↪ 4, if ⇤ satisfies CR⇤i then ÷ satisfies CR÷i.

As a corollary, given the AGM postulates, we recover the same result for the syntactic versions as well.

Finally, Nayak et al [2007] have endorsed the following principle of 'Principled Factored Intersection', which they show to be satisfied by a number of proposals for iterated contraction:

The rationale for PFI remains rather unclear to date. Indeed, the only justifications provided appear to be (a) that PFI avoids a particular difficulty faced by another constraint that has been proposed in the literature-namely Rott's 'Qualified Intersection' principle [Rott, 2001]-and which can be reformulated in a manner that is superficially rather similar to PFI and (b) that PFI entails a pair of prima facie appealing principles. Neither of these considerations strike us as being particularly compelling. For one, Rott's Qualified Intersection principle remains itself unclearly motivated. Secondly, plenty of ill-advised principles can be shown to have certain plausible consequences.

The TeamQueue approach, however, allows us to rest the principle on a far firmer foundation. Indeed:

Proposition 8 Let ⊕ be a TeamQueue combinator, let ⇤ be an AGM revision operator and let ÷ be such that ⪯ ÷A is defined from ⇤ via COMBI using ⊕. If ⇤ satisfies CR⇤1 and CR⇤2 then ÷ satisfies PFI.

6 The Synchronous TeamQueue Combinator

A special case of TeamQueue combinators takes a⪯1↪⪯2 (i) = ¶1↪ 2♦ for all ordered pairs h⪯1↪ ⪯2i and all i. This represents a particularly fair way of combining tpos. In terms of our supermarket analogy, it corresponds to the situation in which the tills process groups of customers at the same speed.

Definition 3 The Synchronous TeamQueue (STQ) combinator is the TeamQueue combinator for which a⪯1↪⪯2 (i) = ¶1↪ 2♦ for all ordered pairs h⪯1↪⪯2i and all i. We will denote the STQ combinator by ⊕STQ.

Example 3 Suppose W = ¶x↪ y↪ z↪w♦, that ⪯1 is the tpo represented by the ordered partition h¶z♦↪ ¶w♦↪ ¶x↪ y♦i and ⪯2 is represented by h¶x↪ z♦↪ ¶y♦↪ ¶w♦i. Then the ordered partition corresponding to ⪯1⊕STQ2 is hT1↪ T2i = h¶x↪ z♦↪ ¶w↪ y♦i.

Roughly, ⪯1⊕STQ2 tries to make each world as low in the ordering as possible, while trying to preserve the information contained in ⪯1 and ⪯2. (The idea is similar to that of the rational closure construction in default reasoning [Lehmann and Magidor, 1992].) We remark that ⊕STQ is commutative, i.e., ⪯1⊕2=⪯2⊕1. It can be characterised semantically, in the absence of domain restrictions, as follows:

Theorem 2 ⊕STQ is the only basic combinator that satisfies both ⊕SPU+ and the following 'Parity' constraint:

Note that ⊕WPU+ is not listed among the characteristic principles: it is entailed by the conjunction of ⊕SPU+ and ⊕PAR.

Whilst ⊕PAR may not be immediately easy to grasp, it can be given a nice formulation in our setting in terms of the notion of strong belief [Battigalli and Siniscalchi, 2002; Stalnaker, 1996]. A sentence A 2 [ ] is strongly believed in in case the only way it can be dislodged by the next revision input B is if B is logically inconsistent with A. That is, A is strongly believed in iff (i) A 2 [ ], and (ii) A 2 [ ⇤B] for all sentences B such that A^B is consistent. Semantically, a consistent sentence A is strongly believed in iff every A-world is strictly more plausible than every ≻A-world, i.e., x ≺ y for every x 2 [[A]], y 2 [[≻A]]. With this in hand, one can show:

Proposition 9 ⊕PAR is equivalent to:

Given COMBI, ⊕SB yields: If ≻B is strongly believed in ÷ A then [( ÷ A) ⇤ B] ✓ [ ⇤ B] \ [( ⇤ ≻A) ⇤ B]. Thus, although we cannot have EHI for all A↪B, the STQ combinator does guarantee it to hold for a certain restricted class of pairs of sentences, namely those A↪B such that ≻B is strongly believed after removing A.

To finish this section, we turn to further behaviour for iterated contraction that can be captured thanks to the further principles satisfied by ⊕STQ.

This raises an obvious question, namely: Which principles of iterated contraction does one recover from the natural, restrained and lexicographic revision operators, respectively, if one defines ÷ from ⇤ using ⊕STQ? As it turns out, both the natural and the restrained revision operator yield the very same iterated contraction operator, which has been discussed in the literature under the name of 'natural contraction' [Nayak et al., 2007], and which sets min(⪯ ↪ [[≻A]])[ min(⪯ ↪W) to be the lowest rank in ⪯ ÷A while leaving ⪯ ÷A otherwise unchanged from⪯ .

Three popular approaches to supplementing the AGM postulates for revision and the DP postulates can be found in the literature: the 'natural' [Boutilier, 1996], 'restrained' [Booth and Meyer, 2006], and 'lexicographic' [Nayak, 1994] approaches. All of these have the semantic consequence that the prior tpo ⪯ determines the posterior tpo ⪯ ⇤A. All three promote the lowest A-worlds in ⪯ to become the lowest overall in ⪯ ⇤A, but differ on what to do with the rest of the ordering. Natural revision leaves everything else unchanged, restrained revision preserves the strict ordering ≺ while additionally making every A-world x strictly lower than every ≻A-world y for which x ⪯ y, and lexicographic revision just makes every A-world lower than every ≻A-world, while preserving the ordering within each of [[A]] and [[≻A]].

Proposition 10 Let ⇤ be any revision operator-such as the natural or restrained revision operator-satisfying the following property:

Let ÷ be the contraction operator defined from ⇤ via COMBI using ⊕STQ. Then ÷ is the natural contraction operator.

We do not have a characterisation of the operator that is recovered from lexicographic revision in this manner, which we call the STQ-lex contraction operator. That is, STQ-lex contraction sets ⪯ ÷A=⪯ ⊕STQ ⪯ ⇤L≻A, where ⇤L is lexicographic revision. We can report, however, that it is distinct from both lexicographic and priority contraction, the other two iterated contraction operators discussed in the literature alongside natural contraction [Nayak et al., 2007]. Roughly, lexicographic contraction works by setting the ith rank Si of ⪯ ÷A to be the union of the ith -lowest A-worlds with the ith -lowest ≻A-worlds.

Example 4 Suppose W = ¶x↪ y↪ z↪w♦ and ⪯ is the tpo represented by h¶x♦↪ ¶y♦↪ ¶z♦↪ ¶w♦i. Let [[A]] = ¶x↪w♦, so that ⪯ ⇤L≻A= h¶y♦↪ ¶z♦↪ ¶x♦↪ ¶w♦i. Then lexicographic contraction yields ⪯ ÷A= h¶x↪ y♦↪ ¶z↪w♦i while STQ-lex contraction yields ⪯ ÷A= h¶x↪ y♦↪ ¶z♦↪ ¶w♦i.

Both lexicographic and priority contraction can, however, still be recovered via the TeamQueue approach. Lexicographic contraction can be recovered from lexicographic revision by combining, not ⪯ and ⪯ ⇤L≻A, but rather ⪯ ⇤LA and ⪯ ⇤L≻A using ⊕STQ. Priority contraction can be recovered from lexicographic revision by combining ⪯ and ⪯ ⇤≻A using a TeamQueue combinator. However, the combinator involved is not ⊕STQ but rather the TeamQueue combinator that is most 'biased' towards ⪯2: the combinator for which, for all ordered pairs h⪯1↪⪯2i, a⪯1↪⪯2 (1) = ¶1↪ 2♦, then a⪯1↪⪯2 (j) = ¶2♦ for all j > 1.

7 Conclusions

We have shown that the issue of extending the Harper identity to iterated belief change (a) is not a straightforward affair but (b) can be fruitfully approached by combining a pair of total preorders by means of TeamQueue combinator. We have also noted that one particular such combinator, the Synchronic TeamQueue combinator ⊕STQ can be put to work to derive various counterparts for contraction of the three best known iterated revision operators.

Whilst the normative appeal of the characteristic syntactic properties ⊕LB and ⊕UB of the TeamQueue family of combinators is clear enough, we do not, at this stage, have a clear enough grasp of the normative appeal of the further syntactic requirement ⊕SB that characterises ⊕STQ. We plan to investigate this issue further in future work.

A second issue that we would like to explore is the question of whether or not it is possible to show that the DarwichePearl postulates are equivalent to the ones proposed by Chopra et al, given a suitable further bridge principle taking us from iterated contraction to iterated revision. Such a task would first involve providing a compelling generalisation of the Levi Identity mentioned in Proposition 1 above.