Krifka (2013): Definitional Generics

This file formalizes [Kri13]'s distinction between descriptive and definitional generic sentences. Madrigals are popular generalizes about the world; A madrigal is polyphonic says how the word madrigal is to be interpreted, which is why an accidental property makes an indefinite-singular generic odd (#A madrigal is popular). Meaning depends on two indices, an interpretation and a world, and a common ground pairs a set of admissible interpretations with a set of worlds (CommonGround). A descriptive update keeps the interpretations and discards worlds (descUpdate); a definitional update keeps the worlds and discards interpretations (defUpdate), and with a topic-comment structure it restricts only the interpretation of the definiendum (defUpdateTopic). Two further claims are theorems: admissible interpretations stay convex under a definitional update whose proposition is convex in the interpretation (ordConnected_defUpdate), and a definitional generic can rest on an empirical finding: once a species rule ties the chromosome number to being a donkey, the descriptive update with Chiquita's count leaves the definitional update with A donkey has 62 chromosomes nothing to do (defUpdateTopic_descUpdate).

Implementation notes

• Common grounds carry finite sets so that the paper's models are decided, and the updates take decidable propositions.
• The species rule is stated per interpretation; the chromosome count is a measure and so the same under every interpretation; and Chiquita, a specimen, is a donkey under every admissible interpretation.
• The paper's data are in Data/Examples/Krifka2013.json. The correlation of subject form with reading, which the paper leaves as a tendency, is not formalized.

TODO

• The paper's definitional update with Feynman is tall and Teller is not tall is meant to leave the middle standard, but with the heights it lists Teller is tall under that standard in the first world, so the update as printed leaves no standard; the descriptive update with Feynman is tall is computed instead.

References

• [Kri13]
• [Bar02a] — the descriptive and metalinguistic uses of tall
• [Coh01] — the rule types of indefinite-singular generics
• [Gre07], [Kri80] — in-virtue-of generics; necessity a posteriori

structure Krifka2013.CommonGround (I : Type u_4) (W : Type u_5) : Type (max u_4 u_5)

A common ground (§3.1): the admissible interpretations and the possible worlds.

• interps : Finset I
• worlds : Finset W

theorem Krifka2013.CommonGround.ext_iff {I : Type u_4} {W : Type u_5} {x y : CommonGround I W} : x = y ↔ x.interps = y.interps ∧ x.worlds = y.worlds

theorem Krifka2013.CommonGround.ext {I : Type u_4} {W : Type u_5} {x y : CommonGround I W} (interps : x.interps = y.interps) (worlds : x.worlds = y.worlds) : x = y

def Krifka2013.instDecidableEqCommonGround.decEq {I✝ : Type u_4} {W✝ : Type u_5} [DecidableEq I✝] [DecidableEq W✝] (x✝ x✝¹ : CommonGround I✝ W✝) : Decidable (x✝ = x✝¹)

Equations

• Krifka2013.instDecidableEqCommonGround.decEq { interps := a, worlds := a_1 } { interps := b, worlds := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Krifka2013.instDecidableEqCommonGround {I✝ : Type u_4} {W✝ : Type u_5} [DecidableEq I✝] [DecidableEq W✝] : DecidableEq (CommonGround I✝ W✝)

Equations

• Krifka2013.instDecidableEqCommonGround = Krifka2013.instDecidableEqCommonGround.decEq

def Krifka2013.CommonGround.descUpdate {I : Type u_1} {W : Type u_2} (cg : CommonGround I W) (φ : I → W → Prop) [(i : I) → (w : W) → Decidable (φ i w)] : CommonGround I W

A descriptive update (14): keep the worlds in which the proposition holds under some admissible interpretation.

Equations

• cg.descUpdate φ = { interps := cg.interps, worlds := {w ∈ cg.worlds | ∃ i ∈ cg.interps, φ i w} }

def Krifka2013.CommonGround.defUpdate {I : Type u_1} {W : Type u_2} (cg : CommonGround I W) (φ : I → W → Prop) [(i : I) → (w : W) → Decidable (φ i w)] : CommonGround I W

A definitional update (15): keep the interpretations under which the proposition holds in every world.

Equations

• cg.defUpdate φ = { interps := {i ∈ cg.interps | ∀ w ∈ cg.worlds, φ i w}, worlds := cg.worlds }

def Krifka2013.CommonGround.defUpdateTopic {I : Type u_1} {W : Type u_2} {X : Type u_3} (cg : CommonGround I W) [Fintype X] (α β : I → W → X → Prop) [(i : I) → (w : W) → (x : X) → Decidable (α i w x)] [(i : I) → (w : W) → (x : X) → Decidable (β i w x)] : CommonGround I W

A definitional update with a predicative topic (25): keep the interpretations of the definiendum α under which whatever falls under it satisfies the definiens β under every admissible interpretation.

Equations

• cg.defUpdateTopic α β = { interps := {i ∈ cg.interps | ∀ w ∈ cg.worlds, ∀ (x : X), α i w x → ∀ i' ∈ cg.interps, β i' w x}, worlds := cg.worlds }

@[simp]

theorem Krifka2013.CommonGround.interps_descUpdate {I : Type u_1} {W : Type u_2} (cg : CommonGround I W) (φ : I → W → Prop) [(i : I) → (w : W) → Decidable (φ i w)] : (cg.descUpdate φ).interps = cg.interps

@[simp]

theorem Krifka2013.CommonGround.worlds_defUpdate {I : Type u_1} {W : Type u_2} (cg : CommonGround I W) (φ : I → W → Prop) [(i : I) → (w : W) → Decidable (φ i w)] : (cg.defUpdate φ).worlds = cg.worlds

theorem Krifka2013.CommonGround.worlds_descUpdate_subset {I : Type u_1} {W : Type u_2} (cg : CommonGround I W) (φ : I → W → Prop) [(i : I) → (w : W) → Decidable (φ i w)] : (cg.descUpdate φ).worlds ⊆ cg.worlds

theorem Krifka2013.CommonGround.interps_defUpdate_subset {I : Type u_1} {W : Type u_2} (cg : CommonGround I W) (φ : I → W → Prop) [(i : I) → (w : W) → Decidable (φ i w)] : (cg.defUpdate φ).interps ⊆ cg.interps

theorem Krifka2013.CommonGround.ordConnected_defUpdate {I : Type u_1} {W : Type u_2} (cg : CommonGround I W) (φ : I → W → Prop) [(i : I) → (w : W) → Decidable (φ i w)] [Preorder I] (hI : (↑cg.interps).OrdConnected) (hφ : ∀ w ∈ cg.worlds, {i : I | φ i w}.OrdConnected) : (↑(cg.defUpdate φ).interps).OrdConnected

Admissible interpretations are convex (§3.1): a definitional update whose proposition is convex in the interpretation, as Feynman is tall is in the standard of tallness, keeps a convex set of interpretations convex.

theorem Krifka2013.CommonGround.defUpdateTopic_descUpdate {I : Type u_1} {W : Type u_2} {X : Type u_3} (cg : CommonGround I W) [Fintype X] (donkey : I → W → X → Prop) [(i : I) → (w : W) → (x : X) → Decidable (donkey i w x)] (chrom : I → W → X → ℕ) (ch : X) (n : ℕ) (hrule : ∀ i ∈ cg.interps, ∀ w ∈ cg.worlds, ∀ (x y : X), donkey i w x → donkey i w y → chrom i w x = chrom i w y) (hchrom : ∀ (i i' : I) (w : W) (x : X), chrom i w x = chrom i' w x) (hch : ∀ i ∈ cg.interps, ∀ w ∈ cg.worlds, donkey i w ch) : ((cg.descUpdate fun (i : I) (w : W) => chrom i w ch = n ∧ donkey i w ch).defUpdateTopic donkey fun (i : I) (w : W) (x : X) => chrom i w x = n) = cg.descUpdate fun (i : I) (w : W) => chrom i w ch = n ∧ donkey i w ch

A definitional generic from an empirical finding ((31)–(36)): with the species rule (33) in the common ground, the chromosome count a measure, and Chiquita a donkey under every admissible interpretation, the descriptive update with her count already settles the definitional update with A donkey has 62 chromosomes.

Tall, popular, polyphonic

@[reducible, inline]

abbrev Krifka2013.Idx : Type

Three interpretations, or three worlds.

Equations

• Krifka2013.Idx = Fin 3

def Krifka2013.standard : Idx → ℕ

The standards of tallness of (16), in centimetres.

Equations

• Krifka2013.standard 0 = 190
• Krifka2013.standard 1 = 180
• Krifka2013.standard 2 = 170

def Krifka2013.feynman : Idx → ℕ

Feynman's height in each world of (16).

Equations

• Krifka2013.feynman 0 = 195
• Krifka2013.feynman 1 = 185
• Krifka2013.feynman 2 = 175

@[reducible, inline]

abbrev Krifka2013.feynmanTall (i w : Idx) : Prop

Feynman is tall under a standard, in a world.

Equations

• Krifka2013.feynmanTall i w = (Krifka2013.standard i ≤ Krifka2013.feynman w)

theorem Krifka2013.descUpdate_feynmanTall : { interps := {0, 1}, worlds := Finset.univ }.descUpdate feynmanTall = { interps := {0, 1}, worlds := {0, 1} }

The descriptive update (17): with the two stricter standards admissible, the world in which Feynman is shortest is discarded.

def Krifka2013.cg₀ : CommonGround Idx Idx

The initial common ground of (20) and (21).

Equations

• Krifka2013.cg₀ = { interps := Finset.univ, worlds := Finset.univ }

@[reducible, inline]

abbrev Krifka2013.popular : Idx → (w : Idx) → Prop

Madrigals are popular holds in the first two worlds under every interpretation.

Equations

• Krifka2013.popular x✝ w = (w ≠ 2)

@[reducible, inline]

abbrev Krifka2013.polyphonic (i : Idx) : Idx → Prop

Madrigals are polyphonic holds under the first two interpretations in every world.

Equations

• Krifka2013.polyphonic i x✝ = (i ≠ 2)

theorem Krifka2013.descUpdate_popular : cg₀.descUpdate popular = { interps := Finset.univ, worlds := {0, 1} }

The descriptive update (20) discards the world in which madrigals are not popular.

theorem Krifka2013.defUpdate_polyphonic : cg₀.defUpdate polyphonic = { interps := {0, 1}, worlds := Finset.univ }

The definitional update (21) discards the interpretation that admits monophonic madrigals.