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

@cite{cooper-2023} @cite{barwise-cooper-1981} @cite{van-benthem-1984}

@cite{cooper-2023} Chapter 7 replaces classical set-theoretic GQ denotations (cf. Core.Quantification.GQ) with witness sets — finite sets of individuals satisfying cardinality conditions specific to each quantifier.

This study formalises Ch. 7 directly. It was formerly substrate at Theories/Semantics/TypeTheoretic/Quantification.lean but is genuinely a single-paper Cooper-textbook replication: only LuckingGinzburg2022 and Phenomena/Anaphora/Studies/Cooper2023 consume it externally, and both are themselves Cooper-2023-anchored discussions.

Key contributions:

• 𝔗(P): the type whose witnesses are P-individuals (§7.2.3)
• 𝔓/𝔓ʸ: purification operators extracting pure properties (§7.2.3)
• qʷ(P): witness set types per quantifier (§7.2.4)
• Austinian propositions (𝔉): probabilistic quantification (§7.3)
• General vs particular witness conditions: predict anaphora (§7.4)
• Complement witness sets: COMPSET anaphora for 'few' (§7.4)
• Contexts with gaps: long distance dependencies (§7.5)

§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 Phenomena.Quantification.Studies.Cooper2023.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

• Phenomena.Quantification.Studies.Cooper2023.PPpty.isPure P = (Nonempty P.Bg ∧ Subsingleton P.Bg)

def Phenomena.Quantification.Studies.Cooper2023.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

• Phenomena.Quantification.Studies.Cooper2023.WitnessType P = { a : E // Nonempty (P a) }

def Phenomena.Quantification.Studies.Cooper2023.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

• Phenomena.Quantification.Studies.Cooper2023.purify P a = ((c : P.Bg) × P.fg c a)

def Phenomena.Quantification.Studies.Cooper2023.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

• Phenomena.Quantification.Studies.Cooper2023.purifyUniv P a = ((c : P.Bg) → P.fg c a)

def Phenomena.Quantification.Studies.Cooper2023.term𝔓_ : Lean.ParserDescr

Notation for purification operators.

Equations

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

def Phenomena.Quantification.Studies.Cooper2023.«term𝔓ʸ_» : Lean.ParserDescr

Equations

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

theorem Phenomena.Quantification.Studies.Cooper2023.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 Phenomena.Quantification.Studies.Cooper2023.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 Phenomena.Quantification.Studies.Cooper2023.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 Phenomena.Quantification.Studies.Cooper2023.WitnessTypeP {E : Type} (P : Semantics.TypeTheoretic.PPpty E) : Type

WitnessType for parametric properties via purification.

Equations

• Phenomena.Quantification.Studies.Cooper2023.WitnessTypeP P = Phenomena.Quantification.Studies.Cooper2023.WitnessType (Phenomena.Quantification.Studies.Cooper2023.purify P)

§7.2.4 Types of witness sets for quantifiers (eqs 20–35)

Each quantifier q defines a type qʷ(P) of witness sets. X : qʷ(P) iff (1) X ⊆ extension of P, and (2) a cardinality condition.

All witness set types share a common subset condition (X ⊆ [↓P]). This structural requirement is what derives conservativity from the witness architecture — it's not stipulated as in @cite{barwise-cooper-1981}.

def Phenomena.Quantification.Studies.Cooper2023.fullExtFinset {E : Type} [Fintype E] (P : E → Prop) [DecidablePred P] : Finset E

Computable extension of P as a Finset. Cooper's [𝔗(P)] or [↓P].

Equations

• Phenomena.Quantification.Studies.Cooper2023.fullExtFinset P = Finset.filter P Finset.univ

structure Phenomena.Quantification.Studies.Cooper2023.WitnessSet {E : Type} (P : E → Prop) (X : Finset E) : Prop

Base witness set condition: X ⊆ extension of P. §7.2.4: every witness set type requires this.

• subset (a : E) : a ∈ X → P a

structure Phenomena.Quantification.Studies.Cooper2023.IsExistW {E : Type} (P : E → Prop) (X : Finset E) extends Phenomena.Quantification.Studies.Cooper2023.WitnessSet P X : Prop

existʷ(P): singleton witness set. Eq (21).

• subset (a : E) : a ∈ X → P a
• card_eq : X.card = 1

structure Phenomena.Quantification.Studies.Cooper2023.IsExistPlW {E : Type} (P : E → Prop) (X : Finset E) extends Phenomena.Quantification.Studies.Cooper2023.WitnessSet P X : Prop

exist_plʷ(P): plural some, |X| ≥ 2. Eq (22).

• subset (a : E) : a ∈ X → P a
• card_ge : X.card ≥ 2

def Phenomena.Quantification.Studies.Cooper2023.IsNoW {E : Type} (_P : E → Prop) (X : Finset E) : Prop

noʷ(P): empty set. Eqs (23–24).

Equations

• Phenomena.Quantification.Studies.Cooper2023.IsNoW _P X = (X = ∅)

def Phenomena.Quantification.Studies.Cooper2023.IsEveryW {E : Type} [Fintype E] (P : E → Prop) [DecidablePred P] (X : Finset E) : Prop

everyʷ(P): the full extension. Eqs (25–26).

Equations

• Phenomena.Quantification.Studies.Cooper2023.IsEveryW P X = (X = Phenomena.Quantification.Studies.Cooper2023.fullExtFinset P)

structure Phenomena.Quantification.Studies.Cooper2023.IsMostW {E : Type} [Fintype E] (P : E → Prop) [DecidablePred P] (θ_num θ_denom : ℕ) (X : Finset E) extends Phenomena.Quantification.Studies.Cooper2023.WitnessSet P X : Prop

mostʷ(P): proportional, |X|/|[↓P]| ≥ θ. Eq (29). Stated as cross-multiplication: X.card * denom ≥ num * ext.card.

• subset (a : E) : a ∈ X → P a
• extPos : (fullExtFinset P).card > 0
• proportion : X.card * θ_denom ≥ θ_num * (fullExtFinset P).card

structure Phenomena.Quantification.Studies.Cooper2023.IsManyAbsW {E : Type} (P : E → Prop) (θ : ℕ) (X : Finset E) extends Phenomena.Quantification.Studies.Cooper2023.WitnessSet P X : Prop

many_aʷ(P): absolute threshold, |X| ≥ θ. Eq (30).

• subset (a : E) : a ∈ X → P a
• card_ge : X.card ≥ θ

structure Phenomena.Quantification.Studies.Cooper2023.IsManyPropW {E : Type} [Fintype E] (P : E → Prop) [DecidablePred P] (θ_num θ_denom : ℕ) (X : Finset E) extends Phenomena.Quantification.Studies.Cooper2023.WitnessSet P X : Prop

many_pʷ(P): proportional, |X|/|[↓P]| ≥ θ. Eq (31).

• subset (a : E) : a ∈ X → P a
• extPos : (fullExtFinset P).card > 0
• proportion : X.card * θ_denom ≥ θ_num * (fullExtFinset P).card

structure Phenomena.Quantification.Studies.Cooper2023.IsFewAbsW {E : Type} (P : E → Prop) (θ : ℕ) (X : Finset E) extends Phenomena.Quantification.Studies.Cooper2023.WitnessSet P X : Prop

few_aʷ(P): absolute, |X| ≤ θ. Eq (32).

• subset (a : E) : a ∈ X → P a
• card_le : X.card ≤ θ

structure Phenomena.Quantification.Studies.Cooper2023.IsFewPropW {E : Type} [Fintype E] (P : E → Prop) [DecidablePred P] (θ_num θ_denom : ℕ) (X : Finset E) extends Phenomena.Quantification.Studies.Cooper2023.WitnessSet P X : Prop

few_pʷ(P): proportional, |X|/|[↓P]| ≤ θ. Eq (33).

• subset (a : E) : a ∈ X → P a
• extPos : (fullExtFinset P).card > 0
• proportion : X.card * θ_denom ≤ θ_num * (fullExtFinset P).card

structure Phenomena.Quantification.Studies.Cooper2023.IsAFewAbsW {E : Type} (P : E → Prop) (θ : ℕ) (X : Finset E) extends Phenomena.Quantification.Studies.Cooper2023.WitnessSet P X : Prop

a_few_aʷ(P): absolute, |X| ≥ θ (same threshold as few, reversed direction). Eq (34).

• subset (a : E) : a ∈ X → P a
• card_ge : X.card ≥ θ

structure Phenomena.Quantification.Studies.Cooper2023.IsAFewPropW {E : Type} [Fintype E] (P : E → Prop) [DecidablePred P] (θ_num θ_denom : ℕ) (X : Finset E) extends Phenomena.Quantification.Studies.Cooper2023.WitnessSet P X : Prop

a_few_pʷ(P): proportional, |X|/|[↓P]| ≥ θ. Eq (35).

• subset (a : E) : a ∈ X → P a
• extPos : (fullExtFinset P).card > 0
• proportion : X.card * θ_denom ≥ θ_num * (fullExtFinset P).card

structure Phenomena.Quantification.Studies.Cooper2023.IsCompFewAbsW {E : Type} [Fintype E] (P : E → Prop) [DecidablePred P] (θ : ℕ) (X : Finset E) extends Phenomena.Quantification.Studies.Cooper2023.WitnessSet P X : Prop

Complement witness set for few (absolute). Eq (81). X̄ : few̄ʷ_a(P) iff |X| ≥ |[𝔗(P)]| − θ. Predicts COMPSET anaphora.

• subset (a : E) : a ∈ X → P a
• card_ge : X.card ≥ (fullExtFinset P).card - θ

structure Phenomena.Quantification.Studies.Cooper2023.IsCompFewPropW {E : Type} [Fintype E] (P : E → Prop) [DecidablePred P] (θ_num θ_denom : ℕ) (X : Finset E) extends Phenomena.Quantification.Studies.Cooper2023.WitnessSet P X : Prop

Complement witness set for few (proportional). Eq (82).

• subset (a : E) : a ∈ X → P a
• extPos : (fullExtFinset P).card > 0
• proportion : X.card * θ_denom ≥ (θ_denom - θ_num) * (fullExtFinset P).card

theorem Phenomena.Quantification.Studies.Cooper2023.isNoW_iff_empty {E : Type} (P : E → Prop) (X : Finset E) : IsNoW P X ↔ X = ∅

noʷ has exactly one witness set: ∅.

theorem Phenomena.Quantification.Studies.Cooper2023.isEveryW_iff {E : Type} [DecidableEq E] [Fintype E] (P : E → Prop) [DecidablePred P] (X : Finset E) : IsEveryW P X ↔ X = fullExtFinset P

everyʷ has exactly one witness set: the full extension.

§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 Phenomena.Quantification.Studies.Cooper2023.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 Phenomena.Quantification.Studies.Cooper2023.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 Phenomena.Quantification.Studies.Cooper2023.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 Phenomena.Quantification.Studies.Cooper2023.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 Phenomena.Quantification.Studies.Cooper2023.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.4 Witness conditions for quantificational ptypes (eqs 59–90)

The central theoretical contribution: how quantifiers evaluate. Each q(P,Q) is witnessed by a pair (X, f) where X is a witness set and f maps witnesses to Q-evidence.

Two patterns:

• General (eq 59): for all quantifiers, uses purified Q
• Particular (eq 63): simpler, only for some quantifiers, better anaphora predictions

structure Phenomena.Quantification.Studies.Cooper2023.GeneralWC_Incr {E : Type} (P Q : Semantics.TypeTheoretic.Ppty E) (isWS : Finset E → Prop) [DecidableEq E] : Type

General witness condition for monotone ↑ quantifiers. §7.4, eq (59a): s : q(P,Q) iff s : [X : qʷ(P), f : (a : 𝔗(X)) → 𝔓(Q){a}] Each member of X must individually witness Q.

• X : Finset E
• witnessOK : isWS self.X
• f (a : E) : a ∈ self.X → Q a

structure Phenomena.Quantification.Studies.Cooper2023.GeneralWC_Decr {E : Type} (P Q : Semantics.TypeTheoretic.Ppty E) (isWS : Finset E → Prop) [DecidableEq E] : Type

General witness condition for monotone ↓ quantifiers. §7.4, eq (59b): Every entity with both P and Q lands in X.

• X : Finset E
• witnessOK : isWS self.X
• f (a : E) : Nonempty (P a) → Nonempty (Q a) → a ∈ self.X

structure Phenomena.Quantification.Studies.Cooper2023.ParticularWC_Exist {E : Type} (P Q : Semantics.TypeTheoretic.Ppty E) : Type

Particular witness condition for exist(P,Q). Eq (63). s : exist(P,Q) iff s : [x : 𝔗(P), e : 𝔓(Q){x}] The x-field enables REFSET (singular) anaphora: "A dog barked. It heard an intruder."

• x : E
• pWit : P self.x
• qWit : Q self.x

structure Phenomena.Quantification.Studies.Cooper2023.ParticularWC_No {E : Type} (P Q : Semantics.TypeTheoretic.Ppty E) : Prop

Particular witness condition for no(P,Q). Eq (70). Every P-entity fails to have Q (type negation). everyʷ(P) as witness set predicts MAXSET anaphora: "No dog barked. They (= the dogs) were all asleep."

• f (a : E) : ∀ (a✝ : P a), IsEmpty (Q a)

structure Phenomena.Quantification.Studies.Cooper2023.ParticularWC_FewComp {E : Type} (P Q : Semantics.TypeTheoretic.Ppty E) [DecidableEq E] : Type

Particular witness condition for few with complement. Eqs (85–86). Uses complement witness set: P-entities lacking Q. Predicts COMPSET anaphora: "Few dogs barked. They (= non-barking dogs) slept through."

• X : Finset E
• allP (a : E) : a ∈ self.X → Nonempty (P a)
• allNotQ (a : E) : a ∈ self.X → IsEmpty (Q a)

def Phenomena.Quantification.Studies.Cooper2023.particular_exist_implies_general {E : Type} [DecidableEq E] (P Q : Semantics.TypeTheoretic.Ppty E) (h : ParticularWC_Exist P Q) (Pd : E → Prop) (hPd : ∀ (a : E), Pd a ↔ Nonempty (P a)) : GeneralWC_Incr P Q (IsExistW Pd)

The particular exist condition implies the general one (with singleton X). §7.4: the particular condition "provides a component in the witness (in the 'x'-field) which can be picked up on by singular anaphora."

Equations

• Phenomena.Quantification.Studies.Cooper2023.particular_exist_implies_general P Q h Pd hPd = { X := {h.x}, witnessOK := ⋯, f := fun (a : E) (ha : a ∈ {h.x}) => ⋯.mpr h.qWit }

inductive Phenomena.Quantification.Studies.Cooper2023.AnaphoraRef : Type

Anaphora set predictions per quantifier. §7.4.1: witness structure determines available anaphora.

• refset : AnaphoraRef

  REFSET: reference to the witness individual/set. "A dog barked. It (= that dog) heard an intruder."

• maxset : AnaphoraRef

  MAXSET: reference to the full extension. "Every dog barked. They (= the dogs) heard an intruder."

• compset : AnaphoraRef

  COMPSET: reference to the complement witness set (for few). "Few dogs barked. They (= the non-barking dogs) slept through."

@[implicit_reducible]

instance Phenomena.Quantification.Studies.Cooper2023.instDecidableEqAnaphoraRef : DecidableEq AnaphoraRef

Equations

• Phenomena.Quantification.Studies.Cooper2023.instDecidableEqAnaphoraRef x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Quantification.Studies.Cooper2023.instReprAnaphoraRef.repr : AnaphoraRef → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Quantification.Studies.Cooper2023.instReprAnaphoraRef : Repr AnaphoraRef

Equations

• Phenomena.Quantification.Studies.Cooper2023.instReprAnaphoraRef = { reprPrec := Phenomena.Quantification.Studies.Cooper2023.instReprAnaphoraRef.repr }

inductive Phenomena.Quantification.Studies.Cooper2023.QuantName : Type

Quantifier names for typed dispatch. §7.4.1: the quantifiers of the English fragment.

• exist : QuantName
• existPl : QuantName
• no : QuantName
• every : QuantName
• most : QuantName
• many : QuantName
• few : QuantName
• aFew : QuantName

@[implicit_reducible]

instance Phenomena.Quantification.Studies.Cooper2023.instDecidableEqQuantName : DecidableEq QuantName

Equations

• Phenomena.Quantification.Studies.Cooper2023.instDecidableEqQuantName x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Quantification.Studies.Cooper2023.instReprQuantName.repr : QuantName → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Quantification.Studies.Cooper2023.instReprQuantName : Repr QuantName

Equations

• Phenomena.Quantification.Studies.Cooper2023.instReprQuantName = { reprPrec := Phenomena.Quantification.Studies.Cooper2023.instReprQuantName.repr }

def Phenomena.Quantification.Studies.Cooper2023.anaphoraAvailable : QuantName → List AnaphoraRef

Which anaphora sets each quantifier makes available. §7.4.1: summary table.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Quantification.Studies.Cooper2023.anaphoraAvailable Phenomena.Quantification.Studies.Cooper2023.QuantName.exist = [Phenomena.Quantification.Studies.Cooper2023.AnaphoraRef.refset]
• Phenomena.Quantification.Studies.Cooper2023.anaphoraAvailable Phenomena.Quantification.Studies.Cooper2023.QuantName.no = [Phenomena.Quantification.Studies.Cooper2023.AnaphoraRef.maxset]
• Phenomena.Quantification.Studies.Cooper2023.anaphoraAvailable Phenomena.Quantification.Studies.Cooper2023.QuantName.every = [Phenomena.Quantification.Studies.Cooper2023.AnaphoraRef.maxset]
• Phenomena.Quantification.Studies.Cooper2023.anaphoraAvailable Phenomena.Quantification.Studies.Cooper2023.QuantName.most = [Phenomena.Quantification.Studies.Cooper2023.AnaphoraRef.maxset]
• Phenomena.Quantification.Studies.Cooper2023.anaphoraAvailable Phenomena.Quantification.Studies.Cooper2023.QuantName.many = [Phenomena.Quantification.Studies.Cooper2023.AnaphoraRef.maxset]

§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 Phenomena.Quantification.Studies.Cooper2023.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 Phenomena.Quantification.Studies.Cooper2023.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 Phenomena.Quantification.Studies.Cooper2023.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 : ℕ

@[implicit_reducible]

instance Phenomena.Quantification.Studies.Cooper2023.instDecidableEqSlashCat : DecidableEq SlashCat

Equations

• Phenomena.Quantification.Studies.Cooper2023.instDecidableEqSlashCat = Phenomena.Quantification.Studies.Cooper2023.instDecidableEqSlashCat.decEq

def Phenomena.Quantification.Studies.Cooper2023.instDecidableEqSlashCat.decEq (x✝ x✝¹ : SlashCat) : Decidable (x✝ = x✝¹)

Equations

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

def Phenomena.Quantification.Studies.Cooper2023.instReprSlashCat.repr : SlashCat → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Quantification.Studies.Cooper2023.instReprSlashCat : Repr SlashCat

Equations

• Phenomena.Quantification.Studies.Cooper2023.instReprSlashCat = { reprPrec := Phenomena.Quantification.Studies.Cooper2023.instReprSlashCat.repr }

structure Phenomena.Quantification.Studies.Cooper2023.IsWhNP : Type

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

• whIdx : ℕ

def Phenomena.Quantification.Studies.Cooper2023.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

• Phenomena.Quantification.Studies.Cooper2023.pptyConj P₁ P₂ x = (P₁ x × P₂ x)

theorem Phenomena.Quantification.Studies.Cooper2023.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 Phenomena.Quantification.Studies.Cooper2023.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

• Phenomena.Quantification.Studies.Cooper2023.TypedPpty T = (T → Type)

def Phenomena.Quantification.Studies.Cooper2023.TypedPPpty (T : Type) : Type (u_1 + 1)

Type-indexed parametric property.

Equations

• Phenomena.Quantification.Studies.Cooper2023.TypedPPpty T = Semantics.TypeTheoretic.Parametric (T → Type)

Phenomena

inductive Phenomena.Quantification.Studies.Cooper2023.DogWorld : Type

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

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

@[implicit_reducible]

instance Phenomena.Quantification.Studies.Cooper2023.instDecidableEqDogWorld : DecidableEq DogWorld

Equations

• Phenomena.Quantification.Studies.Cooper2023.instDecidableEqDogWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Quantification.Studies.Cooper2023.instReprDogWorld.repr : DogWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Quantification.Studies.Cooper2023.instReprDogWorld : Repr DogWorld

Equations

• Phenomena.Quantification.Studies.Cooper2023.instReprDogWorld = { reprPrec := Phenomena.Quantification.Studies.Cooper2023.instReprDogWorld.repr }

@[implicit_reducible]

instance Phenomena.Quantification.Studies.Cooper2023.instFintypeDogWorld : Fintype DogWorld

Equations

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

def Phenomena.Quantification.Studies.Cooper2023.isDog : DogWorld → Prop

Dog property.

Equations

• Phenomena.Quantification.Studies.Cooper2023.isDog Phenomena.Quantification.Studies.Cooper2023.DogWorld.fido = True
• Phenomena.Quantification.Studies.Cooper2023.isDog Phenomena.Quantification.Studies.Cooper2023.DogWorld.rex = True
• Phenomena.Quantification.Studies.Cooper2023.isDog Phenomena.Quantification.Studies.Cooper2023.DogWorld.spot = True
• Phenomena.Quantification.Studies.Cooper2023.isDog Phenomena.Quantification.Studies.Cooper2023.DogWorld.luna = False

@[implicit_reducible]

instance Phenomena.Quantification.Studies.Cooper2023.instDecidablePredDogWorldIsDog : DecidablePred isDog

Equations

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

def Phenomena.Quantification.Studies.Cooper2023.doesBark : DogWorld → Prop

Bark property.

Equations

• Phenomena.Quantification.Studies.Cooper2023.doesBark Phenomena.Quantification.Studies.Cooper2023.DogWorld.fido = True
• Phenomena.Quantification.Studies.Cooper2023.doesBark Phenomena.Quantification.Studies.Cooper2023.DogWorld.rex = False
• Phenomena.Quantification.Studies.Cooper2023.doesBark Phenomena.Quantification.Studies.Cooper2023.DogWorld.spot = True
• Phenomena.Quantification.Studies.Cooper2023.doesBark Phenomena.Quantification.Studies.Cooper2023.DogWorld.luna = False

@[implicit_reducible]

instance Phenomena.Quantification.Studies.Cooper2023.instDecidablePredDogWorldDoesBark : DecidablePred doesBark

Equations

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

theorem Phenomena.Quantification.Studies.Cooper2023.dog_ext_card : (fullExtFinset isDog).card = 3

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

def Phenomena.Quantification.Studies.Cooper2023.aDogBarks : 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

• Phenomena.Quantification.Studies.Cooper2023.aDogBarks = { x := Phenomena.Quantification.Studies.Cooper2023.DogWorld.fido, pWit := { down := trivial }, qWit := { down := trivial } }

theorem Phenomena.Quantification.Studies.Cooper2023.not_noDogBarks : ¬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 Phenomena.Quantification.Studies.Cooper2023.few_has_compset : AnaphoraRef.compset ∈ anaphoraAvailable QuantName.few

few predicts COMPSET; a_few does not.

theorem Phenomena.Quantification.Studies.Cooper2023.a_few_no_compset : AnaphoraRef.compset ∉ anaphoraAvailable QuantName.aFew

inductive Phenomena.Quantification.Studies.Cooper2023.DogPred : Type

Predicate type for the dog example.

• dog : DogPred
• bark : DogPred

@[implicit_reducible]

instance Phenomena.Quantification.Studies.Cooper2023.instDecidableEqDogPred : DecidableEq DogPred

Equations

• Phenomena.Quantification.Studies.Cooper2023.instDecidableEqDogPred x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Quantification.Studies.Cooper2023.instReprDogPred.repr : DogPred → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Quantification.Studies.Cooper2023.instReprDogPred : Repr DogPred

Equations

• Phenomena.Quantification.Studies.Cooper2023.instReprDogPred = { reprPrec := Phenomena.Quantification.Studies.Cooper2023.instReprDogPred.repr }

def Phenomena.Quantification.Studies.Cooper2023.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 Phenomena.Quantification.Studies.Cooper2023.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.

Bridge: witness-based → GQ

Every witness set type induces a classical GQ by existentially quantifying over witness sets. This is the fundamental connection between Cooper's type-theoretic quantifiers and Barwise & Cooper's set-theoretic ones.

def Phenomena.Quantification.Studies.Cooper2023.witnessGQ_exist {E : Type} : Core.Quantification.GQ E

The GQ induced by existential witness sets. exist(A,B) iff some element satisfies both A and B.

Equations

• Phenomena.Quantification.Studies.Cooper2023.witnessGQ_exist A B = ∃ (x : E), A x ∧ B x

def Phenomena.Quantification.Studies.Cooper2023.witnessGQ_every {E : Type} : Core.Quantification.GQ E

The GQ induced by universal witness sets. every(A,B) iff every A-element also satisfies B.

Equations

• Phenomena.Quantification.Studies.Cooper2023.witnessGQ_every A B = ∀ (x : E), A x → B x

Conservativity from witness structure

All witness set types require X ⊆ [↓P] (the subset condition). This structurally entails conservativity: q(P,Q) depends only on P ∩ Q, never on Q outside P. §7.2.4.

This is significant because conservativity is stipulated as an axiom in @cite{barwise-cooper-1981} but derived from the witness architecture.

theorem Phenomena.Quantification.Studies.Cooper2023.witnessGQ_exist_conservative {E : Type} : Core.Quantification.Conservative witnessGQ_exist

Conservativity of witnessGQ_exist: follows from the subset condition in IsExistW. Cooper's key argument: conservativity is structural, not stipulated.

theorem Phenomena.Quantification.Studies.Cooper2023.witnessGQ_every_conservative {E : Type} : Core.Quantification.Conservative witnessGQ_every

Conservativity of witnessGQ_every.

Bridge: witness quantification ↔ extensional truth

Cooper's witness-based quantifiers (type-theoretic) compute the same truth values as the extensional denotations in Semantics.Montague/Quantifier. This bridges the three layers of quantification: Core.Quantification (logical properties) ← proved via conservativity above Semantics.Montague (extensional denotations) ← proved via equivalence below TTR (witness-based) ← definitions above

theorem Phenomena.Quantification.Studies.Cooper2023.particular_exist_iff_witnessGQ {E : Type} (P Q : E → Prop) : (∃ (x : E), P x ∧ Q x) ↔ witnessGQ_exist P Q

TTR's structured particular witness condition is equivalent to the existential GQ being true. This is the key grounding theorem: ParticularWC_Exist P Q is inhabited iff witnessGQ_exist holds.

theorem Phenomena.Quantification.Studies.Cooper2023.universal_iff_witnessGQ {E : Type} (P Q : E → Prop) : (∀ (x : E), P x → Q x) ↔ witnessGQ_every P Q

The universal condition is equivalent to the universal GQ being true.

theorem Phenomena.Quantification.Studies.Cooper2023.particularWC_to_witnessGQ {E : Type} [DecidableEq E] {P Q : Semantics.TypeTheoretic.Ppty E} (w : ParticularWC_Exist P Q) (Pd Qd : E → Prop) (hP : ∀ (a : E), Pd a ↔ Nonempty (P a)) (hQ : ∀ (a : E), Qd a ↔ Nonempty (Q a)) : witnessGQ_exist Pd Qd

TTR's ParticularWC_Exist gives a constructive witness for the existential GQ.

theorem Phenomena.Quantification.Studies.Cooper2023.particularWC_no_to_witnessGQ {E : Type} [DecidableEq E] {P Q : Semantics.TypeTheoretic.Ppty E} (w : ParticularWC_No P Q) (Pd Qd : E → Prop) (hP : ∀ (a : E), Pd a ↔ Nonempty (P a)) (hQ : ∀ (a : E), Qd a ↔ Nonempty (Q a)) : witnessGQ_every Pd fun (x : E) => ¬Qd x

TTR's ParticularWC_No implies the universal GQ with negated scope.

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 Phenomena.Quantification.Studies.Cooper2023.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 Phenomena.Quantification.Studies.Cooper2023.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 Phenomena.Quantification.Studies.Cooper2023.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.

Particular → general witness condition lifting

Each particular witness condition implies the corresponding general one. The particular conditions are preferred because they expose finer-grained structure for anaphora resolution.

def Phenomena.Quantification.Studies.Cooper2023.particular_no_implies_general {E : Type} [DecidableEq E] (P Q : Semantics.TypeTheoretic.Ppty E) (h : ParticularWC_No P Q) (Pd : E → Prop) : GeneralWC_Decr P Q (IsNoW Pd)

Particular no implies general (decreasing) no. §7.4, eqs (70) → (59b): if every P-entity lacks Q, then the empty witness set satisfies the decreasing condition (vacuously: no entity has both P and Q).

Equations

• Phenomena.Quantification.Studies.Cooper2023.particular_no_implies_general P Q h Pd = { X := ∅, witnessOK := ⋯, f := ⋯ }

Complement witness sets and the few/a_few contrast

Cooper's key empirical claim (§7.4.2): few and a_few share the same cardinality threshold but differ in anaphora predictions because few (downward monotone) supports complement witness sets while a_few (upward monotone) does not.

• "Few dogs barked. They slept through." → they = non-barking dogs (COMPSET)
• "A few dogs barked. They heard the noise." → they = barking dogs (REFSET)

theorem Phenomena.Quantification.Studies.Cooper2023.comp_witness_card {E : Type} [DecidableEq E] [Fintype E] (P : E → Prop) [DecidablePred P] (X : Finset E) (_hSub : ∀ a ∈ X, P a) (θ : ℕ) (hFew : X.card ≤ θ) (hXsub : X ⊆ fullExtFinset P) : (fullExtFinset P \ X).card ≥ (fullExtFinset P).card - θ

The complement witness set for few satisfies the complement cardinality condition. §7.4.2, eq (81): X̄ = 𝔗(P) \ X.

theorem Phenomena.Quantification.Studies.Cooper2023.few_comp_partition {E : Type} [DecidableEq E] [Fintype E] (P : E → Prop) [DecidablePred P] (X : Finset E) (hX : X ⊆ fullExtFinset P) : X ∪ fullExtFinset P \ X = fullExtFinset P

few_a and its complement partition the full extension. §7.4.2: X ∪ X̄ = 𝔗(P).

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 Phenomena.Quantification.Studies.Cooper2023.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

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

theorem Phenomena.Quantification.Studies.Cooper2023.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 Phenomena.Quantification.Studies.Cooper2023.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 Phenomena.Quantification.Studies.Cooper2023.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

• Phenomena.Quantification.Studies.Cooper2023.dependencyFamily body P = ((a : E) × body a a × P a)

def Phenomena.Quantification.Studies.Cooper2023.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

• Phenomena.Quantification.Studies.Cooper2023.depFamilyQuant body q = q fun (x : E) => (a : E) × body a x

Monotonicity from witness conditions

§7.4: the general witness condition for ↑ quantifiers (59a) uses existential evidence per witness (f maps each to Q-evidence), while ↓ quantifiers (59b) use universal containment (every P∧Q entity is in X). This structural difference predicts monotonicity direction.

def Phenomena.Quantification.Studies.Cooper2023.generalWC_incr_mono {E : Type} [DecidableEq E] (P Q Q' : Semantics.TypeTheoretic.Ppty E) (isWS : Finset E → Prop) (embed : (a : E) → Q a → Q' a) (w : GeneralWC_Incr P Q isWS) : GeneralWC_Incr P Q' isWS

Upward monotonicity of the increasing witness condition: if Q ⊆ Q' (at Type level), any witness for Q also witnesses Q'. §7.4, consequence of (59a).

Equations

• Phenomena.Quantification.Studies.Cooper2023.generalWC_incr_mono P Q Q' isWS embed w = { X := w.X, witnessOK := ⋯, f := fun (a : E) (ha : a ∈ w.X) => embed a (w.f a ha) }

def Phenomena.Quantification.Studies.Cooper2023.generalWC_decr_mono {E : Type} [DecidableEq E] (P Q Q' : Semantics.TypeTheoretic.Ppty E) (isWS : Finset E → Prop) (embed : (a : E) → Q' a → Q a) (w : GeneralWC_Decr P Q isWS) : GeneralWC_Decr P Q' isWS

Downward monotonicity of the decreasing witness condition: if Q' ⊆ Q, then the decreasing condition on Q implies it on Q'. §7.4, consequence of (59b).

Equations

• Phenomena.Quantification.Studies.Cooper2023.generalWC_decr_mono P Q Q' isWS embed w = { X := w.X, witnessOK := ⋯, f := ⋯ }