The DE < anti-additive < anti-morphic hierarchy

[Ica12]'s function classes (his Definition 1.7, after [Hoe83] and Zwarts; cf. [Chi13] §1.4.3, [Lad80]): additive, multiplicative, anti-additive, and anti-multiplicative functions, stated in equational form over semilattices and instantiated at context functions (Set W → Set W') and generalized quantifiers (Set E → Prop). Following Icard, the plain properties are the binary equations; the IsCompletely* refinements add his unit conditions (adopted for non-trivial linguistic domains, his §1.1).

Main declarations

• IsAdditive, IsMultiplicative, IsAntiAdditive, IsAntiMultiplicative: the four classes, with Monotone/Antitone consequence lemmas;
• IsAntiMorphic: anti-additive and anti-multiplicative (Zwarts's class for superstrong NPIs);
• IsCompletely*: Icard's "completely P" refinements (unit conditions);
• isAntiAdditive_iff_mem, isAntiAdditive_iff_gq: pointwise bridges for the Set- and GQ-typed instances;
• licensesWeakNPI, licensesStrongNPI, licensesSuperstrongNPI: the Zwarts licensing thresholds ([Ica12] §4);
• toy-World witnesses: pnot (anti-morphic), no_student (anti-additive), atMost1_student (DE but not anti-additive — the strictness witness).

The property family ([Ica12] Definition 1.7)

def Entailment.IsAdditive {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (f : α → β) : Prop

Additive: f (p ⊔ q) = f p ⊔ f q.

Equations

• Entailment.IsAdditive f = ∀ (p q : α), f (p ⊔ q) = f p ⊔ f q

def Entailment.IsMultiplicative {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] (f : α → β) : Prop

Multiplicative: f (p ⊓ q) = f p ⊓ f q.

Equations

• Entailment.IsMultiplicative f = ∀ (p q : α), f (p ⊓ q) = f p ⊓ f q

def Entailment.IsAntiAdditive {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeInf β] (f : α → β) : Prop

Anti-additive: f (p ⊔ q) = f p ⊓ f q. Polymorphic in domain and codomain — needed e.g. for [Hoe83]'s S-comparative, anti-additive as a function Set Degree → Set Individual.

Equations

• Entailment.IsAntiAdditive f = ∀ (p q : α), f (p ⊔ q) = f p ⊓ f q

def Entailment.IsAntiMultiplicative {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeSup β] (f : α → β) : Prop

Anti-multiplicative: f (p ⊓ q) = f p ⊔ f q.

Equations

• Entailment.IsAntiMultiplicative f = ∀ (p q : α), f (p ⊓ q) = f p ⊔ f q

def Entailment.IsAntiMorphic {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : α → β) : Prop

Anti-morphic: anti-additive and anti-multiplicative — Zwarts's class of sentential negation, the superstrong-NPI licensors.

Equations

• Entailment.IsAntiMorphic f = (Entailment.IsAntiAdditive f ∧ Entailment.IsAntiMultiplicative f)

Completely-variants ([Ica12] Definition 1.7)

Icard: "by P we mean completely P" for linguistic application — the unit conditions amount to assuming non-trivial domains.

def Entailment.IsCompletelyAdditive {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [OrderTop α] [SemilatticeSup β] [OrderTop β] (f : α → β) : Prop

Completely additive: additive and f ⊤ = ⊤.

Equations

• Entailment.IsCompletelyAdditive f = (Entailment.IsAdditive f ∧ f ⊤ = ⊤)

def Entailment.IsCompletelyMultiplicative {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [OrderBot α] [SemilatticeInf β] [OrderBot β] (f : α → β) : Prop

Completely multiplicative: multiplicative and f ⊥ = ⊥.

Equations

• Entailment.IsCompletelyMultiplicative f = (Entailment.IsMultiplicative f ∧ f ⊥ = ⊥)

def Entailment.IsCompletelyAntiAdditive {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [OrderTop α] [SemilatticeInf β] [OrderBot β] (f : α → β) : Prop

Completely anti-additive: anti-additive and f ⊤ = ⊥.

Equations

• Entailment.IsCompletelyAntiAdditive f = (Entailment.IsAntiAdditive f ∧ f ⊤ = ⊥)

def Entailment.IsCompletelyAntiMultiplicative {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [OrderBot α] [SemilatticeSup β] [OrderTop β] (f : α → β) : Prop

Completely anti-multiplicative: anti-multiplicative and f ⊥ = ⊤.

Equations

• Entailment.IsCompletelyAntiMultiplicative f = (Entailment.IsAntiMultiplicative f ∧ f ⊥ = ⊤)

Monotonicity consequences

Each class refines monotonicity or antitonicity ([Ica12] Def. 1.7's closing remark).

theorem Entailment.IsAdditive.monotone {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (h : IsAdditive f) : Monotone f

Additive implies monotone.

theorem Entailment.IsMultiplicative.monotone {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] {f : α → β} (h : IsMultiplicative f) : Monotone f

Multiplicative implies monotone.

theorem Entailment.IsAntiAdditive.antitone {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeInf β] {f : α → β} (h : IsAntiAdditive f) : Antitone f

Anti-additive implies antitone ([Hoe83] Fact 4).

theorem Entailment.IsAntiMultiplicative.antitone {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeSup β] {f : α → β} (h : IsAntiMultiplicative f) : Antitone f

Anti-multiplicative implies antitone.

theorem Entailment.IsAntiMorphic.antiAdditive {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] {f : α → β} (h : IsAntiMorphic f) : IsAntiAdditive f

Anti-morphic implies anti-additive.

theorem Entailment.IsAntiMorphic.antiMultiplicative {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] {f : α → β} (h : IsAntiMorphic f) : IsAntiMultiplicative f

Anti-morphic implies anti-multiplicative.

theorem Entailment.IsAntiMorphic.antitone {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] {f : α → β} (h : IsAntiMorphic f) : Antitone f

Anti-morphic implies antitone.

mathlib hom-hierarchy bridges

The function classes are the unbundled predicates for mathlib's bundled lattice homs: an additive function is a SupHom, a multiplicative one an InfHom. The anti-classes are the same notions read into the order dual — anti-additivity is additivity composed with toDual (De Morgan duality), so the .antitone consequences are the duals of the .monotone ones.

def Entailment.IsAdditive.toSupHom {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (h : IsAdditive f) : SupHom α β

An additive function bundles as a SupHom.

Equations

• h.toSupHom = { toFun := f, map_sup' := h }

def Entailment.IsMultiplicative.toInfHom {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] {f : α → β} (h : IsMultiplicative f) : InfHom α β

A multiplicative function bundles as an InfHom.

Equations

• h.toInfHom = { toFun := f, map_inf' := h }

theorem Entailment.isAntiAdditive_iff_isAdditive_toDual {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeInf β] {f : α → β} : IsAntiAdditive f ↔ IsAdditive (⇑OrderDual.toDual ∘ f)

De Morgan duality: anti-additivity is additivity into the order dual — f sends joins to meets iff toDual ∘ f preserves joins.

Pointwise bridges

The equational properties at the Set and GQ instances, in the membership forms consumers destructure.

theorem Entailment.isAntiAdditive_iff_mem {γ : Type u_1} {δ : Type u_2} {f : Set γ → Set δ} : IsAntiAdditive f ↔ ∀ (p q : Set γ) (x : δ), x ∈ f (p ∪ q) ↔ x ∈ f p ∧ x ∈ f q

theorem Entailment.isAntiMultiplicative_iff_mem {γ : Type u_1} {δ : Type u_2} {f : Set γ → Set δ} : IsAntiMultiplicative f ↔ ∀ (p q : Set γ) (x : δ), x ∈ f (p ∩ q) ↔ x ∈ f p ∨ x ∈ f q

theorem Entailment.isAntiAdditive_iff_gq {γ : Type u_1} {f : Set γ → Prop} : IsAntiAdditive f ↔ ∀ (p q : Set γ), f (p ∪ q) ↔ f p ∧ f q

The GQ-typed instance (f : Set γ → Prop, Prop as a complete lattice): anti-additivity is the familiar f (p ∪ q) ↔ f p ∧ f q.

Toy-World witnesses and NPI licensing thresholds

theorem Entailment.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 Comparison.gt.overSet ([Hoe83]) instantiate this with P x y := μ x < μ y and P d y := d < μ y respectively.

theorem Entailment.pnot_isAntiAdditive : IsAntiAdditive pnot

Negation is anti-additive.

theorem Entailment.pnot_isAntiMultiplicative : IsAntiMultiplicative pnot

Negation is anti-multiplicative.

theorem Entailment.pnot_isAntiMorphic : IsAntiMorphic pnot

Negation is anti-morphic.

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

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

Equations

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

def Entailment.no_student : Set World → Set World

"No student ___" with fixed restrictor.

Equations

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

theorem Entailment.no_isAntiAdditive_scope : IsAntiAdditive no_student

"No" is anti-additive in scope.

theorem Entailment.no_isDE_scope : IsDE no_student

"No" is DE in scope.

def Entailment.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

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

theorem Entailment.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 Entailment.atMost2_student : Set World → Set World

"At most 2 students ___" with fixed restrictor.

Equations

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

theorem Entailment.atMost_isDE_scope : IsDE atMost2_student

"At most n" is DE in scope.

def Entailment.atMost1_student : Set World → Set World

"At most 1 student ___" with fixed restrictor.

Equations

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

theorem Entailment.atMost1_isDE_scope : IsDE atMost1_student

"At most 1" is still DE.

theorem Entailment.atMost_not_antiAdditive : ¬IsAntiAdditive atMost1_student

"At most n" is not anti-additive (counterexample): the strictness witness for DE ⊊ anti-additive.

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

Weak NPI licensing: requires DE.

Equations

• Entailment.licensesWeakNPI f = Entailment.IsDownwardEntailing f

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

Strong NPI licensing: requires anti-additivity.

Equations

• Entailment.licensesStrongNPI f = Entailment.IsAntiAdditive f

def Entailment.licensesSuperstrongNPI (f : Set World → Set World) : Prop

Superstrong NPI licensing ([Ica12] §4, after Zwarts): requires anti-morphicity — a tad bit under not but not under no.

Equations

• Entailment.licensesSuperstrongNPI f = Entailment.IsAntiMorphic f

DEStrength ↔ proof hierarchy ([Ica12] §4)

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