Dynamic interpretation and Hoare deduction

JAN VAN EIJCK CWI, Kruislaan 413, 1098 SJ Amsterdam, The Netherlands OTS, Trans 10, 3512 JK Utrecht, The Netherlands and FER-JAN DE VRIES CWI, Kruislaan 413, 1098 SJ Amsterdam, The Netherlands

Abstract. In this paper we present a dynamic assignment language which extends the dynamic predicate logic of Groenendijk & Stokhof [1991: 39–100] with ι assignment and with generalized quantifiers. The use of this dynamic assignment language for natural language analysis, along the lines of o.c. and [Barwise, 1987: 1–29], is demonstrated by examples. We show that our representation language permits us to treat a wide variety of ‘donkey sentences’: conditionals with a donkey pronoun in their consequent and quantified sentences with donkey pronouns anywhere in the scope of the quantifier. It is also demonstrated that our account does not suffer from the so-called proportion problem.

Discussions about the correctness or incorrectness of proposals for dynamic interpretation of language have been hampered in the past by the difficulty of seeing through the ramifications of the dynamic semantic clauses (phrased in terms of input-output behaviour) in non-trivial cases. To remedy this, we supplement the dynamic semantics of our representation language with an axiom system in the style of Hoare. While the representation languages of Barwise and Groenendijk & Stokhof were not axiomatized, the rules we propose form a deduction system for the dynamic assignment language which is proved correct and complete with respect to the semantics.

Finally, we define the static meaning of a program π of the dynamic assignment language as the weakest condition φ such that π terminates successfully on all states satisfying φ, and we show that our calculus gives a straightforward method for finding static meanings of the programs of the representation language.

Key words: semantics of natural language, dynamic interpretation, Hoare logic, knowledge representation languages.

1. Introduction

Our starting point is a dynamic perspective on natural language as proposed in [Barwise, 1987: 1–29] and [Groenendijk & Stokhof, 1991: 39–100]. We propose to supplement the purely semantic treatment that was given in those papers with a syntactic account, using the tools of Hoare logic. The key notions to be introduced and discussed in this paper are briefly summarized in the following table. Hopefully the table does provide some guidance through the pages that follow.

π  syntax of dynamic assignment language  §3
[[π]]_{M}  interpretation of program π w.r.t. model M  §4
[[Qx(π_{1}, π_{2})]]_{M}  interpretation of quantified programs  §5,6
M ⊧ φ [A]  valuation A satisfies formula φ in model M  §7
K ⊧ ⟨φ⟩ π ⟨ψ⟩  existential correctness assertion valid in class K §7
K ⊧ {φ} π {ψ}  universal correctness assertion valid in class K §7
K ⊢ ⟨φ⟩ π ⟨ψ⟩  existential correctness assertion derivable for K §7
K ⊢ {φ} π {ψ} universal correctness assertion derivable for K §7
If K ⊢ F then K ⊧ F soundness of the Hoare calculus  §8
If K ⊧ F then K ⊢ F completeness of the Hoare calculus  §9

2. The Dynamic Perspective on Natural Language

For a quick review of the virtues of a dynamic perspective on natural language interpretation, consider mini discourse (1), where the hearer is asked to take two different individuals in mind.

A man walked in. He sat down. Another man walked in.  (1)

Suppose we intend the reading where he is anaphorically linked to the earlier indefinite and another is anaphorically constrained (to borrow a term from Barwise, o.c.) by that same indefinite. We follow Barwise in using superscript indices for antecedents and subscripts for anaphors, to indicate the intention.

A man^{1} walked in. He_{1} sat down. Another_{1} man^{2} walked in.  (2)

What intuitively happens when discourse (2) is processed can be described as follows. First one (i.e., the processor) is invited to focus on an arbitrary man. Then one is asked to consider a choice of man where that man walked in. Furthermore one is asked to focus on a choice of man where that man sat down as well. Next one is assumed to keep this choice of man in mind, and again to pick a reference to an arbitrary man, but in such a way that that man is different from the first man. Finally one is to consider a second choice of man where that second man walked in.

This account sounds like a piece of imperative programming, which suggests that its meaning can be given in terms of a translation into a programming language. Here is such a translation (tense is ignored), in a language which has the same expressive power as the dynamic predicate logic of Groenendijk & Stokhof [1991: 39–100], but which reveals its imperative programming nature a bit more clearly.

ηv_{1} : man v_{1}; walk-in v_{1}; sit-down v_{1};  (3)

ηv_{2} : (v_{2} ≠ v_{1}; man v_{2}); walk-in v_{2}.

The programming language employed in (3) has two kinds of basic statements: assignments and tests. ηx : π is a command to assign an arbitrary individual to x that fulfils requirement π. R(t_{1} ⋯ t_{n}) is a test which succeeds on a given input variable state if the values of the terms t_{1} through t_{n} fulfil the condition specified by the relation symbol R, and fails otherwise. Sequences of statements are formed with the sequencing operator ;. The assignments are non-deterministic, which means that semantically a program is not a function from states to states, but a relation between states (or equivalently, a function from states to sets of states). Test statements narrow down the set of output states. A test relates an input state that satisfies it to itself, and an input state that does not satisfy it to nothing at all.

We will fix the meaning for this assign-and-test mini-language by giving a (dynamic) semantics for it. Next, we specify a set of Hoare style rules for it, by way of axiom system. The advantage of doing both of these things is that the Hoare style rules provide a link to notions of static semantics, thus allowing us to take snapshots of truth conditions at various stages in the discourse processing, so to speak. Stated otherwise, the Hoare style rules allow us to consider projections from dynamic logic to static logic, in the sense of [Van Benthem, 1990].

3. Dynamic Assignment Logic: Syntax and Informal Semantics

This section is meant as an introduction to dynamic predicate logic in its undisguised form as an imperative programming language. The ingredients to be introduced here are atomic tests, sequential program composition, indefinite and definite assignments, program implication and program negation. Later on we will add generalized quantifiers. We call the language we are about to present DAL (Dynamic Assignment Logic).

In natural language, one does not engage in explicitly bookkeeping with regard to the ‘slots’ used for keeping track of individuals mentioned in discourse. One just keeps them in mind, and does not confuse them, that is all. To make sure that in DAL the slots do not get confused, one might stipulate that new assignments to variables which are already ‘active’ are forbidden. We will not impose this constraint on the general framework, but we will define a sublanguage of DAL programs where the constraint is imposed.

We first define the set of programs of DAL and the set av of assignment variables of a DAL program. For simplicity’s sake we take the terms of DAL to be a set of individual variables V (one might want to add constants and deictic parameters to this, but we will not do so here).

Given a set of terms and a set of relation symbols, the set of DAL programs is the smallest set such that the following hold.

1. ⊥ is a program.

2. If t_{1}, t_{2} are terms, then t_{1} = t_{2} is a program.

3. If R is an n-place relation symbol and t_{1}, …, t_{n} are terms, then R(t_{1} ⋯ t_{n}) is a program.

4. If π_{1} and π_{2} are programs then (π_{1}; π_{2}) is a program.

5. If π_{1} and π_{2} are programs then (π_{1} ⇒ π_{2}) is a program.

6. If π is a program, then ¬π is a program.

7. If π is a program and x is a variable, then ηx : π is a program.

8. If π is a program and x is a variable, then ιx : π is a program. Here is the definition of the set av(π) of assignment variables of a program π.

1. av(⊥) = ∅.

2. av(t_{1} = t_{2}) = ∅.

3. av(R(t_{1} ⋯ t_{n})) = ∅.

4. av((π_{1}; π_{2})) = av(π_{1}) ∪ av(π_{2}).

5. av((π_{1} ⇒ π_{2})) = ∅.

6. av(¬π) = ∅.

7. av(ηx : π) = {x} ∪ av(π).

8. av(ιx : π) = {x} ∪ av(π). Next we define the sublanguage of DAL programs (call it DAL_{0}), where no new values get assigned to ‘active’ variables. Here we need simultaneous recursion on π and av(π). It is the smallest set such that the following hold.

1. ⊥ is a program with av(⊥) = ∅.

2. If t_{1}, t_{2} are terms, then t_{1} = t_{2} is a program with av(t_{1} = t_{2}) = ∅.

3. If R is an n-place relation symbol and t_{1}, …, t_{n} are terms, then R(t_{1} ⋯ t_{n}) is a program with av(R(t_{1} ⋯ t_{n})) = ∅.

4. If π_{1} and π_{2} are programs with av(π_{1}) ∩ av(π_{2}) = ∅ then (π_{1}; π_{2}) is a program with av((π_{1}; π_{2})) = av(π_{1}) ∪ av(π_{2}).

5. If π_{1} and π_{2} are programs with av(π_{1}) ∩ av(π_{2}) = ∅ then (π_{1} ⇒ π_{2}) is a program with av((π_{1} ⇒ π_{2})) = ∅.

6. If π is a program, then ¬π is a program with av(¬π) = ∅.

7. If π is a program and x is a variable with x ∉ av(π) then ηx : π is a program with av(ηx : π) = {x} ∪ av(π).

8. If π is a program and x is a variable with x ∉ av(π) then ιx : π is a program with av(ιx : π) = {x} ∪ av(π).

We will follow the usual predicate logical convention of omitting outermost parentheses for readability. Also, it will become evident from the semantic clause for sequential composition that the ; operator is associative. Therefore, we will often take the liberty to write π_{1}; π_{2}; π_{3} instead of (π_{1}; π_{2}); π_{3} or π_{1}; (π_{2}; π_{3}). Also, t_{1} ≠ t_{2} will be used to abbreviate ¬t_{1} = t_{2} (cf. example (3)). Finally, we use ⊤ as an abbreviation for ¬⊥.

The restrictions on assignment variables will for example rule out (4) as a program of DAL_{0} (though not of DAL).

ηv_{1} : man v_{1}; ηv_{1} : boy v_{1}.  (4)

The remainder of this section is devoted to an informal account of the semantics of atomic test predicates, implication, negation and union of DAL programs, and η and ι assignment. Section 4 will give the formal semantics.

Semantically, what we are interested in is states, functions from the set of DAL variables to individuals in a model. Semantically, DAL programs act as state transformers: a DAL program takes an input state and either indicates success by producing an output state or it indicates failure by not producing anything at all. Equivalently, we can view the meaning of a program as a function mapping any input state to the set of all possible outputs the program can produce for that input. A program which is a test will on input A either produce output set {A} (in case the test succeeds) or output set ∅ (in case the test fails). Programs which may produce non-singleton sets are non-deterministic; for some inputs there is more than one possible output state. Examples of non-deterministic programs are η assignment programs; the program ηx : π has, on input A, the set of all states which may differ from A in the fact that they have another x value, namely some value that satisfies π.

The program ⊥ expresses a test which always fails; it is meant to express the same as if true then fail else skip fi. In other words: for every input state A, ⊥ will produce output state ∅. As was mentioned above, we use ⊤ as an abbreviation for ¬⊥. The program ⊤ is a test which always succeeds; in other words, it is meant to express the same as the ALGOL style statement if true then skip else fail fi. In other words, for every input state A, ⊤ will produce output set {A}. Atomic predicates like t_{1} = t_{2} or R(t_{1} ⋯ t_{n}) are meant to express tests which may fail; in ALGOL style notation: if R(t_{1} ⋯ t_{n}) then skip else fail fi. Again in terms of input output behaviour: If R(t_{1} ⋯ t_{n}) evaluates to true in state A, the predicate will have output set {A}, otherwise the output set will be ∅.

Programs of the form (π_{1} ⇒ π_{2}) are intended to treat the interplay of natural language implication and descriptions, as in the following examples.

If a girl^{1} has a boyfriend^{2}, she_{1} teases him_{2}.  (5)
If a man^{1} admires the king^{2}, he_{1} cheers him_{2}.  (6)

Example (5) has the following DAL translation.

(ηv_{1} : girl v_{1}; ηv_{2} : boyfriend v_{2}; has(v_{1}, v_{2})) ⇒ teases(v_{1}, v_{2}).  (7)

To get the semantics right, one has to assume that (7) is true if and only if every output state for the antecedent (8) will be an appropriate input state for the consequent (9)lave/everyslave

ηv_{1} : girl v_{1}; ηv_{2} : boyfriend v_{2}; has(v_{1}, v_{2}).  (8)
teases(v_{1}, v_{2}).  (9)

Negation should allow one to treat examples like the following, where the negation has scope over an indefinite.

The manager^{1} does not use a PC^{2}.  (10)

This example can be translated into DAL as follows:

ιv_{1} : (manager v_{1}); ¬(ηv_{2} : pc v_{2}; use(v_{1}, v_{2})).  (11)

To get the semantics right, a negated program should act as a test: ¬π should accept (without change) all variable states which cannot serve as input for π, and reject all others. In fact, it will turn out that ¬π is definable in terms of ⇒ and ⊥, as π ⇒ ⊥.

Definite descriptions can act as anaphors and antecedents at the same time. Discourse (12) provides an example.

A customer^{1} entered. The woman_{1}^{2} sat down. She_{2} smiled.  (12)

The indices indicate that the woman has a customer as its antecedent, while at the same time acting itself as antecedent for she in the next sentence (and constraining the gender of the pronoun). A DAL translation of (12) is given in (13).

ηv_{1} : customer v_{1}; enter v_{1};  (13)

ιv_{2} : (v_{2} = v_{1}; woman v_{2}); sit-down v_{2}; smile v_{2}.

The ι assignment in (13) is dependent on the η assignment to variable v_{1}. With reference to a particular assignment for v_{1}, the description is unique. Note that the ι assignment to v_{2} does indirectly act as a test on the previous η assignment to v_{1}: this test will weed out η assignments that are inappropriate in the light of the subsequent discourse.

Definite descriptions can also be dependent on each other. Consider the string of characters in (14).

a Âˆ b C.  (14)

Suppose just for an instant that (14) is a state of affairs one is talking about. The state of affairs involves characters and hat symbols (hats for short). With reference to (14), it does make sense to talk about the character with the hat, although (14) neither has a unique character nor a unique hat. We can, for instance, truthfully assert (15) about (14).

The character with the hat is a capital.  (15)

The translation into DAL is straightforward:

ιv_{1} : (character v_{1}; ιv_{2} : (hat v_{2}; with(v_{1}, v_{2}))); capital v_{1}.  (16)

Intuitively, the first ι assignment ‘tries out’ individual characters C until it finds the unique C with the property that a unique hat H for C can be found.

The semantic picture sketched above is still in need of an extra touch. Nothing we have said so far makes clear how the dynamic treatment of definite descriptions is meant to deal with their uniqueness presuppositions. This topic will not be dealt with in this paper (but see [Van Eijck, 1991]).

4. Semantics: Formal Definitions

Assume a model M = ⟨U, I⟩, with U a universe of individuals and I an interpretation function for the first order relation symbols of the language. We consider the set S of all functions A : V → U. This is the set of states for M.

A state A for M = ⟨U, I⟩ determines a valuation V_{A} for the terms of the language as follows: if t ∈ V then V_{A}(t) = A(t) (as we take all our terms to be variables, this is all there is to the definition of V_{A}). If A is a state for M, x a variable and d an element of the universe or M, then A[x := d] is the state for M which is just like A except for the possible difference that x is mapped to d.

We define a function [[π]]_{M} : S → PS by recursion. A, B, C are used as metavariables over states. The function [[π]]_{M} depends on the model M, but for convenience we will often write [[π]] rather than [[π]]_{M}. The function should be read as: on input state A, π may produce any of the outputs in output state set [[π]](A).

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

2. [[R(t_{1} ⋯ t_{n})]](A) = \begin{cases}\{A\} & if ⟨V_{A}(t_{1}), …, V_{A}(t_{n})⟩ ∈ I(R) \\ ∅ & otherwise. \end{cases}

3. [[t_{1} = t_{2}]](A) = \begin{cases}\{A\} & if V_{A}(t_{1}) = V_{A}(t_{2}) \\ ∅ & otherwise. \end{cases}

4. [[(π_{1}; π_{2})]](A) = ⋃{[[π_{2}]](B) | B ∈ [[π_{1}]](A)}.

5. [[(π_{1} ⇒ π_{2})]](A) = \begin{cases}\{A\} & if B ∈ [[π_{1}]](A) implies [[π_{2}]](B) ≠ ∅ \\ ∅ & otherwise. \end{cases}

6. [[¬π]](A) = \begin{cases}\{A\} & if [[π]](A) = ∅ \\ ∅ & otherwise. \end{cases}

7. [[ηx : π]](A) = ⋃{[[π]](A[x := d]) | d ∈ U}.

8. [[ιx : π]](A) = \begin{cases}[[π]](A[x := d]) for the unique d ∈ U \\ for which [[π]](A[x := d]) ≠ ∅ & if such d exists \\ ∅ & otherwise. \end{cases}

Truth is defined in terms of input-output behaviour: π is true relative to model M if there are states A, B for M such that B ∈ [[π]]_{M}(A). Two programs π_{1}, π_{2} are equivalent if for every model M and every state A for M, [[π_{1}]]_{M}(A) = [[π_{2}]]_{M}(A).

Dynamic consequence is defined as follows: π_{1} ⊧ π_{2} if for every model M and for all states A, B for M: if B ∈ [[π_{1}]]_{M}(A) then there is a state C with C ∈ [[π_{2}]]_{M}(B). This choice has a straightforward motivation. The consequence relation mirrors the behaviour of ⇒ at meta level, so we get the following equivalence for free.

π_{1} ⊧ π_{2} iff ⊧ π_{1} ⇒ π_{2}.  (17)

The various other possible consequence relations for dynamic logic will not concern us in this paper.

The statement ηx : π performs a non-deterministic action, for it sanctions any assignment to x of an individual satisfying π. The statement acts as a test at the same time: in case there are no individuals satisfying π the set of output states for any given input state will be empty. In fact, the meaning of ηx : π can be thought of as a random assignment followed by a test, for ηx : π is equivalent to ηx : ⊤; π, or in more standard notation, x := ?; π. It follows immediately from this explanation plus the dynamic meaning of sequential composition that ηx : (π_{1}); π_{2} is equivalent with ηx : (π_{1}; π_{2}).

The interpretation conditions for ι assignment make clear how the uniqueness condition is handled dynamically. The statement ιx : π consists of a test followed by a deterministic action in case the test succeeds: first it is checked whether there is a unique π; if so, this individual is assigned to x; otherwise the program fails (in other words, the set of output states is empty). Thus we see that the two programs ιx : (π_{1}); π_{2} and ιx : (π_{1}; π_{2}) are not equivalent. The program ιx : (π_{1}; π_{2}) succeeds if there is a unique object d satisfying π_{1}; π_{2}, while the requirement for ιx : (π_{1}); π_{2} is stronger: there has to be a unique individual d satisfying π_{1}, and d must also satisfy π_{2}.

The clause for dynamic implication should take care of the proper treatment of the description his wife in example (18).

If the president is married then his wife will be cross with him.  (18)

To indicate the reading where the possessive pronoun his is anaphorically linked to the president, we again use indices. The intended reading of (18) is indicated by the following indexing.

If the president^{1} is married then  (19)

[his_{1} wife]^{2} will be cross with him_{1}.

A suitable translation is the following:

(ιv_{1} : president v_{1}; married v_{1}) ⇒  (20)

(ιv_{2} : wife-of (v_{2}, v_{1}); cross-with(v_{2}, v_{1})).

Assuming that the president has unique reference, we can say the following. Either the subprogram for The president is married will not complete successfully, and then program (20) succeeds, or there will be a unique referent for ι assignment in the subprogram for the consequent, and the subprogram for his wife will be cross with him will succeed, provided that the unique referent for v_{2} satisfies cross-with(v_{2}, v_{1}).

5. Adding Quantifiers

Adding quantifiers to DAL is relatively straightforward. For convenience, we restrict attention to binary quantifiers. Let Q_{1}, Q_{2}, … be a list of binary quantifier symbols. Assume that the interpretation functions of the models M = ⟨D, I⟩ are extended with suitable interpretations for these. That is to say, for every Q_{i}, I(Q_{i}) is a binary quantifier relation on P(D), i.e. a relation satisfying the constraints of extension, isomorphy and conservativity (see for example [Westerståhl, 1989: 1–131]).

A quantifier relation R is conservative (or: lives on its first argument) if R(A, B) iff R(A, A ∩ B). A quantifier relation satisfies extension if adding or deleting individuals from the part of the universe which is outside the extension of the arguments does not affect the relation, i.e., if the relation satisfies R_{E}(A, B) iff R_{E′}(A, B), for all E, E′ with E, E′ ⊇ A ∪ B.

Because of our reliance on conservativity, the analysis provided in this section does not work without further ado for a quantifier like only, as in Only men are chauvinists. This problem will be addressed in Section 6. First we extend the syntax of DAL. The set of DAL programs is the smallest set satisfying the following clauses.

1. – 8. As above, in the definition of DAL.

9. If π_{1} and π_{2} are programs and Q is a quantifier, then Qx(π_{1}, π_{2}) is a program.

For the time being we do not take external dynamic effects of quantifiers into account, i.e. we take our quantifiers to be only internally dynamic. This transpires in the definition of the set of assignment variables of a quantified program.

1. – 8. As above.

9. av(Qx(π_{1}, π_{2})) = ∅. As for the extended version of DAL_{0}, the set of DAL_{0} programs is the smallest set satisfying the following clauses.

1. – 8. As above, in the definition of DAL_{0}.

9. If π_{1} and π_{2} are programs with x ∉ av(π_{1}), x ∉ av(π_{2}) and av(π_{1}) ∩ av(π_{2}) = ∅, and Q is a quantifier, then Qx(π_{1}, π_{2}) is a program with av(Qx(π_{1}, π_{2})) = ∅.

Here is the intended semantics.

1. – 8. As above.

9. [[Qx(π_{1}, π_{2})]](A) = \begin{cases}\{A\} & if \\ & ⟨\{d ∈ U | [[π_{1}]](A[x := d]) ≠ ∅\}, \\ & \{d ∈ U | [[π_{1}; π_{2}]](A[x := d]) ≠ ∅\}⟩ \\ & ∈ I(Q) \\ ∅ & otherwise. \end{cases}

The semantic clause makes clear that quantifiers, as defined here, do not have an external dynamic effect. Externally, they acts as tests: in case the test succeeds the set of output states has the input state as its only member. The internal dynamic effect of a quantifier does interact with the external dynamic effects of definites and indefinites, however.

To see how the semantics of quantification works in the simplest possible case, let us walk through example program (21).

Qx(Sx, T x).  (21)

According to the semantic clause, on input state A this program gives {A} iff the sets (22) and (23) are in the relation I(Q).

{d ∈ U | [[Sx]](A[x := d]) ≠ ∅}.  (22)
{d ∈ U | [[Sx; T x]](A[x := d]) ≠ ∅}.  (23)

According to the semantic clause for atomic tests and the definition of the valuation function for terms, the set (22) can be rewritten as (24).

{d ∈ U | d ∈ I(S)}.  (24)

In the same way, and using the semantic clause for ; , the set (23) can be rewritten as (25).

{d ∈ U | x ∈ I(S) and x ∈ I(T)}.  (25)

Because the Q is assumed to denote a conservative quantifier with first argument as given by (24), (25) can be replaced by (26).

{d ∈ U | x ∈ I(T)}.  (26)

Thus we find that (21) is true iff the sets given in (24) and (26) are in the relation denoted by the quantifier. This is the expected result.

Dynamic effects will start to play a rôle if one or both of the argument programs of a quantified program has an external dynamic effect. The traditional ‘donkey’ examples such as (27) are cases in point (see [Geach, 1962]).

Every girl^{1} who has a boyfriend^{2} teases him_{2}.  (27)

Example (27) has the following DAL translation.

Q_{∀}v_{1}(Gv_{1}; ηv_{2} : Bv_{2}; Hv_{1}v_{2}, T v_{1}v_{2}).  (28)

Here Q_{∀} denotes the generalized universal quantifier, i.e. the relation of inclusion. Establishing the meaning of examples like (27) by direct reasoning about the operational semantics is awkward, so we will guide the reader through the thicket once more.

According to the semantic clause for quantifier programs, on input state A this program gives {A} iff the sets (29) and (30) are in the inclusion relation.

{d ∈ U | [[Gv_{1}; ηv_{2} : Bv_{2}; Hv_{1}v_{2}]](A[v_{1} := d]) ≠ ∅}.  (29)
{d ∈ U | [[Gv_{1}; ηv_{2} : Bv_{2}; Hv_{1}v_{2}; T v_{1}v_{2}]](A[v_{1} := d]) ≠ ∅}.  (30)

First we reduce (29). Applying the semantic clauses for ; and η assignment and for atomic tests makes clear that (29) describes the same set as (31).

{d ∈ U | there is a d′ ∈ U such that  (31)
d ∈ I(G), d′ ∈ I(B), ⟨d, d′⟩ ∈ I(H)}.

Similarly, application of the semantic clauses for ;, for η assignment and for atomic tests makes clear that (30) describes the same set as (32).

{d ∈ U | there is a d′ ∈ U such that  (32)
d ∈ I(G), d′ ∈ I(B), ⟨d, d′⟩ ∈ I(H), ⟨d, d′⟩ ∈ I(T)}.

Paraphrasing this, we see that the semantic clause for quantified programs entails that translation (28) of (27) is true iff the set of girls who have a boyfriend is included in the set of girls who have a boyfriend and tease that boyfriend. Note that this may still be true if some of the girls have several boyfriends and tease only one of them. This shows that the reading we get for (27) is weaker than the one we got for (5). Of course, as soon as we impose the meaning postulate that every girl who has a boyfriend has precisely one boyfriend, the two translations become equivalent again.

The reader might wonder why example (27) gets a weaker interpretation than expected. The answer is that there turns out to be some latitude as to the exact way of internal dynamic binding of assignment variables from the antecedent program of the quantifier in its consequent program. These issues will be dealt with in the next section.

Readers who find the reasoning about dynamic clauses that is necessary to grasp the meaning of examples like (27) awkward have our full sympathy. Bear with us, and the axiom system to be presented in Section 7 will alleviate your problem.

Because we have used conservativity, the above story does not work for the quantifier relation interpreting only. Only P Q is true iff the set of non-Ps is included in the set of non-Qs, or equivalently, if the set of Qs is included in the set of Ps. Because only is not conservative, (33) does not mean the same as (34).

Only girls^{1} who tease a boyfriend^{2} lose him_{2}.  (33)
Only girls^{1} who tease a boyfriend^{2} tease a  (34)

boyfriend and lose him_{2}.

Rather, (33) means something like (35).

Only girls^{1} who tease a boyfriend^{2} lose their boyfriend_{2}.  (35)

This suggests that in this case the pronoun is a pronoun of laziness rather than a genuine donkey pronoun. But pronouns in the context of non-conservative quantifiers pose difficult problems, as is also borne out by the following example.

Only girls^{1} who have a boyfriend^{2} bring him_{2} to the party.  (36)

On its most salient reading, (36) is true as a matter of course, because it can be paraphrased as (37).

No girls^{1} who don’t have a boyfriend^{2} will bring him_{2}  (37)

to the party.

Interestingly, the paraphrase (37) poses a difficulty for our framework too. The problem is that the variable for a boyfriend^{2} is screened off by the negation operator, so that it is not available anymore at the level where him_{2} looks for an antecedent. To deal with (37) one would again need externally dynamic negation. We leave the problem of non-conservative quantifiers that are internally dynamic with the remark that it merits further investigation.

The following example, closely related to (27), gives rise to the so-called proportion problem in traditional discourse representation theory (see [Kamp, 1981: 277–322] for the basics of discourse representation theory, [Kamp & Reyle, 1990] for an up-to-date formulation, and [Heim, 1990: 137–177] for details on the proportion problem).

Most girls^{1} who have a boyfriend^{2} tease him_{2}.  (38)

The proportion problem may arise in connection with (38) in case there are girls who are naughty enough to have a large number of boyfriends and to tease them all. Accounts which give rise to the proportion problem would handle (38) as a case of quantification over girl-boyfriend pairs. To see how the present proposal fares, consider the translation of (38) in DAL.

most v_{1}((girl v_{1}; ηv_{2} : boyfriend v_{2}; have (v_{1}, v_{2})), tease (v_{1}, v_{2})). (39)

This is true in state A if there are states B, C such that the sets given in (40) and (41) are in the most-relation.

{d ∈ U | B ∈ [[girl v_{1}; ηv_{2} : boyfriend v_{2}; have (v_{1}, v_{2})]]  (40)
(A[v_{1} := d])}
{d ∈ U | B ∈ [[girl v_{1}; ηv_{2} : boyfriend v_{2}; have (v_{1}, v_{2});  (41)
tease (v_{1}, v_{2})]](A[v_{1} := d])}

The set given by (40) is the set of all girls who have a boyfriend, while the set given by (41) is the set of all girls who have a boyfriend and tease him. The quantification is over girls, as it should be, and not over girl–boyfriend pairs, as in the accounts which give rise to the proportion problem. In other words, this spells out a reading that does not suffer from the proportion problem. Again this is not the only possible reading; an alternative reading will be discussed in the next section.

To show that the treatment of quantification proposed here is different from the treatment proposed by Groenendijk & Stokhof [1991: 39–100], it is enough to show that their approach suffers from the proportion problem. One of the examples they discuss (o.c., p.81) is, essentially, (42), in the reading which can be paraphrased as (43).

If a girl^{1} has a boyfriend^{2} she usually teases him_{2}.  (42)
In most cases in which a girl^{1} has a boyfriend^{2} she teases him_{2}. (43)

To treat this example, Groenendijk and Stokhof reconstruct Lewis’ adverb of quantification approach in dynamic predicate logic, by reading the quantifier as a relation between sets of states. Dynamic implication, ⇒, would then correspond to →_{∀}, to be interpreted as: for all output states A of the antecedent, applying the consequent to A will produce an output. Similarly, the examples with usually or in most cases are analyzed with →_{M}, to be interpreted as: for most output states A of the antecedent, applying the consequent to A will produce an output. To see that this account does give rise to the proportion problem, observe that output states of the antecedent a girl has a boyfriend where Mary has John as a boyfriend and where the same Mary has Fred as a boyfriend will have to count as different states. The example sentences may have a reading where these should indeed count as different, but the point is that quantification over states makes it impossible to express readings where they should count as the same, as in the reading of (42) which is equivalent to the most salient reading of (38). For such cases, quantification over states does simply lead to incorrect results.

Our approach differs from the approach of Groenendijk & Stokhof precisely in that quantification is always over individuals and never over states. Our reconstruction of (43) would be as follows. Because the quantification is over cases or occasions, we have to add an occasion parameter to the predicates used for translating verb phrases, so have(x,y,o) and tease(x,y,o) for x has y at occasion o and x teases y at occasion o, respectively. The DAL translation of (43) now becomes:

most o_{1}(ηv_{1}(girl v_{1}; ηv_{2} : boyfriend v_{2}; have (v_{1}, v_{2}, o_{1})),  (44)

tease (v_{1}, v_{2}, o_{1})).

To make this true, on our account, the set of occasions at which a girl has a boyfriend and the set of occasions at which a girl has a boyfriend which she teases must be in the most relation.

Of course, on our account there is still a fair amount of latitude as to how (42), (43) and (45) are interpreted.

If a girl has several boyfriends, she usually teases them.  (45)

But the latitude resides where it belongs, for a margin of uncertainty remains as long as it is unclear what counts as an occasion, and it disappears as soon as this is resolved. As soon as we have a model where occasions are fully individuated, our quantificational analysis gives the right meanings. The discussion summarised in [Heim, 1990: 137–177] of the meanings of ‘donkey’ examples with usually should therefore in our view be re-interpreted as a discussion of factors that might be involved in the individuation of occasions.

6. Weak and Strong Readings of Quantifiers

The semantic clause for quantifier programs Qx(π_{1}, π_{2}) in the previous section takes care of the dynamic binding of the assignment variables of the antecedent program π_{1} in the consequent program π_{2} by comparing the set of objects for which π_{1} succeeds with the set of objects for which π_{1}; π_{2} succeeds. Prima facie, there is no compelling reason to use sequential composition of π_{1} and π_{2} to achieve the desired internal binding effect. Another obvious possibility is the choice π_{1} ⇒ π_{2}. We will now explore this alternative. Let us call the quantifier reading presented in the previous section the weak reading of the quantifier. The semantic clause where ⇒ is substituted for ; gives the strong reading of the quantifier. Thus, the clauses for weak and strong readings of quantifiers (which we will distinguish as Q^{w} and Q^{s}) run like this:

Weak readings of quantifiers

[[Q^{w}x(π_{1}, π_{2})]](A) = \begin{cases}\{A\} & if \\ & ⟨\{d ∈ U | [[π_{1}]](A[x := d]) ≠ ∅\}, \\ & \{d ∈ U | [[π_{1}; π_{2}]](A[x := d]) ≠ ∅\}⟩ \\ & ∈ I(Q) \\ ∅ & otherwise. \end{cases}

Strong readings of quantifiers

[[Q^{s}x(π_{1}, π_{2})]](A) = \begin{cases}\{A\} & if \\ & ⟨\{d ∈ U | [[π_{1}]](A[x := d]) ≠ ∅\}, \\ & \{d ∈ U | [[π_{1} ⇒ π_{2}]](A[x := d]) ≠ ∅\}⟩ \\ & ∈ I(Q) \\ ∅ & otherwise. \end{cases}

It is easy to show that as long as the antecedent program π_{1} does not have an external dynamic effect, there is nothing to choose between the weak and the strong reading of a quantifier. The following proposition refers to conservativity and extension; See Section 5 for the definitions.

PROPOSITION 6.1. If Q is a quantifier satisfying extension and conservativity and av(π_{1}) = ∅, then Q^{w}x(π_{1}, π_{2}) and Q^{s}x(π_{1}, π_{2}) are equivalent.

Proof.If av(π_{1}) = ∅, this means that π_{1} is a test. Thus, instead of (46) we can write (47).

{d ∈ U | [[π_{1}; π_{2}]](A[x := d]) ≠ ∅}.  (46)
{d ∈ U | [[π_{1}]](A[x := d]) ≠ ∅ and [[π_{2}]](A[x := d]) ≠ ∅}.  (47)

Let S_{1} be the set {d ∈ U | [[π_{1}]](A[x := d]) ≠ ∅}, and S_{2} the set {d ∈ U | [[π_{2}]](A[x := d]) ≠ ∅}. Then the set given by (47) is the set S_{1} ∩ S_{2}. Thus, the quantifier program Q^{w}x(π_{1}, π_{2}) holds iff the sets S_{1} and S_{1} ∩ S_{2} are in the relation I(Q). Because of the conservativity of Q, this is the case iff S_{1} and S_{2} are in the I(Q) relation. Similarly, if av(π_{1}) = ∅, then instead of (48) we can write (49).

{d ∈ U | [[π_{1} ⇒ π_{2}]](A[x := d]) ≠ ∅}.  (48)
{d ∈ U | [[π_{1}]](A[x := d]) = ∅ or [[π_{2}]](A[x := d]) ≠ ∅}.  (49)

Thus, the set given by (49), with respect to some universe U, is the set (U − S_{1}) ∪ S_{2}. Because Q satisfies extension, we may take U to be any set including the set S_{1} ∪ S_{2}. In particular, if we take U to be S_{1} ∪ S_{2}, the set (U − S_{1}) ∪ S_{2} reduces to S_{2}. Thus, again, the quantifier program succeeds iff S_{1} and S_{2} are in the I(Q) relation.

It is clear from the proof of proposition 6.1 that the strong reading of quantifiers will get us the right results for non-conservative quantifiers provided they satisfy extension and provided their first argument is a test. It turns out that we can handle examples like Only men are chauvinists after all; because only does satisfy extension, the recipe is simply to rely on the strong reading of the quantifier only. Note, however, that non-conservative quantifiers with restriction clauses with a dynamic effect are still beyond our scope.

In Section 5 it transpired that the weak readings of universally quantified donkey sentences were not equivalent to the if then versions of these donkey sentences. The availability of strong readings for quantifiers has remedied this situation, as the following proposition shows.

PROPOSITION 6.2. For any programs π_{1}, π_{2} with av(π_{1}) ∩ av(π_{2}) = ∅: if x is a variable such that x ∉ av(π_{1}) ∪ av(π_{2}), then (ηx : π_{1}) ⇒ π_{2} is equivalent with Q_{∀}^{s}x(π_{1}, π_{2}).

Proof.Take an arbitrary model M and an arbitrary state A for that model, and just check the semantic clauses: [[(ηx : π_{1}) ⇒ π_{2}]]_{M}(A) = {A} iff for all B ∈ [[(ηx : π_{1})]]_{M}(A) it holds that [[π_{2}]]_{M}(B) ≠ ∅. By the semantic clause for η assignment this is the case iff for all B with the property that for some d ∈ U_{M} it is the case that B ∈ [[π_{1}]]_{M}(A[x := d]), it holds that [[π_{2}]]_{M}(B) ≠ ∅. By quantifier logic, this is equivalent to: for all d ∈ U_{M} and for all B, if B ∈ [[π_{1}]]_{M}(A[x := d]), then [[π_{2}]]_{M}(B) ≠ ∅.

The semantic clause for strong readings of quantifiers says that [[Q_{∀}^{s}x(π_{1}, π_{2})]]_{M}(A) = {A} iff all d ∈ U_{M} such that [[π_{1}]]_{M}(A[x := d]) ≠ ∅ have the property that [[π_{1} ⇒ π_{2}]]_{M}(A[x := d]) ≠ ∅. By the semantic clause for ⇒, this condition is equivalent to: for all d ∈ U_{M} such that [[π_{1}]]_{M}(A[x := d]) ≠ ∅ it is the case that all B ∈ [[π_{1}]]_{M}(A[x := d]) have the property that [[π_{2}]]_{M}(B) ≠ ∅. Equivalently: for all d ∈ U_{M} and for all C it holds that if C ∈ [[π_{1}]]_{M}(A[x := d]) then is the case that all B ∈ [[π_{1}]]_{M}(A[x := d]) have the property that [[π_{2}]]_{M}(B) ≠ ∅. By quantifier logic, this in turn is equivalent to: for all d ∈ U_{M} and for all B, if B ∈ [[π_{1}]]_{M}(A[x := d]) then [[π_{2}]]_{M}(B) ≠ ∅.

Since (ηx : π_{1}) ⇒ π_{2} and Q_{∀}^{s}x(π_{1}, π_{2}) are both tests, and since we have shown that these tests succeed in precisely the same circumstances, we have established the claim that the programs are equivalent.

A question one might want to ask now is whether a similar result holds for Q_{∃}^{w}x(π_{1}, π_{2}) and ηx : π_{1}; π_{2}. The answer is of course no, for the simple reason that Q_{∃}^{w}x(π_{1}, π_{2}) is a test while ηx : π_{1}; π_{2} is not. But there is something more to the question than this. For quantifiers like every and most, it is not difficult to invent pairs of example sentences where the first member of the pair has to be paraphrased as a weakly read existential quantifier and the second member as a strongly read one (see below for some standard examples from the literature of such pairs for the quantifiers every and most). It seems to us that it is much harder to find examples of such pairs for the case of some. It is not even completely clear to us if the distinction between Q_{∃}^{w}x(π_{1}, π_{2}) and Q_{∃}^{s}x(π_{1}, π_{2}) makes intuitive sense. This observation might be interpreted as evidence for the case that determiners like some and a are quite special after all, in that they are to be treated in terms of active assignment variables rather than generalized quantifiers. We will not pursue this issue any further here, as it would lead us into the realm of externally dynamic quantification and thus beyond the scope of this paper.

There is extensive discussion in the literature (see e.g. [Chierchia, 1991: 37–78] and the references cited therein) of the distinction between weak and strong readings of quantified ‘donkey’ sentences with quantifiers like every and most. Sentences like (50), (52) and (54) are given in the literature as cases where the weak reading is appropriate, while sentences like (51), (53) and (55) seem to require the strong reading.

If a man has a dime, he puts it in the parking meter.  (50)
If a man owned a slave, he also owned its offspring.  (51)
Every man who has a dime will put it in the parking meter.  (52)
Every man who owned a slave also owned its offspring.  (53)
Most men who have a dime will put it in the parking meter.  (54)
Most men who owned a slave also owned its offspring.  (55)

For the examples (52), (53), (54) and (55) we get the required contrast from the distinction between the two interpretation rules for quantifiers. For examples (50) and (51), an analysis in terms of occasions is needed to get the required contrast. As long as we stick to the treatment of if then clauses in terms of ⇒, we only get the strong readings. But of course, a more subtle analysis of (50) and (51) will treat the if then construction in terms of universal quantification over cases, along the lines sketched in Section 5. The analysis of (50) and (51) now becomes (56) and (57), respectively.

Q_{∀}^{w}o_{1}(ηv_{1} : man v_{1}; ηv_{2} : dime v_{2}; have (v_{1}, v_{2}, o_{1})),  (56)
put-in-parking-meter (v_{1}, v_{2}, o_{1})).
Q_{∀}^{s}o_{1}(ηv_{1} : man v_{1}; ηv_{2} : slave v_{2}; owned (v_{1}, v_{2}, o_{1})),  (57)
ιv_{3} : offspring-of (v_{3}, v_{2}); owned (v_{1}, v_{3}, o_{1})).

We can paraphrase the semantic condition imposed by (56) as follows: every occasion where there is a man with a dime is an occasion where there is a man with a dime who puts a dime in the parking meter. This is intuitively acceptable. The paraphrase for (57) becomes: every occasion where there is a man with a slave that he owns is an occasion where it holds for every man and every slave owned by that man at that occasion, that the man owns the offspring of that slave. This also seems intuitively acceptable. If the reader is not convinced that these are indeed the correct paraphrases of the weak and strong quantifier readings for these examples, the sections that follow will provide an easy means to verify these claims.

Other examples from the folk-lore are also quite easy to handle. Consider examples (58), (59) and (60).

If a man^{1} shares a place with another_{1} man^{2},  (58)

he_{1} shares the housework with him_{2}.

Most customers^{1} who buy a spark plug^{2} buy three other_{2} spark  (59)

plugs with it_{2} (unless they own a 2CV).

If a customer^{1} buys a spark plug^{2}, he_{1} usually buys three other_{2} (60)

spark plugs with it_{2} (unless he owns a 2CV).

In the case of (58) we get the right results if we analyse the if then phrase in terms of weak or strong universal quantification over occasions (some reflection will show that for this example the weak and strong readings are equivalent). The example was invented to argue against a so-called E-type analysis of the pronouns he_{1} and him_{2} (see [Heim, 1990: 137–177]), but in the present perspective there is nothing problematic about such symmetric cases at all. On the analysis we propose, sentence (58) is true iff every occasion in which there are two distinct men sharing a place is an occasion in which there are two distinct men sharing a place and also sharing the housework. Equivalently, sentence (58) is true iff every occasion in which there are two distinct men sharing a place is an occasion in which every pair of distinct men sharing a place is such that they also share the housework.

The equivalence of strong and weak readings also holds for example (59). Under the weak reading, example (59) says that the majority of customers (excluding 2CV owners) that buy a spark plug are customers that buy a spark plug plus three other spark plugs. Under the strong reading, example (59) says that the majority of customers (excluding 2CV owners) that buy a spark plug are customers that for every spark plug that they buy, buy three other ones. It is not difficult to see that in this case as well, the weak and strong readings are equivalent. The same holds for the case of (60), although here we have to analyze in terms of quantification over occasions.

7. An Axiom System for Dynamic Interpretation

Discussions about the correctness or incorrectness of proposals for dynamic interpretation of language have been hampered in the past by the difficulty of seeing through the ramifications of the dynamic semantic clauses in non-trivial cases. To remedy this, we supplement the semantics of our representation language with an axiom system in the style of Hoare (see [Apt, 1981: 431–483] for an overview of this approach). The axioms and proof rules we propose form a deduction system allowing us to prove statements about DAL programs; in Section 8, this calculus is proved sound and in Section 9 it is proved complete with respect to the semantics.

Our deductive system for dynamic logic is a hybrid calculus, with statements characterizing variable states, plus two kinds of correctness statements, which we call universal and existential correctness statements. Thus, the system has three kinds of statements: (i) formulae of a language of first order predicate logic with the same sets of variables and predicate letters as the DAL language under consideration, and extended with the same set of generalized quantifiers (call this assertion language L), (ii) triples of the form {φ} π {ψ}, where φ, ψ are L-formulae, and π is a DAL-program, and (iii) triples of the form ⟨φ⟩ π ⟨ψ⟩, where again φ, ψ are L-formulae, and π is a DAL-program.

The statements of the form φ are used for making assertions about variable states A for L with respect to models M for L. Because the DAL language and the assertion language L have the same set of variables, variable states for the DAL language are variable states for L. The relation M ⊧ φ [A], for state A verifies φ in M, is defined in the standard way. If φ is a formula of the assertion language L, then fv(φ) is the set of free variables of φ, and if φ is an L formula and x, y are variables then [y/x]φ is the result of the substitution of y for all free occurrences of x in φ.

The statements of the form {φ} π {ψ} are universal correctness statements. In the terminology of Hoare’s logic, they express partial correctness. The statement {φ} π {ψ} expresses that all variable states A (for an arbitrary model M) that satisfy φ have the property that if some variable state B is an output state of π for input state A, then B satisfies ψ.

The statements of the form ⟨φ⟩ π ⟨ψ⟩ are existential correctness statements. In terms of Hoare’s logic, they represent the bits one has to add to partial correctness statements to ensure total correctness. The statement ⟨φ⟩ π ⟨ψ⟩ expresses that for all input variable states A (for an arbitrary model M) that satisfies φ there is some variable state B satisfying ψ in the set of output states of π.

Because our intuitions about static meaning seem to be much better developed than our intuitions about dynamic meaning, we can, for a large class of natural language sentences, check whether the intuitive meaning of a sentence S corresponds to the meaning of its DAL translation π in the following precise sense. Does the intuitive meaning of S precisely describe the set of states for which π terminates successfully? In terms of Hoare’s logic, we can describe this set of states by the weakest existential precondition of π with respect to ⊤. What we are looking for is the weakest φ for which the statement ⟨φ⟩ π ⟨⊤⟩ is still true. The φ we are looking for has to satisfy the additional condition that it does not contain free occurrences of the assignment variables of π (the members of av(π)); φ gives the static meaning of the program π.

It may seem that our intention to use the calculus to get from dynamic to static meaning will allow us to get by with just existential correctness statements. To see that this is not so, note that such statements do not allow us to express failure of a program for a given set of input states. The statement ⟨φ⟩ π ⟨⊥⟩ does not express failure of π on input states satisfying φ. Rather, it expresses the fact that for all inputs satisfying φ the program π is guaranteed to produce an output satisfying ⊥, a statement which is absurd for all non-contradictory φ. Failure of a DAL program π on the set of inputs specified by φ, is readily expressed in terms of universal correctness, namely by {φ} π {⊥}. It is clear that in order to treat negation of programs and dynamic implication between programs, both universal and existential correctness statements are needed in the calculus.

The meanings of {φ} π {ψ} and ⟨φ⟩ π ⟨ψ⟩ are formally specified in terms of the dynamic interpretation function [[·]]_{M} that was given above plus a satisfaction relation M ⊧ φ [A], to be read as: variable state A for V satisfies φ in M. This notion is defined in the standard way. The notion of K-validity for correctness statements is defined as follows.

K-validity of Correctness Statements

If F has the form φ, where φ is a formula of the assertion language, then K ⊧ F if M ⊧ F [A] for all models M ∈ K and all states A for M.

If F has the form {φ} π {ψ}, then K ⊧ F if the following holds. For all models M ∈ K, for all states A for M, if M ⊧ φ [A] then for all states B ∈ [[π]]_{M}(A) it is the case that M ⊧ ψ [B].

If F has the form ⟨φ⟩ π ⟨ψ⟩, then K ⊧ F if the following holds. For all models M ∈ K, for all states A for M, if M ⊧ φ [A] then there is at least one state B ∈ [[π]]_{M}(A) with M ⊧ ψ [B]. The atomic predicates of DAL act as tests. The following test axioms account for their behaviour.

Test Axioms

{⊤} ⊥ {⊥}.

⟨⊥⟩ ⊥ ⟨⊥⟩.

{R(t_{1} ⋯ t_{n}) → φ} R(t_{1} ⋯ t_{n}) {φ}.

⟨R(t_{1} ⋯ t_{n}) ∧ φ⟩ R(t_{1} ⋯ t_{n}) ⟨φ⟩.

{t_{1} = t_{2} → φ} t_{1} = t_{2} {φ}.

⟨t_{1} = t_{2} ∧ φ⟩ t_{1} = t_{2} ⟨φ⟩. The axioms for the program ⊥ express that ⊥ always fails. The atomic predicates and the identities each have two axioms. In both cases the first (the axiom for universal correctness) gives the preconditions under which, if the program succeeds, all output states will satisfy φ. The second (the axiom for existential correctness) gives the preconditions which guarantee successful termination, with the postconditions guaranteed by the test.

For purposes of reasoning with the system one needs an oracle rule for the class K of models that one is interested in (for natural language applications such a class will generally be given by specifying a set of meaning postulates that all members of K should satisfy).

K Oracle Rule

Every assertion valid in K is an axiom. The well-known consequence rule holds for universal and existential correctness.

Consequence Rules

\underline{φ → ψ  \{ψ\} π \{χ\}  χ → ξ}

{φ} π {ξ}.

\underline{φ → ψ  ⟨ψ⟩ π ⟨χ⟩  χ → ξ}

⟨φ⟩ π ⟨ξ⟩. Next, one needs to specify the meanings of complex programs in the axiomatic framework.

Rules of Composition

\underline{\{φ\} π_{1} \{ψ\} \{ψ\} π_{2} \{χ\}} {φ} (π_{1}; π_{2}) {χ}.

\underline{⟨φ⟩ π_{1} ⟨ψ⟩ ⟨ψ⟩ π_{2} ⟨χ⟩} ⟨φ⟩ (π_{1}; π_{2}) ⟨χ⟩.

Rules of Negation

{φ} π {⊥} \overline{⟨φ ∧ ψ⟩ ¬π ⟨ψ⟩.}

⟨φ⟩ π ⟨⊤⟩ \overline{\{φ ∨ ψ\} ¬π \{ψ\}.}

Rules of Implication

\underline{\{φ\} π_{1} \{ψ\} ⟨ψ⟩ π_{2} ⟨⊤⟩.} ⟨φ ∧ χ⟩ (π_{1} ⇒ π_{2}) ⟨χ⟩.

\underline{⟨φ⟩ π_{1} ⟨ψ⟩ \{ψ\} π_{2} \{⊥\}.} {φ ∨ χ} (π_{1} ⇒ π_{2}) {χ}.

Rules of η Assignment

{φ} π {ψ} \overline{\{∀xφ\} ηx : π \{ψ\}}.

⟨φ⟩ π ⟨ψ⟩ \overline{⟨∃xφ⟩ ηx : π ⟨ψ⟩}.

Rules of ι Assignment

\underline{⟨φ⟩ π ⟨ψ⟩  \{¬φ\} π \{⊥\}  ⟨ψ⟩ π ⟨χ⟩}

⟨∃x(∀y([y/x]φ ↔ x = y) ∧ ψ)⟩ ιx : π ⟨χ⟩.

\underline{⟨φ⟩ π ⟨⊤⟩  \{¬φ\} π \{⊥\}  \{ψ\} π \{χ\}}

{∀x(∀y([y/x]φ ↔ y = x) → ψ)} ιx : π {χ}. Note that in the static description logic the η and ι operators from the dynamic assignment logic are contextually eliminated.

Rules of Quantification: Weak Readings

\underline{⟨φ⟩ π_{1} ⟨⊤⟩ \{¬φ\} π_{1} \{⊥\} ⟨ψ⟩ π_{1}; π_{2} ⟨⊤⟩ \{¬ψ\} π_{1}; π_{2} \{⊥\}} ⟨Qx(φ, ψ) ∧ χ⟩ Q^{w}x(π_{1}, π_{2}) ⟨χ⟩.

\underline{\{¬φ\} π_{1} \{⊥\} ⟨φ⟩ π_{1} ⟨⊤⟩ \{¬ψ\} π_{1}; π_{2} \{⊥\} ⟨ψ⟩ π_{1}; π_{2} ⟨⊤⟩} {Qx(φ, ψ) → χ} Q^{w}x(π_{1}, π_{2}) {χ}.

Rules of Quantification: Strong Readings

\underline{⟨φ⟩ π_{1} ⟨⊤⟩ \{¬φ\} π_{1} \{⊥\} ⟨ψ⟩ π_{1} ⇒ π_{2} ⟨⊤⟩ \{¬ψ\} π_{1} ⇒ π_{2} \{⊥\}} ⟨Qx(φ, ψ) ∧ χ⟩ Q^{s}x(π_{1}, π_{2}) ⟨χ⟩.

\underline{\{¬φ\} π_{1} \{⊥\} ⟨φ⟩ π_{1} ⟨⊤⟩ \{¬ψ\} π_{1} ⇒ π_{2} \{⊥\} ⟨ψ⟩ π_{1} ⇒ π_{2} ⟨⊤⟩} {Qx(φ, ψ) → χ} Q^{s}x(π_{1}, π_{2}) {χ}. In case we know the quantifier to be ↓MON, ↑MON, MON↓ or MON↑, then in the rules of quantification the first, second, third or fourth premiss, respectively, can be omitted.

Recall that a quantifier Q is ↓MON (downward monotone in its first argument) if Q is interpreted as a relation R between sets with the property that R(S_{1}, S_{2}) and S′_{1} ⊆ S_{1} imply R(S′_{1}, S_{2}). A quantifier Q is ↑MON (upward monotone in its first argument) if Q is interpreted as a relation R between sets with the property that R(S_{1}, S_{2}) and S_{1} ⊆ S′_{1} imply R(S′_{1}, S_{2}). Similarly, MON↓ or MON↑ are used for monotonicity in the second argument. The binary universal quantifier Q_{∀}, for example, is ↓MON and MON↑, while the binary existential quantifier Q_{∃} is ↑MON and MON↑.

Incidentally, the rules of quantification demonstrate that the snapshot language for static meaning (the assertion language) has to have essentially the same expressive power as the language for dynamic meaning (the DAL language), for we need a static counterpart for every dynamic generalized quantifier.

The above axioms and rules engender a notion of K-derivation, as follows. A K-derivation is a finite sequence of correctness formulae F_{1}, …, F_{n} such that for every i, 1 ≤ i ≤ n, F_{i} is a test axiom or a an axiom according to the K oracle rule, or F_{i} is the conclusion of an instance of one of the inference rules while the premisses of that rule occur among F_{1}, …, F_{i−1}. A K-derivation F_{1}, …, F_{n} is said to be a K-derivation of F_{n}. F is called K-derivable in the proof system if there is a K-derivation of F. Notation: K ⊢ F. In the next section, the soundness of this proof system relative to K will be proved.

8. Soundness of the Calculus

An inference from premisses F_{1}, …, F_{n} to conclusion F is called K-valid if K validity of the premisses implies K validity of the conclusion. We will now show that the proof system given in the previous section is correct relative to K, i.e. for every correctness statement F:

K ⊢ F implies K ⊧ F.

To prove this, we first show that the axioms are K-valid, and next that the inference rules preserve K-validity. The soundness result then follows by induction on the length of derivations.

Test Axioms

The soundness of the test axioms for ⊥ is clear from the definition of K validity. For the universal axiom for R(t_{1} ⋯ t_{n}) the reasoning is as follows. Assume a model and a state M, A such that (61).

M ⊧ R(t_{1} ⋯ t_{n}) → φ [A].  (61)

There are two possibilities. If M ⊧ ¬R(t_{1} ⋯ t_{n}) [A], then, by the semantic clause for R(t_{1} ⋯ t_{n}), the output state set will be empty, so trivially every member of this set will satisfy φ. If M ⊧ R(t_{1} ⋯ t_{n}) [A] then, by (61), M ⊧ φ [A]. In this case, by the semantic clause for R(t_{1} ⋯ t_{n}), [[R(t_{1} ⋯ t_{n})]]_{M}(A) = {A}, so again every member of the output set does satisfy φ. For the existential axiom for R(t_{1} ⋯ t_{n}), assume (62).

M ⊧ φ ∧ R(t_{1} ⋯ t_{n}) [A].  (62)

It follows immediately from the semantic clause for R(t_{1} ⋯ t_{n}) that (63).

[[R(t_{1} ⋯ t_{n})]]_{M}(A) = {A}.  (63)

So there is a member of the output set which does satisfy φ. The reasoning for the universal and existential test axioms for t_{1} = t_{2} is similar.

K Oracle Rule

The axioms generated by the K oracle rule are valid by definition.

Consequence Rules

The soundness proof of the first consequence rule is standard (and trivial). We prove the soundness of the second consequence rule. Assume (64), (65) and (66).

K ⊧ φ → ψ.  (64)
K ⊧ ⟨ψ⟩ π ⟨χ⟩.  (65)
K ⊧ χ → ξ.  (66)

We have to show K ⊧ ⟨φ⟩ π ⟨ξ⟩. Take a model M ∈ K and a state A for M such that (67).

M ⊧ φ [A].  (67)

From (64) and (67) it follows that (68).

M ⊧ ψ [A].  (68)

From (68) and (65) it follows that there is a state B ∈ [[π]]_{M}(A) with M ⊧ χ [B]. From this and (66) it follows that there is a state B ∈ [[π]]_{M}(A) with M ⊧ ξ [B].

Rules of Composition

For the first rule of composition, assume (69) and (70).

M ⊧ {φ} π_{1} {ψ} [A].  (69)
M ⊧ {ψ} π_{2} {χ} [A].  (70)

What we have to show is M ⊧ {φ} π_{1}; π_{2} {χ} [A], so we assume M ⊧ φ [A]. Suppose some state C ∈ [[π_{1}; π_{2}]]_{M}(A). Then there is some state B ∈ [[π_{1}]]_{M}(A) such that C ∈ [[π_{2}]]_{M}(B). It follows from (69) and (70) that M ⊧ χ[C].

For the second rule of composition, assume (71) and (72).

M ⊧ ⟨φ⟩ π_{1} ⟨ψ⟩ [A].  (71)
M ⊧ ⟨ψ⟩ π_{2} ⟨χ⟩ [A].  (72)

What we have to show is M ⊧ ⟨φ⟩ π_{1}; π_{2} ⟨χ⟩ [A], so we assume M ⊧ φ [A]. From (71) it follows that there is some state B ∈ [[π_{1}]]_{M}(A) with M ⊧ ψ [B]. From (72) it follows that there is some state C ∈ [[π_{2}]]_{M}(B) with M ⊧ χ[C], which is what we had to prove.

Rules of Negation

If we consider ¬π as an abbreviation for π ⇒ ⊥, we can derive the rules of negation as follows. Assume (73).

{φ} π {⊥}.  (73)

One of the test axioms for ⊥ gives us (74).

⟨⊥⟩ ⊥ ⟨⊤⟩.  (74)

Application of the first rule of implication to (73) and (74) gives (75).

⟨φ ∧ ψ⟩ π ⇒ ⊥ ⟨ψ⟩.  (75)

This takes care of the first rule of negation. For the second rule, assume (76).

⟨φ⟩ π ⟨⊤⟩.  (76)

One of the test axioms for ⊥ gives (77).

{⊤} ⊥ {⊥}.  (77)

Applying the second rule of implication to (76) and (77) gives (78).

{¬φ → ψ} π ⇒ ⊥ {ψ}.  (78)

This takes care of the second rule of negation.

Rules of Implication

For the first rule of implication, assume (79), (80) and (81).

M ⊧ φ ∧ χ [A].  (79)
M ⊧ {φ} π_{1} {ψ} [A].  (80)
M ⊧ ⟨ψ⟩ π_{2} ⟨⊤⟩ [A].  (81)

We have to show (82).

M ⊧ ⟨φ ∧ χ⟩ π_{1} ⇒ π_{2} ⟨χ⟩ [A].  (82)

To show (82), we have to establish the fact that there is some state B ∈ [[π_{1} ⇒ π_{2}]]_{M}(A) with M ⊧ χ [B]. In view of (79), we are done if we can show that [[π_{1} ⇒ π_{2}]]_{M}(A) = {A}. For this it suffices, by the definition of the semantics for π_{1} ⇒ π_{2}, to show that for all B ∈ [[π_{1}]]_{M}(A) it holds that [[π_{2}]]_{M}(B) ≠ ∅. But this follows immediately from (80) and (81). For the second rule of implication, assume (83), (84) and (85).

M ⊧ φ ∨ χ [A].  (83)
M ⊧ ⟨φ⟩ π_{1} ⟨ψ⟩ [A].  (84)
M ⊧ {ψ} π_{2} {⊥} [A].  (85)

We have to show (86).

M ⊧ {φ ∨ χ} π_{1} ⇒ π_{2} {χ} [A].  (86)

Because [[π_{1} ⇒ π_{2}]] is a test, we are done if we can show that if [[π_{1} ⇒ π_{2}]]_{M} ≠ ∅, then M ⊧ χ [A]. This is the case iff either [[π_{1} ⇒ π_{2}]]_{M} = ∅ or M ⊧ χ [A]. In view of the semantic clause for ⇒ this is the case if either there is some state B ∈ [[π_{1}]]_{M}(A) with [[π_{2}]]_{M}(B) = ∅, or M ⊧ χ [A]. From (83) it follows that either M ⊧ φ [A] or M ⊧ χ [A]. In the second case we are done. In the first case, it follows from (84) and (85) that there is indeed a state B ∈ [[π_{1}]]_{M}(A) with [[π_{2}]]_{M}(B) ≠ ∅, which is what was to be shown.

Rules of η Assignment

For the first rule of η assignment, assume (87) and (88).

K ⊧ {φ} π {ψ}.  (87)
M ⊧ ∀xφ [A].  (88)

We have to show (89).

M ⊧ {∀xφ} ηx : π {ψ} [A].  (89)

Assume that state B ∈ [[ηx : π]]_{M}(A). Then B ∈ [[π]]_{M}(A[x := d]) for some d ∈ U. It follows from (88) that M ⊧ φ[A[x := d]], so we derive from (87) that M ⊧ ψ [B]. For the second rule of η assignment, assume (90) and (91).

K ⊧ ⟨φ⟩ π ⟨ψ⟩.  (90)
M ⊧ ∃xφ [A].  (91)

We have to show (92).

M ⊧ ⟨∃xφ⟩ ηx : π ⟨ψ⟩ [A].  (92)

From (91) it follows that there is some d ∈ U with M ⊧ φ [A[x := d]], while from (90) it follows that there is some state B ∈ [[π]]_{M}(A[x := d]) with M ⊧ ψ [B]. By the semantic clause for η assignment it follows, then, that B ∈ [[ηx : π]]_{M}(A).

Rules of ι Assignment

For the first rule of ι assignment, assume (93), (94) and (95).

K ⊧ ⟨φ⟩ π ⟨⊤⟩.  (93)
K ⊧ {¬φ} π {⊥}.  (94)
K ⊧ ⟨ψ⟩ π ⟨χ⟩.  (95)

Suppose (96).

M ⊧ ∃x(∀y([y/x]φ ↔ y = x) ∧ ψ) [A].  (96)

We have to show that there is some B ∈ [[ιx : π]]_{M}(A) with M ⊧ χ [B]. From (96) it follows that there is a d ∈ U such that (97), (98) and (99).

M ⊧ φ [A[x := d]].  (97)
For all d′ ∈ U, if d′ ≠ d, then M ⊧ ¬φ [A[x := d′]].  (98)
M ⊧ ψ [A[x := d]].  (99)

Because of (93) and (97), [[π]]_{M}(A[x := d]) ≠ ∅ and moreover, because of (95) and (99), there is a B ∈ [[π]]_{M}(A[x := d]) with M ⊧ χ [B]. Because of (94) and (98), [[π]]_{M}(A[x := d′]) = ∅ for all d′ ≠ d. Thus, by the semantic clause for ι assignment, [[ιx : π]]_{M}(A) ≠ ∅ and moreover B ∈ [[ιx : π]]_{M}(A). For the second rule of ι assignment, again assume (93) and (94), and furthermore, assume (100).

K ⊧ {ψ} π {χ}.  (100)

Suppose (101).

M ⊧ ∀x(∀y([y/x]φ ↔ y = x) → ψ) [A].  (101)

We have to show (102).

For all B ∈ [[ιx : π]]_{M}(A) it holds that M ⊧ χ [B].  (102)

From (101) it follows that if there is a d such that (97) and (98) then it will hold that (99). Now assume there is no d satisfying (97) and (98).

Then it follows from (93), (94) and the semantic clause for ι assignment that [[ιx : π]](A) = ∅, so trivially (102). If, on the other hand, there is a d satisfying (97) and (98), then (99) will hold. From this and (100) we can derive (103).

For all B ∈ [[π]](A[x := d]), M ⊧ χ [B]  (103)

Now recall that d is the unique object satisfying [[π]](A[x := d]) ≠ ∅. Thus, B ∈ [[π]](A[x := d]) iff B ∈ [[ιx : π]](A[x := d]), and we can derive from this and (103) that (102).

Rules of Quantification

We only treat the rules for weak readings, as the treatment of the rules for strong readings is completely similar. For the first rule of quantification, assume (104), (105), (106), and (107).

K ⊧ ⟨φ⟩ π_{1} ⟨⊤⟩.  (104)
K ⊧ {¬φ} π_{1} {⊥}.  (105)
K ⊧ ⟨ψ⟩ π_{1}; π_{2} ⟨⊤⟩.  (106)
K ⊧ {¬ψ} π_{1}; π_{2} {⊥}.  (107)

Suppose (108).

M ⊧ Qx(φ, ψ) ∧ χ [A].  (108)

We have to establish (109).

M ⊧ ⟨Qx(φ, ψ)⟩ Q^{w}x(π_{1}, π_{2}) ⟨χ⟩ [A].  (109)

We are done if we can show that [[Q^{w}x(π_{1}, π_{2})]]_{M} = {A}. From (108) it follows that the sets {d ∈ U | M ⊧ φ [A[x := d]]} (call this set S_{1}) and {d ∈ U | M ⊧ ψ [A[x := d]]} (call this set S_{2}) are in the relation I(Q) (where I is the interpretation function of M). Suppose M ⊧ φ [A[x := d]]. Then it follows from (104) that [[π_{1}]]_{M}(A[x := d]) ≠ ∅. Thus we have (110).

S_{1} ⊆ {d | [[π_{1}]]_{M}(A[x := d]) ≠ ∅}.  (110)

Suppose conversely that [[π_{1}]]_{M}(A[x := d]) ≠ ∅. Then it follows from (105) that M |̸= ¬φ [A[x := d]], and therefore that M ⊧ φ [A[x := d]]. Thus we have (111).

{d | [[π_{1}]]_{M}(A[x := d]) ≠ ∅} ⊆ S_{1}.  (111)

Similarly, we get from (106) that (112). and from (107) that (113).

S_{2} ⊆ {d | [[π_{1}; π_{2}]]_{M}(A[x := d]) ≠ ∅}.  (112)
{d | [[π_{1}; π_{2}]]_{M}(A[x := d]) ≠ ∅} ⊆ S_{2}.  (113)

From (110) and (111) we have (114), and from (112) and (113) we have (115).

S_{1} = {d | [[π_{1}]]_{M}(A[x := d]) ≠ ∅}.  (114)
S_{2} = {d | [[π_{1}; π_{2}]]_{M}(A[x := d]) ≠ ∅}.  (115)

It follows from (114), (115) and the semantic clause for quantifier programs that [[Q^{w}x(π_{1}, π_{2})]]_{M} = {A}.

Now suppose Q is ↓MON. Then, with S_{1}, S_{2} as above, S′_{1} ⊆ S_{1} implies ⟨S′_{1}, S_{2}⟩ ∈ I(Q). Thus, (111) and (115) are now enough to conclude that [[Q^{w}x(π_{1}, π_{2})]]_{M} = {A}, and we do not need the first premiss. For the cases where Q is ↑MON, MON↓ or MON↑ the reasoning is similar.

For the second rule of quantification, again assume (104), (105), (106), and (107), but now suppose (116).

M ⊧ Qx(φ, ψ) → χ [A].  (116)

We can express (116) equivalently as (117).

M ⊧ ¬Qx(φ, ψ) ∨ χ [A].  (117)

It follows from (117) that either the sets S_{1}, S_{2}, defined as above, are not in relation I(Q) or M ⊧ χ [A]. By the same reasoning as above, the sets S_{1}, S_{2} are in the relation I(Q) iff program Q^{w}x(π_{1}, π_{2}) accepts state A. Thus, by the semantic clause for quantifier programs, either [[Q^{w}x(π_{1}, π_{2})]]_{M}(A) = ∅ or M ⊧ χ [A]. This is what we had to show.

Again suppose Q is ↓MON. Then it follows from ⟨S_{1}, S_{2}⟩ ∉ I(Q) and S_{1} ⊆ S′_{1} that ⟨S′_{1}, S_{2}⟩ ∉ I(Q). Thus we only need (110) to clinch the argument, and the premiss (105) is superfluous. Similarly for the other cases. We have now proved the following theorem.

THEOREM 8.1 (Soundness). If K ⊢ F then K ⊧ F.

9. Completeness of the Calculus

Suppose we establish K ⊢ ⟨φ⟩ π_{1} ⇒ π_{2} ⟨⊤⟩ for some φ with K ⊧ φ. Then it follows by the soundness of the calculus that K ⊧ ⟨φ⟩ π_{1} ⇒ π_{2} ⟨⊤⟩, and by the K validity of φ that for all B in [[π_{1}]]_{M}(A) it holds that [[π_{2}]]_{M}(B) ≠ ∅, for all M ∈ K and all states A for M. In other words, the proof system can be considered as an axiomatisation of the notion of dynamic consequence, relative to classes of models K. To see that the proof system is powerful enough we also have to establish its completeness relative to K. For this we need the concepts of the weakest universal precondition and the weakest existential precondition of a DAL program and a formula of the assertion language.

The weakest universal precondition of a DAL program π and an L formula ψ is the L formula φ for which the following holds: M ⊧ φ [A] iff for all B ∈ [[π]]_{M}(A), it holds that M ⊧ ψ [B] (for arbitrary M). The weakest existential precondition of a DAL program π and an L formula ψ is the L formula φ for which the following holds: M ⊧ φ [A] iff there is a B ∈ [[π]]_{M}(A) with M ⊧ ψ [B] (for arbitrary M).

Note that it follows immediately from these definitions that the weakest universal precondition of a program π and an L formula ψ equals the negation of the weakest existential precondition of π and ¬ψ. This is because for all B ∈ [[π]]_{M}(A) it holds that M ⊧ ψ [B] is equivalent to: there is no B ∈ [[π]]_{M}(A) for which M ⊧ ¬ψ [B]. This equivalence means that either of the two notions would suffice for what follows. For practical purposes, however, it is convenient to use both weakest universal and weakest existential preconditions, so we will define functions for both.

It is not obvious at first sight that the weakest universal and existential precondition of a DAL program and an L formula always exist (as formulas of L), so we have to show that this is indeed the case. We will inductively define functions wup(π, ψ) and wep(π, ψ) of which we will then show that they express the weakest universal precondition, respectively the weakest existential precondition of π and ψ.

wup(⊥, ψ) = ⊤.

wep(⊥, ψ) = ⊥.

wup(R(t_{1} ⋯ t_{n}), ψ) = R(t_{1} ⋯ t_{n}) → ψ.

wep(R(t_{1} ⋯ t_{n}), ψ) = R(t_{1} ⋯ t_{n}) ∧ ψ.

wup(t_{1} = t_{2}), ψ) = t_{1} = t_{2} → ψ.

wep(t_{1} = t_{2}), ψ) = t_{1} = t_{2} ∧ ψ.

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

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

wup(¬π, ψ) = wep(π, ⊤) ∨ ψ.

wep(¬π, ψ) = wup(π, ⊥) ∧ ψ.

wup(π_{1} ⇒ π_{2}, ψ) = wep(π_{1}, wup(π_{2}, ⊥)) ∨ ψ.

wep(π_{1} ⇒ π_{2}, ψ) = wup(π_{1}, wep(π_{2}, ⊤)) ∧ ψ.

wup(ηx : π, ψ) = ∀xwup(π, ψ).

wep(ηx : π, ψ) = ∃xwep(π, ψ).

wup(ιx : π, ψ) = ∀x(∀y([y/x]wep(π, ⊤) ↔ y = x) → wup(π, ψ)).

wep(ιx : π, ψ) = ∃x(∀y([y/x]wep(π, ⊤) ↔ y = x) ∧ wep(π, ψ)).

wup(Q^{w}x(π_{1}, π_{2}), ψ) = Qx(wep(π_{1}, ⊤), wep(π_{1}, wep(π_{2}, ⊤))) → ψ. wep(Q^{w}x(π_{1}, π_{2}), ψ) = Qx(wep(π_{1}, ⊤), wep(π_{1}, wep(π_{2}, ⊤))) ∧ ψ. wup(Q^{s}x(π_{1}, π_{2}), ψ) = Qx(wep(π_{1}, ⊤), wup(π_{1}, wep(π_{2}, ⊤))) → ψ. wep(Q^{s}x(π_{1}, π_{2}), ψ) = Qx(wep(π_{1}, ⊤), wup(π_{1}, wep(π_{2}, ⊤))) ∧ ψ.

To show that these functions indeed give the weakest universal and existential preconditions of a program and a formula, a case by case check is necessary. The cases of atomic programs are checked directly, and induction is used to check the cases of complex programs.

Atomic Test Programs

We only treat the case of R(t_{1} ⋯ t_{n}), the cases of ⊥ and t_{1} = t_{2} being similar. A state A for model M satisfies the weakest existential precondition of a test R(t_{1} ⋯ t_{n}) and a formula ψ by definition of weakest existential precondition iff there is a state B with B ∈ [[R(t_{1} ⋯ t_{n})]]_{M}(A) and M ⊧ ψ [B]. By the semantic clause for atomic tests, this is the case iff M ⊧ R(t_{1} ⋯ t_{n}) [A] and M ⊧ ψ [A]. This in turn is the case iff M ⊧ R(t_{1} ⋯ t_{n}) ∧ ψ [A]. Thus, the weakest existential precondition of R(t_{1} ⋯ t_{n}) and ψ is R(t_{1} ⋯ t_{n}) ∧ ψ.

A state A for model M satisfies the weakest universal precondition of a test R(t_{1} ⋯ t_{n}) and a formula ψ by definition of weakest universal precondition iff for every state B with B ∈ [[R(t_{1} ⋯ t_{n})]]_{M}(A) it holds that M ⊧ ψ [B]. By the semantic clause for atomic tests, this is the case iff it holds that if M ⊧ R(t_{1} ⋯ t_{n}) [A] then M ⊧ ψ [A]. This in turn is the case iff M ⊧ R(t_{1} ⋯ t_{n}) → ψ [A]. Thus, the weakest universal precondition of R(t_{1} ⋯ t_{n}) and ψ is R(t_{1} ⋯ t_{n}) → ψ.

Composition

Left to the reader.

Negation

A state A for model M satisfies the weakest existential precondition of a program ¬π and a formula ψ by definition of weakest existential precondition iff there is a state B with B ∈ [[¬π]]_{M}(A) and M ⊧ ψ [B]. By the semantic clause for negation this is the case iff [[π]]_{M}(A) = ∅ and M ⊧ ψ [A]. By the induction hypothesis this is the case iff M ⊧ wup(π, ⊥) ∧ ψ [A]. Thus, the weakest existential precondition of ¬π and ψ is wup(π, ⊥) ∧ ψ.

A state A for model M satisfies the weakest universal precondition of a program ¬π and a formula ψ by definition of weakest universal precondition iff for all states B with B ∈ [[¬π]]_{M}(A) it holds that M ⊧ ψ [B]. By the semantic clause for negation this is the case iff it holds that either [[π]]_{M}(A) = ∅ or M ⊧ ψ [A]. By the induction hypothesis this is the case iff either M ⊧ wep(π, ⊤) [A] or M ⊧ ψ [A]. This is the case iff M ⊧ wep(π, ⊤) ∨ ψ [A]. Thus, the weakest universal precondition of ¬π and ψ is wep(π, ⊤) ∨ ψ.

Implication

A state A for model M satisfies the weakest existential precondition of a program π_{1} ⇒ π_{2} and a formula ψ by definition of weakest existential precondition iff there is a state B with B ∈ [[π_{1} ⇒ π_{2}]]_{M}(A) and M ⊧ ψ [B].

By the semantic clause for implication this is the case iff for all B with B ∈ [[π_{1}]]_{M}(A) it holds that [[π_{2}]]_{M}(B) ≠ ∅, and M ⊧ ψ [A]. By the induction hypothesis this is the case iff M ⊧ wup(π_{1}, wep(π_{2}, ⊤)) [A] and M ⊧ ψ [A]. This is the case iff M ⊧ wup(π_{1}, wep(π_{2}, ⊤))∧ψ [A]. Thus, the weakest existential precondition of π_{1} ⇒ π_{2} and ψ is wup(π_{1}, wep(π_{2}, ⊤))∧ ψ.

A state A for model M satisfies the weakest universal precondition of a program π_{1} ⇒ π_{2} and a formula ψ by definition of weakest universal precondition iff for all states B with B ∈ [[π_{1} ⇒ π_{2}]]_{M}(A) it holds that M ⊧ ψ [B]. By the semantic clause for implication this is the case iff either there is some state B with B ∈ [[π_{1}]]_{M}(A) and [[π_{2}]]_{M}(B) = ∅, or M ⊧ ψ [A]. By the induction hypothesis this is the case iff either M ⊧ wep(π_{1}, wup(π_{2}, ⊥)) [A] or M ⊧ ψ [A]. This is the case iff M ⊧ wep(π_{1}, wup(π_{2}, ⊥)) ∨ ψ [A]. Thus, the weakest universal precondition of π_{1} ⇒ π_{2} and ψ is wep(π_{1}, wup(π_{2}, ⊥)) ∨ ψ.

η Assignment

Left to the reader.

ι Assignment

A state A for model M satisfies the weakest existential precondition of a program ιx : π and a formula ψ by definition of weakest existential precondition iff there is a state B with B ∈ [[ιx : π]]_{M}(A) and M ⊧ ψ [B]. By the semantic clause for ι assignment, this is the case iff there is a unique d for which [[π]]_{M}(A[x := d]) ≠ ∅, and moreover for this particular d there is a state B with B ∈ [[π]]_{M}(A[x := d]) and M ⊧ ψ [B]. By the induction hypothesis this is the case iff for some x, both M ⊧ ∀y([y/x]wep(π, ⊤) ↔ y = x) [A] and M ⊧ wep(π, ψ) [A]. This is the case iff (118).

M ⊧ ∃x(∀y([y/x]wep(π, ⊤) ↔ y = x) ∧ wep(π, ψ)) [A].  (118)

Thus, the weakest existential precondition of ιx : π and ψ is (119).

∃x(∀y([y/x]wep(π, ⊤) ↔ y = x) ∧ wep(π, ψ)).  (119)

A state A for model M satisfies the weakest universal precondition of a program ιx : π and a formula ψ by definition of weakest universal precondition iff for all states B with B ∈ [[ιx : π]]_{M}(A) it holds that M ⊧ ψ [B]. By the semantic clause for ι assignment, this is the case iff it holds that if there is a unique d with [[π]]_{M}(A[x := d]) ≠ ∅, then any state B with B ∈ [[π]]_{M}(A[x := d]) will have M ⊧ ψ [B]. By the induction hypothesis this is the case iff for any x, M ⊧ ∀y([y/x]wep(π, ⊤) ↔ y = x) [A] implies M ⊧ wup(π, ψ). This is the case iff M ⊧ ∀x(∀y([y/x]wep(π, ⊤) ↔ y = x) → wup(π, ψ)) [A]. Thus, the weakest universal precondition of ιx : π and ψ is (120).

∀x(∀y([y/x]wep(π, ⊤) ↔ y = x) → wup(π, ψ)).  (120)

Quantification

We only give the reasoning for the weakest existential precondition of weak readings. A state A for model M satisfies the weakest existential precondition of a program Q^{w}x(π_{1}, π_{2}) and a formula ψ by definition of weakest existential precondition iff there is a state B with B ∈ [[Q^{w}x(π_{1}, π_{2})]]_{M}(A) and M ⊧ ψ [B]. By the semantic clause for quantification, this is the case iff the sets given by (121) and (122) are in the relation I(Q) and moreover M ⊧ ψ [A].

{d | [[π_{1}]]_{M}(A[x := d]) ≠ ∅}  (121)
{d | [[π_{1}; π_{2}]]_{M}(A[x := d]) ≠ ∅}  (122)

By the induction hypothesis and the semantic rule for ; , this is the case iff the sets given by (123) and (124) are in relation I(Q), and moreover M ⊧ ψ [A].

{d | M ⊧ wep(π_{1}, ⊤) [A]}  (123)
{d | M ⊧ wep(π_{1}, wep(π_{2}, ⊤)) [A]}  (124)

By the semantic properties of Q, this in turn is the case iff (125).

M ⊧ Qx(wep(π_{1}, ⊤), wep(π_{1}, wep(π_{2}, ⊤))) ∧ ψ.  (125)

Thus, the weakest existential precondition of Q^{w}x(π_{1}, π_{2}) and ψ is Qx(wep(π_{1}, ⊤), wep(π_{1}, wep(π_{2}, ⊤)))∧ ψ. This completes the proof that the definitions of wep and wup are indeed adequate, in other words we have established the following.

LEMMA 9.1 (wep/wup adequacy). For all M ∈ K, all states A for M, all ψ ∈ L, and all π ∈ DAL:

M ⊧ wup(π, ψ) [A] iff it holds for all B ∈ [[π]]_{M}(A) that M ⊧ ψ [B].

M ⊧ wep(π, ψ) [A] iff there is a B ∈ [[π]]_{M}(A) with M ⊧ ψ [B].

Next, we show that for all π ∈ DAL and for all ψ ∈ L we have that K ⊢ ⟨wep(π, ψ)⟩ π ⟨ψ⟩ and K ⊢ {wup(π, ψ)} π {ψ}. Again, we proceed by way of an induction argument.

Atomic Test Programs

We only prove the result for the case of R(t_{1} ⋯ t_{n}), the other atomic cases being similar. Assume K ⊧ ⟨wep(R(t_{1} ⋯ t_{n}), ψ)⟩ R(t_{1} ⋯ t_{n}) ⟨ψ⟩. By the definition of wep this is equivalent to K ⊧ ⟨R(t_{1} ⋯ t_{n}) ∧ ψ⟩ R(t_{1} ⋯ t_{n}) ⟨ψ⟩. By the existential test axiom, (126).

K ⊢ ⟨R(t_{1} ⋯ t_{n}) ∧ ψ⟩ R(t_{1} ⋯ t_{n}) ⟨ψ⟩.  (126)

For the universal case, assume (127).

K ⊧ {wup(R(t_{1} ⋯ t_{n}), ψ)} R(t_{1} ⋯ t_{n}) {ψ}.  (127)

By the definition of wup, (127) is equivalent to (128).

K ⊧ {R(t_{1} ⋯ t_{n}) → ψ} R(t_{1} ⋯ t_{n}) {ψ}..  (128)

By one of the test axioms, (129).

K ⊢ {R(t_{1} ⋯ t_{n}) → ψ} R(t_{1} ⋯ t_{n}) {ψ}.  (129)

Composition

Assume K ⊧ ⟨wep(π_{1}; π_{2}, ψ)⟩ π_{1}; π_{2} ⟨ψ⟩. By the definition of wep, this is equivalent to K ⊧ ⟨wep(π_{1}, wep(π_{2}, ψ))⟩ π_{1}; π_{2} ⟨ψ⟩. By the wep adequacy lemma, (130) and (131).

K ⊧ ⟨wep(π_{1}, wep(π_{2}, ψ))⟩ π_{1} ⟨wep(π_{2}, ψ)⟩.  (130)
K ⊧ ⟨wep(π_{2}, ψ)⟩ π_{2} ⟨ψ⟩.  (131)

By the induction hypothesis, (130) and (131) yield (132) and (133).

K ⊢ ⟨wep(π_{1}, wep(π_{2}, ψ))⟩ π_{1} ⟨wep(π_{2}, ψ)⟩.  (132)
K ⊢ ⟨wep(π_{2}, ψ)⟩ π_{2} ⟨ψ⟩.  (133)

Applying the existential composition rule to (132) and (133) gives (134).

K ⊢ ⟨wep(π_{1}, wep(π_{2}, ψ))⟩ π_{1}; π_{2} ⟨ψ⟩.  (134)

The reasoning for universal assertions about weakest universal preconditions of programs of the form π_{1}; π_{2} is similar.

Negation

Assume K ⊧ ⟨wep(¬π, ψ)⟩ ¬π ⟨ψ⟩. By the definition of wep, this is equivalent to K ⊧ ⟨wup(π, ⊥) ∧ ψ⟩ ¬π ⟨ψ⟩. By the wup adequacy lemma, (135)

K ⊧ {wup(π, ⊥)} π {⊥}.  (135)

By the induction hypothesis, (135) yields (136).

K ⊢ {wup(π, ⊥)} π {⊥}.  (136)

An application of one of the negation rules to (136) gives (137).

K ⊢ ⟨wup(π, ⊥) ∧ ψ⟩ ¬π ⟨ψ⟩.  (137)

The reasoning for universal assertions about weakest universal preconditions for programs of the form ¬π is similar.

Implication

Assume K ⊧ ⟨wep(π_{1} ⇒ π_{2}, ψ)⟩ π_{1} ⇒ π_{2} ⟨ψ⟩. By the definition of wep, this is equivalent to K ⊧ ⟨(wup(π, wep(π_{2}, ⊤)) ∧ ψ)⟩ π_{1} ⇒ π_{2} ⟨ψ⟩. By the wup and wep adequacy lemma, (138) and (139).

K ⊧ {wup(π_{1}, wep(π_{2}, ⊤))} π_{1} {wep(π_{2}, ⊤)}.  (138)
K ⊧ ⟨wep(π_{2}, ⊤)⟩ π_{2} ⟨⊤⟩.  (139)

By the induction hypothesis, (138) yields (140) and (139) yields (141).

K ⊢ {wup(π_{1}, wep(π_{2}, ⊤))} π_{1} {wep(π_{2}, ⊤)}.  (140)
K ⊢ ⟨wep(π_{2}, ⊤)⟩ π_{2} ⟨⊤⟩.  (141)

Now apply the first rule of implication to (140), (141):

K ⊢ {wup(π_{1}, wep(π_{2}, ⊤))} π_{1} ⇒ π_{2} {ψ}.  (142)

The reasoning for universal assertions about weakest universal preconditions for programs of the form π_{1} ⇒ π_{2} is similar.

η Assignment

Assume K ⊧ ⟨wep(ηx : π, ψ)⟩ ηx : π ⟨ψ⟩. By the definition of wep this is equivalent to K ⊧ ⟨∃xwep(π, ψ)⟩ ηx : π ⟨ψ⟩. By the wep adequacy lemma, (143).

K ⊧ ⟨wep(π, ψ)⟩ π ⟨ψ⟩.  (143)

By the induction hypothesis, (143) yields (144).

K ⊢ ⟨wep(π, ψ)⟩ π ⟨ψ⟩.  (144)

An application of the existential η assignment rule to (144) gives (145).

K ⊢ ⟨∃xwep(π, ψ)⟩ ηx : π ⟨ψ⟩.  (145)

The reasoning for universal assertions about weakest universal preconditions for programs of the form ηx : π is similar. ι Assignment and Quantification

Left to the reader. We have now established the following lemma.

LEMMA 9.2 (wep/wup derivability). For all π ∈ DAL and for all ψ ∈ L,

K ⊢ ⟨wep(π, ψ)⟩ π ⟨ψ⟩ and K ⊢ {wup(π, ψ)} π {ψ}.

The rest of the proof of the completeness result is very easy. We want to show that K ⊧ F implies K ⊢ F. In case F equals φ for some φ ∈ L, K ⊧ φ implies K ⊢ φ by the K oracle rule. For the case where F equals ⟨φ⟩ π ⟨ψ⟩ the reasoning is as follows. Assume (146).

K ⊧ ⟨φ⟩ π ⟨ψ⟩.  (146)

By the wep adequacy lemma it follows from (146) that (147).

K ⊧ φ → wep(π, ψ).  (147)

From this, by the K oracle rule, (148).

K ⊢ φ → wep(π, ψ).  (148)

From the wep/wup derivability lemma we have (149).

K ⊢ ⟨wep(π, ψ)⟩ π ⟨ψ⟩.  (149)

From (148) and (149) by an application of the existential consequence rule, (150).

K ⊢ ⟨φ⟩ π ⟨ψ⟩.  (150)

By similar reasoning we derive from (151) that (152).

K ⊧ {φ} π {ψ}.  (151)
K ⊢ {φ} π {ψ}.  (152)

This completes the proof of the final result of this section.

THEOREM 9.3 (Completeness). If K ⊧ F then K ⊢ F.

10. Use of the Calculus

The discussion of weakest preconditions in Section 9 will have made clear that the rules of the calculus are given in a format particularly suited to the calculation of weakest universal and existential preconditions. To find the weakest existential precondition of a program π and a formula ψ, proceed as follows. Start with the conclusion ⟨?⟩ π ⟨⊤⟩, and apply the rules of the calculus working backwards, thus decomposing π. This will eventually produce a formula φ to fill the ? slot. Thus, as explained in Section 7, the calculus allows us to calculate the static meanings of (the DAL translations of) natural language example sentences. As a first example, we calculate the static meaning of the conditional donkey sentence given in (5), with DAL translation (7), which is repeated here for convenience.

(ηx : Gx; ηy : By; Hxy) ⇒ T xy.  (153)

We want to find the weakest precondition φ such that (154).

⟨φ⟩ (ηx : Gx; ηy : By; Hxy) ⇒ T xy ⟨⊤⟩.  (154)

According to the existential rule for implication, the formula φ we are looking for is the weakest formula for which we can find a ψ satisfying the following:

\begin{matrix}\begin{matrix}· \\ · \\ · \end{matrix} ; \{φ\} ηx : Gx; ηy : By; Hxy \{ψ\} & \begin{matrix}· \\ · \\ · \end{matrix} ; ⟨ψ⟩ T xy ⟨⊤⟩ \\ ⟨φ⟩ (ηx : Gx; ηy : By; Hxy) ⇒ T xy ⟨⊤⟩. \end{matrix}

To find φ in terms of ψ, look for a χ satisfying the following:

\begin{matrix}\begin{matrix}· \\ · \\ · \end{matrix} ; \{φ\} ηx : Gx; ηy : By \{χ\} & \begin{matrix}· \\ · \\ · \end{matrix} ; \{χ\} Hxy \{ψ\} \\ \{φ\} ηx : Gx; ηy : By \{ψ\}. \end{matrix}

Now we can compute φ in terms of χ, as follows:

\begin{matrix}{\{Gx → ∀y(By → χ)\} Gx \{∀y(By → χ)\} \atop \{∀x(Gx → ∀y(By → χ))\} ηx : Gx\{∀y(By → χ)\}} & {\{By → χ\} By \{χ\} \atop \{∀y(By → χ)\} ηy : By \{χ\}} \\ \{∀x(Gx → ∀y(By → χ))\} ηx : Gx; ηy : By \{χ\}. \end{matrix}

To find χ in terms of ψ, apply the universal axiom for atomic tests (155).

{Hxy → ψ} Hxy {ψ}.  (155)

Finally, to find ψ, we apply the existential axiom for atomic tests (156).

⟨T xy⟩ T xy ⟨⊤⟩.  (156)

Combining these results we find the end result of the whole computation (157).

∀x(Gx → ∀y(By → (Hxy → T xy))).  (157)

From the fact that the procedure calculates the weakest precondition under which (153) can succeed it follows that (157) is the static meaning of this program.

Next we show that ⇒ can be defined in terms of ; and ¬, by deriving two rules for ¬(π_{1}; ¬π_{2}) which are identical to the rules for dynamic implication. To derive the first rule of implication, assume (158) and (159).

{φ} π_{1} {ψ}.  (158)
⟨ψ⟩ π_{2} ⟨⊤⟩.  (159)

Using the two negation rules and the universal rule of sequential composition, we get the following derivation.

{\{φ\} π_{1} \{ψ\} {⟨ψ⟩ π_{2} ⟨⊤⟩ \atop \{ψ\} ¬π_{2} \{⊥\}} \atop \{φ\} π_{1}; ¬π_{2} \{⊥\}} ; ⟨φ ∧ χ⟩ ¬(π_{1}; ¬π_{2}) ⟨χ⟩.

This gives the following derived rule:

{\{φ\} π_{1} \{ψ\} ⟨ψ⟩ π_{2} ⟨⊤⟩ \atop ⟨φ ∧ χ⟩ ¬(π_{1}; ¬π_{2}) ⟨χ⟩.}

For the second rule of implication, start with (160) and (161).

⟨φ⟩ π_{1} ⟨ψ⟩.  (160)
{ψ} π_{2} {⊥}.  (161)

Applying the two rules of negation and the existential rule of sequential composition now gives the following derivation.

{⟨φ⟩ π_{1} ⟨ψ⟩ {\{ψ\} π_{2} \{⊥\} \atop ⟨ψ⟩ ¬π_{2} ⟨⊤⟩} \atop ⟨φ⟩ π_{1}; ¬π_{2} ⟨⊤⟩} ; \{φ ∨ χ\} ¬(π_{1}; ¬π_{2}) \{χ\}.

This gives the following derived rule:

{⟨φ⟩ π_{1} ⟨ψ⟩ \{ψ\} π_{2} \{⊥\} \atop \{φ ∨ χ\} ¬(π_{1}; ¬π_{2}) \{χ\}.}

Next, we derive the static meaning of (38) (under its weak reading), the translation of which is repeated here for convenience.

most^{w} v_{1}(Gv_{1}; ηv_{2} : Bv_{2}; Hv_{1}v_{2}, T v_{1}v_{2}).  (162)

We want to find the weakest precondition φ for which (163).

⟨φ⟩ most^{w} v_{1}(Gv_{1}; ηv_{2} : Bv_{2}; Hv_{1}v_{2}, T v_{1}v_{2}) ⟨⊤⟩.  (163)

By the first quantifier rule, we know that φ equals most^{w} v_{1}(ψ, χ), where ψ and χ are given by (164), (165), (166), and (167).

⟨ψ⟩ Gv_{1}; ηv_{2} : Bv_{2}; Hv_{1}v_{2} ⟨⊤⟩.  (164)
{¬ψ} Gv_{1}; ηv_{2} : Bv_{2}; Hv_{1}v_{2} {⊥}.  (165)
⟨χ⟩ Gv_{1}; ηv_{2} : Bv_{2}; Hv_{1}v_{2}; T v_{1}v_{2} ⟨⊤⟩  (166)
{¬χ} Gv_{1}; ηv_{2} : Bv_{2}; Hv_{1}v_{2}; T v_{1}v_{2} {⊥}.  (167)

Note that (165) and (167) are only there to guarantee that ψ and χ are weakest existential preconditions of the given programs with respect to ⊤. The quantifier rule says that the rule in this case would still hold if we omit (167) (by virtue of the fact that most is MON↑), but of course then there is no guarantee anymore that most v_{1}(ψ, χ) expresses the weakest existential precondition of (162) with respect to ⊤. However, if we take care not to use the consequence rules we calculate weakest preconditions anyway, so then we can omit (165) and (167) and still arrive at the weakest existential precondition of (162) with respect to ⊤.

To calculate the value of ψ, according to the existential rule of sequential composition we have to find a ψ′ satisfying the following:

\begin{matrix}\begin{matrix}· \\ · \\ · \end{matrix} ; ⟨ψ⟩ Gv_{1}; ηv_{2} : Bv_{2} ⟨ψ′⟩ & \begin{matrix}· \\ · \\ · \end{matrix} ; ⟨ψ′⟩ Hv_{1}v_{2} ⟨⊤⟩ \\ ⟨ψ⟩ Gv_{1}; ηv_{2} : Bv_{2}; Hv_{1}v_{2} ⟨⊤⟩. \end{matrix}

The following derivation gives us the value for ψ in terms of ψ′.

{⟨Gv_{1} ∧ ∃v_{2}(Bv_{2} ∧ ψ′)⟩ Gv_{1} ⟨∃v_{2}(Bv_{2} ∧ ψ′)⟩ {⟨Bv_{2} ∧ ψ′⟩ Bv_{2} ⟨ψ′⟩ \atop ⟨∃v_{2}(Bv_{2} ∧ ψ′)⟩ ηv_{2} : Bv_{2} ⟨ψ′⟩} \atop ⟨Gv_{1} ∧ ∃v_{2}(Bv_{2} ∧ ψ′)⟩ Gv_{1}; ηv_{2} : Bv_{2} ⟨ψ′⟩.}

The existential axiom for atomic tests yields that ψ′ has the value Hv_{1}v_{2}, so the outcome of the whole computation of ψ is given in (168).

Gv_{1} ∧ ∃v_{2}(Bv_{2} ∧ Hv_{1}v_{2}).  (168)

A similar derivation gives the value for χ:

Gv_{1} ∧ ∃v_{2}(Bv_{2} ∧ Hv_{1}v_{2} ∧ T v_{1}v_{2})).  (169)

Thus, we arrive at the following static meaning for (162):

most v_{1}(Gv_{1} ∧ ∃v_{2}(Bv_{2} ∧ Hv_{1}v_{2}),  (170)
Gv_{1} ∧ ∃v_{2}(Bv_{2} ∧ Hv_{1}v_{2} ∧ T v_{1}v_{2})).

One final remark on the fact that our calculus is geared to finding preconditions, given a program and an output condition. We hope to have demonstrated the usefulness of this in the above examples. However, one might also be interested in calculating postconditions (which of course is possible with the calculus). It is straightforward to check the following. For a program π which is a test, calculating the weakest existential precondition of π with respect to ⊤ is equivalent to calculating the strongest universal postcondition of π with respect to ⊤. For programs which are not tests, this equivalence breaks down, but in such cases there is a different reason for being interested in postconditions. The strongest universal postcondition with respect to ⊤ of a program π which is not a test will have free occurrences of precisely those variables that are available for external dynamic binding in programs π′ following π.

11. Dynamic Logic and (Non) Monotonicity

It is possible to characterize the difference between the languages DAL and DAL_{0} in terms of the axioms of our calculus, by adding the following rule to the calculus to make it applicable to DAL_{0} programs.

Monotonicity Rule

{φ} π_{1} {ψ} \overline{\{φ\} π_{1}; π_{2} \{ψ\}}, provided fv(φ) = ∅. This rule can be proved sound by induction on the complexity of π_{2}. In the basic case π_{2} has the form of a basic test, let us say π_{2} equals R(t_{1} ⋯ t_{n}). Then certainly one can safely conclude from {φ} π_{1} {ψ} to {φ} π_{1}; R(t_{1} ⋯ t_{n}) {ψ}, because of the fact that R(t_{1} ⋯ t_{n}) is a test and the fact that the conclusion is a conditional statement.

In the induction step, all DAL_{0} constructs which form test programs pose no difficulty, again because of the fact that the conclusion of the Monotonicity Rule is a conditional statement. Thus, the only programming constructs that could cause trouble are sequential composition and η and ι assignment.

Assume that π_{2} has the form π′; π′′. Then we can use the induction hypothesis to conclude from {φ} π_{1} {ψ} to {φ} π_{1}; π′ {ψ}, and use the induction hypothesis again to conclude from this to {φ} π_{1}; π′; π′′ {ψ}.

Assume that π_{2} has the form ηx : π′. Also assume {φ} π_{1} {ψ}, with fv(φ) = ∅. We have to show that one can safely conclude {φ} π_{1}; ηx : π′ {ψ}. First observe that the induction hypothesis gives us: from {φ} π_{1} {ψ} one can conclude {φ} π_{1}; π′ {ψ}. Thus, there is some χ with {φ} π_{1} {χ} and {χ} π′ {ψ}. Moreover, since fv(φ) = ∅, we may assume fv(χ) ⊆ av(π_{1}) (use a simple induction argument). Now it follows from the fact that program π_{1}; ηx : π′ is a DAL_{0} program that x ∉ fv(χ). Thus, ∃xχ is equivalent to χ, as the quantification over x is vacuous. Thus we can conclude from {φ} π_{1} {χ} to {φ} π_{1} {∃xχ}. From {χ} π′ {ψ}, derive with the universal rule for η assignment that {∃xχ} π′ {ψ}. Then the universal composition rule allows us to conclude that {φ} π_{1}; ηxπ′ {ψ}. The reasoning for the case of ι assignment is similar. This completes the proof of the soundness of the Monotonicity Rule for DAL_{0} programs. We can use the monotonicity rule to infer from (171) that (172).

⟨φ⟩ π_{1} ⇒ π_{2} ⟨⊤⟩.  (171)
⟨φ⟩ (π_{1}; π′_{1}) ⇒ π_{2} ⟨⊤⟩.  (172)

Conditions: the precondition formula φ should not have any free variables, and the programs in (171) and (172) should be DAL_{0} programs.

Since M ⊧ π_{1} ⇒ π_{2} [A] iff it holds that if M ⊧ π_{1} [A] then M ⊧ π_{2} [A], this shows that dynamic consequence for DAL_{0} programs is monotonic (provided no program variable is used without previous assignment). It should be noted that all DAL translations of natural language examples in this paper are indeed DAL_{0} programs where no program variables are used without previous assignment.

12. Conclusion

In this paper we have demonstrated the potential of the use of tools from programming language semantics for the semantics of natural language. While η and ι assignment can in principle be decomposed in random assignment with subsequent testing, we have two reasons for preferring the treatment we gave. In the first place, extending the treatment of definite descriptions with an account of their presuppositions (which is an obvious next move in the framework we have presented) would make a decomposition of ι assignment impossible or at least very impractical. Secondly, and more importantly, ι and η assignments are to be preferred over a decomposition in terms of random assignment plus subsequent testing because the introduction of an individual by a definite or an indefinite noun phrase gets an exact counterpart in the dynamic translation language. In other words, the real merit of ι and η assignments is that they allow faithfulness to linguistic form.

Instead of the universal and existential Hoare-style correctness statements that we employed we might have used the toolkit of dynamic logic (cf. [Harel, 1984: 497–604]). Replacing {φ} π {ψ} by φ → [π]ψ and ⟨φ⟩ π ⟨ψ⟩ by φ → ⟨π⟩ψ is all there is to such a change. Still, we prefer our notation, for several reasons. In the first place, it is less cluttered than the dynamic logic notation. Next, the full expressive power of dynamic logic is not needed for our purposes, so it seems wiser to choose a tool that fits the requirements more precisely. Finally, the static {φ} and ⟨φ⟩ statements can be used as comments to annotate DAL programs, thus providing proof outlines for deriving the static meanings of programs.

A set-up where quantifiers, negations, and implications act as tests, and where descriptions are virtually the only externally dynamic elements, will be very strict about which anaphoric links are possible. The framework as it has been set up above does correctly predict that the anaphoric links suggested by the indices in (173) are out.

No boy^{1} owned a car^{2}. ^{∗}He_{1} washed it_{2}.  (173)

The reason for this is our assumption that quantifiers act externally as tests. The binary quantifier that translates no acts externally as a test, so after the processing of the first sentence of discourse (173) we are back with the initial state, and the two pronouns in the second sentence will not get proper referents. It is well-known, however, that relaxations are necessary to deal with the external dynamic effects of symmetric quantifiers and with various cases of so-called subordination (see for example [Roberts, 1989: 683–712] and [Heim, 1990: 137–177]). Our next self-imposed task is to extend and modify the framework to deal with such cases.

Acknowledgements

This paper has benefited from helpful comments by Krzysztof Apt, Reinhard Muskens, Martin Stokhof, Johan van Benthem and Albert Visser.

References

Apt K.R. Apt, ‘Ten Years of Hoare’s Logic: A Survey—Part I’, ACM Transactions on

Programming Languages and Systems, Vol. 3, No. 4, October 1981, 431–483. J. Barwise, ‘Noun Phrases, Generalized Quantifiers and Anaphora’, in P. Gärdenfors (ed.),

Generalized Quantifiers / Linguistic and Logical Approaches, 1–29, Reidel, Dordrecht, 1987.

J. van Benthem, ‘General Dynamics’, ITLI report, Amsterdam, 1990 (to appear in Theo-

retical Linguistics). Gennaro Chierchia, ‘Anaphora and Dynamic Logic’, in M. Stokhof, J. Groenendijk &

D. Beaver (eds.), Quantification and Anaphora I, Edinburgh 1991 (DYANA deliverable R2.2.A), 37–78.

J. van Eijck, ‘The Dynamics of Description’, CWI Technical Report CS-R9143, Amsterdam, October 1991 (also in: T. van der Wouden & W. Sijtsma (eds.), Computational Linguistics in the Netherlands; Papers from the First CLIN Meeting, OTS Working Papers OTS-WP-CL-91-001, Utrecht 1991, 33–58).

G. Evans, ‘Pronouns’, in: Linguistic Inquiry, 11, 1980, 337-362. P.T. Geach, Reference and Generality / An Examination of Some Medieval and Modern

Theories , Cornell University Press, Ithaca & London, 1962 (Third revised edition:

DYNAMIC INTERPRETATION AND HOARE DEDUCTION 43

J. Groenendijk & M. Stokhof, ‘Dynamic Predicate Logic’, Linguistics and Philosophy, 14,

1991, 39–100. D. Harel, ‘Dynamic Logic’, in D. Gabbay & F. Guenthner, Handbook of Philosophical

Logic, Vol. II, Reidel, Dordrecht, 1984, 497–604. I. Heim, ‘E-Type Pronouns and Donkey Anaphora’, Linguistics and Philosophy, 13, 1990,

137–177. C.A.R. Hoare, ‘An Axiomatic Basis for Computer Programming’, Communications of the

ACM, Vol. 12, no. 10, 1969, 567–580, 583. H. Kamp, ‘A Theory of Truth and Semantic Representation’, in Groenendijk e.a. (eds.),

Formal Methods in the Study of Language, Mathematisch Centrum, Amsterdam, 1981, 277–322.

H. Kamp & U. Reyle, From Discourse to Logic, Manuscript, Institute for Computational

Linguistics, University of Stuttgart, 1990. C. Roberts, ‘Modal Subordination and Pronominal Anaphora in Discourse’, Linguistics

and Philosophy, 12, 1989, 683–721. B. Russell, ‘On Denoting’, Mind, 14, 1905, 479–493. D. Westerståhl, ‘Quantifiers in Formal and Natural Languages’, in Gabbay & Guenthner

(eds.), Handbook of Philosophical Logic, Vol. IV, Reidel, Dordrecht, 1989, 1–131.