Inference Systems for Update Semantics

Willem Groeneveld  Frank Veltman

Institute for Logic, Language and Computation Department of Philosophy University of Amsterdam

Contents

1 Introduction 230

2 Abstract Update Semantics 230 2.1 Three Notions of Consequence in Update Semantics . . . . . . . 231 2.2 Structural Properties . . . . . . . . . . . . . . . . . . . . . . . . . 234 2.3 Functional Frames . . . . . . . . . . . . . . . . . . . . . . . . . . 237 2.4 Update-Test Consequence . . . . . . . . . . . . . . . . . . . . . . 240

2.4.1 Structural Completeness for Idempotent Updates: a Gen-

eral Method . . . . . . . . . . . . . . . . . . . . . . . . . . 240 2.4.2 Functional Idempotent Updates . . . . . . . . . . . . . . . 244 2.4.3 Extension to Systems with Connectives . . . . . . . . . . 245

3 The might-systems 247 3.1 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 247 3.2 Three sequent calculi . . . . . . . . . . . . . . . . . . . . . . . . . 248 3.3 The Update-Test Logic of might . . . . . . . . . . . . . . . . . . 253

3.3.1 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . 253 3.3.2 Cut Elimination . . . . . . . . . . . . . . . . . . . . . . . 254

3.4 Starting from Ignorance . . . . . . . . . . . . . . . . . . . . . . . 255 3.5 The Test Logic of might . . . . . . . . . . . . . . . . . . . . . . . 256

4 The normally-presumably-system 256 4.1 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 256 4.2 The static logic of normally . . . . . . . . . . . . . . . . . . . . . 260

4.2.1 Unrestricted Version . . . . . . . . . . . . . . . . . . . . . 264 4.2.2 Restricted Version . . . . . . . . . . . . . . . . . . . . . . 268

5 Discussion and Further Research 272

References 273

1 Introduction

The objective of this report is to provide sound and complete inference systems for the systems of update semantics that were developed by Veltman in [11]. In that paper an update semantics is given for three different languages. Moreover, three more or less natural notions of logical consequence are defined, which make sense for all three semantical systems, and, in fact, make sense for almost any semantical system in which sentence interpretations are functions (or even relations) between information states.

Of the three notions of consequence (details below), two are substructural in the sense that they lack some structural inference rules of classical logic, most prominently Permutation and Monotony. Besides the more language specific details of the three semantical systems, these structural non-validities turn out to be the most problematic part of the completeness theorems.

In section 2 we introduce a general setting of update semantics in which the three notions of consequence can be defined. We determine their interconnections, and review their structural inferential properties (for Update-Test Consequence these structural properties were determined by van Benthem in [7]). We then devote a case study to the notion of Update-Test Consequence (called Mixed Inference in [7] and [3]), the most natural notion of consequence in an update framework. Inspired by work by van Benthem and Kanazawa, we prove a general structural completeness theorem for Update-Test consequence over update systems in which the updates are idempotent relations. All concrete systems of [11] satisfy idempotency. The proof method exploits a connection with Propositional Dynamic Logic that was observed in [3]. We also show that the method can be specialized to the case of idempotent functions. Furthermore we sketch a way in which the method may transfer to systems with connectives, and as an example we treat a variant of Kanazawa’s calculus for Update-Test consequence with relational composition (see [3]).

In section 3 the update semantics for might is treated. Sound and complete inference systems are given for all three consequence relations.

In section 4 we treat the normally, presumably system. We explain the semantics in section 4.1. In section 4.2 we show that for the fragment that only contains the Booleans and normally the three consequence relations coincide. Thus the logic of normaly is essentially static: a equivalent static semantics for this fragment is developed, and axiomatized.

Finally, in section 5 we discuss some of the remaining problems.

Since the objective of this report is to prove some technical results about the systems of update semantics in [11], we assume the reader to be familiar with that work. Although we will state the necessary definitions, for motivation we also refer to [11].

2 Abstract Update Semantics

What is update semantics? In [11] an update semantics is described as a system that interprets some set of formulae L as functions over some set of information states Σ. But as observed by van Benthem in [7], the three notions of consequence that Veltman defines for these update systems are already definable for a larger class of systems, namely those systems that interpret formulae as binary relations. In this section we will take this relational perspective. The functional systems can then be studied as a subclass.

Definition 1 Suppose L is some set of formulae.

1. A frame for L is a structure F = (Σ, ([ϕ])_{ϕ∈L}), where Σ is a set (of information states), and for each ϕ ∈ L, [ϕ] ⊆ Σ × Σ is a binary relation on Σ.

2. A functional frame is a frame F = (Σ, ([ϕ])_{ϕ∈L}) where each relation [ϕ] is a function on Σ. □

Thus frames are precisely the same structures that are called frames in modal logic (for a family of modalities L), and that are called labeled transition systems in computer science. And functional frames (called ‘update systems’ in [11]) just are special cases of frames.

2.1 Three Notions of Consequence in Update Semantics

If all you know about L, Σ, and the interpretations [ϕ] is that they form a frame, two of the three notions of consequence introduced in [11] are already definable. We first introduce some notations and terminology.

Definition 2 If L is some language, a sequent for L is an expression of the form ϕ_{1}, …, ϕ_{n} ⇒ ψ, where ϕ_{1}, …, ϕ_{n} is a finite sequence of formulae of L, and ψ is some formula of L. We allow n = 0, in which case the sequence ϕ_{1}, …, ϕ_{n} is empty, and use the symbol ϵ to refer to the empty sequence. We use X, Y, Z, possibly with subscripts, as meta variables for finite sequences over L. □

Notation 1 Let F = (Σ, ([ϕ])_{ϕ∈L}) be a frame, σ, τ ∈ Σ and ϕ, ϕ_{1}, …, ϕ_{n} ∈ L. Then

1. σ ⟶^{ϕ} τ means that (σ, τ) ∈ [ϕ]

2. σ ⟶^{ϕ_{1},...,ϕn} τ means that (σ, τ) ∈ [ϕ_{1}] ∘ ⋯ ∘ [ϕ_{n}]; here ∘ is relational composition.

3. In a functional frame F, we will also use the postfix notation σ[ϕ] for the result of applying the update function [ϕ] to the state σ. Thus in functional frames, σ[ϕ] = τ means the same as σ ⟶^{ϕ} τ; and σ[ϕ_{1}] ⋯ [ϕ_{n}] = τ means the same as σ ⟶^{ϕ_{1},...,ϕn} τ. □

Definition 3 (Acceptation) Let F = (Σ, ([ϕ])_{ϕ∈L}) be a frame, σ ∈ Σ, ϕ ∈ L. Then σ accepts ϕ, or ϕ is accepted in σ, whenever σ ⟶^{ϕ} σ. Notation: σ ∥− ϕ. □

Definition 4 (Truth and Validity of Sequents) Let F = (Σ, ([ϕ])_{ϕ∈L}) be a frame for L, σ ∈ Σ a state of F. Then we define the truth of a sequent of L in σ inductively on the number of premisses of the sequent as follows:

• F, σ ^{⊧} (ϵ ⇒ ψ) iff σ ∥− ψ

• F, σ ^{⊧} (ϕ, X ⇒ ψ) iff ∀τF: if σ ⟶^{ϕ} τ then F, τ ^{⊧} (X ⇒ ψ)

Sequent validity in F means true in all states of F; notation: F ^{⊧} (X ⇒ ψ).□

Definition 5 (Update-Test Consequence) Let F = (Σ, ([ϕ])_{ϕ∈L}) be a frame. Then ^{⊧}_{2}^{F}, or Update-Test Consequence,^{1} is defined as: ϕ_{1}, …, ϕ_{n} ^{⊧}_{2}^{F} ψ iff for all σ : F, σ ^{⊧} (ϕ_{1}, …, ϕ_{n} ⇒ ψ). □

Definition 6 (Test Consequence) On any frame F, the relation ^{⊧}_{3}^{F} is defined as: ϕ_{1}, …, ϕ_{n} ^{⊧}_{3}^{F} ψ iff for all σ, if σ ∥− ϕ_{1} and … and σ ∥− ϕ_{n} then σ ∥− ψ. This relation is called Test Consequence. □

For the third we need an extra concept, that of a ‘minimal’ information state. This is just the standard notion of generator of a generated frame in modal logic.

Definition 7 A frame F = (Σ, ([ϕ])_{ϕ∈L}) is generated if there is a unique state 0 ∈ Σ such that for each σ ∈ Σ, σ = 0 or there are ϕ_{1}, …, ϕ_{n} ∈ L such that

0 ⟶^{ϕ_{1},...,ϕn} σ.^{2} □

Now the third consequence relation can now be defined as follows.

Definition 8 (Ignorant Consequence) Let F be a generated frame with generator 0. Then ϕ_{1}, …, ϕ_{n} ^{⊧}_{1}^{F} ψ if F, 0 ^{⊧} (ϕ_{1}, …, ϕ_{n} ⇒ ψ). □

In relational frames, our definition of ^{⊧}_{2} is equivalent to

ϕ_{1}, …, ϕ_{n} ^{⊧}_{2} ψ iff rge([ϕ_{1}] ∘ ⋯ ∘ [ϕ_{n}]) ⊆ fix([ψ])

which is the notation of van Benthem (here ∘ is relational composition, rge is the operation that assigns to each binary relation its range, and fix assigns to each binary relation its set of fixed points). And in functional frames, the definition of ^{⊧}_{2} simplifies to

ϕ_{1}, …, ϕ_{n} ^{⊧}_{2} ψ iff for all σ, σ[ϕ_{1}] ⋯ [ϕ_{n}] ∥− ψ

which is Veltman’s notation in.

The three relations are related as follows.

1This notion of logical consequence is called ‘Mixed Inference’ by van Benthem and Kanazawa. Here we have chosen for the more informative name that is due to van Eijck and de Vries ([9]). Notice that the subscripts of the consequence relations are chosen in such a way as to agree with the subscripting in [11].

2The functional generated frames are called ‘expressivley complete update systems’ in the revised version of [11].

Proposition 1 (Connections)

1. On any any generated frame F, if ϕ_{1}, …, ϕ_{n} ^{⊧}_{2}^{F} ψ then ϕ_{1}, …, ϕ_{n} ^{⊧}_{1}^{F} ψ.

2. On any frame F, if ϕ_{1}, …, ϕ_{n} ^{⊧}_{2}^{F} ψ then ϕ_{1}, …, ϕ_{n} ^{⊧}_{3}^{F} ψ.

3. For any other (non-trivial) combination of i, j ∈ {1, 2, 3} there is a functional frame F which distinguishes ^{⊧}_{i} from ^{⊧}_{j}.

Proof: Straightforward. □

On the other hand, under some special circumstances the three relations do coincide.

Proposition 2 (Restricted Connections) Let F = (Σ, ([ϕ])_{ϕ∈L}) be a generated frame. Suppose the following two conditions hold in F:

• Idempotency: for all σ, τ, ϕ: if σ ⟶^{ϕ} τ then τ ⟶^{ϕ} τ

• Permutation: for all ϕ, ψ, [ϕ] ∘ [ψ] = [ψ] ∘ [ϕ]

Then the relations ^{⊧}_{1}, ^{⊧}_{2} and ^{⊧}_{3} coincide in F. Proof: For functional frames this was proven in [11] (see propositions 1.4 and 1.5 of that paper). But that proof doesn’t depend on functionality, as can be seen as follows. By proposition 1.2 above we always have that X ^{⊧}_{2} ψ implies that X ^{⊧}_{3} ψ. So we only need to show that X ^{⊧}_{1} ψ implies that X ^{⊧}_{2} ψ, and that X ^{⊧}_{3} ψ implies X ^{⊧}_{1} ψ. To see the former, suppose that X ^{⊧}_{1} ψ and suppose that σ ⟶^{X} τ; we want to show that τ ⟶^{ψ} τ. Since F is generated there must be some finite sequence Y such that 0 ⟶^{Y} σ; so 0 ⟶^{Y} σ ⟶^{X} τ. By Permutation there must be a σ′ with 0 ⟶^{X} σ′ ⟶^{Y} τ. By our assumption, σ′ ⟶^{ψ} σ′, so σ′ ⟶^{ψ} σ′ ⟶^{Y} τ, so again by Permutation, there is a τ′ with σ′ ⟶^{Y} τ′ ⟶^{ψ} τ, so by Idempotency, τ ⟶^{ψ} τ, which we were after. The implication from X ^{⊧}_{3} ψ to X ^{⊧}_{1} ψ is proven in a similar vein. □

A kind of converse of this proposition can also be proven. Clearly, if the three consequence relations coincide in F, then Idempotency holds, since always ϕ ^{⊧}_{3} ϕ, so ϕ ^{⊧}_{2} ϕ, and the latter is just a rephrasal of Idempotency. Permutation will hold ‘up to equivalence’: it need not hold in F, but it is possible to construct an equivalent frame F′ (equivalent in the sense that ^{⊧}_{i}^{F′}=^{⊧}_{i}^{F} for i = 1, 2, 3) in which Permutation does hold, but we won’t go into the details of this.

Moreover, ^{⊧}_{1} and ^{⊧}_{2} are clearly connected via the construction of generated subframes.

Proposition 3 If K is a class of frames that is closed under generated subframes, then ^{⊧}_{1}^{K} and ^{⊧}_{2}^{K} are identitical. Proof: This follows from the generated subframe lemma of section 2.3. □

2.2 Structural Properties

The structural properties of Update-Test consequence were determined by van Benthem in [7]^{3}. We produce a variant of his proof below. First notice the following. For any fixed set of formulae L, consider the class K of all frames for L. Then for any ϕ_{1}, …, ϕ_{n}, ψ ∈ L, ϕ_{1}, …, ϕ_{n} ^{|̸=}_{2}^{K} ψ, which is witnessed by the following counterframe on the natural numbers {0, …, n}:

0 ⟶^{ϕ_{1}} 1 ⟶ … ⟶ n − 1 ⟶^{ϕn} n

Here all transitions are shown, so in particular it is not the case that n ⟶^{ψ} n. Since the frame pictured is generated and refutes the sequent ϕ_{1}, …, ϕ_{n} ⇒ ψ at the root 0, this also shows that ϕ_{1}, …, ϕ_{n} ^{|̸=}_{1}^{K} ψ.^{4}

Hence ^{⊧}_{1} and ^{⊧}_{2} have no valid sequents, in contrast to ^{⊧}_{3}, for which we do have valid sequents. The latter form a fairly trivial set: ϕ_{1}, …, ϕ_{n} ^{⊧}_{3} ϕ if and only if ϕ is one of the ϕ_{1}, …, ϕ_{n} (consider a frame with one state 0 such that

0 ⟶^{ψ} 0 if and only if ψ ∈ {ϕ_{1}, …, ϕ_{n}}^{5}).

This is all as it should be: under the perspective that L is the set of meta variables that refer to the formulae of some concrete language, we don’t want that any sequent of the form ϕ ⇒ ψ with different symbols ϕ and ψ is valid, since that would yield a trivial logic. We should of course focus on sequent-rules that preserve validity of structural sequents.

We consider Update-Test consequence first.

Definition 9 (Local and Global Sequent Consequence) Let S_{1}, …, S_{n}, S be sequents for some language L and K a class of frames for L. Then

1. Γ ^{⊧}_{2l}^{K} S if for all F ∈ K, and all states σ in F , if F, σ ^{⊧} S_{1} and ... and F, σ ^{⊧} S_{n} then F, σ ^{⊧} S. (Local Consequence).

2. Γ ^{⊧}_{2}^{K} S if for all F ∈ K, if for all σ in F : F, σ ^{⊧} S_{1} and ... and F, σ ^{⊧} S_{n} then for all σ in F: F, σ ^{⊧} S. (Global Consequence). □

The perspective in [7] is global, and that also seems to be the right perspective for actual completeness proofs for some specific system of update semantics. There we are interested in the set of sequents V al(K) = {(X ⇒ ϕ) |^{⊧}_{2} X ⇒ ϕ} for some class K. Of course, ^{⊧}_{2l} and ^{⊧}_{2} are the same if there are no premisssequents, that is , ^{⊧}_{2l} X ⇒ ϕ if and only if ^{⊧}_{2} X ⇒ ϕ. But if we use a sequent calculus to axiomatize V al(K), then this calculus will normally consists of axioms that must valid sequents, and rules that must preserve sequent validity, rather than sequent truth. So we take a global perspective.

3Also see [5] and [6] for observations on various other dynamic notions of consequence.

4These observations carry over quite easily if we only consider the functional frames. Take the frame of the text and notice that al relations there are partial functions. Then add one new state, say the natural number n + 1, to the frame, and make the relations fucntions by adding transitions to this new state.

5Again, this argument carries over to functional frames with only a minor variation.

In [7] van Benthem showed that on the class of all frames ^{⊧}_{2} is completely determined by the rules Left Monotony and Cautious Cut:

{X ⇒ ψ \atop ϕX ⇒ ψ} LM

\begin{matrix}X ⇒ ϕ & XϕY ⇒ ψ \\ XY ⇒ ψ \end{matrix} CC

This was proven as follows. For any set of sequents Γ define a frame F(Γ) = (S, [.]) as follows:

• S = L^{<ω} (the set of all finite sequences of variables in L)

• [ϕ] = {(X, X) | Γ ⊢ X ⇒ ϕ} ∪ {(X, Xϕ) | X ∈ L^{<ω}}

where Γ ⊢ S means that S is derivable from Γ with only LM and CC. Completeness then follows from the observation that F(Γ), X ^{⊧} Y ⇒ ψ if and ony if Γ ⊢ XY ⇒ ψ.

And on the restricted class of functional frames we get one extra rule, Cautious Monotony:

\begin{matrix}X ⇒ ϕ & XY ⇒ ψ \\ XϕY ⇒ ψ \end{matrix} CM

Completeness can then be proven via the representation

[ϕ] = {(X, X) | Γ ⊢ X ⇒ ϕ} ∪ {(X, Xϕ) | Γ ⊬ X ⇒ ϕ}

along similar lines as the previous case.

It turns out that the reason why van Benthem has different representations for the LM, CC case and the LM, CC, CM case was accidental. If we consider a larger class of frames than just the functions, we can use the same representation.

Definition 10

1. Let F be a frame, and s and t states in F. Then s ≤ t if for all sequents X ⇒ p, if F, s ^{⊧} (X ⇒ p) then F, t ^{⊧} (X ⇒ p).

2. LC is the class of models F that satisfy the following ‘loops condition’, for all variables p: if s ⟶^{p} s and s ⟶^{p} t then s ≤ t. □

Proposition 4 CM preserves sequent-truth in F if and only if F ∈ LC. Proof: suppose F ∈ LC, and let x be a state of F such that

1. F, x ^{⊧} X ⇒ p

2. F, x ^{⊧} XY ⇒ q

3. F, x ^{|̸=} XpY ⇒ q By the last condition there must be states s, t, y such that

x ⟶^{X} s ⟶^{p} t ⟶^{Y} y

and not y ⟶^{q} y. By the first condition, s ⟶^{p} s, so by the fact that F ∈ LC, s ≤ t. Since F, t ^{|̸=} Y ⇒ q this implies that F, s ^{|̸=} Y ⇒ q, so F, x ^{|̸=} XY ⇒ q , but this contradicts the second condition. So no state in F satisfies all three conditions, so CM is true in F.

Conversely, suppose F ∉ LC. Then there are states s and t in F and a variable p such that

s ⟶^{p} s, s ⟶^{p} t, and s ≰ t

so for some Y ⇒ q, F, s ^{⊧} Y ⇒ q but F, t ^{|̸=} Y ⇒ q. But then we have that: F, s ^{⊧} ϵ ⇒ p, F, s ^{⊧} Y ⇒ q, but F, s ^{|̸=} pY ⇒ q, so CM is not true in F. □

We can now show that {LM, CC, CM} is sound and complete for the LCframes. This is a consequence of the following more general proposition.

Proposition 5 Let R be any set of sequent rules that includes LM and CC. For a set of sequents Δ define the model M_{R}(Δ) by

• |M_{R}(Δ)| is the set of all finite sequences of variables

• variables are interpreted by:

q^{∗} = {(Y, Y) | Δ ⊢_{R} Y ⇒ q} ∪ {(Y, Y q) | Y ∈ |M(Δ)|}

Then Δ ⊢_{R} X ⇒ p iff M_{R}(Δ) ^{⊧} X ⇒ p. Proof: We first show that

for all Y qX : M_{R}(Δ), X ∥− Y ⇒ q iff Δ ⊢_{R} XY ⇒ q (C)

by induction on the number of symbols in Y. If Y is empty this follows from the definition of ∗. So suppose (C) holds for all Y of lentgh n, and all q, X. If X ∥− pY ⇒ q then Xp ∥− Y ⇒ q since (X, Xp) ∈ p^{∗}, so by the IH, Δ ⊢_{R} XpY ⇒ q.

Conversely, suppose Δ ⊢_{R} XpY ⇒ q, then by the IH, Xp ∥− Y ⇒ q. If (X, X) ∉ p^{∗}, then the only p-move from X is the one to Xp, so X ∥− pY ⇒ q. If on the other hand (X, X) ∈ p^{∗}, Δ ⊢_{R} X ⇒ p. Since by assumption Δ ⊢_{R} XpY ⇒ q and CC ∈ R, Δ ⊢_{R} XY ⇒ q, so by the IH X ∥− Y ⇒ q. Since there only two p-moves from X in this case, to X and Xp, and at both X and Xp, Y ⇒ q is true, it follows that X ∥− pY ⇒ q.

By (C) we have that for all Y, q

M_{R}(Δ), ϵ ∥− Y ⇒ q iff Δ ⊢_{R} Y ⇒ q

Notice that at this stage we already have a sufficiently strong result for completeness for Ignorant Consequence, as well as for local Update -Test consequence. For global consequence, we must us Left Monotonicity, of course. Now it easily follows from LM that

Δ ⊢_{R} Y ⇒ q iff for all X : M_{R}(Δ), X ∥− Y ⇒ q

so M_{R}(Δ) ⊧ Δ. And if Δ ⊬_{R} Y ⇒ q then M_{R}(Δ), ϵ ∦− Y ⇒ q so M_{R}(Δ) |̸= Y ⇒ q. □

So this contruction is quite general after all: we only need LM and CC in the proof. And also, in the part that is sufficient for Ignorant Consequence, we need only CC.

Corollary 1 The structural rules of Ignorant Consequence are completely determined by Cautious Cut. □

Now back to our claim about Cautious Monotony. If we now want to show completeness for {LM, CC, CM} with respect to the class of frames LC, the only thing that is left to show is that M_{{LM,CC,CM}}(Δ) satifies the loops condition. That is, we have to show that

if (X, X) ∈ p^{∗} and (X, Y) ∈ p^{∗} then ∀Zq : if X ∥− Z ⇒ q then Y ∥− Z ⇒ q

Now by definition of p^{∗} we know that Δ ⊢ X ⇒ p and that Y = Xp or Y = X. The case Y = X is trivial, so suppose Y = Xp. From the truth lemma we’ve just proven it follows that if X ∥− Z ⇒ q then Δ ⊢ XZ ⇒ q. So by CM, Δ ⊢ XpZ ⇒ q, so again by the truth lemma, Xp ∥− Z ⇒ q.

It now follows from this, and van Benthem’s completeness result, that the class of fucntional frames and the class LC have the same Update-Test logic. In the next section we will take a modeltheoretic perspective on this equivalence.

Van Benthem’s result on Update Test-Consequence was extended by Kanazawa (in [3]) for a language that contains a binary connective • that is explained semantically as relational composition (we discuss this system in section 2.4.3). Kanazawa also observed that the truth conditions of sequents as given by Update-Test Consequence enable a very simpe translation into Propositional Dynamic Logic, namely

F, s ^{⊧} p_{1}, …, p_{n} ⇒ q iff F, s ^{⊧}_{pdl} [p_{1}] ⋯ [p_{n}]fix(q)

where fix is an operator that maps an action p to its set of fixed points. This may come as no surprise to the reader, since this observation motivated several of the definitions of the present paper, especially the very ‘modal’ like definition of sequent truth. In fact we will try to take the correspondence with modal logic a bit further, and see the above semantic correspondece with PDL as motivation for a way of proving completeness in a fashion that is similar to the Henkin construction in modal logic. This will be the subject of section 2.4.

2.3 Functional Frames

In this section we pay some special attention to functional frames. As we noted above, there are some much weaker contraints on the relations that nevertheless have the same structural logic as the funtional frames. We first introduce some simple and familiar modeltheoretic constructions.

There are two natural notions of subframe in the present setting: the notion of generated subframe from modal logic, and the notion of submodel from first order logic.

Definition 11 Let F_{1} = (S_{1}, [·]_{1}) and F_{2} = (S_{2}, [·]_{2}) be frames. Then F_{1} is a generated subframe of F_{2} provided:

1. S_{1} ⊆ S_{2}

2. there is a unique state 0 ∈ S_{1} such that for all s ∈ S_{2}, s ∈ S_{1} if and only

if there are ϕ_{1}, …, ϕ_{n} ∈ L such that 0 ⟶^{ϕ_{1},...,ϕn} s in F_{2}

3. for all ϕ, [ϕ]_{1} = [ϕ]_{2} ↾ S_{1}. □

So a generated subframe is a generated frame in the sense of section 2.1.

Proposition 6 (Generated Subframe Lemma) Suppose F_{1} is a generated subframe of F_{2}. Then for all states s in F_{1} and all sequents X ⇒ p:

F_{1}, s ∥− X ⇒ p iff F_{2}, s ∥− X ⇒ p

Proof: Offers no problems. □

For the right to left direction of the lemma, the conditions on generated subframes can actually be weakened. The reason for this is that the only ‘formulas’ we have to look at are sequents, which are semantically explained by a universal quantification over possible futures. Hence leaving out some of the possible futures cannot make a true sequent false. Thus the notion of submodel from first order logic is also useful.

Definition 12 Let F_{1} = (S_{1}, [·]_{1}) and F_{2} = (S_{2}, [·]_{2}) be frames. Then F_{1} is a subframe of F_{2} provided:

1. S_{1} ⊆ S_{2}

2. for all ϕ ∈ L, [ϕ]_{1} = [ϕ]_{2} ↾ S_{1} □

Proposition 7 (Subframe Lemma) Suppose F_{1} is a subframe of F_{2}. Then for all states s in F_{1} and all sequents X ⇒ p:

if F_{2}, s ^{⊧} X ⇒ p then F_{1}, s ^{⊧} X ⇒ p

Proof: straightforward. □

The subframe relation has some useful applications.

Definition 13 Let F = (S, [.]) be a frame. Define the frame F_{⊥} = (S_{⊥}, [.]_{⊥}) as follows:

1. S_{⊥} = S ∪ {⊥}, for some object ⊥ ∉ S

2. [p]_{⊥} = [p] ∪ {(s, ⊥) | s ∉ do[p]} ∪ {(⊥, ⊥)}, for all p ∈ L □

This is similar to the familiar trick for making a partial function total by adding a value ‘undefined’.

Proposition 8

1. For all s in F: F, s ^{⊧} X ⇒ p iff F_{⊥}, s ^{⊧} X ⇒ p

2. F ^{⊧} X ⇒ p iff F_{⊥} ^{⊧} X ⇒ p

Proof: since F is a subframe of F_{⊥}, the right to left direction of (1) is immediate from the Subframe Lemma. For the converse, use induction on the length of the sequent. Suppose F, s ^{⊧} ϵ ⇒ p, then s ⟶^{p} s, so s ⟶^{p}_{⊥} s, so F_{⊥}, s ^{⊧} ϵ ⇒ p. Next suppose we have a sequent qX ⇒ p with n+1 premiss occurrences, and suppose F, s ^{⊧} qX ⇒ p. Suppose s ⟶^{q}_{⊥} t. If t ∈ F then by our assumption F, t ^{⊧} X ⇒ p, so by the induction hypothesis F_{⊥}, t ^{⊧} X ⇒ p. But if t = ⊥ then also F_{⊥}, t ^{⊧} X ⇒ p, since all sequents are true at F_{⊥}, ⊥. The latter fact also suffices to derive (2) from (1). □

This proposition has an interesting corollary.

Definition 14

1. LE is the class of frames in which every [ϕ] meets the following ‘loops are endpoints’ condition: if s ⟶^{ϕ} s and s ⟶^{ϕ} t then s = t.

2. P F nc is the class of frames in which each ϕ is interpreted as a partial function.

3. F nc is the class of functional frames. □

Corollary 2 ⊧_{2}^{F nc} and ⊧_{2}^{P F nc} coincide. Proof: One direction is immedate from the fact that F nc ⊆ P F nc. For the other direction, observe that if F ∈ P F nc then F_{⊥} ∈ F nc, so any counter frame in P F nc can be turned into a counter frame in F nc, by the previous proposition. □

The operation of taking subframes also provides a simple technique of finding small counterframes. Suppose Δ ^{|̸=}_{2} p_{1}, …, p_{n} ⇒ q, then for some F, s we have F, s ^{|̸=} p_{1}, …, p_{n} ⇒ q. Then there must be a trace in F that is a witness of the falsity of p_{1}, …, p_{n} ⇒ q, that is there must be states s_{0}, …, s_{n} such that s = s_{0} ⟶^{p_{1}} s_{1} … s_{n−1} ⟶^{pn} s_{n}, but not s_{n} ⟶^{q} s_{n}. Take this trace as a separate subframe, then this is a subframe of the original frame, so Δ is still valid, but p_{1}, …, p_{n} ⇒ q is still false in s.^{6}

With minor modification, this idea also enables us to show that the class of partial functions can even be enlarged to LE without any loss:

Proposition 9 ^{⊧}_{2}^{P F nc} and ^{⊧}_{2}^{LE} coincide. Proof: Since P F nc ⊆ LE, one half of this claim is obvious. We give a sketch of the other half. Suppose Γ ^{|̸=}_{2}^{LE} p_{1}, …, p_{n} ⇒ q. Then there is an LE-frame F with F ^{⊧} Γ, but for some state s in F, F, s ^{|̸=} p_{1}, …, p_{n} ⇒ q. Consider the subframe F_{s} generated by s, then F_{s} ^{⊧} Γ, but F_{s}, s t̸ruep_{1}, …, p_{n} ⇒ q. Now use a minor variant of the technique of unravelling in modal logic: unravel this subframe in such a way that fixed points are not unravelled. Then pick out the falsifying trace in the unraveled frame. This will be a partial functional model: a situation in which s ⟶^{p} t_{1} and s ⟶^{p} t_{2}, while both t_{1} ≠ s and t_{2} ≠ s, cannot occur, since due to the nature of unraveling, one of t_{1}, t_{2} will not be in the falsifying trace; and the fact that the original frame was in LE will make sure that if one of t_{1} or t_{2} equals s, they in fact both equal s. □

6Thus there are in principle good decidability prospects for ^{⊧}_{2}. By contrast, for the standard modal simlarity type {¬, ∨, □}, ^{⊧}_{2} (‘global frame consequence’) is undecidable. See [4, page 38].

However, the previous proposition is still not the final answer to the question what the class of all frames is for which CM is correct in the sense that it preserve ⊧_{2}. As we saw in proposition 4 of the previous section, CM is also sound on the class LC.

Proposition 10 ^{⊧}_{2}^{LE}=^{⊧}_{2}^{LC}. Proof: As LE ⊆ LC it is clear that Γ ^{⊧}_{2}^{LC} S implies Γ ^{⊧}_{2}^{LE} S. For the other direction a pure modeltheoretic explanation is yet to be found, but in turns out that our considerations on completeness of the previous section are sufficient: if Γ ^{|̸=}_{2}^{LC} S, then Γ ⊬_{LM,CC,CM} S, and it then follows form van Benthem’s original proof that Γ ^{|̸=}_{2}^{F nc} S, but F nc ⊆ LE, so Γ ^{|̸=}_{2}^{LE} S. □

2.4 Update-Test Consequence

2.4.1 Structural Completeness for Idempotent Updates: a General Method

The equivalence between the update-test semantics for sequents p_{1}, …, p_{n} ⇒ q and the truth conditions in PDL of [p_{1}] ⋯ [p_{n}]fix(q) suggest that we set op the structural completeness proofs in the same way as we set up a Henkin completeness proof in modal logic. That is, the states of the canonical frame should be sets of sequents; and the actions should also be treated in the PDL fashion, by the above semantic correspondence: for sets of sequents Γ, Δ, and an action ϕ:

Γ ⟶^{ϕ} Δ iff for all X, ψ : if (ϕX ⇒ ψ) ∈ Γ then (X ⇒ ψ) ∈ Δ

This will in principle only work if it is possible to identify states with the sequents that are true in it. Or in the terminology of modal logic, if it is always possible to pass from a model to an equivalent distinguished model. And the latter happens not be the case in the present setting, at least not in general, as we shall shortly see.

In modal logic, passing to a distinguished model is a special case of filtration. Let’s copy the definion of filtration in modal logic (see [1]) to the present setting:

Definition 15 Given a frame F = (Σ, [·]) for some language L, define a relation ≡_{F} on the states of F by

s ≡_{F} t iff for all X, ϕ ∈ L : F, s ^{⊧} X ⇒ ϕ iff F, t ^{⊧} X ⇒ ϕ

For any state s, define ||s||_{≡_{F}} = {t ∈ Σ | s ≡_{F} t}, and define Σ/ ≡_{F}= {||s||_{≡_{F}} | s ∈ Σ}. Then a frame F′ = (Σ′, [·]′) is a filtration of F = (Σ, [·]) provided Σ′ = Σ/ ≡_{F}, and the relations in F′ satisfy the two conditions:

1. if s ⟶^{ϕ} t in F then ||s||_{≡_{F}} ⟶^{ϕ} ||t||_{≡_{F}} in F′

2. if ||s||_{≡_{F}} ⟶^{ϕ} ||t||_{≡_{F}} in F′ then for all X, ψ: if F, s ^{⊧} (ϕX ⇒ ψ) then

F, t ^{⊧} X ⇒ ψ □

Now of course we would like to prove the Filtration Lemma:

for all X, ϕ : F, s ^{⊧} X ⇒ ϕ iff F′, ||s|| ^{⊧} X ⇒ ϕ

but the following example shows that this is not possible in general. Consider the following frame with two distinct states 1 and 2, and all arrows shown:

A one-state frame either has a reflexive p-arrow or not; if it has then ϵ ⇒ p is true, which is false in the original frame; if it hasn’t, p ⇒ p is (trivially) true, which is also false in the original frame.

The reason for this failure is clearly the special status that Update-Test Consequence gives to the reflexive arrows in the frames. In fact, there is a special condition on frames, which is only needed in the proof of the filtration lemma for the basic sequents of the form ϵ ⇒ ϕ, under which filtration is possible:

Definition 16 (Filtration Condition) An L-frame F = (S, [·]) satisfies the Filtration Condition if for all states s ∈ S and all ϕ ∈ L:

if for all X, ψ, if F, s ^{⊧} ϕX ⇒ ψ then F, s ^{⊧} X ⇒ ψ
then F, s ^{⊧} ϵ ⇒ ϕ
□

Lemma 1 (Restricted Filtration Lemma) Suppose that F = (Σ, [·]) satisfies the Filtration Condition and that F′ = (Σ′, [·]′) is a filtration of F. Then

for all X, ϕ : F, s ^{⊧} X ⇒ ϕ iff F′, ||s||_{≡_{F}} ^{⊧} X ⇒ ϕ

Proof: Offers no problems. □

Since Idempotency is equivalent with the validity of all sequents of the form (Xϕ ⇒ ϕ), the following observation is straightforward.

Proposition 11 Idempotency implies the Filtration Condition. □

This suggests that a Henkin style method for proving completeness may work for Idempotent relations. Also, all actual systems of update semantics in [11] have the property of Idempotency, so any technique based on this constraint will be general enough to apply to all those systems.

We start from finitary deduction relations ⊢_{d} between sequents and show that, provided ⊢_{d} has some special properties, there exists a cononical frame F_{d}. First some definitions.

Definition 17 Suppose d is a set of sequent rules with ⊢_{d} its associated finitary deduction relation between sequents.

1. d is normal if for all p, X, q, X_{1}, …, X_{n}, q_{1}, …, q_{n}:

{X_{1} ⇒ q_{1}, …, X_{n} ⇒ q_{n} ⊢_{d} X ⇒ q \atop pX_{1} ⇒ q_{1}, …, pX_{n} ⇒ q_{n} ⊢_{d} pX ⇒ q}

2. The local part of d is d \ {LM}.

3. d is locally normal if its local part is normal. □

We reflect on the force (or rather weakness) of the constraint of (local) normality later on. At present only notice that under the correspondence with PDL, normality is just the K-rule, which is satisfied by any normal modal operator.

Now define a notion of syntactic update on sets of sequents as follows.

Definition 18 For any set of sequents Γ, and any finite sequence X of L, Γ[[X]] =_{df} {(Y ⇒ q) | (XY ⇒ q) ∈ Γ}. □

The idea is that Γ[[X]] prescribes which sequents must be true after doing X in a state where all sequents in Γ are rue.

Lemma 2 Suppose d is locally normal and has local part dl; let Γ be a dltheory. Then

1. Γ ⊢_{dl} pX ⇒ q iff Γ[[p]] ⊢_{dl} X ⇒ q

2. Γ[[p]] is a dl-theory

Proof: To see 1, suppose Γ ⊢_{dl} pX ⇒ q; then (pX ⇒ q) ∈ Γ since Γ is a dl-theory, so (X ⇒ q) ∈ Γ[[p]], so Γ[[p]] ⊢_{dl} X ⇒ q. The converse follows from normality. Now 2 follows from 1 and the assumption that Γ is a dl-theory. □

Lemma 3 Suppose that LM ∈ d, and that Γ is a d-theory. Then Γ[[X]] is a local d-theory that extends Γ. Proof: If dl is the local part of d, then dl ⊆ d, which implies that Γ is also a dl-theory. The first claim now follows form lemma 2.2; the second easily follows from LM. □

Next we define the canonical frame:

Definition 19 (Canonical Frame) Let d be a a set of sequent rules with local part dl. Let Γ be a d-theory. Then the canonical frame C_{d}(Γ) is defined as C_{d}(Γ) = (Σ_{d}(Γ), [·]_{d}), where

• Σ_{d}(Γ) = {Γ[[X]] | X ∈ L^{<ω}}

• [ϕ]_{d} = {(Δ, Δ′) | Δ[[ϕ]] ⊆ Δ′} □

Lemma 4 (Sequent Truth Lemma) Suppose ⊢_{d} is locally normal, and has Left Monotony, Cautious Cut and Reflexivity. Let dl be the local part of d. Then in C_{d}(Γ) the following hold:

1. C_{d}(Γ), Δ ^{⊧} X ⇒ ϕ iff Δ ⊢_{dl} X ⇒ ϕ

2. C_{d}(Γ) ^{⊧} X ⇒ ϕ iff Γ ⊢_{d} X ⇒ ϕ

Proof: We show 1 with induction on the number of premisses of the sequent. Suppose that C_{d}(Γ), Δ ^{⊧} ϵ ⇒ ϕ. Then Δ ⟶^{ϕ} Δ so Δ[[ϕ]] ⊆ Δ. By Reflexivity, (ϕ ⇒ ϕ) ∈ Δ, so (ϵ ⇒ ϕ) ∈ Δ[[ϕ]], so (ϵ ⇒ ϕ) ∈ Δ. Conversely, suppose (ϵ ⇒ ϕ) ∈ Δ. Let (X ⇒ ψ) ∈ Δ[[ϕ]], then (ϕX ⇒ ψ) ∈ Δ, so by CC, (X ⇒ ψ) ∈ Δ. This shows that Δ[[ϕ]] ⊆ Δ and hence that C_{d}(Γ), Δ ^{⊧} ϵ ⇒ ϕ.

For the induction step, suppose C_{d}(Γ), Δ ^{⊧} ϕX ⇒ ψ. By the previous two lemmas, Δ[[ϕ]] is a dl-theory and in Σ_{d}(Γ). Since Δ ⟶^{ϕ} Δ[[ϕ]], our assumption implies C_{d}(Γ), Δ[[ϕ]] ^{⊧} X ⇒ ψ. Hence by the induction hypothesis, Δ[[ϕ]] ⊢_{dl} X ⇒ ψ, so by lemma 2, Δ ⊢_{dl} ϕX ⇒ ψ.

Conversely, if Δ ⊢_{dl} ϕX ⇒ ψ then Δ[[ϕ]] ⊢_{dl} X ⇒ ψ by lemma 2. Then for all Δ′ with Δ ⟶^{ϕ} Δ′, (X ⇒ ψ) ∈ Δ′. But then the induction hypothesis gives that C_{d}(Γ), Δ ^{⊧} ϕX ⇒ ψ.

For 2, suppose that C_{d}(Γ) ^{⊧} X ⇒ ϕ, then in particular C_{d}(Γ), Γ ^{⊧} X ⇒ ϕ so Γ ⊢_{dl} X ⇒ ϕ by 1, so also Γ ⊢_{d} X ⇒ ϕ. Conversely, if Γ ⊢_{d} X ⇒ ϕ then for all Y, (Y X ⇒ ϕ) ∈ Γ by LM and the fact that Γ is a d-theory. Now any Δ in the frame is of the form Γ[[Y]] for some Y, so (X ⇒ ϕ) ∈ Δ for all Δ, so by 1, C_{d}(Γ), Δ ^{⊧} X ⇒ ϕ for all Δ, so C_{d}(Γ) ^{⊧} X ⇒ ϕ. □

Lemma 5 (Structure Lemma) All relations [ϕ]_{d} in C_{d}(Γ) are idempotent. Proof: since then (ϕ ⇒ ϕ) ∈ Δ for all Δ in the frame, the sequent truth lemma yields idempotency. □

As to the status of the constraint of normality: consider any class of frames K; let K_{gen} be the closure of K under generated subframes. Since the generation theorem holds for our sequent semantics (see the previous section), we have that the local consequence relations ^{⊧}_{2l}^{K} and ^{⊧}_{2l}^{K_{gen}} are the same. Now it is simple to show that ^{⊧}_{2l}^{K_{gen}} is normal. Thus,

Proposition 12 If a deduction relation ⊢_{d} is sound and complete for ^{⊧}_{2l}^{K}, then ⊢_{d} is normal. □

It is at present not clear whether something similar holds for global consequence:

Conjecture 1 If ⊢_{d} is sound and complete for ^{⊧}_{2}^{K}, then ⊢_{d} is locally normal.

If the conjecture is true then the assumption of local normality in our completeness construction is quite weak. A possible route of proving the conjecture would be to transform ⊢_{d} into a normal form consisting of the rule LM plus some set of rules that are sound for local consequence.

2.4.2 Functional Idempotent Updates

The above method can be specialized to the case that also the rule Cautious Monotony:

\begin{matrix}X ⇒ p & XY ⇒ q \\ XpY ⇒ q \end{matrix} CM

is present. Of course the previous method is still available, and it will yield a canonical frame that satisfies the Loops Condition (see section 2.3). But now there is the possibility of making the relations functional in the canonical frame, by letting the relations in the frame coincide with the syntactic updates.

Definition 20 (Functional Canonical Frame) Let d be a a set of sequent rules with local part dl. Let Γ be a d-theory. Then the functional canonical frame F_{d}(Γ) is defined as F_{d}(Γ) = (Σ_{d}(Γ), [·]_{d}), where

• Σ_{d}(Γ) = {Γ[[X]] | X ∈ L^{<ω}}

• [ϕ]_{d} = {(Δ, Δ′) | Δ[[ϕ]] = Δ′} □

It is immediately clear that all relations are functions in F_{d}, so the question arises where the rule CM actually comes in. This turns out to be only in the atomic case of the sequent truth lemma, where we have to show that

F_{d}, Δ ^{⊧} ϵ ⇒ ϕ iff Δ ⊢_{dl} ϵ ⇒ ϕ

which comes dow to proving that

Δ[[ϕ]] = Δ iff (ϵ ⇒ ϕ) ∈ Δ

Now the inclusion Δ[[ϕ]] ⊆ Δ is proven just as in the general case with RR and CC, but for the converse Δ ⊆ Δ[[ϕ]] we need CRM. Suppose (ϵ ⇒ ϕ) ∈ Δ, and let (X ⇒ ψ) ∈ Δ, then by CM, (ϕX ⇒ ψ) ∈ Δ, so (X ⇒ ψ) ∈ Δ[[ϕ]].

The rest of the proof remains as before.

Lemma 6 (Functional Sequent Truth Lemma) Suppose ⊢_{d} is locally normal, and has LM, CC, RR and CM. Let dl be the local part of d. Then in F_{d}(Γ) the following hold:

1. F_{d}(Γ), Δ ^{⊧} X ⇒ ϕ iff Δ ⊢_{dl} X ⇒ ϕ

2. F_{d}(Γ) ^{⊧} X ⇒ ϕ iff Γ ⊢_{d} X ⇒ ϕ

Proof: see the general case for the remaining details. □

2.4.3 Extension to Systems with Connectives

Ideally, we would like to see the methods of the previous two sections to be the basis of completeness theorems for actual semantic systems in which there are also connectives present. We will first treat an example, and then set out a general pattern.

In [3], Kanazawa gives a completeness result for a language with only a binary connective •, which is semantically explained as relational composition.

Definition 21 (Language and Semantics) The language is now complex, and is the closure of some set of atoms A under the binary connective •. The frames are as before structures F = (Σ, [·]), but with the understanding that [·] now only interprets atomic formulae as arbitrary binary relations over Σ, and that this interpretation is inherited by complex formule ϕ•ψ via the stipulation [ϕ • ψ] =_{df} [ϕ] ∘ [ψ]. □

Now Kanazawa proves that ^{⊧}_{2} over the class of all frames is completely axiomatized by the following sequent calculus M(•):

{X ⇒ ψ \atop ϕX ⇒ ψ} [LM]  \begin{matrix}X ⇒ ϕ & XϕY ⇒ ψ \\ XY ⇒ ψ \end{matrix} [CC]

{XϕψY ⇒ χ \atop Xϕ • ψY ⇒ χ} [• ⇒_{1}]  {Xϕ • ψY ⇒ χ \atop XϕψY ⇒ χ} [• ⇒_{2}]

\begin{matrix}X ⇒ ϕ & X ⇒ ψ \\ X ⇒ ϕ • ψ \end{matrix} [⇒ •_{1}]  \begin{matrix}Xϕ ⇒ ψ & X ⇒ ϕ • χ \\ X ⇒ (ϕ • ψ) • χ \end{matrix} [⇒ •_{2}]

\underline{X ⇒ ϕ[α • (β • γ)]} ; X ⇒ ϕ[(α • β) • γ] [⇒ Assoc•] ↓↑ both ways

Now consider a variant I(•) of this calculus, with Reflexivity added:

Xϕ ⇒ ϕ RR

\begin{matrix}{X ⇒ ψ \atop ϕX ⇒ ψ} [LM] & \begin{matrix}X ⇒ ϕ & XϕY ⇒ ψ \\ XY ⇒ ψ \end{matrix} [CC] \\ {XϕψY ⇒ χ \atop Xϕ • ψY ⇒ χ} [• ⇒_{1}] & {Xϕ • ψY ⇒ χ \atop XϕψY ⇒ χ} [• ⇒_{2}] \end{matrix}

From the form of the rules it follows that the calculus I(•) is locally normal. Also notice that there are only two rules left for •, but that the other •-rules of M(•) are derivable in I(•) with the help of Reflexivity and Cautious Cut. We leave the verification of this to the reader.

Since I(•) is locally normal, and has CC and RR for all formulae we can define the canonical frame just as before, where the atomic relations are defined by

Γ ⟶^{p} Δ iff Γ[[p]] ⊆ Δ

Now all constructions and proofs carry over provided we can also show for all formulae that

Γ ⟶^{ϕ} Δ iff Γ[[ϕ]] ⊆ Δ

especially for complex formulae involving •. This essentailly boils down to proving that

Γ[[ϕ • ψ]] = Γ[[ϕ]][[ϕ]]

which is straightforward given the rules for •. We leave the details to the reader.

There is one aspect in which this example of a system with connectives is not representative, and that is the fact that in the semantic exlanation of • as relational composition no specific structure of the state space is used. Thus in order to prove that the canonical frame has the right structural properties we only have to show Idempotency of the relations, which simply follows from the fact that the Refexivity rule holds for all formulae. If on the other hand we have a semantics that uses some algebraic structure over the state space in the semantic explanation of some connectives, the proof that the canonical frame reproduces this algebraic structure may be quite involved.

The general outline of our tehnique for a system with connectives is as follows. Suppose we have a language L, which is the closure over a set of atoms A under the connectives c_{1}, …, c_{n} which have arity a_{1}, …, a_{n}, repectively. We want to prove completeness of some calculus ⊢_{d} for some class K of frames F = (Σ, f_{1}, …, f_{n}, [·]) that interprete connective c_{i} by the operation f_{i} via the stipulation that

[c_{i}(ϕ_{1}, …, ϕ_{a_{i}}] = f_{i}([ϕ_{1}], …, [ϕ_{a_{i}}])

Then it seems that our structural completeness method can be specialized as follows.

The basic assumptions that have to obtain are:

Basic Assumptions:

• Deduction Calculus: ⊢_{d} is locally normal, and has LM, CC and RR.

• Semantics: in any frame in K, each [ϕ] is an idempotent relation

We define the ‘base’ of the canonical frame as before: Σ_{d} is the set of all d-theories, and atoms p are interpreted by [p]_{d} = {(Γ, Δ) | Γ[[p]] ⊆ Δ}.

Then the two essental lemmas that have to be proven are

Structure Lemma: there are operations f_{i} such that C_{d} = (Σ_{d}, f_{1}, …, f_{n}, [·]_{d}) is a frame of K.

Dynamic Valuation Lemma: In the canonical frame C_{d} we have for all formulae ϕ that

Γ ⟶^{ϕ} Δ iff Γ[[ϕ]] ⊆ Δ

This latter lemma together with the basic assumptions will enable you to prove the Sequent Truth Lemma just as before, and then the Structure Lemma and standard argumentation yield completeness. The logical rules of ⊢_{d} for the connectives will of course play a major role in the proofs of the Structure Lemma and the Dynamic Valuation Lemma.

Ideally, the completeness proofs in the next sections of the actual update systems with Update-Test Consequence should be dressed in the above format. Though we presently think that this is a viable way, we have not yet found a smooth way of reproducing the algebraic structure which is needed in the proof of the structure lemma. For this reason we have chosen to give the original proofs of [10], rather than messy proofs in the general format.

3 The might-systems

3.1 Semantics

We review the definitions of the update semantics of might from [11].

Definition 22 (Language) Given a finite set of atoms A, L_{0}^{A} is the closure of A under the Booolean connectives ¬, ∨, ∧. L_{1}^{A} = L_{0}^{A} ∪ {might ϕ | ϕ ∈ L_{0}^{A}}. □

So might only occurs as outermost operator.

Definition 23 (Semantics) Given a finite set of atoms A, the set of possible worlds for A is W =_{df} P ow(A). The set of information states is Σ =_{df} P ow(W). The minimal information state is 0 =_{df} W. The update functions are inductively defined as functions from states to states as follows:

1. σ[p] = {w ∈ σ | p ∈ w}

2. σ[¬ϕ] = σ \ σ[ϕ]

3. σ[ϕ ∧ ψ] = σ[ϕ] ∩ σ[ψ]

4. σ[ϕ ∨ ψ] = σ[ϕ] ∪ σ[ψ]

5. σ[might ϕ] = \{ \begin{matrix}∅ & if σ[ϕ] = ∅ \\ σ & otherwise \end{matrix}

□

So in the terminology of section 2 we have defined one specific functional generated frame U = (Σ, [.]). Apply the three definitions of consequence to this frame and what we get is:

Definition 24 (Consequence)

1. ϕ_{1}, …, ϕ_{n} ^{⊧}_{1} ψ iff 0[ϕ_{1}] ⋯ [ϕ_{n}] ∥− ψ

2. ϕ_{1}, …, ϕ_{n} ^{⊧}_{2} ψ iff for all σ, σ[ϕ_{1}] ⋯ [ϕ_{n}] ∥− ψ

3. ϕ_{1}, …, ϕ_{n} ^{⊧}_{3} ψ iff for all σ, if σ ∥− ϕ_{1}, …, σ ∥− ϕ_{n} then σ ∥− ψ

3.2 Three sequent calculi

We present the three sequent calculi of [10]. As to the differences between the three logics of might, observe that

¬p, might p ^{⊧}_{2} ⊥ and might p, ¬p ^{|̸=}_{2} ⊥

but

¬p, might p ^{⊧}_{3} ⊥ and might p, ¬p ^{⊧}_{3} ⊥

So ^{⊧}_{2} and ^{⊧}_{3} are different, and Permutation fails for ^{⊧}_{2}. In fact it will be a property of the layout of the sequents systems given below for ^{⊧}_{2} and ^{⊧}_{3} that they only differ in the structural inference rules.

Also, ^{⊧}_{1} is distinct from ^{⊧}_{2}, since

p ^{⊧}_{1}might q, but p ^{|̸=}_{2}might q

In fact it is not hard to show that for L_{0} conclusions ψ, ^{⊧}_{1} and ^{⊧}_{2} behave the same:

ϕ_{1}, …, ϕ_{n} ^{⊧}_{1} ψ iff ϕ_{1}, …, ϕ_{n} ^{⊧}_{2} ψ

This fact will also be reflected in the systems below: the systems for ^{⊧}_{1} and ^{⊧}_{2} will only differ in the right-introducing might-rules.

We treat the structural rules first. Consider these five rules:

Πϕ ⇒ ϕ RR \begin{matrix}Π ⇒ ϕ & Π, ϕ, Π′ ⇒ ψ \\ Π, Π′ ⇒ ψ \end{matrix} CC \begin{matrix}Π ⇒ ϕ & Π, Π′ ⇒ ψ \\ Π, ϕ, Π′ ⇒ ψ \end{matrix} CM

{Π, ϕ, ψ, Π′ ⇒ χ \atop Π, ψ, ϕ, Π′ ⇒ χ} P ERM {Π, Π′ ⇒ ψ \atop Π, ϕ, Π′ ⇒ ψ} Mon

These are devided over the three systems as follows:

• ⊢_{1}: RR, CC, CM, Perm for ϕ, ψ ∈ L_{0}, Mon for ψ ∈ L_{0} or ϕ =might χ.

• ⊢_{2}: the same as for ⊢_{1}.

• ⊢_{3}: RR, CC, CM, Perm, Mon.^{7}

What may be surprising about the system ⊢_{2} is that in this presentation, Left Monotonicity is not a rule, while we have seen in section 2 that it is a characteristic rule for Update-Test Consequence. But it turns out that LM is admissible for ⊢_{2}. We will prove this after we have presented the whole system.

All three systems contain the same, classical, rules for the Boolean connectives. In these rules all formulae involved must be L_{0} formulae:

\begin{matrix}Π ⇒ ϕ & Π ⇒ ψ \\ Π ⇒ ϕ ∧ ψ \end{matrix} R∧ {Π, ϕ ⇒ χ \atop Π, ϕ ∧ ψ ⇒ χ} L ∧ 1 {Π, ψ ⇒ χ \atop Π, ϕ ∧ ψ ⇒ χ} L ∧ 2

7Of course, CM is not realy needed for ⊢_{3} since it follows from Mon; the rule is included to facilitate comparison with the other systems.

{Π ⇒ ϕ \atop Π ⇒ ϕ ∨ ψ} R ∨ 1 {Π ⇒ ψ \atop Π ⇒ ϕ ∨ ψ} R ∨ 2 \begin{matrix}Π, ϕ ⇒ χ & Π, ψ ⇒ χ \\ Π, ϕ ∨ ψ ⇒ χ \end{matrix} L∨
{Π, ϕ ⇒ ⊥ \atop Π ⇒ ¬ϕ} L¬ Π, ϕ, ¬ϕ ⇒ ⊥ P C {Π, ϕ ⇒ χ \atop Π, ¬¬ϕ ⇒ χ} ¬¬

Actually the condition that all formulae involved must be L_{0} can be weakened in several cases, but for reasons of uniformity we have chosen not too, since these are not the same cases for all three systems. One example of a rule in which the condition is necessary is the left ∨- rule in the case of ⊢_{3}: we have both ¬p, might p ⊢_{3} p and p, might p ⊢_{3} p; but an unrestricted left ∨-rule would then imply that p ∨ ¬p, might p ⊢_{3} p, hence might p ⊢_{3} p, but might p ^{|̸=}_{3} p.

Finally the might-rules. For ⊢_{1} these are:

Δ ⇒ ϕ_{1} … Δ ⇒ ϕ_{n} Δ ⇒ ψ ϕ_{1}, …, ϕ_{n} ⇒might ψ Δ {Π, ϕ ⇒ ⊥ \atop Π, might ϕ ⇒ ⊥} Lm⊥ {Π ⇒ ⊥ \atop Π ⇒ ψ} m − efsq

In the first rule, Δ has to be a diagram (a formula that picks out a unique world, see definition 25 below), and ϕ_{1}, …, ϕ_{n}, ψ ∈ L_{0}. The Ex Falso rule is already derivable from the logical rules for ψ ∈ L_{0}, but is also needed for ψ =might χ.

⊢_{2} and ⊢_{3} have the same logical rules for might, namely:

{Π ⇒ ϕ \atop Π ⇒might ϕ} Rm {Π, ϕ ⇒ ⊥ \atop Π, might ϕ ⇒ ⊥} Lm⊥ {Π ⇒ ⊥ \atop Π ⇒ ψ} m − efsq

Π ⇒might ψ Π, ψ ⇒ ϕ Π, ϕ ⇒might ψ m − Mon Π, ϕ ⇒ ψ Π, might ϕ ⇒might ψ LRm

We leave the verification of soundness to the reader.

Theorem 1 (Soundness) If ⊢_{i} Π ⇒ ϕ then Π ^{⊧}_{i} ϕ, for i ∈ {1, 2, 3}. □

We will now show that LM is an admssible rule for ⊢_{2}. Any instance of LM of the form Σ ⇒ ψ/ might ϕΣ ⇒ ψ is just a special case of Mon. So it remains to prove the case in which we add an L_{0}-premiss.

Lemma 7 If ϕ ∈ L_{0} and ⊢_{2} Π ⇒ ψ then ⊢_{2} ϕ, Π ⇒ ψ. Proof: Induction on the length of the derivation. If Π ⇒ ψ is an axiom (RR or P C) then ϕΠ ⇒ ψ is also an axiom since ϕ ∈ L_{0}. For the induction step use the induction hypothesis and the fact that in every rule of ⊢_{2}, all sequents involved in that rule have the same left context ‘Π’, possibly constrained to be L_{0}; but since ϕ ∈ L_{0}, replacing the context ‘Π’ by ‘ϕΠ’ will also yield an instance of the rule. □

That we have full Left Monotony also implies that for pure L_{0}-sequents we also have full Monotony:

\begin{matrix}{Π, Π′ ⇒ ψ \atop ϕ, Π, Π′ ⇒ ψ} & LM \\ Π, ϕ, Π′ ⇒ ψ \end{matrix} ; P erm

And also for L_{0}-sequents we have that the normal Cut rule is derivable:

\begin{matrix}Π ⇒ ϕ & {ϕ, Π′ ⇒ ψ \atop Π, ϕ, Π′ ⇒ ψ} LM \\ Π, Π′ ⇒ ψ \end{matrix} ; CC

These two facts imply, amongst other things, the following.

Proposition 13 For any L_{0}-sequent Π ⇒ ϕ such that ⊢ Π ⇒ ϕ in classical logic, also ⊢_{i} Π ⇒ ϕ for i ∈ {1, 2, 3}. Proof: Left to the reader. □

In fact the converse is also true.

In order to make sense of the might-rules for ⊢_{1}, we must say what a diagram is.

Definition 25 Fix some enumeration p_{1}, …, p_{n} of the finite set of atoms A. Then a diagram is a sequence Δ = δ_{1}, …, δ_{n} such that either δ_{i} = p_{i} or δ_{i} = ¬p_{i}. If w is a possible world then its associated diagram Δ_{w} satisfies δ_{i} = p_{i} iff p_{i} ∈ w. □

We stated before that the might-rules of ⊢_{2} are derived rules of ⊢_{1}. This can be shown by first observing that

if ϕ_{1}, …, ϕ_{n}, ψ ⊬_{1} ⊥ then ϕ_{1}, …, ϕ_{n} ⊢_{1}might ψ (F)

This fact (F) is specific for ⊢_{1} and will be proven in section 3.4.

Proposition 14 Rm, LRm and m − Mon are derived rules of ⊢_{1}. Proof: For Rm, suppose that Π ⊢_{1} ϕ. If Π ⊢_{1} ⊥ then by m−efsq, Π ⊢_{1}might ϕ. On the other hand, if Π ⊬_{1} ⊥ then by CC and our assumption, Π, ϕ ⊬_{1} ⊥, so by fact (F) above, Π ⊢_{1}might ϕ.

For LRm, suppose that Π, ϕ ⊢_{1} ψ, and first consider the case that Π, ϕ ⊢_{1} ⊥. Then by Lm⊥ and m − efsq, Π, might ϕ ⊢_{1}might ψ. next consider the cae that Π, ϕ ⊬_{1} ⊥, then by fact (F), Π ⊢_{1}might ϕ. Now consider the following derivation:

Π, might ϕ, ψ ⇒ ⊥ Π ⇒might ϕ

Π, ψ ⇒ ⊥ CC

Π, ϕ, ψ ⇒ ⊥ Mon Π, ϕ ⇒ ψ

Πϕ ⇒ ⊥ CC

The application of Mon is warranted since ⊥ is an L_{0} formula. The derivation shows that under our current assumptions, Π, might ϕ, ψ ⊬_{1} ⊥, so by fact (F), Π, might ϕ ⊢_{1}might ψ, which we were after.

To see that m − Mon holds, assume that Π ⊢_{1}might ψ and Π, ψ ⊢_{1} ϕ. In case that Π, ϕ, ψ ⊬_{1} ⊥, the fact (F) proves that Π, ϕ ⊢_{1}might ψ. The case that Π, ϕ, ψ ⊢_{1} ⊥ is proven by the follwoing derivation:

\begin{matrix}{Π, ϕ, ψ ⇒ ⊥ \atop Π, ψ, ϕ ⇒ ⊥} P erm & Π, ψ ⇒ ϕ \\ Π, ψ ⇒ ⊥ \end{matrix} CC
Π, might ψ ⇒ ⊥

Lm⊥

Π ⇒might ψ

Π ⇒ ⊥ CC

Π, ϕ ⇒ ⊥ Mon

Π, ϕ ⇒might ψ m − efsq

□

We end this section by proving some lemmas on diagrams that hold for all three systems and that will play a role in the completeness proofs to be given below. Informally, the reason that these lemmas hold for all three systems is that they only involve the Boolean rules (which are the same for all three systems) and the weak forms of the structural rules. In the following four lemmas, ⊢ is any of the three consequence relations described above.

Lemma 8 Let Δ be a diagram.

1. Δ ⊬ ⊥

2. for every ϕ ∈ L_{0}, Δ ⊢ ϕ or Δ, ϕ ⊢ ⊥

3. (a) Δ ⊢ p iff p occurs in Δ

(b) Δ ⊢ ϕ ∧ ψ iff Δ ⊢ ϕ and Δ ⊢ ψ

(c) Δ ⊢ ϕ ∨ ψ iff Δ ⊢ ϕ or Δ ⊢ ψ

(d) Δ ⊢ ¬ϕ iff Δ, ϕ ⊢ ⊥

Proof: Item 1 follows form the soundness theorem(s). 2 is proven by induction on ϕ; we do two cases. If ϕ is atomic, say ϕ = p, then we have that either p or ¬p occurs in Δ; if p occurs in Δ then Δ ⊢ p by RR and P erm; and if ¬p occurs in Δ then Δ, p ⊢ ⊥ by P C and P erm. Suppose ϕ = ψ ∨ χ, and assume Δ ⊬ ψ ∨ χ, then by the right ∨ rules, Δ ⊬ ψ, and Δ ⊬ χ, so by the induction hypothesis, Δ, ψ ⊢ ⊥ and Δ, χ ⊢ ⊥, so by the left ∨-rule, Δ, ψ ∨ χ ⊢ ⊥. The oter ases are similar.

Item 3 is also relatively straightforward , and we do only one case by way of llustration. Suppose Δ ⊢ ϕ ∨ ψ, but Δ ⊬ ϕ nad Δ ⊬ ψ, then by 2, Δ, ϕ ⊢ ⊥ and Δ, ψ ⊢ ⊥, so by the left ∨ rule, Δ, ϕ ∨ ψ ⊢ ⊥; but now CC and our assumption yield that Δ ⊢ ⊥ which contradicts 1. □

Lemma 9 Let σ ⊆ W and ϕ ∈ L_{0}. Then σ[ϕ] = {w ∈ σ | Δ_{w} ⊢ ϕ}. Proof: By induction on ϕ and the previous lemma. □

Lemma 10 Suppose ϕ_{1}, …, ϕ_{n} ∈ L_{0} and ϕ_{1}, …, ϕ_{n} ⊬ ⊥. Then there exists a diagram Δ such that ϕ_{1}, …, ϕ_{n}, Δ ⊬ ⊥, and Δ ⊢ ϕ_{i} for every ϕ_{i}.

Proof: Assume some enumeration p_{1}, …, p_{k} of the set of atoms A. Define Δ = δ_{1}, …, δ_{k} by

δ_{i+1} = \{ \begin{matrix}p_{i+1} & if ϕ_{1}, …, ϕ_{n}, δ_{1}, …, δ_{i}, p_{i+1} ⊬ ⊥ \\ ¬p_{i+1} & otherwise \end{matrix}

Assume as induction hypothesis ϕ_{1}, …, ϕ_{n}, δ_{1}, …, δ_{i} ⊬ ⊥. Now suppose that ϕ_{1}, …, ϕ_{n}, δ_{1}, …, δ_{i+1} ⊢ ⊥. Then δ_{i+1} = ¬p_{i+1} and both

ϕ_{1}, …, ϕ_{n}, δ_{1}, …, δ_{i}, p_{i+1} ⊢ ⊥ and ϕ_{1}, …, ϕ_{n}, δ_{1}, …, δ_{i}, ¬p_{i+1} ⊢ ⊥

so

ϕ_{1}, …, ϕ_{n}, δ_{1}, …, δ_{i}, p_{i+1} ∨ ¬p_{i+1} ⊢ ⊥

Since everything is L_{0}, we have (from classical logic) that

ϕ_{1}, …, ϕ_{n}, δ_{1}, …, δ_{i} ⊢ p_{i+1} ∨ ¬p_{i+1}

Hence by Cautious Cut, a contradiction with the induction hypothesis arises.

This establishes that ϕ_{1}, …, ϕ_{n}, Δ ⊬ ⊥. Now by lemma 8, either Δ ⊢ ϕ_{i} or Δ, ϕ_{i} ⊢ ⊥. But the latter would imply, with Mon for L_{0}-conclusions and Perm, that ϕ_{1}, …, ϕ_{n}, Δ ⊢ ⊥. So Δ ⊢ ϕ_{i}. □

Lemma 11 Suppose ϕ_{1}, …, ϕ_{n} ⊬ ⊥. Then

0[ϕ_{1}] ⋯ [ϕ_{n}] = {w | θ_{1}, …, θ_{k}, Δ_{w} ⊬ ⊥}

where θ_{1}, …, θ_{k} are the L_{0}-formulae in ϕ_{1}, …, ϕ_{n}. Proof: Induction on n. If n = 0, we have that 0 = W = {w ∈ W | Δ_{w} ⊬ ⊥}.

In the case that n = m + 1 we consider two cases. Case 1: ϕ_{m+1} ∈ L_{0}. Let θ_{1}, …, θ_{j} be the L_{0}-formulae among ϕ_{1}, …, ϕ_{m}. Suppose that w ∈ 0[ϕ_{1}] ⋯ [ϕ_{m+1}]. By lemma 9 this is equivalent to

w ∈ 0[ϕ_{1}] ⋯ [ϕ_{m}] and Δ_{w} ⊢ ϕ_{m+1}

By the induction hypothesis this is equivalent to

θ_{1}, …, θ_{j}, Δ_{w} ⊬ ⊥ and Δ_{w} ⊢ ϕ_{m+1}

By the structural rules CC and CM, the latter is equivlent to

θ_{1}, …, θ_{j}, ϕ_{m+1}, Δ_{w} ⊬ ⊥

which we were after.

Case 2: ϕ_{m+1} =might ψ. First suppose that 0[ϕ_{1}] ⋯ [ϕ_{m}][ψ] = ∅. Then by lemma 9 there are no worlds w such that w ∈ 0[ϕ_{1}] ⋯ [ϕ_{m}] and Δ_{w} ⊢ ψ. So by the induction hypothesis, there is no w such that θ_{1}, …, θ_{j}, Δ_{w} ⊬ ⊥ and Δ_{w} ⊢ ψ. This means that for every diagram Δ we have that θ_{1}, …, θ_{j}, ψ, Δ ⊢ ⊥ so by lemma 10, θ_{1}, …, θ_{j}, ψ ⊢ ⊥; but then by the might-rule ml⊥ we have θ_{1}, …, θ_{j}, might ψ ⊢ ⊥, so by Mon, ϕ_{1}, …, ϕ_{m+1} ⊢ ⊥, contradiction.

Next suppose that 0[ϕ_{1}] ⋯ [ϕ_{m}][ψ] ≠ ∅. Then 0[ϕ_{1}] ⋯ [ϕ_{m}][might ψ] = 0[ϕ_{1}] ⋯ [ϕ_{1}], and we can apply the induction hypothesis. □

3.3 The Update-Test Logic of might

3.3.1 Completeness

Theorem 2 If ϕ_{1}, …, ϕ_{n} ^{⊧}_{2} ψ then ϕ_{1}, …, ϕ_{n} ⊢_{2} ψ. Proof: Suppose that ϕ_{1}, …, ϕ_{n} ⊬_{2} ψ. Let θ_{1}, …, θ_{k} be the L_{0} formulae in ϕ_{1}, …, ϕ_{n}, and distinguish two cases about complexity of ψ.

Case 1: ψ ∈ L_{0}. We want to show that for some σ, σ[ϕ_{1}] ⋯ [ϕ_{n}] ∥− −̸ ψ; we will actually show that we can take σ = 0 in this case. Observe that θ_{1}, …, θ_{k}, ¬ψ ⊬_{2} ⊥, since otherwise θ_{1}, …, θ_{k} ⊢_{2} ψ and then by monotony for L_{0} conclusions ϕ_{1}, …, ϕ_{n} ⊢_{2} ψ, contrary to our assumption. So θ_{1}, …, θ_{k}, ¬ψ ⊬_{2} ⊥, so by lemma 8 and lemma 10, there must be some diagram Δ_{w} such that θ_{1}, …, θ_{k}, Δ_{w} ⊬_{2} ψ. But then by lemma 11, w ∈ 0[ϕ_{1}] ⋯ [ϕ_{n}], but by lemma 9, w ∉ 0[ϕ_{1}] ⋯ [ϕ_{n}][ψ].

Case 2: ψ =might χ. Define a state σ by

σ = 0[¬(θ_{1} ∧ ⋯ ∧ θ_{k} ∧ χ)]

We will show that σ[ϕ_{1}] ⋯ [ϕ_{n}] ∥− −̸might χ. This will be true if

1. σ[ϕ_{1}] ⋯ [ϕ_{n}] ≠ ∅

2. σ[ϕ_{1}] ⋯ [ϕ_{n}][χ] = ∅

It is easy to see that 2 must hold: since ¬(θ_{1} ∧ ⋯ ∧ θ_{k} ∧ χ), θ_{1}, …, θ_{k}, χ ⊢_{2} ⊥, Mon for L_{0}-conclusions yields that ¬(θ_{1} ∧ ⋯ ∧ θ_{k} ∧ χ), ϕ_{1}, …, ϕ_{n}, χ ⊢_{2} ⊥, and then 2 follows from soundness.

To see 1 we make the following claim: if j ≤ n, and θ_{1}, …, θ_{i} are the L_{0}-formulae in ϕ_{1}, …, ϕ_{j}, in the order in which they occur, then

σ[ϕ_{1}] ⋯ [ϕ_{j}] = {w | ¬(θ_{1} ∧ ⋯ ∧ θ_{k} ∧ χ), θ_{1}, …, θ_{i}, Δ_{w} ⊬_{2} ⊥}

We now first show that this is sufficient for 1. Suppose that σ[ϕ_{1}] ⋯ [ϕ_{n}] = ∅; then by the claim and lemma 10, ¬(θ_{1} ∧ ⋯ ∧ θ_{k} ∧ χ), θ_{1}, …, θ_{k} ⊢_{2} ⊥. But then the negation and conjunction rules imply that θ_{1}, …, θ_{k} ⊢_{2} χ, so by Mon for L_{0}-conclusions, ϕ_{1}, …, ϕ_{n} ⊢_{2} χ, so ϕ_{1}, …, ϕ_{n} ⊢_{2}might χ by might-introduction.

Finally we show the claim by induction on j. If j = 0 the claim reduces to lemma 11 if we can show that ¬(θ_{1}∧⋯∧θ_{k}∧χ) ⊬_{2} ⊥. But if ¬(θ_{1}∧⋯∧θ_{k}∧χ) ⊢_{2} ⊥ then ⊢_{2} (θ_{1}∧⋯∧θ_{k}∧χ), so ⊢_{2} χ, so ϕ_{1}, …, ϕ_{n} ⊢_{2} χ, so ϕ_{1}, …, ϕ_{n} ⊢_{2}might χ, which contradicts our assumption.

For the induction step distinguish two cases. Case 1: ϕ_{j+1} ∈ L_{0}. Then by lemma 9,

σ[ϕ_{1}] ⋯ [ϕ_{j+1}] = {w ∈ σ[ϕ_{1}] ⋯ [ϕ_{j}] | Δ_{w} ⊢_{2} ϕ_{j+1}}

which by the induction hypothesis implies that

σ[ϕ_{1}] ⋯ [ϕ_{j+1}] = {w ∈ W | ¬(θ_{1}∧⋯∧θ_{k}∧χ), θ_{1}, …, θ_{i}, Δ_{w} ⊬_{2} ⊥ and Δ_{w} ⊢_{2} ϕ_{j+1}}

which by CC and CM yields that

σ[ϕ_{1}] ⋯ [ϕ_{j+1}] = {w ∈ W | ¬(θ_{1} ∧ ⋯ ∧ θ_{k} ∧ χ), θ_{1}, …, θ_{i}, ϕ_{j+1}, Δ_{w} ⊬_{2} ⊥} Case 2: ϕ_{j+1} =might ψ. Suppose that σ[ϕ_{1}] ⋯ [ϕ_{j}][ψ] = ∅. Then by the induction hypothesis and lemmas 9 and 10,

¬(θ_{1} ∧ ⋯ ∧ θ_{k} ∧ χ), θ_{1}, …, θ_{i}, ψ ⊢_{2} ⊥

But then

θ_{1}, …, θ_{i}, ψ ⊢_{2} θ_{1} ∧ ⋯ ∧ θ_{k} ∧ χ

so

θ_{1}, …, θ_{i}, ψ ⊢_{2} θ_{i+1} ∧ ⋯ ∧ θ_{k} ∧ χ

so by simultaneous might-introduction

θ_{1}, …, θ_{i}, might ψ ⊢_{2}might (θ_{i+1} ∧ ⋯ ∧ θ_{k} ∧ χ)

But then repeated application of the might-monotonicity rule m − Mon yields that

θ_{1}, …, θ_{i}, might ψ, θ_{i+1}, …, θ_{k} ⊢_{2}might (θ_{i+1} ∧ ⋯ ∧ θ_{k} ∧ χ)

And from this it follows that

θ_{1}, …, θ_{i}, might ψ, θ_{i+1}, …, θ_{k} ⊢_{2}might χ

and by hence by Mon that

ϕ_{1}, …, ϕ_{n} ⊢_{2}might χ

which contradicts our assumption. So σ[ϕ_{1}] ⋯ [ϕ_{j}][ψ] ≠ ∅. But then we have σ[ϕ_{1}] ⋯ [ϕ_{j}][might ψ] = σ[ϕ_{1}] ⋯ [ϕ_{j}], and we can apply the induction hypothesis. □

3.3.2 Cut Elimination

In [8] van der Does gives an alternative calculus for ^{⊧}_{2}, which is equivalent to our calculus ⊢_{2}, but allows the elimination of Cautious Cut. His calculus, M_{gd}, actualy arose out of an attempt to prove Cautious Cut elimination for ⊢_{2}, which turned out to be problematic due to the various side conditions on syntactic complexity in the rules of ⊢_{2}. We present the calculus here, but for the proof of the Cut Elimination theorem refer the reader to the cited paper.

The presentation of the system uses the following notational coventions. The symbols ϕ, ψ, χ, … vary over L_{0} formulas, and Δ, Γ, Θ, … over finite sequences of L_{0} formulas. L_{1} formulas are denoted by σ, τ, μ, …, and finite sequences of such formulas by Π, Λ, . . ..

The deduction system M_{gd} consists of two parts, one for L_{0} sequents and one for L_{1} sequents.

The Common part consists of two structural rules.

σ ⇒ σ RR \begin{matrix}Π ⇒ σ & ΠσΛ ⇒ τ \\ ΠΛ ⇒ τ \end{matrix} cautiouscut

The Classical part consists of L_{0}-sequents (χ may be the empty string).

Logical rules

{Γϕ_{i} ⇒ χ \atop Γϕ_{1} ∧ ϕ_{2} ⇒ χ} L_{∧}^{i}  \begin{matrix}Γ ⇒ ϕ_{1} & Γ ⇒ ϕ_{2} \\ Γ ⇒ ϕ_{1} ∧ ϕ_{2} \end{matrix} R_{∧}

\begin{matrix}Γϕ_{1} ⇒ χ & Γϕ_{2} ⇒ χ \\ Γϕ_{1} ∨ ϕ_{2} ⇒ χ \end{matrix} L_{∨}  {Γ ⇒ ϕ_{i} \atop Γ ⇒ ϕ_{1} ∨ ϕ_{2}} R_{∨}^{i}

\begin{matrix}Γ ⇒ ϕ & Γψ ⇒ χ \\ Γϕ ⇒ ψ ⇒ χ \end{matrix} L_{⇒}  {Γϕ ⇒ ψ \atop Γ ⇒ ϕ ⇒ ψ} R_{⇒}

{Γ ⇒ ϕ \atop Γ¬ϕ ⇒} L_{¬}  {Γϕ ⇒ \atop Γ ⇒ ¬ϕ} R_{¬}

{Γϕ ⇒ χ \atop Γ¬¬ϕ ⇒ χ} L_{¬¬}

Structural rules

{ΓΔ ⇒ χ \atop ΓϕΔ ⇒ χ} mon {ΓϕϕΔ ⇒ χ \atop ΓϕΔ ⇒ χ} contr {ΓϕψΔ ⇒ χ \atop ΓψϕΔ ⇒ χ} perm

Might logic. This part consists of L_{1} sequents (τ may be the empty string).

Logical rules

{Πϕ ⇒ \atop Π might ϕ ⇒} L_{m1} ΠΛ ⇒ τ Π might ϕΛ ⇒ τ L_{m2} {Π ⇒ ϕ \atop Π ⇒might ϕ} R_{m}

Πϕ ⇒ ψ Π might ϕ ⇒might ψ ^{might^{1}} Π ⇒might (ϕ ∧ ψ) Πϕ ⇒might ψ ^{might^{2}}

Structural rules

{Π ⇒ \atop ΠΛ ⇒} L_{mon} {Π ⇒ \atop Π ⇒ σ} R_{mon}

Theorem 3 Cautious Cut can be eliminated in M_{gd}. Proof: see [8]. □

3.4 Starting from Ignorance

We first prove a necessary lemma, which is particular for ⊢_{1}.

Lemma 12 If ϕ_{1}, …, ϕ_{n}, ψ ⊬_{1} ⊥ then ϕ_{1}, …, ϕ_{n} ⊢_{1}might ψ. Proof: If there are no might-formulae in ϕ_{1}, …, ϕ_{n}, then by lemma 10 there is some diagram Δ such that Δ ⊢_{1} ϕ_{1}, …, Δ ⊢_{1} ϕ_{n} and Δ ⊢_{1} ψ, but then the diagram rule Δ gives ϕ_{1}, …, ϕ_{n} ⊢_{1}might ψ.

Next suppose that there are might-formulae in ϕ_{1}, …, ϕ_{n}, and let θ_{1}, …, θ_{k} be the L_{0}-formulae in ϕ_{1}, …, ϕ_{n}. If ϕ_{1}, …, ϕ_{n}, ψ ⊬_{1} ⊥ then θ_{1}, …, θ_{k}, ψ ⊬_{1} ⊥ by Mon for L_{0}-conclusions. Hence by the above, θ_{1}, …, θ_{k} ⊢_{1}might ψ, but then again by Mon we can put the might-premisses back in, so ϕ_{1}, …, ϕ_{n} ⊢_{1}might ψ. □

Theorem 4 ϕ_{1}, …, ϕ_{n} ⊢_{1} ψ iff ϕ_{1}, …, ϕ_{n} ^{⊧}_{1} ψ. Proof: We leave the soundness part to the reader.

Suppose ϕ_{1}, …, ϕ_{n} ⊬_{1} ψ. Case I: ψ ∈ L_{0}. We want to show that 0[ϕ_{1}] ⋯ [ϕ_{n}][ψ] ≠ 0[ϕ_{1}] ⋯ [ϕ_{n}]. Let θ_{1}, …, θ_{k} be the L_{0} formulae in ϕ_{1}, …, ϕ_{n}. Then θ_{1}, …, θ_{k}, ¬ψ ⊬_{1} ⊥, since otherwise θ_{1}, …, θ_{k} ⊢_{1} ψ and then by monotony for L_{0} conclusions ϕ_{1}, …, ϕ_{n} ⊢_{1} ψ, contrary to our assumption. So θ_{1}, …, θ_{k}, ¬ψ ⊬_{1} ⊥, so by lemma 8 and lemma 10, there must be some diagram Δ_{w} such that θ_{1}, …, θ_{k}, Δ_{w} ⊬_{1} ψ. But then by lemma 11, w ∈ 0[ϕ_{1}] ⋯ [ϕ_{n}], but by lemma 9, w ∉ 0[ϕ_{1}] ⋯ [ϕ_{n}][ψ].

Case II: ψ =might χ. Our assumption implies that ϕ_{1}, …, ϕ_{n} ⊬_{1} ⊥, which by lemma 11 and lemma 10 implies that 0[ϕ_{1}] ⋯ [ϕ_{n}] ≠ ∅. But by lemma 12, ϕ_{1}, …, ϕ_{n}, χ ⊢_{1} ⊥, hence by soundness, 0[ϕ_{1}] ⋯ [ϕ_{n}][might χ] = ∅. □

3.5 The Test Logic of might

For this case the main work has already been done, because the lemmas 8, 9, and 10 also hold for ⊢_{3}.

Theorem 5 ϕ_{1}, …, ϕ_{n} ⊢_{3} ψ iff ϕ_{1}, …, ϕ_{n} ^{⊧}_{3} ψ. Proof: Soundness is left to the reader. Suppose ϕ_{1}, …, ϕ_{n} ⊬_{3} ψ. We consider two cases. Case I: ψ ∈ L_{0}. Let θ_{1}, …, θ_{k} be the L_{0} formulae in ϕ_{1}, …, ϕ_{n}, and consider the state

σ = {w | Δ_{w} ⊢_{3} θ_{1}, …, θ_{k}}

Then σ ∥− ϕ_{i}, since either ϕ_{i} is one of the θ_{1}, …, θ_{k}, or ϕ_{i} =might χ. In the latter case, suppose that σ ∦−might χ, then σ[χ] = ∅, but then by lemma 9, θ_{1}, …, θ_{k}, χ ⊢_{3} ⊥, so θ_{1}, …, θ_{k}, might χ ⊢_{3} ⊥; but then by Permutation and Monotony for L_{0} conclusions, a contradiction with our assumption arises. Finally σ ∦− ψ: this follows form classical logic and the fact that θ_{1}, …, θ_{k} ⊬_{3} ψ.

Case II: ψ =might χ. Then consider the state

σ = {w | Δ_{w} ⊢_{3} θ_{1}, …, θ_{k}, ¬χ}

where again θ_{1}, …, θ_{k} are the L_{0} formulae in ϕ_{1}, …, ϕ_{n}. Since ϕ_{1}, …, ϕ_{n} ⊬_{3}might χ, we have that θ_{1}, …, θ_{k} ⊬_{3} χ, so σ ≠ ∅. On the other hand σ[χ] = ∅ by lemma 9, so σ ∦−might χ. So we are done if we can show that σ ∥− ϕ_{i}. Again the only interesting case is that ϕ_{i} is not one of the θ’s, and hence is of the form might α. Now if σ ∦−might α, σ[α] = ∅, so by lemma 9, θ_{1}, …, θ_{k}, α, ¬χ ⊢_{3} ⊥; but then θ_{1}, …, θ_{k}, α, ⊢_{3} χ so θ_{1}, …, θ_{k}, might α, ⊢_{3}might χ, which by Monotony contradicts our assumption. □

4 The normally-presumably-system

4.1 Semantics

We repeat the definitions of [11].

Definition 26 (Languages) Let A be a set of atomic formulae. Then L_{0}^{A} is the closure of A under the Boolean connectives ¬, ∨, ∧. L_{2}^{A} consists of L_{0}^{A}, and of every formula of the form normallyϕ for ϕ ∈ L_{0}^{A}, and every formula of the form presumablyϕ for ϕ ∈ L_{0}^{A}. nϕ and pϕ abbreviate normallyϕ and presumablyϕ, respectively. □

The basic idea of the semantics for normallyϕ is that a sentence of that form changes expectations rather than factive information. Factive information is still modeled as a set of possible worlds, just as in the semantics of might. Expectations are modeled as a binary relation over these worlds. The semantics of a sentence of the form presumablyϕ is guided by the idea that these express a property of those worlds in the factive information set that comply best with your expectations.

Definition 27 Let W = P (A) be the set of possible worlds for an atomic vocabulary A. Then an expectation pattern is a preorder on W.

Let ϵ be a pattern on W

1. a world w ∈ W is normal in ϵ if (w, v) ∈ ϵ for all v ∈ W

2. nϵ is the set of all normal worlds in ϵ

3. ϵ is coherent if nϵ ≠ ∅

Let s ⊆ W. Then

1. a world w ∈ W is optimal in (ϵ, s) if w ∈ s and for all v ∈ s, if (v, w) ∈ ϵ then (w, v) ∈ ϵ.

2. m_{(ϵ,s)} is the set of all optimal worlds of (ϵ, s) □

The intuitive idea is that if (w, v) ∈ ϵ, w complies at least as well with your expectations as v. If you learn a sentence normallyϕ this has to be preserved, and hence any pair (w, v) ∈ ϵ such that ϕ is true in v but not in w has to be removed from the pattern. This process is called refinement.

Definition 28 Let ϵ, ϵ′ be patterns on W, and consider a proposition p ⊆ W.

1. ϵ is a refinement of ϵ′ if ϵ ⊆ ϵ′

2. ϵ ∘ p =_{df} {(w, v) ∈ ϵ | if v ∈ p then w ∈ p}. ϵ ∘ p is called the refinement of ϵ with p. □

The refinement operation has the following properties.

Proposition 15

1. ϵ ∘ ∅ = ϵ

2. ϵ ∘ W = W 3. (ϵ ∘ p) ∘ p = ϵ ∘ p

4. (ϵ ∘ p) ∘ q = (ϵ ∘ q) ∘ p

5. if ϵ ⊆ ϵ′ and ϵ′ ∘ p = ϵ′ then ϵ ∘ p = ϵ □

Definition 29 If ϵ is a pattern on W, p ⊆ W, then p is a default in ϵ if p ≠ ∅ and ϵ ∘ p = ϵ. □

Proposition 16 If ϵ is a pattern on W then for all w, v ∈ W:

(w, v) ∈ ϵ iff for all defaults p in ϵ, if v ∈ p then w ∈ p

Proof: for the non obvious part, assume (w, v) ∉ ϵ and consider the proposition p = {u ∈ W | (w, u) ∉ ϵ}. Then w ∉ p, v ∈ p, and p is a defualt in ϵ. □

Finally then we define the set of information states and the semantics.

Definition 30

1. An information state is a pair σ = (ϵ, s) such that either ϵ is a coherent pattern on W and s is a non-empty subset of W, or ϵ = {(w, w) | w ∈ W} and s = ∅.

2. The minimal state is the state 0 = (W × W, W). The maximal or absurd state is the state 1 = ({(w, w) | w ∈ W}, ∅).

3. σ = (ϵ, s) is at least as strong as σ′ = (ϵ′, s′) if ϵ ⊆ ϵ′ and s ⊆ s′. □

Definition 31 (Semantics) Let σ = (ϵ, s) be an information state. Then for any ϕ ∈ L_{2}^{A}, σ[ϕ] is defined as follows

1. If ϕ ∈ l_{0}^{A} then

(ϵ, s)[ϕ] = \{ \begin{matrix}1 & if s ∩ ||ϕ|| = ∅ \\ (ϵ, s ∩ ||ϕ||) & otherwise \end{matrix}

Here ||ϕ|| = W[ϕ], which we can calculate from the semantics of the might-system, since ϕ ∈ L_{0}. (Put otherwise: ||ϕ|| is just the proposition expressed by ϕ, the set of all worlds where ϕ is true.)

2. If ϕ = normallyψ then

(ϵ, s)[normallyψ] = \{ \begin{matrix}1 & if nϵ ∩ ||ψ|| = ∅ \\ (ϵ ∘ ||ψ||, s) & otherwise \end{matrix}

3. If ϕ = presumablyψ then

(ϵ, s)[presumablyψ] = \{ \begin{matrix}(ϵ, s) & if m_{(ϵ,s)} ∩ ||ψ|| = m_{(ϵ,s)} \\ 1 & otherwise \end{matrix}

We end this section with some comments on the duality of defaults as propositions and defaults as patterns since this will play a role in the completeness proofs.

Defaults are defined as derivatives of an expectation pattern: they are those consistent propositions that are preserved by the pattern. From proposition 16 it follows that if two patterns have the same defaults, then they are equal. It does not follow that every set of propositions picks out a unique pattern, though this turns out to be true under some simple constraints on the set of propositions.

Definition 32 let W be a set of possible worlds. Then an expectation set is a set of propositions E ⊆ P (W) such that W ∈ E, ∅ ∉ E, E is closed under unions, and E is closed under intersections. If E is an expectation set then its associated pattern is defined as ϵ(E) =_{df} {(u, v) | ∀q ∈ E : if v ∈ q then u ∈ q}. □

It is not hard to show that ϵ(E) is a coherent pattern. It is also clear that every q ∈ E is a default in ϵ(E). And the converse also holds:

Proposition 17 Let E be an expectation set over W. Then every default of ϵ(E) is already in E, that is, if

1. q ≠ ∅

2. for all (u, v) ∈ ϵ(E), if v ∈ q then u ∈ q

then q ∈ E. Proof: Suppose q satisfies 1. and 2. Describe any v ∈ W by the set of propositions in E that are true of v, as follows:

e(v) = ⋂{p ∈ E | v ∈ p}

Since v ∈ W and W ∈ E, v ∈ e(v), so e(v) is non-empty. And e(v) ∈ E by closure under intersections. Moreover, we have that

if u ∈ e(v) then (u, v) ∈ ϵ(E)

For suppose u ∈ e(v), and let p ∈ E, and v ∈ p, then by definition of e(v), u ∈ p. Since this holds for arbitrary p ∈ E the definition of ϵ(E) gives that (u, v) ∈ ϵ(E).

Next define

q^{+} = ⋃{e(v) | v ∈ q}

Then q^{+} ∈ E by closure under union. Moroever q^{+} = q: if u ∈ q then u ∈ q^{+} since u ∈ e(u) ⊆ q^{+}; and if u ∈ q^{+} then u ∈ e(v) for some v ∈ q. The former impies that (u, v) ∈ ϵ(E) (as we’ve just shown), which combined with the fact that v ∈ q and our assumption that q is preserved by ϵ(E) implies that u ∈ q. □

From the definition of ϵ(E) it is also immediate that every q ∈ E is a default ϵ(E). Thus by proposition 16, E uniquely determines ϵ(E). The construction in the proof of proposition 17 will turn out to be a crucial part of the completeness theorems in the next sections.

4.2 The static logic of normally

For the fragment with only the Booelans and normally, Permutation and Idempotency hold, as is easily seen from proposition 15, so by the results of section 2.1, all three consequence relations collapse to one, essentially static relation.

We determine this consequence relation by developping an alternative static semantics for normally, give a complete characterization of consequence in this static semantics, and then show that this static consequence relation is equivalent to the dynamic consequence relations.

The models are the ordinary Kripke models from modal logic:

Definition 33 (Models, Semantics, Validity) Let A be a set of atomic formulae.

1. A frame is a pair (W, R) where W ≠ ∅ and R is a binary relation over W

2. An A-valuation is a function f : A → {0, 1}.

3. An A-model is a triple M = (W, R, V) where (W, R) is a frame and V is a function that assigns to each w ∈ W an A-valuation V(w).

4. The notion of truth in a world in a model is defined as usual for the Boolean connectives; the truth conditions for n are given by

w ∥− nϕ iff ∃v : v ∥− ϕ and ∀uv : if uRv and v ∥− ϕ then u ∥− ϕ

5. M ^{⊧} ϕ iff for all w in M, M, w ∥− ϕ.

6. Validity is defined as preservation of truth: if K is a class of A- models and ϕ_{1}, …, ϕ_{n}, ψ are A-formulae, then ϕ_{1}, …, ϕ_{n} ^{⊧}_{K} ψ if and only if for all models M in K and all worlds w in M, if M, w ∥− ϕ_{i} for 1 ≤ i ≤ n, then M, w ∥− ψ. □

So almost everything is as we are used to in modal logic. The relation R of a model will play the same role as the expectation pattern in the dynamic semantics. Note that n is not a normal modal operator, since it does not satisfy the K-rule

ϕ_{1}, …, ϕ_{n} ⊢ ψ ; \overline{nϕ_{1}, …, nϕ_{n} ⊢ nψ}

at least not if we look at the class of all models.

Also note that formulae of the form nϕ are global: if they are true in some world they are true in all worlds; and if they are false somewhere they are false everywhere.

The information states that are used in the update semantics for normally are special cases of models. Suppose we have a finite vocabulary of atoms A. Then an information state can be seen as an A-model having four special properties:

1. different worlds carry different valuations

2. the relation is a preorder

3. there are minimal (‘normal’) worlds

A fourth distinction is that

4. the dynamic semantics is defined only for nϕ if ϕ is propositional

that is, formulae in which n can only occur as outermost operator.

So we have allowed ourselves four generalizations. We will show that the first two are inessential. The existence of normal worlds makes a difference but is expressible in the static semantics. Finally, the restriction on the occurrence of n will actually be an issue that we will study: we will prove completeness with and without this restriction.

We will first show that the constraint that the expectation pattern is a preorder is free.

Definition 34 Let M = (W, R, V) be a model. Define the completion of R by

R^{+} = {(u, v) | ∀ϕ : if M ^{⊧} nϕ and M, v ∥− ϕ then M, u ∥− ϕ}

Define the completed model M^{+} = (W, R^{+}, V). □

Then R ⊆ R^{+}, and clearly R^{+} is a preorder. R^{+} fills in the ‘gaps’ of R; we add any pair which was not in the original pattern, although the pair does in fact comply with all true defauls. In view of proposition 16, it may appear that every model is complete, but this need not be so if the model is not distinguished. All finite distinguished models are complete, as a straighforward adaptation of the proof of proposition 16 will show.^{8}

Proposition 18 Let M be a model and let M^{+} be its completion. Then for all ϕ, w: M, w ∥− ϕ iff M^{+}, w ∥− ϕ Proof: an induction in which nϕ is the only interesting case. Suppose M, w ∥− nϕ. Then M ^{⊧} nϕ. Moreover, M, v ∥− ϕ for some v, so by the induction hypothesis, M^{+}, v ∥− ϕ. Next suppose xR^{+}y and M^{+}, y ∥− ϕ, then by the induction hypothesis, M, y ∥− ϕ. So xR^{+}y and M, y ∥− ϕ, but since M ^{⊧} nϕ, the definition of R^{+} implies that M, x ∥− ϕ, and then M^{+}, x ∥− ϕ follows from the induction hypothesis.

The converse follows from the induction hypothesis and the fact that R ⊆ R^{+}. □

Given any class of models K, define K^{+} = {M^{+} | M ∈ K}. Then the previous proposition implies that whatever is valid on K is valid on K^{+}, and that whatever is satisfiable in K is satisfiable in K^{+}. Hence K-validity and K^{+}- validity coincide. This means that from a class of models can we can always pass to a class of preorders that has the same logic.

8For the case of infinite distinguished models the proof of proposition 16 does not carry over, since in that case the proposition p that is used in the proof may not be expressible by some formula.

Next we show that we can remove situations in which different worlds carry the same valuation. The idea why this is so is that in a completed model, worlds that carry the same valuation are R-related to the same worlds, so that we can conceive of them as ‘one’ world.

Lemma 13 Let M be a model. Then for all formulae ϕ and all worlds u, v ∈ W, if u, v carry the same valuation then M, u ∥− ϕ iff M, v ∥− ϕ. Proof: The case where ϕ is atomic is immediate from the assumption on u, v. The Boolean cases are immediate form the induction hypothesis. The case ϕ = nψ is trivial since all worlds satisfy the same norms. □

Lemma 14 Let M^{+} = (W, R^{+}, V) be the completion of M. Let u, v ∈ W carry the same valuation. Then for all w ∈ W, wR^{+}v iff wR^{+}u, and vR^{+}w iff uR^{+}w. Proof: Suppose that u, v ∈ W carry the same valuation, wR^{+}v, but not wR^{+}u. The latter implies that there is some formula nϕ such that M ^{⊧} nϕ, M, u ∥− ϕ, but M, w ∥− −̸ ϕ. Then by proposition 18, M^{+}, u ∥− ϕ and M^{+}, w ∥− −̸ ϕ, so by lemma 13, M^{+}, v ∥− ϕ and M^{+}, w ∥− −̸ ϕ, but this contradicts the fact that wR^{+}v. The other cases are similar. □

The next move is standard now: apply filtration to M^{+} to obtain a distinguished model. We leave the remaning details to the reader.

We will now consider the constraint of the existence of normal worlds, in finite models. To be precise, w is normal in (W, R) if wRv for all v ∈ W. On finite models, the existence of these worlds is equivalent to the condition that (W, R) is closed under finite meets: for every finite subset X of W there is a v ∈ W such that vRu for all u ∈ X. And the latter condition is of course equivalent to the existence of binary meets: if u, v ∈ W then there is a w ∈ W such that wRv and wRu.

Definition 35 If (W, R) is a frame and u, v ∈ W, then u is a predecessor of v provided (u, v) ∈ R^{∗}, where R^{∗} is the Reflexive-transitive closure of R. □

Proposition 19 Consider the class of all frames in which every two worlds have a common predecessor. This class is characterised by np ∧ nq → n(p ∧ q). Proof: Suppose M = (W, R, V) is a model of which the frame has the property. Suppose w ∥− np ∧ nq. Then there are u, v with u ∥− p and v ∥− q. But u, v must have a common predecessor, say z, and since both p and q are downward preserved, z ∥− p ∧ q. That p ∧ q is also preserved downward is straightforward. So w ∥− n(p ∧ q).

Conversely, suppose we have a frame (W, R) and two worlds u, v ∈ W that don’t have a common predecessor. Then the frame consists of three disjunct parts:

• Ru = {z ∈ W | (z, u) ∈ R^{∗}} • Rv = {z ∈ W | (z, v) ∈ R^{∗}}

• the rest: W \ (Ru ∪ Rv)

Then there are no arrows between Ru and Rv; moreover there no arrows from the rest to either Ru or Rv. Make a model on this frame where p, ¬q are true in Ru, ¬p, q are true in Rv, and ¬p, ¬q are true in the rest. Then np and nq are true but n(p ∧ q) is false. □

Notice that the existence of common predecessors is not quite the same as existence of finite meet, though it is of course whenever R is reflexive and transitive.

We’ve now shown that two of the four abstractions we made from the update framework are not esential. Thus two remain, which give the following four logics of interest:

• M, the logic of the class of all models

• N, the logic of the class of all models with finite meet

• M_{1}, which is M restricted to L_{1} formulae

• N_{1}, which is N restricted to L_{1} formulae

Since we’ve shown that finite meet is expressed by np ∧ nq → n(p ∧ q), it would be nice if we can formulate N as M with only this axiom added. This turns out to be possible. However we will only treat details of the completeness proofs of N and N_{1} since these are the logics that have a direct correspondence with the dynamic logic of normally.

But before we do this you may want to know what is exactly the connection between the update semantics for normally and the truth conditional semantics of this section.

Proposition 20 For the fragment with only the Booleans and normally, static consequence coincides with dynamic consequence. Proof: We sketch the main line of argument and leave the details to the reader. We already know that the three dynamic consequence relations coincide, so it is sufficient to show that static consequence coincides with ^{⊧}_{3}. Let P(A) be the set of all possible worlds over a finite set of atoms A. Then for any state (ϵ, s), consider the model M = (P(A), ϵ, V), where V is of course defined by: V(w)(p) = 1 iff p ∈ w. Then show that

(ϵ, s) ∥− ϕ iff for all w ∈ s : M, w ∥− ϕ

From this it follows that ϕ_{1}, …, ϕ_{n} ^{⊧} ψ implies ϕ_{1}, …, ϕ_{n} ^{⊧}_{3} ψ.

For the converse suppose that ϕ_{1}, …, ϕ_{n} ^{|̸=} ψ, then there is a model M = (W, R, V) and a world w ∈ W with M, w ∥− ϕ_{1}, …, ϕ_{n}, M, w ∦− ψ. Define a pattern ϵ by ϵ = {(u, v) | for all χ ∈ L_{0}, if M ^{⊧} nχ and v ^{⊧}_{c} lχ then u ^{⊧}_{c} lχ}, where ^{⊧}_{c} l means ‘true in classical logic’. Then check that ϵ is a coherent pattern, and that for the unique w′ ∈ P(A) with w′ = {p ∈ A | V(w)(p) = 1}, we have that (ϵ, {w′}) ∥− ϕ iff M, w ∥− ϕ. It follows that ϕ_{1}, …, ϕ_{n} ^{|̸=}_{3} ψ. □

4.2.1 Unrestricted Version

We we first consider N, the logic of the class of all preorders that have finite meet, without any syntactic restrictions on occurences of normally. We present N as a sequent calculus where the sequents are of the form Γ ⇒ Δ for finite sets of formulae Γ, Δ.

Reflexivity ϕ ⇒ ϕ [Refl]
Structural Rules  {Γ ⇒ Δ \atop Π, Γ ⇒ Δ, Σ} [Mon]
Γ ⇒ ϕ, Δ Π, ϕ ⇒ Σ

Γ, Π ⇒ Δ, Σ [CUT]

Logical rules for ¬, ∧, ∨

{Γ ⇒ ϕ, Δ \atop Γ, ¬ϕ ⇒ Δ} [¬L]  {Γ, ϕ ⇒ Δ \atop Γ ⇒ ¬ϕ, Δ} [¬R]

{Γ, ϕ, ψ ⇒ Δ \atop Γ, ϕ ∧ ψ ⇒ Δ} [∧L]  \begin{matrix}Γ ⇒ ϕ, Δ & Γ ⇒ ψ, Δ \\ Γ ⇒ ϕ ∧ ψ, Δ \end{matrix} [∧R]

\begin{matrix}Γ, ϕ ⇒ Δ & Γ, ψ ⇒ Δ \\ Γ, ϕ ∨ ψ ⇒ Δ \end{matrix} [∨L]  {Γ ⇒ ϕ, ψ, Δ \atop Γ ⇒ ϕ ∨ ψ, Δ} [∨R]

Logical Rules for n

\begin{matrix}Γ ⇒ nϕ, Δ & Γ ⇒ nψ, Δ \\ Γ ⇒ n(ϕ ∧ ψ), Δ \end{matrix} [n∧] \begin{matrix}Γ ⇒ nϕ, Δ & Γ ⇒ nψ, Δ \\ Γ ⇒ n(ϕ ∨ ψ), Δ \end{matrix} [n∨]

In the following four rules Γ, Δ may only contain formulae of the form nϕ or ¬nϕ.

{Γ, ϕ ⇒ Δ \atop Γ, nϕ ⇒ Δ} [nL]  {Γ ⇒ ϕ, Δ \atop Γ ⇒ nϕ, Δ} [nR]

{Γ, ϕ_{1}, …, ψ_{k} ⇒ Δ \atop Γ, nϕ_{1}, …, nϕ_{k} ⇒ Δ} [MEET] \begin{matrix}Γ, ϕ ⇒ ψ, Δ & Γ, ψ ⇒ ϕ, Δ \\ Γ, nϕ ⇒ nψ, Δ \end{matrix} [REP L]

Here a norm is a formula of the form nϕ or of the form ¬nϕ. This presentation of N is not the most economic one, but we’ve tried to give the system such a form that there is some prospect of proving a Cut Elimination theorem.^{9} Actually N could be presented as an extension of classical logic with the following rules:

1. nϕ, nψ ⊢ n(ϕ ∧ ψ) (n∧′)

2. nϕ, nψ ⊢ n(ϕ ∨ ψ) (n∨′)

9But these attempts have failed until now.

3. n⊥ ⊢ ⊥ (n⊥)

4. ⊢ n⊤ (n⊤)

5. \begin{matrix}N , ϕ ⊢ ψ & N , ψ ⊢ ϕ \\ N , nϕ ⊢ nψ \end{matrix} [REP L′] provided that N is a set of norms

These are the rules for n that are needed in the completeness theorem. We leave it to the reader to verify that these rules are derivable in our sequent calculus.

Definition 36 An N -derivation is a finite sequence of sequents, in which every sequent is either an axiom, or follows from sequents earlier in the sequence by one of the rules. Γ ⊢_{N} Δ iff there are finite subsets Γ′ ⊆ Γ and Δ′ ⊆ Δ and an N -derivation such that Γ′ ⇒ Δ′ is the last sequent. If K is a class of models, then Γ ^{⊧}_{K} Δ if for all M ∈ K and worlds w ∈ M, if M, w ∥− ϕ for all ϕ ∈ Γ then M, w ∥− ψ for some ψ ∈ Δ. □

From (nR) it is easy to see that nϕ ⊢_{N} nnϕ and ¬nϕ ⊢_{N} n¬nϕ, and likewise (nL) implies that nnϕ ⊢_{N} nϕ and n¬nϕ ⊢_{N} ¬nϕ.

Theorem 6 (Soundness) N is sound with respect to the class of all preorders that have finite meet. Proof: left to the reader. The existence of finite meets is relevant for the rules (n∧) and MEET. □

The construction of a canonical model is similar to the standard construction in modal logic. There is one detail that we have to take care of: norms are either true everywhere in a model, or false everywhere. So in the canonical model construction we have to take care that all maximal consistent sets that constitute the model contain the same norms.

Definition 37

1. N (Γ), the norms of Γ, is the set {nϕ | nϕ ∈ Γ} ∪ {¬nϕ | ¬nϕ ∈ Γ}

2. A norm set C is norm-maximal if for every formula ϕ either nϕ ∈ C or ¬nϕ ∈ C.

3. Γ is consistent if Γ ⊬ ⊥. Γ is maximal consistent if Γ is consistent and no proper extension of Γ is consistent.

4. Let C be a norm set. Then Γ is maximal consistent modulo C if Γ is maximal consistent, and N (Γ) = C. □

If Γ is maximal consistent modulo C then C is norm-maximal.

Lemma 15 (First Saturation Lemma) Suppose Γ ⊬ ϕ. Then there is a maximal consistent set Γ′ such that Γ ∪ {¬ϕ} ⊆ Γ′. Proof: Use a standard Lindenbaum argument. □

Next we need a second form of the saturation lemma. We will frequently need an argument of the form: if C is a norm set and C ∪ Σ is consistent then C ∪ Σ can be extended to maximal consistent set modulo C: for this we have to show that we can saturate in such a way that the resulting set contains the same n-formulae as C. But this easily follows if C is already maximal with respect to norms.

Lemma 16 (Second Saturation Lemma) Suppose C is norm-maximal and C∪Σ is consistent. Then there is a Σ′ ⊇ C∪Σ such that Σ′ is maximal consistent modulo C. Proof: By the first saturation lemma there is a maximal consistent Σ′ ⊇ C ∪ Σ. Then clearly C ⊆ N (Σ′); the converse follows from the norm-maximality of C. □

Definition 38 (Canonical Model) Suppose C is a norm-maximal set in an atomic vocabulary A. Then the model M_{A,C} = (W_{A,C}, R_{C}, V) is defined as follows:

• W_{A,C} consists of all sets of L(A)-formulae that are maximal consistent modulo C

• ΣR_{C}Σ′ iff for all nψ ∈ C, if ψ ∈ Σ′ then ψ ∈ Σ

• V (p, Σ) = 1 iff p ∈ Σ □

Lemma 17 If C is norm-maximal in a finite vocabulary A, then M_{A,C} is a finite model. Proof: Suppose Γ_{1} and Γ_{2} are maximal consistent modulo C, and suppose they contain the same L_{0}(A) formulae. Then prove with induction on the structure of ϕ that ϕ ∈ Γ_{1} iff ϕ ∈ Γ_{2}. The atomic case follows from our assumption; the Boolean cases follow from the induction hypothesis and maximal consistency, and the n-case follows from the fact that both are maximal consistent modulo C, so they must contain the same norms.

So we have shown that two maximal consistent sets are identical if they contain the same norms and the same L_{0}-formulae. Next observe that the L_{0}(A) formulae of some maximal consistent set must form a maximal consistent set in classical propositional logic. Hence by our previous observation, there can be at most 2^{k} different maximal consistent sets modulo C, where k is the cardinality of A. □

Lemma 18 (Valuation Lemma) Let C be a norm-maximal set in a finite vocabulary A, and let Γ ∈ W_{A,C}.

1. ¬ϕ ∈ Γ iff ϕ ∉ Γ

2. If ϕ ∧ ψ ∈ Γ iff ϕ ∈ Γ and ψ ∈ Γ

3. ϕ ∨ ψ ∈ Γ iff ϕ ∈ Γ or ψ ∈ Γ 4. nϕ ∈ Γ iff

(a) there is a Γ′ in W_{C,Δ} such that ϕ ∈ Γ′

(b) for all Σ, Σ′ ∈ W_{C,Δ}, if ΣR_{C}Σ′ and ϕ ∈ Σ′ then ϕ ∈ Σ

Proof: The Boolean connectives are standard.

We consider the case of nϕ. Suppose nϕ ∈ Γ. Then nϕ ∈ C. Suppose C∪{ϕ} is inconsistent, that is, C, ϕ ⊢ ⊥. Since also C, ⊥ ⊢ ϕ, the Replacement Rule gives C, nϕ ⊢ n⊥, so by the rule (n⊥), C, nϕ ⊢ ⊥, which can’t be since nϕ ∈ C and C is consistent. So C ∪ {ϕ} is consistent. By the Second Saturation Lemma there must be a set Σ ∈ W_{A,C} with C ∪ {ϕ} ⊆ Σ; so ϕ ∈ Σ.

Next suppose that Σ′, Σ′′ ∈ W_{A,C}, Σ′R_{C}Σ′′ and ϕ ∈ Σ′′. But nϕ ∈ C, so the definition of R_{C} gives that ϕ ∈ Σ′.

For the converse, suppose that clauses 4(a) and 4(b) hold, so we have a Σ with ϕ ∈ Σ and ϕ is downward preserved by the ordering. Consider any Γ ∈ W_{A,C}, consider all norms of C that are true in Γ:

T (Γ) =_{df} {ψ ∈ Γ | nψ ∈ C}

Notice that the maximality of C and the rule (nR) imply that n⊤ ∈ C, so {ψ ∈ Γ | nψ ∈ C} ≠ ∅.

Then

if ϕ ∈ Γ then C, T (Γ) ⊢ ϕ  (1)

For suppose ϕ ∈ Γ but C, T (Γ) ⊬ ϕ, then C, T (Γ), ¬ϕ ⊬ ⊥ so there is a Γ′ that is maximal consistent modulo C and C ∪ T (Γ) ∪ {¬ϕ} ⊆ Γ′. But then Γ′R_{C}Γ, so by the preservation condition on ϕ, ϕ ∈ Γ′, but then Γ′ must be inconsistent.

Now by compactness, if C, T (Γ) ⊢ ϕ there must be a finite subset T of T (Γ) such that C, T ⊢ ϕ; then put t(Γ) = ⋀ T. Use this to describe ϕ by all these finite descriptions of sets of which it is a member:

ϕ^{+} = ⋁{t(Γ) | ϕ ∈ Γ and Γ ∈ W_{A,C}}

This is welldefined, since W_{A,C} is finite because A is finite. Since ϕ^{+} is the disjunction of all t(Γ) with ϕ ∈ Γ it follows from (1) that

C, ϕ^{+} ⊢ ϕ  (2)

On the other hand, we also have that

C, ϕ ⊢ ϕ^{+}  (3)

since otherwise C, ¬t(Γ_{1}), …, ¬t(Γ_{k}), ϕ ⊬ ⊥, where Γ_{1}, …, Γ_{k} list all sets with ϕ ∈ Γ_{i}. Hence it can be extended to a set Σ with ϕ ∈ Σ, which means that Σ is one of the Γ_{i}, so Σ ⊢ t(Γ_{i}) and Σ ⊢ ¬t(Γ_{i}), contradiction.

But (2) and (3) and the Replacement Rule imply that

C, nϕ^{+} ⊢ nϕ

So we are done if we can show that

C ⊢ nϕ^{+}

Well, t(Γ) is of the form ϕ_{1} ∧ … ∧ ϕ_{k} where nϕ_{i} ∈ C, so the rule n∧ gives that C ⊢ n(ϕ_{1} ∧ … ∧ ϕ_{k}), hence Γ ⊢ nt(Γ) so by maximality of Γ, nt(Γ) ∈ Γ so nt(Γ) ∈ C. So by the disjunction rule (n∨), C ⊢ nϕ^{+}. □

Finally we show that the frame of the canonical model has the right structural properties. That R_{C} is a preorder is immediately clear from its definition. So what is left to show is the existence of meets.

Lemma 19 (Canonical Frame lemma) Suppose C is norm-maximal in a vocabulary A, and consider the canonical frame (W_{A,C}, R_{C}). If Γ_{1}, Γ_{2} ∈ W_{A,C} then there is a Σ ∈ W_{A,C} such that ΣR_{C}Γ_{1} and ΣR_{C}Γ_{2}. Proof: Consider the set

C ∪ {ψ ∈ Γ_{1} | nψ ∈ C} ∪ {χ ∈ Γ_{2} | nχ ∈ C}

Suppose that this set is inconsistent, say (we do a simple case) that C, ψ, χ ⊢ ⊥ where ψ ∈ Γ_{1}, χ ∈ Γ_{2}, nψ, nχ ∈ C. Then by the MEET rule, C, nψ, nχ ⊢ ⊥. But nψ, nχ ∈ C, so by Cut, C ⊢ ⊥, contradiction. □

Now standard argumentation establishes

Theorem 7 (Completeness of N) N is complete for the class of all preorders with finite meet. □

4.2.2 Restricted Version

We will now look again at the class of models with meet, but through the eyes of formulae in which normally can only occur as outermost operator.

Definition 39 L_{1} = L_{0} ∪ {nϕ | ϕ ∈ L_{0}}. □

Now we don’t have negations of the form ¬nϕ, so the construction of maximal norm sets does not work here. But this is compensated by the fact that we can exploit some theorems about classical logic, since we now know that whenever we have a formula of the form nϕ, ϕ can’t contain n, so ϕ behaves purely classical. The following change of terminology is forced upon us by the syntactic restriction.

Definition 40 A norm is any formula of the form nψ with ψ ∈ L_{0}. A set of formulae N is a norm set if all formulae in N are norms. The empty set is a norm set. □

The system N1 is simply defined as follows: N 1 is the set of L_{1} instances of the schemata that axiomatize N. It is then immediate from the soundness of N that N 1 is also sound on the class of preorders with finite meet.

The problem that we can’t negate formulas nϕ anymore can be illustrated by an example: n(p ∧ q) ⊬ np. But the conclusion that n(p ∧ q), ¬np ⊬ ⊥ has become useless, since ¬np is not an L_{1}-formula. However we can do something like the following. The closure Δ of {n(p ∧ q), np} is {n(p ∧ q), np, (p ∧ q), ¬(p ∧ q), p, q, ¬p, ¬q}. Put C = {n(p ∧ q)}. This gives four ‘finite’ maximal consistent subsets of Δ that don’t contain np, namely

Γ_{11} = {n(p ∧ q), (p ∧ q), p, q} Γ_{10} = {n(p ∧ q), ¬(p ∧ q), p, ¬q}
Γ_{01} = {n(p ∧ q), ¬(p ∧ q), ¬p, q} Γ_{00} = {n(p ∧ q), ¬(p ∧ q), ¬p, ¬q}

Now we define R_{C} by exactly those pairs that preserve all norms in C, that is, that preserve p ∧ q, the following model results:

(reflexive and transitive arrows not drawn). The R_{C}-connections between the {p, ¬q} set and the {¬p, q} make sure that neither np nor nq is true in the model.

The worlds in the model turn out to correspond exactly to all the finite valuations for p and q, and the relation is just defined to have the right preservation behaviour. This turns out to be possible in general: if C is a finite consistent set of norms in a finite vocabulary A, then the set of all A -valuations can be equipped with a relation R such that in the resulting model all norms in C are true. This will be a leading idea in our completeness proof.

Definition 41 (Finite Canonical Model) Let C be a consistent set of norms. Let A be a set that contains all atomic formulae that occur in C. Then the model F_{A,C} = (W_{A}, R_{C}, V) is defined as follows:

• W_{A} is the set of all A-valuations

• V is the identity function

• R_{C} = {(u, v) | for all nϕ ∈ C : if v(ϕ) = 1 then u(ϕ) = 1} □

This definition makes sense: if nϕ ∈ C then ϕ is a formula that doens’t contain n, and then we know from classical logic how to calculate w(ϕ). It would be circular to define R_{C} directly in terms of the forcing relation, since we then would define M_{C} in terms of itself. Of course, the previous remark shows that after we have defined the model it is no problem to show that in fact

R_{C} = {(u, v) | for all nϕ ∈ C : if M_{C}, v ∥− ϕ then M_{C}, u ∥− ϕ}

We leave this to the reader.

Lemma 20 (Norm Consistency Lemma) Let C be a consistent norm set in a vocabulary A. Then F_{A,C} ^{⊧} C. Proof: . Suppose nϕ ∈ C. Then ϕ ∈ L_{0}. Since by assumption C ⊬ ⊥, also nϕ ⊬ ⊥, so by the MEET rule , ϕ ⊬ ⊥. Since classical logic is part of N 1, the consistency theorem for classical logic implies that there is some valuation v with v(ϕ) = 1 so F_{A,C}, v ∥− ϕ. That R_{C} has the right preservation behaviour for ϕ is true by definition of R_{C}. So F_{A,C} ^{⊧} nϕ. □

Lemma 21 (Consistency Lemma) Let C be a consistent norm set in the vocabulary A, and Σ a consistent set of L_{0}(A)-formulae. Then C ∪Σ is satisfied by some world in F_{A,C}. Proof: by the consistency theorem for classical logic and the previous lemma. □

Now the soundness theorem for N 1 gives that

Corollary 3 If C is a consistent norm set, and Σ a consistent set of L_{0}- formulae, then C ∪ Σ is consistent. □

These observations prove a nice philosophical point: norms don’t imply facts. To be precise, if a set of norms imply some fact then either the set of norms is inconsistent or the fact is valid.

We now turn to a converse of the Norm Consistency Lemma, for which we will make some finiteness assumptions.

Definition 42

1. Δ is closed if it contains n⊤ and n⊥, is closed under subformulae, negations of non-negated L_{0}-formulae, and furthermore contains ¬ϕ whenever it contains nϕ.

2. Suppose C is a norm set. Then C is a consistent n−theory within Δ if C ⊆ Δ, C is consistent, and for every formula nψ ∈ Δ, if C ⊢ nψ then nψ ∈ C.

Lemma 22 Let Δ be a finite closed set, and C a consistent n-theory within Δ. Suppose A includes all atoms in Δ. Then for all nϕ ∈ Δ, F_{A,C} ^{⊧} nϕ iff nϕ ∈ C. Proof: Suppose nϕ ∈ Δ and F_{A,C} ^{⊧} nϕ; then

∃v ∈ W_{C} : v ∥− ϕ  (1)
∀u, v ∈ W_{C} : if uR_{C}v and v ∥− ϕ then u ∥− ϕ  (2)

Describe any world w in the model by the norms in C that are realized by w:

t(w) = ⋀{ψ | nψ ∈ C and w ∥− ψ}

This is well defined since C is finite, and w ∥− n⊤ and n⊤ ∈ C. Notice that w ∥− t(w). Then ’describe’ ϕ by

ϕ^{+} = ⋁{t(w) | w ∥− ϕ}

This is well-defined bacause the model consists of all A-valuations, and A is finite. Then we have that

C ⊢ t(w)  (3)

by (nR) (which implies that ⊢ n⊤) and (n∧) (which implies that nϕ_{1}, …, nϕ_{n} ⊢ n(ϕ_{1} ∧ ⋯ ∧ nϕ_{k}) for k ≤ n). So by the disjunction rule (n∨),

C ⊢ nϕ^{+}  (4)

Next we show that

if w ∥− ϕ then C, t(w) ⊢ ϕ  (5)

For suppose w ∥− ϕ but C, t(w) ⊬ ϕ. Then C, t(w), ¬ϕ ⊬ ⊥, so by the Consistency Lemma there is some world v with v ∥− C ∪ {t(w), ¬ϕ}, so v ∥− ¬ϕ. But by definition of R_{C} and t(w) we must have vR_{C}w, hence by (2) and the assumption that w ∥− ϕ, also v ∥− ϕ, contradiction.

By (5) and the definition of ϕ^{+},

C, ϕ^{+} ⊢ ϕ  (6)

Conversely, we also have

C, ϕ ⊢ ϕ^{+}  (7)

for if this is not the case then C, ϕ, ¬ϕ^{+} ⊢ ⊥ so C ∪ {ϕ, ¬ϕ^{+}} is true in some world v by the consistency lemma. Since v ∥− ϕ, t(v) is one of the disjuncts of ϕ^{+}. However, C ∪ {ϕ, ¬ϕ^{+}} ⊢ ¬t(v), so by soundness, v ∥− ¬t(v), which is impossible.

The Replacement Rule applied to (6) and (7) implies that C, nϕ^{+} ⊢ nϕ, but then by (4) and Cut, C ⊢ nϕ. But nϕ ∈ Δ and C is an n-theory within Δ, so nϕ ∈ C. □

Lemma 23 (Frame Lemma) If A is finite, C is a finite consistent norm set, then F_{A,C} is a preorder that has finite meet. Proof: That F_{A,C} is a preorder is immediate from the definition of R_{C}. Let w, v ∈ W_{A}; consider

Σ = {ψ | nψ ∈ C and w ∥− ψ} ∪ {ψ | nψ ∈ C and v ∥− ψ}

Since nΣ ⊆ C, Σ ⊬ ⊥ by the MEET rule and the consistency of C. Hence by the consistency theorem for classical logic, u ∥− Σ for some u ∈ W. But then by the definition of R_{C} it is immediate that uR_{C}w and uR_{C}v. □

Now we are all set to prove completeness:

Theorem 8 (Completeness) N 1 is complete on the class of preorders with finite meet. Proof: Let Δ be the smallest closed set that extends Γ ∪ {¬ϕ}. Consider two cases: (1) ϕ ∈ L_{0}. Then Γ, ¬ϕ ⊬ ⊥. Define Γ′ = {ψ ∈ Δ | Γ, ¬ϕ ⊢ ψ} and put C = {nψ ∈ Γ′ | nψ ∈ Δ}. Then Γ′ is satisfied by some world in F_{A,C}. So Γ ^{|̸=} ϕ.

Case (2): ϕ is of the form nϕ′. Then define Γ′ = {ψ ∈ Δ | Γ ⊢ ψ} and put C = {nψ ∈ Γ′ | nψ ∈ Δ}. Then nϕ′ ∉ C, so nϕ′ is not true in F_{A,C} while Γ′ is satisfied by some world in F_{A,C}. So Γ ^{|̸=} ϕ. □

Since F_{A,C} is finite if A is, decidability easily follows.

5 Discussion and Further Research

There are two spefic problems that remain to be solved. First, there remains the task of providing completeness theorems for the update semantics that contains both the normally and presumably operators. Second, it would be desirable to reprove the completeness of the Update-Test variant of the might-system along the lines of the general method of section 2.4.3. In both cases we feel that we are ‘almost there’, and prefer to tell the real story at a later occasion, rather than face the unrewarding task of explaining what we don’t yet understand.

We have not paid much attention to decidability issues in the present paper. This is largely due to the fact that for the concrete update systems we discussed, decidability is trivial, since in all cases the semantics is entirely framed in terms of finitely many finite objects - thus a simple semantic ‘try out all cases’ procedure will yield a decision procedure.

Finally, a general issue in proof theory for dynamic semantics has to do with the format of the proof system. We have used sequent calculi in this paper. The advantage of sequent systems is not only their prominence in proof-theoretical studies, but also the fact that the semantic definitions of valid consequence we considered are attributions of some semantic property to sequents. Thus sequent calculi neatly fit the semantic definitions of consequence. The Hoare calculi for update semantics developed in [9] actually describe a class of statements about the semantics that covers more than the semantic entailments ϕ_{1}, …, ϕ_{n} ^{⊧}_{i} ψ, and are less elegant in this respect. On the other hand, our sequent calculi have a lot of side conditions on the rules, and the precise effects of these conditions in terms of proof theoretical properties are not well understood yet.

We started this paper with the contention that the most problematic aspect of the completeness proofs for update semantics consists in the non-validity of the structural rules of Permutation and Monotony. Reconsidering the proofs we have given, we can now say that the failure of Monotony is more problematic than the failure of Permutation, and generates quite a lot of bookkeeping in the proofs. It might be so that a proof system tailored as a tableau method offers more opportunities for an elegant bookkeeping of these non-monotonic phenomena. But on our current information, we are not able to assert that this is presumably so.

References

[1] Robert Goldblatt. Logics of Time and Computation. Second Edition. CSLI Lecture Notes No. 7, CSLI, Stanford, 1992.

[2] Hans Kamp, editor. Conditionals, Defaults, and Belief Revision, Edinburgh, 1990. Dyana Deliverable R2.5.A.

[3] Makoto Kanazawa. Completeness and decidabilty of the mixed style of inference with composition. In Paul Dekker and Martin Stokhof, editors, Proceedings of the Ninth Amsterdam Colloquium, pages 377–391, Institute for Language, Logic and Computation, Department of Philosophy, University of Amterdam, 1994.

[4] Johan van Benthem. Modal Logic and Classical Locic. Bibliopolis/The Humanities Press, Naples/Atlantic Heights (N.J.), 1985.

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

[6] Johan van Benthem. Language in Action. Categories, Lambdas and Dynamic Logic. North Holland, Amsterdam, 1991.

[7] Johan van Benthem. Logic and the flow of information. In D. Prawitz, B. Skyrms, and D. Westerstahl, editors, Proceedings 9th International Congress of Logic, Methodology and Philosophy of Science, Uppsala 1991. North Holland, Amsterdam, 1991.

[8] Jaap van der Does. It might be. Second Draft. Institute for Language, Logic and Computation, Department of Mathematics, University of Amsterdam, August 1994.

[9] Jan van Eijck and Fer-Jan de Vries. A sound and complete calculus for update logic. In Paul Dekker and Martin Stokhof, editors, Proceedings of the Eigth Amsterdam Colloquium, Institute for Language, Logic and Computation, Department of Philosophy, University of Amterdam, 1992. To appear in Journal of Philosophical Logic.

[10] Frank Veltman. Three complete might-logics. Unpublished Notes. Institute for Logic, Language and Computation. Department of Philosophy, University of Amsterdam, 1992.

[11] Frank Veltman. Defaults in update semantics. ITLI Prepublication Series LP-91-02, University of Amsterdam, 1991. Revised version December 1993. Also in [2].