Signature profiles of generalized quantifiers

[PW06] [vB84]

The natural-logic signature calculus instantiated at determiner denotations: each [vB84] double-monotonicity cell realizes a Signature₂ profile (DoubleMono.toSignature₂, certified by the four cell theorems), LeftAntiAdditive/RightAntiAdditive ([PW06] §5.9) are sectionwise IsAntiAdditive at the Prop instance, and every and no get certified profiles — with not every derived by profile composition rather than table lookup.

Main declarations

• DoubleMono.toSignature₂ — the profile of each double-monotonicity cell.
• signature₂_soundFor_upUp … signature₂_soundFor_downDown — the cells realize their profiles.
• leftAntiAdditive_iff_isAntiAdditive, rightAntiAdditive_iff_isAntiAdditive — sectionwise anti-additivity.
• every_sem_soundFor, no_sem_soundFor — certified determiner profiles.

The double-monotonicity cells

def Quantification.DoubleMono.toSignature₂ : DoubleMono → NaturalLogic.Signature₂

The signature profile of each [vB84] double-monotonicity class, at mono/anti granularity.

Equations

• Quantification.DoubleMono.upUp.toSignature₂ = { restrictor := NaturalLogic.Signature.mono, scope := NaturalLogic.Signature.mono }
• Quantification.DoubleMono.downUp.toSignature₂ = { restrictor := NaturalLogic.Signature.anti, scope := NaturalLogic.Signature.mono }
• Quantification.DoubleMono.upDown.toSignature₂ = { restrictor := NaturalLogic.Signature.mono, scope := NaturalLogic.Signature.anti }
• Quantification.DoubleMono.downDown.toSignature₂ = { restrictor := NaturalLogic.Signature.anti, scope := NaturalLogic.Signature.anti }

theorem Quantification.signature₂_soundFor_upUp {α : Type u_1} {q : GQ α} (hr : RestrictorUpwardMono q) (hs : ScopeUpwardMono q) : DoubleMono.upUp.toSignature₂.SoundFor q

↑MON↑ (e.g. some): both positions monotone.

theorem Quantification.signature₂_soundFor_downUp {α : Type u_1} {q : GQ α} (hr : RestrictorDownwardMono q) (hs : ScopeUpwardMono q) : DoubleMono.downUp.toSignature₂.SoundFor q

↓MON↑ (e.g. every): restrictor antitone, scope monotone.

theorem Quantification.signature₂_soundFor_upDown {α : Type u_1} {q : GQ α} (hr : RestrictorUpwardMono q) (hs : ScopeDownwardMono q) : DoubleMono.upDown.toSignature₂.SoundFor q

↑MON↓ (e.g. not all): restrictor monotone, scope antitone.

theorem Quantification.signature₂_soundFor_downDown {α : Type u_1} {q : GQ α} (hr : RestrictorDownwardMono q) (hs : ScopeDownwardMono q) : DoubleMono.downDown.toSignature₂.SoundFor q

↓MON↓ (e.g. no): both positions antitone.

Sectionwise anti-additivity

theorem Quantification.leftAntiAdditive_iff_isAntiAdditive {α : Type u_1} (q : GQ α) : LeftAntiAdditive q ↔ ∀ (S : α → Prop), IsAntiAdditive fun (R : α → Prop) => q R S

LeftAntiAdditive ([PW06] §5.9) is sectionwise anti-additivity in the restrictor, at the Prop instance.

theorem Quantification.rightAntiAdditive_iff_isAntiAdditive {α : Type u_1} (q : GQ α) : RightAntiAdditive q ↔ ∀ (R : α → Prop), IsAntiAdditive (q R)

RightAntiAdditive is sectionwise anti-additivity in the scope.

Certified determiner profiles

theorem Quantification.every_sem_soundFor {α : Type u_1} : { restrictor := NaturalLogic.Signature.anti, scope := NaturalLogic.Signature.mono }.SoundFor every_sem

Every realizes ↓MON↑ as a certified profile, the restrictor side derived from left anti-additivity (every_laa).

theorem Quantification.no_sem_soundFor {α : Type u_1} : { restrictor := NaturalLogic.Signature.anti, scope := NaturalLogic.Signature.anti }.SoundFor no_sem

No realizes ↓MON↓, both positions via anti-additivity (no_laa, no_raa).