A Note on Inference Systems for Update Semantics by Willem Groeneveld and Frank Veltman

Makoto Kanazawa Department of Cognitive and Information Sciences Faculty of Letters, Chiba University 1–33 Yayoi-cho, Inage-ku Chiba-shi, 263, Japan

               kanazawa@cogsci.l.chiba-u.ac.jp

May 19, 1998

Although Section 2 of the paper introduces many useful general techniques, there still seems to be a large gap between what has been learned about abstract update semantics and the results about the concrete systems of Veltman. In this note, I will make one proposal that I hope will narrow this gap.

One thing that makes it difficult to compare Veltman’s logic of might with a more general system is that the semantic clause for might is designed to apply only to a very special kind of model, with a distinguished bottom element. In Veltman’s model, this is ∅, which is the empty set of possible worlds. To study an abstract might logic, it is desirable to be able to interpret might in any model (or frame, in the authors’ terminology) that interprets atomic formulas as arbitray binary relations on the states. In fact, there is a natural way to achieve this, if we make the following simple observation. Let us recall Veltman’s semantic clause for might:

[[might φ]] = { ⟨σ, ∅⟩ | σ[[φ]] = ∅ } ∪ { ⟨σ, σ⟩ | σ[[φ]] ≠ ∅ }.  (1)

In Veltman’s model, ∅ is like a black hole: once you get there, there’s no way to get out of it. The interpretation of every formula loops at ∅. This is exactly like the dummy state ⊥ that Definition 13 of the paper introduces to turn a partial functional model into a total functional one. Applying this technique backwards, one sees that the submodel of Veltman’s model that you get by simply throwing away ∅ is equivalent to the original model. In this new model, all formulas denote partial functions. The semantic clause for might can then be simplified as follows:

[[might φ]] = { ⟨σ, σ⟩ | σ ∈ dom([[φ]]) }.  (2)

Clearly, the interpretation of might φ given by this definition in our new model is the same as the result of restricting the original interpretation of might φ to the states of the new model.

Unlike (1), (2) makes sense in all models, not only those in which atomic formulas denote partial functions. The operator might is now a simple domain operator. Since the clipped Veltman model is just one special model, the logical rules governing the new might operator should be a subset of the rules for might in Veltman’s logic.

Let our language consist of atomic formulas p_{0}, p_{1}, p_{2}, … and formulas of the form might p, where p is atomic. Prohibition to iterate might is not important here, since might might φ would be simply equivalent to might φ. By a translation to PDL by

tr(might φ) = (⟨tr(φ)⟩⊤)?,

one can see that the (global) Update-Test consequence relation

Γ ⊧ X ⇒ φ

between finite sets of sequents Γ and sequents X ⇒ φ in this language is recursive (see Kanazawa 1994). A complete calculus witnessing the recursive enumerability of this relation is not hard to find, and consists of the rules in Figure 1, in addition to Left Monotonicity and Cautious Cut. Let us call this calculus AML. Note that the rules

might-Contraction \frac{X_{1} might φ might φ X_{2} ⇒ ψ}{X_{1} might φ X_{2} ⇒ ψ}
might-Permutation \frac{X_{1} might φ might ψ X_{2} ⇒ χ}{X_{1} might ψ might φ X_{2} ⇒ χ}

are derivable in this calculus by might-Reflexivity, might-Monotonicity, and Cautious Cut.

might-Reflexivity \overline{X might φ ⇒ might φ}

might-Monotonicity \frac{X_{1} X_{2} ⇒ ψ}{X_{1} might φ X_{2} ⇒ ψ}

(might ⇒) \frac{X_{1} might φ φ X_{2} ⇒ ψ}{X_{1} φ X_{2} ⇒ ψ}  (⇒ might) \frac{X ⇒ φ}{X ⇒ might φ}

Figure 1: Rules for abstract might logic AML.

Since AML does not have idempotency for atomic formulas, Groeneveld’s general ‘Henkin-type’ method is not applicable here. There is a straightforward ‘representation’ method, however, that shows completeness. We let X (possibly with subscripts) range over finite sequences of formulas, and Y (possibly with subscripts) range over finite sequences of formulas of the form might p (mightformulas). We write Γ ⊢ X ⇒ φ to mean X ⇒ φ is derivable from Γ by AML.

Definition 1 Let Γ be any finite set of sequents. M_{Γ} is the model ⟨|M_{Γ}|, [[·]]_{M_{Γ}}⟩, where • |M_{Γ}| = { X | X is a finite sequence of formulas }.

• [[p]]_{M_{Γ}} = \{ ⟨X, X p Y ⟩ | \begin{matrix}Γ ⊢ X ⇒ might p ∧ \\ Y is a sequence of might-formulas \} ∪ \end{matrix} \{ ⟨X, X⟩ | Γ ⊢ X ⇒ p \}.

Lemma 2 For every finite sequence of formulas X and every formula φ,

⟨X, X⟩ ∈ [[φ]]_{M_{Γ}} iff Γ ⊢ X ⇒ φ.

Proof. For φ = p, it holds by definition. For φ = might p, this follows from (⇒ might) (for left-to-right) and the definition of M_{Γ}.

Unfortunately, the ‘Groeneveld equivalence’

M_{Γ}, X_{1} ⊧ X_{2} ⇒ φ iff Γ ⊢ X_{1} X_{2} ⇒ φ  (3)

does not always hold. (If Γ ⊬ X_{1} ⇒ might p, then M_{Γ}, X_{1} ⊧ p X_{2} ⇒ φ for all X_{2}, φ.) We do have one half of (3), however, and it is enough to prove M_{Γ} ⊧ Γ.

Lemma 3 Γ ⊢ X_{1} X_{2} ⇒ φ implies M_{Γ}, X_{1} ⊧ X_{2} ⇒ φ.

Proof. Induction on the length of X_{2}.

Induction Basis. X_{2} = Λ. By (one half of) Lemma 2.

Induction Step. X_{2} = ψ X_{3}. The assumption is

Γ ⊢ X_{1} ψ X_{3} ⇒ φ.  (4)

To show M_{Γ}, X_{1} ⊧ ψ X_{3} ⇒ φ, we show that for all Z such that X_{1} \underrightarrow{ψ} Z,

M_{Γ}, Z ⊧ X_{3} ⇒ φ. So assume X \underrightarrow{ψ} Z.

Case 1. ψ = p.

Case 1a. Z = X_{1} p Y. By (4) and might-Monotonicity, Γ ⊢ X_{1} p Y X_{3} ⇒ φ. By induction hypothesis, M_{Γ}, X_{1} p Y ⊧ X_{3} ⇒ φ.

Case 1b. Z = X_{1}. Then Γ ⊢ X_{1} ⇒ p by the construction of M_{Γ}. By (4) and Cautious Cut, Γ ⊢ X_{1} X_{3} ⇒ p. By induction hypothesis, M_{Γ}, X_{1} ⊧ X_{3} ⇒ p.

Case 2. φ = might p. Then Z = X_{1} and by Lemma 2, Γ ⊢ X_{1} ⇒ might p. By (4) and Cautious Cut, Γ ⊢ X_{1} X_{3} ⇒ φ. By induction hypothesis, M_{Γ}, X_{1} ⊧ X_{3} ⇒ φ.

Lemma 4 Γ ⊢ X ⇒ φ implies M_{Γ} ⊧ X ⇒ φ.

Proof. By Lemma 3 and Left Monotonicity.

Let us now show the converse of Lemma 4. Let X be a finite sequence of formulas. By the might-prefix of X, mprefix(X), we mean the longest prefix of X that entirely consists of might-formulas. By the fattening of X, fattening(X), we mean the result of replacing each occurrence of an atomic formula p by might p p.

Lemma 5 For every finite sequence of formulas X and every formula φ,

Γ ⊢ X ⇒ φ iff Γ ⊢ fattening(X) ⇒ φ.

Proof. By might-Monotonicity and (might ⇒). Lemma 6 For every finite sequence of atomic formulas X,

mprefix(fattening(X)) \underrightarrow{X} fattening(X)

in M_{Γ}. Proof. By might-Reflexivity and might-Monotonicity. Lemma 7 M_{Γ} ⊧ X ⇒ φ implies Γ ⊢ X ⇒ φ. Proof. By Lemmas 2 and 6, M_{Γ}, mprefix(fattening(X)) ⊧ X ⇒ φ implies Γ ⊢ fattening(X) ⇒ φ. By (one half of) Lemma 5, Γ ⊢ X ⇒ φ follows.

By Lemmas 4 and 7, we get Theorem 8 Let Γ be a finite set of sequents. For every sequent X ⇒ φ,

Γ ⊢ X ⇒ φ iff M_{Γ} ⊧ X ⇒ p.

\frac{X ⇒ φ}{X ⇒ might φ}  \frac{X φ ⇒ ⊥}{X might φ ⇒ ⊥}  \frac{X ⇒ ⊥}{X ⇒ ψ}
\frac{X ⇒ might ψ X ψ ⇒ φ}{X φ ⇒ might ψ}  \frac{X φ ⇒ ψ}{X might φ ⇒ ψ}

Figure 2: Rules for concrete might logic.

Having shown the completeness of AML, let us compare it to the mightrules for Update-Test Consequence given in the paper (Figure 2).

The first rule is simply our (⇒ might). The second and the third rules can be seen to be valid in the abstract setting if we set [[⊥]] = ∅, which is the interpretation we get by clipping the Veltman model. The last two rules are invalid in our abstract setting—it is easy to produce countermodels—and can be seen to depend on some special features of the concrete model. Our rules might-Reflexivity and might-Monotonicity are present in the concrete might logic in the form of general Reflexivity and Monotonicity. What about our rule (might ⇒)? I conjecture that this is an admissible, but underivable rule of the concrete might logic.

References

Groeneveld, Willem and Frank Veltman. 1994. Inference systems for update semantics. Institute for Logic, Language and Computation, Department of Philosophy, University of Amsterdam.

Kanazawa, Makoto. 1994. Completeness and decidability of the mixed style of inference with composition. In Paul Dekker and Martin Stokhof, eds., Proceedings of the Ninth Amsterdam Colloquium, pp. 377–391. Institute for Logic, Language and Computation, Department of Philosophy, University of Amsterdam.