State Effect: Assignment Threading

@cite{heim-1982} @cite{heim-1983} @cite{veltman-1996}

The state effect underlies anaphora resolution in dynamic semantics. It threads variable assignments through interpretation, allowing one sentence to bind variables that later sentences can access.

This module collects state-based semantic frameworks:

• File Change Semantics: meanings as context change potentials over files (sets of world-assignment pairs)
• Update Semantics: propositional update with epistemic modals

Both are instances of the state effect: they differ in whether the state tracks assignments (FCS) or just worlds (Update Semantics).

File Change Semantics

Heim's File Metaphor:

• The context is a "file" of information about discourse referents
• Each "file card" is a possibility: (world, assignment) pair
• Sentences update the file by adding/removing cards
• Indefinites "open" new file cards

⟦φ⟧ : File → File (sentences are context change potentials)

@[reducible, inline]

abbrev Semantics.Dynamic.FileChangeSemantics.File (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

A File is an information state: set of (world, assignment) pairs.

This is Heim's "file metaphor" - each pair is a "file card".

Equations

• Semantics.Dynamic.FileChangeSemantics.File W E = Semantics.Dynamic.Core.InfoState W E

@[reducible, inline]

abbrev Semantics.Dynamic.FileChangeSemantics.FileCard (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A File Card is a single possibility: (world, assignment).

Equations

• Semantics.Dynamic.FileChangeSemantics.FileCard W E = Semantics.Dynamic.Core.Possibility W E

def Semantics.Dynamic.FileChangeSemantics.File.novel {W : Type u_1} {E : Type u_2} (f : File W E) (x : ℕ) : Prop

Variable x is NOVEL in file f iff f doesn't constrain x.

Indefinites require their variable to be novel - this prevents the same variable being reused inappropriately.

Equations

• f.novel x = Semantics.Dynamic.Core.InfoState.novelAt f x

def Semantics.Dynamic.FileChangeSemantics.File.familiar {W : Type u_1} {E : Type u_2} (f : File W E) (x : ℕ) : Prop

Variable x is FAMILIAR in file f iff f constrains x uniquely.

Definites require their variable to be familiar - the discourse must have already established who "the X" refers to.

Equations

• f.familiar x = Semantics.Dynamic.Core.InfoState.definedAt f x

def Semantics.Dynamic.FileChangeSemantics.File.updateProp {W : Type u_1} {E : Type u_2} (f : File W E) (φ : W → Bool) : File W E

Update file with proposition: eliminate cards where φ fails.

f[φ] = { c ∈ f | φ(c.world) }

Equations

• f.updateProp φ = f⟦φ⟧

def Semantics.Dynamic.FileChangeSemantics.File.introduce {W : Type u_1} {E : Type u_2} (f : File W E) (x : ℕ) (dom : Set E) : File W E

Introduce new discourse referent (indefinite).

f[x:=?] adds cards for each possible entity value of x. Requires x to be NOVEL (precondition).

Equations

• f.introduce x dom = Semantics.Dynamic.Core.InfoState.randomAssign f x dom

@[reducible, inline]

abbrev Semantics.Dynamic.FileChangeSemantics.FCP (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

File Change Potential (FCP): the semantic type for sentences in FCS.

Equations

• Semantics.Dynamic.FileChangeSemantics.FCP W E = (Semantics.Dynamic.FileChangeSemantics.File W E → Semantics.Dynamic.FileChangeSemantics.File W E)

def Semantics.Dynamic.FileChangeSemantics.FCP.atom {W : Type u_1} {E : Type u_2} (pred : W → Bool) : FCP W E

Atomic predicate update.

Equations

• Semantics.Dynamic.FileChangeSemantics.FCP.atom pred f = f.updateProp pred

def Semantics.Dynamic.FileChangeSemantics.FCP.indefinite {W : Type u_1} {E : Type u_2} (x : ℕ) (dom : Set E) (body : FCP W E) : FCP W E

Indefinite introduction: requires novelty.

This models "a man" - introduces a new discourse referent.

Equations

• Semantics.Dynamic.FileChangeSemantics.FCP.indefinite x dom body f = body (f.introduce x dom)

def Semantics.Dynamic.FileChangeSemantics.FCP.definite {W : Type u_1} {E : Type u_2} (x : ℕ) (body : FCP W E) : FCP W E

Definite reference: requires familiarity.

This models "the man" - presupposes the referent is established.

Equations

• Semantics.Dynamic.FileChangeSemantics.FCP.definite x body f = if f.familiar x then body f else ∅

def Semantics.Dynamic.FileChangeSemantics.FCP.conj {W : Type u_1} {E : Type u_2} (φ ψ : FCP W E) : FCP W E

Conjunction: sequential file update.

f[φ ∧ ψ] = f[φ][ψ]

Delegates to Core.CCP.seq.

Equations

• φ.conj ψ = φ ;; ψ

noncomputable def Semantics.Dynamic.FileChangeSemantics.FCP.neg {W : Type u_1} {E : Type u_2} (φ : FCP W E) : FCP W E

Negation: test-based (standard FCS).

f[¬φ] = f if f[φ] = ∅, else ∅

Note: This does NOT validate DNE. Delegates to Core.CCP.neg.

Equations

• φ.neg = Semantics.Dynamic.Core.CCP.neg φ

def Semantics.Dynamic.FileChangeSemantics.requiresNovelty {W : Type u_1} {E : Type u_2} (f : File W E) (x : ℕ) : Prop

Novelty precondition for indefinites.

Attempting to introduce a non-novel variable is undefined behavior (typically modeled as returning ∅ or crash).

Equations

• Semantics.Dynamic.FileChangeSemantics.requiresNovelty f x = f.novel x

def Semantics.Dynamic.FileChangeSemantics.requiresFamiliarity {W : Type u_1} {E : Type u_2} (f : File W E) (x : ℕ) : Prop

Familiarity precondition for definites.

Equations

• Semantics.Dynamic.FileChangeSemantics.requiresFamiliarity f x = f.familiar x

Relation to Semantics.Dynamic.Core.Basic

The Semantics.Dynamic.Core.Basic module provides the canonical infrastructure. This module provides FCS-specific vocabulary as aliases:

This Module	Semantics.Dynamic.Core
File	InfoState
FileCard	Possibility
novel	novelAt
familiar	definedAt
introduce	randomAssign
updateProp	update

Update Semantics

In Update Semantics:

• Information states are sets of worlds (not assignments)
• Sentences update states by eliminating incompatible worlds
• "Might φ" is a TEST: passes if some φ-worlds remain
• No discourse referents (simpler than DRT/DPL)

⟦φ⟧ : State → State where State = Set World

@[reducible, inline]

abbrev Semantics.Dynamic.UpdateSemantics.State (W : Type u_1) : Type u_1

Update Semantics state: a set of possible worlds.

Unlike DPL/DRT, no assignment component - US focuses on propositional content.

Equations

• Semantics.Dynamic.UpdateSemantics.State W = Set W

def Semantics.Dynamic.UpdateSemantics.Update (W : Type u_1) : Type u_1

Update function: how a sentence modifies a state.

Equations

• Semantics.Dynamic.UpdateSemantics.Update W = (Semantics.Dynamic.UpdateSemantics.State W → Semantics.Dynamic.UpdateSemantics.State W)

def Semantics.Dynamic.UpdateSemantics.Update.prop {W : Type u_1} (φ : W → Bool) : Update W

Propositional update: eliminate worlds where φ fails.

⟦φ⟧(s) = { w ∈ s | φ(w) }

Equations

• Semantics.Dynamic.UpdateSemantics.Update.prop φ s = {w : W | w ∈ s ∧ φ w = true}

def Semantics.Dynamic.UpdateSemantics.Update.conj {W : Type u_1} (φ ψ : Update W) : Update W

Conjunction: sequential update.

⟦φ ∧ ψ⟧ = ⟦ψ⟧ ∘ ⟦φ⟧

Delegates to Core.CCP.seq.

Equations

• φ.conj ψ = φ ;; ψ

noncomputable def Semantics.Dynamic.UpdateSemantics.Update.neg {W : Type u_1} (φ : Update W) : Update W

Negation: test and possibly fail.

⟦¬φ⟧(s) = s if ⟦φ⟧(s) = ∅, else ∅

Delegates to Core.CCP.neg.

Equations

• φ.neg = Semantics.Dynamic.Core.CCP.neg φ

noncomputable def Semantics.Dynamic.UpdateSemantics.Update.might {W : Type u_1} (φ : Update W) : Update W

Epistemic "might": compatibility test.

⟦might φ⟧(s) = s if ⟦φ⟧(s) ≠ ∅, else ∅

Delegates to Core.CCP.might.

Equations

• φ.might = Semantics.Dynamic.Core.CCP.might φ

noncomputable def Semantics.Dynamic.UpdateSemantics.Update.must {W : Type u_1} (φ : Update W) : Update W

Epistemic "must": universal test.

⟦must φ⟧(s) = s if ⟦φ⟧(s) = s, else ∅

Delegates to Core.CCP.must.

Equations

• φ.must = Semantics.Dynamic.Core.CCP.must φ

theorem Semantics.Dynamic.UpdateSemantics.might_is_test {W : Type u_1} (φ : Update W) (s : State W) (h : Set.Nonempty (φ s)) : φ.might s = s

Might is a TEST: it doesn't change the state (if it passes).

theorem Semantics.Dynamic.UpdateSemantics.might_order_matters {W : Type u_1} [Nontrivial W] : ∃ (p : W → Bool), ∃ (s : State W), (Update.prop p).conj (Update.prop fun (w : W) => !p w).might s = ∅ ∧ Set.Nonempty ((Update.prop fun (w : W) => !p w).might.conj (Update.prop p) s)

Order matters for epistemic might.

"It's raining and it might not be raining" is contradictory: after learning rain, the might-not-rain test fails (no ¬rain worlds remain). But "it might not be raining and it's raining" can succeed: the might test passes on the initial state, then learning eliminates ¬rain worlds.

Requires Nontrivial W: for empty or singleton W, no state has both p-worlds and ¬p-worlds, making the second conjunct unsatisfiable.

def Semantics.Dynamic.UpdateSemantics.supports {W : Type u_1} (s : State W) (φ : Update W) : Prop

State s supports φ iff updating with φ doesn't change s.

s ⊨ φ iff ⟦φ⟧(s) = s

Equations

• Semantics.Dynamic.UpdateSemantics.supports s φ = (φ s = s)

def Semantics.Dynamic.UpdateSemantics.accepts {W : Type u_1} (s : State W) (φ : Update W) : Prop

State s accepts φ iff updating with φ yields a non-empty state.

s accepts φ iff ⟦φ⟧(s) ≠ ∅

Equations

• Semantics.Dynamic.UpdateSemantics.accepts s φ = Set.Nonempty (φ s)