Polarity Builder — Derived NPI Licensing from Entailment Signatures #
@cite{von-fintel-1999} @cite{icard-2012}
Bridge between the theory-neutral Fragment (DEStrength) and the formal
monotonicity hierarchy (IsDE, IsAntiAdditive, IsAntiMorphic, IsStrawsonDE).
Design principle #
A MonotonicityProfile bundles a context with its @cite{icard-2012} projectivity
signature (EntailmentSig). All DE/AA/AM classification is derived from the
signature via EntailmentSig.toDEStrength — no independent Bool flags. Only
isStrawsonDE remains independent, since Strawson-DE is
not captured by the standard entailment signature lattice.
Key result #
"Only" has strongestLevel = none (not classically DE) yet
licensesWeakNPI = true (Strawson-DE suffices). This is @cite{von-fintel-1999}'s central insight, derived not stipulated.
A context function bundled with its @cite{icard-2012} entailment signature.
The entSig is the single source of truth for DE/AA/AM classification:
Bool flags (isDE, isAA, isAM) are derived from the signature via
EntailmentSig.toDEStrength, not stored independently.
isStrawsonDE remains an independent flag because Strawson-DE is not captured by the standard entailment signature lattice.
- name : String
Name for documentation
- entSig : Core.NaturalLogic.EntailmentSig
@cite{icard-2012} entailment signature
- isStrawsonDE : Bool
Is Strawson-DE? (independent of entSig)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Derived: is the context DE (any DE strength)?
Equations
- p.isDE = p.entSig.toDEStrength.isSome
Instances For
Derived: is the context anti-additive?
Equations
- p.isAA = match p.entSig.toDEStrength with | some Core.NaturalLogic.DEStrength.antiAdditive => true | some Core.NaturalLogic.DEStrength.antiMorphic => true | x => false
Instances For
Derived: is the context anti-morphic?
Equations
Instances For
Strongest DE level, derived from entSig.
Maps to the Fragment's DEStrength enum. Strawson-DE is intentionally
excluded: it doesn't correspond to a classical DE level.
Equations
Instances For
Does this profile have at least Strawson-DE?
Equations
- p.isAtLeastStrawsonDE = (p.isDE || p.isStrawsonDE)
Instances For
Derived: licenses weak NPIs.
Requires at least DE, or Strawson-DE. This is the key insight: Strawson-DE suffices for weak NPI licensing.
Equations
Instances For
Derived: licenses strong NPIs.
Requires anti-additive. Strawson-DE and plain DE are insufficient for strong NPIs like "lift a finger".
Equations
- p.licensesStrongNPI = p.isAA
Instances For
Derive ContextPolarity from entSig.
Equations
Instances For
Negation profile: anti-morphic (strongest level).
Negation licenses both weak and strong NPIs.
Equations
- Semantics.Entailment.PolarityBuilder.negationProfile = { name := "negation", entSig := Core.NaturalLogic.EntailmentSig.antiAddMult }
Instances For
"No student" profile: anti-additive.
"No student" licenses both weak and strong NPIs.
Equations
- Semantics.Entailment.PolarityBuilder.noStudentProfile = { name := "no_student", entSig := Core.NaturalLogic.EntailmentSig.antiAdd }
Instances For
"At most 2 students" profile: DE only.
"At most n" licenses weak NPIs but not strong NPIs.
Equations
- Semantics.Entailment.PolarityBuilder.atMost2Profile = { name := "atMost2_student", entSig := Core.NaturalLogic.EntailmentSig.anti }
Instances For
"Only" profile: Strawson-DE only (not classically DE).
Von Fintel's central example: "only" is Strawson-DE but not DE.
It licenses weak NPIs despite not being classically DE.
entSig is mono (only is UE in its presupposition argument),
but the key fact is it's Strawson-DE without being classically DE.
Equations
- Semantics.Entailment.PolarityBuilder.onlyProfile = { name := "only", entSig := Core.NaturalLogic.EntailmentSig.mono, isStrawsonDE := true }
Instances For
Negation: AM → licenses both weak and strong NPIs #
"No student": AA → licenses both #
"At most 2 students": DE → licenses weak only #
"Only": Strawson-DE only → licenses weak but NOT strong #
Von Fintel's central insight, derived not stipulated: "only" licenses weak NPIs despite not being classically DE.
This is the key separation theorem: strongestLevel = none (no classical
DE level) yet licensesWeakNPI = true (Strawson-DE suffices).
The Bool flags above are justified by formal proofs in the dependency chain. These witness theorems connect profiles to their semantic proofs.
Negation is anti-morphic (formal proof).
Negation is anti-additive (formal proof).
Negation is DE (formal proof).
"No student" is anti-additive (formal proof).
"No student" is DE (formal proof).
"At most 2 students" is DE (formal proof).
"Only" is Strawson-DE (formal proof).
"Only" is NOT DE (formal proof).
The builder's licensing predictions are consistent with the hierarchy: AM ⊃ AA ⊃ DE ⊃ Strawson-DE for weak NPI licensing.
Strong NPI licensing requires anti-additive: only AM and AA profiles suffice.
Derive whether a monotonicity profile licenses a specific polarity item.
This bridges the Builder's monotonicity proofs to the Fragment's empirical item types. Licensing is derived from the profile's proved properties and the item's polarity type — not stipulated.
Equations
- One or more equations did not get rendered due to their size.
Instances For
7a. Per-item bridge: Negation (AM) #
7b. Per-item bridge: "No student" (AA) #
7c. Per-item bridge: "At most 2" (DE) #
7d. Per-item bridge: "Only" (Strawson-DE) #
isLicensedIn ↔ licensesItem agreement #
The Fragment's isLicensedIn says whether a context is in an item's
empirical licensing list. The Builder's licensesItem derives licensing
from monotonicity proofs. These should agree: when a context licenses an
item empirically, the corresponding monotonicity profile should derive the
same prediction.
Negation empirically licenses "ever" and the Builder agrees.
Negation empirically licenses "lift a finger" and the Builder agrees.
"Only" empirically licenses "ever" (via only_focus) and the Builder agrees.
"At most 2" empirically blocks "lift a finger" and the Builder agrees.
PPIs: "some (stressed)" not licensed under negation, Builder agrees.
strengthSufficient ↔ licensesWeakNPI/licensesStrongNPI agreement #
strengthSufficient from AntiAdditivity.lean checks the DEStrength
hierarchy. The Builder's derived licensing should agree with it for each
profile-to-strength mapping.
AM profile: strength sufficient for both weak and strong, Builder agrees.
AA profile: strength sufficient for both, Builder agrees.
DE profile: sufficient for weak but not strong, Builder agrees.
Full hierarchy agreement: strengthSufficient and Builder licensing are
consistent across all 4 levels × 2 NPI types.
EntailmentSig-derived property verification #
All DE/AA/AM flags are now derived from entSig. Verify they produce the expected values for each profile.
Negation: ◇⊟ →.downward, strongest =.antiMorphic
"No student": ◇ →.downward, strongest =.antiAdditive
"At most 2": − →.downward, strongest =.weak DE
"Only": mono →.upward (not classically DE; Strawson-DE only)