Kadmon & Landman (1993): Any

@cite{kadmon-landman-1993}

Kadmon, N. & Landman, F. (1993). Any. Linguistics and Philosophy 16: 353–422.

The Unified Analysis

K&L propose a unified analysis of polarity-sensitive (PS) any and free choice (FC) any. The word any is unambiguous: it is always an indefinite that contributes widening and strengthening. The PS/FC difference reduces to whether the indefinite NP is interpreted episodically or generically.

The analysis has four components:

• (A) any CN = the corresponding indefinite a CN + widening + strengthening
• (FC) PS any is a regular indefinite; FC any is a generic indefinite
• (B) Widening: any widens the CN denotation along a contextual dimension
• (C) Strengthening: any is licensed only if widening creates a stronger statement (wide interpretation ⇒ narrow interpretation)
• (D) Locality: Strengthening is checked at the local proposition level

Unification with Entailment Signatures

K&L's strengthening condition subsumes @cite{ladusaw-1979}'s DE condition: widening an existential strengthens the embedding statement exactly when the context is DE. But K&L's formulation is deeper — it explains why DE contexts license and relates the distribution to the meaning of any itself. Moreover, K&L show that DE is more pervasive than Ladusaw recognized: adversative predicates are DE on a constant perspective (§3.3), and conditional antecedents are DE on a constant implicit restriction (§3.5). The only genuinely non-DE licensing K&L identify is metalinguistic: any in negated because-clauses is licensed by strengthening the denial of a factive presupposition (§3.4).

This file bridges K&L's analysis to the EntailmentSig lattice from Core.Logic.NaturalLogic, providing a principled derivation of each LicensingContext from the strengthening condition rather than stipulating the list.

Sorry vs Glad

K&L's most striking empirical contribution: adversative predicates (surprised, sorry) license any because they are DE on a constant perspective, while non-adversatives (glad, sure) are not DE and do not freely license any. The difference traces to lexical semantics: sorry that A entails want ¬A, while glad that A entails want A.

The Strengthening Condition

K&L's principle (C): any is licensed only if widening creates a stronger statement. For assertions, "stronger" = entailment. For a context C and domains D ⊆ D' (narrow ⊆ wide):

C(∃x∈D', Px) ⊆ C(∃x∈D, Px)    — the wide interpretation entails the narrow

This holds exactly when C is DE (antitone). K&L's insight is that this is not a coincidence: it is because any widens that it must create a stronger statement, and it is because DE reverses entailment that widening in DE contexts strengthens.

def KadmonLandman1993.klStrengthening {World : Type u_1} {Entity : Type u_2} (C : Exhaustification.FreeChoice.Ctx World) (D D' : Set Entity) (P : Entity → Set World) (_hD : D ⊆ D') : Prop

K&L's strengthening condition: widening domain D to D' in context C creates a stronger statement.

This is the central licensing predicate. Any is licensed in context C iff klStrengthening holds for the relevant widening.

Equations

• KadmonLandman1993.klStrengthening C D D' P _hD = (C (Exhaustification.FreeChoice.existsInDomain D' P) ⊆ C (Exhaustification.FreeChoice.existsInDomain D P))

theorem KadmonLandman1993.de_satisfies_strengthening {World : Type u_1} {Entity : Type u_2} (C : Exhaustification.FreeChoice.Ctx World) (hDE : ∀ (p q : Set World), p ⊆ q → C q ⊆ C p) (D D' : Set Entity) (P : Entity → Set World) (hD : D ⊆ D') : klStrengthening C D D' P hD

Theorem (K&L → Ladusaw). In any DE context, strengthening is automatically satisfied.

This is the formal content of K&L's claim that their analysis "makes the same predictions as Ladusaw's" for standard cases. The proof delegates to widening_strengthens_in_de from FreeChoice.lean.

theorem KadmonLandman1993.ue_violates_strengthening {World : Type u_1} {Entity : Type u_2} (C : Exhaustification.FreeChoice.Ctx World) (hUE : ∀ (p q : Set World), p ⊆ q → C p ⊆ C q) (D D' : Set Entity) (P : Entity → Set World) (hD : D ⊆ D') : C (Exhaustification.FreeChoice.existsInDomain D P) ⊆ C (Exhaustification.FreeChoice.existsInDomain D' P)

Theorem (Strengthening fails in UE). In UE contexts, widening weakens — the opposite of strengthening. This is why any is ungrammatical in positive contexts.

The Unification: LicensingContext → EntailmentSig

The two LicensingContext types in linglib (Core: 19 constructors, Phenomena: 15 constructors) list licensing environments as a surface inventory. K&L's analysis provides the explanatory principle: each context has an entailment signature, and any is licensed when that signature guarantees strengthening.

The function below maps each licensing context to its entailment signature in Icard's lattice. This replaces the stipulated list with a derived classification: contexts license any because their entailment signature is on the DE side, not because they appear on an enumerated list.

@[reducible, inline]

abbrev KadmonLandman1993.contextEntailmentSig (c : Features.LicensingContext) : Core.NaturalLogic.EntailmentSig

Each licensing context's entailment signature, projected from the canonical Semantics.Polarity.Licensing.contextProperties mapping.

Contexts on the DE side (anti, antiAdd, antiAddMult) guarantee strengthening. Contexts that are not monotone (questions, superlatives) license any via other mechanisms (entropy, Strawson-DE) — their signatures are .mono or higher, indicating that plain DE-based strengthening is not the explanation.

This mapping unifies the surface inventory with the algebraic hierarchy from @cite{icard-2012}.

Equations

• KadmonLandman1993.contextEntailmentSig c = (Semantics.Polarity.Licensing.contextProperties c).signature

def KadmonLandman1993.guaranteesStrengthening (ctx : Features.LicensingContext) : Bool

A licensing context guarantees K&L strengthening iff its entailment signature is on the DE side.

Equations

• KadmonLandman1993.guaranteesStrengthening ctx = match (KadmonLandman1993.contextEntailmentSig ctx).toDEStrength with | some val => true | none => false

@[reducible, inline]

abbrev KadmonLandman1993.klExplanation (c : Features.LicensingContext) : Semantics.Polarity.Licensing.LicensingMechanism

Each context's K&L licensing mechanism, projected from contextProperties.

This is the unifying function: instead of stipulating that each context licenses, we explain why.

Equations

• KadmonLandman1993.klExplanation c = (Semantics.Polarity.Licensing.contextProperties c).mechanism

theorem KadmonLandman1993.strengthening_implies_de (ctx : Features.LicensingContext) (h : klExplanation ctx = Semantics.Polarity.Licensing.LicensingMechanism.byStrengthening) : guaranteesStrengthening ctx = true

Consistency check: every context classified as byStrengthening has a DE entailment signature. After Phase 1 unification, both sides project from a single contextProperties map, so the check reduces to concrete enum-case verification.

Compatibility with Ladusaw (1979)

K&L's classification refines @cite{ladusaw-1979}'s: every context that Ladusaw classifies as DE is also classified as byStrengthening by K&L. But K&L additionally explains adversative predicates and conditionals with implicit restrictions — cases where Ladusaw's DE condition is necessary but not sufficient for a full account.

theorem KadmonLandman1993.ladusaw_de_is_kl_strengthening (ctx : Features.LicensingContext) (hDE : Ladusaw1979.licensingStrength ctx = Ladusaw1979.LicensingStrength.antiAdditive ∨ Ladusaw1979.licensingStrength ctx = Ladusaw1979.LicensingStrength.downwardEntailing) : klExplanation ctx = Semantics.Polarity.Licensing.LicensingMechanism.byStrengthening

Ladusaw's DE contexts are always K&L strengthening contexts.

If Ladusaw classifies a context as DE or anti-additive, K&L explains it as byStrengthening. K&L's analysis is strictly more explanatory: Ladusaw describes where NPIs occur (DE contexts), K&L explains why (widening + strengthening).

Adversative Predicates (K&L §3.3)

K&L's analysis of sorry vs glad is one of the paper's most important empirical contributions. The key insight:

• sorry that A ↔ want ¬A (lexical entailment)
• glad that A ↔ want A (lexical entailment)

For sorry: sorry(A) entails want(¬A). If I'm sorry that a set is nonempty, I want it empty. But wanting a set empty → wanting all subsets empty. So the wide interpretation (wider set nonempty) entails the narrow (narrower set nonempty). Strengthening holds → any is licensed.

For glad: glad(A) entails want(A). Wanting a set to have members does NOT entail wanting each particular subset to have members — the wish could be satisfied another way. Strengthening fails → any is not freely licensed.

The formal content is derived from StrawsonEntailment.lean: sorryFull is Strawson-DE, gladFull is UE. The lexical semantics of sorry (= factive + adversative preference) and glad (= factive + congruent preference) directly determine their monotonicity properties. K&L's "DE on a constant perspective" corresponds to bestOf being held constant — the bestOf parameter is the "perspective" in K&L's three-place relation.

theorem KadmonLandman1993.sorry_licenses_any (dox bestOf : Semantics.Entailment.World → Set Semantics.Entailment.World) : Semantics.Entailment.StrawsonEntailment.IsStrawsonDE (Semantics.Entailment.StrawsonEntailment.sorryFull dox bestOf) fun (p : Set Semantics.Entailment.World) (w : Semantics.Entailment.World) => ∀ w' ∈ dox w, p w'

K&L's prediction derived: sorry licenses NPIs because it is Strawson-DE — DE on a constant perspective (the bestOf parameter).

The proof is imported from StrawsonEntailment.sorryFull_isStrawsonDE. K&L's lexical-semantic argument (sorry → want ¬A → "wanting emptiness is DE") is captured by the contraposition step in that proof: p ≤ q and ¬q(w') implies ¬p(w') at all best worlds.

theorem KadmonLandman1993.sorry_not_classically_de : ¬Semantics.Entailment.Polarity.IsDownwardEntailing (Semantics.Entailment.StrawsonEntailment.sorryFull (fun (w : Semantics.Entailment.World) => {w}) fun (x : Semantics.Entailment.World) => {Semantics.Entailment.World.w1})

K&L's prediction derived: sorry is NOT classically DE — the doxastic factivity presupposition blocks it.

theorem KadmonLandman1993.glad_does_not_license (dox bestOf : Semantics.Entailment.World → Set Semantics.Entailment.World) : Monotone (Semantics.Entailment.StrawsonEntailment.gladFull dox bestOf)

K&L's prediction derived: glad does NOT license NPIs because it is UE — wider scope entails narrower scope in the SAME direction, so widening weakens rather than strengthens.

K&L: "wanting a set to have members does not entail wanting each particular subset to have members. My wish could be satisfied in another way."

structure KadmonLandman1993.SettleForLessDatum : Type

K&L's "settle for less" analysis (§3.3.2): glad CAN license any on a special interpretation where the speaker settles for less than what they really want.

"Be glad we got ANY tickets!" conveys: (1) What I really want is better tickets. (2) Nobody who really counts likes us. (3) I settle for less — a phonologist likes me, I'm glad about that.

On this reading, the "narrow wish" (phonologist likes me) is PREFERRED to the "wide wish" (linguist likes me). This preference reversal creates strengthening: if I'd settle for a phonologist liking me, I'd certainly settle for a linguist liking me (the wider set).

The analysis does not contradict glad_does_not_license because the "settle for less" reading involves a different semantic structure: the preference relation between narrow and wide wishes is reversed.

• sentence : String
• grammatical : Bool
• notes : String

def KadmonLandman1993.settle_glad_tickets : SettleForLessDatum

Equations

• KadmonLandman1993.settle_glad_tickets = { sentence := "Be glad we got ANY tickets!", grammatical := true, notes := "settle for less: narrow wish preferred to wide wish" }

def KadmonLandman1993.settle_glad_anybody : SettleForLessDatum

Equations

• KadmonLandman1993.settle_glad_anybody = { sentence := "I'm glad ANYBODY likes me!", grammatical := true, notes := "settle for less: phonologist liking me ≻ linguist liking me" }

def KadmonLandman1993.sure_no_settle : SettleForLessDatum

Equations

• KadmonLandman1993.sure_no_settle = { sentence := "*I'm sure we got ANY tickets!", grammatical := false, notes := "sure has no settle-for-less interpretation" }

Conditional Antecedents and Implicit Restrictions (K&L §3.5)

K&L's analysis of any in conditional antecedents parallels their adversative analysis: both involve "DE on a constant parameter."

• Sorry: sorry(x, p, A) is DE in A when perspective p is held constant
• Conditionals: if_R(A, C) is DE in A when implicit restriction R is held constant

Under Kratzer's restrictor analysis (@cite{kratzer-1986}), "if A, must C" = necessity over the A-restricted modal base. The antecedent position is classically DE — strengthening the antecedent shrinks the domain, making the universal check easier to satisfy. Widening the antecedent domain therefore strengthens the conditional.

The formal proof is imported from StrawsonEntailment.conditional_antecedent_DE.

theorem KadmonLandman1993.conditional_satisfies_strengthening (domain : Semantics.Entailment.World → Set Semantics.Entailment.World) (β : Set Semantics.Entailment.World) : Semantics.Entailment.Polarity.IsDownwardEntailing fun (α : Set Semantics.Entailment.World) => Semantics.Entailment.StrawsonEntailment.condNecessity domain α β

K&L's prediction derived: conditional antecedents satisfy strengthening because the antecedent of conditional necessity is classically DE.

"If John subscribes to any newspaper, he gets well informed." Widening "newspaper" to include unimportant newspapers strengthens the conditional: if it holds for all newspapers (wide), it holds for important ones (narrow).

This connects K&L's "DE on a constant restriction" (§3.5) to the formal DE proof from StrawsonEntailment.lean. The domain parameter corresponds to Kratzer's modal base — the implicit restriction that is held constant.

theorem KadmonLandman1993.conditional_de_on_constant_domain (domain : Semantics.Entailment.World → Set Semantics.Entailment.World) (β : Set Semantics.Entailment.World) : Phenomena.Polarity.Studies.KadmonLandman1993.Apparatus.IsDE_OnConstant (fun (d : Semantics.Entailment.World → Set Semantics.Entailment.World) (α : Set Semantics.Entailment.World) => Semantics.Entailment.StrawsonEntailment.condNecessity d α β) domain

The conditional antecedent case and the adversative case are both instances of K&L's "DE on a constant parameter" pattern.

• condNecessity domain α β: DE in α, holding domain constant
• sorryFull bestOf p: Strawson-DE in p, holding bestOf constant

This is formalized by IsDE_OnConstant in the Apparatus sibling file: a multi-place function is DE in one argument when another is held constant. The difference: conditionals are classically DE (no presupposition), while adversatives are only Strawson-DE (factivity presupposition blocks classical DE).

Negated Because-Clauses (K&L §3.4)

K&L's analysis of any in negated because-clauses is the only genuinely non-DE licensing mechanism in the paper. The key empirical facts:

• (105) "It isn't because Sue said anything bad about me that I'm angry." — any licensed (grammatical)
• (106) "*I didn't help him because I have any sympathy for urban guerillas, although I do sympathize..." — any not licensed when the negative implication is canceled
• (109) Extended text where because-clause negation is natural (Linebarger 1987)

K&L argue, contra @cite{linebarger-1987}:

1. not because [S___] is NOT DE. K&L show that because [S___] is not upward-entailing (unlike because of [NP___]), so negating it does not produce a DE context.

2. not because of [NP___] IS DE. K&L demonstrate this with clear entailment patterns (pp. 391–392).

3. any in negated because-clauses is licensed metalinguistically: because carries a factive presupposition (the complement is true). The negation in these sentences denies this presupposition — it rejects the claim that because P is true. Any strengthens this presupposition denial: rejecting "because anybody read her paper that she's happy" is stronger than rejecting "because a linguist read her paper that she's happy."

This is structurally different from DE-based strengthening: the strengthening applies to the metalinguistic act of presupposition denial, not to the truth-conditional content. K&L explicitly note that this does not lead to the over-licensing problems of Linebarger's NI account (p. 398).

structure KadmonLandman1993.BecauseClauseDatum : Type

A because-clause licensing datum.

• sentence : String
• grammatical : Bool
• negativeImplication : Bool

  Whether the negative implication (presupposition denial) is present

• notes : String

def KadmonLandman1993.because_ex105 : BecauseClauseDatum

Equations

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

def KadmonLandman1993.because_ex106 : BecauseClauseDatum

Equations

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

def KadmonLandman1993.because_ex122 : BecauseClauseDatum

Equations

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

def KadmonLandman1993.because_ex125 : BecauseClauseDatum

Equations

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

def KadmonLandman1993.because_ex132 : BecauseClauseDatum

Equations

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

FC Any as Generic Indefinite (K&L §2.1, §4)

K&L's treatment of the PS/FC distinction:

• PS any: regular indefinite NP + widening + strengthening
• FC any: generic indefinite NP + widening + strengthening

The apparent universal force of FC any is not quantificational — it emerges from the combination of:

1. Generic interpretation (modal, law-like, exception-tolerating)
2. Widening (extends the CN along a contextual dimension)
3. The resulting dimensional universality (K&L §4.3)

This explains why:

• FC any shares properties with generic indefinites (exceptions, counterfactual entailments, law-like readings)
• almost can modify any owl (dimensionally universal) but not an owl (not dimensionally universal)
• FC any is "more universal" than regular generics (because widening eliminates some vagueness, creating dimensional universality)

inductive KadmonLandman1993.AnyInterpretation : Type

Classification of the NP containing any

• episodic : AnyInterpretation
• generic : AnyInterpretation

@[implicit_reducible]

instance KadmonLandman1993.instDecidableEqAnyInterpretation : DecidableEq AnyInterpretation

Equations

• KadmonLandman1993.instDecidableEqAnyInterpretation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KadmonLandman1993.instReprAnyInterpretation.repr : AnyInterpretation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KadmonLandman1993.instReprAnyInterpretation : Repr AnyInterpretation

Equations

• KadmonLandman1993.instReprAnyInterpretation = { reprPrec := KadmonLandman1993.instReprAnyInterpretation.repr }

def KadmonLandman1993.interpretationOf : Features.LicensingContext → AnyInterpretation

Determine the interpretation from the licensing context

Equations

• KadmonLandman1993.interpretationOf Features.LicensingContext.negation = KadmonLandman1993.AnyInterpretation.episodic
• KadmonLandman1993.interpretationOf Features.LicensingContext.nobody = KadmonLandman1993.AnyInterpretation.episodic
• KadmonLandman1993.interpretationOf Features.LicensingContext.withoutClause = KadmonLandman1993.AnyInterpretation.episodic
• KadmonLandman1993.interpretationOf Features.LicensingContext.few = KadmonLandman1993.AnyInterpretation.episodic
• KadmonLandman1993.interpretationOf Features.LicensingContext.atMost = KadmonLandman1993.AnyInterpretation.episodic
• KadmonLandman1993.interpretationOf Features.LicensingContext.conditionalAntecedent = KadmonLandman1993.AnyInterpretation.episodic
• KadmonLandman1993.interpretationOf Features.LicensingContext.beforeClause = KadmonLandman1993.AnyInterpretation.episodic
• KadmonLandman1993.interpretationOf Features.LicensingContext.onlyFocus = KadmonLandman1993.AnyInterpretation.episodic
• KadmonLandman1993.interpretationOf Features.LicensingContext.tooTo = KadmonLandman1993.AnyInterpretation.episodic
• KadmonLandman1993.interpretationOf Features.LicensingContext.comparativeNP = KadmonLandman1993.AnyInterpretation.episodic
• KadmonLandman1993.interpretationOf Features.LicensingContext.comparativeS = KadmonLandman1993.AnyInterpretation.episodic
• KadmonLandman1993.interpretationOf Features.LicensingContext.adversative = KadmonLandman1993.AnyInterpretation.episodic
• KadmonLandman1993.interpretationOf Features.LicensingContext.sinceTemporal = KadmonLandman1993.AnyInterpretation.episodic
• KadmonLandman1993.interpretationOf Features.LicensingContext.modalPossibility = KadmonLandman1993.AnyInterpretation.generic
• KadmonLandman1993.interpretationOf Features.LicensingContext.modalNecessity = KadmonLandman1993.AnyInterpretation.generic
• KadmonLandman1993.interpretationOf Features.LicensingContext.imperative = KadmonLandman1993.AnyInterpretation.generic
• KadmonLandman1993.interpretationOf Features.LicensingContext.generic = KadmonLandman1993.AnyInterpretation.generic
• KadmonLandman1993.interpretationOf Features.LicensingContext.freeRelative = KadmonLandman1993.AnyInterpretation.generic
• KadmonLandman1993.interpretationOf Features.LicensingContext.question = KadmonLandman1993.AnyInterpretation.episodic
• KadmonLandman1993.interpretationOf Features.LicensingContext.superlative = KadmonLandman1993.AnyInterpretation.episodic
• KadmonLandman1993.interpretationOf Features.LicensingContext.universalRestrictor = KadmonLandman1993.AnyInterpretation.episodic
• KadmonLandman1993.interpretationOf Features.LicensingContext.doubtVerb = KadmonLandman1993.AnyInterpretation.episodic
• KadmonLandman1993.interpretationOf Features.LicensingContext.denyVerb = KadmonLandman1993.AnyInterpretation.episodic

theorem KadmonLandman1993.fc_iff_generic (ctx : Features.LicensingContext) : interpretationOf ctx = AnyInterpretation.generic ↔ klExplanation ctx = Semantics.Polarity.Licensing.LicensingMechanism.byGenericIndefinite

K&L's prediction: FC any occurs exactly in generic-interpretation contexts, and these are the contexts explained by generic indefinite analysis (not by DE-based strengthening).

Domain Vagueness Distinguishes Generics from Universals (K&L §4.1.2)

K&L's formal distinction: every owl is domain precise (each context determines a unique set of owls to quantify over), while an owl in generic use is domain vague (the "normalcy" restriction is inherently underspecified). This explains why:

• every poodle gives live birth is false (one male counterexample suffices)
• a poodle gives live birth is true (male poodles are legitimate exceptions)

The vagueness is essential to exception tolerance: because the domain is never fully pinned down, apparent counterexamples can always be excluded as falling outside the quantification under some precisification.

inductive KadmonLandman1993.DomainPrecision : Type

Whether a quantifier is domain precise or domain vague. K&L: every and no are domain precise; generic NPs are domain vague; any is domain vague with additional dimensional universality.

• precise : DomainPrecision
• vague : DomainPrecision

@[implicit_reducible]

instance KadmonLandman1993.instDecidableEqDomainPrecision : DecidableEq DomainPrecision

Equations

• KadmonLandman1993.instDecidableEqDomainPrecision x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KadmonLandman1993.instReprDomainPrecision.repr : DomainPrecision → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KadmonLandman1993.instReprDomainPrecision : Repr DomainPrecision

Equations

• KadmonLandman1993.instReprDomainPrecision = { reprPrec := KadmonLandman1993.instReprDomainPrecision.repr }

structure KadmonLandman1993.AlmostDatum : Type

almost modifiability tracks domain precision or dimensional universality. K&L (§4.3): almost can modify NPs that are either domain precise (true universals like every) or dimensionally universal (any). Generic NPs (an owl) are domain vague without dimensional universality, so almost cannot modify them.

• np : String
• almostOK : Bool
• precision : DomainPrecision
• dimUniversal : Bool

def KadmonLandman1993.instDecidableEqAlmostDatum.decEq (x✝ x✝¹ : AlmostDatum) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance KadmonLandman1993.instDecidableEqAlmostDatum : DecidableEq AlmostDatum

Equations

• KadmonLandman1993.instDecidableEqAlmostDatum = KadmonLandman1993.instDecidableEqAlmostDatum.decEq

def KadmonLandman1993.instReprAlmostDatum.repr : AlmostDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KadmonLandman1993.instReprAlmostDatum : Repr AlmostDatum

Equations

• KadmonLandman1993.instReprAlmostDatum = { reprPrec := KadmonLandman1993.instReprAlmostDatum.repr }

def KadmonLandman1993.AlmostDatum.predicted (d : AlmostDatum) : Bool

almost is compatible iff the NP is domain precise or dimensionally universal. This is K&L's prediction, derived from the definitions.

Equations

• d.predicted = (d.precision == KadmonLandman1993.DomainPrecision.precise || d.dimUniversal)

def KadmonLandman1993.almost_every : AlmostDatum

Equations

• KadmonLandman1993.almost_every = { np := "every owl", almostOK := true, precision := KadmonLandman1993.DomainPrecision.precise, dimUniversal := false }

def KadmonLandman1993.almost_generic_a : AlmostDatum

Equations

• KadmonLandman1993.almost_generic_a = { np := "an owl", almostOK := false, precision := KadmonLandman1993.DomainPrecision.vague, dimUniversal := false }

def KadmonLandman1993.almost_any : AlmostDatum

Equations

• KadmonLandman1993.almost_any = { np := "any owl", almostOK := true, precision := KadmonLandman1993.DomainPrecision.vague, dimUniversal := true }

def KadmonLandman1993.almost_no : AlmostDatum

Equations

• KadmonLandman1993.almost_no = { np := "no owl", almostOK := true, precision := KadmonLandman1993.DomainPrecision.precise, dimUniversal := false }

def KadmonLandman1993.almost_some : AlmostDatum

Equations

• KadmonLandman1993.almost_some = { np := "some owl", almostOK := false, precision := KadmonLandman1993.DomainPrecision.vague, dimUniversal := false }

Verification: K&L's Core Examples

structure KadmonLandman1993.KLDatum : Type

An NPI licensing datum extended with K&L's explanation.

K&L's locality condition (D) requires distinguishing the local entailment signature (at the narrowest operator scoping over any) from the global signature (at the sentence level). For most examples these coincide; they diverge when any is embedded under multiple operators (e.g., any in the scope of every under negation).

• sentence : String

  The sentence

• grammatical : Bool

  Grammaticality judgment

• explanation : Semantics.Polarity.Licensing.LicensingMechanism

  K&L's licensing mechanism for the judgment

• localSig : Core.NaturalLogic.EntailmentSig

  The entailment signature at the LOCAL proposition (narrowest operator scoping over any). This is the signature that matters for strengthening under K&L's locality condition (D).

• globalSig : Core.NaturalLogic.EntailmentSig

  The entailment signature at the GLOBAL (sentence) level. Defaults to localSig when there is only one relevant operator.

• wideningDimension : String

  Notes on the widening dimension

@[implicit_reducible]

instance KadmonLandman1993.instReprKLDatum : Repr KLDatum

Equations

• KadmonLandman1993.instReprKLDatum = { reprPrec := KadmonLandman1993.instReprKLDatum.repr }

def KadmonLandman1993.instReprKLDatum.repr : KLDatum → ℕ → Std.Format

Equations

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

def KadmonLandman1993.ex1 : KLDatum

Equations

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

def KadmonLandman1993.ex2 : KLDatum

Equations

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

def KadmonLandman1993.ex10 : KLDatum

Equations

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

def KadmonLandman1993.ex27b : KLDatum

Equations

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

def KadmonLandman1993.ex55 : KLDatum

Equations

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

def KadmonLandman1993.ex56 : KLDatum

Equations

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

def KadmonLandman1993.ex72 : KLDatum

Equations

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

def KadmonLandman1993.ex73 : KLDatum

Equations

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

def KadmonLandman1993.ex82 : KLDatum

Equations

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

def KadmonLandman1993.ex143 : KLDatum

Equations

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

def KadmonLandman1993.allExamples : List KLDatum

The examples collectively verify K&L's predictions:

• Grammatical sentences with byStrengthening have DE local signatures
• Ungrammatical sentences have non-DE local signatures
• FC any examples have byGenericIndefinite explanation

Equations

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

Locality via Signature Composition

K&L's locality condition (D) states that strengthening must hold at the local proposition — the narrowest operator scoping over any.

In Icard's framework, the local signature is the composition of signatures along the path from any to the local operator. Example (56):

*It's not the case that [every boy has any potatoes]

Path from any to local operator every: every_scope = multiplicative (⊞) → UE → strengthening fails

Even though the global context (under negation) is DE, the local context (scope of every) is UE. This correctly predicts (56) is bad.

The Hidden Normalcy Parameter IS Domain Vagueness (K&L §4.1)

The traditional GEN operator (traditionalGEN in Generics.lean) is a universal quantifier over situations with a hidden normalcy predicate:

GEN_s [normal(s) ∧ restrictor(s)] [scope(s)]

K&L's insight (§4.1.1–§4.1.2) is that this normalcy predicate is inherently vague. There is no single correct way to fill in "normal" — different contexts suggest different completions, and speakers knowingly leave it underspecified.

A VagueRestriction captures this precisely:

• The precise part (v₀) contains normalcy properties everyone agrees on
• The precisifications (V) are the consistent ways to complete "normalcy"
• Each precisification determines a NormalcyPredicate

traditionalGEN under a fixed normalcy predicate is what you get when you pick one precisification. K&L's domain vagueness is the meta-level fact that this choice is never fully determined.

This explains why traditionalGEN is criticized for hiding all the work in the normalcy parameter (see docstring of Generics.lean): K&L's framework makes explicit that the parameter is inherently vague, not merely unknown.

def KadmonLandman1993.gen {D : Type u_1} (domain : List D) (normal restrictor scope : D → Bool) : Bool

The traditional GEN operator: ∀s. normal(s) ∧ restrictor(s) → scope(s).

This is the standard analysis of generic sentences (see Theories/Semantics/Lexical/Noun/Kind/Generics.lean), defined locally to avoid import chain issues. K&L's contribution is explaining WHY the normalcy parameter is context-dependent: it is inherently vague.

Equations

• KadmonLandman1993.gen domain normal restrictor scope = domain.all fun (d : D) => !(normal d && restrictor d) || scope d

theorem KadmonLandman1993.exception_tolerance_via_normalcy {D : Type u_1} (domain : List D) (restrictor scope n₁ n₂ : D → Bool) (s : D) (_hs : s ∈ domain) (_hNorm₁ : n₁ s = true) (_hRestr : restrictor s = true) (_hFails : scope s = false) (hNotNorm₂ : n₂ s = false) : (n₂ s && restrictor s) = false

Bridge: GEN under a fixed normalcy predicate is a single-precisification instance of K&L's vague generic.

K&L's analysis explains what the traditional GEN leaves implicit:

• When you evaluate GEN with a specific normal parameter, you are choosing one precisification of the vague restriction
• The "exception tolerance" of generics arises because different normalcy predicates (= different precisifications) yield different domains, and an entity that is a counterexample under one may be outside the domain under another (a "legitimate exception")

The theorem: if domain vagueness holds (some precisifications differ), then there exist two normalcy predicates under which GEN gives different truth values — the entity that causes failure under n₁ is excluded from the domain under n₂.

theorem KadmonLandman1993.domain_vagueness_explains_gen_exceptions {Property : Type u_1} {Entity : Type u_2} (X : Phenomena.Polarity.Studies.KadmonLandman1993.Apparatus.VagueRestriction Property) (apply : Property → Set Entity) (scope : Entity → Prop) (hVague : Phenomena.Polarity.Studies.KadmonLandman1993.Apparatus.isDomainVague X apply) (hSub : Phenomena.Polarity.Studies.KadmonLandman1993.Apparatus.genericSubTrue X apply scope) : ∃ v₁ ∈ X.precisifications, ∃ v₂ ∈ X.precisifications, Phenomena.Polarity.Studies.KadmonLandman1993.Apparatus.domainOf v₁ apply ≠ Phenomena.Polarity.Studies.KadmonLandman1993.Apparatus.domainOf v₂ apply ∧ Phenomena.Polarity.Studies.KadmonLandman1993.Apparatus.genericTrue X apply scope v₁

K&L's explanation for why generics tolerate exceptions.

Domain vagueness (multiple precisifications with different domains) maps directly to exception tolerance in the GEN operator: for any apparent counterexample, there exists a precisification of normalcy under which that counterexample is outside the domain.

"A poodle gives live birth": male poodles are counterexamples under the precisification where normalcy includes all poodles, but they are outside the domain under the precisification where normalcy is restricted to female poodles (the relevant class for reproduction).

The vague restriction framework explains what the traditional GEN operator merely stipulates: the normalcy parameter is not unknown but inherently underspecified, and this underspecification is an essential feature of generic meaning, not a bug.

Widening Interacts with Implicit Restrictions (K&L §3.5.3)

K&L's deepest formal argument concerns any in conditional antecedents. The standard DE analysis says conditional antecedents are DE, so strengthening holds. But K&L note that natural language conditionals are NOT classically DE — the inference from (140) to (141) is dubious:

• (140) If John subscribes to a newspaper, he gets well informed.
• (141) If John subscribes to a newspaper and he can't read, he gets well informed.

K&L's resolution (§3.5.2–§3.5.3): conditionals are DE on a constant implicit restriction. The implicit restriction R_A determines which "cases" are relevant. When the implicit restriction changes between premise and conclusion, the inference may fail. But the strengthening inferences required for licensing any always go through, because:

1. The narrow interpretation (before widening) has restriction R_narrow (e.g., "important newspapers that John can read")

2. Widening along the dimension "important vs. unimportant" does two things simultaneously:

   • Widens the CN denotation (adds unimportant newspapers)
   • Weakens the implicit restriction (R_wide cannot undo the widening by excluding the very entities widening brought in)

3. R_wide is never stronger than R_narrow: the restriction on the wide interpretation may be "somewhat weaker" but cannot exclude entities that R_narrow already included.

4. Therefore widening + restriction weakening = strengthening always holds: the wide interpretation (more entities in antecedent, weaker restriction) entails the narrow interpretation (fewer entities, stronger restriction).

K&L (p. 404): "Conditionals always satisfy strengthening, because of the relation between the restrictions of the wide and narrow interpretations."

This is formalized below as a theorem about vague restrictions: widening along a dimension weakens the restriction, and the widened conditional (with its weakened restriction) always entails the narrow conditional (with its original restriction).

def KadmonLandman1993.conditionalWithRestriction {Case : Type u_1} (restriction antecedent consequent : Case → Prop) : Prop

A conditional with an implicit restriction: "if A then C" is true iff in all relevant cases satisfying both the restriction and the antecedent, the consequent holds.

K&L (p. 400, eq. (147)): ∀c ↾ R_A(c). A(c) → C(c)

The restriction parameter is the implicit contextual restriction (Kratzer's modal base) that determines which cases count as "relevant."

Equations

• KadmonLandman1993.conditionalWithRestriction restriction antecedent consequent = ∀ (c : Case), restriction c → antecedent c → consequent c

theorem KadmonLandman1993.widening_satisfies_conditional_strengthening {Case : Type u_1} (R_narrow R_wide A_narrow A_wide consequent : Case → Prop) (hRestrWeaker : ∀ (c : Case), R_narrow c → R_wide c) (hAntWeaker : ∀ (c : Case), A_narrow c → A_wide c) (hWide : conditionalWithRestriction R_wide A_wide consequent) : conditionalWithRestriction R_narrow A_narrow consequent

K&L's core theorem (§3.5.3): Widening always satisfies strengthening in conditional antecedents.

If the wide restriction is weaker than the narrow restriction (it includes all cases the narrow restriction includes), then the wide conditional entails the narrow conditional.

K&L (p. 404): "The strengthening inference that has to hold for any to be licensed need not be an inference on a constant restriction. However, strengthening inferences do always go through, because of the relation between the restrictions of the wide and narrow interpretations. The two restrictions are always the same, except that the restriction of the premise may be somewhat weaker (but never stronger), than the restriction of the conclusion."

This is the deepest theorem of the paper: it explains why any is always licensed in conditional antecedents, without requiring classical DE of the whole conditional.

The key insight: widening CANNOT undo itself via the restriction. If widening adds unimportant newspapers to the CN denotation, the restriction cannot then exclude unimportant newspapers — that would defeat the purpose of widening. So the wide restriction is always at least as permissive as the narrow restriction.

theorem KadmonLandman1993.widening_weakens_restriction {Property : Type u_1} {Entity : Type u_2} (X : Phenomena.Polarity.Studies.KadmonLandman1993.Apparatus.VagueRestriction Property) (onDimension : Property → Prop) [DecidablePred onDimension] (apply : Property → Set Entity) : Phenomena.Polarity.Studies.KadmonLandman1993.Apparatus.domainOf X.precise apply ⊆ Phenomena.Polarity.Studies.KadmonLandman1993.Apparatus.domainOf (Phenomena.Polarity.Studies.KadmonLandman1993.Apparatus.widenAlong X onDimension).precise apply

Corollary: Widening along a dimension creates the required restriction-weakening.

When widening removes a property P from the CN restriction (adding both P-entities and ¬P-entities), the implicit restriction must also be weakened to accommodate both. This is because the restriction cannot re-exclude the entities that widening brought in — doing so would "undo the effect of widening" (K&L §3.5.3, p. 403).

K&L (p. 403): "We think it is natural to assume that this can never happen: the restriction cannot undo the effect of widening. Hence, the process of widening has the effect of minimally altering the restriction (if necessary), and in the case of our example, we get that the wide interpretation is as in (150)."

This formalizes the principle that the wide restriction is always at most as strong as the narrow restriction — never stronger.

theorem KadmonLandman1993.any_always_licensed_in_conditionals {Case : Type u_1} (R_narrow R_wide A_narrow A_wide consequent : Case → Prop) (hRestrWeaker : ∀ (c : Case), R_narrow c → R_wide c) (hAntWeaker : ∀ (c : Case), A_narrow c → A_wide c) : conditionalWithRestriction R_wide A_wide consequent → conditionalWithRestriction R_narrow A_narrow consequent

Main result: any is always licensed in conditional antecedents.

Combining widening_satisfies_conditional_strengthening with widening_weakens_restriction: widening the CN in a conditional antecedent simultaneously (1) widens the antecedent domain and (2) weakens the implicit restriction. Both of these go in the same direction — making the conditional more general. The wider conditional (with its weakened restriction) always entails the narrower conditional (with its original restriction).

This is K&L's explanation for why any is "always licensed in antecedents of conditionals" (§3.5.4, p. 404) — not because conditionals are simply DE, but because widening and restriction- weakening conspire to guarantee strengthening.