Licensing contexts

A licensing context is a construction that can host a polarity item. It places a licenser over the item and realizes a function of Haspelmath's implicational map, where it realizes one, and what its licenser carries is a theorem about the operators it denotes. Clausal negation is anti-morphic. Nobody, the restrictor of a universal, without, deny, before, too … to and the clausal comparative are anti-additive and no more, and doubt downward entailing and no more. Few and at most are scalar: downward entailing, and not even that once exhaustified against the stronger no and at most n − 1, the determiner exhaustification Quantifier.GQ.exhaustified. Every downward entailing context is so non-trivially. Focus only, adversatives, superlatives, conditional antecedents and temporal since are downward entailing only modulo their presuppositions, the modals, imperatives, generics and free relatives are modal licensers, and questions license by relevance. A study can state the theory of a licenser of its own; the named constructions are the shared inventory that lexical entries cite.

Main declarations

• PolarityItem.LicensingContext: the named constructions.
• PolarityItem.LicensingContext.licenser, PolarityItem.LicensingContext.haspelmath: the operator a construction places over the item and its function on Haspelmath's map.
• Quantifier.GQ.exhaustified: a determiner exhaustified against its scale-mates.
• PolarityItem.LicensingContext.holds_negation, holds_nobody_iff, not_isStrawsonUE_nobody, not_holds_exhaustified_few, …: the certificates of each context's licenser.

Implementation notes

• A context is a name, so the lexical entries that list the contexts an item is attested in are computable data with decidable equality, while the licenser, often defined classically, is a function of the name. Distinct constructions can share a licenser: the necessity modal, the imperative, the generic and the free relative are all necessities, and the clausal comparative and too … to both exceed the clause's degrees.
• The inventory is the contexts the library gives a semantics, not an exhaustive list. It realizes six of Haspelmath's nine functions; the irrealis non-specific function, where nonveridical rather than downward-entailing operators license, has no context yet, and neither do many licensers of the downward-entailing literature, such as negative adverbs, neither … nor, the restrictor of no or not every.
• Before is Anscombe's universal reading, before ever. Too … to is the subject's degree exceeding every degree at which the infinitive holds, after Meier. Doubt is not believing and deny asserting the negation, over a doxastic or assertoric accessibility.
• The free relative is read as a necessity over its alternatives, with the modal presupposition of -ever; the generic is a necessity over normal worlds.
• Haspelmath's placements are his book's. Nobody, before-clauses and adversatives sit between direct and indirect negation there, so they realize no function here, nor do the rows outside the map's inventory.

References

• [Lad79]
• [Zwa98]
• [vdW97]
• [vF99a]
• [Gaj11]
• [BN18]
• [Ans64]
• [Hoe83]
• [Mei03]
• [Chi06]
• [KL93]
• [vR03a]
• [Has97]

Determiners exhaustified against their scale-mates

def Quantifier.GQ.exhaustified {α : Type u_1} (Q : GQ α) (C : Set (GQ α)) : GQ α

The determiner Q exhaustified against its scale-mates C holds, at each restrictor, of the scopes where Q holds and every scale-mate holding there is entailed, entailment holding the restrictor fixed and quantifying over scopes ([Gaj11]'s O with ALT-1).

Equations

• Q.exhaustified C A = Exhaustification.exh ((fun (x : Quantifier.GQ α) => x A) '' C) (Q A)

theorem Quantifier.GQ.exhaustified_iff {α : Type u_1} {Q : GQ α} {C : Set (GQ α)} {A P : α → Prop} : Q.exhaustified C A P ↔ Q A P ∧ ∀ Q' ∈ C, Q' A P → Q A ≤ Q' A

theorem Quantifier.GQ.not_exhaustified_of_not_le {α : Type u_1} {Q Q' : GQ α} {C : Set (GQ α)} {A P : α → Prop} (hQ' : Q' ∈ C) (hP : Q' A P) (h : ¬Q A ≤ Q' A) : ¬Q.exhaustified C A P

A scale-mate holding but not entailed is excluded.

theorem Quantifier.GQ.exhaustified_eq_of_forall_le {α : Type u_1} {Q : GQ α} {C : Set (GQ α)} {A : α → Prop} (h : ∀ Q' ∈ C, ∀ (P : α → Prop), Q' A P → Q A ≤ Q' A) : Q.exhaustified C A = Q A

At the bottom of its scale a determiner is its own exhaustification.

theorem Quantifier.GQ.exhaustified_no {α : Type u_1} : no.exhaustified {everyᶜ} = no

No is the bottom of its scale, so exhaustified no is no.

inductive PolarityItem.LicensingContext : Type

A licensing context is a construction that can host a polarity item. What it does to the item is the licenser it places over the item's position (LicensingContext.licenser), and where it sits typologically is the function of [Has97]'s implicational map it realizes (LicensingContext.haspelmath). Distinct constructions can share a licenser, as the necessity modal, the imperative, the generic and the free relative do.

• negation : LicensingContext

  Clausal negation, as in not, complement over predicates.

• nobody : LicensingContext

  A negative quantifier, as in nobody, over a restrictor true of something.

• few : LicensingContext

  Few NP, the proportional reading of the English fragment, below the stronger no on its scale.

• atMost : LicensingContext

  At most n NP, below the stronger at most n − 1 on its scale.

• universalRestrictor : LicensingContext

  The restrictor of a universal, as in everyone who, over a scope false of something.

• withoutClause : LicensingContext

  A without-phrase, the matrix predicate holding without the phrase's.

• beforeClause : LicensingContext

  A before-clause, Anscombe's universal before.

• clausalComparative : LicensingContext

  A clausal comparative, taller than S, the individual above every degree of the clause.

• tooTo : LicensingContext

  Too ADJ to VP, the individual above every degree at which the infinitive holds.

• doubtVerb : LicensingContext

  A verb of doubting, as in I doubt that, which does not believe its complement.

• denyVerb : LicensingContext

  A verb of denying, as in she denied that, which asserts the negation of its complement.

• onlyFocus : LicensingContext

  The scope of focus only, von Fintel's only.

• adversative : LicensingContext

  An adversative predicate, as in sorry, surprised, regret.

• superlative : LicensingContext

  A superlative, in its comparison class.

• conditionalAntecedent : LicensingContext

  The antecedent of a conditional, the modal-horizon counterfactual.

• sinceTemporal : LicensingContext

  Temporal since, as in it's been five years since.

• question : LicensingContext

  A question.

• modalPossibility : LicensingContext

  A possibility modal.

• modalNecessity : LicensingContext

  A necessity modal.

• imperative : LicensingContext

  An imperative, a necessity over what is commanded.

• generic : LicensingContext

  A generic sentence, a necessity over normal worlds.

• freeRelative : LicensingContext

  A free relative, as in whatever, whoever, a necessity over its alternatives.

@[instance_reducible]

instance PolarityItem.instDecidableEqLicensingContext : DecidableEq LicensingContext

Equations

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

@[instance_reducible]

instance PolarityItem.instFintypeLicensingContext : Fintype LicensingContext

Equations

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

@[instance_reducible]

instance PolarityItem.instReprLicensingContext : Repr LicensingContext

Equations

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

def PolarityItem.instReprLicensingContext.repr : LicensingContext → ℕ → Std.Format

Equations

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

def PolarityItem.LicensingContext.haspelmath : LicensingContext → Option Indefinite.HaspelmathFunction

The function of [Has97]'s implicational map a construction realizes, if any.

Equations

• PolarityItem.LicensingContext.negation.haspelmath = some Indefinite.HaspelmathFunction.directNeg
• PolarityItem.LicensingContext.withoutClause.haspelmath = some Indefinite.HaspelmathFunction.indirectNeg
• PolarityItem.LicensingContext.doubtVerb.haspelmath = some Indefinite.HaspelmathFunction.indirectNeg
• PolarityItem.LicensingContext.denyVerb.haspelmath = some Indefinite.HaspelmathFunction.indirectNeg
• PolarityItem.LicensingContext.clausalComparative.haspelmath = some Indefinite.HaspelmathFunction.comparative
• PolarityItem.LicensingContext.conditionalAntecedent.haspelmath = some Indefinite.HaspelmathFunction.conditional
• PolarityItem.LicensingContext.question.haspelmath = some Indefinite.HaspelmathFunction.question
• PolarityItem.LicensingContext.modalPossibility.haspelmath = some Indefinite.HaspelmathFunction.freeChoice
• PolarityItem.LicensingContext.modalNecessity.haspelmath = some Indefinite.HaspelmathFunction.freeChoice
• PolarityItem.LicensingContext.imperative.haspelmath = some Indefinite.HaspelmathFunction.freeChoice
• PolarityItem.LicensingContext.generic.haspelmath = some Indefinite.HaspelmathFunction.freeChoice
• PolarityItem.LicensingContext.freeRelative.haspelmath = some Indefinite.HaspelmathFunction.freeChoice
• PolarityItem.LicensingContext.nobody.haspelmath = none
• PolarityItem.LicensingContext.few.haspelmath = none
• PolarityItem.LicensingContext.atMost.haspelmath = none
• PolarityItem.LicensingContext.universalRestrictor.haspelmath = none
• PolarityItem.LicensingContext.beforeClause.haspelmath = none
• PolarityItem.LicensingContext.tooTo.haspelmath = none
• PolarityItem.LicensingContext.onlyFocus.haspelmath = none
• PolarityItem.LicensingContext.adversative.haspelmath = none
• PolarityItem.LicensingContext.superlative.haspelmath = none
• PolarityItem.LicensingContext.sinceTemporal.haspelmath = none

The parameters of the operator families

structure PolarityItem.Predicate : Type 1

A domain of individuals and a predicate over it.

• ι : Type

  The individuals.

• A : self.ι → Prop

  The predicate.

structure PolarityItem.FinitePredicateextends PolarityItem.Predicate : Type 1

A finite domain and a predicate over it.

• ι : Type
• A : self.ι → Prop
• fin : Fintype self.ι

  The domain is finite.

structure PolarityItem.NonemptyPredicateextends PolarityItem.Predicate : Type 1

A predicate true of something, the restrictor of a negative quantifier.

• ι : Type
• A : self.ι → Prop
• nonempty : ∃ (x : self.ι), self.A x

structure PolarityItem.NonuniversalPredicateextends PolarityItem.Predicate : Type 1

A predicate false of something, the scope of a universal.

• ι : Type
• A : self.ι → Prop
• nonuniversal : ∃ (x : self.ι), ¬self.A x

structure PolarityItem.BoundedPredicateextends PolarityItem.FinitePredicate : Type 1

A bound and a finite predicate, the restrictor of at most n.

• ι : Type
• A : self.ι → Prop
• fin : Fintype self.ι
• n : ℕ

  The bound.

structure PolarityItem.MainClause : Type 1

A time line and the run times of a main clause.

• T : Type

  The times.

• ord : LinearOrder self.T

  The times are linearly ordered.

• A : Set (NonemptyInterval self.T)

  The run times of the main clause.

structure PolarityItem.Measured : Type 1

A measure of individuals on a linearly ordered scale, and the individual compared.

• E : Type

  The individuals.

• D : Type

  The degrees.

• ord : LinearOrder self.D

  The degrees are linearly ordered.

• μ : self.E → self.D

  The measure.

• x : self.E

  The individual compared.

structure PolarityItem.Accessibility : Type 1

An accessibility relation over worlds, and the evaluation world.

• W : Type

  The worlds.

• R : SetRel self.W self.W

  The accessibility relation.

• w : self.W

  The evaluation world.

structure PolarityItem.SerialAccessibilityextends PolarityItem.Accessibility : Type 1

An accessibility relation with a world accessible from the evaluation world.

• W : Type
• R : SetRel self.W self.W
• w : self.W
• serial : ∃ (v : self.W), (self.w, v) ∈ self.R

structure PolarityItem.Frame : Type 1

An accessibility relation over worlds.

• W : Type

  The worlds.

• R : SetRel self.W self.W

  The accessibility relation.

structure PolarityItem.Focus : Type 1

A focused individual among others, over worlds.

• ι : Type

  The individuals.

• W : Type

  The worlds.

• x : self.ι

  The focused individual.

structure PolarityItem.Attitude : Type 1

The doxastic state, the domain and the ordering source of an adversative attitude.

• W : Type

  The worlds.

• dox : self.W → Set self.W

  The doxastic state.

• base : self.W → Set self.W

  The domain.

• g : self.W → Set (self.W → Prop)

  The ordering source.

structure PolarityItem.Superlative : Type 1

A measure of the members of a comparison class, and the individual described.

• α : Type

  The individuals.

• W : Type

  The worlds.

• D : Type

  The degrees.

• pre : Preorder self.D

  The degrees are preordered.

• μ : self.α → self.D

  The measure.

• x : self.α

  The individual described.

structure PolarityItem.Horizon : Type 1

The modal horizon and the consequent of a counterfactual.

• I : Type

  The evaluation indices.

• W : Type

  The worlds.

• horizon : self.I → Set self.W

  The modal horizon.

• q : Set self.W

  The consequent.

structure PolarityItem.Ago : Type 1

A time line and the shift back to the reference time of since.

• T : Type

  The times.

• ord : LinearOrder self.T

  The times are linearly ordered.

• ago : self.T → self.T

  The shift back.

The licensers of the contexts

@[reducible, inline]

abbrev PolarityItem.LicensingContext.exceedsFamily : OperatorFamily

The degrees a clause leaves the compared individual above.

Equations

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

@[reducible, inline]

abbrev PolarityItem.LicensingContext.necessityFamily : ModalFamily

Necessity over a frame.

Equations

• PolarityItem.LicensingContext.necessityFamily = { Param := PolarityItem.Frame, W := fun (p : PolarityItem.Frame) => p.W, op := fun (p : PolarityItem.Frame) => p.R.core }

noncomputable def PolarityItem.LicensingContext.licenser : LicensingContext → Licenser

The licenser a construction places over the position of a polarity item.

Equations

• One or more equations did not get rendered due to their size.
• PolarityItem.LicensingContext.clausalComparative.licenser = PolarityItem.Licenser.classical PolarityItem.LicensingContext.exceedsFamily
• PolarityItem.LicensingContext.tooTo.licenser = PolarityItem.Licenser.classical PolarityItem.LicensingContext.exceedsFamily
• PolarityItem.LicensingContext.question.licenser = PolarityItem.Licenser.question
• PolarityItem.LicensingContext.modalNecessity.licenser = PolarityItem.Licenser.modal PolarityItem.LicensingContext.necessityFamily
• PolarityItem.LicensingContext.imperative.licenser = PolarityItem.Licenser.modal PolarityItem.LicensingContext.necessityFamily
• PolarityItem.LicensingContext.generic.licenser = PolarityItem.Licenser.modal PolarityItem.LicensingContext.necessityFamily
• PolarityItem.LicensingContext.freeRelative.licenser = PolarityItem.Licenser.modal PolarityItem.LicensingContext.necessityFamily

Classical licensers

theorem PolarityItem.LicensingContext.holds_negation (s : DEStrength) : negation.licenser.Holds s.toSignature

theorem PolarityItem.LicensingContext.holds_nobody_iff {s : DEStrength} : nobody.licenser.Holds s.toSignature ↔ s ≤ DEStrength.antiAdditive

theorem PolarityItem.LicensingContext.holds_few_iff {s : DEStrength} : few.licenser.Holds s.toSignature ↔ s ≤ DEStrength.weak

theorem PolarityItem.LicensingContext.holds_atMost_iff {s : DEStrength} : atMost.licenser.Holds s.toSignature ↔ s ≤ DEStrength.weak

theorem PolarityItem.LicensingContext.holds_universalRestrictor_iff {s : DEStrength} : universalRestrictor.licenser.Holds s.toSignature ↔ s ≤ DEStrength.antiAdditive

theorem PolarityItem.LicensingContext.holds_withoutClause_iff {s : DEStrength} : withoutClause.licenser.Holds s.toSignature ↔ s ≤ DEStrength.antiAdditive

theorem PolarityItem.LicensingContext.holds_beforeClause_iff {s : DEStrength} : beforeClause.licenser.Holds s.toSignature ↔ s ≤ DEStrength.antiAdditive

theorem PolarityItem.LicensingContext.holds_exceedsFamily_iff {s : DEStrength} : (Licenser.classical exceedsFamily).Holds s.toSignature ↔ s ≤ DEStrength.antiAdditive

theorem PolarityItem.LicensingContext.holds_clausalComparative_iff {s : DEStrength} : clausalComparative.licenser.Holds s.toSignature ↔ s ≤ DEStrength.antiAdditive

theorem PolarityItem.LicensingContext.holds_tooTo_iff {s : DEStrength} : tooTo.licenser.Holds s.toSignature ↔ s ≤ DEStrength.antiAdditive

theorem PolarityItem.LicensingContext.holds_doubtVerb_iff {s : DEStrength} : doubtVerb.licenser.Holds s.toSignature ↔ s ≤ DEStrength.weak

theorem PolarityItem.LicensingContext.holds_denyVerb_iff {s : DEStrength} : denyVerb.licenser.Holds s.toSignature ↔ s ≤ DEStrength.antiAdditive

Non-triviality

Each downward entailing licenser has an operator that is not upward entailing, so it is not downward entailing by being constant.

theorem PolarityItem.LicensingContext.not_isStrawsonUE_negation : ¬negation.licenser.IsStrawsonUE

theorem PolarityItem.LicensingContext.not_isStrawsonUE_nobody : ¬nobody.licenser.IsStrawsonUE

theorem PolarityItem.LicensingContext.not_isStrawsonUE_few : ¬few.licenser.IsStrawsonUE

theorem PolarityItem.LicensingContext.not_isStrawsonUE_atMost : ¬atMost.licenser.IsStrawsonUE

theorem PolarityItem.LicensingContext.not_isStrawsonUE_universalRestrictor : ¬universalRestrictor.licenser.IsStrawsonUE

theorem PolarityItem.LicensingContext.not_isStrawsonUE_withoutClause : ¬withoutClause.licenser.IsStrawsonUE

theorem PolarityItem.LicensingContext.not_isStrawsonUE_beforeClause : ¬beforeClause.licenser.IsStrawsonUE

theorem PolarityItem.LicensingContext.not_isStrawsonUE_exceedsFamily : ¬(Licenser.classical exceedsFamily).IsStrawsonUE

theorem PolarityItem.LicensingContext.not_isStrawsonUE_doubtVerb : ¬doubtVerb.licenser.IsStrawsonUE

theorem PolarityItem.LicensingContext.not_isStrawsonUE_denyVerb : ¬denyVerb.licenser.IsStrawsonUE

theorem PolarityItem.LicensingContext.not_isStrawsonUE_onlyFocus : ¬onlyFocus.licenser.IsStrawsonUE

theorem PolarityItem.LicensingContext.not_isStrawsonUE_adversative : ¬adversative.licenser.IsStrawsonUE

theorem PolarityItem.LicensingContext.not_isStrawsonUE_superlative : ¬superlative.licenser.IsStrawsonUE

theorem PolarityItem.LicensingContext.not_isStrawsonUE_conditionalAntecedent : ¬conditionalAntecedent.licenser.IsStrawsonUE

theorem PolarityItem.LicensingContext.not_isStrawsonUE_sinceTemporal : ¬sinceTemporal.licenser.IsStrawsonUE

Scalar licensers

Few and at most n exhaustified against their stronger scale-mates assert some, so they are not downward entailing ([Gaj11]'s (45), (48)).

theorem PolarityItem.LicensingContext.not_holds_exhaustified_few : ¬few.licenser.exhaustified.Holds NaturalLogic.Signature.anti

theorem PolarityItem.LicensingContext.not_holds_exhaustified_atMost : ¬atMost.licenser.exhaustified.Holds NaturalLogic.Signature.anti

Strawson licensers

theorem PolarityItem.LicensingContext.isStrawsonDE_onlyFocus : onlyFocus.licenser.IsStrawsonDE

theorem PolarityItem.LicensingContext.not_holds_onlyFocus : ¬onlyFocus.licenser.Holds NaturalLogic.Signature.anti

theorem PolarityItem.LicensingContext.isStrawsonDE_adversative : adversative.licenser.IsStrawsonDE

theorem PolarityItem.LicensingContext.not_holds_adversative : ¬adversative.licenser.Holds NaturalLogic.Signature.anti

theorem PolarityItem.LicensingContext.isStrawsonDE_superlative : superlative.licenser.IsStrawsonDE

theorem PolarityItem.LicensingContext.not_holds_superlative : ¬superlative.licenser.Holds NaturalLogic.Signature.anti

theorem PolarityItem.LicensingContext.isStrawsonDE_conditionalAntecedent : conditionalAntecedent.licenser.IsStrawsonDE

theorem PolarityItem.LicensingContext.not_holds_conditionalAntecedent : ¬conditionalAntecedent.licenser.Holds NaturalLogic.Signature.anti

theorem PolarityItem.LicensingContext.isStrawsonDE_sinceTemporal : sinceTemporal.licenser.IsStrawsonDE

theorem PolarityItem.LicensingContext.not_holds_sinceTemporal : ¬sinceTemporal.licenser.Holds NaturalLogic.Signature.anti

Modal licensers and questions

theorem PolarityItem.LicensingContext.licensesFreeChoice_necessityFamily : (Licenser.modal necessityFamily).LicensesFreeChoice

theorem PolarityItem.LicensingContext.licensesFreeChoice_modalPossibility : modalPossibility.licenser.LicensesFreeChoice