File Change Semantics

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

Heim's File Change Semantics, the pioneering dynamic semantic framework that treats sentence meanings as context change potentials (FCPs) operating on files — structured information states tracking which discourse referents are active.

Heim's File Metaphor (Ch III)

A file F = ⟨Dom(F), Sat(F)⟩ is a pair:

• Dom(F): a set of variable indices — the "file cards" currently open
• Sat(F): a set of ⟨world, assignment⟩ sequences satisfying the file

Sentences denote file change potentials: partial functions from files to files. Partiality is essential — it models presupposition as definedness:

• Novelty: indefinites require their index NOT in Dom(F)
• Familiarity: definites require their index IN Dom(F)

When a precondition fails, the FCP is undefined, not empty.

FCP Rules (@cite{heim-1982}, Ch III §2.1)

Connective	FCP
Atomic P(x₁,...,xₙ)	Filter Sat(F) by the predicate
φ ∧ ψ	(F + φ) + ψ (sequential update)
¬φ	{s ∈ Sat(F) | s ∉ Sat(F + φ)}
if φ then ψ	F + ¬(φ ∧ ¬ψ)
∃x.φ (indefinite)	Extend Dom by x, widen Sat, then update with φ

Design note on atomic domain expansion. @cite{heim-1982}'s rule (i'') specifies that atomic updates expand the domain: Dom(F + φ) = Dom(F) ∪ {i₁,...,iₙ}. We follow the modern convention (shared by DRT and DPL) where domain expansion is handled solely by the indefinite operator (indef), and atomic predicates preserve the domain. This simplifies the algebra without affecting truth conditions, since in practice every variable mentioned in an atomic predicate has already been introduced by an indefinite or a definite.

Truth (@cite{heim-1982}, Ch III §3.2, criterion (C))

φ is true w.r.t. F iff F + φ is defined and Sat(F + φ) is nonempty. This is not idempotency — it is a weaker condition that builds existential quantification into the notion of truth itself.

Relation to Core Infrastructure

This Module	Semantics.Dynamic.Core
HeimFile	Context W E (enriched with dom/sat structure)
FCP (partial)	CCP (total)
novelty guard	InfoState.novelAt
familiarity guard	InfoState.definedAt

structure Semantics.Dynamic.FileChangeSemantics.HeimFile (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A Heim File: ⟨Dom(F), Sat(F)⟩.

Dom(F) is the set of discourse referent indices currently active. Sat(F) is the set of ⟨world, assignment⟩ possibilities satisfying the file's conditions.

This captures formal definition of a file as a structured pair, not merely a flat set of possibilities. The domain tracks which variables carry information — the key structural innovation over bare info states.

• dom : Set ℕ

  Domain: the set of active discourse referent indices.

• sat : Core.InfoState W E

  Satisfaction set: possibilities consistent with the file.

theorem Semantics.Dynamic.FileChangeSemantics.HeimFile.ext_iff {W : Type u_1} {E : Type u_2} {x y : HeimFile W E} : x = y ↔ x.dom = y.dom ∧ x.sat = y.sat

theorem Semantics.Dynamic.FileChangeSemantics.HeimFile.ext {W : Type u_1} {E : Type u_2} {x y : HeimFile W E} (dom : x.dom = y.dom) (sat : x.sat = y.sat) : x = y

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

A File Change Potential: a partial function from files to files.

central semantic type. Partiality (modeled via Option) captures presupposition-as-definedness: when a novelty or familiarity precondition fails, the FCP returns none rather than an empty file.

Equations

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

def Semantics.Dynamic.FileChangeSemantics.HeimFile.empty {W : Type u_1} {E : Type u_2} : HeimFile W E

The empty file: no discourse referents, all possibilities.

Equations

• Semantics.Dynamic.FileChangeSemantics.HeimFile.empty = { dom := ∅, sat := Set.univ }

def Semantics.Dynamic.FileChangeSemantics.HeimFile.absurd {W : Type u_1} {E : Type u_2} (dom : Set ℕ) : HeimFile W E

The absurd file: no possibilities.

Equations

• Semantics.Dynamic.FileChangeSemantics.HeimFile.absurd dom = { dom := dom, sat := ∅ }

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

Variable x is NOVEL in file F iff x ∉ Dom(F).

Novelty Condition: an indefinite NP with index x is felicitous only if x has not yet been used.

Equations

• F.novel x = ¬x ∈ F.dom

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

Variable x is FAMILIAR in file F iff x ∈ Dom(F).

Familiarity Condition: a definite NP with index x is felicitous only if x is already in the domain.

Equations

• F.familiar x = (x ∈ F.dom)

def Semantics.Dynamic.FileChangeSemantics.HeimFile.consistent {W : Type u_1} {E : Type u_2} (F : HeimFile W E) : Prop

A file is consistent (non-absurd) iff its satisfaction set is non-empty.

File truth in (Ch III §1.2): "F is true iff there is at least one sequence a_N such that a_N ∈ Sat(F)."

Equations

• F.consistent = Set.Nonempty F.sat

def Semantics.Dynamic.FileChangeSemantics.HeimFile.refersTo {W : Type u_1} {E : Type u_2} (F : HeimFile W E) (i : ℕ) (x : E) : Prop

Card i in F refers to entity x iff every satisfying sequence assigns x to position i.

(Ch III §2.3, p. 207): "Card i in F refers to x iff, for all a_N ∈ Sat(F), a_i = x."

Equations

• F.refersTo i x = ∀ (p : Semantics.Dynamic.Core.Possibility W E), p ∈ F.sat → p.assignment i = x

def Semantics.Dynamic.FileChangeSemantics.HeimFile.toInfoState {W : Type u_1} {E : Type u_2} (F : HeimFile W E) : Core.InfoState W E

Project to the underlying InfoState.

Equations

• F.toInfoState = F.sat

def Semantics.Dynamic.FileChangeSemantics.HeimFile.ofContext {W : Type u_1} {E : Type u_2} (c : Core.Context W E) : HeimFile W E

Build a HeimFile from a Context.

Equations

• Semantics.Dynamic.FileChangeSemantics.HeimFile.ofContext c = { dom := c.definedVars, sat := c.state }

theorem Semantics.Dynamic.FileChangeSemantics.HeimFile.novel_iff_not_familiar {W : Type u_1} {E : Type u_2} (F : HeimFile W E) (x : ℕ) : F.novel x ↔ ¬F.familiar x

Novelty and familiarity are complementary.

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

Atomic predicate update: filter satisfaction set by predicate.

F + [P(x₁,...,xₙ)] = ⟨Dom(F), {s ∈ Sat(F) | P holds of s}⟩

Domain is unchanged; only the satisfaction set shrinks.

Note: rule (i'') on p. 198 specifies that atomic updates also expand the domain: Dom(F + φ) = Dom(F) ∪ {i₁,...,iₙ}. We follow the modern convention where domain expansion is handled by indef only. This is equivalent in practice because every variable in an atomic predicate has been previously introduced.

Equations

• Semantics.Dynamic.FileChangeSemantics.FCP.atom pred F = some { dom := F.dom, sat := {p : Semantics.Dynamic.Core.Possibility W E | p ∈ F.sat ∧ pred p} }

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

Atomic predicate on world only.

Equations

• Semantics.Dynamic.FileChangeSemantics.FCP.atomW pred = Semantics.Dynamic.FileChangeSemantics.FCP.atom fun (p : Semantics.Dynamic.Core.Possibility W E) => pred p.world

def Semantics.Dynamic.FileChangeSemantics.FCP.atomVar {W : Type u_1} {E : Type u_2} (pred : E → Prop) (x : ℕ) : FCP W E

Atomic predicate on assignment at variable x.

Equations

• Semantics.Dynamic.FileChangeSemantics.FCP.atomVar pred x = Semantics.Dynamic.FileChangeSemantics.FCP.atom fun (p : Semantics.Dynamic.Core.Possibility W E) => pred (p.assignment x)

def Semantics.Dynamic.FileChangeSemantics.FCP.atomVar2 {W : Type u_1} {E : Type u_2} (pred : E → E → Prop) (x y : ℕ) : FCP W E

Binary predicate on two variables.

Equations

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

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

Sequential composition (conjunction): F + [φ ∧ ψ] = (F + φ) + ψ.

successive file change. If either step is undefined (presupposition failure), the whole is undefined.

Equations

• (φ +> ψ) F = (φ F).bind ψ

def Semantics.Dynamic.FileChangeSemantics.FCP.«term_+>_» : Lean.TrailingParserDescr

Equations

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

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

Negation: F + [¬φ] = ⟨Dom(F), {s ∈ Sat(F) | s ∉ Sat(F + φ)}⟩.

per-element negation: keep assignments from Sat(F) that do NOT survive the update with φ. The domain is preserved — negation is a test that doesn't introduce new drefs.

If φ is undefined on F (presupposition failure in the scope of negation), the negation is also undefined.

Equations

• φ.neg F = match φ F with | none => none | some F' => some { dom := F.dom, sat := {p : Semantics.Dynamic.Core.Possibility W E | p ∈ F.sat ∧ ¬p ∈ F'.sat} }

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

Conditional: F + [if φ then ψ] = F + [¬(φ ∧ ¬ψ)].

analysis of conditionals as negated conjunctions of the antecedent with the negated consequent.

Equations

• φ.cond ψ = (φ +> ψ.neg).neg

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

Indefinite introduction: F + [∃x.φ].

Defined only if x is NOVEL in F (the Novelty Condition). When defined:

1. Extend Dom(F) by x
2. Widen Sat(F) to all re-assignments of x (random assignment)
3. Update with the body φ

This is Heim's key innovation: indefinites don't quantify, they change the file structure by opening a new file card.

Equations

• Semantics.Dynamic.FileChangeSemantics.FCP.indef x body F = if F.novel x then have F' := { dom := F.dom ∪ {x}, sat := F.sat.randomAssignFull x }; body F' else none

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

Definite reference: F + [the x. φ].

Defined only if x is FAMILIAR in F (the Familiarity Condition). When defined, updates with the body φ without changing the domain structure — the dref is already established.

familiarity theory of definiteness.

Equations

• Semantics.Dynamic.FileChangeSemantics.FCP.def_ x body F = if F.familiar x then body F else none

def Semantics.Dynamic.FileChangeSemantics.FCP.id {W : Type u_1} {E : Type u_2} : FCP W E

Identity FCP: no change.

Equations

• Semantics.Dynamic.FileChangeSemantics.FCP.id F = some F

def Semantics.Dynamic.FileChangeSemantics.FCP.fail {W : Type u_1} {E : Type u_2} : FCP W E

Absurd FCP: always undefined (total presupposition failure).

Equations

• Semantics.Dynamic.FileChangeSemantics.FCP.fail x✝ = none

def Semantics.Dynamic.FileChangeSemantics.trueIn {W : Type u_1} {E : Type u_2} (F : HeimFile W E) (φ : FCP W E) : Prop

φ is true w.r.t. F iff F + φ is defined and the result is a consistent (true) file.

This is truth criterion (C) (Ch III §3.2, p. 214): "A formula φ is true w.r.t. a file F if F + φ is true" — where a file is true iff Sat(F) ≠ ∅. Existential quantification is built into the notion of truth itself: indefinites need not be explicitly bound by ∃.

Equations

• Semantics.Dynamic.FileChangeSemantics.trueIn F φ = ∃ (F' : Semantics.Dynamic.FileChangeSemantics.HeimFile W E), φ F = some F' ∧ F'.consistent

def Semantics.Dynamic.FileChangeSemantics.falseIn {W : Type u_1} {E : Type u_2} (F : HeimFile W E) (φ : FCP W E) : Prop

φ is false w.r.t. F iff F + φ is defined but the result is an inconsistent (absurd) file.

criterion (C): "false w.r.t. F if F + φ is false."

Equations

• Semantics.Dynamic.FileChangeSemantics.falseIn F φ = ∃ (F' : Semantics.Dynamic.FileChangeSemantics.HeimFile W E), φ F = some F' ∧ ¬F'.consistent

def Semantics.Dynamic.FileChangeSemantics.supports {W : Type u_1} {E : Type u_2} (F : HeimFile W E) (φ : FCP W E) : Prop

F supports φ iff F + φ = F (idempotency of update).

This is the dynamic notion of entailment/support: F already "knows" φ iff updating with φ changes nothing. This is stronger than truth — support implies truth (when F is consistent) but not vice versa.

Note: this is sometimes called "truth as idempotency" in the update semantics literature (@cite{veltman-1996}), but it is NOT truth definition, which is the weaker trueIn.

Equations

• Semantics.Dynamic.FileChangeSemantics.supports F φ = (φ F = some F)

def Semantics.Dynamic.FileChangeSemantics.fileEntails {W : Type u_1} {E : Type u_2} (F : HeimFile W E) (φ : FCP W E) : Prop

F entails φ iff F supports φ (F + φ = F).

Equations

• Semantics.Dynamic.FileChangeSemantics.fileEntails F φ = Semantics.Dynamic.FileChangeSemantics.supports F φ

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

φ semantically entails ψ iff for all files F, if F + φ is defined then F + φ supports ψ.

Equations

• Semantics.Dynamic.FileChangeSemantics.fcpEntails φ ψ = ∀ (F F' : Semantics.Dynamic.FileChangeSemantics.HeimFile W E), φ F = some F' → Semantics.Dynamic.FileChangeSemantics.supports F' ψ

def Semantics.Dynamic.FileChangeSemantics.definedOn {W : Type u_1} {E : Type u_2} (F : HeimFile W E) (φ : FCP W E) : Prop

φ is defined on F (the update doesn't trigger presupposition failure).

Equations

• Semantics.Dynamic.FileChangeSemantics.definedOn F φ = ∃ (F' : Semantics.Dynamic.FileChangeSemantics.HeimFile W E), φ F = some F'

theorem Semantics.Dynamic.FileChangeSemantics.trueIn_definedOn {W : Type u_1} {E : Type u_2} (F : HeimFile W E) (φ : FCP W E) (h : trueIn F φ) : definedOn F φ

Truth implies definedness.

theorem Semantics.Dynamic.FileChangeSemantics.supports_trueIn {W : Type u_1} {E : Type u_2} (F : HeimFile W E) (φ : FCP W E) (hsup : supports F φ) (hcons : F.consistent) : trueIn F φ

Support implies truth for consistent files.

theorem Semantics.Dynamic.FileChangeSemantics.seq_assoc {W : Type u_1} {E : Type u_2} (φ ψ χ : FCP W E) : φ +> ψ +> χ = φ +> (ψ +> χ)

Sequential composition is associative.

theorem Semantics.Dynamic.FileChangeSemantics.id_seq {W : Type u_1} {E : Type u_2} (φ : FCP W E) : FCP.id +> φ = φ

Identity is left unit for sequential composition.

theorem Semantics.Dynamic.FileChangeSemantics.seq_id {W : Type u_1} {E : Type u_2} (φ : FCP W E) : φ +> FCP.id = φ

Identity is right unit for sequential composition.

theorem Semantics.Dynamic.FileChangeSemantics.atom_preserves_dom {W : Type u_1} {E : Type u_2} (pred : Core.Possibility W E → Prop) (F : HeimFile W E) : Option.map (fun (x : HeimFile W E) => x.dom) (FCP.atom pred F) = some F.dom

Atomic updates preserve the domain.

theorem Semantics.Dynamic.FileChangeSemantics.neg_preserves_dom {W : Type u_1} {E : Type u_2} (φ : FCP W E) (F F' : HeimFile W E) (h : φ.neg F = some F') : F'.dom = F.dom

Negation preserves the domain.

theorem Semantics.Dynamic.FileChangeSemantics.indef_familiar_none {W : Type u_1} {E : Type u_2} (x : ℕ) (body : FCP W E) (F : HeimFile W E) (h : F.familiar x) : FCP.indef x body F = none

Indefinite is undefined when variable is familiar (not novel).

theorem Semantics.Dynamic.FileChangeSemantics.def_novel_none {W : Type u_1} {E : Type u_2} (x : ℕ) (body : FCP W E) (F : HeimFile W E) (h : F.novel x) : FCP.def_ x body F = none

Definite is undefined when variable is novel (not familiar).

theorem Semantics.Dynamic.FileChangeSemantics.indef_intermediate_has_x {W : Type u_1} {E : Type u_2} (x : ℕ) (F : HeimFile W E) : x ∈ { dom := F.dom ∪ {x}, sat := F.sat.randomAssignFull x }.dom

The intermediate file passed to the body of an indefinite has x in its domain.

theorem Semantics.Dynamic.FileChangeSemantics.cond_eq {W : Type u_1} {E : Type u_2} (φ ψ : FCP W E) : φ.cond ψ = (φ +> ψ.neg).neg

Conditional is definable from negation and conjunction.

theorem Semantics.Dynamic.FileChangeSemantics.atom_eliminative {W : Type u_1} {E : Type u_2} (pred : Core.Possibility W E → Prop) (F F' : HeimFile W E) (h : FCP.atom pred F = some F') : F'.sat ⊆ F.sat

Atomic update is eliminative: Sat(F + P) ⊆ Sat(F).

This is Principle (A): information only grows (possibilities only decrease).

theorem Semantics.Dynamic.FileChangeSemantics.neg_eliminative {W : Type u_1} {E : Type u_2} (φ : FCP W E) (F F' : HeimFile W E) (h : φ.neg F = some F') : F'.sat ⊆ F.sat

Negation is eliminative: Sat(F + ¬φ) ⊆ Sat(F).

theorem Semantics.Dynamic.FileChangeSemantics.seq_eliminative {W : Type u_1} {E : Type u_2} (φ ψ : FCP W E) (hφ : ∀ (F F' : HeimFile W E), φ F = some F' → F'.sat ⊆ F.sat) (hψ : ∀ (F F' : HeimFile W E), ψ F = some F' → F'.sat ⊆ F.sat) (F F' : HeimFile W E) (h : (φ +> ψ) F = some F') : F'.sat ⊆ F.sat

Sequential composition of eliminative FCPs is eliminative.

theorem Semantics.Dynamic.FileChangeSemantics.def_preserves_dom {W : Type u_1} {E : Type u_2} (x : ℕ) (body : FCP W E) (hbody : ∀ (G G' : HeimFile W E), body G = some G' → G'.dom = G.dom) (F F' : HeimFile W E) (h : FCP.def_ x body F = some F') : F'.dom = F.dom

Domain monotonicity for definite updates: when the body preserves the domain, so does the definite FCP.

theorem Semantics.Dynamic.FileChangeSemantics.supports_idempotent {W : Type u_1} {E : Type u_2} (F : HeimFile W E) (φ : FCP W E) (h : supports F φ) : (φ +> φ) F = φ F

Support is idempotent: if F supports φ, then updating twice is the same as once.

def Semantics.Dynamic.FileChangeSemantics.liftCCP {W : Type u_1} {E : Type u_2} (u : Core.CCP (Core.Possibility W E)) : FCP W E

Lift a total CCP to a (total) FCP that preserves domain.

Equations

• Semantics.Dynamic.FileChangeSemantics.liftCCP u F = some { dom := F.dom, sat := u F.sat }

theorem Semantics.Dynamic.FileChangeSemantics.liftCCP_seq {W : Type u_1} {E : Type u_2} (u v : Core.CCP (Core.Possibility W E)) : liftCCP (u.seq v) = liftCCP u +> liftCCP v

Lift preserves sequential composition.

theorem Semantics.Dynamic.FileChangeSemantics.liftCCP_definedOn {W : Type u_1} {E : Type u_2} (u : Core.CCP (Core.Possibility W E)) (F : HeimFile W E) : definedOn F (liftCCP u)

Lifted CCPs are always defined (total).

def Semantics.Dynamic.FileChangeSemantics.resultSat {W : Type u_1} {E : Type u_2} (φ : FCP W E) (F : HeimFile W E) : Option (Core.InfoState W E)

Extract the satisfaction set from the result of an FCP.

Equations

• Semantics.Dynamic.FileChangeSemantics.resultSat φ F = Option.map (fun (x : Semantics.Dynamic.FileChangeSemantics.HeimFile W E) => x.sat) (φ F)

def Semantics.Dynamic.FileChangeSemantics.liftDRS {W : Type u_1} {E : Type u_2} (R : Core.DynProp.DRS (Core.Possibility W E)) : FCP W E

Lift a DRS (relational meaning) to an FCP via the relational image.

This connects FCPs to the relational algebra in Core.DynProp. The resulting FCP preserves domain and is always defined (total).

Equations

• Semantics.Dynamic.FileChangeSemantics.liftDRS R = Semantics.Dynamic.FileChangeSemantics.liftCCP (Semantics.Dynamic.Core.lift R)

theorem Semantics.Dynamic.FileChangeSemantics.liftDRS_seq {W : Type u_1} {E : Type u_2} (R₁ R₂ : Core.DynProp.DRS (Core.Possibility W E)) : liftDRS (R₁ ⨟ R₂) = liftDRS R₁ +> liftDRS R₂

liftDRS preserves sequential composition: lifting a relational sequence equals sequencing lifted FCPs.

This shows the FCS algebra homomorphically embeds the DynProp algebra — the unification underlying @cite{muskens-1996}.

theorem Semantics.Dynamic.FileChangeSemantics.atom_eq_liftDRS_test {W : Type u_1} {E : Type u_2} (pred : Core.Possibility W E → Prop) : FCP.atom pred = liftDRS [pred]

Atomic FCP equals lifting a test from DynProp.

FCS's atom pred = lifting DynProp.test (λ p => pred p). This shows atomic FCPs are exactly the relational tests, connecting Principle (A) to the DynProp algebra.