def Semantics.Entailment.AntiAdditivity.IsAntiAdditive (f : BProp World → BProp World) : Prop

Anti-additive: forall A B, f(A | B) = f(A) & f(B).

Equations

• Semantics.Entailment.AntiAdditivity.IsAntiAdditive f = ∀ (p q : BProp Semantics.Entailment.World) (w : Semantics.Entailment.World), f (Semantics.Entailment.por p q) w = (f p w && f q w)

def Semantics.Entailment.AntiAdditivity.IsAntiMorphic (f : BProp World → BProp World) : Prop

Anti-morphic (AM): Anti-additive + distributes ∧ to ∨ in both directions.

∀ A B, f(A ∧ B) = f(A) ∨ f(B)

This is the characteristic property of negation (De Morgan's law).

Equations

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

theorem Semantics.Entailment.AntiAdditivity.antiAdditive_implies_de (f : BProp World → BProp World) (hAA : IsAntiAdditive f) : Polarity.IsDownwardEntailing f

Anti-additive implies DE.

The left-to-right direction of anti-additivity is exactly the DE property.

theorem Semantics.Entailment.AntiAdditivity.antiMorphic_implies_antiAdditive (f : BProp World → BProp World) (hAM : IsAntiMorphic f) : IsAntiAdditive f

Anti-morphic implies anti-additive.

By definition, anti-morphic is anti-additive plus the ∧-to-∨ property.

theorem Semantics.Entailment.AntiAdditivity.antiMorphic_implies_de (f : BProp World → BProp World) (hAM : IsAntiMorphic f) : Polarity.IsDownwardEntailing f

Anti-morphic implies DE.

Transitive: AM → AA → DE.

theorem Semantics.Entailment.AntiAdditivity.pnot_isAntiAdditive : IsAntiAdditive pnot

Negation is anti-additive.

¬(A ∨ B) = ¬A ∧ ¬B (De Morgan's law, part 1)

theorem Semantics.Entailment.AntiAdditivity.pnot_distributes_and (p q : BProp World) (w : World) : pnot (pand p q) w = (pnot p w || pnot q w)

Negation satisfies the conjunction-to-disjunction property.

¬(A ∧ B) = ¬A ∨ ¬B (De Morgan's law, part 2)

theorem Semantics.Entailment.AntiAdditivity.pnot_isAntiMorphic : IsAntiMorphic pnot

Negation is anti-morphic.

This is the strongest level in the hierarchy.

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

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

For a fixed restrictor, "no ___" as a function of scope.

Equations

• Semantics.Entailment.AntiAdditivity.no' restr scope x✝ = Semantics.Entailment.allWorlds.all fun (x : Semantics.Entailment.World) => !(restr x && scope x)

def Semantics.Entailment.AntiAdditivity.no_student : BProp World → BProp 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.

No A (B ∨ C) ⊣⊢ No A B ∧ No A C

Proof: "No student smokes or drinks" iff "No student smokes and no student drinks"

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

"No" is DE in scope.

Follows from anti-additivity.

def Semantics.Entailment.AntiAdditivity.atMost (n : ℕ) (restr scope : BProp World) : Bool

"At most n A's are B" - true if |A ∩ B| ≤ n.

We use a simplified version for our 4-world model.

Equations

• Semantics.Entailment.AntiAdditivity.atMost n restr scope = decide ((List.filter (fun (w : Semantics.Entailment.World) => restr w && scope w) Semantics.Entailment.allWorlds).length ≤ n)

def Semantics.Entailment.AntiAdditivity.atMost2_student : BProp World → BProp 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.

If P ⊆ Q, then "At most n A's are Q" ⊢ "At most n A's are P"

Because |A ∩ P| ≤ |A ∩ Q| when P ⊆ Q.

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

"At most 1 student ___" with fixed restrictor.

Using atMost 1 (not 2) because with only 2 students in p01, atMost 2 is trivially always true and hence vacuously anti-additive.

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 (the DE proof generalizes to any n).

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

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

The right-to-left direction of anti-additivity fails:

• "At most 1 student smokes" ∧ "At most 1 student drinks" does NOT imply "At most 1 student smokes or drinks"

Counterexample: let p = {w0} (only w0 smokes), q = {w1} (only w1 drinks). Then p01 ∩ p = {w0} (1 ≤ 1 ✓), p01 ∩ q = {w1} (1 ≤ 1 ✓), but p01 ∩ (p ∨ q) = {w0, w1} (2 > 1 ✗).

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

Weak NPI licensing: Requires DE context.

Examples: ever, any (unstressed), alcun

Equations

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

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

Strong NPI licensing: Requires Anti-Additive context.

Examples: lift a finger, in weeks, until

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

Strong NPIs require .antiAdditive or stronger:

• "*Few people lifted a finger" — few is only DE, not AA
• "No one lifted a finger" — no one is AA ✓

Weak NPIs accept .weak or stronger:

• "Few people ever complained" — few is DE ✓
• "No one ever complained" — no one is AA (≥ weak) ✓

def Semantics.Entailment.AntiAdditivity.IsAdditive (f : BProp World → BProp World) : Prop

Additive: f(A ∨ B) = f(A) ∨ f(B) and f(⊤) = ⊤. Dual of anti-additive. Preserved by "some" in both arguments.

Equations

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

def Semantics.Entailment.AntiAdditivity.IsMultiplicative (f : BProp World → BProp World) : Prop

Multiplicative: f(A ∧ B) = f(A) ∧ f(B) and f(⊥) = ⊥. Dual of anti-morphic's ∧-to-∨ clause. Preserved by "every" in scope.

Equations

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

def Semantics.Entailment.AntiAdditivity.IsAntiMultiplicative (f : BProp World → BProp World) : Prop

Anti-multiplicative: f(A ∧ B) = f(A) ∨ f(B) and f(⊥) = ⊤. Dual of anti-additive. Characteristic of "not every".

Equations

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

theorem Semantics.Entailment.AntiAdditivity.additive_implies_ue (f : BProp World → BProp World) (hAdd : IsAdditive f) : Polarity.IsUpwardEntailing f

Additive implies UE: f distributes over ∨ ⇒ f preserves entailment. Proof mirrors antiAdditive_implies_de.

theorem Semantics.Entailment.AntiAdditivity.multiplicative_implies_ue (f : BProp World → BProp World) (hMult : IsMultiplicative f) : Polarity.IsUpwardEntailing f

Multiplicative implies UE.

theorem Semantics.Entailment.AntiAdditivity.antiMultiplicative_implies_de (f : BProp World → BProp World) (hAM : IsAntiMultiplicative f) : Polarity.IsDownwardEntailing f

Anti-multiplicative implies DE.