Heim (1982): File Change Semantics and Anaphora #
@cite{heim-1982}
Formal analysis of cross-sentential anaphora using @cite{heim-1982}'s
File Change Semantics. This study file connects the FCS theory
(Theories/Semantics/Dynamic/FileChange/Basic.lean) to the empirical
data in Phenomena/Anaphora/CrossSentential.lean.
Key Claims Formalized #
Indefinites introduce discourse referents (new file cards): "A man walked in" opens a new dref that persists across sentences.
Negation blocks dref export: "John didn't see a bird" confines the bird's dref to the scope of negation — it doesn't persist.
Conjunction is sequential update: "A man walked in. He sat down." = F + [∃x. man(x) ∧ walkedIn(x)] + [satDown(x)].
Novelty-Familiarity Condition: indefinites require novel indices; definites require familiar ones. Violations are presupposition failure (undefinedness), not falsehood.
Truth criterion (C): φ is true w.r.t. F iff Sat(F + φ) is nonempty (@cite{heim-1982}, Ch III §3.2). This builds existential quantification into the notion of truth.
Connection to Empirical Data #
Each section below derives FCS predictions that account for specific
data in CrossSententialAnaphora.
We work with a simple model: W = possible worlds, E = entities.
Predicates are modeled as functions on possibilities.
"A man walked in. He sat down."
This accounts for CrossSententialAnaphora.indefinitePersists. 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₁.
The indefinite "a man walked in" as an FCP: ∃x. man(x) ∧ walkedIn(x).
Equations
- One or more equations did not get rendered due to their size.
Instances For
"He sat down" as an FCP: satDown(x).
Equations
- Heim1982.heSatDown satDown x = Semantics.Dynamic.FileChangeSemantics.FCP.atomVar satDown x
Instances For
The full discourse "A man walked in. He sat down."
Equations
- Heim1982.indefinitePersistsDiscourse man walkedIn satDown x = Heim1982.aManWalkedIn man walkedIn x +> Heim1982.heSatDown satDown x
Instances For
When x is novel, the indefinite FCP is defined (not a presupposition failure) — provided the body is total.
After the indefinite, x is in the domain — provided the body preserves domain membership.
This is the formal content of "indefinites introduce discourse referents" — the defining claim of @cite{heim-1982}.
"John didn't see a bird. *It was singing."
This accounts for CrossSententialAnaphora.standardNegationBlocks.
The FCS analysis: negation closes the scope of the indefinite's dref.
After F + [¬(∃x. bird(x) ∧ saw(j,x))], x is NOT in Dom — the
negation's domain matches the input domain, not the extended one.
A variable introduced inside negation is NOT in the output domain.
Negation preserves the input domain (neg_preserves_dom), so a
novel variable stays novel after negation — the dref is trapped
inside the scope of ¬.
The Novelty-Familiarity Condition is @cite{heim-1982}'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 returning none.
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.
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).
An indefinite followed by a definite with the same index is well-defined: the indefinite makes x familiar for the definite.
"A man₁ walked in. He₁ sat down." — after the indefinite introduces dref 1, the definite "he₁" finds it familiar.
@cite{heim-1982}'s truth definition (Ch III §3.2, p. 214):
(C) A formula φ is true w.r.t. a file F if F + φ is true, and false w.r.t. F if F + φ is false.
A file is true iff Sat(F) ≠ ∅. So truth of φ w.r.t. F amounts to Sat(F + φ) being nonempty. Crucially, this builds existential quantification into the notion of truth, making Existential Closure dispensable (Ch III §3.1).
Truth unfolds to: F + φ is defined and has nonempty Sat.
Falsity unfolds to: F + φ is defined but has empty Sat.
Support (idempotency) implies truth for consistent files.
Support is idempotent: if F supports φ, then updating twice equals updating once.
@cite{heim-1982}'s Principle (A): file change only eliminates possibilities, never adds them. This holds for atomic updates, negation, and their compositions.
Negation is eliminative: Sat(F + ¬φ) ⊆ Sat(F).
Sequential composition preserves eliminativity.
We instantiate the FCS framework with a concrete finite model
to verify the theory matches the empirical data from
CrossSententialAnaphora.
Equations
- Heim1982.instDecidableEqExWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- Heim1982.instReprExWorld = { reprPrec := Heim1982.instReprExWorld.repr }
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✝
Instances For
Equations
- Heim1982.instDecidableEqExEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- Heim1982.instReprExEntity = { reprPrec := Heim1982.instReprExEntity.repr }
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✝
Instances For
Starting file: no discourse referents, all possibilities.
Equations
- Heim1982.startFile = { dom := ∅, sat := Set.univ }
Instances For
Each datum in CrossSententialAnaphora corresponds to a structural
property of FCS. The per-datum theorems below verify that the FCS
predictions match the empirical judgments.
FCS correctly records that indefinite persistence is felicitous.
FCS correctly records that standard negation blocks.
FCS correctly records that universals block.
FCS correctly records that negative quantifiers block.
FCS correctly records that definite reference is felicitous.
FCS correctly records that conditionals block antecedent drefs.
The structural FCS properties that account for each datum:
| Datum | FCS Property | Theorem |
|---|---|---|
indefinitePersists | indef extends Dom; body preserves it | indef_adds_to_dom |
universalBlocks | Universal = ∀ = ¬∃¬; negation preserves Dom | neg_blocks_dref |
negativeBlocks | Negation preserves Dom | neg_blocks_dref |
standardNegationBlocks | Same mechanism | neg_blocks_dref |
conditionalAntecedent | Conditional = ¬(φ ∧ ¬ψ); negation preserves Dom | cond_eq + neg_blocks_dref |
definiteReference | def_ requires familiarity; succeeds when dref established | indef_then_def_defined |