Chierchia 2006: Domain Widening and the PSI Typology

@cite{chierchia-2006} @cite{chierchia-2013} @cite{fox-2007} @cite{bar-lev-fox-2020} @cite{haspelmath-1997} @cite{kadmon-landman-1993} @cite{alonso-ovalle-moghiseh-2025}

Formalizes the lasting contributions of @cite{chierchia-2006} "Broaden Your Views: Implicatures of Domain Widening and the 'Logicality' of Language."

What survived to 2026 consensus

The paper's central contribution is the parametric decomposition of polarity-sensitive items (PSIs) along two dimensions:

1. Domain alternative grain: MAX (large subdomains only, even-like) vs MIN (all subdomains including singletons, antiexhaustive)
2. Strengthening requirement: whether exhaustification must yield proper strengthening (result strictly stronger than plain meaning)

The specific operators (O/E/O⁻, σ/σ̃) have been superseded by Innocent Exclusion + Innocent Inclusion (@cite{fox-2007}, @cite{bar-lev-fox-2020}), but the parametric space endures as the standard cross-linguistic PSI classification.

What was superseded

• O/E/O⁻ enrichment operators → replaced by IE + II
• σ/σ̃ as LF operators with feature checking → replaced by obligatory exhaustification and closure properties
• Recursive pragmatics as sole mechanism → pluralistic consensus (grammatical exh + RSA + team semantics)

Key result

Each PSI class maps to a contiguous region on @cite{haspelmath-1997}'s implicational map, explaining why indefinite pronoun series cover contiguous function ranges cross-linguistically.

Theoretical engine

The mechanism behind PSI licensing is domain widening reversal (@cite{kadmon-landman-1993}, proved in Exhaustification.FreeChoice): widening strengthens in DE but weakens in UE. The PSI parameter space refines this into D-MAX (even-like) vs D-MIN (antiexhaustive) enrichment.

inductive Phenomena.Polarity.Studies.Chierchia2006.DomainAltGrain : Type

Domain alternative grain size.

@cite{chierchia-2006} table (76)/(94):

• max: Only large subdomains. Triggers even-like enrichment (E): the speaker chose the strongest alternative she has evidence for. Pure NPIs (alcuno, mai, ever).
• min: All subdomains including singletons. Triggers antiexhaustive enrichment (O⁻ in 2006; IE+II in 2026): every subdomain must be satisfiable, yielding universal-like force. FCIs (any, qualsiasi, irgendein).

• max : DomainAltGrain
• min : DomainAltGrain

instance Phenomena.Polarity.Studies.Chierchia2006.instDecidableEqDomainAltGrain : DecidableEq DomainAltGrain

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instDecidableEqDomainAltGrain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Polarity.Studies.Chierchia2006.instBEqDomainAltGrain.beq : DomainAltGrain → DomainAltGrain → Bool

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instBEqDomainAltGrain.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Polarity.Studies.Chierchia2006.instBEqDomainAltGrain : BEq DomainAltGrain

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instBEqDomainAltGrain = { beq := Phenomena.Polarity.Studies.Chierchia2006.instBEqDomainAltGrain.beq }

def Phenomena.Polarity.Studies.Chierchia2006.instReprDomainAltGrain.repr : DomainAltGrain → ℕ → Std.Format

Equations

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

instance Phenomena.Polarity.Studies.Chierchia2006.instReprDomainAltGrain : Repr DomainAltGrain

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instReprDomainAltGrain = { reprPrec := Phenomena.Polarity.Studies.Chierchia2006.instReprDomainAltGrain.repr }

structure Phenomena.Polarity.Studies.Chierchia2006.PSIProfile : Type

The PSI profile: the 2026-consensus distillation of @cite{chierchia-2006}'s parametric PSI typology.

The original paper used σ (weak) vs σ̃ (presuppositional) for implicature freezing, and O/E/O⁻ for enrichment. These specific operators have been superseded by IE+II (@cite{bar-lev-fox-2020}), but the parameters they encode remain the standard way to classify PSIs cross-linguistically.

• grain : DomainAltGrain

  Domain alternative grain (MAX vs MIN)

• obligatoryDomainAlts : Bool

  Whether domain alternatives are obligatorily active

• requiresProperStrengthening : Bool

  Whether exhaustification must yield proper strengthening (corresponds to @cite{chierchia-2006}'s presuppositional σ̃)

• hasScalarAlts : Bool

  Whether scalar alternatives are also activated

def Phenomena.Polarity.Studies.Chierchia2006.instDecidableEqPSIProfile.decEq (x✝ x✝¹ : PSIProfile) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Polarity.Studies.Chierchia2006.instDecidableEqPSIProfile : DecidableEq PSIProfile

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instDecidableEqPSIProfile = Phenomena.Polarity.Studies.Chierchia2006.instDecidableEqPSIProfile.decEq

instance Phenomena.Polarity.Studies.Chierchia2006.instBEqPSIProfile : BEq PSIProfile

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instBEqPSIProfile = { beq := Phenomena.Polarity.Studies.Chierchia2006.instBEqPSIProfile.beq }

def Phenomena.Polarity.Studies.Chierchia2006.instBEqPSIProfile.beq : PSIProfile → PSIProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Polarity.Studies.Chierchia2006.instBEqPSIProfile.beq x✝¹ x✝ = false

def Phenomena.Polarity.Studies.Chierchia2006.instReprPSIProfile.repr : PSIProfile → ℕ → Std.Format

Equations

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

instance Phenomena.Polarity.Studies.Chierchia2006.instReprPSIProfile : Repr PSIProfile

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instReprPSIProfile = { reprPrec := Phenomena.Polarity.Studies.Chierchia2006.instReprPSIProfile.repr }

def Phenomena.Polarity.Studies.Chierchia2006.pureNPI : PSIProfile

Pure NPIs: alcuno (Italian), mai (Italian), ever (English). D-MAX, obligatory, weak σ, no scalar.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2006.npiFCI : PSIProfile

NPI/FCIs: English any. D-MIN, obligatory, weak σ, no scalar. NPI in DE (exhaustification vacuous), FCI under modals.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2006.pureFCI : PSIProfile

Pure universal FCIs: Italian qualsiasi/qualunque. D-MIN, obligatory, presuppositional σ̃, no scalar. Positive polarity: proper strengthening fails in DE.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2006.efciNpiFci : PSIProfile

Existential FCI (NPI/FCI): German irgendein. D-MIN, obligatory, weak σ, with scalar alts. Like any but with scalar implicatures; needs rescue mechanisms.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2006.efciPureFci : PSIProfile

Existential pure FCI: Italian uno qualsiasi. D-MIN, obligatory, presuppositional σ̃, with scalar alts.

Equations

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

Connecting PSI Theory to Distributional Typology

Each PSI class predicts an eligible region on @cite{haspelmath-1997}'s implicational map — the set of functions where items of that class can appear. The eligible region is derived from the PSI parameters and the monotonicity classification of Haspelmath functions (isDE, isFC), not hardcoded.

The derivation:

• No obligatory alts (plain indefinites): No polarity sensitivity → eligible only where neither DE licensing nor FC licensing is required.
• D-MAX, weak σ (pure NPIs): Even-like enrichment (E) is informative only in DE contexts → filter to DE functions.
• D-MAX, σ̃: Contradictory — even-like enrichment requires DE, but σ̃'s proper strengthening fails in DE (sigma_bold_fails_in_de) → empty.
• D-MIN, weak σ (NPI/FCIs): In DE, exhaustification is vacuous → NPI; under modals, antiexhaustive → FC. Also usable in irrealis. Filter to DE ∪ FC ∪ irrealis.
• D-MIN, σ̃ (pure FCIs): Proper strengthening fails in DE → filter to FC only.

def Phenomena.Polarity.Studies.Chierchia2006.PSIProfile.predictedFunctions (p : PSIProfile) : List Typology.IndefiniteFunction

The Haspelmath functions predicted by a PSI class.

Derived from PSI parameters via the monotonicity classification of Haspelmath functions (IndefiniteFunction.isDE, IndefiniteFunction.isFC). Each branch filters IndefiniteFunction.all by the semantic property that the PSI class's enrichment mechanism targets.

Equations

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

Each PSI class maps to a contiguous Haspelmath region

This is the central bridge between @cite{chierchia-2006}'s exhaustification theory and @cite{haspelmath-1997}'s typological generalization. It explains why indefinite pronoun series cover contiguous function ranges: each PSI class's eligible region is contiguous, and surface forms cover contiguous subsets of their class's region.

theorem Phenomena.Polarity.Studies.Chierchia2006.pureNPI_contiguous : Typology.isContiguous pureNPI.predictedFunctions = true

Pure NPI region {question..directNeg} is contiguous.

theorem Phenomena.Polarity.Studies.Chierchia2006.npiFCI_contiguous : Typology.isContiguous npiFCI.predictedFunctions = true

NPI/FCI region {irrealis..freeChoice} is contiguous.

theorem Phenomena.Polarity.Studies.Chierchia2006.pureFCI_contiguous : Typology.isContiguous pureFCI.predictedFunctions = true

Pure FCI region {comparative, freeChoice} is contiguous.

theorem Phenomena.Polarity.Studies.Chierchia2006.efciNpiFci_contiguous : Typology.isContiguous efciNpiFci.predictedFunctions = true

EFCI NPI/FCI has same eligible region as NPI/FCI (scalar alts don't change distributional range, only add uniqueness readings).

theorem Phenomena.Polarity.Studies.Chierchia2006.efciPureFci_contiguous : Typology.isContiguous efciPureFci.predictedFunctions = true

EFCI pure FCI has same eligible region as pure FCI.

theorem Phenomena.Polarity.Studies.Chierchia2006.all_psi_classes_contiguous : ([pureNPI, npiFCI, pureFCI, efciNpiFci, efciPureFci].all fun (p : PSIProfile) => Typology.isContiguous p.predictedFunctions) = true

All five PSI classes have contiguous predicted function ranges.

theorem Phenomena.Polarity.Studies.Chierchia2006.dMax_presuppositional_empty : { grain := DomainAltGrain.max, obligatoryDomainAlts := true, requiresProperStrengthening := true, hasScalarAlts := false }.predictedFunctions = []

D-MAX + presuppositional is unattested: the combination of requiring DE contexts (D-MAX) and proper strengthening (σ̃) is contradictory, since DE contexts are exactly where strengthening fails.

Matching cross-linguistic data to PSI predictions

Each surface form's actual Haspelmath functions (from @cite{haspelmath-1997}'s typological data in Typology.lean) should be a subset of its PSI class's predicted (eligible) region.

All function lists are derived from Typology.lean profiles — not hardcoded — so changes to the typological data will break exactly the theorems they should.

theorem Phenomena.Polarity.Studies.Chierchia2006.italian_nessuno_matches : Phenomena.Polarity.Studies.Chierchia2006.functionsSubset✝ (Phenomena.Polarity.Studies.Chierchia2006.seriesFunctions✝ Typology.italian "nessuno") pureNPI.predictedFunctions = true

theorem Phenomena.Polarity.Studies.Chierchia2006.italian_qualsiasi_matches : Phenomena.Polarity.Studies.Chierchia2006.functionsSubset✝ (Phenomena.Polarity.Studies.Chierchia2006.seriesFunctions✝ Typology.italian "qualunque/qualsiasi") pureFCI.predictedFunctions = true

theorem Phenomena.Polarity.Studies.Chierchia2006.italian_qualcuno_matches : Phenomena.Polarity.Studies.Chierchia2006.functionsSubset✝ (Phenomena.Polarity.Studies.Chierchia2006.seriesFunctions✝ Typology.italian "qualcuno") { grain := DomainAltGrain.max, obligatoryDomainAlts := false, requiresProperStrengthening := false, hasScalarAlts := false }.predictedFunctions = true

theorem Phenomena.Polarity.Studies.Chierchia2006.english_anyNPI_matches : Phenomena.Polarity.Studies.Chierchia2006.functionsSubset✝ (Phenomena.Polarity.Studies.Chierchia2006.seriesFunctions✝ Typology.english "any- (NPI)") npiFCI.predictedFunctions = true

theorem Phenomena.Polarity.Studies.Chierchia2006.english_anyFC_matches : Phenomena.Polarity.Studies.Chierchia2006.functionsSubset✝ (Phenomena.Polarity.Studies.Chierchia2006.seriesFunctions✝ Typology.english "any- (FC)") npiFCI.predictedFunctions = true

theorem Phenomena.Polarity.Studies.Chierchia2006.german_irgendwer_matches : Phenomena.Polarity.Studies.Chierchia2006.functionsSubset✝ (Phenomena.Polarity.Studies.Chierchia2006.seriesFunctions✝ Typology.german "irgendwer") efciNpiFci.predictedFunctions = true

theorem Phenomena.Polarity.Studies.Chierchia2006.mandarin_shei_matches : Phenomena.Polarity.Studies.Chierchia2006.functionsSubset✝ (Phenomena.Polarity.Studies.Chierchia2006.seriesFunctions✝ Typology.mandarin "shéi (谁, non-interrog.)") npiFCI.predictedFunctions = true

Deriving the core empirical contrast

@cite{chierchia-2006}'s most striking prediction: Italian qualsiasi and English any differ under negation.

• "I didn't see any student" — grammatical (NPI reading)
• "Non ho visto qualsiasi studente" — marginal, only rhetorical ¬∀

This follows from requiresProperStrengthening: any (weak σ) allows vacuous exhaustification in DE; qualsiasi (presuppositional σ̃) requires proper strengthening, which fails in DE since the exhaustified meaning is not strictly stronger than the plain meaning.

The paper derives two LF representations for any under negation:

1. σ scopes above ¬ → freeze implicature, then negate → rhetorical reading
2. σ scopes below ¬ → negate, then check implicature → NPI reading (implicature is entailed by assertion, so it vanishes)

For qualsiasi, only option (1) is available: σ̃ requires proper strengthening, which option (2) cannot deliver (the implicature is vacuous in DE). This is formalized as the requiresProperStrengthening parameter blocking DE eligibility.

theorem Phenomena.Polarity.Studies.Chierchia2006.npiFCI_eligible_in_all_de : ((List.filter (fun (x : Typology.IndefiniteFunction) => x.isDE) Typology.IndefiniteFunction.all).all fun (x : Typology.IndefiniteFunction) => npiFCI.predictedFunctions.contains x) = true

Every DE Haspelmath function is in the NPI/FCI eligible region. D-MIN + weak σ: exhaustification is vacuous in DE (NPI reading).

theorem Phenomena.Polarity.Studies.Chierchia2006.pureFCI_not_eligible_in_any_de : ((List.filter (fun (x : Typology.IndefiniteFunction) => x.isDE) Typology.IndefiniteFunction.all).all fun (f : Typology.IndefiniteFunction) => !pureFCI.predictedFunctions.contains f) = true

No DE Haspelmath function is in the pure FCI eligible region. D-MIN + σ̃: proper strengthening fails in DE (sigma_bold_fails_in_de).

theorem Phenomena.Polarity.Studies.Chierchia2006.pureNPI_eligible_in_all_de : ((List.filter (fun (x : Typology.IndefiniteFunction) => x.isDE) Typology.IndefiniteFunction.all).all fun (x : Typology.IndefiniteFunction) => pureNPI.predictedFunctions.contains x) = true

Every DE function is in the pure NPI eligible region. D-MAX + weak σ: even-like enrichment is informative in DE.

theorem Phenomena.Polarity.Studies.Chierchia2006.pureNPI_not_eligible_in_fc : ((List.filter (fun (x : Typology.IndefiniteFunction) => x.isFC) Typology.IndefiniteFunction.all).all fun (f : Typology.IndefiniteFunction) => !pureNPI.predictedFunctions.contains f) = true

No FC function is in the pure NPI eligible region. D-MAX items lack antiexhaustive enrichment.

theorem Phenomena.Polarity.Studies.Chierchia2006.dMin_sigma_determines_de : ((List.filter (fun (x : Typology.IndefiniteFunction) => x.isDE) Typology.IndefiniteFunction.all).all fun (f : Typology.IndefiniteFunction) => npiFCI.predictedFunctions.contains f && !pureFCI.predictedFunctions.contains f) = true

The qualsiasi/any contrast: among D-MIN items, every DE function is included by weak σ (any) and excluded by σ̃ (qualsiasi).

Connection to @cite{alonso-ovalle-moghiseh-2025}

PSI profiles predict which EFCI rescue mechanism is available:

• Items with hasScalarAlts = true activate both scalar and domain alternatives, creating the EFCI contradiction.
• requiresProperStrengthening constrains rescue: presuppositional σ̃ limits to partial exhaustification (proper strengthening preserved).

def Phenomena.Polarity.Studies.Chierchia2006.PSIProfile.toEFCIRescue (p : PSIProfile) : Option AlonsoOvalleMoghiseh2025.EFCIRescue

Map PSI profiles to EFCI rescue type (none if not an EFCI).

Equations

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

def Phenomena.Polarity.Studies.Chierchia2006.PSIProfile.toFCIFlavor (p : PSIProfile) : Option AlonsoOvalleMoghiseh2025.FCIFlavor

Map PSI profiles to FCI flavor (none if not an FCI). Only D-MIN items are FCIs — D-MAX items are pure NPIs.

Equations

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

theorem Phenomena.Polarity.Studies.Chierchia2006.irgendein_is_existential : efciNpiFci.toFCIFlavor = some AlonsoOvalleMoghiseh2025.FCIFlavor.existential

theorem Phenomena.Polarity.Studies.Chierchia2006.any_is_universal : npiFCI.toFCIFlavor = some AlonsoOvalleMoghiseh2025.FCIFlavor.universal

theorem Phenomena.Polarity.Studies.Chierchia2006.qualsiasi_is_universal : pureFCI.toFCIFlavor = some AlonsoOvalleMoghiseh2025.FCIFlavor.universal

theorem Phenomena.Polarity.Studies.Chierchia2006.pureNPI_not_fci : pureNPI.toFCIFlavor = none

theorem Phenomena.Polarity.Studies.Chierchia2006.irgendein_rescue_both : efciNpiFci.toEFCIRescue = some AlonsoOvalleMoghiseh2025.EFCIRescue.both

theorem Phenomena.Polarity.Studies.Chierchia2006.pureNPI_no_rescue : pureNPI.toEFCIRescue = none

Bridging PSI profiles to Fragment entries

Core.Lexical.PolarityItem.PolarityType is a 5-way distributional classification. PSIProfile is a 4-parameter theoretical decomposition. Each PSI class predicts exactly one PolarityType, and each Fragment entry's polarityType should match its PSI profile's predicted type.

def Phenomena.Polarity.Studies.Chierchia2006.PSIProfile.toPolarityType (p : PSIProfile) : Core.Lexical.PolarityItem.PolarityType

Map a PSI profile to the expected PolarityType.

Equations

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

theorem Phenomena.Polarity.Studies.Chierchia2006.pureNPI_polarityType : pureNPI.toPolarityType = Core.Lexical.PolarityItem.PolarityType.npiWeak

theorem Phenomena.Polarity.Studies.Chierchia2006.npiFCI_polarityType : npiFCI.toPolarityType = Core.Lexical.PolarityItem.PolarityType.npi_fci

theorem Phenomena.Polarity.Studies.Chierchia2006.pureFCI_polarityType : pureFCI.toPolarityType = Core.Lexical.PolarityItem.PolarityType.fci

theorem Phenomena.Polarity.Studies.Chierchia2006.efciNpiFci_polarityType : efciNpiFci.toPolarityType = Core.Lexical.PolarityItem.PolarityType.npi_fci

theorem Phenomena.Polarity.Studies.Chierchia2006.efciPureFci_polarityType : efciPureFci.toPolarityType = Core.Lexical.PolarityItem.PolarityType.fci

theorem Phenomena.Polarity.Studies.Chierchia2006.any_profile_consistent : Fragments.English.PolarityItems.any.polarityType = npiFCI.toPolarityType

theorem Phenomena.Polarity.Studies.Chierchia2006.ever_profile_consistent : Fragments.English.PolarityItems.ever.polarityType = pureNPI.toPolarityType

theorem Phenomena.Polarity.Studies.Chierchia2006.mai_profile_consistent : Fragments.Italian.PolarityItems.mai.polarityType = pureNPI.toPolarityType

theorem Phenomena.Polarity.Studies.Chierchia2006.alcuno_profile_consistent : Fragments.Italian.PolarityItems.alcuno.polarityType = pureNPI.toPolarityType

theorem Phenomena.Polarity.Studies.Chierchia2006.nessuno_profile_consistent : Fragments.Italian.PolarityItems.nessuno.polarityType = pureNPI.toPolarityType

theorem Phenomena.Polarity.Studies.Chierchia2006.qualsiasi_profile_consistent : Fragments.Italian.PolarityItems.qualsiasi.polarityType = pureFCI.toPolarityType

theorem Phenomena.Polarity.Studies.Chierchia2006.qualunque_profile_consistent : Fragments.Italian.PolarityItems.qualunque.polarityType = pureFCI.toPolarityType

theorem Phenomena.Polarity.Studies.Chierchia2006.uno_qualsiasi_profile_consistent : Fragments.Italian.PolarityItems.uno_qualsiasi.polarityType = efciPureFci.toPolarityType

theorem Phenomena.Polarity.Studies.Chierchia2006.irgendein_profile_consistent : Fragments.German.PolarityItems.irgendein.polarityType = efciNpiFci.toPolarityType

Exercising the Exhaustification theory layer

This section connects @cite{chierchia-2006}'s PSI typology to the formal results in Exhaustification.FreeChoice and Exhaustification.Operators.

σ̃: Presuppositional implicature freezing (§3.3, §5.3)

σ "freezes" the implicature; σ̃ adds a presupposition that the frozen meaning is strictly stronger than the plain meaning (definition (72)). sigma_bold_fails_in_de delegates to entailment_reversal_in_de.

SI vacuity in DE (§4.1)

D-MAX (even-like) enrichment is an SI. SIs are vacuous in DE (si_vacuous_in_de), explaining why pure NPIs are confined to DE.

O⁻ yields universal force (§5.1)

Antiexhaustive enrichment of ∃x∈D.P(x) with D-MIN alternatives gives ∀a∈D. P(a) (antiexh_yields_universal). This is the "birth of universal readings" behind FCI universal force.

def Phenomena.Polarity.Studies.Chierchia2006.sigmaBoldDefined {World : Type u_1} (plain enriched : World → Prop) : Prop

σ̃'s presupposition: the enriched meaning is strictly stronger than the plain meaning. @cite{chierchia-2006} definition (72).

This must hold for σ̃ to be defined (felicitous). Items selecting σ̃ (qualsiasi, qualunque) require proper strengthening; items selecting plain σ (any, ever) don't.

Equations

• Phenomena.Polarity.Studies.Chierchia2006.sigmaBoldDefined plain enriched = ((∀ (w : World), enriched w → plain w) ∧ ¬∀ (w : World), plain w → enriched w)

theorem Phenomena.Polarity.Studies.Chierchia2006.sigma_bold_fails_in_de {World : Type u_1} (C : (World → Prop) → World → Prop) (hDE : ∀ (p q : World → Prop), (∀ (w : World), p w → q w) → ∀ (w : World), C q w → C p w) (plain enriched : World → Prop) (h_stronger : ∀ (w : World), enriched w → plain w) : ¬sigmaBoldDefined (C plain) (C enriched)

σ̃'s presupposition fails in DE contexts.

@cite{chierchia-2006} §5.3: This is the formal content of the qualsiasi/any contrast. If enrichment properly strengthens at the base level (enriched ⊂ plain), then embedding in a DE context reverses the entailment: C(plain) ⊆ C(enriched), making the enriched meaning under C strictly WEAKER, not stronger.

Delegates to Exhaustification.FreeChoice.entailment_reversal_in_de: the DE reversal gives C(plain) ⊆ C(enriched), which contradicts σ̃'s requirement that C(enriched) be strictly stronger than C(plain).

theorem Phenomena.Polarity.Studies.Chierchia2006.dMax_enrichment_vacuous_in_de {World : Type u_1} (C : (World → Prop) → World → Prop) (hDE : ∀ (p q : World → Prop), (∀ (w : World), p w → q w) → ∀ (w : World), C q w → C p w) (weak strong : World → Prop) (h_ent : ∀ (w : World), strong w → weak w) (w : World) : ¬(C weak w ∧ ¬C strong w)

SI vacuity in DE blocks D-MAX enrichment in UE.

@cite{chierchia-2006} §4.1: D-MAX items (pure NPIs) trigger even-like (E) enrichment, which is an SI. SIs are vacuous in DE (si_vacuous_in_de), so E enrichment is informative only in non-DE contexts — but D-MAX items require DE. This is why pure NPIs are confined to DE contexts.

Instantiates Exhaustification.FreeChoice.si_vacuous_in_de.

theorem Phenomena.Polarity.Studies.Chierchia2006.fci_universal_from_oMinus {World : Type u_1} {Entity : Type u_2} (D : List Entity) (P : Entity → World → Prop) (w : World) (h : Exhaustification.oMinus (Exhaustification.dMinAlts D P) (Exhaustification.existsIn D P) w) (a : Entity) : a ∈ D → P a w

O⁻ yields universal force from existential base (§5.1).

D-MIN items (FCIs) activate all subdomain alternatives. When antiexhaustive enrichment (O⁻) is applied to ∃x∈D.P(x) with D-MIN alternatives, the result entails ∀a∈D. P(a).

This is the "birth of universal readings" — re-exported from Exhaustification.antiexh_yields_universal.

Italian FCI judgment data from @cite{chierchia-2006} §2

These observations are the core empirical motivations:

1. Two FCI constructions: [qualsiasi/qualunque N] (universal FCI) vs [un N qualsiasi/qualunque] (existential FCI)
2. Quantificational force contrast: universal FCI → ∀; existential FCI → ∃
3. Subtrigging: bare universal FCIs are marginal in episodic contexts; adding a relative clause modifier restores grammaticality
4. Negation scope: universal FCIs under negation yield only ¬∀ (rhetorical reading), not NPI ¬∃

inductive Phenomena.Polarity.Studies.Chierchia2006.Judgment : Type

Grammaticality judgment for Italian FCI constructions.

• grammatical : Judgment
• marginal : Judgment
• ungrammatical : Judgment

instance Phenomena.Polarity.Studies.Chierchia2006.instDecidableEqJudgment : DecidableEq Judgment

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instDecidableEqJudgment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Polarity.Studies.Chierchia2006.instBEqJudgment : BEq Judgment

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instBEqJudgment = { beq := Phenomena.Polarity.Studies.Chierchia2006.instBEqJudgment.beq }

def Phenomena.Polarity.Studies.Chierchia2006.instBEqJudgment.beq : Judgment → Judgment → Bool

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instBEqJudgment.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Polarity.Studies.Chierchia2006.instReprJudgment : Repr Judgment

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instReprJudgment = { reprPrec := Phenomena.Polarity.Studies.Chierchia2006.instReprJudgment.repr }

def Phenomena.Polarity.Studies.Chierchia2006.instReprJudgment.repr : Judgment → ℕ → Std.Format

Equations

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

inductive Phenomena.Polarity.Studies.Chierchia2006.QForce : Type

Quantificational force of the FCI reading.

• universal : QForce
• existential : QForce
• ambiguous : QForce

instance Phenomena.Polarity.Studies.Chierchia2006.instDecidableEqQForce : DecidableEq QForce

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instDecidableEqQForce x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Polarity.Studies.Chierchia2006.instBEqQForce : BEq QForce

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instBEqQForce = { beq := Phenomena.Polarity.Studies.Chierchia2006.instBEqQForce.beq }

def Phenomena.Polarity.Studies.Chierchia2006.instBEqQForce.beq : QForce → QForce → Bool

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instBEqQForce.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Polarity.Studies.Chierchia2006.instReprQForce : Repr QForce

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instReprQForce = { reprPrec := Phenomena.Polarity.Studies.Chierchia2006.instReprQForce.repr }

def Phenomena.Polarity.Studies.Chierchia2006.instReprQForce.repr : QForce → ℕ → Std.Format

Equations

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

inductive Phenomena.Polarity.Studies.Chierchia2006.FCIType : Type

FCI construction type: [qualsiasi N] vs [un N qualsiasi].

• universal : FCIType
• existential : FCIType

instance Phenomena.Polarity.Studies.Chierchia2006.instDecidableEqFCIType : DecidableEq FCIType

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instDecidableEqFCIType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Polarity.Studies.Chierchia2006.instBEqFCIType : BEq FCIType

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instBEqFCIType = { beq := Phenomena.Polarity.Studies.Chierchia2006.instBEqFCIType.beq }

def Phenomena.Polarity.Studies.Chierchia2006.instBEqFCIType.beq : FCIType → FCIType → Bool

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instBEqFCIType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Polarity.Studies.Chierchia2006.instReprFCIType : Repr FCIType

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instReprFCIType = { reprPrec := Phenomena.Polarity.Studies.Chierchia2006.instReprFCIType.repr }

def Phenomena.Polarity.Studies.Chierchia2006.instReprFCIType.repr : FCIType → ℕ → Std.Format

Equations

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

inductive Phenomena.Polarity.Studies.Chierchia2006.FCIContext : Type

Embedding context for FCI observations.

• future : FCIContext
• imperative : FCIContext
• episodic_bare : FCIContext
• episodic_subtrigged : FCIContext
• negation_bare : FCIContext
• negation_subtrigged : FCIContext

instance Phenomena.Polarity.Studies.Chierchia2006.instDecidableEqFCIContext : DecidableEq FCIContext

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instDecidableEqFCIContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Polarity.Studies.Chierchia2006.instBEqFCIContext : BEq FCIContext

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instBEqFCIContext = { beq := Phenomena.Polarity.Studies.Chierchia2006.instBEqFCIContext.beq }

def Phenomena.Polarity.Studies.Chierchia2006.instBEqFCIContext.beq : FCIContext → FCIContext → Bool

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instBEqFCIContext.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Polarity.Studies.Chierchia2006.instReprFCIContext : Repr FCIContext

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instReprFCIContext = { reprPrec := Phenomena.Polarity.Studies.Chierchia2006.instReprFCIContext.repr }

def Phenomena.Polarity.Studies.Chierchia2006.instReprFCIContext.repr : FCIContext → ℕ → Std.Format

Equations

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

structure Phenomena.Polarity.Studies.Chierchia2006.FCIObservation : Type

An Italian FCI observation from @cite{chierchia-2006} §2.

• sentence : String

  The sentence (schematic)

• exampleNum : String

  Example number in the paper

• fciType : FCIType

  FCI construction type

• context : FCIContext

  Embedding context

• force : QForce

  Available quantificational force

• judgment : Judgment

  Grammaticality judgment

def Phenomena.Polarity.Studies.Chierchia2006.instReprFCIObservation.repr : FCIObservation → ℕ → Std.Format

Equations

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

instance Phenomena.Polarity.Studies.Chierchia2006.instReprFCIObservation : Repr FCIObservation

Equations

• Phenomena.Polarity.Studies.Chierchia2006.instReprFCIObservation = { reprPrec := Phenomena.Polarity.Studies.Chierchia2006.instReprFCIObservation.repr }

def Phenomena.Polarity.Studies.Chierchia2006.obs_10a : FCIObservation

(10a): "Domani interrogherò qualsiasi studente" (future, universal FCI) — Both ∀ and ∃ readings available.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2006.obs_10b : FCIObservation

(10b): "Domani interrogherò uno studente qualsiasi" (future, existential FCI) — Only ∃ reading.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2006.obs_10c : FCIObservation

(10c): "Prendi qualunque dolce" (imperative, universal FCI) — Both ∀ and ∃ readings available.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2006.obs_10d : FCIObservation

(10d): "Prendi un dolce qualunque" (imperative, existential FCI) — Only ∃ reading.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2006.obs_11a : FCIObservation

(11a): "Ieri ho parlato con un qualsiasi filosofo" (bare episodic, EFCI) — Marginal without modifier.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2006.obs_11b : FCIObservation

(11b): "Ieri ho parlato con un qualsiasi filosofo che fosse interessato" — Marginal; the paper notes RC "if anything, makes things worse" for existential FCIs. Subtrigging does not rescue EFCIs.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2006.obs_11c : FCIObservation

(11c): "Ieri ho parlato con qualsiasi filosofo" (bare episodic, universal FCI) — Marginal without modifier.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2006.obs_11d : FCIObservation

(11d): "Ieri ho parlato con qualsiasi filosofo che fosse interessato" — Fully grammatical: subtrigging rescues universal FCIs.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2006.obs_12 : FCIObservation

(12)/(73a): "Non leggerò qualunque libro" (negation + bare universal FCI) — Only ¬∀ (rhetorical) reading; NOT the NPI ¬∃ reading.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2006.obs_73b : FCIObservation

(73b): "Non leggerò qualunque libro che mi consiglierà Gianni" — With RC under negation: ∀¬ or ¬∃ readings become available.

Equations

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

theorem Phenomena.Polarity.Studies.Chierchia2006.subtrigging_rescues_universal : obs_11c.judgment = Judgment.marginal ∧ obs_11d.judgment = Judgment.grammatical

Subtrigging contrast: bare universal FCI is marginal in episodic; subtrigged universal FCI is grammatical.

theorem Phenomena.Polarity.Studies.Chierchia2006.subtrigging_no_help_existential : obs_11a.judgment = Judgment.marginal ∧ obs_11b.judgment = Judgment.marginal

Subtrigging does NOT rescue existential FCIs in episodic contexts.

theorem Phenomena.Polarity.Studies.Chierchia2006.universal_fci_ambiguous_force : ([obs_10a, obs_10c].all fun (x : FCIObservation) => x.force == QForce.ambiguous) = true

Universal FCIs always admit ∀ (and sometimes ∃): force is ambiguous.

theorem Phenomena.Polarity.Studies.Chierchia2006.existential_fci_existential_force : ([obs_10b, obs_10d].all fun (x : FCIObservation) => x.force == QForce.existential) = true

Existential FCIs have ∃ force only.

theorem Phenomena.Polarity.Studies.Chierchia2006.negation_rhetorical_only : obs_12.force = QForce.universal

Under negation, bare universal FCI yields only ¬∀ (rhetorical), not NPI ¬∃. This is the qualsiasi/any contrast: qualsiasi under negation ≠ NPI.