Kadmon and Landman (1993): Any

Kadmon and Landman analyze any CN as the indefinite a CN with its domain widened along a contextual dimension, licensed only when the widening makes the statement stronger, a condition checked at the narrowest operator over the indefinite; free-choice any is the same item under a generic interpretation. Widening weakens an existential, so strengthening holds exactly under an antitone context, which is why Ladusaw's downward-entailing contexts license. Adversatives are downward entailing on a constant perspective, a negated because-clause licenses only by metalinguistic denial, and conditional antecedents strengthen once the implicit restriction is fixed. The generic restriction is a vague property set whose precisifications give the normality of GEN.

Main results

• de_satisfies_strengthening, ue_widening_weakens, ladusaw_de_is_kl_strengthening: widening strengthens under an antitone context and weakens under a monotone one, so Ladusaw's contexts are strengthening contexts.
• strengthening_sorryThat, not_strengthening_wants: sorry licenses any and glad does not.
• widening_satisfies_conditional_strengthening: conditional antecedents strengthen.
• rows_agree: the paper's judgments follow its classification.
• any_cn_dimensionally_universal, domain_vague_allows_exceptions: widening makes any CN universal along its dimension, and domain vagueness lets a generic tolerate exceptions.
• almost_rows: almost modifies domain-precise and dimensionally universal noun phrases.
• genericSubTrue_not_superTrue_iff_indet: on a finite precisification space, exception tolerance is Fine's borderline status.

Implementation notes

• The rows record, at the narrowest operator over any, a substrate LicensingContext where one exists and otherwise the local entailment signature; the settle-for-less and metalinguistic readings are the paper's own annotations, so rows_agree checks the paper's classification against its judgments rather than deriving those two readings.
• The vague-restriction apparatus is Set-based; on a finite enumeration of the precisifications, supervaluation is SignType.supervaluation over it.

References

• [KL93]
• [Lad79]
• [Lin87a]
• [Fin75]

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.existsInDomain {World : Type u_1} {Entity : Type u_2} (D : Set Entity) (P : Entity → Set World) : Set World

The existential over a domain D is ∃ x ∈ D, P x.

Equations

• KadmonLandman1993.existsInDomain D P w = ∃ x ∈ D, P x w

theorem KadmonLandman1993.existsInDomain_mono {World : Type u_1} {Entity : Type u_2} {D D' : Set Entity} (P : Entity → Set World) (h : D ⊆ D') : existsInDomain D P ⊆ existsInDomain D' P

Widening the domain weakens the existential.

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

K&L's strengthening condition holds when widening the domain D to D' in context C creates a stronger statement, the wide interpretation entailing the narrow one.

Equations

• KadmonLandman1993.Strengthening C D D' P = (C (KadmonLandman1993.existsInDomain D' P) ⊆ C (KadmonLandman1993.existsInDomain D P))

theorem KadmonLandman1993.de_satisfies_strengthening {World : Type u_1} {Entity : Type u_2} {C : Set World → Set 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, since widening must strengthen and DE reverses entailment.

theorem KadmonLandman1993.ue_widening_weakens {World : Type u_1} {Entity : Type u_2} {C : Set World → Set World} (hUE : Monotone C) (D D' : Set Entity) (P : Entity → Set World) (hD : D ⊆ D') : C (existsInDomain D P) ⊆ C (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.

Compatibility with Ladusaw 1979

Each context's licensing mechanism is read off its licenser (PolarityItem.Licenser.mechanism), so this file's classification cannot drift from the semantics. 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 (L : PolarityItem.Licenser) (hDE : Ladusaw1979.IsDownwardEntailing L) : L.mechanism = PolarityItem.LicensingMechanism.strengthening

Ladusaw-DE contexts are K&L strengthening contexts; Ladusaw describes where NPIs occur, and K&L explain why.

Adversative predicates: sorry vs glad

K&L §3.3 reduce the adversatives to want on a constant perspective: being sorry that A is wanting A false, and being glad that A is wanting A. Wanting a set empty entails wanting each of its subsets empty, so sorry satisfies the strengthening condition; wanting a set inhabited does not entail wanting each subset inhabited, so glad does not.

def KadmonLandman1993.wants {World : Type u_1} (best : World → Set World) (A : Set World) : Set World

On a perspective whose best worlds at w are best w, one wants A at w when those best worlds are A-worlds. Being glad that A is wanting A.

Equations

• KadmonLandman1993.wants best A = {w : World | best w ⊆ A}

def KadmonLandman1993.sorryThat {World : Type u_1} (best : World → Set World) (A : Set World) : Set World

Being sorry that A is wanting A false on the same perspective.

Equations

• KadmonLandman1993.sorryThat best A = KadmonLandman1993.wants best Aᶜ

theorem KadmonLandman1993.strengthening_sorryThat {World : Type u_1} (best : World → Set World) {Entity : Type u_2} {D D' : Set Entity} (P : Entity → Set World) (hD : D ⊆ D') : Strengthening (sorryThat best) D D' P

Sorry satisfies the strengthening condition, so it licenses any.

theorem KadmonLandman1993.not_strengthening_wants : ¬Strengthening (wants fun (x : Bool) => {false}) {true} Set.univ fun (x : Bool) => {x}

Glad fails the strengthening condition, so it does not license any. The best world bought the false car, so one is glad that some car was bought but not that the true car was.

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) : Antitone fun (x : Set W) => Conditional.strictImp domain x β

Conditional antecedents satisfy strengthening, since conditional necessity is DE in its antecedent with the modal base held constant. In K&L's (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)) is true when 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. 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", in K&L's words.

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 — (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.

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 (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

The indefinite containing any is interpreted episodically (PS any) or generically (FC any).

• episodic : AnyInterpretation
• generic : AnyInterpretation

@[instance_reducible]

instance KadmonLandman1993.instDecidableEqAnyInterpretation : DecidableEq AnyInterpretation

Equations

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

@[instance_reducible]

instance KadmonLandman1993.instReprAnyInterpretation : Repr AnyInterpretation

Equations

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

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

Equations

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

noncomputable def KadmonLandman1993.interpretationOf (c : PolarityItem.LicensingContext) : AnyInterpretation

The interpretation of any in a licensing context is projected from the licensing mechanism, and is 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 : PolarityItem.LicensingContext) : interpretationOf c = AnyInterpretation.generic ↔ c.licenser.mechanism = PolarityItem.LicensingMechanism.genericIndefinite

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 (SignType.supervaluation) is Finset-based for computability; the finite case is below.

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

A vague restriction ⟨v₀, V⟩ (K&L §4.1) is a precise part, the 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 holds the 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 is the set of 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

A restriction is domain precise (K&L (164)) when 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

A restriction is domain vague when it is not domain precise, so that 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)) removes 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 being 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, since with fewer constraints more entities qualify. This is the restriction-weakening half of K&L §3.5.3, that 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

A restriction is universal with respect to a dimension (K&L (175)) when, 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)) when 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

A restriction is dimensionally universal (K&L (177)) when it is 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), since 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 = ∅

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 set of properties, "An owl hunts mice" being ∀ ↾ X_owl(Owl)(Hunts mice), (158) and (159), which (161) glosses as all normal owls hunt mice, with what counts as normal inherently vague. The vague set plays the part of GEN's normality: a precisification induces a Genericity.Normality, whose normal owls are the owls with its properties, and the generic under a precisification is GEN under that normality. Exception tolerance is the freedom to choose another precisification.

def KadmonLandman1993.precisificationNormality {Property : Type u_1} {Entity : Type u_2} (apply : Property → Set Entity) : Genericity.Normality (Set Property) Entity

Under the normality a precisification induces (161), the normal instances of a restrictor are those with every property of the precisification.

Equations

• KadmonLandman1993.precisificationNormality apply = Genericity.Normality.ofAccess fun (x : Set Property) => KadmonLandman1993.domainOf x apply

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

Under one precisification, the generic (159) holds when every instance of the restrictor with the precisified properties satisfies the scope, GEN under the normality the precisification induces.

Equations

• KadmonLandman1993.genericTrue apply R scope v = (v ∈ (KadmonLandman1993.precisificationNormality apply).gen R {e : Entity | scope e})

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

A generic is supervaluationistically true when it is true under every precisification.

Equations

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

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

A generic is subvaluationistically true when it is true under some precisification, the exception-tolerant reading.

Equations

• KadmonLandman1993.genericSubTrue X apply R scope = ∃ v ∈ X.precisifications, KadmonLandman1993.genericTrue apply R 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) (R : Set Entity) (scope : Entity → Prop) (hVague : isDomainVague X apply) (hSub : genericSubTrue X apply R scope) : ∃ v₁ ∈ X.precisifications, ∃ v₂ ∈ X.precisifications, domainOf v₁ apply ≠ domainOf v₂ apply ∧ genericTrue apply R scope v₁

K&L explain 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, so 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 status, supervaluation value 0. "A poodle gives live birth" is Fine-indefinite and K&L-assertable.

theorem KadmonLandman1993.genericSuperTrue_iff_superTrue {Property : Type u_1} {Entity : Type u_2} (X : VagueRestriction Property) (apply : Property → Set Entity) (R : Set Entity) (scope : Entity → Prop) [DecidablePred (genericTrue apply R scope)] (V : Finset (Set Property)) (hV : ↑V = X.precisifications) : genericSuperTrue X apply R scope ↔ SignType.supervaluation V (genericTrue apply R scope) = 1

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) (R : Set Entity) (scope : Entity → Prop) [DecidablePred (genericTrue apply R scope)] (V : Finset (Set Property)) (hV : ↑V = X.precisifications) : genericSubTrue X apply R scope ∧ ¬genericSuperTrue X apply R scope ↔ SignType.supervaluation V (genericTrue apply R scope) = 0

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 and 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

The domain precision of a noun phrase's restriction, Section 4.1.2.

• precise : DomainPrecision
• vague : DomainPrecision

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

@[instance_reducible]

instance KadmonLandman1993.instReprDomainPrecision : Repr DomainPrecision

Equations

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

structure KadmonLandman1993.AlmostRow : Type

An almost row records the noun phrase, its precision, whether it is a true universal and whether it is dimensionally universal, and the judgment.

• precision : DomainPrecision
• universal : Bool
• dimUniversal : Bool
• ok : Bool

def KadmonLandman1993.instDecidableEqAlmostRow.decEq (x✝ x✝¹ : AlmostRow) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance KadmonLandman1993.instDecidableEqAlmostRow : DecidableEq AlmostRow

Equations

• KadmonLandman1993.instDecidableEqAlmostRow = KadmonLandman1993.instDecidableEqAlmostRow.decEq

def KadmonLandman1993.AlmostRow.ofDatum (e : Datum) : Option AlmostRow

An almost row from the paper's features.

Equations

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

def KadmonLandman1993.almostRows : List AlmostRow

The almost data of Sections 4.1.1 and 4.3.

Equations

• KadmonLandman1993.almostRows = List.filterMap KadmonLandman1993.AlmostRow.ofDatum KadmonLandman1993.Examples.all

theorem KadmonLandman1993.almost_rows (r : AlmostRow) : r ∈ almostRows → (r.ok = true ↔ r.universal = true ∧ r.precision = DomainPrecision.precise ∨ r.dimUniversal = true)

Almost modifies a domain-precise true universal or a dimensionally universal noun phrase, such as every owl, no owl and any owl, but not some owl nor generic an owl.

The licensing data

inductive KadmonLandman1993.Context : Type

The licensing contexts the paper's rows name.

• negation : Context
• generic : Context
• universalRestrictor : Context
• adversative : Context
• conditionalAntecedent : Context

@[instance_reducible]

instance KadmonLandman1993.instDecidableEqContext : DecidableEq Context

Equations

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

@[instance_reducible]

instance KadmonLandman1993.instReprContext : Repr Context

Equations

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

def KadmonLandman1993.instReprContext.repr : Context → ℕ → Std.Format

Equations

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

def KadmonLandman1993.Context.toLicensingContext : Context → PolarityItem.LicensingContext

The library's licensing context a row's context is.

Equations

• KadmonLandman1993.Context.negation.toLicensingContext = PolarityItem.LicensingContext.negation
• KadmonLandman1993.Context.generic.toLicensingContext = PolarityItem.LicensingContext.generic
• KadmonLandman1993.Context.universalRestrictor.toLicensingContext = PolarityItem.LicensingContext.universalRestrictor
• KadmonLandman1993.Context.adversative.toLicensingContext = PolarityItem.LicensingContext.adversative
• KadmonLandman1993.Context.conditionalAntecedent.toLicensingContext = PolarityItem.LicensingContext.conditionalAntecedent

structure KadmonLandman1993.Row : Type

A licensing row records the context at the narrowest operator over any, a licensing context or a local entailment signature, the settle-for-less and metalinguistic-denial readings, and the judgment.

• context : Option Context
• localSignature : NaturalLogic.Signature
• settleForLess : Bool
• metalinguistic : Bool
• grammatical : Bool

def KadmonLandman1993.contextOf : String → Option Context

Equations

• KadmonLandman1993.contextOf "negation" = some KadmonLandman1993.Context.negation
• KadmonLandman1993.contextOf "generic" = some KadmonLandman1993.Context.generic
• KadmonLandman1993.contextOf "universalRestrictor" = some KadmonLandman1993.Context.universalRestrictor
• KadmonLandman1993.contextOf "adversative" = some KadmonLandman1993.Context.adversative
• KadmonLandman1993.contextOf "conditionalAntecedent" = some KadmonLandman1993.Context.conditionalAntecedent
• KadmonLandman1993.contextOf x✝ = none

def KadmonLandman1993.signatureOf : String → Option NaturalLogic.Signature

Equations

• KadmonLandman1993.signatureOf "all" = some NaturalLogic.Signature.all
• KadmonLandman1993.signatureOf "mono" = some NaturalLogic.Signature.mono
• KadmonLandman1993.signatureOf "anti" = some NaturalLogic.Signature.anti
• KadmonLandman1993.signatureOf "mult" = some NaturalLogic.Signature.mult
• KadmonLandman1993.signatureOf x✝ = none

def KadmonLandman1993.Row.ofDatum (e : Datum) : Option Row

A row from the paper's features.

Equations

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

def KadmonLandman1993.rows : List Row

The licensing data of Sections 1 to 3.

Equations

• KadmonLandman1993.rows = List.filterMap KadmonLandman1993.Row.ofDatum KadmonLandman1993.Examples.all

theorem KadmonLandman1993.rows_agree (r : Row) : r ∈ rows → (r.grammatical = true ↔ (∃ c ∈ r.context, c.toLicensingContext.licenser.Licenses English.PolarityItems.any) ∨ r.localSignature.toDEStrength ≠ ⊥ ∨ r.settleForLess = true ∨ r.metalinguistic = true)

On the paper's own data, any is grammatical exactly when its context licenses it, as a downward-entailing or a generic context, or the local signature is downward entailing, so widening strengthens, or it is read as settling for less under glad, or as a metalinguistic denial under a negated because.