Proofs

A

Proof of Theorem 4

Let Φ be a law, M ! ∈ M!Φ , and let T !Φ be the output of our algorithms on input theory T and law Φ. M

If T ∪ {Φ} #|= ⊥, then M ! ∈ M \ {M :#|= Φ} and M ! is Kn ! a model of T Φ = T ∪ {Φ}. Let T ∪ {Φ} |= ⊥. We analyze each case. K n

!

!

!

!

Let Φ be some ϕ ∈ F. Then M = %W , R & where W = (W \ val(¬ϕ)) ∪ val(ϕ) is minimal w.r.t. W and R! ⊆ R is maximal w.r.t. R, for some M = %W, R& ∈ M. As we have assumed the syntactical classical revision operator # is sound and complete w.r.t. its semantics and is moreM! M! over minimal, we have |= S # ϕ. Because R! ⊆ R, |= E . Thus it is enough to show that M ! is a model of the added laws. Given (ϕi ∧ π ∧ ϕA ) → %a&* ∈ T !ϕ , for every w ∈ W! , if M!

|= ϕi ∧ π ∧ ϕA , then w ∈ W (because S #|= (π ∧ ϕA ) → ⊥). CPL w From w ! ϕi and ϕi → %a&* ∈ Xa , we have Ra (w) #= ∅. M!

Suppose R!a (w) = ∅. As |= S # ϕ ∪ E and R! is maximal, M !!

every M !! = %W!! , R!! & s.t. |= S # ϕ ∪ E is s.t. R!!a (w) = ∅, and then S # ϕ ∪ E |= (π ∧ ϕA ) → [a]⊥. Because T |= Kn Kn (π ∧ ϕA ) → %a&*, and S #|= (π ∧ ϕA ) → ⊥ and S # ϕ #|= CPL CPL (π ∧ ϕA ) → ⊥, we get S # ϕ, E , X |= ¬(π ∧ ϕA ), and Kn ! then (ϕi ∧ π ∧ ϕA ) → %a&* ∈ / T ϕ . Hence R!a (w) #= ∅, and M!

|= (ϕi ∧ π ∧ ϕA ) → %a&*. If (π ∧ ϕA ) → [a]⊥ ∈ T !ϕ , then S |= (π ∧ ϕA ) → ⊥. CPL M!

Thus, for every w ∈ W! , if |= π ∧ ϕA , R!a (w) = ∅ and the w result follows. Let Φ now have the form ϕ → [a]ψ, for ϕ, ψ ∈ F. Then M! = %W! , R! & for some M = %W, R& ∈ M s.t. W! = W and R! ⊆ R, where R! is maximal w.r.t. R. M!

M!

From W! = W, |= S . As R! ⊆ R, |= E . Because S ∪E ⊆ ! T ϕ→[a]ψ , it suffices to show that M ! is a model of the added laws. M! M! By definition, |= ϕ → [a]ψ, and then |= (π∧ϕA ) → [a]ψ for every π ∈ IP(S ∧ ϕ). If (ϕi ∧π∧ϕA ) → %a&* ∈ T !ϕ→[a]ψ , then for every w ∈ W! , if w ! ϕi ∧ π ∧ ϕA , we have w ! ϕi . As w ∈ W, and ϕi → %a&* ∈ Xa , Ra (w) = ∅. If R!a (w) = ∅, then w! ! ¬ψ for every w! ∈ Ra (w). Thus as far as we added (π ∧ ϕA ) → [a]ψ to T !ϕ→[a]ψ , we must have T !ϕ→[a]ψ |= (π ∧ ϕA ) → [a]⊥. Kn Hence R!a (w) ! #= ∅. Let (ϕi ∧ T|= (π∧ϕA )→$a%¬ψ ¬(π ∧ ϕA )) → %a&* ∈ Kn

!

T !ϕ→[a]ψ . !

M!

For every w ∈ W , if |= ϕi ∧ w ¬(π ∧ ϕ ), then w ! ϕ , and as w ∈W A i (π∧ϕA )→$a%¬ψ

T|= Kn

and ϕi → %a&* ∈ Xa , we have Ra (w) #= ∅. If R!a (w) = ∅, beM!

cause |= S ∧E and R! is maximal, every M !! = %W!! , R!! & s.t. ! M !! |= S ∧ E is s.t. R!!a (w) = ∅. Then S , E |= &∈w & → [a]⊥. K n ! & → [a]⊥, and as ϕ → %a&* ∈ Xa , But then T |= i &∈w K n

! / W, a contradiction. T |= ¬( &∈w & ∧ ϕi ), and then w ∈ Kn ! Hence Ra (w) #= ∅. Finally, let Φ be of the form ϕ → %a&*, for some ϕ ∈ F. Then M ! = %W! , R! & for some M = %W, R& ∈ M s.t. W! = W and R! = R ∪ Rϕ,' , with a = {(w, w! ) : w! ∈ rt(w, ϕ → %a&*, M , M)} Rϕ,' a such that R! is minimal!w.r.t. R. M M! From W! = W, |= S . As R ⊆ R! , |= X . As far as S ∪ X ⊆ T !ϕ→$a%' , it is enough to show that M ! satisfies the added laws. M! M! By definition, |= ϕ → %a&*, and then |= (π ∧ ϕA ) → %a&* for every π ∈ IP(S ∧ ϕ). " ! ! If (ϕi ∧ π ∧ ϕA ) → [a](ψi ∨ π ! ∈IP(S ) (π ∧ ϕA )) ∈ A! ⊆atm(π ! )

T !ϕ→$a%' , then for every w ∈ W! , if w ! ϕi ∧ π ∧ ϕA , then M

M

w ! ϕi . Because |= ϕi → [a]ψi , we have |= ψ for all w! i M

!

w! ∈ W s.t. (w, w! ) ∈ Ra , and then |= ψi for every w! ∈ W! w! s.t. (w, w! ) ∈ R!a \ Rϕ,' . Now, given (w, w! ) ∈ Rϕ,' , we a a M!" ! ! (π ∧ ϕ ), and the result follows. have |= ! A π ∈IP(S ) w! A! ⊆atm(π ! !) Let (ϕi ∧ T|= (π∧ϕA )→[a]⊥ ¬(π ∧ ϕA )) → [a]ψi ∈ Kn

T !ϕ→$a%' . !

∈

For every w

W! ,

M!

if |= w

ϕi ∧

M

T|= (π∧ϕA )→[a]⊥ ¬(π ∧ ϕA ), then w ! ϕi , and as |= ϕi → Kn M [a]ψi , we have |= ψ for all w! ∈ W s.t. (w, w! ) ∈ Ra . Thus w! i M! |= ψi for every w! ∈ W! s.t. (w, w! ) ∈ R!a \ Rϕ,' . Now, a w! if w #! ϕ, then Rϕ,' = ∅ and the result follows. Othera wise, if w ! ϕ, then T #|= (π ∧ ϕ ) → [a]⊥, and then A K

(ϕi ∧

!

n

T|= (π∧ϕA )→[a]⊥ Kn

¬(π ∧ ϕA )) → [a]ψi has not been put

in T !ϕ→$a%' , a contradiction. Let now (π ∧ ϕA ∧ &) → [a]& ∈ T !ϕ→$a%' . For every w ∈ M!

M!

M

W! , if |= π ∧ ϕA ∧ &, then |= &, and then |= &. From w w w (π ∧ ϕA ∧ &) → [a]& ∈ T !ϕ→$a%' , we have T |= & → [a]⊥ Kn or T #|= & → [a]¬& and T |= & → [a]&. In both cases, K K n

n

M

M!

|= & for every w! ∈ Ra (w), and then |= & for every w! s.t. w! w! M!

(w, w! ) ∈ R! \ Rϕ,' . It remains to show that |= & for every a w! ! ϕ,' ! ! w ∈ W s.t. (w, w ) ∈ Ra . M!

Suppose #|= &. Then ¬& ∈ w! \w. From the construction of w! M ! , there is M !! = %W!! , R!! & ∈ M s.t. there is (u, v) ∈ R!!a M !!

M !!

and ¬& ∈ v \ u, i.e., |= & and |= ¬&. From (u, v) ∈ R!!a , we u v M !!

do not have T |= & → [a]⊥. From |= ¬&, we do not have Kn v T |= & → [a]&. Thus the algorithm has not put (π ∧ϕA ∧&) → Kn [a]& in T !ϕ→$a%' , a contradiction.

B Proof of Theorem 5 Definition 13 T is modular if and only if M = {M : M is a supra-model of T} = # ∅.

Lemma 1 Let Φ be a law. If T is modular and T ∪{Φ} |= ⊥, Kn ! then T Φ is modular. Proof: Let Φ be nonclassical. Suppose T !Φ is not modular. Then there is ϕ! ∈ F s.t. T !ϕ |= ϕ! and S ! #|= ϕ! , where S ! Kn CPL ! ! is static laws in T Φ . Suppose T #|= ϕ . Then we must have Kn ! ! ! ¬ϕ → [a]⊥ and T |= ¬ϕ → %a&*. T !Φ |= Φ Kn Kn Suppose Φ has the form ϕ → [a]ψ, for ϕ, ψ ∈ F. Then for all ϕ ∧ ¬ϕ! -contexts, as far as T !Φ |= (ϕ ∧ ¬ϕ! ) → [a]⊥, Kn ϕ! if and only if (ϕ ∧ ¬ϕ! ) → %a&* ∈ / T !Φ . Then T !Φ |= Kn ! ! S |= ϕ , a contradiction. CPL Suppose Φ is of the form ϕ → %a&*, for ϕ ∈ F. Then for all ϕ ∧ ¬ϕ! -contexts such that T !Φ |= (ϕ ∧ ¬ϕ! ) → %a&*, Kn ! ! T Φ |= (ϕ ∧ ¬ϕ ) → [a]⊥ is impossible as far as Ea− has Kn ϕ! if and only if S ! |= ϕ! , a been weakened. Then T !Φ |= Kn CPL contradiction. Hence we have T |= ϕ! . Because Φ is nonclassical, S ! = Kn ! S . Then T |= ϕ and S #|= ϕ! , and hence T is not modular. K CPL n

Let now Φ be some ϕ ∈ F. Suppose T !ϕ is not modular, i.e., there is ϕ!! ∈ F s.t. T !ϕ |= ϕ!! and S ! = S # ϕ #|= ϕ!! . K CPL n

From S ! #|= ϕ!! , there is v ∈ val(S ! ) s.t. v ! # ϕ!! . CPL !! If v ∈ val(S ), as T is modular, T*|= ϕ . From this and Kn

T !ϕ |= ϕ!! , we must have T !ϕ |= ¬ϕ!! → [a]⊥ and T !ϕ |= Kn Kn Kn !! ¬ϕ → %a&*. From the latter, we get T |= ¬ϕ!! → %a&*, Kn and from the first we have T |= ¬ϕ!! → [a]⊥. Putting both Kn !! results together we get T |= ϕ . As S #|= ϕ!! , we have a Kn CPL contradiction. If v ∈ / val(S ), then T !ϕ #|= ¬ϕ!! → %a&*, as no executabilKn !! ity for context ¬ϕ has been put into T !ϕ . Hence T !ϕ #|= ϕ!! , Kn a contradiction. Lemma 2 If Mbig = %Wbig , Rbig & is a model of T, then M for every M = %W, R& such that |= T there is a mini! mal (w.r.t. set inclusion) extension R ⊆ Rbig \ R such that M ! = %val(S ), R ∪ R! & is a model of T. Proof: Let Mbig = %Wbig , Rbig & be a model of T, and let M = M %W, R& be such that |= T. Consider M ! = %val(S ), R&. If M!

|= T, we have R! = ∅ ⊆ Rbig \ R that is minimal. Suppose M!

then #|= T. We extend M ! to a model of T that is a minimal M!

extension of M . As #|= T, there is v ∈ val(S ) \ W such that M!

M!

#|= T. Then there is Φ ∈ T such that #|= Φ. If Φ is some v v ϕ ∈ F, as v ∈ Wbig , Mbig is not a model of T. If Φ is of the form ϕ → [a]ψ, for ϕ, ψ ∈ F, there is v! ∈ val(S ) such that (v, v! ) ∈ Ra and v! #! ψ, a contradiction since Ra (v) = ∅. Let now Φ have the form ϕ → %a&* for some ϕ ∈ F. Then M!

M

M

big |= ϕ. As v ∈ Wbig , if #|= ϕ → %a&*, then #|= big T. Hence, v v Rbig a (v) #= ∅. Thus taking any (v, v! ) ∈ Rbig a gives us a minimal R! = {(v, v! )} such that M !! = %val(S ), R ∪ R! & is a model of T.

Lemma 3 Let T be modular, and Φ be a law. Then T |= Φ K $W,R%

if and only if every M ! = %val(S ), R! & such that |= R ⊆ R! is a model of Φ.

n

T and

Proof: M (⇒): Straightforward, as T |= Φ implies |= Φ for every M K n

M

such that |= T, in particular for those that are extensions of some model of T. (⇐): Suppose T #|= Φ. Then there is M = %W, R& such K M

n

M

that |= T and #|= Φ. As T is modular, the big model Mbig = %Wbig , Rbig & of T is a model of T. Then by Lemma 2 there is a minimal extension R! of R w.r.t. Rbig such that M ! = M %val(S ), R ∪ R! & is a model of T. Because #|= Φ, there is M w ∈ W such that #|= Φ. If Φ is some ϕ ∈ F or an effect law, w M!

any extension M ! of M is such that #|= Φ. If Φ is of the form w M

ϕ → %a&*, then |= ϕ and Ra (w) = ∅. As any extension of w M is such that (u, v) ∈ R! if and only if u ∈ val(S ) \ W, only worlds other than those in W get a new leaving arrow. Thus M! (R ∪ R! )a (w) = ∅, and then #|= Φ. w Lemma 4 Let T be modular and Φ a law. If M ! = M %val(S ! ), R! & is a model of T !Φ , then there is M = {M :|= T} ! ! s.t. M ∈ MΦ . M!

M!

Proof: Let M ! = %val(S ! ), R! & be such that |= T !Φ . If |= T, M

!

the result follows. Suppose #|= T. We analyze each case. Let Φ be of the form ϕ → [a]ψ, for ϕ, ψ ∈ F. Let M = {M : M = %val(S ), R&}. As T is modular, by Lemmas 2 and 3, M is non-empty and contains only models of T. Suppose M ! is not a minimal model of T !ϕ→[a]ψ , i.e., there is M !! such that M !! /M M ! for some M ∈ M. Then M ! and M !! differ only in the effect of a in a given ϕ-world, viz. a π ∧ ϕA -context, for some π ∈ IP(S ∧ ϕ) and ϕA = ! ! p ∧ pi ∈atm(π) ¬pi such that A ⊆ atm(π). pi ∈atm(π) i pi ∈A

M!

Because #|=

pi ∈A /

M !!

(π ∧ ϕA ) → %a&¬ψ, we must have |= M !!

(π ∧ ϕA ) → %a&¬ψ, and then #|= ϕ → [a]ψ. Hence M ! is minimal w.r.t. /M . When revising by an effect law, S ! = S . Hence taking the right R and Rϕ,¬ψ such that M = %val(S ), R& and a M M ! ϕ,¬ψ R = R \ Ra , for some Rϕ,¬ψ ⊆ {(w, w! ) :|= ϕ, |= a w w! ¬ψ and (w, w! ) ∈ Ra }, we have M ∈ M and then M ! ∈ M!ϕ→[a]ψ . Let Φ have the form ϕ → %a&*, for ϕ ∈ F. Let M = {M : M = %val(S ), R&}. As T is modular, by Lemmas 2 and 3, M is non-empty and contains only models of T. Suppose that M ! is not a minimal model of T !ϕ→$a%' , i.e., M !!

there is M !! such that |= T !ϕ→$a%' and M !! /M M ! for some M ∈ M. Then M ! and M !! differ only on the executability of a in a given ϕ-world, A -context, for ! i.e., a π ∧ ϕ! some π ∈ IP(S ∧ ϕ) and ϕA = pi ∈atm(π) pi ∧ pi ∈atm(π) ¬pi , pi ∈A

pi ∈A /

such that A ⊆ atm(π). This means M !! has no arrow leaving M !!

this π ∧ ϕA -world. Then |= M

!!

(π ∧ ϕA ) → [a]⊥, and hence

#|= ϕ → %a&*. Hence M is a minimal model of T !ϕ→$a%' w.r.t. /M . When revising by executability laws, S ! = S . Thus taking the right R and a minimal Rϕ,' such that M = %val(S ), R& a M and R! = R ∪ Rϕ,' , for some Rϕ,' ⊆ {(w, w! ) :|= a a w ϕ and w! ∈ rt(w, ϕ → %a&*, M , M)}, we get M ∈ M and then M ! ∈ M!ϕ→$a%' . Finally, let Φ be some ϕ ∈ F. Then M ! is such that for every w ∈ W! , if R!a (w) #= ∅, then w ∈ val(S ) and Ra (w) #= ∅ for every M = %W, R& ∈ M. Choosing the right M ∈ M the result follows. !

Proof of Theorem 5 Let T !Φ be the output of our algorithms on input theory T and law Φ. If T !Φ = T ∪ {Φ}, then T ∪ {Φ} #|= ⊥, and hence K M!

n

M

every M ! such that |= T !Φ is such that M ! ∈ M \ {M :#|= Φ} and the result follows. Suppose T∪{Φ} |= ⊥. From the hypothesis that T is modKn ular and Lemma 1, T ! is modular. Then M ! = %val(S ! ), R& is a model of T ! , by Lemma 2. From this and Lemma 3 the result follows.