Reasoning about Update Logic

Jan van Eijck^{1,2} & Fer-Jan de Vries^{1}

1CWI, P.O. Box 4079, 1009 AB Amsterdam, The Netherlands

2OTS, Trans 10, 3512 JK Utrecht, The Netherlands

Abstract

Logical frameworks for analysing the dynamics of information processing abound [4, 5, 8, 10, 12, 14, 20, 22]. Some of these frameworks focus on the dynamics of the interpretation process, some on the dynamics of the process of drawing inferences, and some do both of these. Formalisms galore, so it is felt that some conceptual streamlining would pay off.

This paper is part of a larger scale enterprise to pursue the obvious parallel between information processing and imperative programming. We demonstrate that logical tools from theoretical computer science are relevant for the logic of information flow. More specifically, we show that the perspective of Hoare logic [13, 18] can fruitfully be applied to the conceptual simplification of information flow logics.

Part one of this program consisted of the analysis of ‘dynamic interpretation’ in this way, using the example of dynamic predicate logic [10]; the results were published in [7]. The present paper constitutes the second part of the program, the analysis of ‘dynamic inference’. Here we focus on Veltman’s update logic [22].

Update logic is an example of a logical framework which takes the dynamics of drawing inferences into account by modelling information growth as discarding of possibilities. This paper shows how information logics like update logic can fruitfully be studied by linking their dynamic principles to static ‘correctness descriptions’.

Our theme is exemplified by providing a sound and complete Hoare/Pratt style deduction system for update logic. The Hoare/Pratt correctness statements use modal propositional dynamic logic as assertion language and connect update logic to the modal propositional logic S5.

The connection with S5 provides a clear link between the dynamic and the static semantics of update logic. The fact that update logic is decidable was noted already in [2]; the connection with S5 provides an alternative proof. The S5 connection can also be used for rephrasing the validity notions of update logic and for performing consistency checks.

In conclusion, it is argued that interpreting the dynamic statements of information logics as dynamic modal operators has much wider applicability. In fact, the method can be used to axiomatize quite a wide range of information logics.

1991 Mathematics Subject Classification: 03B65, 68Q55. 1991 CR Categories: F.3.1, I.2.4, I.2.7. Keywords and Phrases: dynamic interpretation, Hoare logic, dynamic logic, knowledge representation languages. Note: Accepted for publication in the Journal of Philosophical Logic.

1 Introduction

In the logical analysis of information and information processing two approaches can be distinguished. One approach takes the notion of truth as central. In this static approach growth of information by means of an utterance is viewed as adding the truth conditional content of the utterance to a given information state. The notion of inference is also defined in terms of truth conditions, as meaning inclusion in all models. The other approach takes information and information change as its central notions. A state of information is given by the set of possibilities which it leaves open. The nature of the possibilities varies of course with the theory of information at issue. In Lewis [17] the possibilities are possible answers to questions like ‘Who is the speaker?’, ‘What is the current topic of conversation?’, etcetera. In Heim [12] and Kamp [14] the possibilities are the discoure markers that are salient for anaphoric reference at the current stage of the discourse. In Groenendijk and Stokhof [10] they are possible assignments of values to variables. In Gärdenfors [8] the possibilities are (in the simplest version of the theory) the possible models of a given set of sentences. In Veltman [22] the possibilities are possible valuations for a set of proposition letters.

The first approach to information processing may be called static: evaluation at a given state is the basic notion. The second approach is dynamic in that information change is at the core of the approach. In the dynamic perspective, the meaning of a sentence is equated with its information change potential, with the effect that it has on a given state of information. Meanings are functions from information states to information states.

If one applies this to the semantics of natural language, (see for example Karttunen [15], Stalnaker [21], Kamp [14], Heim [12] and Barwise [1]) then the meaning of a text is the change it brings about in the information state of anyone who accepts the information conveyed by it. One perspective on dynamic semantics for natural language is to view this approach as a proposal to represent the meanings of natural language sentences not by means of formulae from static logic but by means of expressions from a dynamic action language. The action languages that have been proposed display an intriguing mix of features of programming languages and features of logical languages.

It has been demonstrated by example in [1] that under a dynamic regime compositional translations become feasible for fragments of natural language which include features that have resisted compositional treatment in the static representation approach (the most notable features being the handling of ‘donkey’ pronouns and pronominal binding across sentence boundaries).

The move from static logic to dynamic logic raises some interesting questions. In the first place, due to this transition we seem to have lost the deduction systems that static logical languages carry with them. This was noted by Barwise in [1], one of the first papers to propose an action language as representation medium for natural language meaning. Here the quest for a complete set of axioms for the dynamic inference notion that is engendered by the action language is put forward as an open problem. Next it can be asked what is the precise relation between the static semantics and the dynamic semantics of natural language. Are there systematic ways to derive the static meaning of a sentence from its dynamic representation?

These questions are intimately connected. Our contention is that they should be tackled together and moreover that theoretical computer science can guide the way. In computer science the view that the meaning of a program is a function from information states to information states is common ground. In the case of imperative programming languages this perspective has led to Hoare logic [13] as a successful means to construct deductive systems for reasoning about imperative programs.

To apply this to information processing in a very general sense, consider a reader of a text π as an agent who uses π to update her or his knowledge φ. Unless there is a consistency clash the agent will end up with more specific knowledge φ′. Taking our cue from Hoare logic we ask the following question. What is the weakest formula φ such that any knowledge implying φ remains consistent during the process of absorbing the information from text π? This weakest precondition φ for successful processing represents the static meaning of text π. It is the careful analysis of these weakest preconditions that leads to Hoare deduction systems which are sound and complete for a given dynamic semantics.

In this paper we will study Veltman’s [22] update logic from this perspective. The simplest version of update logic is exemplary for dynamic approaches to information. Information states are just sets of valuations to a set P of proposition letters, i.e. sets of subsets of P. Valuations to proposition letters might be called possible worlds, so information states are sets of possible worlds. The set W of all possible worlds is PP, the information state W is the state of complete ignorance (no possibility is excluded), for any w ∈ W, the state {w} is a state of complete information (all possibilities except w have been excluded), ∅ is the absurd information state (nothing is compatible with the information). A further simplifying assumption of Veltman’s update logic is the disregard of information revision (a central aspect of, e.g., Gärdenfors [8]).

Update logic can be used for the analysis of the epistemic sense of maybe or might. If I say Maybe it rains, or Mary might be at home then I wish to convey that the possibility of rain cannot be excluded on the basis of what I know, or that my evidence about Mary’s whereabouts does not exclude her being at home (she took a day off from work, or I see light at her window).

It is hoped that the simplicity of update logic will help us to clarify our more general points about the relation between static and dynamic concepts in theories of information processing. We are in fact convinced that the link between the statics and dynamics of update logic by means of a Hoare/Pratt style analysis can be generalised to more complex systems of information flow logic.

To end this introduction, here is an overview of the contents and structure of the paper. In Section 2 Veltman’s update logic is presented. Section 3 consists of a brief review of the tools from propositional modal logic that we will need. Section 4 contains the definition of validity for the assertion logic that is the foundation of our adaptation of Hoare/Pratt assertion reasoning to update semantics. The key notion of this section is the notion of a weakest precondition for a program of update logic. Section 5 links weakest preconditions to the next state conditions for update logic that were proposed by Van Benthem [2]. Section 6 contains the Hoare/Pratt calculus engendered by the notion of weakest preconditions of update programs. In Section 7 we prove the soundness and in Section 8 the completeness of the Hoare/Pratt calculus. In Section 9 we illustrate how the weakest preconditions analysis and the link to modal propositional logic can be used for reasoning about update logic. Section 10 demonstrates how weakest preconditions and the Hoare/Pratt calculus that is based on them can be used for reasoning about consistency of update programs. Finally, in Section 11 we wind up our story by connecting our program with related work and listing some directions for future research.

2 Update Logic: Syntax and Semantics

The characteristic feature of Veltman’s update logic (see Veltman [22]) is the epistemic modal operator might. Due to the presence of this operator the meanings of ‘update programs’ have to be phrased in terms of input information sets, and have to be phrased dynamically. The formulae of update logic have to be distinguished from the formulae of the static language used to make assertions about update logic. Because of the dynamic flavour of the former we will refer to these as ‘update programs’. We will see that sequential composition of update programs does not in general reduce to Boolean conjunction.

An update program π maps an information state I to a new information state [[π]](I). To see that might is the key feature, note that the semantics for the fragment of update logic without might can be given by means of a dynamic yes/no function for individual propositional valuations, which reduces the semantics immediately to ordinary static propositional logic.

Following Veltman [22] (and in fact, slightly simplifying his syntax), we can define the language of epistemic update logic over a set of proposition letters P as the smallest set L_{P} such that the following hold:

Definition 1 (Syntax of Update Logic L_{P})

1. ⊥ ∈ L_{P}.

2. If p ∈ P then p ∈ L_{P}.

3. If π and π′ ∈ L_{P}, then (π; π′) ∈ L_{P} , (π ∪ π′) ∈ L_{P}.

4. If π ∈ L_{P}, then ¬π ∈ L_{P} , might π ∈ L_{P}.

5. Nothing else is in L_{P}.

The semantics of L_{P} is given in terms of input-output behaviour. We take the set W of worlds over P to be the set PP. Any subset of W is an information state. Progams are interpreted as functions from information states to information states, i.e., as functions in PW → PW. The clauses are as follows:

Definition 2 (Semantics of Update Logic)

1. [[⊥]](I) = ∅.

2. [[p]](I) = I ∩ {w | p ∈ w}.

3. [[π; π′]](I) = [[π′]]([[π]](I)).

4. [[π ∪ π′]](I) = [[π]](I) ∪ [[π′]](I).

5. [[¬π]](I) = I − [[π]](I).

6. [[might π]](I) = \{ \begin{matrix}I & if [[π]](I) ≠ ∅, \\ ∅ & otherwise. \end{matrix}

We will follow the usual conventions and drop outermost parentheses as much as possible. Also, since sequential composition is associative we will write both π_{1}; (π_{2}; π_{3}) and (π_{1}; π_{2}); π_{3} as π_{1}; π_{2}; π_{3}.

Intuitively, a program of the form might π does not provide information about the world but about available information. A program might π is acceptable, given an information state I, if there is at least one world w ∈ I for which π is accepted in the sense that w ∈ [[π]](I). If such a w can be found, the output information state of might π is equal to its input information state; this agrees with the intuition that might π does not say anything at all about what the world is like. In the other case, i.e., the case were [[π]](I) = ∅, the output information state of might π equals ∅.

As was mentioned already, the might operator is the key feature of update logic. Yet another way to see this is to note that the semantic clause for might π introduces an element of non distributivity (this terminology is taken from [11]) into the semantics, in the sense that unions of input states do not distribute over output states: (1) does not in general hold.

[[π]](I) = ⋃_{i∈I}[[π]]({i}). (1)

More specifically, it does not in general hold that [[π]](I) ⊆ ⋃_{i∈I}[[π]]({i}). Counterexample: take π equal to might p and let I = {w, w′} with p ∈ w and p ∉ w′. Then [[might p]]({w}) ∪ [[might p]]({w′}) = {w}, but [[might p]](I) = I = {w, w′}.

On the other hand, a simple induction on the complexity of π shows that Lemma 1 holds for all π ∈ L_{P} and all information states I. In the terminology of Groenendijk & Stokhof [11]: epistemic update logic is eliminative.

Lemma 1 (Elimination Lemma) For all I: [[π]](I) ⊆ I.

3 Assertion Logic

The presence of the modal might operator in a dynamic setting which is otherwise fully propositional strongly suggests the use a modal propositional logic as language to make static assertions about update programs in, i.e., as assertion language. But we also want to be able to talk about execution results, so we add the update programs themselves as a second kind of modality. The syntax of our assertion language mal_{P} is as follows:

Definition 3 (Syntax of mal_{P})

1. ⊥ ∈ mal_{P}.

2. If p ∈ P then p ∈ mal_{P}.

3. If φ, ψ ∈ mal_{P}, then (φ ∧ ψ), ¬φ, ◇φ ∈ mal_{P}.

4. If φ ∈ mal_{P} and π ∈ L_{P} then ⟨π⟩φ ∈ mal_{P}.

5. Nothing else is in mal_{P}.

As is customary, we abbreviate ¬⊥ as ⊤, ¬(¬φ ∧ ¬ψ) as (φ ∨ ψ), ¬(φ ∧ ¬ψ) as (φ → ψ), ¬◇¬φ as □φ, ¬⟨π⟩¬φ as [π]φ, Also, we omit outermost parentheses for readability. We will refer to propositional modal logic (which is defined by omitting clause 4 from the definition of mal_{P}) as ml_{P}.

We consider information states I ∈ PW as universal Kripke models; thus, I is considered as the Kripke model with accessibility relation I × I. Recall from the literature (see e.g. [9]) that the modal logic determined by the class of finite universal frames is S5. Moreover, for any finite universal model (a universal frame with valuations assigned to all of its worlds) there is a finite subset I of W validating the same formulae. I can be got by throwing away the extra copies of the worlds with identical valuations: because of the universal accessibility this makes no difference to validity.

It is convenient to define the interpretation of an mal_{P} formula with respect to an information state.

Definition 4 (Interpretation of φ with respect to I)

1. ||⊥||_{I} = ∅.

2. ||p||_{I} = {w ∈ I | p ∈ w}.

3. ||φ ∧ ψ||_{I} = ||φ||_{I} ∩ ||ψ||_{I}.

4. ||¬φ||_{I} = I − ||φ||_{I}.

5. ||◇φ||_{I} = \{ \begin{matrix}I & if ||φ||_{I} ≠ ∅, \\ ∅ & otherwise. \end{matrix}

6. ||⟨π⟩φ||_{I} = ||φ||_{[[π]](I)}. We can now can define the notion I, w ⊢⊢ φ (world w forces formula φ in information state I) as w ∈ ||φ||_{I}.

In Hoare style reasoning about update logic the notions of relativisation and localisation of modal formulae play an important role. Localisations of modal formulae are defined in Kracht [16]. If φ, ψ are in mal_{P}, then φ↓ψ, the localisation of φ to ψ, is given by the following definition. Definition 5 (Localised modal formulae φ↓ψ)

\begin{aligned}⊥↓ψ & = & ⊥ \\ p↓ψ & = & p ∧ ψ \\ (φ_{1} ∧ φ_{2})↓ψ & = & (φ_{1}↓ψ) ∧ (φ_{2}↓ψ) \\ (¬φ)↓ψ & = & ψ ∧ ¬(φ↓ψ) \\ (◇φ)↓ψ & = & ψ ∧ ◇(ψ ∧ (φ↓ψ)). \\ (⟨π⟩φ)↓ψ & = & ψ ∧ ⟨π⟩(ψ ∧ (φ↓ψ)). \end{aligned}

Localisation is closely related to the usual notion of a relativised modal formula. Definition 6 (Relativised modal formulae φ^{ψ})

\begin{aligned}⊥^{ψ} & = & ⊥ \\ p^{ψ} & = & ψ → p \\ (φ_{1} ∧ φ_{2})^{ψ} & = & φ_{1}^{ψ} ∧ φ_{2}^{ψ} \\ (¬φ)^{ψ} & = & ¬(φ^{ψ}) \\ (◇φ)^{ψ} & = & ◇(ψ ∧ φ^{ψ}). \\ (⟨π⟩φ)^{ψ} & = & ⟨π⟩(ψ ∧ φ^{ψ}). \end{aligned}

The connection between the two notions is given by the following lemma. Lemma 2 (Van Benthem) φ↓ψ iff φ^{ψ} ∧ ψ. Proof: Induction on the structure of φ. For example, in the case of negation the reasoning is as follows.

¬φ↓ψ = ↓ def  ψ ∧ ¬(φ↓ψ)
= ind hyp  ψ ∧ ¬(φ^{ψ} ∧ ψ)
= prop logic ψ ∧ ¬(φ^{ψ})
= ↓ def  ψ ∧ (¬φ)^{ψ}.

Given this connection, the following lemma will not come as a surprise (the first item is from the modal folklore, the second from Kracht [16]). Lemma 3 (Relativisation and Localisation)

1. ||φ^{ψ}||_{I} = (I − ||ψ||_{I}) ∪ ||φ||_{||ψ||_{I}}.

2. ||φ↓ψ||_{I} = ||φ||_{||ψ||_{I}}. Proof: Both assertions are proved by induction on the complexity of φ.

4 Correctness Statements for Update Logic

Once we have a notion of validity for assertions, the assertion language can be used to make correctness assertions about update logic. Here is the validity notion. Definition 7 Assume φ ∈ mal_{P}. Then ⊧ φ if for all I ⊆ W, I = ||φ||_{I}. Now we immediately have the following. Lemma 4 ⊧ φ ↔ ⟨π⟩ψ iff for all I: ||φ||_{I} = ||ψ||_{[[π]](I)}. Proof: Immediate from Definition 4 and Definition 7. Note that it follows from Lemma 4 that ⊧ φ ↔ ⟨π⟩⊤ iff for all I: ||φ||_{I} = [[π]](I). The correctness statements suggest the following notion of weakest precondition for update logic. Definition 8 A formula φ ∈ ml_{P} is a weakest precondition (WP) of the program π ∈ L_{P} and the formula ψ ∈ mal_{P} if for all I: ||φ||_{I} = ||ψ||_{[[π]](I)}.

It is not obvious at first sight that WPs of an L_{P} program π and an mal_{P} formula ψ always exist (as formulae of ml_{P}). We will demonstrate now that they do, by inductively defining a function wp(π, ψ), of which we will show that it expresses a WP of π and ψ. Definition 9 (wp)

1. wp(⊥, ψ) = ⊥.

2. wp(p, ψ) = ψ↓p.

3. wp(π_{1}; π_{2}, ψ) = wp(π_{1}, wp(π_{2}, ψ)).

4. wp(π_{1} ∪ π_{2}, ψ) = ψ↓(wp(π_{1}, ⊤) ∨ wp(π_{2}, ⊤)).

5. wp(¬π, ψ) = ψ↓¬wp(π, ⊤).

6. wp(might π, ψ) = ◇wp(π, ⊤) ∧ ψ. An easy induction shows that wp(π, ψ) ∈ ml_{P}, for π ∈ L_{P} and ψ ∈ mal_{P}. Lemma 5 shows that the function wp(π, ψ) does indeed express a WP of a program π and a modal propositional formula ψ. Lemma 5 (wp adequacy) ||wp(π, ψ)||_{I} = ||ψ||_{[[π]](I)}. Proof: We prove the claim with induction on the structure of π.

||wp(⊥, ψ)||_{I} = wp def  ||⊥||_{I}
= || ||_{I} def ∅
= [[ ]] def  ||ψ||_{[[⊥]](I)}.
||wp(p, ψ)||_{I} = wp def  ||ψ↓p||_{I}
= loc lemma ||ψ||_{||p||_{I}}
= [[ ]] def  ||ψ||_{[[p]](I)}.

||wp(π_{1}; π_{2}, ψ)||_{I} = wp def ||wp(π_{1}, wp(π_{2}, ψ))||_{I}
= ind hyp ||wp(π_{2}, ψ)||_{[[π_{1}]](I)}
= ind hyp ||ψ||_{[[π_{2}]]([[π_{1}]](I))}
= [[ ]] def ||ψ||_{[[π_{1};π_{2}]](I)}.
||wp(π_{1} ∪ π_{2}, ψ)||_{I} = wp def  ||ψ↓(wp(π_{1}, ⊤) ∨ wp(π_{2}, ⊤))||_{I}
= loc lemma  ||ψ||_{||wp(π_{1},⊤)∨wp(π_{2},⊤)||_{I}}
= ind hyp , || ||_{I} def ||ψ||_{[[π_{1}]](I)∪[[π_{2}]](I)}
= [[ ]] def  ||ψ||_{[[π_{1}∪π_{2}]](I)}.
||wp(¬π, ψ)||_{I} = wp def  ||ψ↓¬wp(π, ⊤)||_{I}
= loc lemma  ||ψ||_{||¬wp(π,⊤)||_{I}}
= || ||_{I} def  ||ψ||_{I−||wp(π,⊤)||_{I}}
= ind hyp, || ||_{I} def ||ψ||_{I−[[π]](I)}
= [[ ]] def  ||ψ||_{[[¬π]](I)}.
||wp(might π, ψ)||_{I} = wp def  ||◇wp(π, ⊤) ∧ ψ||_{I}
= || ||_{I} def  ||◇wp(π, ⊤)||_{I} ∩ ||ψ||_{I}
= ◇ def in S5  \{ \begin{matrix}||ψ||_{I} & if ||wp(π, ⊤)||_{I} ≠ ∅, \\ ∅ & otherwise \end{matrix}
= ind hyp, || ||_{I} def \{ \begin{matrix}||ψ||_{I} & if [[π]](I) ≠ ∅, \\ ∅ & otherwise \end{matrix}
= [[ ]] def  ||ψ||_{[[might π]](I)}.

This completes the proof of the lemma. Lemma 6

1. ||wp(π, ⊤)||_{I} = [[π]](I).

2. ⊧ φ ↔ ⟨π⟩⊤ iff for all I: ||wp(π, ⊤)||_{I} = ||φ||_{I}. Proof: The first item:

||wp(π, ⊤)||_{I} = wp adeq ||⊤||_{[[π]](I)}
= || ||_{I} def [[π]](I).

The second item follows from Lemma 4 and the first item. Lemma 7 ||wp(π, ψ)||_{I} = ||ψ↓wp(π, ⊤)||_{I}. Proof:

||wp(π, ψ)||_{I} = wp adeq  ||ψ||_{[[π]](I)}
= Lemma 6 ||ψ||_{||wp(π,⊤)||_{I}}
= loc lemma ||ψ↓wp(π, ⊤)||_{I}.

5 Weakest Preconditions Versus Next State Conditions

In [2] and [3], Van Benthem has studied update logic by looking at update programs π as functions of the form λI · NEXT STATE(I, π), were NEXT STATE is the function producing the information state which results from processing π in information state I, i.e., π is considered as λI · [[π]](I). The investigation in [2, 3] was carried out in semantic terms, without reference to a specific assertion language, but it can easily be transposed in a setting of assertions from modal propositional logic. Some illuminating conversations between Johan van Benthem and the authors, backed up by an exchange of letters of explanation and consecutive drafts of the present paper, have fully cleared up the connection between his perspective and ours. His generous help in clarifying the issues raised in this section is herewith gratefully acknowledged.

Definition 10 A formula ψ ∈ ml_{P} is a next state condition (NSC) of the formula φ ∈ ml_{P} and the program π ∈ L_{P} if for all I: ||ψ||_{I} = [[π]](||φ||_{I}).

The following function nsc is a reformulation in modal logic of Van Benthem’s characterisation of the next state function.

Definition 11 (nsc)

1. nsc (φ, ⊥) = ⊥.

2. nsc (φ, p) = p ∧ φ.

3. nsc (φ, π_{1}; π_{2}) = nsc (nsc (φ, π_{1}), π_{2}).

4. nsc (φ, π_{1} ∪ π_{2}) = nsc (φ, π_{1}) ∨ nsc (φ, π_{2}).

5. nsc (φ, ¬π) = ¬nsc (φ, π) ∧ φ.

6. nsc (φ, might π) = ◇nsc (φ, π) ∧ φ.

Lemma 8 (nsc adequacy) ||nsc (φ, π)||_{I} = [[π]](||φ||_{I}).

Induction on the structure of π.

||nsc (φ, ⊥)||_{I} = nsc def ||⊥||_{I}
= || ||_{I} def ∅
= [[ ]] def  [[⊥]](||φ||_{I}).
||nsc (φ, p)]_{I} = nsc def ||p ∧ ψ||_{I}
= || ||_{I} def ||p||_{I} ∩ ||φ||_{I}
= [[ ]] def  [[p]](||φ||_{I}).
||nsc (φ, π_{1}; π_{2})||_{I} = nsc def ||nsc (nsc (φ, π_{1}), π_{2})||_{I}
= ind hyp [[π_{2}]](||nsc (φ, π_{1})||_{I})
= ind hyp [[π_{2}]]([[π_{1}]](||φ||_{I}))
= [[ ]] def [[π_{1}; π_{2}]](||φ||_{I}).
||nsc (φ, π_{1} ∪ π_{2})||_{I} = nsc def ||nsc (φ, π_{1}) ∨ nsc (φ, π_{2})||_{I}
= ind hyp [[π_{1}]](||φ||_{I}) ∪ [[π_{2}]](||φ||_{I})
= [[ ]] def [[π_{1} ∪ π_{2}]](||φ||_{I}).

||nsc (φ, ¬π)||_{I} = nsc def  ||¬nsc (φ, π) ∧ φ||_{I}
= || ||_{I} def  (I − ||nsc (φ, π)||_{I}) ∩ ||φ||_{I}
= ind hyp  (I − [[π]](||φ||_{I})) ∩ ||φ||_{I}
= elim lemma (||φ||_{I} − [[π]](||φ||_{I})) ∩ ||φ||_{I}
= [[ ]] def  [[¬π]](||φ||_{I}).
||nsc (φ, might π)||_{I} = nsc def  ||◇nsc (φ, π) ∧ φ||_{I}
= || ||_{I} def  ||◇nsc (φ, π)||_{I} ∩ ||φ||_{I}
= ◇ def in S5 \{ \begin{matrix}||φ||_{I} & if ||nsc (φ, π)||_{I} ≠ ∅, \\ ∅ & otherwise \end{matrix}
= ind hyp  \{ \begin{matrix}||φ||_{I} & if [[π]](||φ||_{I}) ≠ ∅, \\ ∅ & otherwise \end{matrix}
= [[ ]] def  [[might π]](||φ||_{I}).

This completes the proof of the lemma. Lemma 9 ||nsc (⊤, π)||_{I} = [[π]](I). Proof:

||nsc (⊤, π)||_{I} = nsc adeq [[π]](||⊤||_{I})
= || ||_{I} def [[π]](I).

The following theorem gives the precise connections between WPs and NSCs. Theorem 10

1. ||nsc (φ, π)||_{I} = ||wp(π, ⊤)↓φ||_{I}.

2. ||wp(π, ψ)||_{I} = ||ψ↓nsc (⊤, π)||_{I}. Proof: The first item:

nsc (φ, π)||_{I} = nsc adeq [[π]](||φ||_{I})
= Lemma 6 ||wp(π, ⊤)||_{||φ||_{I}}
= loc lemma ||wp(π, ⊤)↓φ||_{I}.

The second item:

||wp(π, ψ)||_{I} = wp adeq  ||ψ||_{[[π]](I)}
= Lemma 9 ||ψ||_{||nsc (⊤,π)||_{I}}
= loc lemma ||ψ↓nsc (⊤, π)||_{I}.

6 A Hoare/Pratt Calculus for Update Logic

We now present the axioms and rules of a deduction system for update logic based on the concept of WPs from Section 4. We start with the axiom schemata for propositional logic. A 1 φ → (ψ → φ). A 2 (φ → (ψ → χ)) → ((φ → ψ) → (φ → χ)). A 3 (¬φ → ¬ψ) → (ψ → φ). Next, we take the axiom schemata of S5 modal logic for the □ modality. A 4 □(φ → ψ) → (□φ → □ψ). A 5 □φ → φ. A 6 □φ → □□φ. A 7 ◇□φ → φ. These are the propositional S5 modalities. Here are the axiom schemata for the program modalities. A 8 ⊥ ↔ ⟨⊥⟩φ. A 9 φ↓p ↔ ⟨p⟩φ. A 10 ⟨π_{1}⟩⟨π_{2}⟩φ ↔ ⟨π_{1}; π_{2}⟩φ. A 11 φ↓(⟨π_{1}⟩⊤ ∨ ⟨π_{2}⟩⊤) ↔ ⟨π_{1} ∪ π_{2}⟩φ. A 12 φ↓[π]⊥ ↔ ⟨¬π⟩φ. A 13 (◇⟨π⟩⊤ ∧ φ) ↔ ⟨mightπ⟩φ. The rules of inference are as follows. R 1 (Necessitation for □) Conclude from ⊢ φ to ⊢ □φ. R 2 (Necessitation for program modalities) For every program π of update logic: conclude from ⊢ φ to ⊢ [π]φ. R 3 (Modus Ponens) Conclude from ⊢ φ → ψ and ⊢ φ to ⊢ ψ. The notion of theoremhood in the calculus is standard. Definition 12 Formula φ is a theorem of the calculus, notation ⊢ φ, if φ fits one of the axiom schemata or φ follows from theorems in the calculus by an application of one of the inference rules. Here is an example of a derived schema. Proposition 11 For every update program π, the K schema is derivable: ⊢ ([π](φ → ψ) ∧ [π]φ) → [π]ψ. Proof: Induction on the complexity of π.

7 Soundness of the Calculus

To prove that the calculus is sound, we have to prove that if ⊢ φ, then φ is valid in the sense defined in Section 4. As usual, soundness is proved by induction on the length of the derivation of φ. For this, we have to check that every axiom of the calculus is valid and that the rules of the calculus preserve validity.

Theorem 12 (Soundness) For all φ ∈ mal_{P}: If ⊢ φ then ⊧ φ.

Proof: First, it is obvious that the axiom schemata of propositional logic are valid. Next, observe that it follows from the definition of || ||_{I} that

||□φ||_{I} = \{ \begin{matrix}I & if ||φ||_{I} = I, \\ ∅ & otherwise. \end{matrix}

For the validity of Axiom 4 we have to show (2).

For all I, ||□(φ → ψ) → (□φ → □ψ)||_{I} = I. (2)

This is equivalent to (3).

For all I, ||□(φ → ψ)||_{I} ⊆ ||□φ → □ψ||_{I}. (3)

Two cases. If ||φ → ψ||_{I} ≠ I, then ||□(φ → ψ)||_{I} = ∅, and (3) trivially holds. Assume therefore that ||φ → ψ||_{I} = I. This is equivalent to ||φ||_{I} ⊆ ||ψ||_{I} (∗). Now if ||φ||_{I} ≠ I, then ||□φ||_{I} = ∅ and ||□φ||_{I} ⊆ ||□ψ||_{I}, in other words ||□φ → □ψ||_{I} = I, and (3) holds. If, on the other hand, ||φ||_{I} = I, then by ∗, ||ψ||_{I} = I, and again (3) holds because ||□φ||_{I} ⊆ ||□ψ||_{I}.

For Axiom 5, observe that ||□φ → φ||_{I} = I iff ||□φ||_{I} ⊆ ||φ||_{I} iff it holds that if ||φ||_{I} = I then I ⊆ ||φ||_{I}, which is always true.

For Axiom 6, we have to show that ||□φ → □□φ||_{I} = I, or equivalently, ||□φ||_{I} ⊆ ||□□φ||_{I}. If ||φ||_{I} ≠ I then ||□φ||_{I} = ∅, and the claim holds. If ||φ||_{I} = I then ||□φ||_{I} = I, and so ||□□φ||_{I} = I, and the the claim holds in this case too.

For Axiom 7, observe: ||◇□φ → φ||_{I} = I iff ||◇□φ||_{I} ⊆ ||φ||_{I} iff if ||□φ||_{I} ≠ ∅ then I ⊆ ||φ||_{I} iff if ||φ||_{I} = I then I ⊆ ||φ||_{I} iff true.

Axiom 8: ||⊥ ↔ ⟨⊥⟩φ||_{I} = I iff ||⊥||_{I} = ||⟨⊥⟩φ||_{I} iff ∅ = ||⟨⊥⟩φ||_{I} iff true.

The reasoning for Axiom 9: ||φ↓p ↔ ⟨p⟩φ||_{I} = I iff ||φ↓p||_{I} = ||⟨p⟩φ||_{I} iff (Lemma 3) true.

Axiom 10:

||⟨π_{1}⟩⟨π_{2}⟩φ ↔ ⟨π_{1}; π_{2}⟩φ||_{I} = I iff ||⟨π_{1}⟩⟨π_{2}⟩φ||_{I} = ||⟨π_{1}; π_{2}⟩φ||_{I} iff ||⟨π_{2}⟩φ||_{[[π_{i}]]I} = ||⟨π_{1}; π_{2}⟩φ||_{I} iff ||φ||_{[[π_{2}]]([[π_{i}]]I)} = ||⟨π_{1}; π_{2}⟩φ||_{I} iff true.

Axiom 11:

||φ↓(⟨π_{1}⟩⊤ ∨ ⟨π_{2}⟩⊤) ↔ ⟨π_{1} ∪ π_{2}⟩φ||_{I} = I iff ||φ↓(⟨π_{1}⟩⊤ ∨ ⟨π_{2}⟩⊤)||_{I} = ||⟨π_{1} ∪ π_{2}⟩φ||_{I} iff ||φ||_{||⟨π_{1}⟩⊤∨⟨π_{2}⟩⊤||_{I}} = ||⟨π_{1} ∪ π_{2}⟩φ||_{I} iff ||φ||_{||⟨π_{1}⟩⊤||_{I}∪||⟨π_{2}⟩⊤||_{I}} = ||⟨π_{1} ∪ π_{2}⟩φ||_{I} iff ||φ||_{[[π_{1}]]I∪[[π_{2}]]I} = ||⟨π_{1} ∪ π_{2}⟩φ||_{I} iff true.

Axiom 12:

||φ↓[π]⊥ ↔ ⟨¬π⟩φ||_{I} = I iff ||φ↓[π]⊥||_{I} = ||⟨¬π⟩φ||_{I} iff ||φ||_{[π]⊥||_{I}} = ||⟨¬π⟩φ||_{I} iff ||φ||_{I−[[π]]I} = ||⟨¬π⟩φ||_{I} iff true.

Axiom 13:

||(◇⟨π⟩⊤ ∧ φ) ↔ ⟨mightπ⟩φ||_{I} = I iff ||◇⟨π⟩⊤ ∧ φ||_{I} = ||⟨mightπ⟩φ||_{I} iff ||◇⟨π⟩⊤||_{I} ∩ ||φ||_{I} = ||⟨mightπ⟩φ||_{I} iff if ||⟨π⟩⊤||_{I} ≠ ∅ then ||⟨mightπ⟩φ||_{I} = ||φ||_{I}, otherwise ||⟨mightπ⟩φ||_{I} = ∅. iff if [[π]]I ≠ ∅ then ||⟨mightπ⟩φ||_{I} = ||φ||_{I}, otherwise ||⟨mightπ⟩φ||_{I} = ∅. iff (semantic clause for mightπ) true.

This establishes that all axiom schemata are valid. We now check the validity of the rules of inference.

Rule 1:

Observe that if for all I, ||φ||_{I} = I, then for all I, ||□φ||_{I} = I.

Rule 2:

If for all I, ||φ||_{I} = I, then for all I, ||[π]φ||_{I} = (I − [[π]]I) ∪ ||φ||_{[[π]]I} = (I − [[π]]I) ∪ [[π]]I = I.

Rule 3:

If for all I, ||φ → ψ||_{I} = I (∗) and for all I, ||φ||_{I} = I (∗∗), then for all I, ||φ|||I ⊆ ||ψ||_{I} (from ∗) and thus, by ∗∗, for all I, I ⊆ ||ψ||_{I}, i.e., ||ψ||_{I} = I.

This concludes the checking of the inference rules and the soundness proof.

8 Completeness of the Calculus

Theorem 13 The calculus is complete, i.e., for all mal_{P} formulae φ, if ⊧ φ then ⊢ φ.

Proof: First observe that the following translation function ^{∗} from mal_{P} to ml_{P} preserves validity.

\begin{aligned}(φ ∧ ψ)^{∗} & = & φ^{∗} ∧ ψ^{∗} \\ (¬φ)^{∗} & = & ¬φ^{∗} \\ (◇φ)^{∗} & = & ◇φ^{∗} \\ (⟨⊥⟩φ)^{∗} & = & ⊥ \\ (⟨p⟩φ)^{∗} & = & φ^{∗}↓p \\ (⟨π_{1}; π_{2}⟩φ)^{∗} & = & (⟨π_{1}⟩⟨π_{2}⟩φ)^{∗} \\ (⟨π_{1} ∪ π_{2}⟩φ)^{∗} & = & φ^{∗}↓((⟨π_{1}⟩⊤)^{∗} ∨ (⟨π_{2}⟩⊤)^{∗}) \\ (⟨¬π⟩φ)^{∗} & = & φ^{∗}↓([π]⊥)^{∗} \\ (⟨mightπ⟩φ)^{∗} & = & (◇(⟨π⟩⊤)^{∗} ∧ φ^{∗}) \end{aligned}

Thus, it follows from ⊧ φ that ⊧ φ^{∗}. Next, use the completeness of S5 to conclude from ⊧ φ^{∗} that ⊢ φ^{∗}. Finally, note that the translation steps and their inverses in the definition of ^{∗} are licensed by Schema 8 through Schema 13 of the calculus. This allows us to conclude from ⊢ φ^{∗} that ⊢ φ.

9 Reasoning about Update Logic via S5

Just for the record we mention a fact about update logic which follows immediately from our ‘reduction to S5’ (but note that this fact was already proved in [2]).

Theorem 14 Update logic is decidable.

Proof: The decision problem for update logic is the question: which π ∈ L_{P} have the property that they are valid (accepted in every input state I)? In other words: which π have the property that for all I it holds that [[π]](I) = I? The decision procedure for π is as follows. Use the definition of wp to find wp(π, ⊤). By Lemma 6 we know that [[π]](I) = ||wp(π, ⊤)||_{I}, so the decision problem for π reduces to the question whether wp(π, ⊤) is S5-valid. Use the decision procedure for S5 to settle this question.

In update logic there is a distinction between acceptable and accepted information, witness the following definition.

Definition 13

1. A program π is accepted in I if I = [[π]](I).

2. A program π is acceptable in I if [[π]](I) ≠ ∅.

It is the universal version of the first of these which is taken as the notion for universal validity, but one might consider the universal version of the second one just as well.

Definition 14

1. A program π is always accepted (or valid) if for all I it holds that [[π]](I) = I.

2. A program π is always acceptable if for all I ≠ ∅ it holds that [[π]](I) ≠ ∅.

An obvious question suggests itself: are the notions of being always accepted and being always acceptable equivalent? Using the S5 connection it is easy to see that they are not and to clarify the relation between them . We need not concern ourselves with the case of I = ∅, for the elimination lemma forces [[π]](∅) = ∅ for every π. Thus, there is no harm in adopting the usual convention that S5 models have a non-empty set of worlds. The ‘static’ version of π is always accepted is (4).

S5 ⊧ wp(π, ⊤). (4)

The ‘static’ version for π is always acceptable, on the other hand, is (5). Note that this translation hinges on the assumption of non-emptyness of S5 models.

S5 ⊧ ◇wp(π, ⊤). (5)

So the notion of being always acceptable is decidable as well, but it does not coincide with the notion of being always accepted. Indeed, we have that S5 ⊧ φ implies S5 ⊧ ◇φ, because of the reflexivity of accessibility, so (4) implies (5), but not the other way around. Take φ equal to ◇p → p for a simple counterexample. We have S5 |̸= ◇p → p (take a non-p world in a model containing both p and non-p worlds), but S5 ⊧ ◇(◇p → p). To see this latter fact, take an arbitrary w in an arbitrary universal S5 model I. If there are no p worlds, then I, w ⊢⊢ ◇(◇p → p); if there are p worlds, then there is a p world w′ for which I, w′ ⊧ ◇p → p, so by the fact that accessibility is universal again I, w ⊢⊢ ◇(◇p → p). Note, by the way, that ◇(◇p → p) is the modal counterpart of a predicate logical sentence that philosophical logicians sometimes refer to as ‘Plato’s principle’: ∃x(∃xP x → P x).

The S5 counterexample can be transposed to update logic, of course: p ∪ ¬might p is an example of a program which is always acceptable but not always accepted.

For a next illustration of reasoning about update logic via S5 we take a quick look at valid consequence in update logic. In his paper [22] Veltman discusses various notions of valid consequence. He distinguishes the following three definitions.

Definition 15

1. π_{1} ⊧_{1} π_{2} if for all I it holds that [[π_{1}]](I) = I implies [[π_{2}]](I) = I.

2. π_{1} ⊧_{2} π_{2} if for all I it holds that [[π_{1}]](I) = [[π_{2}]]([[π_{1}]](I)).

3. π_{1} ⊧_{3} π_{2} if [[π_{1}]](W) = [[π_{2}]]([[π_{1}]](W)).

The following proposition reduces these notions to S5.

Proposition 15

1. π_{1} ⊧_{1} π_{2} iff S5 ⊢ □wp(π_{1}, ⊤) → □wp(π_{2}, ⊤).

2. π_{1} ⊧_{2} π_{2} iff S5 ⊢ wp(π_{1}, ⊤) ↔ wp(π_{1}; π_{2}, ⊤).

3. π_{1} ⊧_{3} π_{2} iff S5 ⊢ (∧∧◇φ_{i}) → (wp(π_{1}, ⊤) ↔ wp(π_{1}; π_{2}, ⊤)), where the φ_{i} are all conjunctions of the form (¬)p_{1} ∧ ⋯ ∧ (¬)p_{n}, with p_{1}, …, p_{n} the list of proposition letters occurring in π_{1} or π_{2}.

Proof: The first item:

For all I: [[π_{1}]](I) = I implies [[π_{2}]](I) = I

iff for all I: if for all w ∈ I: I, w ⊢⊢ wp(π_{1}, ⊤) then for all w ∈ I: I, w ⊢⊢ wp(π_{2}, ⊤)
iff for all I: I ⊧ □wp(π_{1}, ⊤) → □wp(π_{2}, ⊤)
iff S5 ⊢ □wp(π_{1}, ⊤) → □wp(π_{2}, ⊤).

The second item is immediate from the definitions of the validity notions, the wp adequacy lemma and the completeness of S5.

For the third item, note that I ⊧ ∧∧◇φ_{i} (where ⊧ denotes S5 validity) for precisely those information sets I that express total ignorance with respect to all proposition letters in π_{1} and π_{2}, i.e., for the sets I that are indistinguishable from W as far as π_{1} and π_{2} are concerned. The S5 formula expresses that for such I, all worlds in [[π_{1}; π_{2}]](I) are worlds in [[π_{2}]](I) and vice versa. This is precisely what the validity notion ⊧_{3} expresses.

As Willem Groeneveld pointed out to us, this reduction to S5 can be simplified somewhat by defining wp(π, ⊤) directly, as follows.

Definition 16

1. wp(⊥, ⊤) = ⊥.

2. wp(p, ⊤) = p.

3. wp(π_{1}; π_{2}, ⊤) = wp(π_{2}, ⊤)↓wp(π_{1}, ⊤).

4. wp(π_{1} ∪ π_{2}, ⊤) = wp(π_{1}, ⊤) ∨ wp(π_{2}, ⊤).

5. wp(¬π, ⊤) = ¬wp(π, ⊤).

6. wp(might π, ⊤) = ◇wp(π, ⊤).

10 Calculations of Consistency

Veltman calls a program π of L_{P} consistent if there is some information state I for which [[π]](I) ≠ ∅. Intuitively, consistent programs are programs that can be used to convey information. By the soundness of the Hoare/Pratt calculus, consistency of an update program π boils down to the question whether there is some S5 consistent φ ∈ ml_{P} such that ⊢ φ ↔ ⟨π⟩top. We illustrate how to check consistency for two examples taken from Veltman [22]. We calculate with WPs, but by virtue of the fact that WP reasoning and NSC reasoning are equivalent (Theorem 10), calculations with NSCs work just as well.

Example 1 might p; ¬p is consistent.

Proof:

wp(might p; ¬p , ⊤) = wp(might p; wp(¬p , ⊤))
= wp(might p; ¬wp(p, ⊤))
= wp(might p; ¬p)
= ◇p ∧ ¬p

Since ◇p ∧ ¬p does have S5 models, so it is not S5-provably equivalent to ⊥.

Example 2 ¬p ; might p is not consistent.

Proof:

wp(¬p ; might p, ⊤) = wp(¬p; wp(might p, ⊤))
= wp(¬p, ◇wp(p, ⊤))
= wp(¬p, ◇p)
= ◇p↓¬wp(p, ⊤)
= ◇p↓¬p
= ¬p ∧ ◇(p ∧ (p↓¬p))
= ¬p ∧ ◇(p ∧ ¬p))
= ¬p ∧ ⊥
= ⊥

Of course, these results can also be established in our weakest precondition Hoare/Pratt calculus. By using the matching axiom schemata we derive that ⊢ (◇p ∧ ¬p) ↔ ⟨might p; ¬p⟩⊤, and that ⊢ (◇p↓¬p) ↔ ⟨¬p; might p⟩⊤. In short, by our construction of a calculus for update logic we claim to have established a clean connection between a species of information flow logic and good old static S5.

11 Conclusion

There is scope for quite a bit of further work. In the first place, one could explore Veltman’s extended versions of update logic in the same spirit. More specifically, a modal study of the preference relation on information states that Veltman proposes seems to be worthwhile: this would lead to a link to a trimodal system with one modal operator 1 reflecting the dynamics of discarding possibilities (basically, our S5 box □), a modal operator 2 interpreted in terms of the preference order on the set of all worlds (the ‘normally’ relation), and finally a modal operator 3 interpreted in terms of the preference relation restricted to the current input information set (the ‘presumably’ relation). Thus, the modal perspective on defaults would use a relation of ‘being as least as likely as’ between worlds. 2 φ (for: φ holds by default) would hold in a world w ∈ W if in all worlds w′ ∈ W that are at least as likely as w, φ holds. 3 φ (for: φ presumably holds) would hold in a world w ∈ W, given a current information set I, if in all worlds w′ ∈ I that are at least as likely as w, φ holds.

In a different direction, one may study the combination of the calculus given here with the calculus from [7] in a system of quantificational update logic satisfying the desiderata which Groenendijk and Stokhof list in [11]. In such a system one would be able to handle the combination of epistemic operators like might or maybe (the province of update logic) and pronominal bindings across sentence boundaries (the key application area of dynamic predicate logic and dynamic Montague grammar [10]), as in the following example sentence.

(6) A man walked out. Maybe he was angry.

A suitable representation medium for such examples is a system of dynamic assignment logic with epistemic modalities. Such a system is developed in Van Eijck and Cepparello [6] and axiomatized in a similar way to the approach of the present paper, but now with modal predicate logic instead of modal propositional logic as assertion language.

The more general moral of the paper, however, is in the demonstration that techniques from theoretical computer science can be applied fruitfully to information logic, broadly conceived. A dynamic logic in the spirit of Hoare and Pratt geared to this application was proposed by Van Benthem in [5], and worked out further in De Rijke [20].

In this logic there is an explicit modality ⊑ for ‘becoming more specific about what on assumes to be the case’, or ‘increasing one’s information’. The process of expanding one’s set of assumptions to make it include φ, for example, is given by the program ⊑; φ?. The process of purging one’s set of assumptions to take one back to a state where φ fails is given by ⊑ˇ ; ¬φ? (hereˇ is the operator which takes a program to its converse).

Dynamic modal logics have a procedural part and a propositional part which are connected by modes (expand to φ, retract to φ, test for φ) and projections (being in the domain of π, being in the range of π, being a fixpoint for π). As is demonstrated in De Rijke [19], such systems can be used to analyse information logics which have operations for both ‘updating’ and ‘downdating’ (retracting information). The central point of their use remains the Hoare/Pratt style analysis of the connection between procedural notions (properties of programs) and static notions (properties of states), in the spirit that was demonstrated above.

Acknowledgement

This paper has benefited from helpful comments by Johan van Benthem, Giovanna Cepparello, Tim Fernando, Willem Groeneveld, Marcus Kracht, Frank Veltman, Kees Vermeulen, Jørgen Villadsen, Albert Visser, and an anonymous referee of this journal. Thank you all.

References

[1] J. Barwise. Noun phrases, generalized quantifiers and anaphora. In P. Gärdenfors, editor, Generalized Quantifiers: linguistic and logical approaches, pages 1–30. D. Reidel Publishing Company, Dordrecht, 1987.

[2] J. van Benthem. Semantic parallels in natural language and computation. In H.-D. Ebbinghaus et al., editors, Logic Colloquium, Granada, 1987, pages 331–375, Amsterdam, 1989. Elsevier.

[3] J. van Benthem. General dynamics. Theoretical Linguistics, 17:159–201, 1991.

[4] J. van Benthem. Language in Action: categories, lambdas and dynamic logic. Studies in Logic 130. Elsevier, Amsterdam, 1991.

[5] J. van Benthem. Logic and the flow of information. Technical Report LP-91-10, ILLC, University of Amsterdam, 1991.

[6] J. van Eijck and G. Cepparello. Dynamic modal predicate logic. Technical Report OTS-WP-CL-93-005, OTS, Utrecht, October 1993. Also in M. Kanazawa and C.J. Piñon (eds.), Dynamics, Polarity, and Quantification, CSLI, Stanford 1994.

[7] J. van Eijck and F.J. de Vries. Dynamic interpretation and Hoare deduction. Journal of Logic, Language, and Information, 1:1–44, 1992.

[8] P. Gärdenfors. Knowledge in Flux: Modelling the Dynamics of Epistemic States. MIT Press, 1988.

[9] R. Goldblatt. Logics of Time and Computation, Second Edition, Revised and Expanded, volume 7 of CSLI Lecture Notes. CSLI, Stanford, 1992 (first edition 1987). Distributed by University of Chicago Press.

[10] J. Groenendijk and M. Stokhof. Dynamic predicate logic. Linguistics and Philosophy, 14:39–100, 1991.

[11] J. Groenendijk and M. Stokhof. Two theories of dynamic semantics. In J. van Eijck, editor, Logics in AI—European Workshop JELIA ’90, pages 55–64, Berlin, 1991. Springer Lecture Notes in Artificial Intelligence.

[12] I. Heim. The Semantics of Definite and Indefinite Noun Phrases. PhD thesis, University of Massachusetts, Amherst, 1982.

[13] C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):567–580, 583, 1969.

[14] H. Kamp. A theory of truth and semantic representation. In J. Groenendijk et al., editors, Formal Methods in the Study of Language. Mathematisch Centrum, 1981.

[15] L. Karttunen. Discourse referents. In J. McCawley, editor, Syntax and Semantics 7, pages 363–385. Academic Press, 1976.

[16] M. Kracht. Splittings and the finite model property. Logic group preprint series, Department of Philosophy, University of Utrecht, 1991. To appear in the JSL.

[17] D. Lewis. Score keeping in a language game. Journal of Philosophical Logic, 8:339–359, 1979.

[18] V. Pratt. Semantical considerations on Floyd–Hoare logic. Proceedings 17th IEEE Symposium on Foundations of Computer Science, pages 109–121, 1976.

[19] M. de Rijke. Meeting some neighbours. Technical Report LP-92-10, ILLC, University of Amsterdam, 1992. Also in Van Eijck and Visser (eds.), Logic and Information Flow, MIT Press, 1994.

[20] M. de Rijke. A system of dynamic modal logic. Technical Report LP-92-08, ILLC, University of Amsterdam, 1992.

[21] R. Stalnaker. Pragmatics. In D. Davidson and G. Harman, editors, Semantics of Natural Language, pages 380–397. Reidel, 1972.

[22] F. Veltman. Defaults in update semantics. Technical report, Department of Philosophy, University of Amsterdam, 1991. To appear in the Journal of Philosophical Logic.