(Grove, 1988)

This paper proposes a model-theoretic characterization of the belief revision ($\ast$) operation discussed by AGM. Grove’s idea is to give a “spheres semantics” inspired by (Lewis, 1973a) for $\ast$, thus enriching the purely syntactic approach by AGM.

Grove’s sets the stage without taking a stance on some (trivial) background assumptions, so I will fill in the gaps.

Let $F$ be the set of well-formed sentences in a Boolean language, and $L\subseteq F$ be the set of “logical theses of some logic”, i.e. let $L$ be the set of propositional tautologies and to be closed under modus ponens. Define:

1. A theory $T\in \mathcal{T}$ is a subset of $F$ that is closed under modus ponens, i.e. $Cn(T)=T$.
2. A set of formulas $S$ is consistent, $Con(S)$, iff $Con(S)\ne F$.
3. The revision function $+:\mathcal{T}\times F\to \mathcal{T}$ satisfies the following axioms: for any $T\in \mathcal{T}$ and $A\in F$,
   • (+1) $T+A=Cn(T+A)$ [this holds trivially],
   • (+2) $A\in T+A$,
   • (+3) $T+A=Cn(T\cup \{A\})$, if $\neg A\notin T$,
   • (+4) $Cn(T+A)\ne F$, if $\neg A\notin L$,
   • (+5) $T+A=T+B$, if $A\leftrightarrow B\in L$,
   • (+7) $T+(A\wedge B)\subseteq Cn((T+A)\cup \{B\})$,
   • (+8) $Cn((T+A)\cup \{B\})\subseteq T+(A\wedge B)$, if $\neg B\notin T+A$.

There are two objects that deserve extensive discussion: maximal consistent extensions of $L$, and the function $t$.

1. Maximal Consistent Extensions of $L$

Grove does not take the notion of possible world as primitive, but he starts from syntactic objects (sentences) and then constructs other objects (maximal consistent sets of sentences) that are basically equivalent to possible worlds.

The set $M_L$ is the set of maximal consistent extensions of $L$, and it consists of sets $m\subseteq F$ such that:

Maximal Consistent Extensions of the Logic $L$

Let $L\subseteq F$ be a logic, where $F$ is the set of all well-formed formulae. Then, define $M_L$ as the set of consistent maximal extensions of the logic $L$, that is

$$m\in M_L⟺\{\begin{array}{ll}1.L\subseteq m& \\ 2.Cn(m)\ne F& (\text{Consistency})\\ 3.\forall n\subseteq F,\text{ if }m\subset n,\text{ then }Cn(n)=F& (\text{Maximality})\end{array}$$

Note that, for any $m\in M_L$, $m$ is a theory.

Proposition

For any $m\in M_L$, $m$ is a theory.

bproof Consider $m\in M_L$ and suppose for reductio that $m\ne Cn(m)$. Since $m\subseteq Cn(m)$ by the Reflexivity of $Cn$, $m\ne Cn(m)$ implies that there is $x\in Cn(m)$ such that $x\notin m$. Set $n:=Cn(m)$. Clearly, we have $n\in \mathcal{T}$ and $m\subset n$. Since $m\in M_L$, $m$ must be maximal, and hence $n=Cn(m)=F$, contradicting the consistency of $m$. Therefore, $m=Cn(m)$. eproof

The following propositions clarifies why $m$ is a possible world. First, let me establish that $M_L$ could have been defined in a different, equivalent way.

Proposition

Let $m\subseteq F$.

$$m\in M_L⟺\{\begin{array}{ll}1.L\subseteq m& \\ 2.Cn(m)\ne F& \text{(Consistency})\\ 3.\text{ For all A∈F: either A∈m or ¬A∈m.}& (\text{Completeness})\end{array}$$

bproof ($⟹$) Take arbitrary $m\in M_L$ and $A\in F$. Obviously, (1) and (2) hold. So, let me prove that (3) holds as well. We have two cases: either $A\in m$ or $A\notin m$.

1. If $A\in m$ we are done.
2. Suppose that $A\notin m$. Consider now $n:=Cn(m\cup \{A\})$. Since $m\subseteq m\cup \{A\}$, by Monotonicity $Cn(m)\subseteq Cn(m\cup \{A\})$, and by Reflexivity $m\subseteq Cn(m)\subseteq Cn(m\cup \{A\})=n$. Since $A\in n$ but $A\notin m$, $m\subset n$. By the maximality of $m$, since $m\subset n$, it must be the case that $n=Cn(m\cup \{A\})=F$. Therefore, $m\cup \{A\}$ must be inconsistent, meaning $m\cup \{A\}⊢\perp$. By the deduction theorem for classical logic, we have that $m⊢A\to \perp$. Since $A\to \perp$ is classically equivalent to $\neg A$, we have that $m⊢\neg A$. Since $m$ is a theory (i.e., $m=Cn(m)$), it follows that $\neg A\in m$.

Therefore, either $A\in m$ or $\neg A\in m$.

($⟸$) Suppose that, $L\subseteq m$, $Cn(m)\ne F$, and that for all $A\in F$, either $A\in m$ or $\neg A\in m$. We need to prove that $m$ is a theory and that it is maximal.

1. Let me first prove that $m$ is a theory. We need to prove that $m=Cn(m)$. ($\subseteq$) Obviously $m\subseteq Cn(m)$. ($\supseteq$) Let us show that, if $A\in Cn(m)$, then $A\in m$. Suppose for reductio that $A\in Cn(m)$ and $A\notin m$. By the completeness of $m$, $\neg A\in m$. Since $m\subseteq Cn(m)$, $\neg A\in Cn(m)$. Since $A,\neg A\in Cn(m)$, $Cn(m)=F$, contradicting the consistency of $m$. Therefore, $A\in m$. Since $A$ is arbitrary, we have $Cn(m)\subseteq m$, proving that $m$ is a theory, i.e. $m=Cn(m)$.
2. Let me now prove that $m$ is maximal. Suppose that and $m\subset n$, namely $m\subseteq n$ and there exists some $A\in n$ such that $A\notin m$. By the completeness of $m$, $\neg A\in m$. Since $m\subset n$, both $A$ and $\neg A$ are in $n$. Hence, $Cn(n)=F$. Therefore, $m$ is maximal.

Therefore, if $m$ has (1)-(3) it must be maximal, and so $m\in M_L$. eproof

Proposition

For any $m\in M_L$, there exists exactly one possible world $w\in W$ such that $w\models m$.

bproof First, recall that a possible world $w$ is basically a function (a valuation) from the set of propositional variables $\Phi \subseteq F$ that maps each $p_i\in \Phi$ to either $0$ (false) or $1$ (true). The satisfaction relation $w\models A$ for any complex formula $A\in F$ is defined recursively from this basis.

Consider now any $m\in M_L$.

Part 1: Existence. We must first construct a world $w_m$ from $m$ and show that it satisfies $m$.

First, let us construct the world $w_m$. We define a valuation $w_m:\Phi \to \{0,1\}$ based on the contents of $m$. For any propositional variable $p\in \Phi$:

• If $p\in m$, we define $w_m(p)=1$.
• If $p\notin m$, we define $w_m(p)=0$. Note that, from ^03a961, we know that if $p\notin m$, then $\neg p\in m$. So this definition is complete.

Second, let us show that $w_m\models m$: We must show that this $w_m$ satisfies every formula in $m$. We can prove by induction on the structure of any formula $A\in F$ that $A\in m⟺w_m\models A$.

• Base Case (Atoms): For any $p\in \Phi$, $p\in m⟺w_m(p)=1⟺w_m\models p$. This holds by our definition of $w_m$.
• Inductive Step (Negation): Assume $B\in m⟺w_m\models B$. We show $\neg B\in m⟺w_m\models \neg B$.
  • $w_m\models \neg B⟺w_m/\models B$ (by definition of $\models$)
  • $⟺B\notin m$ (by inductive hypothesis)
  • $⟺\neg B\in m$ (by ^03a961).
• Inductive Step (Conjunction): Assume $B\in m⟺w_m\models B$ and $C\in m⟺w_m\models C$.
  • $w_m\models B\wedge C⟺w_m\models B$ and $w_m\models C$ (by definition of $\models$).
  • $⟺B\in m$ and $C\in m$ (by inductive hypothesis)
  • $⟺(B\wedge C)\in m$ (since $m$ is a theory, it’s closed under conjunction)

(This holds for all other connectives as well.) Since $A\in m⟺w_m\models A$ holds for all $A\in F$, it follows that $m$ satisfies all and only the formulas $A$ in $m$. Therefore, $w_m\models m$. This proves at least one such world exists.

Part 2: Uniqueness. We must now show that $w_m$ is the only such world. Assume there is another world $w^{\prime }\in W$ (a different valuation) such that $w^{\prime }\models m$. To show $w^{\prime }=w_m$, we only need to show that they agree on all propositional variables, i.e., $w^{\prime }(p)=w_m(p)$ for all $p\in \Phi$. Let $p$ be an arbitrary propositional variable in $\Phi$.

• Case 1: $p\in m$.
  • By our construction, $w_m(p)=1$.
  • Since $w^{\prime }\models m$ and $p\in m$, it must be that $w^{\prime }\models p$.
  • By definition of $\models$, this means $w^{\prime }(p)=1$.
  • Thus, $w^{\prime }(p)=w_m(p)$.
• Case 2: $p\notin m$.
  • By our construction, $w_m(p)=0$.
  • Since $m$ is maximal and $p\notin m$, we know by ^03a961 $\neg p\in m$.
  • Since $w^{\prime }\models m$ and $\neg p\in m$, it must be that $w^{\prime }\models \neg p$.
  • By definition of $\models$, this means $w^{\prime }(p)=0$.
  • Thus, $w^{\prime }(p)=w_m(p)$.

Since $w^{\prime }$ and $w_m$ agree on all propositional variables, they are the same valuation, i.e., $w^{\prime }=w_m$. Therefore, for any $m\in M_L$, there exists one and only one world $w$ that satisfies it. eproof

In other words, there exists a function $f:M_L\to W$ such that $f(m)=w_m$ such that $w\models m$. This function is also a bijection.

Proposition

For all $w\in W$ there exists a unique $m\in M_L$ such that $w\models m$.

bproof Consider an arbitrary $w\in W$.

Part 1: Existence. Construct the set $m_w$ as follows

$$m_w:=\{A\in F:w\models A\}$$

Clearly, it follows that $w\models m_w$ by construction—i.e., $w\models A$ for all $A\in m_w$. Second, let me prove that $m_w$ is in $M_L$.

1. $m_w$ is a theory. Obviously $m_w\subseteq Cn(m_w)$, so consider an arbitrary $A\in Cn(m_w)$ and let me show that $A\in m_w$. Since $m_w⊢A$, by the Soundness of classical propositional logic, $m_w\models A$. Since $w\models m_w$, $w\models A$. Therefore, by the definition of $m_w$, $A\in m_w$. Since $Cn(m_w)\subseteq m_w$, we have that $m_w$ is a theory.
2. $m_w$ is an extension of $L$. For all $B\in L$, we have that $B$ is satisfied by any world in $W$. So, $w\models B$ for all $B\in L$. Hence, $L\subseteq m_w$ for by construction.
3. $m_w$ is consistent. Suppose for reductio that $m_w$ is inconsistent, i.e. $Cn(m_w)=m_w=F$ (for $m_w$ is a theory). Then, we have that $w\models F$, and hence $w\models \perp$, contradicting $w⊭\perp$. Hence, $m_w$ is consistent.
4. $m_w$ is maximal. Suppose $m_w\subset n$ for some $n\subseteq F$. There must be some $A\in F$ such that $A\in n$ and $A\notin m_w$. Since $A\notin m_w$, it follows that $w⊭A$, and hence by the definition of $\models$, $w\models \neg A$. By the construction of $m_w$, $\neg A\in m_w$. Since $m_w\subset n$, $\neg A\in n$. Since $\neg A,A\in n$, $Cn(n)=F$. Therefore, $m_w$ is maximal.

Concluding, for any $w\in W$ there exists a set of formulas $m_w$ such that $w\models m_w$ and $m_w$ is a maximal consistent extension of $L$ (i.e., $m\in M_L$).

Part 2: Uniqueness. Suppose $w\models m$ and $w\models m^{\prime }$ with $m,m^{\prime }\in M_L$. Suppose (without loss of generality) that there exists some $A$ such that $A\in m$ and $A\notin m^{\prime }$ ($m\ne m^{\prime }$). By ^03a961, since $A\notin m^{\prime }$, $\neg A\in m^{\prime }$. Therefore, since $w\models m$ and $w\models m^{\prime }$, we have $w\models A$ and $w\models \neg A$. By the definition of $\models$, it follows that $w\models A$ and $w⊭A$: contradiction. Therefore, $m=m^{\prime }$. eproof

Before moving on, consider the following definition.

Def

Let $T\in \mathcal{T}$ be a theory. Define

$$\left|T\right|:=\{m\in M_L:T\subseteq m\}.$$

In a way, $\left|T\right|$ is the set of possible worlds that make $T$ true.

2. Properties of $t$

Define the following operation $t$.

$t$

Let $S\subseteq M_L$. Define the function $t:\mathcal{P}(M_L)\to \mathcal{P}(F)$ such that:

$$t(S)=\bigcap S.$$

Note that, if $S=\varnothing$, then $t(S)=F$. For $\bigcap S=\{x\in F:\text{ For all }R\in S(x\in R)\}$, but if $S=\varnothing$ the condition—i.e. $\text{For all }R\in S(x\in R)\}$—is (trivially) satisfied by any $x\in F$.

Properties of $t$

Let $S\subseteq M_L$.

1. $t(S)$ is a theory.
2. $t(|T|)=T$ (for all theories $T$, assuming compactness).
3. $t(S)$ is consistent if and only if $S\ne \varnothing$.
4. $t(S\cap |A|)=Cn(t(S)\cup \{A\})$.
5. If $S\subseteq S^{\prime }$, then $t(S^{\prime })\subseteq t(S)$.
6. If $T\subseteq T^{\prime }$, then $|T^{\prime }|\subseteq |T|$.

Let $S\subseteq M_L$ be a collection of maximal and consistent extensions of $L$.

(1) $t(S)$ is a theory. ($\subseteq$) Obviously, $t(S)\subseteq Cn(t(S))$ by the Reflexivity of $Cn$. ($\supseteq$) Let us show the other direction. Consider an arbitrary $x\in Cn(t(S))$. Recall that $t(S)=\bigcap S$.

1. Since $t(S)\subseteq m$ for every $m\in S$, by the Monotonicity of $Cn$, we have $Cn(t(S))\subseteq Cn(m)$ for every $m\in S$.
2. Since every $m\in M_L$ is a theory (maximal consistent sets are closed), $Cn(m)=m$.
3. Therefore, $Cn(t(S))\subseteq m$ for every $m\in S$.
4. Consequently, $x\in m$ for all $m\in S$.
5. Thus, $x\in \bigcap S=t(S)$.

(2) $t(\left|T\right|)=T$, if $T$ is a theory and we have compactness. By definition, $\left|T\right|=\{m\in M_L:T\subseteq m\}$ and so $t(\left|T\right|)=\bigcap \left|T\right|=\bigcap \{m\in M_L:T\subseteq m\}$. Clearly, if $T$ is inconsistent (i.e., $T=Cn(T)=F$), it follows that there is no $m$ such that $T\subseteq m$ (if $T\subseteq m$, $m=F$ and hence $Cn(m)=F$, contradicting the consistency of $m$). Hence, $\left|T\right|=\varnothing$, so $t(\left|T\right|)=F$ and $T=F$ ex hypothesi, proving our equality. So, suppose that $T$ is consistent.

($\supseteq$) Suppose $A\in T$. Since $T\subseteq m$ for all $m\in \left|T\right|$, $A\in m$ for all such $m$. Therefore $A\in \bigcap \left|T\right|=t(\left|T\right|)$.

($\subseteq$) Suppose $A\in t(\left|T\right|)$. Thus, $A\in m$ for all $m\in M_L$ such that $T\subseteq m$. Suppose for reductio that $A\notin T=Cn(T)$, for $T$ is a theory. Since $T$ is consistent ex hypothesi and $A\notin Cn(T)$, it follows that $T^{\prime }:=Cn(T\cup \{\neg A\})\ne F$—if $Cn(T\cup \{\neg A\})=F$, it follows that $T⊢\neg A\to \perp$, i.e. $T⊢A$, and so $A\in T$. Now, to prove a contradiction, we need to show that there exists a set $m$ such that $T\subseteq T^{\prime }\subseteq m$ and such that $m$ is a maximal consistent extension of $L$ (which implies $m\in |T|$ yet $A\notin m$). To do so, we need both Compactness and Zorn’s Lemma.

1. First, define the collection of sets $\mathcal{K}:=\{X\subseteq F:Cn(X)\ne F\text{ and }{T}^{\prime }\subseteq X\}$. Clearly, $(\mathcal{K},\subseteq )$ is a poset. Consider now an arbitrary chain $\mathcal{C}\subseteq \mathcal{K}$, and let us show that $\mathcal{C}$ has an upper bound in $\mathcal{K}$. Define $R:={\bigcup }_{X\in \mathcal{C}}X$. Clearly, $X\subseteq R$ for all $X\in \mathcal{C}$. We need to prove that $R\in \mathcal{K}$, i.e. that $T^{\prime }\subseteq R$ and $Cn(R)\ne F$. Since $T^{\prime }\subseteq X$ for all $X\in \mathcal{C}$, and $X\subseteq R$, it follows that $T^{\prime }\subseteq R$. Suppose now for reductio that $Cn(R)=F$. By Compactness, there must be a finite subset $R_0\subseteq R$ such that $Cn(R_0)=F$. Since $R_0\subseteq R={\bigcup }_{X\in \mathcal{C}}X$ is finite and $\mathcal{C}$ is a chain, there must be a set $X^{\ast }\in \mathcal{C}$ such that $R_0\subseteq X^{\ast }$. By the Monotonicity of $Cn$, $Cn(R_0)\subseteq Cn(X^{\ast })$, and so $Cn(X^{\ast })=F$, contradicting the fact that $X^{\ast }\in \mathcal{K}$. Therefore, $Cn(R)\ne F$, and so $R\in \mathcal{K}$. Therefore, $\mathcal{C}$ has an upper bound in $\mathcal{K}$. Since $\mathcal{C}$ is an arbitrary chain in $\mathcal{K}$, we conclude that any such chain has an upper bound in $\mathcal{K}$.
2. By Zorn’s Lemma, it follows that $\mathcal{K}$ has at least one maximal element: let us call it $m$. By definition of $\mathcal{K}$, $Cn(m)\ne F$ and $T^{\prime }\subseteq m$. We must show that $m$ is in $M_L$. We have already established that $m$ is consistent. Note then that, since $T^{\prime }:=Cn(T\cup \{\neg A\})$, $L\subseteq T^{\prime }\subseteq m$, hence $m$ is an extension of $L$. Ultimately, note that $m$ is maximal. If $m\subset n$, for some $n\subseteq F$, it must be the case that $Cn(n)=F$—if $Cn(n)\ne F$, then (since $T^{\prime }\subseteq m\subset n$), $n\in \mathcal{K}$, contradicting the maximality of $m\in \mathcal{K}$. Thus, $m\in M_L$. Moreover, we have that $T\subseteq m$, for $T\subseteq T\cup \{\neg A\}\subseteq Cn(T\cup \{\neg A\})\subseteq m$Therefore, $m\in \left|T\right|$. However, $\neg A\in T^{\prime }\subseteq m$. Since $m$ is consistent, $A\notin m$. This contradicts the hypothesis that $A\in t(\left|T\right|)$ (which requires $A$ to be in every $m\in \left|T\right|$). Therefore, we conclude that $A\in T$.
3. Since $A$ is an arbitrary formula in $t(\left|T\right|)$, we have that $t(\left|T\right|)\subseteq T$.

We conclude that $t(\left|T\right|)=T$.

(3) $t(S)$ is consistent iff $S$ is nonempty. ($⟹$) If $S=\varnothing$, by definition we have that $t(S)=F$, and hence $Cn(t(S))=F$. $(⟸)$ Suppose that $t(S)$ is inconsistent, meaning that $Cn(t(S))=F$. Since $t(S)=\bigcap S$, where $S\subseteq M_L$, it clearly follows that $t(S)\subseteq m$ for all $m\in S$. If there is at least one $m\in S$, by the monotonicity of $Cn$, $Cn(t(S))\subseteq Cn(m)$, implying that $Cn(m)=F$. However, this contradicts the consistency of $m$, thus there exists no $m\in S$, meaning $S=\varnothing$.

(4) $t(S\cap |A|)=Cn(t(S)\cup \{A\})$. We distinguish three cases based on the status of the set $S$.

Case 1: $S=\varnothing$. In this case, the intersection $S\cap |A|=\varnothing$. By definition, $t(\varnothing )=F$ (the inconsistent theory).

• LHS: $t(\varnothing )=F$.
• RHS: $Cn(t(\varnothing )\cup \{A\})=Cn(F\cup \{A\})=F$. The equality holds trivially.

Case 2: $S\ne \varnothing$, but $S\cap |A|=\varnothing$. In this case, the intersection is empty, so the LHS is $t(\varnothing )=F$. For the RHS, note that since $S\cap |A|=\varnothing$, it follows that for all $m\in S$, $m\notin |A|$, i.e., $A\notin m$. Since every $m\in M_L$ is complete, $\neg A\in m$ for all $m\in S$. Consequently, $\neg A\in \bigcap S=t(S)$. Therefore, the set $t(S)\cup \{A\}$ contains both $\neg A$ and $A$, making it inconsistent. Thus $Cn(t(S)\cup \{A\})=F$. The equality holds.

Case 3: $S\cap |A|\ne \varnothing$. This is the principal case. Let us prove the equality by mutual inclusion.

($\subseteq$) Let $x\in t(S\cap |A|)$.

1. We prove that $A\to x\in t(S)$. Suppose for reductio that $A\to x\notin t(S)$. Since $t(S)=\bigcap S$, there must exist some $m\in S$ such that $A\to x\notin m$.
2. Since $m$ is complete, $\neg (A\to x)\in m$. This is classically equivalent to $A\wedge \neg x\in m$, which implies $A\in m$ and $\neg x\in m$.
3. Since $m\in S$ and $A\in m$, it follows that $m\in S\cap |A|$.
4. However, by our initial hypothesis, $x\in t(S\cap |A|)$, which implies $x\in m^{\prime }$ for all $m^{\prime }\in S\cap |A|$. Therefore, $x\in m$. We now have $x\in m$ and $\neg x\in m$, contradicting the consistency of $m$.
5. Therefore, the assumption was false, and $A\to x\in t(S)$. By Modus Ponens, $Cn(t(S)\cup \{A\})$ contains $x$.

($\supseteq$) Let $x\in Cn(t(S)\cup \{A\})$.

1. By the deduction theorem (or definition of consequence), $t(S)\cup \{A\}⊢x$, which implies $t(S)⊢A\to x$.
2. Since $t(S)$ is a theory, $(A\to x)\in t(S)$. By definition of $t(S)$, for all $m\in S$, $(A\to x)\in m$.
3. Consider now any $m\in S\cap |A|$. For such $m$, we have $m\in S$ and $A\in m$.
4. Since $(A\to x)\in m$ and $A\in m$, it follows by closure of $m$ that $x\in m$.
5. Since $x$ is in every $m\in S\cap |A|$, $x\in t(S\cap |A|)$.

(5) For $S,S^{\prime }\subseteq M_L$, if $S\subseteq S^{\prime }$, then $t(S^{\prime })\subseteq t(S)$. Let $S,S^{\prime }\subseteq M_L$ and suppose $S\subseteq S^{\prime }$. By definition, $t(S^{\prime })=\bigcap S^{\prime }$, which is the set of all formulae $A$ such that $A\in m$ for all $m\in S^{\prime }$. Consider any $A\in t(S^{\prime })$. By definition, $A$ is contained in every world in $S^{\prime }$. Since $S\subseteq S^{\prime }$, every world $m\in S$ is also a world in $S^{\prime }$. Therefore, $A$ must be contained in every world $m\in S$. Consequently, $A\in \bigcap S=t(S)$. Since $A$ was arbitrary, $t(S^{\prime })\subseteq t(S)$. This relates to the general set-theoretic property that $X\subseteq Y⟹\bigcap Y\subseteq \bigcap X$ (Reverse-Inclusion Property).

(6) For $T,T^{\prime }\in \mathcal{T}$, if $T\subseteq T^{\prime }$ then $\left|T^{\prime }\right|\subseteq \left|T\right|$. Let $T,T^{\prime }\in \mathcal{T}$ and suppose $T\subseteq T^{\prime }$. Consider any $m^{\prime }\in \left|T^{\prime }\right|$, that is any $m^{\prime }$ such that $T^{\prime }\subseteq m^{\prime }$. Clearly, $T\subseteq T^{\prime }\subseteq m^{\prime }$, hence $T\subseteq m^{\prime }$, so $m^{\prime }\in \left|T\right|$. So, $\left|T^{\prime }\right|\subseteq \left|T\right|$.

The proof is complete. eproof

3. Systems of Spheres

Systems of Spheres

Let $\mathbf{S}$ be a collection of subsets of $M_L$, i.e. $\mathbf{S}\subseteq \mathcal{P}(M_L)$. $\mathbf{S}$ is a system of spheres centered on $X$ (${\mathbf{S}}_X$) for some subset $X\subseteq M_L$, if it satisfies the following conditions:

• (S1: Nestedness) $\mathbf{S}$ is totally ordered by $\subseteq$: if $U,V\in \mathbf{S}$, then $U\subseteq V$ or $V\subseteq U$.
• (S2: Centering) $X$ is the $\subseteq$-minimum of $\mathbf{S}$: $X\in S$ and, for all $U\in \mathbf{S}$, $X\subseteq U$.
• (S3: ?) $M_L\in \mathbf{S}$.
• (S4: Limit Assumption) If $A\in F$ and $U\cap \left|A\right|\ne \varnothing$ for some $U\in \mathbf{S}$, then there exists a sphere $U^{\ast }\in \mathbf{S}$ such that: (1) $U^{\ast }\cap \left|A\right|\ne \varnothing$, and (2) $V\cap \left|A\right|\ne \varnothing$ implies $U\subseteq V$ for all $V\in \mathbf{S}$.

The main differences between ^0e19fa and ^93cc74 are the following:

1. Grove’s systems of spheres are not required to be closed under nonempty intersections and finite unions.
2. More significantly, Grove’s systems of spheres are not centered on single worlds, but on sets of “worlds”.

We have that, for any $A\in F$,

1. If $\left|A\right|\cap \bigcup \mathbf{S}\ne \varnothing$, then S4 ensures that there exists some sphere in $\mathbf{S}$, call it $c(A)$, which intersects $\left|A\right|$ and is smaller than any other sphere with this property.
2. If $\left|A\right|\cap \bigcup \mathbf{S}=\varnothing$, then S3 implies that $\left|A\right|=\varnothing$, and we take $c(A):=M_L$.

Thus, given a sphere system $\mathbf{S}$, we can define a function $f_{\mathbf{S}}:F\to \mathcal{P}(M_L)$ such that

$$f_{\mathbf{S}}(A):=\left|A\right|\cap c(A)$$

(N.b. recall that $c(A)$ is a sphere.) In other words, $f_{\mathbf{S}}$ selects the closes worlds in $M_L$ to $X$ where $A$ holds. Note that S4 (the Limit Assumption) plays a crucial role here, for it ensures that $f_{\mathbf{S}}$ is nonempty when $A$ is not inconsistent (i.e., $\neg A\notin L$).

Grove proposes a different kind of model, which he claims to be equivalent to ^0e19fa.

Total Order on $M_L$

Let $X\subseteq M_L$ and ${\le }_X$ ($\le$ for simplicity) be a relation on $M_L$ satisfying the following:

• ($\le 1$) $\le$ is connected: for all $x,y\in M_L$, either $x\le y$ or $y\le x$.
• ($\le 2$) $\le$ is transitive.
• ($\le 3$) If $\left|A\right|\ne \varnothing$, then the set $\{x\in \left|A\right|:x\le y,\text{ for all }y\in \left|A\right|\}\ne \varnothing$ – this is the analogue of S4.
• ($\le 4$) $x\in M_L$ is $\le$-minimal (i.e., $x\le y$ for all $y\in M_L$) if, and only if, $x\in X$.

Proposition

^0e19fa and ^02e2bf are equivalent.

bproof TBD eproof

Before introducing the main proofs by Grove, consider the following useful lemma.

Lemma

Let $A,B\in F$.

$$\begin{array}{rlrl}(1)& & \left|A\wedge B\right|& =\left|A\right|\cap \left|B\right|\\ (2)& & \left|A\vee B\right|& =\left|A\right|\cup \left|B\right|\end{array}$$

bproof The proof is straightforward.

1. Note that $\left|A\wedge B\right|$ is the set of $m\in M_L$ such that $A\wedge B\in m$. Since $m$ is a theory ^9d8d32, $A,B\in m$, so $m\in \left|A\right|\cap \left|B\right|$. The other direction follows analogously.
2. Note that $\left|A\vee B\right|$ is the set of $m\in M_L$ such that $A\vee B\in m$. Since $m$ is a theory ^9d8d32, either $A\in m$ or $B\in m$, so $m\in \left|A\right|\cup \left|B\right|$. The other direction follows analogously.

This completes the proof. eproof

Augmentation (“ $/$”) vs. Revision (“$+$”)

In ^19b236, $T+A:=t(f_{\mathbf{S}}(A))$. It is useful to see what augmentation amounts to in terms of spheres system. First, by ^243d0b, for any $S\subseteq M_L$ and $A\in F$,

$$t(S\cap \left|A\right|)=Cn(t(S)\cup \{A\})$$

Therefore, by properties (2) and (4) in ^243d0b,

$$\begin{array}{rl}T/A& =Cn(T\cup \{A\})\\ & =Cn(t(\left|T\right|)\cup \{A\})\\ & =t(\left|T\right|\cap \left|A\right|)\end{array}$$

So, while revising a theory $T$ by $A$ means taking $t(f_{\mathbf{S}}(A))$, where $\mathbf{S}$ is a system centered on $T$, expanding a theory $T$ by $A$ means taking $t(\left|T\right|\cap \left|A\right|)$. (N.b., if $\left|T\right|\cap \left|A\right|=\varnothing$, it follows that $t(\left|T\right|\cap \left|A\right|)=F$, as expected.)

4. Soundness and Completeness

The following two theorems are the main result of (Grove, 1988).

4.1. Soundness

Soundness

Let $\mathbf{S}$ be a system of spheres in $M_L$ centered on $\left|T\right|$ for some theory $T\in \mathcal{T}$. If we define, for any $A\in F$,

$$T+A:=t(f_{\mathbf{S}}(A))$$

then the axioms (+2) to (+8) are all satisfied.

bproof Let $\mathbf{S}$ be a system of spheres in $M_L$ centered on $\left|T\right|$ for some theory $T\in \mathcal{T}$.

(+1) Clearly, $Cn(t(f_{\mathbf{S}}(A)))=t(f_{\mathbf{S}}(A))$, for $t(S)$ is a theory for any $S\subseteq M_L$ by ^243d0b, and $f_{\mathbf{S}}(A)=c(A)\cap \left|A\right|\subseteq M_L$.

(+2) Let me prove that $A\in T+A$. We have $f_{\mathbf{S}}(A))=t(\left|A\right|\cap c(A)$ by definition. Since $c(A)$ is a sphere, it is a set of $m\in M_L$. By ^243d0b (prop. 4), it follows that

$$\begin{array}{rl}t(f_{\mathbf{S}}(A))& =t(\left|A\right|\cap c(A))\\ & =Cn(t(c(A))\cup \{A\})\end{array}$$

and since $A⊢A$, $A\in Cn(t(c(A))\cup \{A\})=t(f_{\mathbf{S}}(A))$.

(+3) Suppose $\neg A\notin T$, and let me prove that $T+A=Cn(T\cup \{A\})$. Since $\neg A\notin T$, it follows that $T\cup \{A\}$ is consistent, i.e. there exists some $m\in M_L$ such that $T\subseteq m$ and $A\in m$. Therefore, $\left|T\right|\cap \left|A\right|\ne \varnothing$. Since $\left|T\right|$ is the smallest sphere in $\mathbf{S}$ and $\left|T\right|\cap \left|A\right|\ne \varnothing$, it follows that $c(A)=\left|T\right|$. So,

$$t(f_{\mathbf{S}}(A))=t(\left|A\right|\cap \left|T\right|)$$

and since $\left|T\right|\subseteq M_L$, it follows from ^243d0b (prop. 4)

$$\begin{array}{rlr}t(f_{\mathbf{S}}(A))& =t(\left|A\right|\cap \left|T\right|)& \\ & =Cn(t(\left|T\right|)\cup \{A\})& \\ & =Cn(T\cup \{A\})& [\text{By Prop. 2 of }t]\end{array}$$

(+4) Suppose $\neg A\notin L$, and let me show that $Con(T+A)$, i.e. that $Cn(T+A)\ne F$. Let me show that $T+A\ne \varnothing$, and conclude from ^243d0b (prop. 3).

Since $\neg A\notin L$, $A$ is not a contradiction, therefore there exists some $m\in M_L$ such that $A\in m$. So $\left|A\right|$ is nonempty. Since we also have that $\left|A\right|\cap \bigcup \mathbf{S}=M_L$ is nonempty, by S4 $c(A)$ is nonempty, and it is the smallest $U\in \mathbf{S}$ such that $U\cap \left|A\right|$ is nonempty. Hence, $\left|A\right|\cap c(A)$ is nonempty, and by ^243d0b (prop. 3), $t(\left|A\right|\cap c(A))=t(f_{\mathbf{S}}(A))$ is consistent.

(+5) Suppose $A\leftrightarrow B\in L$, and let me show that $T+A=T+B$. Since $L\subseteq m$, for all $m\in M_L$, we have that $\left|A\right|=\left|B\right|$: if $m\in \left|A\right|$, since $m$ is a theory and $A\leftrightarrow B\in m$, $m\in \left|B\right|$, and the same goes for any $m\in \left|B\right|$. Since $\left|A\right|=\left|B\right|$, $c(A)=c(B)$, and therefore $\left|A\right|\cap c(A)=\left|B\right|\cap c(B)$, which implies that

$$\begin{array}{rl}\left|A\right|\cap c(A)& =\left|B\right|\cap c(B)\\ f_{\mathbf{S}}(A)& =f_{\mathbf{S}}(B)\\ t(f_{\mathbf{S}}(A))& =t(f_{\mathbf{S}}(B))\\ T+A& =T+B\end{array}$$

(+7) We need to prove $T+(A\wedge B)\subseteq Cn((T+A)\cup \{B\})$. First, note that by ^f62804, $\left|A\wedge B\right|=\left|A\right|\cap \left|B\right|\subseteq \left|A\right|$. This means that any sphere intersecting $\left|A\wedge B\right|$ does intersect $\left|A\right|$ as well. Consider now $c(A)$, i.e. the sphere $U$ such that (1) $U\cap \left|A\right|\ne \varnothing$, and (2) $U\subseteq V$ for all $V$ with $V\cap \left|A\right|\ne \varnothing$. Since $c(A\wedge B)$ intersects $\left|A\wedge B\right|$ by definition, from the reasoning above it follows that it does intersect $\left|A\right|$ as well. By the definition of $c(A)$, then $c(A)\subseteq c(A\wedge B)$.

For any $A,B\in F$: $c(A)\subseteq c(A\wedge B)$.

$c(A)$ is a sphere $U\in \mathbf{S}$ such that: $U\cap \left|A\right|\ne \varnothing$ and, for all $V\cap \left|A\right|\ne \varnothing$, $U\subseteq V$. Consider now $c(A\wedge B)$. Since $c(A\wedge B)\cap \left|A\wedge B\right|\ne \varnothing$ by definition, $c(A\wedge B)\cap \left|A\right|\ne \varnothing$. By the definition of $c(A)$, it follows that $c(A)\subseteq c(A\wedge B)$.

Here is a graph showing why this is the case:

Therefore,

$$\begin{array}{rcl}c(A)& \subseteq & c(A\wedge B)\\ c(A)\cap \left|A\right|\cap \left|B\right|& \subseteq & c(A\wedge B)\cap \left|A\right|\cap \left|B\right|\end{array}$$

By prop. 5 of ^243d0b (i.e., the Reverse-Inclusion Property), it follows that

$$\begin{array}{r}t(c(A\wedge B)\cap \left|A\right|\cap \left|B\right|)\subseteq t(c(A)\cap \left|A\right|\cap \left|B\right|)\\ t(c(A\wedge B)\cap \left|A\wedge B\right|)\subseteq t(c(A)\cap \left|A\right|\cap \left|B\right|)\end{array}$$

By definition, $t(c(A\wedge B)\cap \left|A\wedge B\right|)=T+(A\wedge B)$. Regarding the RHS, apply prop. 4 of ^243d0b by setting $S:=c(A)\cap \left|A\right|\subseteq M_L$, and so

$$\begin{array}{rl}t(c(A)\cap \left|A\right|\cap \left|B\right|)& =t\left(\right(c(A)\cap \left|A\right|)\cap \left|B\right|)\\ & =Cn\left(t\right(c(A)\cap \left|A\right|)\cup \{B\})\\ & =Cn\left(\right(T+A)\cup \{B\})\\ & =(T+A)/B\end{array}$$

Therefore, we conclude that $T+(A\wedge B)\subseteq (T+A)/B$.

(+8) Suppose $\neg B\notin T+A$. We need to prove $Cn((T+A)\cup \{B\})\subseteq T+(A\wedge B)$. Since $\neg B\notin T+A$ and $T+A$ is a theory—see the proof of (+1)—it follows that $B$ is consistent with the theory $T+A$, i.e. there exists at least one possible world $m\in M_L$ such that $m\in \left|B\right|$ and $m\in \left|T+A\right|$. Hence $\left|T+A\right|\cap \left|B\right|\ne \varnothing$. We need to prove that also the “generating set” of $T+A$, i.e. $c(A)\cap \left|A\right|$, is consistent with $B$, i.e. that $c(A)\cap \left|A\right|\cap \left|B\right|\ne \varnothing$.

Suppose for reductio that $c(A)\cap \left|A\right|\cap \left|B\right|=\varnothing$. So, for any $m\in c(A)\cap \left|A\right|$, $B\notin m$. Since $m$ is complete for all $m\in M_L$, it follows that $\neg B\in m$ for all $m\in c(A)\cap \left|A\right|$. Thus, $\neg B\in t(c(A)\cap \left|A\right|)=T+A$, contradicting our hypothesis. Therefore,

$$\begin{array}{rl}c(A)\cap \left|A\right|\cap \left|B\right|& =c(A)\cap \left|A\wedge B\right|\\ & \ne \varnothing \end{array}$$

Therefore, the closest sphere intersecting $\left|A\right|$ also intersects $\left|A\wedge B\right|$, and so by the definition of $c(A\wedge B)$, it follows that $c(A\wedge B)\subseteq c(A)$. [Also, consider that the definition of $c(A)$ and ^f62804 imply that $c(A)\subseteq c(A\wedge B)$. Therefore, $c(A)=c(A\wedge B)$.]

We then argue as above:

$$\begin{array}{rcl}c(A\wedge B)& \subseteq & c(A)\\ c(A\wedge B)\cap \left|A\right|\cap \left|B\right|& \subseteq & c(A)\cap \left|A\right|\cap \left|B\right|\\ t(c(A)\cap \left|A\right|\cap \left|B\right|)& \subseteq & t(c(A\wedge B)\cap \left|A\right|\cap \left|B\right|)\end{array}$$

By definition, $t(c(A\wedge B)\cap \left|A\wedge B\right|)=T+(A\wedge B)$. Regarding the LHS, apply prop. 4 of ^243d0b by setting $S:=c(A)\cap \left|A\right|\subseteq M_L$, and so

$$\begin{array}{rl}t(c(A)\cap \left|A\right|\cap \left|B\right|)& =t\left(\right(c(A)\cap \left|A\right|)\cap \left|B\right|)\\ & =Cn\left(t\right(c(A)\cap \left|A\right|)\cup \{B\})\\ & =Cn\left(\right(T+A)\cup \{B\})\\ & =(T+A)/B\end{array}$$

Therefore, we conclude that $(T+A)/B\subseteq T+(A\wedge B)$.

So, we have proved that, if $T+A:=t(f_{\mathbf{S}}(A))$, then $+$ satisfies (+1)-(+8). eproof

4.2. Completeness

Completeness

Let $+:\mathcal{T}\times F\to \mathcal{T}$ be any function satisfying (+1)-(+8). Then, for any fixed theory $T$, there is a system of spheres on $M_L$, $\mathbf{S}$, centered on $\left|T\right|$ and satisfying $T+A=t(f_{\mathbf{S}}(A))$ for all $A\in F$.

bproof Let $+:\mathcal{T}\times F\to \mathcal{T}$ be any function satisfying (+1)-(+8). Consider an arbitrary theory $T\in \mathcal{T}$. Define ${\mathbf{S}}^{\prime }$ as the class of all nonempty subsets $U\subseteq M_L$ satisfying the following conditions:

1. (Relevance) For all $u\in U$ there is $A\in F$ such that $u\in \left|T+A\right|$, and
2. (Swallowing) For all $A\in F$, if $\left|A\right|\cap U\ne \varnothing$, then $\left|T+A\right|\subseteq U$.

Then, define $\mathbf{S}$ as follows:

$$\mathbf{S}:=\{\begin{array}{ll}{\mathbf{S}}^{\prime }\cup \{M_L\}& \text{T consistent}\\ {\mathbf{S}}^{\prime }\cup \{M_L,\varnothing \}& \text{otherwise}\end{array}$$

(In other words, the candidate sphere system $\mathbf{S}$ is obtained by adding the universe (and possibly the empty set) to ${\mathbf{S}}^{\prime }$.) Let me now prove that $\mathbf{S}$ is a system of spheres.

Part One: $\mathbf{S}$ is a system of spheres.

(S1) Distinguish two cases.

Case 1: $T$ is inconsistent. By construction, $\mathbf{S}={\mathbf{S}}^{\prime }\cup \{M_L,\varnothing \}$. Let $U,V\in \mathbf{S}$.

• If $U=\varnothing$ or $V=\varnothing$: Since $\varnothing \subseteq X$ for any set $X$, the nesting condition ($U\subseteq V$ or $V\subseteq U$) holds trivially.
• If $U=M_L$ or $V=M_L$: Since $X\subseteq M_L$ for any set of worlds $X$, nesting holds trivially.
• If $U,V\in {\mathbf{S}}^{\prime }$: These are nonempty sets satisfying Relevance and Swallowing. The proof is identical to Case 2 below. (Note: In step 6, the non-emptiness of $|T+(A\vee B)|$ is guaranteed by axiom (+4) solely because $A\vee B$ is consistent. it does not require $T$ to be consistent).

Case 2: T is consistent. Let $U,V\in \mathbf{S}$. Suppose for reductio that $U⊈V$ and $V⊈U$. This means there exist worlds $u\in U\setminus V$ and $v\in V\setminus U$.

1. Since $u\in U$, by (Relevance) there is some $A$ such that $u\in \left|T+A\right|$. By (+2), $A\in T+A$, hence for all $m\in \left|T+A\right|$, $A\in m$—that is, $\left|T+A\right|\subseteq \left|A\right|$. So, $A\in u$. Since $u\in \left|A\right|\cap U$, the intersection is not empty, and by (Swallowing) we have $\left|T+A\right|\subseteq U$.
2. Since $u\in \left|T+A\right|$ and $u\notin V$, it follows that $\left|T+A\right|⊈V$.
3. By the contrapositive of Swallowing for $V$: If $\left|T+A\right|⊈V$, then $\left|A\right|\cap V=\varnothing$.
4. Analogously for $v$: There exists $B$ such that $v\in \left|T+B\right|\subseteq V$. Since $v\notin U$, $\left|T+B\right|⊈U$. By Swallowing for $U$, $\left|B\right|\cap U=\varnothing$.
5. Consider now $A\vee B$.
   • $u\in \left|T+A\right|\subseteq \left|A\right|\subseteq \left|A\vee B\right|$. Since $u\in U$, $\left|A\vee B\right|\cap U\ne \varnothing$. By Swallowing, $\left|T+(A\vee B)\right|\subseteq U$.
   • $v\in \left|T+B\right|\subseteq \left|B\right|\subseteq \left|A\vee B\right|$. Since $v\in V$, $\left|A\vee B\right|\cap V\ne \varnothing$. By Swallowing, $\left|T+(A\vee B)\right|\subseteq V$.
   • Therefore, $\left|T+(A\vee B)\right|\subseteq U\cap V$.
6. By (+4), since $T$ is consistent ex hypothesi, $T+(A\vee B)$ is consistent (unless $A\vee B$ is logically false, which is impossible since $u\ni A$), so $\left|T+(A\vee B)\right|\ne \varnothing$. Let $z\in \left|T+(A\vee B)\right|$.
   • $z\in U$ and $z\in V$.
   • Also, since $A\vee B\in T+(A\vee B)$ by (+2), we have $z\in \left|A\vee B\right|$, so $z\in \left|A\right|$ or $z\in \left|B\right|$.
   • If $z\in \left|A\right|$: since $z\in V$, $\left|A\right|\cap V\ne \varnothing$. Contradiction with (3).
   • If $z\in \left|B\right|$: since $z\in U$, $\left|B\right|\cap U\ne \varnothing$. Contradiction with (4).
7. Either way, we get a contradiction. So, our initial assumption was false. $\mathbf{S}$ is nested.

(S2) Let me show tha (1) $\left|T\right|\in \mathbf{S}$ and that, (2) for all $U\in \mathbf{S}$, $\left|T\right|\subseteq U$.

(1) To prove that $\left|T\right|\in \mathbf{S}$, distinguish two cases.

(1.1) If $T$ is inconsistent, i.e. $T=F$, then $\left|T\right|=\varnothing$, and by construction of $\mathbf{S}$ for the inconsistent case, $\varnothing \in \mathbf{S}$. Moreover, $\left|T\right|$ is hence a $\subseteq$-minimum for $\mathbf{S}$ in this case, for $\varnothing \subseteq U$ for any set $U$.

So, suppose $T$ is consistent.

1. (Relevance) Let me show that Relevance holds for $\left|T\right|$. Consider now an arbitrary $m\in \left|T\right|$ and an arbitrary tautology in $L$, which I will call $\top$. Since $T$ is consistent ex hypothesi, $\neg \top \notin T$, hence by (+3) it follows that $T+\top =Cn(T\cup \{\top \})$. Since $\top \in L\subseteq T$, $T+\top =Cn(T)=T$, for $T$ is a theory ex hypothesi. Therefore, it immediately follows that $m\in \left|T+\top \right|=\left|T\right|$.
2. (Swallowing) Consider an arbitrary $A\in F$ and suppose $\left|A\right|\cap \left|T\right|\ne \varnothing$. That is, there exists a possible world $m\in M_L$ such that $A\in m$ and $T\subseteq m$. Therefore, $\neg A\notin T$ (otherwise, $A,\neg A\in m$, contradicting the consistency of $m\in M_L$). By (+3) $T+A=Cn(T\cup \{A\})$. This implies that $\left|T+A\right|=\left|T\right|\cap \left|A\right|$ [see callout below]. Therefore, we have that $\left|T+A\right|=\left|T\right|\cap \left|A\right|\subseteq \left|T\right|$, proving that $\left|T\right|$ satisfies (Swallowing).

If $\neg A\notin T$, $\left|T+A\right|=\left|Cn(T\cup \{A\})\right|=\left|T\right|\cap \left|A\right|$

(Note: This assumes the case where $\neg A\notin T$, so $T+A=Cn(T\cup \{A\})$.)

($\subseteq$) Suppose $m\in M_L$ is such that $m\in \left|T+A\right|$. This means $Cn(T\cup \{A\})\subseteq m$. Since $T\subseteq Cn(T\cup \{A\})$ and $A\in Cn(T\cup \{A\})$, it follows that $T\subseteq m$ and $A\in m$. Therefore, $m\in |T|$ and $m\in |A|$, so $m\in |T|\cap |A|$.

($\supseteq$) Suppose $m\in M_L$ is such that $m\in \left|T\right|\cap \left|A\right|$. From the latter, $T\subseteq m$ and $A\in m$, which implies $T\cup \{A\}\subseteq m$. By Monotonicity for $Cn$, $Cn(T\cup \{A\})\subseteq Cn(m)$. Since $m$ is a world (maximal consistent set), $Cn(m)=m$. Thus, $Cn(T\cup \{A\})\subseteq m$, meaning $m\in \left|Cn(T\cup \{A\})\right|$. Since $\neg A\notin T$ ex hypothesi, $T+A=Cn(T\cup \{A\})$, hence $m\in \left|T+A\right|$.

Concluding, $\left|T+A\right|=\left|T\right|\cap \left|A\right|$.

Therefore, $\left|T\right|\in {\mathbf{S}}^{\prime }$, and so $\left|T\right|\in \mathbf{S}$. Consider now any $U\in \mathbf{S}$, and let me show that $\left|T\right|\subseteq U$. First, note that either $U=M_L$ or $U\in {\mathbf{S}}^{\prime }$, which implies that $U$ is nonempty.

1. $U\in {\mathbf{S}}^{\prime }$. Since $\top \in F$, $\left|\top \right|=M_L$ and $U$ is nonempty, we have that $U\cap \left|\top \right|\ne \varnothing$. By (Swallowing), $\left|T+\top \right|\subseteq U$. Since $T$ is consistent ex hypothesi, $\neg \top \notin T$, hence by (+3) it follows that $T+\top =Cn(T\cup \{\top \})$. Since $\top \in L\subseteq T$, $T+\top =Cn(T)=T$, for $T$ is a theory ex hypothesi. Therefore, $\left|T+\top \right|=\left|T\right|$, and so $\left|T\right|\subseteq U$. Since $U$ is arbitrary, $\left|T\right|$ is a $\subseteq$-minimum.
2. $U=M_L$. Obviously, $\left|T\right|\subseteq M_L$.

Thus, (S2) holds.

(S3) $M_L\in \mathbf{S}$ by construction.

(S4) We must prove: If $|A|\cap \bigcup \mathbf{S}\ne \varnothing$ (i.e., if $A$ is consistent), then there exists a sphere $U\in \mathbf{S}$ such that:

1. $U\cap |A|\ne \varnothing$ (It intersects $|A|$).
2. For any $V\in \mathbf{S}$, if $V\cap |A|\ne \varnothing$, then $U\subseteq V$ (It is the smallest such sphere).

Assume $|A|\cap \bigcup \mathbf{S}\ne \varnothing$ (i.e., $A$ is consistent). We construct the specific set $U_A$ as defined by Grove.

$$U_A:=\bigcup \{|T+B|:|A|\subseteq |B|\}$$

(In words: The union of all revisions by $B$ where $B$ is logically weaker than $A$).

1. Prove (1). Naturally, $|A|\subseteq |A|$ holds. Therefore, $|T+A|$ is one of the sets included in the union $U_A$. Since $\left|A\right|\ne \varnothing$, $\neg A\notin L$ (note that $L\subseteq m$, for all $m\in M_L$). By postulate (+4), $T+A$ is consistent, so $|T+A|\ne \varnothing$. By postulate (+2), $A\in T+A$, and so $|T+A|\subseteq |A|$. Since $|T+A|\subseteq U_A$, $|T+A|\subseteq |A|$, and $\left|T+A\right|\ne \varnothing$, then

$U_A\cap |A|\ne \varnothing .$

1. Prove (2a). We must show $U_A\in \mathbf{S}$, i.e. that it satisfies the two conditions for ${\mathbf{S}}^{\prime }$: Relevance and Swallowing.

   1. (Relevance). By definition, $U_A$ is a union of sets of the form $|T+B|$. Therefore, every world $u\in U_A$ belongs to some $|T+B|$.

   2. (Swallowing) We need to prove that, for all $C\in F$, if $|C|\cap U_A\ne \varnothing$, then $|T+C|\subseteq U_A$. Suppose $|C|\cap U_A\ne \varnothing$. By the definition of $U_A$, this implies that there is some $B\in F$ such that (i) $|A|\subseteq |B|$ and (ii) $|C|\cap |T+B|\ne \varnothing$.

      Consider the sentence $B\vee C$. Note that $|A|\subseteq |B|\subseteq |B\vee C|$. Therefore, by the definition of $U_A$, $|T+(B\vee C)|$ is part of the union $U_A$, so $|T+(B\vee C)|\subseteq U_A$. We now claim that $|C|\cap |T+(B\vee C)|\ne \varnothing$. Suppose for reductio that $|C|\cap |T+(B\vee C)|=\varnothing$. This implies that, for all worlds $m\in M_L$ such that $T+(B\vee C)\subseteq m$, $C\notin m$, and hence $C\notin T+(B\vee C)$. Since $T+(B\vee C)$ is a theory, $\neg C\in T+(B\vee C)$. Since $T+(B\vee C)$ is consistent by (+4), it cannot imply $\neg (B\vee C)$. Since it implies $\neg C$, it must be that $\neg B\notin T+(B\vee C)$ (otherwise it would imply both negations, and thus the negation of the disjunction). Since $\neg B\notin T+(B\vee C)$, we can apply (+7) and (+8) to establish:

      $$T+((B\vee C)\wedge B)=Cn((T+(B\vee C))\cup \{B\})$$

      Since $((B\vee C)\wedge B)$ is logically equivalent to $B$, the LHS is $T+B$. If $\neg C\in T+(B\vee C)$ (as assumed), then $\neg C$ must also be in the expansion on the RHS. Therefore, $\neg C\in T+B$. But this means $|C|\cap |T+B|=\varnothing$ (for any $m\in M_L$ is consistent), contradicting assumption (ii) above.

      Therefore, $|C|\cap |T+(B\vee C)|\ne \varnothing$, which implies $\neg C\notin T+(B\vee C)$. We can now apply (+8):

      $$Cn((T+(B\vee C))\cup \{C\})\subseteq T+((B\vee C)\wedge C)=T+C$$

      We now translate this syntactic inclusion into semantic set inclusion. Recall that if theory $X\subseteq Y$, then $|Y|\subseteq |X|$.

      $$\begin{array}{rlr}|T+C|& \subseteq |Cn((T+(B\vee C))\cup \{C\})|& \\ & =|T+(B\vee C)|\cap |C|& [\ast ]\\ & \subseteq |T+(B\vee C)|& \end{array}$$

      Since we established earlier that $|T+(B\vee C)|\subseteq U_A$, it follows by transitivity that $|T+C|\subseteq U_A$. Thus, Swallowing holds.

Step $[\ast ]$

The step denoted by $[\ast ]$ relies on a crucial relationship between syntactic expansion and semantic intersection of truth-sets. The following provides justification for why $|Cn(K\cup \{C\})|=|K|\cap |C|$ (where $K$ is the theory $T+(B\vee C)$).

First, note that the following holds:

$$m\in |Cn(K\cup \{C\})|⟺K\subseteq m\text{ and }C\in m$$

$(⟹)$ obviously holds: since $K\subseteq Cn(K\cup \{C\})$ and $C\in Cn(K\cup \{C\})$, if $Cn(K\cup \{C\})\subseteq m$, clearly $K\subseteq m$ and $C\in m$. $(⟸)$ suppose now that $K\subseteq m$ and $C\in m$. Since $K\cup \{C\}\subseteq m$ ex hypothesi, by Monotonicity $Cn(K\cup \{C\})\subseteq Cn(m)=m$, for $m$ is a theory. Hence, $m\in \left|Cn(K\cup \{C\})\right|$.

Moreover, the following is clearly true:

$$K\subseteq m\text{ and }C\in m⟺m\in |K|\cap |C|$$

For

1. $K\subseteq m$ is the definition of $m\in |K|$.
2. $C\in m$ is the definition of $m\in |C|$.

Combining the two iffs, we get $m\in |Cn(K\cup \{C\})|⟺m\in |K|\cap |C|$, which means that:

$$\left|Cn(K\cup \{C\})\right|=\left|K\right|\cap \left|C\right|$$

N.b. Don’t forget that $\left|\cdot \right|$ returns different value, depending on whether its argument is a formula $C\in F$ of a set of formulas $K\subseteq F$!

2. Prove (2b). We need to prove $U_A$ is the Smallest Sphere (Minimality). Let $V$ be any sphere in $\mathbf{S}$ such that $V\cap |A|\ne \varnothing$. We must show $U_A\subseteq V$. Take any component $|T+B|$ that makes up $U_A$ (where $|A|\subseteq |B|$). Since $V\cap |A|\ne \varnothing$ and $|A|\subseteq |B|$, it follows that $V\cap |B|\ne \varnothing$.

   Since $V$ is a sphere in $\mathbf{S}$, it must satisfy the Swallowing condition. Because $V$ intersects $|B|$, by (Swallowing) $|T+B|\subseteq V$. Since this holds for every $B$ such that $|A|\subseteq |B|$, the entire union is contained in $V$:

   $$U_A\subseteq V$$

We have constructed a set $U_A$ that is a valid sphere in $\mathbf{S}$, intersects $|A|$, and is a subset of every other sphere intersecting $|A|$. Thus, Condition (S4) holds.

Part Two: $T+A=t(f_{\mathbf{S}}(A))$.

We need to verify that the system of spheres $\mathbf{S}$ we constructed actually generates the original revision function $+$. Specifically, we want to prove:

$T+A=t(f_{\mathbf{S}}(A))$

We will prove the stronger condition that the sets of worlds are identical:

$|T+A|=|A|\cap c(A)$

Case 1: $A$ is Inconsistent ($\neg A\in L$).

1. By Postulate (+2), $A\in T+A$. If $A$ is logically false, then $T+A$ contains a contradiction, so $T+A=F$ (the inconsistent theory). Thus, $|T+A|=\varnothing$.
2. On the sphere side, if $A$ is inconsistent, $|A|=\varnothing$. Therefore, $f_{\mathbf{S}}(A)=|A|\cap c(A)=\varnothing \cap c(A)=\varnothing$.
3. The equality holds: $|T+A|=\varnothing =|A|\cap c(A)$.

Case 2: $A$ is Consistent ($\neg A\notin L$). We prove the equality by mutual inclusion.

Direction 1: $|T+A|\subseteq |A|\cap c(A)$

1. Since $A$ is consistent, by Postulate (+4), $T+A$ is consistent, so $|T+A|\ne \varnothing$. Also, $A\in T+A$ implies $|T+A|\subseteq |A|$.
2. Recall that $c(A)$ is the smallest sphere in $\mathbf{S}$ intersecting $|A|$. Since $|T+A|\subseteq |A|$ and $|T+A|\ne \varnothing$, we know $|A|\cap \bigcup \mathbf{S}\ne \varnothing$, so $c(A)$ exists.
3. Since $c(A)$ is a sphere in our system $\mathbf{S}$, it must satisfy the Swallowing condition, i.e. if $|A|\cap c(A)\ne \varnothing$, then $|T+A|\subseteq c(A)$.
4. Since $c(A)$ is the smallest sphere intersecting $|A|$, the antecedent is true. Therefore, $|T+A|\subseteq c(A)$.
5. Combining this with $|T+A|\subseteq |A|$, we get: $|T+A|\subseteq |A|\cap c(A)$

Direction 2: $|A|\cap c(A)\subseteq |T+A|$. This relies on the specific sphere $U_A$ constructed in Part One. Recall $U_A=\bigcup \{|T+B|:|A|\subseteq |B|\}$.

1. Minimality: In Part One, we proved that $U_A$ is a sphere intersecting $|A|$ and that for any sphere $V$ intersecting $|A|$, $U_A\subseteq V$. By definition, $c(A)$ is the smallest sphere intersecting $|A|$. Therefore, $c(A)\subseteq U_A$. (Note: In fact, $c(A)=U_A$, but inclusion is sufficient here).

2. Intersecting: Since $c(A)\subseteq U_A$, intersecting both sides with $|A|$ preserves the subset relation: $|A|\cap c(A)\subseteq |A|\cap U_A$

3. Collapsing the Union: We now evaluate $|A|\cap U_A$.

$$\begin{array}{rl}|A|\cap U_A& =|A|\cap \bigcup \{|T+B|:\left|A\right|\subseteq \left|B\right|\}\\ & =\bigcup \{|A|\cap |T+B|:\left|A\right|\subseteq \left|B\right|\}\end{array}$$

Consider any term $|A|\cap |T+B|$ in this union (where $\left|A\right|\subseteq \left|B\right|$). If the intersection is empty, it contributes nothing. If the intersection is non-empty ($|A|\cap |T+B|\ne \varnothing$), then $\neg A\notin T+B$. We can apply postulates (+7) and (+8):

$$\begin{array}{rlr}(T+B)/A& =T+(B\wedge A)& \\ & =T+A& (\text{since }\left|A\right|\subseteq \left|B\right|,\left|A\wedge B\right|=\left|A\right|\cap \left|B\right|=\left|A\right|)\end{array}$$

In terms of worlds: $|T+B|\cap |A|=|T+A|$. Therefore, every non-empty component of the union is exactly equal to $|T+A|$. Thus:

$$|A|\cap U_A=|T+A|$$

4. Conclusion: Substituting this back into step 2:

$$|A|\cap c(A)\subseteq |T+A|$$

Concluding, since we have proved both $|T+A|\subseteq |A|\cap c(A)$ and $|A|\cap c(A)\subseteq |T+A|$, we have:

$$|T+A|=|A|\cap c(A)$$

Since $T+A$ is a theory, by ^243d0b (prop.2) applying the theory operator $t(\cdot )$ to both sides yields:

$$\begin{array}{rl}t(\left|T+A\right|)& =t(\left|A\right|\cap c(A))\\ T+A& =t(f_{\mathbf{S}}(A))\end{array}$$

eproof

5. Alternative Modeling

Grove presents an alternative method for modeling a belief revision operation $+$ using a relation $\le$ on the set of formulas $F$. This modeling is advantageous because the axioms for revision do not uniquely determine the specific changes required; generally, there are multiple valid choices for $T+A$ upon revision by $A$. Consequently, it is natural to consider an ordering of sentences to facilitate decisions regarding which elements to remove from or add to $T$.

Plausibility Relation ( $\le$)

Consider the relation $\le \subseteq F^2$ satisfying the following properties:

1. $\le$ is connected.
2. $\le$ is transitive.
3. If $A\to B\vee C\in L$, then $B\le A$ or $C\le A$.
4. $A$ is $\le$-minimal in $F$ if and only if $\neg A\notin T$.
5. $A$ is $\le$-maximal in $F$ if and only if $\neg A\in L$.

The expression $A\le B$ is interpreted as “$A$ is at least as plausible as $B$”.

Observations regarding these axioms:

• Axiom (3) implies that if $A\to B$, then $B\le A$. This follows from the equivalence of $B$ with $B\vee B$, and the fact that “$(B\le A)\vee (B\le A)$” is equivalent to $B\le A$.
• Axiom (4) assigns the minimal position to any sentence $A$ that is either in $T$ or consistent with $T$ (assuming $T$ is a consistent theory). Since revision $+$ based on $\le$ functions by selecting the sentences that are “most plausible” given $T$, it is reasonable to assign a privileged position to such sentences. These instances do not require actual revision (removing information from $T$), but rather augmentation (adding information without loss).

To prove that this is indeed an alternative modeling of $+$, Grove shows that this relation is equivalent to a system of spheres $\mathbf{S}$ centered on $T$.

Lemma

Consider a system of spheres $\mathbf{S}$ centered on $\left|T\right|$, and define the following relation on $F$:

$$A{\le }_{S}B:⟺c(A)\subseteq c(B)$$

and let us stipulate that $A{<}_{S}B$ iff $c(A)\subset c(B)$. It follows that:

1. ${\le }_S$ satisfies axioms (1)-(5);
2. the following definition of revision is identical to the one determined by $\mathbf{S}$:

$$T+A:=\{B\in F:A\wedge B{<}_{S}A\wedge \neg B\}$$

bproof Part One. Let me first prove that ${\le }_S$ satisfies axioms (1)-(5) of ^7efc5a.

• $(\le 1)-(\le 2)$. Connectivity follows from the fact that $\mathbf{S}$ is nested, while transitivity follows from the properties of $\subseteq$.
• ($\le 3$). Suppose $A\to B\vee C\in L$. Since $A\to B\vee C$, we have that $\left|A\right|\subseteq \left|B\vee C\right|=\left|B\right|\cup \left|C\right|$ (if $m\in \left|A\right|$, since $A\to B\vee C\in L\subseteq m$ and $m$ is a theory, $B\vee C\in m$, and since $m$ is consistent either $B\in m$ or $C\in m$). We have to show that either $c(B)\subseteq c(A)$ or $c(C)\subseteq c(A)$.
  1. First, consider consider $c(B\vee C)$, namely the sphere in $\mathbf{S}$ that intersects $\left|B\vee C\right|$ and such that, for any other sphere $U$ intersecting $\left|B\vee C\right|$, $c(B\vee C)\subseteq U$. Consider $c(A)$. By definition, $c(A)\cap \left|A\right|\ne \varnothing$, and since $\left|A\right|\subseteq \left|B\vee C\right|$, we have $c(A)\cap \left|B\vee C\right|\ne \varnothing$. By definition, it follows $c(B\vee C)\subseteq c(A)$.
  2. Now, we observe that $c(B\vee C)=c(B)$ or $c(B\vee C)=c(C)$. Note that $|B|\subseteq |B\vee C|$, so any sphere intersecting $|B|$ intersects $|B\vee C|$, implying $c(B\vee C)\subseteq c(B)$. Similarly $c(B\vee C)\subseteq c(C)$.
  3. Since $c(B\vee C)$ intersects $|B|\cup |C|$, it must intersect at least one of them. If it intersects $|B|$, then by definition of $c(B)$, $c(B)\subseteq c(B\vee C)$. Combined with the above, $c(B)=c(B\vee C)\subseteq c(A)$, so $B{\le }_{S}A$. If it intersects $|C|$, then $c(C)=c(B\vee C)\subseteq c(A)$, so $C{\le }_{S}A$.
• Minimality ($\le 4$): $A$ is minimal iff $c(A)\subseteq c(B)$ for all $B$. This holds iff $c(A)$ is the smallest sphere in $\mathbf{S}$, which is $|T|$ (by S2). $c(A)=|T|$ iff $|A|\cap |T|\ne \varnothing$, which is equivalent to $\neg A\notin T$.
• Maximality ($\le 5$): $A$ is maximal iff $c(B)\subseteq c(A)$ for all $B$. This holds iff $c(A)$ is the largest sphere, $M_L$ (by S3). By convention, $c(A)=M_L$ iff $|A|=\varnothing$, i.e., $\neg A\in L$.

Part Two. Define $T+A$ as follows:

T+A := \{ B\in F: A \land B <_{S} A \land \neg B \} \tag{\dagger}

We show that this set is equal to $t(f_{\mathbf{S}}(A))$. ($\subseteq$) Consider any $B\in (†)$. By definition:

$$\begin{array}{rl}A\wedge B& {<}_{S}A\wedge \neg B\\ c(A\wedge B)& \subset c(A\wedge \neg B)\end{array}$$

Suppose for reductio that $B\notin t(f_{\mathbf{S}}(A))$. This means there exists some world $m\in c(A)\cap \left|A\right|$ such that $B\notin m$. Since $m$ is complete, $\neg B\in m$, and so $m\in \left|A\wedge \neg B\right|$. Since $c(A)$ intersects $\left|A\wedge \neg B\right|$ (at $m$), it follows that $c(A\wedge \neg B)\subseteq c(A)$. Also, note that by definition, $c(A\wedge B)$ intersects $\left|A\wedge B\right|$, and since $\left|A\wedge B\right|\subseteq \left|A\right|$, it intersects $|A|$. Thus $c(A)\subseteq c(A\wedge B)$. Combining these inclusions: $c(A\wedge \neg B)\subseteq c(A)\subseteq c(A\wedge B)$. However, ex hypothesi, $c(A\wedge B)\subset c(A\wedge \neg B)$. This implies a contradiction ($X\subseteq Y$ and $Y\subset X$ is impossible). Therefore, $B\in t(f_{\mathbf{S}}(A))$.

($\supseteq$) Let $B\in t(f_{\mathbf{S}}(A))$. By definition, $B\in m$ for all $m\in f_{\mathbf{S}}(A)=c(A)\cap |A|$, and so $f_{\mathbf{S}}(A)=c(A)\cap \left|A\right|\subseteq |B|$. This implies that $c(A)$ contains no worlds where $A$ is true and $B$ is false. Equivalently:

$c(A)\cap |A\wedge \neg B|=\varnothing$

Suppose for reductio that $B\notin (†)$. This means $A\wedge B/{<}_{S}A\wedge \neg B$. Since ${\le }_S$ is connected, this implies $A\wedge \neg B{\le }_{S}A\wedge B$, or:

$c(A\wedge \neg B)\subseteq c(A\wedge B)$

Now we observe the relationship with $c(A)$. Since $c(A)$ intersects $|A|$, it must intersect either $|A\wedge B|$ or $|A\wedge \neg B|$ (that is, since there is at least one $m\in \left|A\right|\cap c(A)$, either $B\in m$ of $\neg B\in m$). We established above that $c(A)\cap |A\wedge \neg B|=\varnothing$. Therefore, $c(A)$ must intersect $|A\wedge B|$. Since $c(A\wedge B)$ is the smallest sphere intersecting $|A\wedge B|$, it follows that $c(A\wedge B)\subseteq c(A)$. Combining these facts:

$c(A)\subseteq c(A\wedge \neg B)\subseteq c(A\wedge B)\subseteq c(A)$

This chain implies equality: $c(A)=c(A\wedge \neg B)$. However, by definition, $c(A\wedge \neg B)$ must intersect $|A\wedge \neg B|$. If they are equal, $c(A)$ must intersect $|A\wedge \neg B|$. But we established at the start that $c(A)\cap |A\wedge \neg B|=\varnothing$: contradiction.

Therefore:

$$\{B\in F:A\wedge B{<}_{S}A\wedge \neg B\}=t(f_{\mathbf{S}}(A))$$

completing our proof. eproof

Corollary

The belief revision operator $+$ defined via the relation ${\le }_S$ satisfies the AGM postulates (+1)–(+8).

bproof This result is an immediate consequence of Lemma ^448b11 and Theorem ^19b236.

1. Lemma ^448b11 establishes that the revision operator defined by the relation (i.e., $\{B:A\wedge B{<}_{S}A\wedge \neg B\}$) is identical to the operator defined by the system of spheres (i.e., $t(f_{\mathbf{S}}(A))$).
2. Theorem ^19b236 establishes that the operator defined by the system of spheres satisfies postulates (+1)–(+8).

Therefore, by transitivity, the operator defined via ${\le }_S$ satisfies the postulates. eproof

Representation by Ordering on Formulas

Let $+:\mathcal{T}\times F\to \mathcal{T}$ be any function satisfying (+1)-(+8). Then for any (fixed) theory $T$ there is a relation $<$ on $F$ such that, for all $A\in F$:

$$T+A=\{B\in F:(A\wedge B)<(A\wedge \neg B)\}$$

bproof This result follows from combining the representation of $+$ by spheres (Theorem 2) with the equivalence between spheres and formula orderings.

Since $+$ satisfies postulates (+1)-(+8), by Theorem 2 ^f347f9, there exists a system of spheres $\mathbf{S}$ centered on $|T|$ such that for all $A\in F$, $T+A=t(f_{\mathbf{S}}(A))$. Given this system $\mathbf{S}$, we define the relation $\le$ on $F$ as:

$$A\le B⟺c(A)\subseteq c(B)$$

and $A<B$ iff $c(A)\subset c(B)$. By Lemma ^448b11, the revision operator determined by this relation is identical to the one determined by the system of spheres $\mathbf{S}$. Specifically:

$$t(f_{\mathbf{S}}(A))=\{B\in F:(A\wedge B)<(A\wedge \neg B)\}$$

Substituting the identity from step 1 into step 3, we obtain $T+A=\{B\in F:(A\wedge B)<(A\wedge \neg B)\}$. eproof

Soundness of Ordering-Based Revision

Let $\le$ be any relation on $F$ satisfying postulates $(\le 1)$ to $(\le 5)$. Then the revision operation defined by:

$$T+A=\{B\in F:(A\wedge B)<(A\wedge \neg B)\}$$

satisfies the AGM axioms (+1) to (+8).

bproof Strategy: We prove this by constructing a system of spheres $\mathbf{S}$ from the relation $\le$ and showing they determine the same revision. Since sphere-based revision satisfies the axioms ^19b236, the relation-based revision must as well. eproof