def Semantics.Entailment.AntiAdditivity.IsAntiAdditive {α : Type u_1} {β : Type u_2} (f : Set α → Set β) : Prop

Anti-additive: f(A ∪ B) = f(A) ∩ f(B) (pointwise iff form).

Polymorphic in domain and codomain — this is needed e.g. for @cite{hoeksema-1983}'s S-comparative, which is anti-additive as a function Set Degree → Set Individual.

Equations

• Semantics.Entailment.AntiAdditivity.IsAntiAdditive f = ∀ (p q : Set α) (x : β), f (p ∪ q) x ↔ f p x ∧ f q x

def Semantics.Entailment.AntiAdditivity.IsAntiMorphic {α : Type u_1} {β : Type u_2} (f : Set α → Set β) : Prop

Anti-morphic (AM): Anti-additive + distributes ∩ to ∪.

Equations

• Semantics.Entailment.AntiAdditivity.IsAntiMorphic f = (Semantics.Entailment.AntiAdditivity.IsAntiAdditive f ∧ ∀ (p q : Set α) (x : β), f (p ∩ q) x ↔ f p x ∨ f q x)

theorem Semantics.Entailment.AntiAdditivity.IsAntiAdditive.antitone {α : Type u_1} {β : Type u_2} {f : Set α → Set β} (hAA : IsAntiAdditive f) : Antitone f

Anti-additive implies antitone (@cite{hoeksema-1983} Fact 4: the polarity-environment classification of anti-additive operators as downward-entailing). Codomain need not be Set World.

theorem Semantics.Entailment.AntiAdditivity.IsAntiMorphic.antiAdditive {α : Type u_1} {β : Type u_2} {f : Set α → Set β} (hAM : IsAntiMorphic f) : IsAntiAdditive f

Anti-morphic implies anti-additive.

theorem Semantics.Entailment.AntiAdditivity.IsAntiMorphic.antitone {α : Type u_1} {β : Type u_2} {f : Set α → Set β} (hAM : IsAntiMorphic f) : Antitone f

Anti-morphic implies antitone.

theorem Semantics.Entailment.AntiAdditivity.isAntiAdditive_forall_mem {α : Type u_1} {β : Type u_2} (P : α → β → Prop) : IsAntiAdditive fun (X : Set α) (y : β) => ∀ x ∈ X, P x y

Any function of the form fun X y => ∀ x ∈ X, P x y is anti-additive in X.

npComparative and sComparative (@cite{hoeksema-1983}) instantiate this with P x y := μ x < μ y and P d y := d < μ y respectively.

theorem Semantics.Entailment.AntiAdditivity.pnot_isAntiAdditive : IsAntiAdditive pnot

Negation is anti-additive.

theorem Semantics.Entailment.AntiAdditivity.pnot_distributes_and (p q : Set World) (w : World) : pnot (pand p q) w ↔ pnot p w ∨ pnot q w

Negation satisfies the conjunction-to-disjunction property.

theorem Semantics.Entailment.AntiAdditivity.pnot_isAntiMorphic : IsAntiMorphic pnot

Negation is anti-morphic.

def Semantics.Entailment.AntiAdditivity.no' (restr scope : Set World) : Set World

"No A is B" = ∀x. A(x) → ¬B(x).

Equations

• Semantics.Entailment.AntiAdditivity.no' restr scope x✝ = ∀ x ∈ Semantics.Entailment.allWorlds, ¬(restr x ∧ scope x)

def Semantics.Entailment.AntiAdditivity.no_student : Set World → Set World

"No student ___" with fixed restrictor.

Equations

• Semantics.Entailment.AntiAdditivity.no_student = Semantics.Entailment.AntiAdditivity.no' Semantics.Entailment.p01

theorem Semantics.Entailment.AntiAdditivity.no_isAntiAdditive_scope : IsAntiAdditive no_student

"No" is anti-additive in scope.

theorem Semantics.Entailment.AntiAdditivity.no_isDE_scope : Polarity.IsDE no_student

"No" is DE in scope.

def Semantics.Entailment.AntiAdditivity.atMost (n : ℕ) (restr scope : Set World) : Prop

"At most n A's are B" - true if at most n worlds satisfy both. Uses an existential over a sublist witness so the def is decidable only when the predicates are decidable, but stays in Prop.

Equations

• Semantics.Entailment.AntiAdditivity.atMost n restr scope = ∀ (ws : List Semantics.Entailment.World), ws.Nodup → (∀ w ∈ ws, restr w ∧ scope w) → ws.length ≤ n

theorem Semantics.Entailment.AntiAdditivity.atMost_mono (n : ℕ) (restr p q : Set World) (hpq : ∀ (w : World), p w → q w) (h : atMost n restr q) : atMost n restr p

Monotonicity: if p ⊆ q (entailment) and q has at most n witnesses, so does p.

def Semantics.Entailment.AntiAdditivity.atMost2_student : Set World → Set World

"At most 2 students ___" with fixed restrictor.

Equations

• Semantics.Entailment.AntiAdditivity.atMost2_student scope x✝ = Semantics.Entailment.AntiAdditivity.atMost 2 Semantics.Entailment.p01 scope

theorem Semantics.Entailment.AntiAdditivity.atMost_isDE_scope : Polarity.IsDE atMost2_student

"At most n" is DE in scope.

def Semantics.Entailment.AntiAdditivity.atMost1_student : Set World → Set World

"At most 1 student ___" with fixed restrictor.

Equations

• Semantics.Entailment.AntiAdditivity.atMost1_student scope x✝ = Semantics.Entailment.AntiAdditivity.atMost 1 Semantics.Entailment.p01 scope

theorem Semantics.Entailment.AntiAdditivity.atMost1_isDE_scope : Polarity.IsDE atMost1_student

"At most 1" is still DE.

theorem Semantics.Entailment.AntiAdditivity.atMost_not_antiAdditive : ¬IsAntiAdditive atMost1_student

"At most n" is not anti-additive (counterexample).

def Semantics.Entailment.AntiAdditivity.licensesWeakNPI (f : Set World → Set World) : Prop

Weak NPI licensing: requires DE.

Equations

• Semantics.Entailment.AntiAdditivity.licensesWeakNPI f = Semantics.Entailment.Polarity.IsDownwardEntailing f

def Semantics.Entailment.AntiAdditivity.licensesStrongNPI (f : Set World → Set World) : Prop

Strong NPI licensing: requires Anti-Additive.

Equations

• Semantics.Entailment.AntiAdditivity.licensesStrongNPI f = Semantics.Entailment.AntiAdditivity.IsAntiAdditive f

DEStrength ↔ Proof Hierarchy

@cite{icard-2012}

DEStrength	Proof Predicate	Example Licensor
.weak	IsDE	few, at most n
.antiAdditive	IsAntiAdditive	no, nobody, without
.antiMorphic	IsAntiMorphic	not, never

def Semantics.Entailment.AntiAdditivity.IsAdditive {α : Type u_1} {β : Type u_2} (f : Set α → Set β) : Prop

Additive: f(A ∪ B) = f(A) ∪ f(B) and f(⊤) = ⊤.

Equations

• Semantics.Entailment.AntiAdditivity.IsAdditive f = ((∀ (p q : Set α) (x : β), f (p ∪ q) x ↔ f p x ∨ f q x) ∧ ∀ (x : β), f Set.univ x)

def Semantics.Entailment.AntiAdditivity.IsMultiplicative {α : Type u_1} {β : Type u_2} (f : Set α → Set β) : Prop

Multiplicative: f(A ∩ B) = f(A) ∩ f(B) and f(⊥) = ⊥.

Equations

• Semantics.Entailment.AntiAdditivity.IsMultiplicative f = ((∀ (p q : Set α) (x : β), f (p ∩ q) x ↔ f p x ∧ f q x) ∧ ∀ (x : β), ¬f ∅ x)

def Semantics.Entailment.AntiAdditivity.IsAntiMultiplicative {α : Type u_1} {β : Type u_2} (f : Set α → Set β) : Prop

Anti-multiplicative: f(A ∩ B) = f(A) ∪ f(B) and f(⊥) = ⊤.

Equations

• Semantics.Entailment.AntiAdditivity.IsAntiMultiplicative f = ((∀ (p q : Set α) (x : β), f (p ∩ q) x ↔ f p x ∨ f q x) ∧ ∀ (x : β), f ∅ x)

theorem Semantics.Entailment.AntiAdditivity.IsAdditive.monotone {α : Type u_1} {β : Type u_2} {f : Set α → Set β} (hAdd : IsAdditive f) : Monotone f

Additive implies monotone.

theorem Semantics.Entailment.AntiAdditivity.IsMultiplicative.monotone {α : Type u_1} {β : Type u_2} {f : Set α → Set β} (hMult : IsMultiplicative f) : Monotone f

Multiplicative implies monotone.

theorem Semantics.Entailment.AntiAdditivity.IsAntiMultiplicative.antitone {α : Type u_1} {β : Type u_2} {f : Set α → Set β} (hAM : IsAntiMultiplicative f) : Antitone f

Anti-multiplicative implies antitone.