Heim (1982): The Semantics of Definite and Indefinite Noun Phrases

This file formalizes the file change semantics of Chapter III of [heim-1982]: indefinites and definites are alike variables, and they differ in a felicity condition on files, the Extended Novelty-Familiarity-Condition (§2.4, §5.1): an indefinite's card must be new to the file, a definite's already present and, if it has descriptive content, entailed by it. Logical forms are interpreted by their file change potentials, the four rules of §4.4: an atom filters the file and adds its cards, a cumulative formula updates in sequence, the universal quantifier tests the file against its two auxiliary updates, and negation tests it against one. The truth of an utterance is the truth of the resulting file, criterion (C) of §3.2, so Existential Closure is dispensable. The logical forms LF and the rules LF.fcp are stated over the substrate's file change potentials, and the claims the dissertation draws are proved on its own texts: felicity conditions project through the elementary steps of file change (admits_pretzel), a card introduced under every or not does not outlive its sentence (not_admits_everyDog), and criterion (C) gives a free indefinite existential force (trueIn_indef).

Implementation notes

A file is the substrate's State of world–assignment points, with felicity its Part-definedness, satisfaction sets in place of Sat(F) and domains in place of Dom(F); principle (A) of §1.2, that an update only filters the satisfaction set, is the informativeness order. Quantifier Indexing and Existential Closure are not represented, as the revised rules make them dispensable. Accommodating a novel definite (§5.2) is modelled by placing its indefinite card either inside the auxiliary file of a negation or in the initial file. Examples are numbered as in the dissertation, by chapter and section.

References

• [heim-1982]

@[reducible, inline]

abbrev Heim1982.File (W : Type u_3) (M : Type u_4) : Type (max u_4 u_3)

A file (Ch. III): a referential information state with numbered cards.

Equations

• Heim1982.File W M = DynamicSemantics.State W ℕ M

inductive Heim1982.LF (M : Type u_3) : Type u_3

Logical forms of the revised theory (Ch. III §4.4, §5.1): atomic formulas over indexed variables, indefinite and definite noun phrases with their descriptive content, cumulative (sequenced), universally quantified and negated formulas. Predicates are interpreted directly.

• atom {M : Type u_3} {n : ℕ} (ζ : (Fin n → M) → Prop) (args : Fin n → ℕ) : LF M
• indef {M : Type u_3} (i : ℕ) (N : M → Prop) : LF M
• defNP {M : Type u_3} (i : ℕ) (N : M → Prop) : LF M
• seq {M : Type u_3} (φ ψ : LF M) : LF M
• every {M : Type u_3} (φ₁ φ₂ : LF M) : LF M
• neg {M : Type u_3} (ψ : LF M) : LF M

def Heim1982.LF.pro {M : Type u_2} (i : ℕ) : LF M

A pronoun or trace: a definite without descriptive content.

Equations

• Heim1982.LF.pro i = Heim1982.LF.defNP i fun (x : M) => True

def Heim1982.LF.pred₁ {M : Type u_2} (N : M → Prop) (i : ℕ) : LF M

A one-place predication at card i.

Equations

• Heim1982.LF.pred₁ N i = Heim1982.LF.atom (fun (m : Fin 1 → M) => N (m 0)) fun (x : Fin 1) => i

def Heim1982.LF.pred₂ {M : Type u_2} (R : M → M → Prop) (i j : ℕ) : LF M

A two-place predication at cards i, j.

Equations

• Heim1982.LF.pred₂ R i j = Heim1982.LF.atom (fun (m : Fin (Nat.succ 0).succ → M) => R (m 0) (m 1)) ![i, j]

def Heim1982.LF.atomState {W : Type u_1} {M : Type u_2} {n : ℕ} (ζ : (Fin n → M) → Prop) (args : Fin n → ℕ) : File W M

The proposition state of an atomic formula: the points with exactly the atom's cards, whose values stand in ζ.

Equations

• Heim1982.LF.atomState ζ args = {q : DynamicSemantics.Possibility W ℕ (Part M) | q.domain = Set.range args ∧ ∃ (m : Fin n → M), (∀ (k : Fin n), m k ∈ q.assignment (args k)) ∧ ζ m}

def Heim1982.LF.unary {W : Type u_1} {M : Type u_2} (N : M → Prop) (i : ℕ) : DynamicSemantics.FCP W ℕ M

The file change of a one-place atom.

Equations

• Heim1982.LF.unary N i = DynamicSemantics.FCP.ofState (Heim1982.LF.atomState (fun (m : Fin 1 → M) => N (m 0)) fun (x : Fin 1) => i)

def Heim1982.LF.fcp {W : Type u_1} {M : Type u_2} : LF M → DynamicSemantics.FCP W ℕ M

Rules (I)–(IV) of Ch. III §4.4 with the Extended Novelty-Familiarity- Condition of §5.1: an atom merges the file with its proposition state (filtering at familiar cards, adding novel ones); an indefinite is defined only if its card is novel and then introduces it; a definite is defined only if its card is familiar and the file entails its content, and then changes nothing; sequencing composes; every keeps the points of F all of whose extensions in F + φ₁ extend to (F + φ₁) + φ₂; not keeps the points of F with no extension in F + ψ.

Equations

• One or more equations did not get rendered due to their size.
• (Heim1982.LF.atom ζ args).fcp = DynamicSemantics.FCP.ofState (Heim1982.LF.atomState ζ args)
• (Heim1982.LF.indef i N).fcp = DynamicSemantics.FCP.indef i (Heim1982.LF.unary N i)
• (φ.seq ψ).fcp = DynamicSemantics.CCP.Partial.seq φ.fcp ψ.fcp
• ψ.neg.fcp = ψ.fcp.neg

theorem Heim1982.LF.unary_eq_atomVar {W : Type u_1} {M : Type u_2} (N : M → Prop) (i : ℕ) : unary N i = DynamicSemantics.FCP.atomVar N i

The Extended Novelty-Familiarity-Condition

theorem Heim1982.LF.admits_indef {W : Type u_1} {M : Type u_2} (i : ℕ) (N : M → Prop) (F : File W M) : DynamicSemantics.CCP.Partial.admits (indef i N).fcp F ↔ DynamicSemantics.State.Novel F i

An indefinite is defined exactly when its card is novel.

theorem Heim1982.LF.admits_defNP {W : Type u_1} {M : Type u_2} (i : ℕ) (N : M → Prop) (F : File W M) : DynamicSemantics.CCP.Partial.admits (defNP i N).fcp F ↔ DynamicSemantics.State.Familiar F i ∧ DynamicSemantics.FCP.supports F (unary N i)

A definite is defined exactly when its card is familiar and the file entails its descriptive content.

theorem Heim1982.LF.supports_unary_true {W : Type u_1} {M : Type u_2} (F : File W M) {i : ℕ} (h : DynamicSemantics.State.Familiar F i) : DynamicSemantics.FCP.supports F (unary (fun (x : M) => True) i)

theorem Heim1982.LF.fcp_pro {W : Type u_1} {M : Type u_2} (F : File W M) {i : ℕ} (h : DynamicSemantics.State.Familiar F i) : (pro i).fcp F = Part.some F

A pronoun at a familiar card changes nothing.

theorem Heim1982.LF.admits_pro {W : Type u_1} {M : Type u_2} (F : File W M) (i : ℕ) : DynamicSemantics.CCP.Partial.admits (pro i).fcp F ↔ DynamicSemantics.State.Familiar F i

A pronoun is defined exactly when its card is familiar.

theorem Heim1982.LF.fcp_indef {W : Type u_1} {M : Type u_2} {F : File W M} {i : ℕ} (N : M → Prop) (h : DynamicSemantics.State.Novel F i) : (indef i N).fcp F = Part.some {p : DynamicSemantics.Possibility W ℕ (Part M) | p ∈ DynamicSemantics.State.randomAssign F i ∧ ∃ m ∈ p.assignment i, N m}

The file change of an indefinite at a novel card: random assignment then filtering.

theorem Heim1982.LF.mem_fcp_indef {W : Type u_1} {M : Type u_2} {F F' : File W M} {i : ℕ} {N : M → Prop} : F' ∈ (indef i N).fcp F ↔ DynamicSemantics.State.Novel F i ∧ F' = {p : DynamicSemantics.Possibility W ℕ (Part M) | p ∈ DynamicSemantics.State.randomAssign F i ∧ ∃ m ∈ p.assignment i, N m}

Membership and projection through the rules

theorem Heim1982.LF.mem_fcp_seq {W : Type u_1} {M : Type u_2} {φ ψ : LF M} {F F' : File W M} : F' ∈ (φ.seq ψ).fcp F ↔ ∃ F₁ ∈ φ.fcp F, F' ∈ ψ.fcp F₁

theorem Heim1982.LF.mem_fcp_every {W : Type u_1} {M : Type u_2} {φ₁ φ₂ : LF M} {F F' : File W M} : F' ∈ (φ₁.every φ₂).fcp F ↔ ∃ F₁ ∈ φ₁.fcp F, ∃ F₂ ∈ φ₂.fcp F₁, F' = {p : DynamicSemantics.Possibility W ℕ (Part M) | p ∈ F ∧ ∀ q ∈ F₁, p ≤ q → ∃ r ∈ F₂, q ≤ r}

theorem Heim1982.LF.subset_of_mem_fcp_every {W : Type u_1} {M : Type u_2} {φ₁ φ₂ : LF M} {F F' : File W M} (h : F' ∈ (φ₁.every φ₂).fcp F) : F' ⊆ F

The universal quantifier tests the file: its output is a subset.

theorem Heim1982.LF.admits_seq_of_mem {W : Type u_1} {M : Type u_2} {φ ψ : LF M} {F F' : File W M} (h : F' ∈ φ.fcp F) (h' : DynamicSemantics.CCP.Partial.admits ψ.fcp F') : DynamicSemantics.CCP.Partial.admits (φ.seq ψ).fcp F

theorem Heim1982.LF.admits_pro_seq {W : Type u_1} {M : Type u_2} {ψ : LF M} {F : File W M} {i : ℕ} (h : DynamicSemantics.State.Familiar F i) (h' : DynamicSemantics.CCP.Partial.admits ψ.fcp F) : DynamicSemantics.CCP.Partial.admits ((pro i).seq ψ).fcp F

theorem Heim1982.LF.admits_every_of_mem {W : Type u_1} {M : Type u_2} {φ₁ φ₂ : LF M} {F F₁ : File W M} (h : F₁ ∈ φ₁.fcp F) (h' : DynamicSemantics.CCP.Partial.admits φ₂.fcp F₁) : DynamicSemantics.CCP.Partial.admits (φ₁.every φ₂).fcp F

theorem Heim1982.LF.every_eq_cond {W : Type u_1} {M : Type u_2} (φ₁ φ₂ : LF M) : (φ₁.every φ₂).fcp = φ₁.fcp.cond φ₂.fcp

Rule (III) is the negated conjunction ¬(φ₁ ∧ ¬φ₂).

theorem Heim1982.LF.admits_every {W : Type u_1} {M : Type u_2} (φ₁ φ₂ : LF M) (F : File W M) : DynamicSemantics.CCP.Partial.admits (φ₁.every φ₂).fcp F ↔ ∃ (h : DynamicSemantics.CCP.Partial.admits φ₁.fcp F), DynamicSemantics.CCP.Partial.admits φ₂.fcp ((φ₁.fcp F).get h)

Felicity conditions of a quantified formula project as those of a conditional: the restrictive term must be felicitous in the file, the nuclear scope in the file updated with it.

Cards through the rules

theorem Heim1982.LF.novel_atomState {W : Type u_1} {M : Type u_2} {n : ℕ} {ζ : (Fin n → M) → Prop} {args : Fin n → ℕ} {j : ℕ} (hj : j ∉ Set.range args) : DynamicSemantics.State.Novel (atomState ζ args) j

A card not among an atom's is novel at its proposition state.

theorem Heim1982.LF.familiar_of_mem_indef {W : Type u_1} {M : Type u_2} {F F' : File W M} {i : ℕ} {N : M → Prop} (h : F' ∈ (indef i N).fcp F) : DynamicSemantics.State.Familiar F' i

theorem Heim1982.LF.familiar_of_mem_indef_of_familiar {W : Type u_1} {M : Type u_2} {F F' : File W M} {i j : ℕ} {N : M → Prop} (hj : DynamicSemantics.State.Familiar F j) (h : F' ∈ (indef i N).fcp F) : DynamicSemantics.State.Familiar F' j

theorem Heim1982.LF.novel_of_mem_indef {W : Type u_1} {M : Type u_2} {F F' : File W M} {i j : ℕ} {N : M → Prop} (hij : j ≠ i) (hj : DynamicSemantics.State.Novel F j) (h : F' ∈ (indef i N).fcp F) : DynamicSemantics.State.Novel F' j

theorem Heim1982.LF.familiar_of_mem_atom {W : Type u_1} {M : Type u_2} {n : ℕ} {ζ : (Fin n → M) → Prop} {args : Fin n → ℕ} {F F' : File W M} {j : ℕ} (hj : DynamicSemantics.State.Familiar F j) (h : F' ∈ (atom ζ args).fcp F) : DynamicSemantics.State.Familiar F' j

theorem Heim1982.LF.novel_of_mem_atom {W : Type u_1} {M : Type u_2} {n : ℕ} {ζ : (Fin n → M) → Prop} {args : Fin n → ℕ} {F F' : File W M} {j : ℕ} (hj : j ∉ Set.range args) (hF : DynamicSemantics.State.Novel F j) (h : F' ∈ (atom ζ args).fcp F) : DynamicSemantics.State.Novel F' j

Principle (A) of §1.2 and false files

theorem Heim1982.LF.le_of_mem_fcp {W : Type u_1} {M : Type u_2} (φ : LF M) {F F' : File W M} : F' ∈ φ.fcp F → F ≤ F'

Principle (A): every update ascends in informativeness.

theorem Heim1982.LF.fcp_empty {W : Type u_1} {M : Type u_2} (φ : LF M) {F' : File W M} : F' ∈ φ.fcp ∅ → F' = ∅

Once false, always false (§3.2): every update of the absurd file is absurd.

Truth (§3.2)

Criterion (C): an utterance is true with respect to a file iff the resulting file is true, i.e. has a satisfying point (FCP.trueIn). No existential closure is needed: a novel card ranges over the whole domain, a familiar one over the values its card admits.

theorem Heim1982.LF.trueIn_indef {W : Type u_1} {M : Type u_2} {F : File W M} {i : ℕ} (N : M → Prop) (h : DynamicSemantics.State.Novel F i) : DynamicSemantics.FCP.trueIn F (indef i N).fcp ↔ Set.Nonempty F ∧ ∃ (m : M), N m

A free indefinite has existential force: "A woman₁ …" is true w.r.t. a true file iff some individual is a woman.

theorem Heim1982.LF.trueIn_pro_pred {W : Type u_1} {M : Type u_2} {F : File W M} {i : ℕ} (N : M → Prop) (h : DynamicSemantics.State.Familiar F i) : DynamicSemantics.FCP.trueIn F ((pro i).seq (pred₁ N i)).fcp ↔ ∃ p ∈ F, ∃ m ∈ p.assignment i, N m

A definite has the force of its card: "She₁ is a woman" is true w.r.t. a file iff some point's value at card 1 is a woman.

The book's texts

def Heim1982.aDog {M : Type u_2} (dog cameIn layDown : M → Prop) : LF M

Ch. I §1 (9): "A dog₁ came in. It₁ lay down under the table."

Equations

• Heim1982.aDog dog cameIn layDown = (Heim1982.LF.indef 1 dog).seq ((Heim1982.LF.pred₁ cameIn 1).seq ((Heim1982.LF.pro 1).seq (Heim1982.LF.pred₁ layDown 1)))

def Heim1982.everyDog {M : Type u_2} (dog cameIn layDown : M → Prop) : LF M

Ch. I §1 (16): "Every dog₁ came in. It₁ lay down under the table."

Equations

• Heim1982.everyDog dog cameIn layDown = ((Heim1982.LF.indef 1 dog).every (Heim1982.LF.pred₁ cameIn 1)).seq ((Heim1982.LF.pro 1).seq (Heim1982.LF.pred₁ layDown 1))

def Heim1982.noDog {M : Type u_2} (dog cameIn layDown : M → Prop) : LF M

Ch. I §1 (17): "No dog₁ came in. It₁ lay down under the table."

Equations

• Heim1982.noDog dog cameIn layDown = ((Heim1982.LF.indef 1 dog).seq (Heim1982.LF.pred₁ cameIn 1)).neg.seq ((Heim1982.LF.pro 1).seq (Heim1982.LF.pred₁ layDown 1))

def Heim1982.womanDog {M : Type u_2} (dog woman : M → Prop) (bit hit : M → M → Prop) : LF M

Ch. III §2.4 (5): "A woman₁ was bitten by a dog₂. She₁ hit him₂."

Equations

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

def Heim1982.pretzelText {M : Type u_2} (person pretzel : M → Prop) (bought ate : M → M → Prop) : LF M

Ch. III §4.1 (2): "Everyone₁ bought a pretzel₂ and ate it₂."

Equations

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

def Heim1982.kingLocal {M : Type u_2} (king : M → Prop) (lunch : M → M → Prop) (m i : ℕ) : LF M

Ch. III §5.2 (10) with the king's card accommodated in the auxiliary file of the negation.

Equations

• Heim1982.kingLocal king lunch m i = ((Heim1982.LF.indef i king).seq (Heim1982.LF.pred₂ lunch m i)).neg

def Heim1982.kingGlobal {M : Type u_2} (king : M → Prop) (lunch : M → M → Prop) (m i : ℕ) : LF M

Ch. III §5.2 (10) with the king's card accommodated in the initial file.

Equations

• Heim1982.kingGlobal king lunch m i = (Heim1982.LF.indef i king).seq (Heim1982.LF.pred₂ lunch m i).neg

theorem Heim1982.admits_aDog {W : Type u_1} {M : Type u_2} {dog cameIn layDown : M → Prop} {F : File W M} (h : DynamicSemantics.State.Novel F 1) : DynamicSemantics.CCP.Partial.admits (aDog dog cameIn layDown).fcp F

(9) is felicitous whenever card 1 is novel: the indefinite's card is familiar for the pronoun of the next sentence.

theorem Heim1982.not_admits_everyDog {W : Type u_1} {M : Type u_2} {dog cameIn layDown : M → Prop} {F : File W M} (h : DynamicSemantics.State.Novel F 1) (ht : DynamicSemantics.FCP.trueIn F ((LF.indef 1 dog).every (LF.pred₁ cameIn 1)).fcp) : ¬DynamicSemantics.CCP.Partial.admits (everyDog dog cameIn layDown).fcp F

(16) is infelicitous whenever card 1 is novel and the universal sentence is true: every returns a subset of the file, at which card 1 is still novel, so the pronoun is undefined.

theorem Heim1982.not_admits_noDog {W : Type u_1} {M : Type u_2} {dog cameIn layDown : M → Prop} {F : File W M} (h : DynamicSemantics.State.Novel F 1) (ht : DynamicSemantics.FCP.trueIn F ((LF.indef 1 dog).seq (LF.pred₁ cameIn 1)).neg.fcp) : ¬DynamicSemantics.CCP.Partial.admits (noDog dog cameIn layDown).fcp F

(17) is infelicitous whenever card 1 is novel and the negated sentence is true, for the same reason.

theorem Heim1982.admits_womanDog {W : Type u_1} {M : Type u_2} {dog woman : M → Prop} {bit hit : M → M → Prop} {F : File W M} (h1 : DynamicSemantics.State.Novel F 1) (h2 : DynamicSemantics.State.Novel F 2) : DynamicSemantics.CCP.Partial.admits (womanDog dog woman bit hit).fcp F

§2.4 (5) is felicitous whenever cards 1 and 2 are novel in the initial file: the definites of its second sentence find their cards in the file the first sentence has produced.

theorem Heim1982.admits_pretzel {W : Type u_1} {M : Type u_2} {person pretzel : M → Prop} {bought ate : M → M → Prop} {F : File W M} (h1 : DynamicSemantics.State.Novel F 1) (h2 : DynamicSemantics.State.Novel F 2) : DynamicSemantics.CCP.Partial.admits (pretzelText person pretzel bought ate).fcp F

§4.1 (2) is felicitous against a file at which cards 1 and 2 are novel: "it₂" finds its card in the intermediate file produced by "a pretzel₂" inside the nuclear scope.

theorem Heim1982.novel_of_mem_kingLocal {W : Type u_1} {M : Type u_2} {king : M → Prop} {lunch : M → M → Prop} {F F' : File W M} {m i : ℕ} (h : DynamicSemantics.State.Novel F i) (hF' : F' ∈ (kingLocal king lunch m i).fcp F) : DynamicSemantics.State.Novel F' i

Accommodation in the auxiliary file of the negation (§5.2) leaves the initial file's cards as they were: the king's card does not survive the negation, the narrow-scope reading.

theorem Heim1982.familiar_of_mem_kingGlobal {W : Type u_1} {M : Type u_2} {king : M → Prop} {lunch : M → M → Prop} {F F' : File W M} {m i : ℕ} (hF' : F' ∈ (kingGlobal king lunch m i).fcp F) : DynamicSemantics.State.Familiar F' i ∧ ∀ p ∈ F', ∃ x ∈ p.assignment i, king x

Accommodation in the initial file (§5.2) makes the king's card part of the resulting file, which thereby entails that there is a king.