Documentation

Linglib.Theories.Dialogue.DisjunctiveUpdate

Disjunctive Context Updating #

@cite{caie-2023}

Michael Caie. Context Dynamics. Semantics and Pragmatics 16, Article 3: 1–37.

The Problem #

Standard accounts of conversational updating (@cite{stalnaker-1978}) assume that, at each world w in the context set, there is a unique compositional context c_w interpreting an assertion of φ. The context set is updated by diagonalization: eliminate w iff ⟦φ⟧^{c_w} is false at w.

@cite{caie-2023} argues this uniqueness assumption fails for context-sensitive expressions like configurational predicates ("pair of socks"), where multiple compositional contexts may be available at a single world. Standard Updating combined with Minimal Symmetry and Preservation incorrectly predicts the falsity of Safe Information in natural discourses.

The Solution #

Disjunctive Multi-Context Updating: at each world w, there is a non-empty set I^φ_w of compositional contexts. A world w survives iff some context in I^φ_w makes φ true at w. When I^φ_w is a singleton, this reduces to Standard Updating.

Contextual Pruning: interpretation sets narrow across discourse. If β immediately follows α, the contexts available for β at w are exactly those that made α true at w.

Architecture #

Disjunctive Updating is an instance of ∃-projection from Core.Semantics.ParameterizedUpdate: the parameter is the compositional context C, and the fragment set F c w := I w c says which contexts are available at each world. disjunctiveUpdate = existentialUpdate and prune = fiberwiseFilter (both with argument order swapped).

This means general results — De Morgan duality, monotone collapse, sequential update = single conjunctive update — apply directly.

Relationship to Existing Infrastructure #

ContextSet.update c p in CommonGround.lean is the special case where every world gets the same interpretation (no context sensitivity). See disjunctiveUpdate_constant.
The SpecSpace in Supervaluation/Basic.lean is the ∀-dual: super-truth = true under ALL specs; Caie's survival = true under SOME.
CCP in Dynamic/Core/CCP.lean operates on ⟨assignment, world⟩ pairs; ContextFragment here uses ⟨compositional-context, world⟩ — a structural analogue with different conceptual content.

structure Dialogue.DisjunctiveUpdate.ContextFragment (C : Type u_3) (W : Type u_4) :

Type (max u_3 u_4)

A context fragment: an ordered pair ⟨compositional context, world⟩.

Context fragments are the state representation for Disjunctive Updating. The compositional context determines how context-sensitive expressions (indexicals, gradable adjectives, configurational predicates) are interpreted; the world determines matters of fact.

Structurally analogous to Possibility W E in Dynamic/Core/CCP.lean (⟨world, assignment⟩ pairs in dynamic semantics), but the non-world parameter is a compositional context rather than a variable assignment.

ctx : C
world : W

Instances For

@[reducible, inline]

abbrev Dialogue.DisjunctiveUpdate.InterpAssignment (C : Type u_3) (W : Type u_4) :

Type (max u_3 u_4)

An interpretation assignment maps worlds to predicates on compositional contexts. I w c holds iff c is available to interpret an assertion at w.

@cite{caie-2023}: "for each world w in the relevant context set, a non-empty set of compositional contexts that interpret that assertion of φ at w: I^φ_w."

This is a FragmentSet C W with swapped argument order: I w c ↔ F c w where F : FragmentSet C W.

Equations

Dialogue.DisjunctiveUpdate.InterpAssignment C W = (W → C → Prop)

Instances For

@[reducible, inline]

abbrev Dialogue.DisjunctiveUpdate.InterpAssignment.toFragmentSet {C : Type u_1} {W : Type u_2} (I : InterpAssignment C W) :

Core.Semantics.ParameterizedUpdate.FragmentSet C W

Convert an InterpAssignment to a FragmentSet by swapping argument order. This is the bridge between Caie's convention (index by world first) and the ParameterizedUpdate convention (index by parameter first).

Equations

I.toFragmentSet c w = I w c

Instances For

def Dialogue.DisjunctiveUpdate.standardUpdate {C : Type u_1} {W : Type u_2} (cs : Set W) (c_w : W → C) (sem : C → W → Prop) :

Set W

Standard Updating with explicit diagonalization (@cite{stalnaker-1978}, formulated following @cite{caie-2023} §1).

At each world w, a unique compositional context c_w determines the proposition expressed. The diagonal proposition is {w ∈ C : w ∈ ⟦φ⟧^{c_w}}.

Note: Assertion.Stalnaker.assert in Stalnaker.lean implements the degenerate case where the proposition is fixed across worlds (no diagonalization needed). This definition makes the compositional context parameter explicit.

Equations

Dialogue.DisjunctiveUpdate.standardUpdate cs c_w sem w = (cs w ∧ sem (c_w w) w)

Instances For

@[reducible, inline]

abbrev Dialogue.DisjunctiveUpdate.disjunctiveUpdate {C : Type u_1} {W : Type u_2} (cs : Set W) (I : InterpAssignment C W) (sem : C → W → Prop) :

Set W

Disjunctive Multi-Context Updating (@cite{caie-2023} §3).

A world w survives iff there exists some compositional context c in the interpretation set I_w such that ⟦φ⟧^c is true at w. When I_w is a singleton {c_w}, this reduces to standardUpdate.

Defined as existentialUpdate from ParameterizedUpdate with the interpretation assignment as the fragment set (argument order swapped).

@cite{caie-2023}: "The result of updating the context given the assertion is C^φ = {w ∈ C_φ : w ∈ ⟦φ⟧^c, for some c ∈ I^φ_w}."

Equations

Dialogue.DisjunctiveUpdate.disjunctiveUpdate cs I sem = Core.Semantics.ParameterizedUpdate.existentialUpdate cs I.toFragmentSet sem

Instances For

@[reducible, inline]

abbrev Dialogue.DisjunctiveUpdate.prune {C : Type u_1} {W : Type u_2} (I : InterpAssignment C W) (sem : C → W → Prop) :

InterpAssignment C W

Contextual Pruning (@cite{caie-2023} §3): restrict interpretation sets to truth-making contexts.

If β immediately follows α in a discourse at world w, the compositional contexts available for β at w are exactly those that made α true at w.

Defined as fiberwiseFilter from ParameterizedUpdate (argument order swapped).

@cite{caie-2023}: "if {c : c ∈ I^α_w and w ∈ ⟦α⟧^c} ≠ ∅, then I^β_w = {c : c ∈ I^α_w and w ∈ ⟦α⟧^c}."

Note: the paper's definition includes a non-emptiness precondition — pruning applies only when at least one context survives. This definition unconditionally restricts; in all applications here, the pruned set is non-empty by construction (both discourses have truth-making contexts at every world).

Equations

Dialogue.DisjunctiveUpdate.prune I sem w c = Core.Semantics.ParameterizedUpdate.fiberwiseFilter I.toFragmentSet sem c w

Instances For

def Dialogue.DisjunctiveUpdate.fragmentation {C : Type u_1} {W : Type u_2} (cs : Set W) (I : InterpAssignment C W) :

ContextFragment C W → Prop

The fragmentation of a context set: all ⟨c, w⟩ pairs where w is in the context set and c is an available interpretation at w.

@cite{caie-2023}: "Call a context fragment an ordered pair of a compositional context and a world, and call the fragmentation of C_φ the set of context fragments ⟨c, w⟩ such that w ∈ C_φ and c interprets φ in w."

Equations

Dialogue.DisjunctiveUpdate.fragmentation cs I f = (cs f.world ∧ I f.world f.ctx)

Instances For

def Dialogue.DisjunctiveUpdate.fragmentWorlds {C : Type u_1} {W : Type u_2} (frags : ContextFragment C W → Prop) :

Set W

Project fragments to their world components.

Equations

Dialogue.DisjunctiveUpdate.fragmentWorlds frags w = ∃ (c : C), frags { ctx := c, world := w }

Instances For

theorem Dialogue.DisjunctiveUpdate.disjunctiveUpdate_eq_fragmentWorlds {C : Type u_1} {W : Type u_2} (cs : Set W) (I : InterpAssignment C W) (sem : C → W → Prop) :

disjunctiveUpdate cs I sem = fragmentWorlds fun (f : ContextFragment C W) => fragmentation cs I f ∧ sem f.ctx f.world

Disjunctive updating is equivalent to updating the fragmentation and projecting to worlds.

theorem Dialogue.DisjunctiveUpdate.standard_eq_disjunctive_singleton {C : Type u_1} {W : Type u_2} (cs : Set W) (c_w : W → C) (sem : C → W → Prop) :

standardUpdate cs c_w sem = disjunctiveUpdate cs (fun (w : W) (c : C) => c = c_w w) sem

Standard Updating is the singleton case of Disjunctive Updating. When the interpretation set at each world is {c_w}, the existential in Disjunctive Updating collapses to a single check.

theorem Dialogue.DisjunctiveUpdate.disjunctiveUpdate_mono_interp {C : Type u_1} {W : Type u_2} (cs : Set W) (I₁ I₂ : InterpAssignment C W) (sem : C → W → Prop) (h : ∀ (w : W) (c : C), I₁ w c → I₂ w c) (w : W) :

disjunctiveUpdate cs I₁ sem w → disjunctiveUpdate cs I₂ sem w

Expanding interpretation sets can only add worlds to the result.

theorem Dialogue.DisjunctiveUpdate.disjunctiveUpdate_constant {C : Type u_1} {W : Type u_2} (cs : Set W) (c₀ : C) (sem : C → W → Prop) :

disjunctiveUpdate cs (fun (x : W) (c : C) => c = c₀) sem = fun (w : W) => cs w ∧ sem c₀ w

When there is a single fixed interpretation for all worlds, disjunctive updating reduces to propositional filtering — the mechanism formalized as ContextSet.update in CommonGround.lean.

This witnesses the fact that ContextSet.update is the degenerate case of Disjunctive Updating where context sensitivity plays no role: the same proposition is expressed at every world.

theorem Dialogue.DisjunctiveUpdate.disjunctiveUpdate_eq_contextSet_update {C : Type u_1} {W : Type u_2} (cs : Set W) (c₀ : C) (sem : C → W → Prop) :

disjunctiveUpdate cs (fun (x : W) (c : C) => c = c₀) sem = Core.CommonGround.ContextSet.update cs (sem c₀)

Disjunctive updating with a fixed context reduces to ContextSet.update.

This explicitly connects the general framework to the infrastructure in CommonGround.lean: context-insensitive assertions (same proposition at every world) update via ordinary propositional filtering.

theorem Dialogue.DisjunctiveUpdate.generalized_preservation {C : Type u_1} {W : Type u_2} (I : InterpAssignment C W) (sem : C → W → Prop) (w : W) (c₀ : C) (h_unique : ∀ (c : C), I w c ↔ c = c₀) (h_true : sem c₀ w) (c : C) :

prune I sem w c ↔ c = c₀

Generalized Preservation (@cite{caie-2023} §3): if there is a unique compositional context interpreting α at w, and it makes α true, then it persists as the unique context for subsequent assertions.

@cite{caie-2023}: "for each w ∈ C_α if there is a unique compositional context c that interprets an assertion of α in w, then if w ∈ C^α, then c uniquely interprets the subsequent assertion of β in w."

This follows directly from Contextual Pruning: when the input is a singleton and the element makes α true, pruning preserves it.

def Dialogue.DisjunctiveUpdate.discourseStep {C : Type u_1} {W : Type u_2} (cs : Set W) (I : InterpAssignment C W) (sem : C → W → Prop) :

Set W × InterpAssignment C W

A discourse step: update the context set and prune interpretation sets. Returns the new context set and the narrowed interpretation assignment.

Equations

Dialogue.DisjunctiveUpdate.discourseStep cs I sem = (Dialogue.DisjunctiveUpdate.disjunctiveUpdate cs I sem, Dialogue.DisjunctiveUpdate.prune I sem)

Instances For

theorem Dialogue.DisjunctiveUpdate.discourseStep_restricts {C : Type u_1} {W : Type u_2} (cs : Set W) (I : InterpAssignment C W) (sem : C → W → Prop) :

match discourseStep cs I sem with | (cs', I') => (∀ (w : W), cs' w → cs w) ∧ ∀ (w : W) (c : C), I' w c → I w c

Sequential discourse steps are monotonically restrictive in both the context set and interpretation sets.

theorem Dialogue.DisjunctiveUpdate.contextual_pruning_sequential {C : Type u_1} {W : Type u_2} (cs : Set W) (I : InterpAssignment C W) (sem₁ sem₂ : C → W → Prop) :

disjunctiveUpdate (disjunctiveUpdate cs I sem₁) (prune I sem₁) sem₂ = disjunctiveUpdate cs I fun (c : C) (w : W) => sem₁ c w ∧ sem₂ c w

Contextual Pruning reduces to the general sequential ∃-update theorem: asserting α then β (with pruned parameters) = single ∃-update checking both α and β under the same parameter.

This is @cite{caie-2023}'s central mechanism, obtained for free from sequential_existentialUpdate in ParameterizedUpdate.lean.

Sarah's Socks (@cite{caie-2023} §2.1) #

Tim has strong preferences about socks. Two discourses communicate that Tim likes matching socks and dislikes mixed ones:

Tim Likes Matching: (1) Sarah has two pairs of socks. (2) Tim likes both of them. (3) Both of them are matching.

Tim Dislikes Mixed: (1) Sarah has two pairs of socks. (4) Tim dislikes both of them. (5) Both of them are mixed.

Model #

Worlds (TimPref): Tim likes matching pairs, or likes mixed pairs.
Contexts (DressInt): dressing intension is matching or mixed.
Initial interpretation set: both intensions at every world.
4 context fragments: {matching, mixed} × {likesMatching, likesMixed}.

Verification Table (from @cite{caie-2023}) #

For Tim Likes Matching:

	C⁽¹⁾	C⁽¹⁾⁽²⁾	C⁽¹⁾⁽²⁾⁽³⁾
⟨matchInt, wMatch⟩	✓	✓	✓
⟨mixedInt, wMatch⟩	✓	✗	✗
⟨matchInt, wMixed⟩	✓	✗	✗
⟨mixedInt, wMixed⟩	✓	✓	✗

Only ⟨matchInt, wMatch⟩ survives: Tim likes matching socks.

inductive Dialogue.DisjunctiveUpdate.TimPref :

Tim's preference: the world parameter.

likesMatching : TimPref
likesMixed : TimPref

Instances For

@[implicit_reducible]

instance Dialogue.DisjunctiveUpdate.instDecidableEqTimPref :

DecidableEq TimPref

Equations

Dialogue.DisjunctiveUpdate.instDecidableEqTimPref x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Dialogue.DisjunctiveUpdate.instReprTimPref :

Equations

Dialogue.DisjunctiveUpdate.instReprTimPref = { reprPrec := Dialogue.DisjunctiveUpdate.instReprTimPref.repr }

def Dialogue.DisjunctiveUpdate.instReprTimPref.repr :

TimPref → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.

Instances For

inductive Dialogue.DisjunctiveUpdate.DressInt :

Dressing intension: the compositional context parameter. Determines which non-overlapping pairings of Sarah's socks are in the domain of quantification.

matching : DressInt
mixed : DressInt

Instances For

@[implicit_reducible]

instance Dialogue.DisjunctiveUpdate.instDecidableEqDressInt :

DecidableEq DressInt

Equations

Dialogue.DisjunctiveUpdate.instDecidableEqDressInt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Dialogue.DisjunctiveUpdate.instReprDressInt.repr :

DressInt → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.

Instances For

@[implicit_reducible]

instance Dialogue.DisjunctiveUpdate.instReprDressInt :

Equations

Dialogue.DisjunctiveUpdate.instReprDressInt = { reprPrec := Dialogue.DisjunctiveUpdate.instReprDressInt.repr }

def Dialogue.DisjunctiveUpdate.SarahsSocks.likes :

DressInt → TimPref → Prop

"Tim likes both of them": true when the intension picks the kind of pairs Tim likes.

Equations

Instances For

@[implicit_reducible]

instance Dialogue.DisjunctiveUpdate.SarahsSocks.instDecidableLikes (c : DressInt) (w : TimPref) :

Decidable (likes c w)

Equations

def Dialogue.DisjunctiveUpdate.SarahsSocks.dislikes (c : DressInt) (w : TimPref) :

"Tim dislikes both of them": complement of likes.

Equations

Dialogue.DisjunctiveUpdate.SarahsSocks.dislikes c w = ¬Dialogue.DisjunctiveUpdate.SarahsSocks.likes c w

Instances For

@[implicit_reducible]

instance Dialogue.DisjunctiveUpdate.SarahsSocks.instDecidableDislikes (c : DressInt) (w : TimPref) :

Decidable (dislikes c w)

Equations

Dialogue.DisjunctiveUpdate.SarahsSocks.instDecidableDislikes c w = Dialogue.DisjunctiveUpdate.SarahsSocks.instDecidableDislikes._aux_1 c w

def Dialogue.DisjunctiveUpdate.SarahsSocks.isMatching :

DressInt → TimPref → Prop

"Both of them are matching": true under matching intension.

Equations

Instances For

@[implicit_reducible]

instance Dialogue.DisjunctiveUpdate.SarahsSocks.instDecidableIsMatching (c : DressInt) (w : TimPref) :

Decidable (isMatching c w)

Equations

Dialogue.DisjunctiveUpdate.SarahsSocks.instDecidableIsMatching Dialogue.DisjunctiveUpdate.DressInt.matching x✝ = isTrue trivial
Dialogue.DisjunctiveUpdate.SarahsSocks.instDecidableIsMatching Dialogue.DisjunctiveUpdate.DressInt.mixed x✝ = isFalse ⋯

def Dialogue.DisjunctiveUpdate.SarahsSocks.isMixed :

DressInt → TimPref → Prop

"Both of them are mixed": true under mixed intension.

Equations

Instances For

@[implicit_reducible]

instance Dialogue.DisjunctiveUpdate.SarahsSocks.instDecidableIsMixed (c : DressInt) (w : TimPref) :

Decidable (isMixed c w)

Equations

Dialogue.DisjunctiveUpdate.SarahsSocks.instDecidableIsMixed Dialogue.DisjunctiveUpdate.DressInt.mixed x✝ = isTrue trivial
Dialogue.DisjunctiveUpdate.SarahsSocks.instDecidableIsMixed Dialogue.DisjunctiveUpdate.DressInt.matching x✝ = isFalse ⋯

def Dialogue.DisjunctiveUpdate.SarahsSocks.timLikesMatchingResult (w : TimPref) :

Tim Likes Matching result: w survives iff there exists a context c such that likes c w (surviving (2)) AND isMatching c w (surviving (3)). The conjunction arises from Contextual Pruning: only contexts that made (2) true are available to interpret (3).

Equations

One or more equations did not get rendered due to their size.

Instances For

@[implicit_reducible]

instance Dialogue.DisjunctiveUpdate.SarahsSocks.instDecidableTimLikesMatchingResult (w : TimPref) :

Decidable (timLikesMatchingResult w)

Equations

Dialogue.DisjunctiveUpdate.SarahsSocks.instDecidableTimLikesMatchingResult w = Dialogue.DisjunctiveUpdate.SarahsSocks.instDecidableTimLikesMatchingResult._aux_1 w

def Dialogue.DisjunctiveUpdate.SarahsSocks.timDislikesMixedResult (w : TimPref) :

Tim Dislikes Mixed result: w survives iff ∃ c, dislikes c w ∧ isMixed c w.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[implicit_reducible]

instance Dialogue.DisjunctiveUpdate.SarahsSocks.instDecidableTimDislikesMixedResult (w : TimPref) :

Decidable (timDislikesMixedResult w)

Equations

Dialogue.DisjunctiveUpdate.SarahsSocks.instDecidableTimDislikesMixedResult w = Dialogue.DisjunctiveUpdate.SarahsSocks.instDecidableTimDislikesMixedResult._aux_1 w

theorem Dialogue.DisjunctiveUpdate.SarahsSocks.tlm_keeps_matching :

timLikesMatchingResult TimPref.likesMatching

Tim Likes Matching keeps the matching-preference world.

theorem Dialogue.DisjunctiveUpdate.SarahsSocks.tlm_eliminates_mixed :

¬timLikesMatchingResult TimPref.likesMixed

Tim Likes Matching eliminates the mixed-preference world.

theorem Dialogue.DisjunctiveUpdate.SarahsSocks.tdm_keeps_matching :

timDislikesMixedResult TimPref.likesMatching

Tim Dislikes Mixed keeps the matching-preference world.

theorem Dialogue.DisjunctiveUpdate.SarahsSocks.tdm_eliminates_mixed :

¬timDislikesMixedResult TimPref.likesMixed

Tim Dislikes Mixed eliminates the mixed-preference world.

theorem Dialogue.DisjunctiveUpdate.SarahsSocks.discourses_agree (w : TimPref) :

timLikesMatchingResult w ↔ timDislikesMixedResult w

Both discourses yield the same result.

def Dialogue.DisjunctiveUpdate.SarahsSocks.facts (w : TimPref) :

The set of fact-worlds: those where Tim likes matching and dislikes mixed.

Equations

Instances For

@[implicit_reducible]

instance Dialogue.DisjunctiveUpdate.SarahsSocks.instDecidableFacts (w : TimPref) :

Decidable (facts w)

Equations

theorem Dialogue.DisjunctiveUpdate.SarahsSocks.safe_info_i_tlm (w : TimPref) :

timLikesMatchingResult w → facts w

Safe Information condition (i): the update result is a subset of the fact-worlds. Under Disjunctive Updating, asserting Tim Likes Matching eliminates all non-fact worlds.

theorem Dialogue.DisjunctiveUpdate.SarahsSocks.safe_info_ii_tlm (w : TimPref) :

facts w → timLikesMatchingResult w

Safe Information condition (ii): every fact-world where the discourse occurs is retained.

theorem Dialogue.DisjunctiveUpdate.SarahsSocks.safe_info_i_tdm (w : TimPref) :

timDislikesMixedResult w → facts w

Safe Information condition (i) for Tim Dislikes Mixed.

theorem Dialogue.DisjunctiveUpdate.SarahsSocks.safe_info_ii_tdm (w : TimPref) :

facts w → timDislikesMixedResult w

Safe Information condition (ii) for Tim Dislikes Mixed.

theorem Dialogue.DisjunctiveUpdate.SarahsSocks.standard_update_incompatible (c : DressInt) (w : TimPref) :

¬(likes c w ∧ dislikes c w)

@cite{caie-2023} §2.2, first Claim: Standard Updating + Preservation + Minimal Symmetry → ¬Safe Information.

Under Minimal Symmetry, the same dressing intension c interprets sentence (1) in both discourses (at fact-worlds w₁ and w₂ that agree on all pre-assertion facts). Under Preservation, c persists to interpret later sentences. Safe Information (ii) then requires:

likes c w (for TLM to retain a fact-world)
dislikes c w (for TDM to retain a fact-world) But dislikes = ¬likes, so no intension c satisfies both.

This is the paper's central argument against Standard Updating.

theorem Dialogue.DisjunctiveUpdate.SarahsSocks.uniform_charity_retains_nonfact :

(∃ (c : DressInt), likes c TimPref.likesMixed) ∧ (∃ (c : DressInt), isMatching c TimPref.likesMixed) ∧ ¬facts TimPref.likesMixed

@cite{caie-2023} §2.2, second Claim: Standard Updating + Uniform Charity → ¬Safe Information (condition i).

Under Uniform Charity (prefer truth-making interpretations), each sentence individually has a truth-making context at every world. Under Standard Updating (unique context per sentence, shifts allowed), each sentence is interpreted by its truth-making context. No world is eliminated, so the update result includes non-fact worlds.

Witness: at .likesMixed, sentence (2) is true under mixed intension (Tim likes mixed pairs in that world) and sentence (3) is true under matching intension. Yet .likesMixed is not a fact-world.

theorem Dialogue.DisjunctiveUpdate.SarahsSocks.tlm_agrees_with_framework (w : TimPref) :

timLikesMatchingResult w ↔ disjunctiveUpdate (disjunctiveUpdate (fun (x : TimPref) => True) (fun (x : TimPref) (x_1 : DressInt) => True) fun (c : DressInt) (w : TimPref) => likes c w) (prune (fun (x : TimPref) (x_1 : DressInt) => True) fun (c : DressInt) (w : TimPref) => likes c w) (fun (c : DressInt) (w : TimPref) => isMatching c w) w

The hand-computed Tim Likes Matching result agrees with the Prop-valued disjunctiveUpdate applied via discourseStep.

This connects the hand-computed verification above to the general theory.

theorem Dialogue.DisjunctiveUpdate.SarahsSocks.tdm_agrees_with_framework (w : TimPref) :

timDislikesMixedResult w ↔ disjunctiveUpdate (disjunctiveUpdate (fun (x : TimPref) => True) (fun (x : TimPref) (x_1 : DressInt) => True) fun (c : DressInt) (w : TimPref) => dislikes c w) (prune (fun (x : TimPref) (x_1 : DressInt) => True) fun (c : DressInt) (w : TimPref) => dislikes c w) (fun (c : DressInt) (w : TimPref) => isMixed c w) w

The hand-computed Tim Dislikes Mixed result agrees with the Prop-valued framework. Mirror of tlm_agrees_with_framework.

theorem Dialogue.DisjunctiveUpdate.SarahsSocks.dislikes_eq_not_likes (c : DressInt) (w : TimPref) :

dislikes c w ↔ ¬likes c w

Dislikes is the complement of likes.

theorem Dialogue.DisjunctiveUpdate.SarahsSocks.matching_mixed_compl (c : DressInt) (w : TimPref) :

isMatching c w ↔ ¬isMixed c w

isMatching and isMixed are complements.