Exceptive quantifiers

This file defines the semantics of exceptive constructions, every student but John and except for John, every student, over generalized quantifiers. An exceptive subtracts an exception set from the restrictor of a determiner, in the Boolean algebra of predicates on the domain. A restrictive exceptive is one the quantification needs: it holds with the subtraction and fails without it, which [VF93] gives as the semantics of the free exceptive. The exception set of a quantification is the least set whose subtraction makes it true, his semantics of the but-phrase, so that the phrase names the set responsible for the falsehood of the quantification.

Main definitions

• Restrictive, IsExceptionSet: domain subtraction with restrictiveness, and the exception set as the least verifying subtraction.

Main results

• IsExceptionSet.unique, IsExceptionSet.le_restrictor, isExceptionSet_iff_disjoint, isExceptionSet_iff_sInf_eq: the exception set is unique, lies within the restrictor, is disjoint from every verifying subset of the restrictor, and is the intersection of the verifying subtractions.
• isExceptionSet_every_iff, isExceptionSet_no_iff: with every the exception set is the restrictor minus the scope, with no their intersection.
• IsExceptionSet.eq_bot_of_restrictorMonotone, Restrictive.not_of_restrictorMonotone, Restrictive.mono: a left-upward-monotone determiner admits only the empty exception set and no restrictive exceptive; a left-downward-monotone one preserves restrictiveness under enlarging the exception.

Implementation notes

Restrictor, scope and exception set are predicates, so subtraction is \, inclusion ≤ and disjointness Disjoint of the pointwise Boolean algebra, and every R S is definitionally R ≤ S (every_iff_le) and no R S definitionally R ≤ Sᶜ (no_iff_le_compl). The disjointness formulation of the uniqueness condition is equivalent to the definition only for an exception set within the restrictor, which the definition entails (IsExceptionSet.le_restrictor) and the formulation does not.

References

• [VF93]

Domain subtraction with restrictiveness and the exception set

def Quantifier.Exceptive.Restrictive {α : Type u_1} (Q : GQ α) (A C B : α → Prop) : Prop

A restrictive exceptive subtracts the exception set C from the restrictor, so that the quantification holds with the subtraction and fails without it, (17) of [VF93] and his semantics of the free exceptive (38).

Equations

• Quantifier.Exceptive.Restrictive Q A C B = (Q (A \ C) B ∧ ¬Q A B)

def Quantifier.Exceptive.IsExceptionSet {α : Type u_1} (Q : GQ α) (A C B : α → Prop) : Prop

C is the exception set of the quantification when it is the least set whose subtraction from the restrictor makes the quantification true, (20) and (21) of [VF93] and his semantics of the but-phrase.

Equations

• Quantifier.Exceptive.IsExceptionSet Q A C B = IsLeast {S : α → Prop | Q (A \ S) B} C

theorem Quantifier.Exceptive.Restrictive.not_of_restrictorMonotone {α : Type u_1} {Q : GQ α} {A C B : α → Prop} (hQ : Q.RestrictorMonotone) : ¬Restrictive Q A C B

A left-upward-monotone determiner falsifies every restrictive exceptive.

theorem Quantifier.Exceptive.Restrictive.mono {α : Type u_1} {Q : GQ α} {A C B : α → Prop} (hQ : Q.RestrictorAntitone) (h : Restrictive Q A C B) {C' : α → Prop} (hC : C ≤ C') : Restrictive Q A C' B

Under a left-downward-monotone determiner a restrictive exceptive survives enlarging the exception set, the inference the exception set blocks.

theorem Quantifier.Exceptive.IsExceptionSet.unique {α : Type u_1} {Q : GQ α} {A C B : α → Prop} (h : IsExceptionSet Q A C B) {C' : α → Prop} (h' : IsExceptionSet Q A C' B) : C = C'

The exception set is unique.

theorem Quantifier.Exceptive.IsExceptionSet.le_restrictor {α : Type u_1} {Q : GQ α} {A C B : α → Prop} (h : IsExceptionSet Q A C B) : C ≤ A

The exception set lies within the restrictor, since subtracting C ⊓ A subtracts as much as C.

theorem Quantifier.Exceptive.IsExceptionSet.eq_bot_of_restrictorMonotone {α : Type u_1} {Q : GQ α} {A C B : α → Prop} (hQ : Q.RestrictorMonotone) (h : IsExceptionSet Q A C B) : C = ⊥

A left-upward-monotone determiner has only the empty exception set, since once the quantification holds with C subtracted it holds with nothing subtracted.

theorem Quantifier.Exceptive.IsExceptionSet.restrictive {α : Type u_1} {Q : GQ α} {A C B : α → Prop} (h : IsExceptionSet Q A C B) (hC : C ≠ ⊥) : Restrictive Q A C B

A nonempty exception set is restrictive, so the uniqueness condition subsumes restrictiveness.

theorem Quantifier.Exceptive.IsExceptionSet.of_iff_le {α : Type u_1} {Q : GQ α} {A B r : α → Prop} (h : ∀ (S : α → Prop), Q (A \ S) B ↔ r ≤ S) : IsExceptionSet Q A r B

When subtracting S rescues the quantification exactly when S covers r, the exception set is r. This is the culprit reasoning of [VF93]'s §1.6, which instantiates to A \ B for every and A ⊓ B for no.

The three formulations of the uniqueness condition

theorem Quantifier.Exceptive.isExceptionSet_iff_disjoint {α : Type u_1} {Q : GQ α} {A C B : α → Prop} (hCA : C ≤ A) : IsExceptionSet Q A C B ↔ Q (A \ C) B ∧ ∀ D ≤ A, Q D B → Disjoint C D

In the second formulation of (21) the exception set is disjoint from every subset of the restrictor that verifies the quantification. The hypothesis C ≤ A is what the definition entails (IsExceptionSet.le_restrictor) and this formulation alone does not.

theorem Quantifier.Exceptive.isExceptionSet_iff_sInf_eq {α : Type u_1} {Q : GQ α} {A C B : α → Prop} : IsExceptionSet Q A C B ↔ Q (A \ C) B ∧ sInf {S : α → Prop | Q (A \ S) B} = C

In the third formulation of (21) the exception set is the intersection of the sets whose subtraction verifies the quantification.

The universal determiners

theorem Quantifier.Exceptive.isExceptionSet_every {α : Type u_1} (A B : α → Prop) : IsExceptionSet GQ.every A (A \ B) B

With every the exception set is the restrictor minus the scope, since subtracting S rescues every exactly when S covers the restrictor elements outside the scope.

theorem Quantifier.Exceptive.isExceptionSet_no {α : Type u_1} (A B : α → Prop) : IsExceptionSet GQ.no A (A ⊓ B) B

With no the exception set is the intersection of restrictor and scope.

theorem Quantifier.Exceptive.isExceptionSet_every_iff {α : Type u_1} {A C B : α → Prop} : IsExceptionSet GQ.every A C B ↔ A \ B = C

(23) of [VF93] for every.

theorem Quantifier.Exceptive.isExceptionSet_no_iff {α : Type u_1} {A C B : α → Prop} : IsExceptionSet GQ.no A C B ↔ A ⊓ B = C

(23) of [VF93] for no.

theorem Quantifier.Exceptive.restrictive_every_iff {α : Type u_1} {A C B : α → Prop} : Restrictive GQ.every A C B ↔ A \ B ≤ C ∧ ¬A ≤ B

A restrictive exceptive with every covers the exceptions, of which there are some.

theorem Quantifier.Exceptive.restrictive_no_iff {α : Type u_1} {A C B : α → Prop} : Restrictive GQ.no A C B ↔ A ⊓ B ≤ C ∧ ¬Disjoint A B

A restrictive exceptive with no covers the overlap, which is nonempty.