Witness-set quantification

[Coo23] [BC81]

Witness-set semantics for natural-language quantifiers: a quantifier q(P, Q) is witnessed by a finite set X of P-individuals satisfying a quantifier-specific cardinality condition, together with evidence that each member of X (or alternatively each member outside X) bears Q. The architecture descends from [BC81]'s notion of witness sets, formulated as type-theoretic predicates in [Coo23] Ch. 7.

This file extracts the framework as reusable substrate. It is consumed by Studies.Cooper2023.Ch7 (Cooper's own deployment) and Studies.LuckingGinzburg2022 (the Referential Transparency Theory of quantification, which uses witness sets as a comparator for its refset/compset/maxset framework).

Main definitions

• WitnessSet P X — the base condition X ⊆ ext(P) shared by all quantifier-specific witness types. Structural conservativity follows.
• IsExistW, IsNoW, IsEveryW, IsMostW, IsManyAbsW, IsManyPropW, IsFewAbsW, IsFewPropW, IsAFewAbsW, IsAFewPropW, IsCompFewAbsW, IsCompFewPropW — quantifier-specific witness-set conditions.
• GeneralWC_Incr, GeneralWC_Decr — general witness conditions parameterised by an isWS predicate (monotone-increasing / monotone-decreasing forms).
• ParticularWC_Exist, ParticularWC_No, ParticularWC_FewComp — particular (anaphora-exposing) witness conditions.
• AnaphoraRef, QuantName, anaphoraAvailable — per-quantifier anaphora-set predictions (REFSET / MAXSET / COMPSET).
• witnessGQ_exist, witnessGQ_every — induced classical generalised-quantifier denotations.

Main statements

• witnessGQ_exist_conservative, witnessGQ_every_conservative — conservativity follows structurally from the WitnessSet subset condition, rather than being stipulated as in [BC81].
• particular_exist_iff_witnessGQ, universal_iff_witnessGQ, particularWC_to_witnessGQ, particularWC_no_to_witnessGQ — bridges between particular witness conditions and the classical GQ denotations.
• particular_exist_implies_general, particular_no_implies_general — every particular condition implies the matching general one.
• comp_witness_card, few_comp_partition — complement-witness-set combinatorics underpinning COMPSET anaphora.
• generalWC_incr_mono, generalWC_decr_mono — monotonicity of the general witness conditions follows from their structural shape.

Implementation notes

• All witness-set predicates take a DecidablePred P : E → Prop rather than a Ppty E := E → Type. This matches [BC81]'s set-theoretic formulation and lets Lean's decide close finite cardinality goals. Ppty-shaped witness conditions (ParticularWC_*, GeneralWC_*) coexist for the Type-valued TTR predicates used in compositional semantics.
• Anaphora-availability is encoded as a finite enumeration (anaphoraAvailable : QuantName → List AnaphoraRef) rather than a derived predicate. The list is empirical (Cooper §7.4.1 Table); the Lean encoding is for downstream decide-based dispatch.

Extension of a predicate as a Finset

def Semantics.TypeTheoretic.fullExtFinset {E : Type} [Fintype E] (P : E → Prop) [DecidablePred P] : Finset E

The extension [↓P] of a predicate P as a Finset.

Equations

• Semantics.TypeTheoretic.fullExtFinset P = Finset.filter P Finset.univ

Witness-set predicates

structure Semantics.TypeTheoretic.WitnessSet {E : Type} (P : E → Prop) (X : Finset E) : Prop

Base witness-set condition ([BC81]): a witness set for P is a subset of [↓P]. Every quantifier-specific witness type extends this condition.

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

structure Semantics.TypeTheoretic.IsExistW {E : Type} (P : E → Prop) (X : Finset E) extends Semantics.TypeTheoretic.WitnessSet P X : Prop

existʷ(P): a singleton witness set.

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

structure Semantics.TypeTheoretic.IsExistPlW {E : Type} (P : E → Prop) (X : Finset E) extends Semantics.TypeTheoretic.WitnessSet P X : Prop

exist_plʷ(P): a plural-some witness set, |X| ≥ 2.

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

def Semantics.TypeTheoretic.IsNoW {E : Type} (_P : E → Prop) (X : Finset E) : Prop

noʷ(P): the empty witness set.

Equations

• Semantics.TypeTheoretic.IsNoW _P X = (X = ∅)

def Semantics.TypeTheoretic.IsEveryW {E : Type} [Fintype E] (P : E → Prop) [DecidablePred P] (X : Finset E) : Prop

everyʷ(P): the full extension.

Equations

• Semantics.TypeTheoretic.IsEveryW P X = (X = Semantics.TypeTheoretic.fullExtFinset P)

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

mostʷ(P): proportional, |X| / |[↓P]| ≥ θ_num / θ_denom. Stated as cross-multiplication.

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

structure Semantics.TypeTheoretic.IsManyAbsW {E : Type} (P : E → Prop) (θ : ℕ) (X : Finset E) extends Semantics.TypeTheoretic.WitnessSet P X : Prop

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

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

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

many_pʷ(P): proportional threshold.

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

structure Semantics.TypeTheoretic.IsFewAbsW {E : Type} (P : E → Prop) (θ : ℕ) (X : Finset E) extends Semantics.TypeTheoretic.WitnessSet P X : Prop

few_aʷ(P): absolute upper bound, |X| ≤ θ.

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

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

few_pʷ(P): proportional upper bound.

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

structure Semantics.TypeTheoretic.IsAFewAbsW {E : Type} (P : E → Prop) (θ : ℕ) (X : Finset E) extends Semantics.TypeTheoretic.WitnessSet P X : Prop

a_few_aʷ(P): absolute lower bound (same threshold as few_a, reversed direction).

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

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

a_few_pʷ(P): proportional lower bound.

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

structure Semantics.TypeTheoretic.IsCompFewAbsW {E : Type} [Fintype E] (P : E → Prop) [DecidablePred P] (θ : ℕ) (X : Finset E) extends Semantics.TypeTheoretic.WitnessSet P X : Prop

Complement witness set for few (absolute): 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 Semantics.TypeTheoretic.IsCompFewPropW {E : Type} [Fintype E] (P : E → Prop) [DecidablePred P] (θ_num θ_denom : ℕ) (X : Finset E) extends Semantics.TypeTheoretic.WitnessSet P X : Prop

Complement witness set for few (proportional).

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

theorem Semantics.TypeTheoretic.isNoW_iff_empty {E : Type} (P : E → Prop) (X : Finset E) : IsNoW P X ↔ X = ∅

noʷ has exactly one witness set: ∅.

theorem Semantics.TypeTheoretic.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.

General and particular witness conditions

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

General witness condition for monotone-increasing quantifiers ([Coo23] §7.4): a witness set X plus a per-element mapping into Q-evidence.

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

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

General witness condition for monotone-decreasing quantifiers: a witness set X plus universal containment of P ∩ Q-entities in X.

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

structure Semantics.TypeTheoretic.ParticularWC_Exist {E : Type} (P Q : Ppty E) : Type

Particular witness condition for exist(P, Q): a specific individual x witnessing both P and Q. 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 Semantics.TypeTheoretic.ParticularWC_No {E : Type} (P Q : Ppty E) : Prop

Particular witness condition for no(P, Q): every P-entity fails to bear Q. With everyʷ(P) as the witness set, predicts MAXSET anaphora ("No dog barked. They were all asleep.").

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

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

Particular witness condition for few with complement: a set of P-entities all lacking Q. Predicts COMPSET anaphora ("Few dogs barked. They slept through.").

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

def Semantics.TypeTheoretic.particular_exist_implies_general {E : Type} [DecidableEq E] (P Q : 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 a singleton witness set.

Equations

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

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

The particular no condition implies the general decreasing one with the empty witness set.

Equations

• Semantics.TypeTheoretic.particular_no_implies_general P Q h Pd = { X := ∅, witnessOK := ⋯, f := ⋯ }

Anaphora-set predictions

The witness-set architecture predicts which anaphora sets each quantifier makes available ([Coo23] §7.4.1, Table).

inductive Semantics.TypeTheoretic.AnaphoraRef : Type

Anaphora-set kinds reachable from a quantified noun phrase.

• refset : AnaphoraRef

  REFSET: the witness individual or set ("A dog barked. It heard an intruder.").

• maxset : AnaphoraRef

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

• compset : AnaphoraRef

  COMPSET: the complement witness set ("Few dogs barked. They slept through.").

@[implicit_reducible]

instance Semantics.TypeTheoretic.instDecidableEqAnaphoraRef : DecidableEq AnaphoraRef

Equations

• Semantics.TypeTheoretic.instDecidableEqAnaphoraRef x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.TypeTheoretic.instReprAnaphoraRef.repr : AnaphoraRef → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.TypeTheoretic.instReprAnaphoraRef : Repr AnaphoraRef

Equations

• Semantics.TypeTheoretic.instReprAnaphoraRef = { reprPrec := Semantics.TypeTheoretic.instReprAnaphoraRef.repr }

inductive Semantics.TypeTheoretic.QuantName : Type

The English fragment's quantifier names.

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

@[implicit_reducible]

instance Semantics.TypeTheoretic.instDecidableEqQuantName : DecidableEq QuantName

Equations

• Semantics.TypeTheoretic.instDecidableEqQuantName x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.TypeTheoretic.instReprQuantName : Repr QuantName

Equations

• Semantics.TypeTheoretic.instReprQuantName = { reprPrec := Semantics.TypeTheoretic.instReprQuantName.repr }

def Semantics.TypeTheoretic.instReprQuantName.repr : QuantName → ℕ → Std.Format

Equations

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

def Semantics.TypeTheoretic.anaphoraAvailable : QuantName → List AnaphoraRef

Per-quantifier anaphora-set predictions ([Coo23] §7.4.1).

Equations

• One or more equations did not get rendered due to their size.
• Semantics.TypeTheoretic.anaphoraAvailable Semantics.TypeTheoretic.QuantName.exist = [Semantics.TypeTheoretic.AnaphoraRef.refset]
• Semantics.TypeTheoretic.anaphoraAvailable Semantics.TypeTheoretic.QuantName.existPl = [Semantics.TypeTheoretic.AnaphoraRef.refset, Semantics.TypeTheoretic.AnaphoraRef.maxset]
• Semantics.TypeTheoretic.anaphoraAvailable Semantics.TypeTheoretic.QuantName.no = [Semantics.TypeTheoretic.AnaphoraRef.maxset]
• Semantics.TypeTheoretic.anaphoraAvailable Semantics.TypeTheoretic.QuantName.every = [Semantics.TypeTheoretic.AnaphoraRef.maxset]
• Semantics.TypeTheoretic.anaphoraAvailable Semantics.TypeTheoretic.QuantName.most = [Semantics.TypeTheoretic.AnaphoraRef.maxset]
• Semantics.TypeTheoretic.anaphoraAvailable Semantics.TypeTheoretic.QuantName.many = [Semantics.TypeTheoretic.AnaphoraRef.maxset]
• Semantics.TypeTheoretic.anaphoraAvailable Semantics.TypeTheoretic.QuantName.aFew = [Semantics.TypeTheoretic.AnaphoraRef.refset, Semantics.TypeTheoretic.AnaphoraRef.maxset]

Induced classical GQ denotations

def Semantics.TypeTheoretic.witnessGQ_exist {E : Type} : Quantification.GQ E

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

Equations

• Semantics.TypeTheoretic.witnessGQ_exist A B = ∃ (x : E), A x ∧ B x

def Semantics.TypeTheoretic.witnessGQ_every {E : Type} : Quantification.GQ E

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

Equations

• Semantics.TypeTheoretic.witnessGQ_every A B = ∀ (x : E), A x → B x

theorem Semantics.TypeTheoretic.witnessGQ_exist_conservative {E : Type} : Quantification.Conservative witnessGQ_exist

Conservativity of witnessGQ_exist follows structurally from the WitnessSet subset condition — not stipulated as in [BC81].

theorem Semantics.TypeTheoretic.witnessGQ_every_conservative {E : Type} : Quantification.Conservative witnessGQ_every

Conservativity of witnessGQ_every.

Bridges between particular witness conditions and GQs

theorem Semantics.TypeTheoretic.particular_exist_iff_witnessGQ {E : Type} (P Q : E → Prop) : (∃ (x : E), P x ∧ Q x) ↔ witnessGQ_exist P Q

The particular existential condition equals the existential GQ denotation (both unfold to ∃ x, P x ∧ Q x).

theorem Semantics.TypeTheoretic.universal_iff_witnessGQ {E : Type} (P Q : E → Prop) : (∀ (x : E), P x → Q x) ↔ witnessGQ_every P Q

The universal condition equals the universal GQ denotation.

theorem Semantics.TypeTheoretic.particularWC_to_witnessGQ {E : Type} [DecidableEq E] {P Q : 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

ParticularWC_Exist constructs a witness for the existential GQ.

theorem Semantics.TypeTheoretic.particularWC_no_to_witnessGQ {E : Type} [DecidableEq E] {P Q : 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

ParticularWC_No constructs the universal GQ with negated scope.

Complement witness sets and the few / a_few contrast

theorem Semantics.TypeTheoretic.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 of a few_a witness set satisfies the complement cardinality condition.

theorem Semantics.TypeTheoretic.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

A witness set and its complement partition the extension.

Monotonicity from witness-condition shape

def Semantics.TypeTheoretic.generalWC_incr_mono {E : Type} [DecidableEq E] (P Q Q' : 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 general witness condition.

Equations

• Semantics.TypeTheoretic.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 Semantics.TypeTheoretic.generalWC_decr_mono {E : Type} [DecidableEq E] (P Q Q' : 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 general witness condition.

Equations

• Semantics.TypeTheoretic.generalWC_decr_mono P Q Q' isWS embed w = { X := w.X, witnessOK := ⋯, f := ⋯ }