Disjunctive Context Updating

[Cai23]

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

The Problem

Standard accounts of conversational updating ([Sta78]) 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.

[Cai23] 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 over a fragment set (§ 0): meaning depends on a parameter — here 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).

The § 0 substrate is deliberately framework-general (thresholds, precisifications, comparison classes, assignments are all parameters in the same sense), so the 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/Update.lean operates on ⟨assignment, world⟩ pairs; ContextFragment here uses ⟨compositional-context, world⟩ — a structural analogue with different conceptual content.

Framework-agnostic infrastructure for parameter uncertainty: meaning depends on a parameter (threshold, compositional context, comparison class, variable assignment) and truth at a world involves quantifying over available parameters.

A fragment set F ⊆ P × W is a fiber bundle over worlds W; the fiber at w, F_w = {p : F(p, w)}, collects the parameters available at that world. An assertion φ with parameterized semantics ⟦φ⟧ : P → W → Prop acts as a fiberwise filter: F' = {(p, w) ∈ F : ⟦φ⟧(p, w)}. Theories differ in how they project from the bundle back to worlds, via the ∃ ⊣ Δ ⊣ ∀ adjunction:

• ∃-projection ([Cai23], [Bar02a]): w survives iff ∃ p ∈ F_w, ⟦φ⟧(p, w)
• ∀-projection (supervaluation, [Fin75]): w survives iff ∀ p ∈ F_w, ⟦φ⟧(p, w)
• Σ-projection (RSA, [LG17]): score(w) = Σ_p weight(p) · ⟦φ⟧(p, w) — a soft interpolation, not formalized here

Comparison classes ([Kle80]) are ∃-projected parameters in the same sense. When the semantics is antitone in the parameter (degree semantics: d > θ), the projections collapse to extremal checks, and the gap between min and max is the borderline region where ∃ and ∀ disagree.

@[reducible, inline]

abbrev Caie2023.FragmentSet (P : Type u_3) (W : Type u_4) : Type (max u_3 u_4)

A fragment set: a relation between parameters and worlds. F(p, w) holds iff parameter p is available at world w. The fiber at w is F_w = {p : F p w}.

Generalizes InterpAssignment C W from [Cai23] (argument order swapped).

Equations

• Caie2023.FragmentSet P W = (P → W → Prop)

def Caie2023.fiberwiseFilter {P : Type u_1} {W : Type u_2} (F : FragmentSet P W) (sem : P → W → Prop) : FragmentSet P W

Fiberwise filter: restrict a fragment set to parameter–world pairs where the semantics holds.

Generalizes Contextual Pruning ([Cai23]): after asserting α, only parameters that made α true remain available.

Equations

• Caie2023.fiberwiseFilter F sem p w = (F p w ∧ sem p w)

def Caie2023.existentialProjection {P : Type u_1} {W : Type u_2} (F : FragmentSet P W) (sem : P → W → Prop) : Set W

Existential projection: w survives iff some parameter in F_w makes the semantics true.

This is [Cai23]'s disjunctive updating and [Bar02a]'s dynamics of vagueness.

Equations

• Caie2023.existentialProjection F sem w = ∃ (p : P), F p w ∧ sem p w

def Caie2023.universalProjection {P : Type u_1} {W : Type u_2} (F : FragmentSet P W) (sem : P → W → Prop) : Set W

Universal projection: w survives iff all parameters in F_w make the semantics true.

This is super-truth ([Fin75]): truth under all admissible precisifications.

Equations

• Caie2023.universalProjection F sem w = ∀ (p : P), F p w → sem p w

def Caie2023.existentialUpdate {P : Type u_1} {W : Type u_2} (cs : Set W) (F : FragmentSet P W) (sem : P → W → Prop) : Set W

Existential update: restrict to the context set, then ∃-project.

existentialUpdate cs F sem w ↔ w ∈ cs ∧ ∃ p ∈ F_w, sem(p, w).

Equations

• Caie2023.existentialUpdate cs F sem w = (cs w ∧ Caie2023.existentialProjection F sem w)

def Caie2023.universalUpdate {P : Type u_1} {W : Type u_2} (cs : Set W) (F : FragmentSet P W) (sem : P → W → Prop) : Set W

Universal update: restrict to the context set, then ∀-project.

universalUpdate cs F sem w ↔ w ∈ cs ∧ ∀ p ∈ F_w, sem(p, w).

Equations

• Caie2023.universalUpdate cs F sem w = (cs w ∧ Caie2023.universalProjection F sem w)

theorem Caie2023.deMorgan_existential_universal {P : Type u_1} {W : Type u_2} (F : FragmentSet P W) (sem : P → W → Prop) (w : W) : existentialProjection F sem w ↔ ¬universalProjection F (fun (p : P) (w : W) => ¬sem p w) w

De Morgan duality (∃-side): ∃-projection of sem ↔ negation of ∀-projection of the negation.

theorem Caie2023.deMorgan_universal_existential {P : Type u_1} {W : Type u_2} (F : FragmentSet P W) (sem : P → W → Prop) (w : W) : universalProjection F sem w ↔ ¬existentialProjection F (fun (p : P) (w : W) => ¬sem p w) w

De Morgan duality (∀-side): ∀-projection of sem ↔ negation of ∃-projection of the negation.

theorem Caie2023.monotoneCollapse_exists {P : Type u_1} {W : Type u_2} [Preorder P] (F : FragmentSet P W) (sem : P → W → Prop) (w : W) (p₀ : P) (h_least : IsLeast {p : P | F p w} p₀) (h_anti : Antitone fun (p : P) => sem p w) : existentialProjection F sem w ↔ sem p₀ w

Monotone collapse (∃): when sem is Antitone in p and F_w has a least element, ∃-projection reduces to checking the minimum.

The Antitone condition on fun p => sem p w means p₁ ≤ p₂ → sem p₂ w → sem p₁ w — truth propagates downward in the parameter ordering. This is the standard situation in degree semantics: ⟦tall⟧(θ, w) = degree(w) > θ is antitone in θ.

theorem Caie2023.monotoneCollapse_forall {P : Type u_1} {W : Type u_2} [Preorder P] (F : FragmentSet P W) (sem : P → W → Prop) (w : W) (p₀ : P) (h_greatest : IsGreatest {p : P | F p w} p₀) (h_anti : Antitone fun (p : P) => sem p w) : universalProjection F sem w ↔ sem p₀ w

Monotone collapse (∀): when sem is Antitone in p and F_w has a greatest element, ∀-projection reduces to checking the maximum.

For degree semantics: the ∀-projection ∀ θ ∈ Θ, degree(w) > θ collapses to degree(w) > max(Θ).

theorem Caie2023.projections_agree_iff_clear {P : Type u_1} {W : Type u_2} [Preorder P] (F : FragmentSet P W) (sem : P → W → Prop) (w : W) (p_min p_max : P) (h_least : IsLeast {p : P | F p w} p_min) (h_greatest : IsGreatest {p : P | F p w} p_max) (h_anti : Antitone fun (p : P) => sem p w) : (existentialProjection F sem w ↔ universalProjection F sem w) ↔ sem p_max w ∨ ¬sem p_min w

Corollary: when sem is antitone and F_w has both a least and greatest element, the ∃ and ∀ projections agree iff w is outside the borderline region — either sem holds at the hardest parameter (clearly in) or fails at the easiest (clearly out).

The borderline region where projections disagree is precisely sem p_min w ∧ ¬ sem p_max w.

theorem Caie2023.sequential_existentialUpdate {P : Type u_1} {W : Type u_2} (cs : Set W) (F : FragmentSet P W) (sem₁ sem₂ : P → W → Prop) : existentialUpdate (existentialUpdate cs F sem₁) (fiberwiseFilter F sem₁) sem₂ = existentialUpdate cs F fun (p : P) (w : W) => sem₁ p w ∧ sem₂ p w

Sequential ∃-update with pruning: asserting α then β (where β's parameters are pruned by α) equals a single ∃-update checking both α and β.

This is the general form of Contextual Pruning ([Cai23]): the two-step process (update context set by α, prune parameters by α, then update by β) is equivalent to a single update requiring both α and β under the same parameter.

theorem Caie2023.sequential_universalUpdate {P : Type u_1} {W : Type u_2} (cs : Set W) (F : FragmentSet P W) (sem₁ sem₂ : P → W → Prop) : universalUpdate (universalUpdate cs F sem₁) (fiberwiseFilter F sem₁) sem₂ = universalUpdate cs F fun (p : P) (w : W) => sem₁ p w ∧ sem₂ p w

Sequential ∀-update with pruning: asserting α then β (where β's parameters are pruned by α) equals a single ∀-update checking both α and β.

The ∀ case works because: if all parameters satisfy α (first step), then "pruned parameters" = "all parameters", so requiring β for pruned parameters = requiring β for all parameters.

theorem Caie2023.existentialProjection_mono {P : Type u_1} {W : Type u_2} (F₁ F₂ : FragmentSet P W) (sem : P → W → Prop) (h : ∀ (p : P) (w : W), F₁ p w → F₂ p w) (w : W) : existentialProjection F₁ sem w → existentialProjection F₂ sem w

∃-projection is Monotone in the fragment set: expanding available parameters can only add surviving worlds. The FragmentSet P W type P → W → Prop carries the pointwise → ordering, and ∃-projection preserves it.

theorem Caie2023.universalProjection_anti {P : Type u_1} {W : Type u_2} (F₁ F₂ : FragmentSet P W) (sem : P → W → Prop) (h : ∀ (p : P) (w : W), F₁ p w → F₂ p w) (w : W) : universalProjection F₂ sem w → universalProjection F₁ sem w

∀-projection is Antitone in the fragment set: expanding available parameters can only remove surviving worlds (more to check).

theorem Caie2023.existentialUpdate_restricts {P : Type u_1} {W : Type u_2} (cs : Set W) (F : FragmentSet P W) (sem : P → W → Prop) (w : W) : existentialUpdate cs F sem w → cs w

∃-update only removes worlds from the context set.

theorem Caie2023.universalUpdate_restricts {P : Type u_1} {W : Type u_2} (cs : Set W) (F : FragmentSet P W) (sem : P → W → Prop) (w : W) : universalUpdate cs F sem w → cs w

∀-update only removes worlds from the context set.

theorem Caie2023.fiberwiseFilter_sub {P : Type u_1} {W : Type u_2} (F : FragmentSet P W) (sem : P → W → Prop) (p : P) (w : W) : fiberwiseFilter F sem p w → F p w

Fiberwise filter only removes parameters.

theorem Caie2023.universalUpdate_implies_existentialUpdate {P : Type u_1} {W : Type u_2} (cs : Set W) (F : FragmentSet P W) (sem : P → W → Prop) (w : W) (h_ne : ∃ (p : P), F p w) : universalUpdate cs F sem w → existentialUpdate cs F sem w

∀-update implies ∃-update when the fiber is non-empty. Super-truth implies disjunctive survival.

theorem Caie2023.singleton_projections_agree {P : Type u_1} {W : Type u_2} (p₀ : P) (sem : P → W → Prop) (w : W) : existentialProjection (fun (p : P) (x : W) => p = p₀) sem w ↔ universalProjection (fun (p : P) (x : W) => p = p₀) sem w

When F_w is a singleton {p₀}, both projections agree with a direct check of sem(p₀, w). No parameter uncertainty.

theorem Caie2023.existentialUpdate_singleton {P : Type u_1} {W : Type u_2} (cs : Set W) (p₀ : P) (sem : P → W → Prop) : existentialUpdate cs (fun (p : P) (x : W) => p = p₀) sem = fun (w : W) => cs w ∧ sem p₀ w

Singleton ∃-update reduces to propositional filtering.

structure Caie2023.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 V M in Dynamic/Possibility.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

@[reducible, inline]

abbrev Caie2023.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.

[Cai23]: "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

• Caie2023.InterpAssignment C W = (W → C → Prop)

@[reducible, inline]

abbrev Caie2023.InterpAssignment.toFragmentSet {C : Type u_1} {W : Type u_2} (I : InterpAssignment C W) : 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 § 0 convention (index by parameter first).

Equations

• I.toFragmentSet c w = I w c

def Caie2023.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 ([Sta78], formulated following [Cai23] §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

• Caie2023.standardUpdate cs c_w sem w = (cs w ∧ sem (c_w w) w)

@[reducible, inline]

abbrev Caie2023.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 ([Cai23] §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 (§ 0) with the interpretation assignment as the fragment set (argument order swapped).

[Cai23]: "The result of updating the context given the assertion is C^φ = {w ∈ C_φ : w ∈ ⟦φ⟧^c, for some c ∈ I^φ_w}."

Equations

• Caie2023.disjunctiveUpdate cs I sem = Caie2023.existentialUpdate cs I.toFragmentSet sem

@[reducible, inline]

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

Contextual Pruning ([Cai23] §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 (§ 0, argument order swapped).

[Cai23]: "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

• Caie2023.prune I sem w c = Caie2023.fiberwiseFilter I.toFragmentSet sem c w

def Caie2023.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.

[Cai23]: "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

• Caie2023.fragmentation cs I f = (cs f.world ∧ I f.world f.ctx)

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

Project fragments to their world components.

Equations

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

theorem Caie2023.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 Caie2023.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 Caie2023.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 Caie2023.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 Caie2023.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 = 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 Caie2023.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 ([Cai23] §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.

[Cai23]: "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 Caie2023.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

• Caie2023.discourseStep cs I sem = (Caie2023.disjunctiveUpdate cs I sem, Caie2023.prune I sem)

theorem Caie2023.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 Caie2023.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 [Cai23]'s central mechanism, obtained for free from sequential_existentialUpdate (§ 0).

Sarah's Socks ([Cai23] §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 [Cai23])

For Tim Likes Matching:

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

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

inductive Caie2023.TimPref : Type

Tim's preference: the world parameter.

• likesMatching : TimPref
• likesMixed : TimPref

@[instance_reducible]

instance Caie2023.instDecidableEqTimPref : DecidableEq TimPref

Equations

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

def Caie2023.instReprTimPref.repr : TimPref → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Caie2023.instReprTimPref.repr Caie2023.TimPref.likesMixed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Caie2023.TimPref.likesMixed")).group prec✝

@[instance_reducible]

instance Caie2023.instReprTimPref : Repr TimPref

Equations

• Caie2023.instReprTimPref = { reprPrec := Caie2023.instReprTimPref.repr }

inductive Caie2023.DressInt : Type

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

@[instance_reducible]

instance Caie2023.instDecidableEqDressInt : DecidableEq DressInt

Equations

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

def Caie2023.instReprDressInt.repr : DressInt → ℕ → Std.Format

Equations

• Caie2023.instReprDressInt.repr Caie2023.DressInt.matching prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Caie2023.DressInt.matching")).group prec✝
• Caie2023.instReprDressInt.repr Caie2023.DressInt.mixed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Caie2023.DressInt.mixed")).group prec✝

@[instance_reducible]

instance Caie2023.instReprDressInt : Repr DressInt

Equations

• Caie2023.instReprDressInt = { reprPrec := Caie2023.instReprDressInt.repr }

def Caie2023.SarahsSocks.likes : DressInt → TimPref → Prop

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

Equations

• Caie2023.SarahsSocks.likes Caie2023.DressInt.matching Caie2023.TimPref.likesMatching = True
• Caie2023.SarahsSocks.likes Caie2023.DressInt.mixed Caie2023.TimPref.likesMixed = True
• Caie2023.SarahsSocks.likes x✝¹ x✝ = False

@[instance_reducible]

instance Caie2023.SarahsSocks.instDecidableLikes (c : DressInt) (w : TimPref) : Decidable (likes c w)

Equations

• Caie2023.SarahsSocks.instDecidableLikes Caie2023.DressInt.matching Caie2023.TimPref.likesMatching = isTrue trivial
• Caie2023.SarahsSocks.instDecidableLikes Caie2023.DressInt.matching Caie2023.TimPref.likesMixed = isFalse ⋯
• Caie2023.SarahsSocks.instDecidableLikes Caie2023.DressInt.mixed Caie2023.TimPref.likesMatching = isFalse ⋯
• Caie2023.SarahsSocks.instDecidableLikes Caie2023.DressInt.mixed Caie2023.TimPref.likesMixed = isTrue trivial

def Caie2023.SarahsSocks.dislikes (c : DressInt) (w : TimPref) : Prop

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

Equations

• Caie2023.SarahsSocks.dislikes c w = ¬Caie2023.SarahsSocks.likes c w

@[instance_reducible]

instance Caie2023.SarahsSocks.instDecidableDislikes (c : DressInt) (w : TimPref) : Decidable (dislikes c w)

Equations

• Caie2023.SarahsSocks.instDecidableDislikes c w = Caie2023.SarahsSocks.instDecidableDislikes._aux_1 c w

def Caie2023.SarahsSocks.isMatching : DressInt → TimPref → Prop

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

Equations

• Caie2023.SarahsSocks.isMatching Caie2023.DressInt.matching x✝ = True
• Caie2023.SarahsSocks.isMatching Caie2023.DressInt.mixed x✝ = False

@[instance_reducible]

instance Caie2023.SarahsSocks.instDecidableIsMatching (c : DressInt) (w : TimPref) : Decidable (isMatching c w)

Equations

• Caie2023.SarahsSocks.instDecidableIsMatching Caie2023.DressInt.matching x✝ = isTrue trivial
• Caie2023.SarahsSocks.instDecidableIsMatching Caie2023.DressInt.mixed x✝ = isFalse ⋯

def Caie2023.SarahsSocks.isMixed : DressInt → TimPref → Prop

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

Equations

• Caie2023.SarahsSocks.isMixed Caie2023.DressInt.mixed x✝ = True
• Caie2023.SarahsSocks.isMixed Caie2023.DressInt.matching x✝ = False

@[instance_reducible]

instance Caie2023.SarahsSocks.instDecidableIsMixed (c : DressInt) (w : TimPref) : Decidable (isMixed c w)

Equations

• Caie2023.SarahsSocks.instDecidableIsMixed Caie2023.DressInt.mixed x✝ = isTrue trivial
• Caie2023.SarahsSocks.instDecidableIsMixed Caie2023.DressInt.matching x✝ = isFalse ⋯

def Caie2023.SarahsSocks.timLikesMatchingResult (w : TimPref) : Prop

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.

@[instance_reducible]

instance Caie2023.SarahsSocks.instDecidableTimLikesMatchingResult (w : TimPref) : Decidable (timLikesMatchingResult w)

Equations

• Caie2023.SarahsSocks.instDecidableTimLikesMatchingResult w = Caie2023.SarahsSocks.instDecidableTimLikesMatchingResult._aux_1 w

def Caie2023.SarahsSocks.timDislikesMixedResult (w : TimPref) : Prop

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.

@[instance_reducible]

instance Caie2023.SarahsSocks.instDecidableTimDislikesMixedResult (w : TimPref) : Decidable (timDislikesMixedResult w)

Equations

• Caie2023.SarahsSocks.instDecidableTimDislikesMixedResult w = Caie2023.SarahsSocks.instDecidableTimDislikesMixedResult._aux_1 w

theorem Caie2023.SarahsSocks.tlm_keeps_matching : timLikesMatchingResult TimPref.likesMatching

Tim Likes Matching keeps the matching-preference world.

theorem Caie2023.SarahsSocks.tlm_eliminates_mixed : ¬timLikesMatchingResult TimPref.likesMixed

Tim Likes Matching eliminates the mixed-preference world.

theorem Caie2023.SarahsSocks.tdm_keeps_matching : timDislikesMixedResult TimPref.likesMatching

Tim Dislikes Mixed keeps the matching-preference world.

theorem Caie2023.SarahsSocks.tdm_eliminates_mixed : ¬timDislikesMixedResult TimPref.likesMixed

Tim Dislikes Mixed eliminates the mixed-preference world.

theorem Caie2023.SarahsSocks.discourses_agree (w : TimPref) : timLikesMatchingResult w ↔ timDislikesMixedResult w

Both discourses yield the same result.

def Caie2023.SarahsSocks.facts (w : TimPref) : Prop

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

Equations

• Caie2023.SarahsSocks.facts Caie2023.TimPref.likesMatching = True
• Caie2023.SarahsSocks.facts Caie2023.TimPref.likesMixed = False

@[instance_reducible]

instance Caie2023.SarahsSocks.instDecidableFacts (w : TimPref) : Decidable (facts w)

Equations

• Caie2023.SarahsSocks.instDecidableFacts Caie2023.TimPref.likesMatching = isTrue trivial
• Caie2023.SarahsSocks.instDecidableFacts Caie2023.TimPref.likesMixed = isFalse ⋯

theorem Caie2023.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 Caie2023.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 Caie2023.SarahsSocks.safe_info_i_tdm (w : TimPref) : timDislikesMixedResult w → facts w

Safe Information condition (i) for Tim Dislikes Mixed.

theorem Caie2023.SarahsSocks.safe_info_ii_tdm (w : TimPref) : facts w → timDislikesMixedResult w

Safe Information condition (ii) for Tim Dislikes Mixed.

theorem Caie2023.SarahsSocks.standard_update_incompatible (c : DressInt) (w : TimPref) : ¬(likes c w ∧ dislikes c w)

[Cai23] §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 Caie2023.SarahsSocks.uniform_charity_retains_nonfact : (∃ (c : DressInt), likes c TimPref.likesMixed) ∧ (∃ (c : DressInt), isMatching c TimPref.likesMixed) ∧ ¬facts TimPref.likesMixed

[Cai23] §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 Caie2023.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 Caie2023.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 Caie2023.SarahsSocks.dislikes_eq_not_likes (c : DressInt) (w : TimPref) : dislikes c w ↔ ¬likes c w

Dislikes is the complement of likes.

theorem Caie2023.SarahsSocks.matching_mixed_compl (c : DressInt) (w : TimPref) : isMatching c w ↔ ¬isMixed c w

isMatching and isMixed are complements.