Witness sets

A witness set for a type ⟨1⟩ quantifier Q living on A is a subset of A that Q holds of (§4.9 of Barwise and Cooper). Such a quantifier holds of X exactly when A ∩ X is a witness set. Witness sets characterise the monotone quantifiers: an increasing quantifier holds of X iff X contains one of its witness sets, and a decreasing quantifier holds of X iff X ∩ A is contained in one (C11). Living on A already confines the minimal sets in Q to A, so the minimal witness sets are exactly the minimal sets in the quantifier.

Main definitions

• Quantifier.NP.Witness Q A w: w ⊆ A and Q w.

Main statements

• Quantifier.NP.LivesOn.apply_iff_witness: a quantifier living on A holds of X iff A ∩ X is a witness set.
• Quantifier.NP.LivesOn.monotone_apply_iff, Quantifier.NP.LivesOn.antitone_apply_iff: C11 for increasing and decreasing quantifiers.
• Quantifier.NP.LivesOn.minimal_witness_iff: the minimal witness sets of a quantifier living on A are its minimal sets.

Implementation notes

Witness sets are predicates, like the arguments of an NP; a study over a finite domain states a Finset witness X as (· ∈ X).

References

• J. Barwise, R. Cooper, Generalized Quantifiers and Natural Language (1981)

def Quantifier.NP.Witness {α : Type u_1} (Q : NP α) (A w : α → Prop) : Prop

A witness set for a quantifier living on A is a subset of A in the quantifier ([BC81] §4.9).

Equations

• Q.Witness A w = ((∀ (x : α), w x → A x) ∧ Q w)

theorem Quantifier.NP.LivesOn.apply_iff_witness {α : Type u_1} {Q : NP α} {A X : α → Prop} (h : Q.LivesOn A) : Q X ↔ Q.Witness A fun (x : α) => A x ∧ X x

A quantifier living on A holds of X iff A ∩ X is a witness set, whatever its monotonicity.

theorem Quantifier.NP.LivesOn.monotone_apply_iff {α : Type u_1} {Q : NP α} {A X : α → Prop} (h : Q.LivesOn A) (hm : Monotone Q) : Q X ↔ ∃ (w : α → Prop), Q.Witness A w ∧ ∀ (x : α), w x → X x

C11(i) says that an increasing quantifier living on A holds of X iff some witness set is contained in X.

theorem Quantifier.NP.LivesOn.antitone_apply_iff {α : Type u_1} {Q : NP α} {A X : α → Prop} (h : Q.LivesOn A) (hm : Antitone Q) : Q X ↔ ∃ (w : α → Prop), Q.Witness A w ∧ ∀ (x : α), X x ∧ A x → w x

C11(ii) says that a decreasing quantifier living on A holds of X iff X ∩ A is contained in some witness set.

theorem Quantifier.NP.LivesOn.minimal_witness_iff {α : Type u_1} {Q : NP α} {A w : α → Prop} (h : Q.LivesOn A) : Minimal (Q.Witness A) w ↔ Minimal Q w

The minimal witness sets of a quantifier living on A are its minimal sets, since a minimal set in Q lies inside A, Q holding also of its intersection with A.