Heim (1982): File Change Semantics and Anaphora #
Formal analysis of cross-sentential anaphora using [Hei82]'s
File Change Semantics. This study file connects the FCS theory
(Semantics/Dynamic/FileChange/Basic.lean) to the example rows
in Data/Examples/Heim1982.json (Heim1982.Examples).
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 ([Hei82], 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
example rows in Heim1982.Examples.
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 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₁.
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 [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 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 [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 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.
[Hei82]'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.
[Hei82]'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 in
Heim1982.Examples.
Equations
- Heim1982.instDecidableEqExWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
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.instReprExWorld = { reprPrec := Heim1982.instReprExWorld.repr }
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 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.
Indefinite persistence is judged acceptable; FCS predicts this via
indef_adds_to_dom (the indefinite extends Dom and nothing closes it).
Single negation blocks; FCS predicts this via neg_blocks_dref
(negation preserves the input domain).
Universals block; FCS predicts this via ∀ = ¬∃¬ and neg_blocks_dref.
Negative quantifiers block; same negation mechanism (neg_blocks_dref).
Definite reference is acceptable; FCS predicts this via
indef_then_def_defined (the established dref satisfies familiarity).
If-clause indefinites don't persist; FCS predicts this via the
conditional's negation encoding (¬(φ ∧ ¬ψ)) and neg_blocks_dref.