Intolerance — Horn 1989 / Gajewski 2011

@cite{horn-1989} @cite{gajewski-2011}

A generalized-quantifier-typed function f : Set α → Prop is Intolerant iff it cannot map both a set x and its complement xᶜ to truth — equivalently, it sits "above the midpoint" of its scale.

@cite{gajewski-2011} (eq. 80, p. 131) introduces this in the form "f is Intolerant iff if f is not trivial, then for all x: ¬f x ∨ ¬f xᶜ" to make Appendix 2's hierarchy AA ⊆ DE + Intolerant ⊆ DE work cleanly: the trivial case is included by stipulation so that the AA inclusion is not blocked by trivially-true functions.

Examples

• no is Intolerant: #Few of my friends are linguists and few of them aren't (eq. 82a) — the conjunction is incoherent.
• fewer than n is not Intolerant when scale density permits: Fewer than 4 of my friends are linguists and fewer than 4 aren't (eq. 83) is consistent if I have ≤ 6 friends.

Hierarchy

Appendix 2 (p. 143) proves AA ⊆ DE + Intolerant. The reverse inclusion DE + Intolerant ⊆ DE is trivial. The strict inclusion (AA ⊊ DE + Intolerant) is asserted but not proved by Gajewski; would need a witness function that is DE + Intolerant but not AA.

def Semantics.Entailment.Intolerance.IsTrivial {α : Type u_1} (f : Set α → Prop) : Prop

A GQ-typed function is trivial if it is constantly true or constantly false.

Equations

• Semantics.Entailment.Intolerance.IsTrivial f = ((∀ (x : Set α), f x) ∨ ∀ (x : Set α), ¬f x)

def Semantics.Entailment.Intolerance.IsIntolerant {α : Type u_1} (f : Set α → Prop) : Prop

@cite{gajewski-2011} eq. 80: a function f : Set α → Prop is Intolerant iff it is trivial, OR for every x, at most one of f x and f xᶜ holds.

@cite{horn-1989}: Intolerant functions are "above the midpoint of their scale" — they cannot accept both a property and its complement.

Equations

• Semantics.Entailment.Intolerance.IsIntolerant f = (Semantics.Entailment.Intolerance.IsTrivial f ∨ ∀ (x : Set α), ¬f x ∨ ¬f xᶜ)

def Semantics.Entailment.Intolerance.IsAntiAdditiveGQ {α : Type u_1} (f : Set α → Prop) : Prop

A GQ-typed AA function (f : Set α → Prop with f (p ∪ q) ↔ f p ∧ f q).

Equations

• Semantics.Entailment.Intolerance.IsAntiAdditiveGQ f = ∀ (p q : Set α), f (p ∪ q) ↔ f p ∧ f q

def Semantics.Entailment.Intolerance.IsDownwardEntailingGQ {α : Type u_1} (f : Set α → Prop) : Prop

A GQ-typed DE function.

Equations

• Semantics.Entailment.Intolerance.IsDownwardEntailingGQ f = ∀ (p q : Set α), p ⊆ q → f q → f p

theorem Semantics.Entailment.Intolerance.isAntiAdditiveGQ_implies_isDEGQ {α : Type u_1} (f : Set α → Prop) (hAA : IsAntiAdditiveGQ f) : IsDownwardEntailingGQ f

AA-GQ implies DE-GQ. Standard.

theorem Semantics.Entailment.Intolerance.antiAdditiveGQ_implies_intolerant {α : Type u_1} (f : Set α → Prop) (hAA : IsAntiAdditiveGQ f) : IsIntolerant f

@cite{gajewski-2011} Appendix 2 (p. 143): AA implies Intolerant.

Proof sketch (Gajewski's): suppose f is AA and not trivial. For arbitrary a, suppose f a = True and f aᶜ = True. Then f (a ∪ aᶜ) ↔ f a ∧ f aᶜ gives f Set.univ = True. Since AA implies DE, every y ⊆ Set.univ has f y = True — contradicting non-triviality. So either ¬f a or ¬f aᶜ.