Signature profiles of generalized quantifiers

This file instantiates the natural-logic signature calculus at determiner denotations. The left and right anti-additivity of Peters and Westerståhl are sectionwise anti-additivity of the restrictor and scope positions at the Prop instance, and every and no receive certified Signature₂ profiles, with not every derived by profile composition.

Main results

• leftAntiAdditive_iff_isAntiAdditive, rightAntiAdditive_iff_isAntiAdditive: the two anti-additivities as sectionwise IsAntiAdditive.
• soundFor_every, soundFor_no: the certified determiner profiles.

References

• [PW06]
• [vB84]

Sectionwise anti-additivity

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

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

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

RightAntiAdditive is sectionwise anti-additivity in the scope.

Certified determiner profiles

theorem Quantifier.GQ.soundFor_every {α : Type u_1} : { restrictor := NaturalLogic.Signature.anti, scope := NaturalLogic.Signature.mono }.SoundFor every

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

theorem Quantifier.GQ.soundFor_no {α : Type u_1} : { restrictor := NaturalLogic.Signature.anti, scope := NaturalLogic.Signature.anti }.SoundFor no

No realizes ↓MON↓, both positions via anti-additivity (leftAntiAdditive_no, rightAntiAdditive_no).