Ladusaw (1979): Polarity Sensitivity as Inherent Scope Relations

Ladusaw's licensing condition says that a negative polarity item is acceptable only in the scope of a downward-entailing expression, one that reverses entailment among its arguments, so that the affective environments of the earlier literature are characterized rather than listed. Every environment credited to the dissertation denotes a downward-entailing operator (cited_environments_de), questions do not (question_not_de), and a downward-entailing environment licenses the weak polarity items (ladusaw_generalization). The determiners behind three of these environments are downward entailing in exactly the argument where they license: no in its scope and its restrictor, few in its scope, and every in its restrictor but not its scope (determiner_monotonicity).

Implementation notes

• Ladusaw reads a conditional antecedent as the antecedent of a material conditional, which is downward entailing (materialAntecedent); the library's LicensingContext.conditionalAntecedent is von Fintel's counterfactual, downward entailing only modulo its presupposition.
• The dissertation's scan in the library has no text layer; environments is the list the library credits to it. The anti-additive licensers and the strong polarity items postdate the dissertation, and questions license weak items by another route, so the converse of the generalization is not stated.

References

• [Lad79]

def Ladusaw1979.IsDownwardEntailing (L : PolarityItem.Licenser) : Prop

An environment is downward entailing when the operator it places over the item reverses entailment.

Equations

• Ladusaw1979.IsDownwardEntailing L = L.Holds NaturalLogic.Signature.anti

structure Ladusaw1979.Consequent : Type 1

A conditional's consequent, over worlds.

• W : Type

  The worlds.

• q : Set self.W

  The consequent.

def Ladusaw1979.materialAntecedent : PolarityItem.Licenser

The antecedent of a material conditional, Ladusaw's reading of conditional antecedents.

Equations

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

theorem Ladusaw1979.isDownwardEntailing_materialAntecedent : IsDownwardEntailing materialAntecedent

noncomputable def Ladusaw1979.environments : List PolarityItem.Licenser

The licensing environments credited to the dissertation are negation, negative quantifiers, without, the restrictor of a universal, few, at most, the antecedent of a conditional, before, too … to, and the clausal comparative.

Equations

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

theorem Ladusaw1979.cited_environments_de (c : PolarityItem.Licenser) : c ∈ environments → IsDownwardEntailing c

Every environment credited to the dissertation is downward entailing.

theorem Ladusaw1979.question_not_de : ¬IsDownwardEntailing PolarityItem.LicensingContext.question.licenser

Questions are not downward entailing.

theorem Ladusaw1979.ladusaw_generalization (L : PolarityItem.Licenser) (hc : IsDownwardEntailing L) (hn : ¬L.IsStrawsonUE) (e : PolarityItem) (he : e.licensor = some PolarityItem.DEStrength.weak) : L.Licenses e

A downward-entailing environment licenses the weak polarity items, the dissertation's generalization, which the library takes as its definition of licensing by strengthening once the environment is not downward entailing by being constant.

theorem Ladusaw1979.determiner_monotonicity {α : Type u_1} [Fintype α] [Nonempty α] : Quantifier.GQ.no.ScopeAntitone ∧ Quantifier.GQ.no.RestrictorAntitone ∧ Quantifier.GQ.few.ScopeAntitone ∧ Quantifier.GQ.every.RestrictorAntitone ∧ ¬Quantifier.GQ.every.ScopeAntitone

no reverses entailment in both arguments, few in its scope, and every in its restrictor but not its scope, which is where each licenses a polarity item.