Caie 2023: disjunctive context updating

This file formalizes the account of conversational updating in [Cai23]. On the orthodox account ([Sta78]) each world in the context set fixes a unique compositional context ([Kap89]) that interprets an assertion there, and updating proceeds by diagonalization: eliminate a world exactly when the proposition the assertion expresses at it is false there. Caie argues that a discourse like Sarah has two pairs of socks. Tim likes both of them. Both of them are matching. refutes the uniqueness assumption. Its first sentence leaves matching and mixed pairings of Sarah's four socks equally available, and the discourse conveys Tim's preference only because the second sentence narrows the pairings that interpret the third. Dropping uniqueness, a world survives when some available context makes the assertion true, and the contexts available to an assertion are those that made its predecessor true.

Both accounts update by asserting a diagonal proposition, so the revision is to the proposition asserted rather than to the update rule: diagonal evaluates the semantics at each world's chosen context, disjunctiveDiagonal quantifies existentially over the contexts available there.

Main definitions

• diagonal, disjunctiveDiagonal — the propositions Standard and Disjunctive Updating assert
• prune — Contextual Pruning: the contexts an assertion leaves to its successor
• fragments, updateFragments — the ⟨context, world⟩ pairs and their filtration
• run — a discourse, each assertion pruning the next
• Charitable — Uniform Charity, the context shift Standard Updating needs

Main results

• fragments_prune — one filtration of the fragment set updates and prunes at once
• run_eq_inter — a discourse updates on the conjunction of its sentences under one context
• prune_singleton — a unique interpretation is passed on to the next assertion
• run_timLikesMatching, run_timDislikesMixed — either discourse leaves exactly the worlds where the Facts hold, so Safe Information holds of both
• preservation_drops_fact_world, charity_not_safe — the two horns of the dilemma facing Standard Updating

References

• [Cai23]
• [Sta78]
• [Kap89]
• [Kri09b]
• [Bar02b]
• [Bar13]

The propositions the two accounts assert

def Caie2023.diagonal {C : Type u_1} {W : Type u_2} (interp : W → C) (sem : C → W → Prop) : Set W

The proposition Standard Updating asserts ([Sta78]): a world belongs to it when the assertion is true there under the unique compositional context that interprets it there.

Equations

• Caie2023.diagonal interp sem = {w : W | sem (interp w) w}

def Caie2023.disjunctiveDiagonal {C : Type u_1} {W : Type u_2} (I : W → Set C) (sem : C → W → Prop) : Set W

The proposition Disjunctive Multi-Context Updating asserts: a world belongs to it when the assertion is true there under some context available there, so a world is eliminated only when the disjunction of the propositions the assertion expresses at it is false there.

Equations

• Caie2023.disjunctiveDiagonal I sem = {w : W | ∃ c ∈ I w, sem c w}

theorem Caie2023.contextSet_assert_disjunctiveDiagonal {C : Type u_1} {W : Type u_2} (cs : Set W) (I : W → Set C) (sem : C → W → Prop) : HasCommonGround.contextSet (HasAssertion.assert (Filter.principal cs) (disjunctiveDiagonal I sem)) = cs ∩ disjunctiveDiagonal I sem

Updating a context set is Stalnakerian assertion of the diagonal proposition ([Sta78]), on either account: the accounts differ in the proposition asserted, not in the rule that consumes it.

theorem Caie2023.disjunctiveDiagonal_singleton {C : Type u_1} {W : Type u_2} (interp : W → C) (sem : C → W → Prop) : disjunctiveDiagonal (fun (w : W) => {interp w}) sem = diagonal interp sem

Where a unique context interprets the assertion, the disjunction collapses to the diagonal: Disjunctive Updating is Standard Updating shorn of the uniqueness assumption.

theorem Caie2023.diagonal_subset_disjunctiveDiagonal {C : Type u_1} {W : Type u_2} (interp : W → C) (I : W → Set C) (sem : C → W → Prop) (h : ∀ (w : W), interp w ∈ I w) : diagonal interp sem ⊆ disjunctiveDiagonal I sem

Standard Updating eliminates at least as much as Disjunctive Updating, whenever the context it selects is one of the available ones.

def Caie2023.Charitable {C : Type u_1} {W : Type u_2} (interp : W → C) (sem : C → W → Prop) : Prop

Uniform Charity ([Cai23] §2.2): where some compositional context makes an assertion true at a world, the context that interprets it there is one that does.

Equations

• Caie2023.Charitable interp sem = ∀ (w : W), (∃ (c : C), sem c w) → sem (interp w) w

theorem Caie2023.inter_diagonal_of_charitable {C : Type u_1} {W : Type u_2} (cs : Set W) (interp : W → C) (sem : C → W → Prop) (hch : Charitable interp sem) (h : ∀ w ∈ cs, ∃ (c : C), sem c w) : cs ∩ diagonal interp sem = cs

A charitable interpretation eliminates no world at which any context makes the assertion true.

Contextual pruning

def Caie2023.prune {C : Type u_1} {W : Type u_2} (I : W → Set C) (sem : C → W → Prop) : W → Set C

Contextual Pruning ([Cai23] §3): the contexts that interpret the next assertion at a world are those that made this one true there.

Equations

• Caie2023.prune I sem w = {c : C | c ∈ I w ∧ sem c w}

theorem Caie2023.prune_nonempty_iff {C : Type u_1} {W : Type u_2} (I : W → Set C) (sem : C → W → Prop) (w : W) : (prune I sem w).Nonempty ↔ w ∈ disjunctiveDiagonal I sem

Pruning leaves a context available exactly at the worlds the assertion does not eliminate, so the paper's proviso — that pruning applies only where some context survives — holds at every world of the updated context set.

theorem Caie2023.prune_singleton {C : Type u_1} {W : Type u_2} (I : W → Set C) (sem : C → W → Prop) (w : W) (c₀ : C) (h : I w = {c₀}) (htrue : sem c₀ w) : prune I sem w = {c₀}

Generalized Preservation ([Cai23] §3): a context that uniquely interprets an assertion at a world the assertion does not eliminate uniquely interprets the next assertion there.

Context fragments

def Caie2023.fragments {C : Type u_1} {W : Type u_2} (cs : Set W) (I : W → Set C) : Set (C × W)

The fragmentation of a context set: the ⟨compositional context, world⟩ pairs whose world is in the context set and whose context interprets the assertion there. Conversational states of this shape are those of [Bar02b] and [Bar13], where the non-world component fixes the delineation of a gradable adjective.

Equations

• Caie2023.fragments cs I = {f : C × W | f.2 ∈ cs ∧ f.1 ∈ I f.2}

def Caie2023.updateFragments {C : Type u_1} {W : Type u_2} (sem : C → W → Prop) (X : Set (C × W)) : Set (C × W)

Updating a set of context fragments: drop every fragment whose context makes the assertion false at its world.

Equations

• Caie2023.updateFragments sem X = {f : C × W | f ∈ X ∧ sem f.1 f.2}

theorem Caie2023.fragments_prune {C : Type u_1} {W : Type u_2} (cs : Set W) (I : W → Set C) (sem : C → W → Prop) : fragments (cs ∩ disjunctiveDiagonal I sem) (prune I sem) = updateFragments sem (fragments cs I)

One filtration of the fragment set does the work of both parts of an update step: the fragments of the updated context set under the pruned interpretations are exactly the fragments that survive the assertion.

theorem Caie2023.snd_image_updateFragments {C : Type u_1} {W : Type u_2} (cs : Set W) (I : W → Set C) (sem : C → W → Prop) : Prod.snd '' updateFragments sem (fragments cs I) = cs ∩ disjunctiveDiagonal I sem

The updated context set is the world components of the surviving fragments.

Discourses

def Caie2023.run {C : Type u_1} {W : Type u_2} : Set W → (W → Set C) → List (C → W → Prop) → Set W

A discourse: each assertion updates the context set and prunes the contexts available to its successor. The worlds where an assertion does not occur are taken to have been eliminated before it is evaluated, as they are in the paper.

Equations

• Caie2023.run x✝¹ x✝ [] = x✝¹
• Caie2023.run x✝¹ x✝ (sem :: rest) = Caie2023.run (x✝¹ ∩ Caie2023.disjunctiveDiagonal x✝ sem) (Caie2023.prune x✝ sem) rest

theorem Caie2023.run_eq_inter {C : Type u_1} {W : Type u_2} (cs : Set W) (I : W → Set C) (ss : List (C → W → Prop)) (h : ∀ w ∈ cs, (I w).Nonempty) : run cs I ss = cs ∩ disjunctiveDiagonal I fun (c : C) (w : W) => ∀ s ∈ ss, s c w

A discourse eliminates a world exactly when no context available there at the outset makes all of its sentences true: pruning makes a discourse update on the conjunction of its sentences under a single interpretation.

Sarah's socks

inductive Caie2023.Pairing : Type

The two kinds of pairing of Sarah's four socks: two striped or two solid (matching), or one striped and one solid (mixed). A dressing intension puts the pairings of one kind in the domain of quantification of the configurational predicate pair of socks ([Kri09b]), and Tim likes the pairs of one kind and dislikes those of the other, so a compositional context and a world of the reduced model are each a Pairing.

• matching : Pairing
• mixed : Pairing

@[instance_reducible]

instance Caie2023.instDecidableEqPairing : DecidableEq Pairing

Equations

• Caie2023.instDecidableEqPairing x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Caie2023.SarahsSocks.hasTwoPairs : Pairing → Pairing → Prop

(1) Sarah has two pairs of socks: true under every dressing intension, since each puts exactly two non-overlapping pairings in the domain, and so uninformative.

Equations

• Caie2023.SarahsSocks.hasTwoPairs x✝¹ x✝ = True

def Caie2023.SarahsSocks.likesBoth (c w : Pairing) : Prop

(2) Tim likes both of them: true when the pairings in the domain are of the kind Tim likes.

Equations

• Caie2023.SarahsSocks.likesBoth c w = (c = w)

def Caie2023.SarahsSocks.bothMatching (c : Pairing) : Pairing → Prop

(3) Both of them are matching: true under a matching dressing intension, whatever Tim's preferences.

Equations

• Caie2023.SarahsSocks.bothMatching c x✝ = (c = Caie2023.Pairing.matching)

def Caie2023.SarahsSocks.dislikesBoth (c w : Pairing) : Prop

(4) Tim dislikes both of them: true when the pairings in the domain are of the kind Tim dislikes.

Equations

• Caie2023.SarahsSocks.dislikesBoth c w = (c ≠ w)

def Caie2023.SarahsSocks.bothMixed (c : Pairing) : Pairing → Prop

(5) Both of them are mixed.

Equations

• Caie2023.SarahsSocks.bothMixed c x✝ = (c = Caie2023.Pairing.mixed)

def Caie2023.SarahsSocks.initial : Pairing → Set Pairing

Initial Context ([Cai23] §3): the presuppositions are symmetric between the two kinds of pairing, so both intensions interpret (1) at every world.

Equations

• Caie2023.SarahsSocks.initial x✝ = Set.univ

def Caie2023.SarahsSocks.facts : Set Pairing

The Facts: Tim likes matching pairs of socks and dislikes mixed ones.

Equations

• Caie2023.SarahsSocks.facts = {w : Caie2023.Pairing | Caie2023.SarahsSocks.likesBoth Caie2023.Pairing.matching w}

def Caie2023.SarahsSocks.timLikesMatching : List (Pairing → Pairing → Prop)

Tim Likes Matching: (1), (2), (3).

Equations

• Caie2023.SarahsSocks.timLikesMatching = [Caie2023.SarahsSocks.hasTwoPairs, Caie2023.SarahsSocks.likesBoth, Caie2023.SarahsSocks.bothMatching]

def Caie2023.SarahsSocks.timDislikesMixed : List (Pairing → Pairing → Prop)

Tim Dislikes Mixed: (1), (4), (5).

Equations

• Caie2023.SarahsSocks.timDislikesMixed = [Caie2023.SarahsSocks.hasTwoPairs, Caie2023.SarahsSocks.dislikesBoth, Caie2023.SarahsSocks.bothMixed]

theorem Caie2023.SarahsSocks.run_timLikesMatching : run Set.univ initial timLikesMatching = facts

Safe Information for Tim Likes Matching: the discourse leaves exactly the worlds where the Facts hold, so it conveys Tim's preference (condition (i)) and eliminates no world where it holds (condition (ii)).

theorem Caie2023.SarahsSocks.run_timDislikesMixed : run Set.univ initial timDislikesMixed = facts

Safe Information for Tim Dislikes Mixed: the discourse that says the opposite of each of (2) and (3) leaves the same worlds.

Why Standard Updating fails

theorem Caie2023.SarahsSocks.preservation_drops_fact_world (c : Pairing) : ¬(facts ⊆ diagonal (fun (x : Pairing) => c) likesBoth ∧ facts ⊆ diagonal (fun (x : Pairing) => c) dislikesBoth)

Minimal Symmetry gives the two discourses a compositional context that interprets their common first sentence in both, and Preservation carries it to the second sentence of each. No dressing intension makes both (2) and (4) true where the Facts hold, so one of the discourses eliminates a world where they do: Safe Information (ii) fails.

theorem Caie2023.SarahsSocks.exists_true_intension (w : Pairing) : (∃ (c : Pairing), likesBoth c w) ∧ (∃ (c : Pairing), dislikesBoth c w) ∧ (∃ (c : Pairing), bothMatching c w) ∧ ∃ (c : Pairing), bothMixed c w

Every sentence of either discourse is true at every world under some dressing intension, so Uniform Charity governs the interpretation of each of them.

theorem Caie2023.SarahsSocks.charity_not_safe (interp₂ interp₃ : Pairing → Pairing) (h₂ : Charitable interp₂ likesBoth) (h₃ : Charitable interp₃ bothMatching) : ¬Set.univ ∩ diagonal interp₂ likesBoth ∩ diagonal interp₃ bothMatching ⊆ facts

Avoiding the first horn by letting the context shift between sentences costs the second: under Uniform Charity (2) and (3) are each interpreted so as to come out true, neither eliminates anything, and the worlds where Tim likes mixed pairs survive the discourse. Safe Information (i) fails.