Licensers

A licenser is what a construction places over the position of a polarity item: a family of operators, one for each choice of what the construction leaves open, such as the model, a restrictor, a bound or an accessibility relation. A classical licenser maps between bounded lattices, a scalar licenser does so with a stronger mate on its scale, von Fintel's map into trivalent propositions carries a presupposition, a modal licenser quantifies over worlds, and a question licenser is a wh-question.

Following Gajewski, a licenser has two meanings: the plain one below the exhaustivity operator and the one above it, with its direct implicature, the exhaustification against its stronger scale-mates, factored in. Only a scalar licenser has a direct implicature. Every negative polarity item needs the plain meaning downward entailing modulo presupposition, after von Fintel, and not trivially so, not upward entailing as well, after Bylinina and Nouwen; an item needing a stronger strength of negation needs it outright of the other meaning. Gajewski asks only for downward entailment there, and the library keeps Zwarts's strengths, which agree with it on the scale endpoints. A modal licenser licenses free choice when the antiexhaustified existential under one of its operators is consistent, after Chierchia, and a question licenses by relevance, since widening the domain of a wh-question never lowers its value, after van Rooy.

Main definitions

• PolarityItem.Licenser: the five kinds of licenser.
• PolarityItem.Licenser.exhaustified: the licenser with its direct implicature factored in.
• PolarityItem.Licenser.Holds, PolarityItem.Licenser.IsStrawsonDE, PolarityItem.Licenser.IsStrawsonUE, PolarityItem.Licenser.Carries: a signature held outright, downward and upward entailment modulo presupposition, and a strength of negation carried.
• PolarityItem.Licenser.LicensesFreeChoice, PolarityItem.Licenser.LicensesByRelevance: the free-choice and question routes.

Implementation notes

• The unit conditions of Signature.HoldsFor do not exclude constant maps, which are downward entailing and, if constantly false, anti-additive; requiring weak strength not to be upward entailing as well excludes them.
• The question route states the weak form the theory of question value proves, that widening never lowers the question's value; van Rooy's strict condition for rhetorical questions is not formalized.

References

• [vF99a]
• [Gaj11]
• [Zwa98]
• [BN18]
• [Ica12]
• [Chi06]
• [vR03a]

structure PolarityItem.OperatorFamily : Type 2

A family of operators between bounded lattices, indexed by what a construction leaves open.

• Param : Type 1

  What the construction leaves open.

• Dom : self.Param → Type

  The lattice the item's position ranges over.

• Cod : self.Param → Type

  The lattice of the result.

• latDom (p : self.Param) : Lattice (self.Dom p)

  The domain is a lattice.

• bndDom (p : self.Param) : BoundedOrder (self.Dom p)

  The domain is bounded.

• latCod (p : self.Param) : Lattice (self.Cod p)

  The codomain is a lattice.

• bndCod (p : self.Param) : BoundedOrder (self.Cod p)

  The codomain is bounded.

• op (p : self.Param) : self.Dom p → self.Cod p

  The operator at each parameter.

structure PolarityItem.PresupposingFamily : Type 2

A family of operators into trivalent propositions, indexed by what a construction leaves open.

• Param : Type 1

  What the construction leaves open.

• Dom : self.Param → Type

  The lattice the item's position ranges over.

• W : self.Param → Type

  The worlds of the trivalent propositions.

• latDom (p : self.Param) : Lattice (self.Dom p)

  The domain is a lattice.

• bndDom (p : self.Param) : BoundedOrder (self.Dom p)

  The domain is bounded.

• op (p : self.Param) : self.Dom p → self.W p → SignType

  The operator at each parameter.

structure PolarityItem.ModalFamily : Type 2

A family of modal operators over worlds, indexed by what a construction leaves open.

• Param : Type 1

  What the construction leaves open.

• W : self.Param → Type

  The worlds.

• op (p : self.Param) : Set (self.W p) → Set (self.W p)

  The operator at each parameter.

structure PolarityItem.ScalarFamilyextends PolarityItem.OperatorFamily : Type 2

A family of operators on a scale with stronger mates, each paired with its meaning enriched by its direct implicature, the exhaustification against those mates ([Gaj11]'s O with ALT-1).

• Param : Type 1
• Dom : self.Param → Type
• Cod : self.Param → Type
• latDom (p : self.Param) : Lattice (self.Dom p)
• bndDom (p : self.Param) : BoundedOrder (self.Dom p)
• latCod (p : self.Param) : Lattice (self.Cod p)
• bndCod (p : self.Param) : BoundedOrder (self.Cod p)
• op (p : self.Param) : self.Dom p → self.Cod p
• exhaustified (p : self.Param) : self.Dom p → self.Cod p

  The operator exhaustified against its stronger scale-mates, at each parameter.

inductive PolarityItem.Licenser : Type 2

A licenser is the operator a construction places over the position of a polarity item, a classical operator, a scalar operator with its enrichment, an operator into trivalent propositions, a modal operator, or a question.

• classical (F : OperatorFamily) : Licenser
• scalar (F : ScalarFamily) : Licenser
• strawson (F : PresupposingFamily) : Licenser
• modal (F : ModalFamily) : Licenser
• question : Licenser

inductive PolarityItem.LicensingMechanism : Type

A context licenses polarity items by strengthening, as a generic context licensing free choice items ([KL93], [Day96]), or by the relevance of a question ([vR03a]).

• strengthening : LicensingMechanism
• genericIndefinite : LicensingMechanism
• entropy : LicensingMechanism

@[instance_reducible]

instance PolarityItem.instDecidableEqLicensingMechanism : DecidableEq LicensingMechanism

Equations

• PolarityItem.instDecidableEqLicensingMechanism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance PolarityItem.instReprLicensingMechanism : Repr LicensingMechanism

Equations

• PolarityItem.instReprLicensingMechanism = { reprPrec := PolarityItem.instReprLicensingMechanism.repr }

def PolarityItem.instReprLicensingMechanism.repr : LicensingMechanism → ℕ → Std.Format

Equations

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

def PolarityItem.Licenser.exhaustified : Licenser → Licenser

The licenser with its direct implicature factored in, the meaning above the exhaustivity operator, is the enriched operators of a scalar licenser and any other licenser itself.

Equations

• One or more equations did not get rendered due to their size.
• x✝.exhaustified = x✝

def PolarityItem.Licenser.Holds : Licenser → NaturalLogic.Signature → Prop

A licenser holds a signature outright when every operator in its family does; an operator into trivalent propositions holds it on its truth set, and a scalar operator on its plain meaning.

Equations

• (PolarityItem.Licenser.classical F).Holds x✝ = ∀ (p : F.Param), x✝.HoldsFor (F.op p)
• (PolarityItem.Licenser.scalar { toOperatorFamily := F, exhaustified := exhaustified }).Holds x✝ = ∀ (p : F.Param), x✝.HoldsFor (F.op p)
• (PolarityItem.Licenser.strawson F).Holds x✝ = ∀ (p : F.Param), x✝.HoldsFor fun (x : F.Dom p) => Trivalent.posExt (F.op p x)
• (PolarityItem.Licenser.modal F).Holds x✝ = False
• PolarityItem.Licenser.question.Holds x✝ = False

def PolarityItem.Licenser.IsStrawsonDE : Licenser → Prop

A licenser is Strawson downward entailing when every operator in its family is downward entailing modulo its presupposition.

Equations

• (PolarityItem.Licenser.classical F).IsStrawsonDE = ∀ (p : F.Param), Antitone (F.op p)
• (PolarityItem.Licenser.scalar { toOperatorFamily := F, exhaustified := exhaustified }).IsStrawsonDE = ∀ (p : F.Param), Antitone (F.op p)
• (PolarityItem.Licenser.strawson F).IsStrawsonDE = ∀ (p : F.Param), NaturalLogic.IsStrawsonDE (F.op p)
• (PolarityItem.Licenser.modal F).IsStrawsonDE = False
• PolarityItem.Licenser.question.IsStrawsonDE = False

def PolarityItem.Licenser.IsStrawsonUE : Licenser → Prop

A licenser is Strawson upward entailing when every operator in its family is upward entailing modulo its presupposition; a constant operator is both this and downward entailing.

Equations

• (PolarityItem.Licenser.classical F).IsStrawsonUE = ∀ (p : F.Param), Monotone (F.op p)
• (PolarityItem.Licenser.scalar { toOperatorFamily := F, exhaustified := exhaustified }).IsStrawsonUE = ∀ (p : F.Param), Monotone (F.op p)
• (PolarityItem.Licenser.strawson F).IsStrawsonUE = ∀ (p : F.Param), NaturalLogic.IsStrawsonUE (F.op p)
• (PolarityItem.Licenser.modal F).IsStrawsonUE = False
• PolarityItem.Licenser.question.IsStrawsonUE = False

def PolarityItem.Licenser.Carries (L : Licenser) : DEStrength → Prop

A licenser carries weak strength when it is downward and not upward entailing modulo presupposition, the condition every negative polarity item puts on the meaning below the exhaustivity operator ([vF99a], [Gaj11]'s Condition 1, [BN18]'s (53)), and a stronger strength when it also holds that strength outright with its direct implicature factored in.

Equations

• L.Carries PolarityItem.DEStrength.weak = (L.IsStrawsonDE ∧ ¬L.IsStrawsonUE)
• L.Carries x✝ = ((L.IsStrawsonDE ∧ ¬L.IsStrawsonUE) ∧ L.exhaustified.Holds x✝.toSignature)

def PolarityItem.Licenser.mechanism : Licenser → LicensingMechanism

The route by which a licenser licenses.

Equations

• (PolarityItem.Licenser.classical F).mechanism = PolarityItem.LicensingMechanism.strengthening
• (PolarityItem.Licenser.scalar F).mechanism = PolarityItem.LicensingMechanism.strengthening
• (PolarityItem.Licenser.strawson F).mechanism = PolarityItem.LicensingMechanism.strengthening
• (PolarityItem.Licenser.modal F).mechanism = PolarityItem.LicensingMechanism.genericIndefinite
• PolarityItem.Licenser.question.mechanism = PolarityItem.LicensingMechanism.entropy

def PolarityItem.Licenser.LicensesFreeChoice : Licenser → Prop

A modal licenser licenses free choice when, under one of its operators and over a domain of at least two possible witnesses, the antiexhaustified existential is consistent ([Chi06]).

Equations

• One or more equations did not get rendered due to their size.
• (PolarityItem.Licenser.classical F).LicensesFreeChoice = False
• (PolarityItem.Licenser.scalar F).LicensesFreeChoice = False
• (PolarityItem.Licenser.strawson F).LicensesFreeChoice = False
• PolarityItem.Licenser.question.LicensesFreeChoice = False

def PolarityItem.Licenser.LicensesByRelevance : Licenser → Prop

A question licenses a domain widener by relevance, since widening the domain of a wh-question never lowers its value in any decision problem ([vR03a]).

Equations

• One or more equations did not get rendered due to their size.
• (PolarityItem.Licenser.classical F).LicensesByRelevance = False
• (PolarityItem.Licenser.scalar F).LicensesByRelevance = False
• (PolarityItem.Licenser.strawson F).LicensesByRelevance = False
• (PolarityItem.Licenser.modal F).LicensesByRelevance = False

theorem PolarityItem.Licenser.licensesByRelevance_question : question.LicensesByRelevance

theorem PolarityItem.Licenser.Holds.of_le {L : Licenser} {σ τ : NaturalLogic.Signature} (h : L.Holds σ) (hστ : σ ≤ τ) : L.Holds τ

theorem PolarityItem.Licenser.Holds.toSignature_of_le {L : Licenser} {s t : DEStrength} (h : L.Holds t.toSignature) (hst : s ≤ t) : L.Holds s.toSignature

theorem PolarityItem.Licenser.isStrawsonDE_of_holds_anti {L : Licenser} (h : L.Holds NaturalLogic.Signature.anti) : L.IsStrawsonDE

theorem PolarityItem.Licenser.Carries.weak {L : Licenser} {s : DEStrength} (h : L.Carries s) : L.Carries DEStrength.weak

theorem PolarityItem.Licenser.Carries.of_le {L : Licenser} {s t : DEStrength} (h : L.Carries s) (hts : t ≤ s) : L.Carries t

Carrying a strength carries every weaker one.

theorem PolarityItem.Licenser.carries_iff_of_ne_weak {L : Licenser} {s : DEStrength} (hs : s ≠ DEStrength.weak) : L.Carries s ↔ L.Carries DEStrength.weak ∧ L.exhaustified.Holds s.toSignature

theorem PolarityItem.Licenser.carries_classical_iff {s : DEStrength} {F : OperatorFamily} : (classical F).Carries s ↔ (classical F).Holds s.toSignature ∧ ¬(classical F).IsStrawsonUE

A classical licenser carries a strength exactly when it holds it outright and is non-trivial.

theorem PolarityItem.Licenser.holds_toSignature_iff {L : Licenser} {s s₀ : DEStrength} (h : L.Holds s₀.toSignature) (hn : ∀ (s : DEStrength), s₀ < s → ¬L.Holds s.toSignature) : L.Holds s.toSignature ↔ s ≤ s₀

A licenser holding exactly the strength s₀ outright holds s exactly when s ≤ s₀.

theorem PolarityItem.Licenser.not_holds_toSignature {L : Licenser} {s : DEStrength} (h : ¬L.Holds NaturalLogic.Signature.anti) : ¬L.Holds s.toSignature

A licenser holding no strength outright holds none.

theorem PolarityItem.Licenser.carries_iff_eq_weak {L : Licenser} {s : DEStrength} (hde : L.IsStrawsonDE) (hn : ¬L.IsStrawsonUE) (h : ¬L.exhaustified.Holds NaturalLogic.Signature.anti) : L.Carries s ↔ s = DEStrength.weak

A non-trivial licenser that is downward entailing modulo presupposition, and not outright once its direct implicature is factored in, carries exactly weak strength ([Gaj11]).