Kadmon & Landman 1993: Any

Formalizes [KL93]'s unified analysis of any: any CN is the indefinite a CN plus widening of the CN denotation along a contextual dimension, licensed only if widening creates a stronger statement (strengthening), checked at the local proposition (locality); free-choice any is the same item with a generic interpretation. Strengthening subsumes [Lad79]'s DE condition — widening an existential strengthens exactly when the context is DE — but K&L stress it is necessary, not sufficient: each and comparative more often than are DE yet resist any because widening must also make pragmatic sense (their §3.2).

Main declarations

• Strengthening: the licensing condition — widening D to D' in context C creates a stronger statement;
• de_satisfies_strengthening: antitone (DE) contexts satisfy strengthening;
• GuaranteesStrengthening, klExplanation: per-context classification, projected from Semantics.Polarity.Licensing.contextProperties;
• ladusaw_de_is_kl_strengthening: Ladusaw-DE contexts are strengthening contexts;
• sorry_licenses_any, glad_does_not_license: the adversative asymmetry (Strawson-DE vs UE, K&L §3.3);
• widening_satisfies_conditional_strengthening: widening plus restriction-weakening guarantees strengthening in conditional antecedents (K&L §3.5.3);
• VagueRestriction, widenAlong, dimensionallyUniversal: the domain-vagueness apparatus behind FC any and the almost test (K&L §4);
• domain_vague_allows_exceptions: exception tolerance of generics from domain vagueness;
• VagueRestriction.toSpecSpace: the finite-case bridge to [Fin75]'s supervaluation — K&L's exception-tolerance zone is Fine's borderline zone.

The strengthening condition

K&L's component (C): any is licensed only if widening creates a stronger statement. For a context C and domains D ⊆ D', the wide interpretation must entail the narrow: C (∃x∈D', Px) ⊆ C (∃x∈D, Px). This holds exactly when C is antitone, which is why DE contexts license — and why widening in UE contexts, where it weakens, leaves any unlicensed.

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

K&L's strengthening condition: widening the domain D to D' in context C creates a stronger statement — the wide interpretation entails the narrow one.

Equations

• KadmonLandman1993.Strengthening C D D' P = (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 : Antitone C) (D D' : Set Entity) (P : Entity → Set World) (hD : D ⊆ D') : Strengthening C D D' P

In a DE (antitone) context, strengthening is automatic. K&L note that for many examples this makes the same predictions as [Lad79], while explaining why DE contexts license: widening must strengthen, and DE reverses entailment.

theorem KadmonLandman1993.ue_widening_weakens {World : Type u_1} {Entity : Type u_2} {C : Exhaustification.FreeChoice.Ctx World} (hUE : Monotone C) (D D' : Set Entity) (P : Entity → Set World) (hD : D ⊆ D') : C (Exhaustification.FreeChoice.existsInDomain D P) ⊆ C (Exhaustification.FreeChoice.existsInDomain D' P)

In a UE (monotone) context, widening weakens — the opposite of strengthening. This is K&L's explanation for why any is out in plain positive contexts.

Licensing contexts and entailment signatures

Each context's entailment signature and licensing mechanism are projected from the canonical Semantics.Polarity.Licensing.contextProperties table, so this file's classification cannot drift from the substrate's.

@[reducible, inline]

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

A licensing context's entailment signature in [Ica12]'s lattice — the Strawson-operative row, matching K&L's own convention of checking the DE pattern modulo factive presuppositions.

Equations

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

@[reducible, inline]

abbrev KadmonLandman1993.GuaranteesStrengthening (c : Features.LicensingContext) : Prop

A context guarantees K&L strengthening iff its entailment signature is on the DE side. Contexts with .mono or higher signatures are licensed by other routes: K&L defer questions to [KL90] and never discuss superlatives — the Strawson-DE route for the latter is later literature ([vF99a]).

Equations

• KadmonLandman1993.GuaranteesStrengthening c = ((KadmonLandman1993.contextEntailmentSig c).toDEStrength.isSome = true)

@[reducible, inline]

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

A licensing context's K&L mechanism, projected from contextProperties: why the context licenses, not merely that it does.

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

Drift sentry: every context classified byStrengthening has a DE entailment signature.

Compatibility with Ladusaw 1979

K&L's classification refines [Lad79]'s: every Ladusaw-DE context is a strengthening context, but K&L additionally explain adversative predicates (DE on a constant perspective) and conditionals with implicit restrictions.

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 ∨ klExplanation ctx = Semantics.Polarity.Licensing.LicensingMechanism.byStrawsonDE

Ladusaw-DE contexts are K&L strengthening contexts — or, where the DE status is itself only Strawson (superlatives, per the later [vF99a]), the Strawson refinement of strengthening. Ladusaw describes where NPIs occur; K&L and the Strawson tradition explain why.

Adversative predicates: sorry vs glad

K&L §3.3: sorry that A entails want ¬A, and wanting a set empty entails wanting all its subsets empty, so for sorry the wide interpretation entails the narrow — strengthening holds. Glad that A entails want A, and wanting a set inhabited does not entail wanting each subset inhabited, so strengthening fails. K&L summarize: adversative predicates are DE on a constant perspective (and so guarantee strengthening), while predicates like glad are not DE. The constant "perspective" is the bestOf parameter; the factive presupposition means the DE pattern is Strawson, not classical.

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

Sorry licenses NPIs: it is Strawson-DE — DE with the perspective (bestOf) held constant. Imported from StrawsonEntailment.sorryFull_isStrawsonDE; consumed by VonFintel1999's cross-framework bridge.

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

Sorry is not classically DE: the doxastic factivity presupposition blocks it. K&L adopt Ladusaw's convention that the DE pattern need only hold of the sentence minus its factive presupposition.

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

Glad does not freely license NPIs: it is UE, so widening weakens. K&L: wanting a set to have members does not entail wanting each particular subset to have members.

structure KadmonLandman1993.SettleForLessDatum : Type

A settle-for-less datum (K&L §3.3.2): any under glad is licensed only on the interpretation where the speaker's preferred "narrow wish" cannot be satisfied and they settle for the wide one. With the real wish identified with the narrow wish, being glad of the wide statement entails that one would be glad of the narrow one — K&L's (101) entails (102) — so strengthening is satisfied.

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

def KadmonLandman1993.settleGladTickets : SettleForLessDatum

K&L (76B).

Equations

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

def KadmonLandman1993.settleGladAnybody : SettleForLessDatum

K&L (88). The widening runs from phonologists to linguists, so the narrow wish (a phonologist likes me) is the preferred, real wish.

Equations

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

def KadmonLandman1993.sureNoSettle : SettleForLessDatum

K&L (95): sure allows no settle-for-less interpretation — their (96)–(98) lack the characteristic negative implication — so any under sure is never rescued.

Equations

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

Conditional antecedents

K&L §3.5 treat conditionals and adversatives as one pattern — DE with a parameter held constant (the implicit restriction, resp. the perspective); in mathlib terms, Antitone (f param) for fixed param. Under the restrictor analysis of conditionals (cf. [Kra86]), the antecedent of conditional necessity is classically DE once the modal base is fixed, so widening the antecedent domain strengthens the conditional.

theorem KadmonLandman1993.conditional_satisfies_strengthening {W : Type u_1} (domain : W → Set W) (β : Set W) : Entailment.IsDownwardEntailing fun (α : Set W) => Entailment.condNecessity domain α β

Conditional antecedents satisfy strengthening: conditional necessity is DE in its antecedent with the modal base held constant. K&L (143): "If John subscribes to any newspaper, he gets well informed" — widening newspaper to include unimportant newspapers strengthens the conditional.

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

A conditional with an implicit restriction (K&L's (147)): true iff every relevant case satisfying the restriction and the antecedent satisfies the consequent.

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

Widening always satisfies strengthening in conditional antecedents (K&L §3.5.3). Natural-language conditionals are not classically DE — their (140) does not entail (141) — because the implicit restriction can shift. But the restriction cannot undo the effect of widening, so the wide restriction is never stronger than the narrow one, and then the wide conditional entails the narrow one. K&L: strengthening inferences "do always go through, because of the relation between the restrictions of the premise and of the conclusion. The two restrictions are always the same, except that the restriction of the premise may be somewhat weaker (but never stronger), as dictated by the widening."

Negated because-clauses: metalinguistic licensing

K&L §3.4, contra [Lin87a]: not because [S_] is not DE (because [S_] is not UE, so negating it yields no DE context), while not because of [NP_] is DE and licenses any freely — their (122)/(123) need no negative implication. In because [S_], any is licensed only metalinguistically: the negation denies because's factive presupposition, and any strengthens that denial. Merely implying the denial is not enough — the rhetorical conditional (132) can imply it but lacks the metalinguistic denial, and any is out. This is the paper's only genuinely non-DE licensing mechanism.

structure KadmonLandman1993.BecauseClauseDatum : Type

A because-clause licensing datum. The prediction checked below is grammatical = npComplement || metalinguisticDenial; both fields are annotations transcribed from K&L's §3.4 discussion, so the #guard is a consistency check on the transcription, not a derived prediction.

• sentence : String
• grammatical : Bool
• npComplement : Bool

  because of [NP_] (DE under negation, licenses freely) vs because [S_]

• metalinguisticDenial : Bool

  Whether the metalinguistic presupposition-denial reading is available. Mere implication of the denial does not suffice (K&L on (132)).

• notes : String

def KadmonLandman1993.becauseEx105 : BecauseClauseDatum

K&L (105).

Equations

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

def KadmonLandman1993.becauseEx106 : BecauseClauseDatum

K&L (106), from [Lin87a]; marked #.

Equations

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

def KadmonLandman1993.becauseEx109 : BecauseClauseDatum

K&L (109): the any-bearing sentence of their own constructed Sir Winfred passage; marked #. The surrounding text cancels the negative implication, and any is bad.

Equations

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

def KadmonLandman1993.becauseEx122 : BecauseClauseDatum

K&L (122).

Equations

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

def KadmonLandman1993.becauseEx123 : BecauseClauseDatum

K&L (123): the felicitous Sir Winfred variant — the minimal pair with (109), substituting because of + NP.

Equations

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

def KadmonLandman1993.becauseEx125 : BecauseClauseDatum

K&L (125).

Equations

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

def KadmonLandman1993.becauseEx132 : BecauseClauseDatum

K&L (132): the rhetorical conditional; marked *. It can imply the denial of the presupposition, but cannot metalinguistically deny it.

Equations

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

FC any as generic indefinite

K&L's component (FC): PS any is a regular indefinite, FC any a generic indefinite; the apparent universal force of FC any emerges from genericity plus widening (§4.3). The episodic/generic split below is projected from the substrate's mechanism classification. K&L themselves analyze only plain generics like their (10) and tentatively extend to modals; routing imperatives and free relatives through the generic mechanism follows the substrate, not K&L's text (they explicitly defer directives to later work and never discuss free relatives).

inductive KadmonLandman1993.AnyInterpretation : Type

Interpretation of the indefinite containing any: episodic (PS any) or generic (FC 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 (c : Features.LicensingContext) : AnyInterpretation

The interpretation of any in a licensing context, projected from the licensing mechanism: generic exactly when the substrate classifies the context as licensed by the generic indefinite.

Equations

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

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

Vague restrictions and precisifications

K&L §4.1: every owl is domain precise — context determines a unique domain — while generic an owl is domain vague: the normalcy restriction is inherently underspecified, and different precisifications yield different domains. This is what lets generics tolerate exceptions ("a poodle gives live birth" survives male poodles). The Set-based notions are stated locally because the supervaluation substrate (Semantics/Supervaluation, [Fin75]) is Finset-based for computability; the finite-case bridge is VagueRestriction.toSpecSpace below.

structure KadmonLandman1993.VagueRestriction (Property : Type u_1) : Type u_1

A vague restriction ⟨v₀, V⟩ (K&L §4.1): a precise part (properties known to hold) together with its consistent completions, each extending the precise part, which is itself a minimal precisification.

• precise : Set Property

  The precise part: properties definitely in the restriction.

• precisifications : Set (Set Property)

  The consistent ways to complete the restriction.

• extends_precise (v : Set Property) : v ∈ self.precisifications → self.precise ⊆ v

  Every precisification extends the precise part.

• precise_mem : self.precise ∈ self.precisifications

  The precise part is itself a (minimal) precisification.

def KadmonLandman1993.domainOf {Property : Type u_1} {Entity : Type u_2} (props : Set Property) (apply : Property → Set Entity) : Set Entity

The domain induced by a property set: the entities satisfying every property.

Equations

• KadmonLandman1993.domainOf props apply = {e : Entity | ∀ P ∈ props, e ∈ apply P}

def KadmonLandman1993.isDomainPrecise {Property : Type u_1} {Entity : Type u_2} (X : VagueRestriction Property) (apply : Property → Set Entity) : Prop

Domain precise (K&L (164)): every precisification determines the same domain as the precise part.

Equations

• KadmonLandman1993.isDomainPrecise X apply = ∀ v ∈ X.precisifications, KadmonLandman1993.domainOf v apply = KadmonLandman1993.domainOf X.precise apply

def KadmonLandman1993.isDomainVague {Property : Type u_1} {Entity : Type u_2} (X : VagueRestriction Property) (apply : Property → Set Entity) : Prop

Domain vague: not domain precise — some precisifications yield different domains.

Equations

• KadmonLandman1993.isDomainVague X apply = ¬KadmonLandman1993.isDomainPrecise X apply

theorem KadmonLandman1993.isDomainPrecise_of_forall_eq {Property : Type u_1} {Entity : Type u_2} (X : VagueRestriction Property) (apply : Property → Set Entity) (h : ∀ v ∈ X.precisifications, v = X.precise) : isDomainPrecise X apply

If every precisification equals the precise part, the restriction is domain precise — the case of every and no.

def KadmonLandman1993.widenAlong {Property : Type u_1} (X : VagueRestriction Property) (onDimension : Property → Prop) : VagueRestriction Property

Widening along a dimension (K&L (174)): remove the properties on the dimension from the precise part and from every precisification.

Equations

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

theorem KadmonLandman1993.widenAlong_weakens_precise {Property : Type u_1} (X : VagueRestriction Property) (onDimension : Property → Prop) : (widenAlong X onDimension).precise ⊆ X.precise

Widening weakens the restriction: the widened precise part is a subset of the original.

theorem KadmonLandman1993.widenAlong_expands_domain {Property : Type u_1} {Entity : Type u_2} (X : VagueRestriction Property) (onDimension : Property → Prop) (apply : Property → Set Entity) : domainOf X.precise apply ⊆ domainOf (widenAlong X onDimension).precise apply

Widening expands the domain: fewer constraints, more entities qualify. This is the restriction-weakening half of K&L §3.5.3: the restriction cannot undo the effect of widening.

Dimensional universality

K&L (175)–(177): after widening along a dimension {P, ¬P}, no entity is excluded on the basis of that dimension, so the quantifier is universal with respect to it. Any CN is dimensionally universal; generic a CN is not. Since almost requires a domain-precise universal or a dimensionally universal NP, this derives almost any owl vs ungrammatical almost an owl (§4.3).

def KadmonLandman1993.universalWrtDimension {Property : Type u_1} {Entity : Type u_2} (X : VagueRestriction Property) (onDimension : Property → Prop) (apply : Property → Set Entity) (baseDenotation : Set Entity) : Prop

Universality with respect to a dimension (K&L (175)): after widening along the dimension, every entity in the base denotation is in the domain.

Equations

• KadmonLandman1993.universalWrtDimension X onDimension apply baseDenotation = (baseDenotation ⊆ KadmonLandman1993.domainOf (KadmonLandman1993.widenAlong X onDimension).precise apply)

def KadmonLandman1993.nonTrivialDimension {Property : Type u_1} {Entity : Type u_2} (onDimension : Property → Prop) (apply : Property → Set Entity) (baseDenotation : Set Entity) : Prop

A dimension is non-trivial on a base set (K&L (176)): some entity satisfies a property on the dimension and some entity fails one.

Equations

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

def KadmonLandman1993.dimensionallyUniversal {Property : Type u_1} {Entity : Type u_2} (X : VagueRestriction Property) (apply : Property → Set Entity) (baseDenotation : Set Entity) : Prop

Dimensionally universal (K&L (177)): universal with respect to some non-trivial dimension.

Equations

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

theorem KadmonLandman1993.any_cn_dimensionally_universal {Property : Type u_1} {Entity : Type u_2} (X : VagueRestriction Property) (onDimension : Property → Prop) (apply : Property → Set Entity) (baseDenotation : Set Entity) (hNT : nonTrivialDimension onDimension apply baseDenotation) (hBase : baseDenotation ⊆ domainOf {P : Property | P ∈ X.precise ∧ ¬onDimension P} apply) : dimensionallyUniversal (widenAlong X onDimension) apply baseDenotation

Any CN is dimensionally universal (K&L §4.3): widening along a non-trivial dimension yields universality with respect to that dimension.

theorem KadmonLandman1993.widenAlong_precise_eq_empty {Property : Type u_1} (X : VagueRestriction Property) (onDimension : Property → Prop) (hAllOnDim : ∀ P ∈ X.precise, onDimension P) : (widenAlong X onDimension).precise = ∅

Total widening: if every precise property is on the dimension, widening empties the precise part — K&L's case where any CN becomes not only universal with respect to the dimension but truly universal.

Generic quantification as vague universality

K&L §4.1.1: a generic is a universal restricted by a vague property set — "An owl hunts mice" is ∀ ↾ X_owl(Owl)(Hunts mice), their (159). The traditional GEN operator's hidden normalcy parameter (Semantics/Genericity/Generics.lean) is, on this view, a choice of precisification; exception tolerance is the freedom to choose another.

def KadmonLandman1993.genericTrue {Property : Type u_1} {Entity : Type u_2} (apply : Property → Set Entity) (scope : Entity → Prop) (v : Set Property) : Prop

Truth under one precisification: every entity in the induced domain satisfies the scope.

Equations

• KadmonLandman1993.genericTrue apply scope v = ∀ e ∈ KadmonLandman1993.domainOf v apply, scope e

def KadmonLandman1993.genericSuperTrue {Property : Type u_1} {Entity : Type u_2} (X : VagueRestriction Property) (apply : Property → Set Entity) (scope : Entity → Prop) : Prop

Supervaluationist truth: true under every precisification.

Equations

• KadmonLandman1993.genericSuperTrue X apply scope = ∀ v ∈ X.precisifications, KadmonLandman1993.genericTrue apply scope v

def KadmonLandman1993.genericSubTrue {Property : Type u_1} {Entity : Type u_2} (X : VagueRestriction Property) (apply : Property → Set Entity) (scope : Entity → Prop) : Prop

Subvaluationist truth: true under some precisification — the exception-tolerant reading.

Equations

• KadmonLandman1993.genericSubTrue X apply scope = ∃ v ∈ X.precisifications, KadmonLandman1993.genericTrue apply scope v

theorem KadmonLandman1993.domain_vague_allows_exceptions {Property : Type u_1} {Entity : Type u_2} (X : VagueRestriction Property) (apply : Property → Set Entity) (hVague : isDomainVague X apply) : ∃ v₁ ∈ X.precisifications, ∃ v₂ ∈ X.precisifications, domainOf v₁ apply ≠ domainOf v₂ apply

Domain vagueness yields two precisifications with different domains — the room generics need for legitimate exceptions.

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

K&L's explanation of exception tolerance: if the restriction is domain vague and the generic is subvaluationistically true, then there are precisifications with different domains and the generic holds under one of them — an apparent counterexample may fall outside the domain under the operative precisification.

Grounding in Fine 1975 supervaluation

When the precisification set is finite, K&L's truth notions are [Fin75]'s: genericSuperTrue is super-truth on the induced specification space, and the exception-tolerance zone — sub-true but not super-true — is exactly Fine's borderline (indet) status. "A poodle gives live birth" is Fine-indefinite and K&L-assertable.

def KadmonLandman1993.VagueRestriction.toSpecSpace {Property : Type u_1} (X : VagueRestriction Property) (V : Finset (Set Property)) (hV : ↑V = X.precisifications) : Semantics.Supervaluation.SpecSpace (Set Property)

The specification space induced by a vague restriction whose precisifications are enumerated by a finset. Nonemptiness is K&L's axiom that the precise part is itself a precisification.

Equations

• X.toSpecSpace V hV = { admissible := V, nonempty := ⋯ }

theorem KadmonLandman1993.VagueRestriction.mem_toSpecSpace {Property : Type u_1} {X : VagueRestriction Property} {V : Finset (Set Property)} {hV : ↑V = X.precisifications} {v : Set Property} : v ∈ (X.toSpecSpace V hV).admissible ↔ v ∈ X.precisifications

theorem KadmonLandman1993.genericSuperTrue_iff_superTrue {Property : Type u_1} {Entity : Type u_2} (X : VagueRestriction Property) (apply : Property → Set Entity) (scope : Entity → Prop) [DecidablePred (genericTrue apply scope)] (V : Finset (Set Property)) (hV : ↑V = X.precisifications) : genericSuperTrue X apply scope ↔ Semantics.Supervaluation.superTrue (genericTrue apply scope) (X.toSpecSpace V hV) = Core.Duality.Truth3.true

On a finite precisification space, K&L's supervaluationist truth is [Fin75]'s super-truth.

theorem KadmonLandman1993.genericSubTrue_not_superTrue_iff_indet {Property : Type u_1} {Entity : Type u_2} (X : VagueRestriction Property) (apply : Property → Set Entity) (scope : Entity → Prop) [DecidablePred (genericTrue apply scope)] (V : Finset (Set Property)) (hV : ↑V = X.precisifications) : genericSubTrue X apply scope ∧ ¬genericSuperTrue X apply scope ↔ Semantics.Supervaluation.superTrue (genericTrue apply scope) (X.toSpecSpace V hV) = Core.Duality.Truth3.indet

K&L's exception-tolerance zone is Fine's borderline zone. A generic that is subvaluationistically but not supervaluationistically true is exactly one whose supervaluation status is indefinite: assertable for K&L, borderline for [Fin75].

The almost test

K&L: almost modifies domain-precise true universal quantifiers (∀ or ¬∃) and, after §4.3, dimensionally universal NPs. Some owl is domain precise (K&L p. 412 group it with every owl and no owl) but not universal, so almost some owl is out; generic an owl has universal force but a vague domain; any owl is rescued by dimensional universality.

inductive KadmonLandman1993.DomainPrecision : Type

Domain precision of an NP's restriction (K&L §4.1.2).

• 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

An almost-modification datum.

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

  Whether the NP is a true universal (∀ or ¬∃).

• dimUniversal : Bool

@[implicit_reducible]

instance KadmonLandman1993.instDecidableEqAlmostDatum : DecidableEq AlmostDatum

Equations

• KadmonLandman1993.instDecidableEqAlmostDatum = KadmonLandman1993.instDecidableEqAlmostDatum.decEq

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

Equations

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

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

K&L's condition: a domain-precise universal, or a dimensionally universal NP.

Equations

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

def KadmonLandman1993.almostEvery : AlmostDatum

Equations

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

def KadmonLandman1993.almostNo : AlmostDatum

Equations

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

def KadmonLandman1993.almostSome : AlmostDatum

Equations

• KadmonLandman1993.almostSome = { np := "some owl", almostOK := false, precision := KadmonLandman1993.DomainPrecision.precise, universalForce := false, dimUniversal := false }

def KadmonLandman1993.almostGenericA : AlmostDatum

Equations

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

def KadmonLandman1993.almostAny : AlmostDatum

Equations

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

Key examples

localSig is the entailment signature at the narrowest operator scoping over any — the one K&L's locality condition (D) checks; globalSig the sentence-level signature. For adversatives the signature idealizes the factive presupposition away, per K&L's adoption of Ladusaw's convention (sorry_not_classically_de shows classical DE fails).

structure KadmonLandman1993.KLDatum : Type

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

• sentence : String
• grammatical : Bool
• explanation : Semantics.Polarity.Licensing.LicensingMechanism

  K&L's licensing mechanism for the judgment.

• localSig : NaturalLogic.EntailmentSig

  Signature at the narrowest operator scoping over any.

• globalSig : NaturalLogic.EntailmentSig

  Sentence-level signature; defaults to localSig.

• wideningDimension : Option String

@[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

K&L (1): PS any under negation.

Equations

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

def KadmonLandman1993.ex2 : KLDatum

K&L (2): positive context — widening weakens, so strengthening fails.

Equations

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

def KadmonLandman1993.ex10 : KLDatum

K&L (10): FC any in a generic context.

Equations

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

def KadmonLandman1993.ex27b : KLDatum

K&L (27b): restrictor of a universal is anti-additive.

Equations

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

def KadmonLandman1993.ex55 : KLDatum

K&L (55): scope of a universal is UE.

Equations

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

def KadmonLandman1993.ex56 : KLDatum

K&L (56): locality. The global signature (under negation) composes to DE, but the local context (scope of every) is UE, so any is out despite the DE global context.

Equations

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

def KadmonLandman1993.ex72 : KLDatum

K&L (72): adversatives license (DE on a constant perspective).

Equations

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

def KadmonLandman1993.ex73 : KLDatum

K&L (73): non-adversatives do not license.

Equations

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

def KadmonLandman1993.ex82 : KLDatum

K&L (82).

Equations

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

def KadmonLandman1993.ex143 : KLDatum

K&L (143): conditional antecedent.

Equations

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

def KadmonLandman1993.allExamples : List KLDatum

Equations

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