Heim (1982): File Change Semantics and Anaphora

[Hei82]

Formal analysis of cross-sentential anaphora using [Hei82]'s File Change Semantics. This study file connects the FCS theory (Semantics/Dynamic/FileChange.lean) to the example rows in Data/Examples/Heim1982.json (Heim1982.Examples).

Key Claims Formalized

1. Indefinites introduce discourse referents (new file cards): "A man walked in" opens a new dref that persists across sentences.

2. Negation blocks dref export: "John didn't see a bird" confines the bird's dref to the scope of negation — it doesn't persist.

3. Conjunction is sequential update: "A man walked in. He sat down." = F + [∃x. man(x) ∧ walkedIn(x)] + [satDown(x)].

4. Novelty-Familiarity Condition: indefinites require novel indices; definites require familiar ones. Violations are presupposition failure (undefinedness), not falsehood.

5. Truth criterion (C): φ is true w.r.t. F iff Sat(F + φ) is nonempty ([Hei82], Ch III §3.2). This builds existential quantification into the notion of truth — see FCP.trueIn, FCP.supports_trueIn, FCP.supports_idempotent, and the eliminativity family (Principle (A)) in Semantics/Dynamic/FileChange.lean.

Connection to Empirical Data

Each section below derives FCS predictions that account for specific example rows in Heim1982.Examples.

We work with a simple model: W = possible worlds, E = entities. Predicates are modeled as functions on possibilities. Heim's file cards are numbered, so referents are ℕ.

"A man walked in. He sat down."

This accounts for Examples.indefinite_persists. The FCS analysis: the indefinite "a man" introduces dref x₁ into Dom(F). The pronoun "he" in the second sentence accesses x₁, which persists because no operator (negation, quantifier) has closed x₁'s scope.

The discourse is modeled as: F + [∃x₁. man(x₁) ∧ walkedIn(x₁)] + [satDown(x₁)] where ∃x₁ extends Dom(F) to include x₁.

def Heim1982.aManWalkedIn {W : Type u_1} {E : Type u_2} (man walkedIn : E → Prop) (x : ℕ) : DynamicSemantics.FCP W ℕ E

The indefinite "a man walked in" as an FCP: ∃x. man(x) ∧ walkedIn(x).

Equations

• Heim1982.aManWalkedIn man walkedIn x = DynamicSemantics.FCP.indef x (DynamicSemantics.CCP.Partial.seq (DynamicSemantics.FCP.atomVar man x) (DynamicSemantics.FCP.atomVar walkedIn x))

def Heim1982.heSatDown {W : Type u_1} {E : Type u_2} (satDown : E → Prop) (x : ℕ) : DynamicSemantics.FCP W ℕ E

"He sat down" as an FCP: satDown(x).

Equations

• Heim1982.heSatDown satDown x = DynamicSemantics.FCP.atomVar satDown x

def Heim1982.indefinitePersistsDiscourse {W : Type u_1} {E : Type u_2} (man walkedIn satDown : E → Prop) (x : ℕ) : DynamicSemantics.FCP W ℕ E

The full discourse "A man walked in. He sat down."

Equations

• Heim1982.indefinitePersistsDiscourse man walkedIn satDown x = DynamicSemantics.CCP.Partial.seq (Heim1982.aManWalkedIn man walkedIn x) (Heim1982.heSatDown satDown x)

theorem Heim1982.indef_defined_when_novel {W : Type u_1} {E : Type u_2} (x : ℕ) (F : DynamicSemantics.State W ℕ E) (hnovel : ∀ p ∈ F, ¬(p.assignment x).Dom) (body : DynamicSemantics.FCP W ℕ E) (hbody : (body (F.randomAssign x)).Dom) : DynamicSemantics.CCP.Partial.admits (DynamicSemantics.FCP.indef x body) F

When x is novel, the indefinite FCP is defined (not a presupposition failure) — provided the body is defined on the randomly assigned file.

theorem Heim1982.indef_adds_to_dom {W : Type u_1} {E : Type u_2} (x : ℕ) (body : DynamicSemantics.FCP W ℕ E) (F : DynamicSemantics.State W ℕ E) {F' : DynamicSemantics.State W ℕ E} (hres : F' ∈ DynamicSemantics.FCP.indef x body F) (hbody : ∀ (G : DynamicSemantics.State W ℕ E), G.Familiar x → ∀ G' ∈ body G, DynamicSemantics.State.Familiar G' x) : F'.Familiar x

After the indefinite, x is familiar — provided the body preserves familiarity.

This is the formal content of "indefinites introduce discourse referents" — the defining claim of [Hei82].

"John didn't see a bird. *It was singing."

This accounts for Examples.standard_negation_blocks. The FCS analysis: negation closes the scope of the indefinite's dref. After F + [¬(∃x. bird(x) ∧ saw(j,x))], x is NOT familiar — negation keeps points of the input file, where x was never assigned.

theorem Heim1982.neg_blocks_dref {W : Type u_1} {E : Type u_2} (x : ℕ) (φ : DynamicSemantics.FCP W ℕ E) {F F' : DynamicSemantics.State W ℕ E} (hnovel : ∀ p ∈ F, ¬(p.assignment x).Dom) (h : F' ∈ φ.neg F) (p : DynamicSemantics.Possibility W ℕ (Part E)) : p ∈ F' → ¬(p.assignment x).Dom

A variable introduced inside negation stays novel in the output.

Negation is eliminative over the input file (FCP.neg_eliminative), so a novel variable stays novel after negation — the dref is trapped inside the scope of ¬.

The Novelty-Familiarity Condition is [Hei82]'s formalization of the indefinite/definite contrast (Ch III §2.2, p. 202):

• Indefinites REQUIRE novelty (x ∉ Dom(F))
• Definites REQUIRE familiarity (x ∈ Dom(F))

Violations cause undefinedness (presupposition failure), not falsehood. This is modeled by FCPs being Part-undefined.

theorem Heim1982.novelty_violation {W : Type u_1} {E : Type u_2} (x : ℕ) (body : DynamicSemantics.FCP W ℕ E) (F : DynamicSemantics.State W ℕ E) (hne : Set.Nonempty F) (h : F.Familiar x) : ¬DynamicSemantics.CCP.Partial.admits (DynamicSemantics.FCP.indef x body) F

An indefinite with a familiar index causes presupposition failure.

This accounts for why "*A man₁ walked in. A man₁ sat down." is infelicitous when the second indefinite reuses index 1.

theorem Heim1982.familiarity_violation {W : Type u_1} {E : Type u_2} (x : ℕ) (body : DynamicSemantics.FCP W ℕ E) (F : DynamicSemantics.State W ℕ E) (h : ¬F.Familiar x) : ¬DynamicSemantics.CCP.Partial.admits (DynamicSemantics.FCP.def_ x body) F

A definite with a novel index causes presupposition failure.

This accounts for why "#He₁ sat down." is infelicitous at the start of a discourse (when no index 1 dref has been established).

theorem Heim1982.def_familiar {W : Type u_1} {E : Type u_2} (x : ℕ) (body : DynamicSemantics.FCP W ℕ E) (F : DynamicSemantics.State W ℕ E) (hfam : F.Familiar x) : DynamicSemantics.FCP.def_ x body F = body F

On a file where x is familiar, the definite applies transparently.

With indef_adds_to_dom, this derives "A man₁ walked in. He₁ sat down.": the indefinite makes index 1 familiar, so the definite "he₁" is no presupposition failure.

We instantiate the FCS framework with a concrete finite model to verify the theory matches the empirical data in Heim1982.Examples.

inductive Heim1982.ExWorld : Type

A simple model world type.

• w₀ : ExWorld

@[instance_reducible]

instance Heim1982.instDecidableEqExWorld : DecidableEq ExWorld

Equations

• Heim1982.instDecidableEqExWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Heim1982.instReprExWorld : Repr ExWorld

Equations

• Heim1982.instReprExWorld = { reprPrec := Heim1982.instReprExWorld.repr }

def Heim1982.instReprExWorld.repr : ExWorld → ℕ → Std.Format

Equations

• Heim1982.instReprExWorld.repr Heim1982.ExWorld.w₀ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heim1982.ExWorld.w₀")).group prec✝

inductive Heim1982.ExEntity : Type

A simple entity type.

• john : ExEntity
• mary : ExEntity
• bird₁ : ExEntity

@[instance_reducible]

instance Heim1982.instDecidableEqExEntity : DecidableEq ExEntity

Equations

• Heim1982.instDecidableEqExEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Heim1982.instReprExEntity : Repr ExEntity

Equations

• Heim1982.instReprExEntity = { reprPrec := Heim1982.instReprExEntity.repr }

def Heim1982.instReprExEntity.repr : ExEntity → ℕ → Std.Format

Equations

• Heim1982.instReprExEntity.repr Heim1982.ExEntity.john prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heim1982.ExEntity.john")).group prec✝
• Heim1982.instReprExEntity.repr Heim1982.ExEntity.mary prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heim1982.ExEntity.mary")).group prec✝
• Heim1982.instReprExEntity.repr Heim1982.ExEntity.bird₁ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heim1982.ExEntity.bird₁")).group prec✝

def Heim1982.startFile : DynamicSemantics.State ExWorld ℕ ExEntity

Starting file: no discourse referents, all worlds open — the minimal state.

Equations

• Heim1982.startFile = ⊥

Each row in Heim1982.Examples corresponds to a structural property of FCS. The per-row theorems below check the row's recorded judgment against the FCS prediction derived above.

theorem Heim1982.datum_indefinitePersists : Examples.indefinite_persists.judgment = Features.Judgment.acceptable

Indefinite persistence is judged acceptable; FCS predicts this via indef_adds_to_dom (the indefinite makes its index familiar and nothing closes it).

theorem Heim1982.datum_standardNegationBlocks : Examples.standard_negation_blocks.judgment = Features.Judgment.unacceptable

Single negation blocks; FCS predicts this via neg_blocks_dref (negation keeps only input-file points).

theorem Heim1982.datum_universalBlocks : Examples.universal_blocks.judgment = Features.Judgment.unacceptable

Universals block; FCS predicts this via ∀ = ¬∃¬ and neg_blocks_dref.

theorem Heim1982.datum_negativeBlocks : Examples.negative_blocks.judgment = Features.Judgment.unacceptable

Negative quantifiers block; same negation mechanism (neg_blocks_dref).

theorem Heim1982.datum_definiteReference : Examples.definite_reference.judgment = Features.Judgment.acceptable

Definite reference is acceptable; FCS predicts this via def_familiar (the established dref satisfies familiarity).

theorem Heim1982.datum_conditionalAntecedent : Examples.conditional_antecedent.judgment = Features.Judgment.unacceptable

If-clause indefinites don't persist; FCS predicts this via the conditional's negation encoding (¬(φ ∧ ¬ψ)) and neg_blocks_dref.