Exceptive Quantifiers

@cite{peters-westerstahl-2006} @cite{von-fintel-1993} @cite{gajewski-2002}

Semantic operators for "but"-exceptive constructions:

"every student but John passed" = every(student \ {John}, passed) ∧ ¬passed(John)

Only universal quantifiers (positive or negative) license exceptives.

Von Fintel (1993) Operators

• ExcI: the inclusive exceptive operator (every...but)
• ExcE: the exclusive exceptive operator (no...but)
• ExceptiveCompatible: which quantifiers license exceptives

Peters & Westerståhl (2006) Operators

• IsException: whether an element is an exception for a quantifier
• ExcW: the weak exceptive operator (@cite{peters-westerstahl-2006} Ch 8, (8.31))
• ExcS: the strong exceptive operator (@cite{peters-westerstahl-2006} Ch 8, (8.33))

Key Results

Under CONSERV, only PositiveStrong/NegativeStrong quantifiers produce non-trivial exceptive readings — explaining the universal-only pattern.

def Semantics.Quantification.Exceptive.ExcI {α : Type u_1} (Q : Core.Quantification.GQ α) (A E B : α → Prop) : Prop

Inclusive exceptive (@cite{von-fintel-1993}): Q(A \ E, B) ∧ ¬Q(A, B).

"Every student but John passed" = every(student \ {John}, passed) ∧ ¬every(student, passed)

The second conjunct asserts that the exception matters: without removing E, the quantified claim would be false.

Equations

• Semantics.Quantification.Exceptive.ExcI Q A E B = (Q (fun (x : α) => A x ∧ ¬E x) B ∧ ¬Q A B)

def Semantics.Quantification.Exceptive.ExcE {α : Type u_1} (Q : Core.Quantification.GQ α) (A E B : α → Prop) : Prop

Exclusive exceptive (@cite{von-fintel-1993}): Q(A \ E, B) ∧ complement condition on E.

"No student but John passed" = no(student \ {John}, passed) ∧ John passed

The complement condition requires that all excepted elements satisfy B.

Equations

• Semantics.Quantification.Exceptive.ExcE Q A E B = (Q (fun (x : α) => A x ∧ ¬E x) B ∧ ∀ (x : α), E x → A x → B x)

def Semantics.Quantification.Exceptive.IsException {α : Type u_1} (a : α) (A B : α → Prop) : Prop

Whether an element is an "exception" for a positive generalization Q₁(A, B): an element of A that is NOT in B (i.e., a counterexample to the generalization).

For "every student passed", John is an exception if John is a student who did not pass — i.e., John ∈ A \ B.

For negative generalizations (like "no"), the notion inverts: an exception would be an element of A ∩ B. We handle this via IsExceptionNeg.

@cite{peters-westerstahl-2006} Ch 8, p299.

Equations

• Semantics.Quantification.Exceptive.IsException a A B = (A a ∧ ¬B a)

def Semantics.Quantification.Exceptive.IsExceptionNeg {α : Type u_1} (a : α) (A B : α → Prop) : Prop

Whether an element is an "exception" for a negative generalization: an element of A that IS in B (a counterexample to "no A is B").

@cite{peters-westerstahl-2006} Ch 8, p299.

Equations

• Semantics.Quantification.Exceptive.IsExceptionNeg a A B = (A a ∧ B a)

def Semantics.Quantification.Exceptive.ExcW {α : Type u_1} (Q₁ : Core.Quantification.GQ α) (C A B : α → Prop) : Prop

Weak exceptive (@cite{peters-westerstahl-2006} Ch 8, (8.31)):

Exc_w(Q₁, C)(A, B) ⟺ Q₁(A \ C, B) ∧ something in A ∩ C is an exception for Q₁

"Every student but John passed" (weak reading): = every(student \ {John}, passed) ∧ ∃x ∈ student ∩ {John}, x ∉ passed = every(student \ {John}, passed) ∧ John didn't pass

The weak version only requires SOME excepted element to be an actual exception.

Equations

• Semantics.Quantification.Exceptive.ExcW Q₁ C A B = (Q₁ (fun (x : α) => A x ∧ ¬C x) B ∧ ∃ (x : α), A x ∧ C x ∧ Semantics.Quantification.Exceptive.IsException x A B)

def Semantics.Quantification.Exceptive.ExcS {α : Type u_1} (Q₁ : Core.Quantification.GQ α) (C A B : α → Prop) : Prop

Strong exceptive (@cite{peters-westerstahl-2006} Ch 8, (8.33)):

Exc_s(Q₁, C)(A, B) ⟺ Q₁(A \ C, B) ∧ A ∩ C ≠ ∅ ∧ everything in A ∩ C is an exception for Q₁

"Every student but John passed" (strong reading): = every(student \ {John}, passed) ∧ {John} ∩ student ≠ ∅ ∧ ∀x ∈ student ∩ {John}, x ∉ passed = every(student \ {John}, passed) ∧ John is a student ∧ John didn't pass

The strong version requires EVERY excepted element to be an actual exception, and that the exception set is non-empty.

P&W argue this is the correct analysis: the UC (Uniqueness Condition) follows from Exc_s but not from Exc_w.

Equations

• Semantics.Quantification.Exceptive.ExcS Q₁ C A B = (Q₁ (fun (x : α) => A x ∧ ¬C x) B ∧ (∃ (x : α), A x ∧ C x) ∧ ∀ (x : α), A x → C x → Semantics.Quantification.Exceptive.IsException x A B)

def Semantics.Quantification.Exceptive.ExcWNeg {α : Type u_1} (Q₁ : Core.Quantification.GQ α) (C A B : α → Prop) : Prop

Weak exceptive for negative quantifiers (@cite{peters-westerstahl-2006} Ch 8, (8.31)):

Exc_w(no, C)(A, B) ⟺ no(A \ C, B) ∧ something in A ∩ C is in B

"No student but John passed" (weak reading): = no(student \ {John}, passed) ∧ John passed

Equations

• Semantics.Quantification.Exceptive.ExcWNeg Q₁ C A B = (Q₁ (fun (x : α) => A x ∧ ¬C x) B ∧ ∃ (x : α), A x ∧ C x ∧ Semantics.Quantification.Exceptive.IsExceptionNeg x A B)

def Semantics.Quantification.Exceptive.ExcSNeg {α : Type u_1} (Q₁ : Core.Quantification.GQ α) (C A B : α → Prop) : Prop

Strong exceptive for negative quantifiers (@cite{peters-westerstahl-2006} Ch 8, (8.33)):

Exc_s(no, C)(A, B) ⟺ no(A \ C, B) ∧ A ∩ C ≠ ∅ ∧ everything in A ∩ C is in B

"No student but John passed" (strong reading): = no(student \ {John}, passed) ∧ John is a student ∧ John passed

Equations

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

def Semantics.Quantification.Exceptive.ExceptiveCompatible {α : Type u_1} (Q : Core.Quantification.GQ α) : Prop

A quantifier is exceptive-compatible iff there exist A, E, B such that ExcI(Q, A, E, B). @cite{von-fintel-1993}: only (variants of) every and no are compatible.

Equations

• Semantics.Quantification.Exceptive.ExceptiveCompatible Q = ∃ (A : α → Prop) (E : α → Prop) (B : α → Prop), Semantics.Quantification.Exceptive.ExcI Q A E B

theorem Semantics.Quantification.Exceptive.positiveStrong_exceptive {α : Type u_1} (Q : Core.Quantification.GQ α) (hCons : Core.Quantification.Conservative Q) (hPS : Core.Quantification.PositiveStrong Q) (hNontriv : ∃ (A : α → Prop) (B : α → Prop), ¬Q A B) : ExceptiveCompatible Q

PositiveStrong quantifiers can yield non-trivial inclusive exceptives.

For "every": every(A\E, B) can be true (all non-excepted As are Bs) while every(A, B) is false (the excepted elements fail B). @cite{von-fintel-1993}, @cite{peters-westerstahl-2006} Ch 8.

theorem Semantics.Quantification.Exceptive.symmetric_not_exceptive {α : Type u_1} (Q : Core.Quantification.GQ α) (hCons : Core.Quantification.Conservative Q) (hSym : Core.Quantification.QSymmetric Q) (hPS : Core.Quantification.PositiveStrong Q) : ¬ExceptiveCompatible Q

Symmetric quantifiers are NOT exceptive-compatible (under CONSERV + PS).

Intuition: under CONSERV + SYMM, Q depends only on |A ∩ B|. Removing elements from A while keeping them out of E cannot simultaneously make Q(A\E, B) true and Q(A, B) false, because the intersection |A∩B| ⊇ |(A\E)∩B| — removing elements from A can only shrink the intersection, not enlarge it. @cite{von-fintel-1993}, @cite{peters-westerstahl-2006} Ch 8.