Cooper (2023) Ch. 7 — Witness-based quantification

[Coo23] [BC81] [vB84]

Cooper's From Perception to Communication Ch. 7 replaces classical set-theoretic GQ denotations (cf. Quantification.GQ) with witness sets — finite sets of individuals satisfying cardinality conditions specific to each quantifier. The reusable substrate (witness-set types, particular/general witness conditions, induced GQ denotations, conservativity proofs, anaphora-availability tables) lives in Linglib/Semantics/TypeTheoretic/WitnessQuantification.lean; this file contains Cooper's chapter-specific deployment.

Main definitions

• PPpty.isPure, WitnessType, WitnessTypeP — pure-property witness types (§7.2.3).
• purify (𝔓), purifyUniv (𝔓ʸ) — Cooper's purification operators (§7.2.3) extracting pure properties for weak/strong donkey readings.
• ExperienceBase and friends — Austinian-propositions / frequentist conditional-probability machinery (§7.3).
• pptyConj, CntxtWithGap, CntxtFull, SlashCat, IsWhNP, TypedPpty, recSubtract, dependencyFamily, depFamilyQuant — long-distance-dependency apparatus (§7.5).

Main statements

• purify_trivial, purify_nonempty_iff, purifyUniv_nonempty_iff — characterising lemmas for the purification operators.
• purify_pure_equiv, purifyUniv_pure_equiv, donkey_readings_agree_when_pure — for pure properties, weak and strong donkey readings coincide.
• Phenomenon-anchored theorems (dog_ext_card, aDogBarks, not_noDogBarks, few_has_compset, a_few_no_compset, bark_given_dog_prob) — Cooper's worked examples against the graduated witness-set substrate.

§7.2.3 Pure properties, purification, and 𝔗(P) (eqs 11–19)

A parametric property P : PPpty E has background P.Bg and foreground P.fg. P is pure when Bg is trivial (≅ Unit): no extra background constraints.

Purification folds background conditions into the property body:

• 𝔓(P): existential — ∃ context satisfying bg, body holds (weak donkey)
• 𝔓ʸ(P): universal — ∀ contexts satisfying bg, body holds (strong donkey)

def Cooper2023Ch7.PPpty.isPure {E : Type} (P : Semantics.TypeTheoretic.PPpty E) : Prop

A parametric property is pure when its background is trivial. §7.2.3, eq (7a): P.bg has only the x-field.

Equations

• Cooper2023Ch7.PPpty.isPure P = (Nonempty P.Bg ∧ Subsingleton P.Bg)

def Cooper2023Ch7.WitnessType {E : Type} (P : Semantics.TypeTheoretic.Ppty E) : Type

The type of witnesses for property P. §7.2.3, eq (17): a : 𝔗(P) iff 𝔓(P){a} is witnessed. For a pure property, 𝔗(P) = {a : E // Nonempty (P a)}.

Equations

• Cooper2023Ch7.WitnessType P = { a : E // Nonempty (P a) }

def Cooper2023Ch7.purify {E : Type} (P : Semantics.TypeTheoretic.PPpty E) : Semantics.TypeTheoretic.Ppty E

Existential purification of a parametric property. §7.2.3, eq (12): 𝔓(P) merges background conditions into the body via existential quantification. 𝔓(P)(a) = Σ (c : Bg), fg c a.

Equations

• Cooper2023Ch7.purify P a = ((c : P.Bg) × P.fg c a)

def Cooper2023Ch7.purifyUniv {E : Type} (P : Semantics.TypeTheoretic.PPpty E) : Semantics.TypeTheoretic.Ppty E

Universal purification of a parametric property. §7.2.3, eq (13): 𝔓ʸ(P) universally quantifies over background contexts. Used for strong donkey readings.

Equations

• Cooper2023Ch7.purifyUniv P a = ((c : P.Bg) → P.fg c a)

def Cooper2023Ch7.term𝔓_ : Lean.ParserDescr

Notation for purification operators.

Equations

• Cooper2023Ch7.term𝔓_ = Lean.ParserDescr.node `Cooper2023Ch7.term𝔓_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝔓") (Lean.ParserDescr.cat `term 1024))

def Cooper2023Ch7.«term𝔓ʸ_» : Lean.ParserDescr

Equations

• Cooper2023Ch7.«term𝔓ʸ_» = Lean.ParserDescr.node `Cooper2023Ch7.«term𝔓ʸ_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝔓ʸ") (Lean.ParserDescr.cat `term 1024))

theorem Cooper2023Ch7.purify_trivial {E : Type} (P : Semantics.TypeTheoretic.Ppty E) (a : E) : purify (Semantics.TypeTheoretic.Parametric.trivial P) a = ((_ : Unit) × P a)

For a trivial parametric property, purification adds only a Unit factor.

theorem Cooper2023Ch7.purify_nonempty_iff {E : Type} (P : Semantics.TypeTheoretic.PPpty E) (a : E) : Nonempty (purify P a) ↔ ∃ (c : P.Bg), Nonempty (P.fg c a)

Purified property is witnessed iff the original is witnessable under some context.

theorem Cooper2023Ch7.purifyUniv_nonempty_iff {E : Type} (P : Semantics.TypeTheoretic.PPpty E) (a : E) : Nonempty (purifyUniv P a) ↔ ∀ (c : P.Bg), Nonempty (P.fg c a)

Universal purification: witnessed iff property holds under all contexts.

def Cooper2023Ch7.WitnessTypeP {E : Type} (P : Semantics.TypeTheoretic.PPpty E) : Type

WitnessType for parametric properties via purification.

Equations

• Cooper2023Ch7.WitnessTypeP P = Cooper2023Ch7.WitnessType (Cooper2023Ch7.purify P)

§7.3 Austinian propositions and probabilistic quantification (eqs 36–58)

Probabilities for quantifiers are estimated from an agent's finite experience base 𝔉 — a set of Austinian propositions recording categorical judgments [sit=a, type=T].

Frequentist conditional probability: p_𝔉(T₁‖T₂) = |[T₁∧T₂]_𝔉| / |[T₂]_𝔉|

structure Cooper2023Ch7.ExperienceBase (E P : Type) [DecidableEq E] [DecidableEq P] : Type

An experience base: the agent's memory of categorical judgments. §7.3, eq (37): 𝔉 is a finite set of [sit=a, type=T] records. Parameterized over entity type E and predicate type P.

• judgments : Finset (E × P)

  The observed entity-predicate judgments

def Cooper2023Ch7.ExperienceBase.ext {E P : Type} [DecidableEq E] [DecidableEq P] (𝔉 : ExperienceBase E P) (p : P) : Finset E

Extension of predicate p relative to 𝔉. §7.3, eq (38): [T]_𝔉 = {a | a :_𝔉 T}.

Equations

• 𝔉.ext p = Finset.image Prod.fst ({x ∈ 𝔉.judgments | x.2 = p})

def Cooper2023Ch7.ExperienceBase.jointExt {E P : Type} [DecidableEq E] [DecidableEq P] (𝔉 : ExperienceBase E P) (p q : P) : Finset E

Joint extension: entities classified under both predicates.

Equations

• 𝔉.jointExt p q = 𝔉.ext p ∩ 𝔉.ext q

def Cooper2023Ch7.ExperienceBase.condProb {E P : Type} [DecidableEq E] [DecidableEq P] (𝔉 : ExperienceBase E P) (p q : P) : ℕ × ℕ

Frequentist conditional probability estimate (as numerator/denominator). §7.3, eq (36): p_𝔉(T₁‖T₂) = |[T₁∧T₂]_𝔉| / |[T₂]_𝔉|.

Equations

• 𝔉.condProb p q = ((𝔉.jointExt p q).card, (𝔉.ext q).card)

def Cooper2023Ch7.ExperienceBase.reliability {E P : Type} [DecidableEq E] [DecidableEq P] (𝔉 : ExperienceBase E P) (p q : P) : ℕ

Reliability of a probability estimate (count before log). §7.3, eq (40): reliability = ln min(|[T₁]_𝔉|, |[T₂]_𝔉|).

Equations

• 𝔉.reliability p q = min (𝔉.ext p).card (𝔉.ext q).card

§7.5 Long distance dependencies (eqs 114–158)

Cooper extends contexts with gap and wh-assignments to handle extraction, relative clauses, and wh-questions.

structure Cooper2023Ch7.CntxtWithGap (AssgnType CntxtType : Type) : Type

Context with gap assignment. §7.5: Cntxt = [𝔰, 𝔤, 𝔠] (the 3-field gap-aware context Cooper introduces around the slash-category discussion).

• 𝔰 : AssgnType
• 𝔤 : AssgnType
• 𝔠 : CntxtType

structure Cooper2023Ch7.CntxtFull (AssgnType CntxtType : Type) : Type

Full context with wh- and gap assignments. §7.5: Cntxt = [𝔰, 𝔴, 𝔤, 𝔠] (the 4-field context for wh-extraction; Cooper's Ch. 8 eq (10) extends this to the 5-field {q, 𝔰, 𝔴, 𝔤, 𝔠}).

• 𝔰 : AssgnType
• 𝔴 : AssgnType
• 𝔤 : AssgnType
• 𝔠 : CntxtType

structure Cooper2023Ch7.SlashCat : Type

Slash category: S/i is a sentence missing constituent at gap i. §7.5, eq (149): the TTR analogue of slash categories.

• mother : String
• gapIdx : ℕ

def Cooper2023Ch7.instDecidableEqSlashCat.decEq (x✝ x✝¹ : SlashCat) : Decidable (x✝ = x✝¹)

Equations

• Cooper2023Ch7.instDecidableEqSlashCat.decEq { mother := a, gapIdx := a_1 } { mother := b, gapIdx := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Cooper2023Ch7.instDecidableEqSlashCat : DecidableEq SlashCat

Equations

• Cooper2023Ch7.instDecidableEqSlashCat = Cooper2023Ch7.instDecidableEqSlashCat.decEq

def Cooper2023Ch7.instReprSlashCat.repr : SlashCat → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Cooper2023Ch7.instReprSlashCat : Repr SlashCat

Equations

• Cooper2023Ch7.instReprSlashCat = { reprPrec := Cooper2023Ch7.instReprSlashCat.repr }

structure Cooper2023Ch7.IsWhNP : Type

WhNP condition. §7.5, eq (149a): σ : WhNP iff σ : NP and Ω.bg ⊑ [𝔴:[xᵢ:Ind]] for some i.

• whIdx : ℕ

def Cooper2023Ch7.pptyConj {E : Type} (P₁ P₂ : Semantics.TypeTheoretic.Ppty E) : Semantics.TypeTheoretic.Ppty E

Property conjunction. §7.5, eq (153): P₁ & P₂ for relative clauses. "child who Sam hugged" = child ∧ hugged-by-Sam.

Equations

• Cooper2023Ch7.pptyConj P₁ P₂ x = (P₁ x × P₂ x)

theorem Cooper2023Ch7.pptyConj_nonempty {E : Type} (P₁ P₂ : Semantics.TypeTheoretic.Ppty E) (x : E) (h₁ : Nonempty (P₁ x)) (h₂ : Nonempty (P₂ x)) : Nonempty (pptyConj P₁ P₂ x)

Property conjunction preserves witnesses.

def Cooper2023Ch7.TypedPpty (T : Type) : Type 1

Type-indexed property: properties of objects of type T. §7.5, eq (152): P : ᵀPpty iff P.bg ⊑ [x:T].

Equations

• Cooper2023Ch7.TypedPpty T = (T → Type)

def Cooper2023Ch7.TypedPPpty (T : Type) : Type (u_1 + 1)

Type-indexed parametric property.

Equations

• Cooper2023Ch7.TypedPPpty T = Semantics.TypeTheoretic.Parametric (T → Type)

Phenomena

inductive Cooper2023Ch7.DogWorld : Type

Example: "a dog barks" (§7.4.1).

• fido : DogWorld
• rex : DogWorld
• spot : DogWorld
• luna : DogWorld

@[implicit_reducible]

instance Cooper2023Ch7.instDecidableEqDogWorld : DecidableEq DogWorld

Equations

• Cooper2023Ch7.instDecidableEqDogWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Cooper2023Ch7.instReprDogWorld : Repr DogWorld

Equations

• Cooper2023Ch7.instReprDogWorld = { reprPrec := Cooper2023Ch7.instReprDogWorld.repr }

def Cooper2023Ch7.instReprDogWorld.repr : DogWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Cooper2023Ch7.instFintypeDogWorld : Fintype DogWorld

Equations

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

def Cooper2023Ch7.isDog : DogWorld → Prop

Dog property.

Equations

• Cooper2023Ch7.isDog Cooper2023Ch7.DogWorld.fido = True
• Cooper2023Ch7.isDog Cooper2023Ch7.DogWorld.rex = True
• Cooper2023Ch7.isDog Cooper2023Ch7.DogWorld.spot = True
• Cooper2023Ch7.isDog Cooper2023Ch7.DogWorld.luna = False

@[implicit_reducible]

instance Cooper2023Ch7.instDecidablePredDogWorldIsDog : DecidablePred isDog

Equations

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

def Cooper2023Ch7.doesBark : DogWorld → Prop

Bark property.

Equations

• Cooper2023Ch7.doesBark Cooper2023Ch7.DogWorld.fido = True
• Cooper2023Ch7.doesBark Cooper2023Ch7.DogWorld.rex = False
• Cooper2023Ch7.doesBark Cooper2023Ch7.DogWorld.spot = True
• Cooper2023Ch7.doesBark Cooper2023Ch7.DogWorld.luna = False

@[implicit_reducible]

instance Cooper2023Ch7.instDecidablePredDogWorldDoesBark : DecidablePred doesBark

Equations

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

theorem Cooper2023Ch7.dog_ext_card : (Semantics.TypeTheoretic.fullExtFinset isDog).card = 3

The full extension of isDog is {fido, rex, spot}.

def Cooper2023Ch7.aDogBarks : Semantics.TypeTheoretic.ParticularWC_Exist (fun (x : DogWorld) => PLift (isDog x)) fun (x : DogWorld) => PLift (doesBark x)

Particular witness for "a dog barks": fido barks and is a dog.

Equations

• Cooper2023Ch7.aDogBarks = { x := Cooper2023Ch7.DogWorld.fido, pWit := { down := trivial }, qWit := { down := trivial } }

theorem Cooper2023Ch7.not_noDogBarks : ¬Semantics.TypeTheoretic.ParticularWC_No (fun (x : DogWorld) => PLift (isDog x)) fun (x : DogWorld) => PLift (doesBark x)

"No dog barks" fails: fido is a dog that barks.

theorem Cooper2023Ch7.few_has_compset : Semantics.TypeTheoretic.AnaphoraRef.compset ∈ Semantics.TypeTheoretic.anaphoraAvailable Semantics.TypeTheoretic.QuantName.few

few predicts COMPSET; a_few does not.

theorem Cooper2023Ch7.a_few_no_compset : Semantics.TypeTheoretic.AnaphoraRef.compset ∉ Semantics.TypeTheoretic.anaphoraAvailable Semantics.TypeTheoretic.QuantName.aFew

inductive Cooper2023Ch7.DogPred : Type

Predicate type for the dog example.

• dog : DogPred
• bark : DogPred

@[implicit_reducible]

instance Cooper2023Ch7.instDecidableEqDogPred : DecidableEq DogPred

Equations

• Cooper2023Ch7.instDecidableEqDogPred x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cooper2023Ch7.instReprDogPred.repr : DogPred → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cooper2023Ch7.instReprDogPred.repr Cooper2023Ch7.DogPred.dog prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cooper2023Ch7.DogPred.dog")).group prec✝

@[implicit_reducible]

instance Cooper2023Ch7.instReprDogPred : Repr DogPred

Equations

• Cooper2023Ch7.instReprDogPred = { reprPrec := Cooper2023Ch7.instReprDogPred.repr }

def Cooper2023Ch7.simpleExp : ExperienceBase DogWorld DogPred

Simple experience base: 3 dogs observed, 2 bark.

Equations

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

theorem Cooper2023Ch7.bark_given_dog_prob : simpleExp.condProb DogPred.bark DogPred.dog = (2, 3)

Two of three dogs bark: p(bark‖dog) = 2/3.

Structural theorems

Key theoretical claims of Ch 7, connecting witness-based quantification to classical GQ properties and each other.

Purification and donkey anaphora

Existential purification 𝔓 gives weak donkey readings; universal purification 𝔓ʸ gives strong donkey readings. For pure properties (trivial Bg), both collapse to identity.

theorem Cooper2023Ch7.purify_pure_equiv {E : Type} (P : Semantics.TypeTheoretic.PPpty E) (hPure : PPpty.isPure P) (a : E) : Nonempty (purify P a) ↔ Nonempty (P.fg ⋯.some a)

Purification of a pure property is equivalent to the original. §7.2.3: if P.Bg ≅ Unit, then 𝔓(P) ≃ P.fg.

theorem Cooper2023Ch7.purifyUniv_pure_equiv {E : Type} (P : Semantics.TypeTheoretic.PPpty E) (hPure : PPpty.isPure P) (a : E) : Nonempty (purifyUniv P a) ↔ Nonempty (P.fg ⋯.some a)

Universal purification of a pure property also collapses.

theorem Cooper2023Ch7.donkey_readings_agree_when_pure {E : Type} (P : Semantics.TypeTheoretic.PPpty E) (hPure : PPpty.isPure P) (a : E) : Nonempty (purify P a) ↔ Nonempty (purifyUniv P a)

For pure properties, weak and strong donkey readings agree. §7.2.3: the distinction only matters when Bg is non-trivial.

Record path subtraction (⊖) for LDD

§7.5, eq (118): T ⊖ π removes a field from a record type. This is the operation underlying gap-threading: a transitive verb type minus its object field yields the gap-containing type.

def Cooper2023Ch7.recSubtract (fields : List (String × Type)) (path : String) : List (String × Type)

Record path subtraction: remove a named field from a record. §7.5, eq (118): T ⊖ π removes field π from T. Encoded as filtering on a list of (label, type) pairs.

Equations

• Cooper2023Ch7.recSubtract fields path = List.filter (fun (p : String × Type) => decide (p.1 ≠ path)) fields

theorem Cooper2023Ch7.recSubtract_removes (fields : List (String × Type)) (path : String) (p : String × Type) : p ∈ recSubtract fields path → p.1 ≠ path

Subtraction removes exactly the targeted field.

theorem Cooper2023Ch7.recSubtract_preserves (fields : List (String × Type)) (path label : String) (h : label ≠ path) (p : String × Type) : p ∈ fields → p.1 = label → p ∈ recSubtract fields path

Subtraction preserves other fields.

Dependency families and generalization (T^π)

§7.5, eq (133): T^π = λv.[T ⊖ π ∧ {π : v}]. A dependency family abstracts over the gap, yielding a function from entities to record types. This is the TTR analogue of lambda-abstraction over a trace in transformational grammar.

def Cooper2023Ch7.dependencyFamily {E : Type} (body : E → Semantics.TypeTheoretic.Ppty E) : Semantics.TypeTheoretic.Ppty E → Type

Dependency family: abstract over a gap to get a property. §7.5, eq (133): T^π(v) fills gap π with v.

Equations

• Cooper2023Ch7.dependencyFamily body P = ((a : E) × body a a × P a)

def Cooper2023Ch7.depFamilyQuant {E : Type} (body : E → Semantics.TypeTheoretic.Ppty E) (q : Semantics.TypeTheoretic.Quant E) : Type

Merging a dependency family with a quantifier yields a scope-taking constituent. §7.5, eq (137): "which child Sam hugged" = Quant derived from T^π.

Equations

• Cooper2023Ch7.depFamilyQuant body q = q fun (x : E) => (a : E) × body a x