inductive NeoGricean.Exhaustivity.EFCI.AlternativeType : Type

Types of alternatives for EFCIs.

Scalar alternatives differ in quantificational force. Domain alternatives differ in domain restriction.

• scalar : AlternativeType

  Scalar alternatives: some vs all

• domain : AlternativeType

  Domain alternatives: ∃x∈D vs ∃x∈D' for D' ⊂ D

instance NeoGricean.Exhaustivity.EFCI.instDecidableEqAlternativeType : DecidableEq AlternativeType

Equations

• NeoGricean.Exhaustivity.EFCI.instDecidableEqAlternativeType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance NeoGricean.Exhaustivity.EFCI.instBEqAlternativeType : BEq AlternativeType

Equations

• NeoGricean.Exhaustivity.EFCI.instBEqAlternativeType = { beq := NeoGricean.Exhaustivity.EFCI.instBEqAlternativeType.beq }

def NeoGricean.Exhaustivity.EFCI.instBEqAlternativeType.beq : AlternativeType → AlternativeType → Bool

Equations

• NeoGricean.Exhaustivity.EFCI.instBEqAlternativeType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def NeoGricean.Exhaustivity.EFCI.instReprAlternativeType.repr : AlternativeType → ℕ → Std.Format

Equations

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

instance NeoGricean.Exhaustivity.EFCI.instReprAlternativeType : Repr AlternativeType

Equations

• NeoGricean.Exhaustivity.EFCI.instReprAlternativeType = { reprPrec := NeoGricean.Exhaustivity.EFCI.instReprAlternativeType.repr }

structure NeoGricean.Exhaustivity.EFCI.EFCIAlternative (World : Type u_1) : Type u_1

An EFCI alternative with its type and whether it's pre-exhaustified.

• content : Prop' World

  The propositional content

• altType : AlternativeType

  The type of alternative

• isPreExhaustified : Bool

  Is this a pre-exhaustified domain alternative?

Domain Alternatives

For an existential over domain D, domain alternatives are existentials over proper subsets D' ⊂ D.

Singleton subdomain alternatives are most relevant:

• ∃x∈{d}. P(x) = P(d)

These become the basis for pre-exhaustified alternatives.

@[reducible, inline]

abbrev NeoGricean.Exhaustivity.EFCI.Domain (Entity : Type u_3) : Type u_3

A domain: a set of entities that an existential quantifies over.

Equations

• NeoGricean.Exhaustivity.EFCI.Domain Entity = Set Entity

def NeoGricean.Exhaustivity.EFCI.singletonSubdomains {Entity : Type u_2} (D : Domain Entity) : Set (Domain Entity)

Generate singleton subdomain alternatives. For domain D = {a, b, c}, generates {a}, {b}, {c}.

Equations

• NeoGricean.Exhaustivity.EFCI.singletonSubdomains D = {S : NeoGricean.Exhaustivity.EFCI.Domain Entity | ∃ d ∈ D, S = {d}}

def NeoGricean.Exhaustivity.EFCI.existsInDomain {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (P : Entity → Prop' World) : Prop' World

The existential assertion over a domain. ∃x∈D. P(x) holds at world w iff some entity in D satisfies P at w.

Equations

• NeoGricean.Exhaustivity.EFCI.existsInDomain D P w = ∃ d ∈ D, P d w

def NeoGricean.Exhaustivity.EFCI.singletonAlt {World : Type u_1} {Entity : Type u_2} (d : Entity) (P : Entity → Prop' World) : Prop' World

A singleton domain alternative. ∃x∈{d}. P(x) = P(d)

Equations

• NeoGricean.Exhaustivity.EFCI.singletonAlt d P = P d

Pre-Exhaustified Domain Alternatives

Following @cite{chierchia-2013}, domain alternatives are pre-exhaustified: the exhaustification operator applies to them before they enter the alternative set for the main exhaustification.

For singleton alternative P(d): Pre-exh(P(d)) = P(d) ∧ ∀y≠d. ¬P(y) = "d is the only one satisfying P"

Domain alternatives convey uniqueness.

def NeoGricean.Exhaustivity.EFCI.preExhaustify {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (d : Entity) (P : Entity → Prop' World) : Prop' World

Pre-exhaustify a singleton domain alternative. P(d) becomes: P(d) ∧ ∀y∈D, y≠d → ¬P(y) "d is the unique satisfier in D"

Equations

• NeoGricean.Exhaustivity.EFCI.preExhaustify D d P w = (P d w ∧ ∀ y ∈ D, y ≠ d → ¬P y w)

def NeoGricean.Exhaustivity.EFCI.preExhDomainAlts {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (P : Entity → Prop' World) : Set (Prop' World)

The set of pre-exhaustified domain alternatives.

Equations

• NeoGricean.Exhaustivity.EFCI.preExhDomainAlts D P = {φ : Prop' World | ∃ d ∈ D, φ = NeoGricean.Exhaustivity.EFCI.preExhaustify D d P}

Scalar Alternatives

For an existential ∃x. P(x), the scalar alternative is ∀x. P(x).

In UE contexts: ∀ is stronger than ∃ In DE contexts: ∃ is stronger than ∀

def NeoGricean.Exhaustivity.EFCI.universalAlt {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (P : Entity → Prop' World) : Prop' World

The universal (scalar) alternative to an existential.

Equations

• NeoGricean.Exhaustivity.EFCI.universalAlt D P w = ∀ d ∈ D, P d w

def NeoGricean.Exhaustivity.EFCI.scalarAlts {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (P : Entity → Prop' World) : Set (Prop' World)

The scalar alternative set for an existential.

Equations

• NeoGricean.Exhaustivity.EFCI.scalarAlts D P = {NeoGricean.Exhaustivity.EFCI.universalAlt D P}

def NeoGricean.Exhaustivity.EFCI.efciAlternatives {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (P : Entity → Prop' World) : Set (Prop' World)

The full EFCI alternative set combines:

1. The prejacent (existential assertion)
2. Scalar alternatives (universal)
3. Pre-exhaustified domain alternatives

Equations

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

def NeoGricean.Exhaustivity.EFCI.scalarOnlyAlts {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (P : Entity → Prop' World) : Set (Prop' World)

Alternative set with only scalar alternatives (pruned domain). Used when partial exhaustification prunes domain alternatives.

Equations

• NeoGricean.Exhaustivity.EFCI.scalarOnlyAlts D P = {NeoGricean.Exhaustivity.EFCI.existsInDomain D P} ∪ NeoGricean.Exhaustivity.EFCI.scalarAlts D P

def NeoGricean.Exhaustivity.EFCI.domainOnlyAlts {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (P : Entity → Prop' World) : Set (Prop' World)

Alternative set with only domain alternatives (pruned scalar). Used when partial exhaustification prunes scalar alternatives.

Equations

• NeoGricean.Exhaustivity.EFCI.domainOnlyAlts D P = {NeoGricean.Exhaustivity.EFCI.existsInDomain D P} ∪ NeoGricean.Exhaustivity.EFCI.preExhDomainAlts D P

Exhaustification Operator

O_ALT(φ) = φ ∧ ∧{¬ψ : ψ ∈ IE(ALT, φ)}

where IE(ALT, φ) is the set of innocently excludable alternatives.

An alternative ψ is innocently excludable if:

• ψ is in ALT
• ψ is stronger than φ
• Negating ψ is consistent with φ and negations of other IE alternatives

def NeoGricean.Exhaustivity.EFCI.simpleExh {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) : Prop' World

Simple exhaustification: negate all stronger alternatives. This is a simplified version; full IE requires MC-set computation.

Equations

• NeoGricean.Exhaustivity.EFCI.simpleExh ALT φ w = (φ w ∧ ∀ ψ ∈ ALT, (∀ (v : World), φ v → ψ v) → ψ ≠ φ → ¬ψ w)

The Problem: Exhaustifying Both Types Causes Contradiction

Consider domain D = {a, b} and predicate "came":

1. Prejacent: ∃x∈{a,b}. came(x) = "a came ∨ b came"

2. Scalar alt: ∀x∈{a,b}. came(x) = "a came ∧ b came" After exh: ¬(a came ∧ b came) = "not both came"

3. Pre-exh domain alts:

   • [a]: came(a) ∧ ¬came(b) = "only a came"
   • [b]: came(b) ∧ ¬came(a) = "only b came" After exh: ¬[only a] ∧ ¬[only b] = (came(a) → came(b)) ∧ (came(b) → came(a)) = came(a) ↔ came(b)

Combined with prejacent (a ∨ b) and scalar neg ¬(a ∧ b):

• (a ∨ b) ∧ ¬(a ∧ b) ∧ (a ↔ b)
• = (a ∨ b) ∧ (a ⊕ b) ∧ (a ↔ b)
• = ⊥

This is why EFCIs need rescue mechanisms.

def NeoGricean.Exhaustivity.EFCI.isContradictory {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) : Prop

Check if an alternative set leads to contradiction when exhaustified.

Equations

• NeoGricean.Exhaustivity.EFCI.isContradictory ALT φ = ∀ (w : World), ¬NeoGricean.Exhaustivity.EFCI.simpleExh ALT φ w

Rescue Mechanism 1: Modal Insertion (Irgendein-type)

Insert a covert epistemic modal ◇_epi above the existential: ◇∃x. P(x)

Now domain alternatives become: ◇[P(a) ∧ ∀y≠a. ¬P(y)]

Under modal, these are compatible with each other: ◇[only a] ∧ ◇[only b] = "possibly only a, possibly only b" = modal variation

No contradiction!

def NeoGricean.Exhaustivity.EFCI.covertEpi {World : Type u_1} (φ : Prop' World) : Prop' World

Covert epistemic modal (possibility).

Equations

• NeoGricean.Exhaustivity.EFCI.covertEpi φ x✝ = ∃ (w : World), φ w

def NeoGricean.Exhaustivity.EFCI.withModalInsertion {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (P : Entity → Prop' World) : Prop' World

Modal insertion: wrap existential in covert epistemic.

Equations

• NeoGricean.Exhaustivity.EFCI.withModalInsertion D P = NeoGricean.Exhaustivity.EFCI.covertEpi (NeoGricean.Exhaustivity.EFCI.existsInDomain D P)

Rescue Mechanism 2: Partial Exhaustification (Yek-i-type)

Instead of exhaustifying both alt types, prune one:

Option A: Prune domain alts → only scalar exh Result: ∃x. P(x) ∧ ¬∀x. P(x) = "some but not all" (Not what yek-i does in root contexts)

Option B: Prune scalar alts → only domain exh Result: ∃x. P(x) ∧ ¬[only a] ∧ ¬[only b] ∧... For |D| ≥ 2: ∃!x. P(x) = "exactly one satisfies P" This IS what yek-i does!

def NeoGricean.Exhaustivity.EFCI.partialExhDomainOnly {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (P : Entity → Prop' World) : Prop' World

Partial exhaustification with pruned scalar alternatives. Only domain alternatives are exhaustified.

Equations

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

def NeoGricean.Exhaustivity.EFCI.partialExhScalarOnly {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (P : Entity → Prop' World) : Prop' World

Partial exhaustification with pruned domain alternatives. Only scalar alternatives are exhaustified.

Equations

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

inductive NeoGricean.Exhaustivity.EFCI.EFCIRescue : Type

EFCI types based on available rescue mechanisms.

• none : EFCIRescue

  No rescue available (vreun): ungrammatical in UE root

• modalInsertion : EFCIRescue

  Modal insertion available (irgendein): epistemic reading in root

• partialExh : EFCIRescue

  Partial exhaustification available (yek-i): uniqueness in root

• both : EFCIRescue

  Both mechanisms available

instance NeoGricean.Exhaustivity.EFCI.instDecidableEqEFCIRescue : DecidableEq EFCIRescue

Equations

• NeoGricean.Exhaustivity.EFCI.instDecidableEqEFCIRescue x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def NeoGricean.Exhaustivity.EFCI.instBEqEFCIRescue.beq : EFCIRescue → EFCIRescue → Bool

Equations

• NeoGricean.Exhaustivity.EFCI.instBEqEFCIRescue.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance NeoGricean.Exhaustivity.EFCI.instBEqEFCIRescue : BEq EFCIRescue

Equations

• NeoGricean.Exhaustivity.EFCI.instBEqEFCIRescue = { beq := NeoGricean.Exhaustivity.EFCI.instBEqEFCIRescue.beq }

def NeoGricean.Exhaustivity.EFCI.instReprEFCIRescue.repr : EFCIRescue → ℕ → Std.Format

Equations

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

instance NeoGricean.Exhaustivity.EFCI.instReprEFCIRescue : Repr EFCIRescue

Equations

• NeoGricean.Exhaustivity.EFCI.instReprEFCIRescue = { reprPrec := NeoGricean.Exhaustivity.EFCI.instReprEFCIRescue.repr }

def NeoGricean.Exhaustivity.EFCI.rootBehavior : EFCIRescue → String

EFCI type determines root context behavior.

Equations

• NeoGricean.Exhaustivity.EFCI.rootBehavior NeoGricean.Exhaustivity.EFCI.EFCIRescue.none = "Ungrammatical (no rescue)"
• NeoGricean.Exhaustivity.EFCI.rootBehavior NeoGricean.Exhaustivity.EFCI.EFCIRescue.modalInsertion = "Epistemic modal reading (speaker ignorance)"
• NeoGricean.Exhaustivity.EFCI.rootBehavior NeoGricean.Exhaustivity.EFCI.EFCIRescue.partialExh = "Uniqueness reading (exactly one)"
• NeoGricean.Exhaustivity.EFCI.rootBehavior NeoGricean.Exhaustivity.EFCI.EFCIRescue.both = "Either epistemic or uniqueness (context determines)"

def NeoGricean.Exhaustivity.EFCI.vreunType : EFCIRescue

EFCI type for vreun (Romanian).

Equations

• NeoGricean.Exhaustivity.EFCI.vreunType = NeoGricean.Exhaustivity.EFCI.EFCIRescue.none

def NeoGricean.Exhaustivity.EFCI.irgendeinType : EFCIRescue

EFCI type for irgendein (German). Actually allows both mechanisms, but modal insertion is primary in root.

Equations

• NeoGricean.Exhaustivity.EFCI.irgendeinType = NeoGricean.Exhaustivity.EFCI.EFCIRescue.both

def NeoGricean.Exhaustivity.EFCI.yekiType : EFCIRescue

EFCI type for yek-i (Farsi). Only partial exhaustification available.

Equations

• NeoGricean.Exhaustivity.EFCI.yekiType = NeoGricean.Exhaustivity.EFCI.EFCIRescue.partialExh

Modal Contexts

Under deontic modals (permission), yek-i yields free choice: ◇_deo[∃x. P(x)] with domain exh = ◇_deo[P(a) ∧ ¬P(b)] ∨ ◇_deo[P(b) ∧ ¬P(a)] (simplified) = For each x, ◇_deo[P(x)]

Under epistemic modals, yek-i yields modal variation: ◇_epi[∃x. P(x)] with domain exh = At least two individuals are epistemically possible

inductive NeoGricean.Exhaustivity.EFCI.ModalFlavor : Type

Modal flavor type.

• deontic : ModalFlavor
• epistemic : ModalFlavor

instance NeoGricean.Exhaustivity.EFCI.instDecidableEqModalFlavor : DecidableEq ModalFlavor

Equations

• NeoGricean.Exhaustivity.EFCI.instDecidableEqModalFlavor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def NeoGricean.Exhaustivity.EFCI.instBEqModalFlavor.beq : ModalFlavor → ModalFlavor → Bool

Equations

• NeoGricean.Exhaustivity.EFCI.instBEqModalFlavor.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance NeoGricean.Exhaustivity.EFCI.instBEqModalFlavor : BEq ModalFlavor

Equations

• NeoGricean.Exhaustivity.EFCI.instBEqModalFlavor = { beq := NeoGricean.Exhaustivity.EFCI.instBEqModalFlavor.beq }

instance NeoGricean.Exhaustivity.EFCI.instReprModalFlavor : Repr ModalFlavor

Equations

• NeoGricean.Exhaustivity.EFCI.instReprModalFlavor = { reprPrec := NeoGricean.Exhaustivity.EFCI.instReprModalFlavor.repr }

def NeoGricean.Exhaustivity.EFCI.instReprModalFlavor.repr : ModalFlavor → ℕ → Std.Format

Equations

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

inductive NeoGricean.Exhaustivity.EFCI.EFCIReading : Type

EFCI reading type under different conditions.

• plainExistential : EFCIReading

  Plain existential (DE contexts)

• uniqueness : EFCIReading

  Uniqueness (root, partial exh)

• freeChoice : EFCIReading

  Free choice (deontic modal)

• modalVariation : EFCIReading

  Modal variation (epistemic modal)

• epistemicIgnorance : EFCIReading

  Epistemic ignorance (modal insertion)

instance NeoGricean.Exhaustivity.EFCI.instDecidableEqEFCIReading : DecidableEq EFCIReading

Equations

• NeoGricean.Exhaustivity.EFCI.instDecidableEqEFCIReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance NeoGricean.Exhaustivity.EFCI.instBEqEFCIReading : BEq EFCIReading

Equations

• NeoGricean.Exhaustivity.EFCI.instBEqEFCIReading = { beq := NeoGricean.Exhaustivity.EFCI.instBEqEFCIReading.beq }

def NeoGricean.Exhaustivity.EFCI.instBEqEFCIReading.beq : EFCIReading → EFCIReading → Bool

Equations

• NeoGricean.Exhaustivity.EFCI.instBEqEFCIReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance NeoGricean.Exhaustivity.EFCI.instReprEFCIReading : Repr EFCIReading

Equations

• NeoGricean.Exhaustivity.EFCI.instReprEFCIReading = { reprPrec := NeoGricean.Exhaustivity.EFCI.instReprEFCIReading.repr }

def NeoGricean.Exhaustivity.EFCI.instReprEFCIReading.repr : EFCIReading → ℕ → Std.Format

Equations

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

def NeoGricean.Exhaustivity.EFCI.efciReading (rescue : EFCIRescue) (isDE : Bool) (modal : Option ModalFlavor) : Option EFCIReading

Determine EFCI reading based on context and rescue mechanism.

Equations

• One or more equations did not get rendered due to their size.
• NeoGricean.Exhaustivity.EFCI.efciReading NeoGricean.Exhaustivity.EFCI.EFCIRescue.none isDE none = if isDE = true then some NeoGricean.Exhaustivity.EFCI.EFCIReading.plainExistential else none

Theoretical Predictions

1. Root context prediction: yek-i → uniqueness, irgendein → epistemic
2. Deontic prediction: Both → free choice
3. Epistemic prediction: Both → modal variation
4. DE prediction: Both → plain existential

theorem NeoGricean.Exhaustivity.EFCI.yeki_root_uniqueness : efciReading yekiType false none = some EFCIReading.uniqueness

Yek-i in root yields uniqueness

theorem NeoGricean.Exhaustivity.EFCI.irgendein_root_uniqueness : efciReading irgendeinType false none = some EFCIReading.uniqueness

Irgendein in root can yield uniqueness (with partial exh rescue)

theorem NeoGricean.Exhaustivity.EFCI.deontic_freeChoice (rescue : EFCIRescue) : efciReading rescue false (some ModalFlavor.deontic) = some EFCIReading.freeChoice

Under deontic modal: free choice

theorem NeoGricean.Exhaustivity.EFCI.epistemic_modalVariation (rescue : EFCIRescue) : efciReading rescue false (some ModalFlavor.epistemic) = some EFCIReading.modalVariation

Under epistemic modal: modal variation

theorem NeoGricean.Exhaustivity.EFCI.de_plainExistential (rescue : EFCIRescue) (modal : Option ModalFlavor) : efciReading rescue true modal = some EFCIReading.plainExistential

In DE context: plain existential

Universal Free Choice Items

Universal FCIs like English "any" and Italian "qualunque" contrast with existential FCIs like German "irgendein" and Farsi "yek-i":

FCI Type	Base Force	Examples	Morphological Hints
Existential	∃	irgendein, yek-i, vreun	Often contains "one"
Universal	∀	any, qualunque, whatever	Often wh-based

Chierchia's analysis

Both FCI types have the same underlying existential semantics. The universal force of "any" emerges from obligatory exhaustification of domain alternatives.

• "any" = ∃ + obligatory domain alternatives (always active)
• "some" = ∃ + optional domain alternatives (relevance-gated)

The "any" Distribution

1. NPI use (DE contexts): "I didn't see any students"

   • In DE, exhaustification is vacuous (domain alts are entailed)
   • Result: plain existential reading

2. FC use (modal contexts): "You may read any book"

   • Under modal, domain alts yield free choice
   • Result: universal-like permission

3. Generic use: "Any owl hunts mice" (subtrigging)

   • Generic contexts license FC reading
   • Result: universal generalization

Why "any" Fails in Positive Episodic Contexts

"*There are any cookies"

Exhaustifying domain alternatives in UE episodic contexts yields contradiction:

• ∃d∈D. P(d) (assertion)
• ∀d∈D. ¬[P(d) ∧ ∀y≠d.¬P(y)] (domain alt negation)

With two witnesses d₁, d₂: the second clause requires that for any d satisfying P, some other y also satisfies P. Combined with the first clause, this leads to infinite regress/contradiction for finite domains.

Contrast with "some"

"Some" has the same alternatives as "any", but they are optional. When not activated (low relevance), "some" = plain existential. "Any" must activate alternatives, hence the restricted distribution.

inductive NeoGricean.Exhaustivity.EFCI.FCIFlavor : Type

FCI flavor: existential vs universal force.

Note: "Universal" FCIs have existential base meaning but universal surface force due to obligatory exhaustification.

• existential : FCIFlavor
• universal : FCIFlavor

instance NeoGricean.Exhaustivity.EFCI.instDecidableEqFCIFlavor : DecidableEq FCIFlavor

Equations

• NeoGricean.Exhaustivity.EFCI.instDecidableEqFCIFlavor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def NeoGricean.Exhaustivity.EFCI.instBEqFCIFlavor.beq : FCIFlavor → FCIFlavor → Bool

Equations

• NeoGricean.Exhaustivity.EFCI.instBEqFCIFlavor.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance NeoGricean.Exhaustivity.EFCI.instBEqFCIFlavor : BEq FCIFlavor

Equations

• NeoGricean.Exhaustivity.EFCI.instBEqFCIFlavor = { beq := NeoGricean.Exhaustivity.EFCI.instBEqFCIFlavor.beq }

instance NeoGricean.Exhaustivity.EFCI.instReprFCIFlavor : Repr FCIFlavor

Equations

• NeoGricean.Exhaustivity.EFCI.instReprFCIFlavor = { reprPrec := NeoGricean.Exhaustivity.EFCI.instReprFCIFlavor.repr }

def NeoGricean.Exhaustivity.EFCI.instReprFCIFlavor.repr : FCIFlavor → ℕ → Std.Format

Equations

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

structure NeoGricean.Exhaustivity.EFCI.UniversalFCI : Type

Universal FCI: existential with obligatorily active domain alternatives.

• baseIsExistential : Bool

  Base meaning is existential

• obligatoryDomainAlts : Bool

  Domain alternatives are always active (not relevance-gated)

• modalRescue : Bool

  Can be rescued via modal insertion

• genericRescue : Bool

  Can be rescued via generic/subtrigging

def NeoGricean.Exhaustivity.EFCI.any_FCI : UniversalFCI

English "any" as a Universal FCI

Equations

• NeoGricean.Exhaustivity.EFCI.any_FCI = { }

def NeoGricean.Exhaustivity.EFCI.qualunque_FCI : UniversalFCI

Italian "qualunque" as a Universal FCI

Equations

• NeoGricean.Exhaustivity.EFCI.qualunque_FCI = { }

inductive NeoGricean.Exhaustivity.EFCI.UFCIContext : Type

Context type for determining Universal FCI distribution.

• positiveEpisodic : UFCIContext
• negation : UFCIContext
• conditional_ant : UFCIContext
• deonticModal : UFCIContext
• epistemicModal : UFCIContext
• generic : UFCIContext
• question : UFCIContext

instance NeoGricean.Exhaustivity.EFCI.instDecidableEqUFCIContext : DecidableEq UFCIContext

Equations

• NeoGricean.Exhaustivity.EFCI.instDecidableEqUFCIContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def NeoGricean.Exhaustivity.EFCI.instBEqUFCIContext.beq : UFCIContext → UFCIContext → Bool

Equations

• NeoGricean.Exhaustivity.EFCI.instBEqUFCIContext.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance NeoGricean.Exhaustivity.EFCI.instBEqUFCIContext : BEq UFCIContext

Equations

• NeoGricean.Exhaustivity.EFCI.instBEqUFCIContext = { beq := NeoGricean.Exhaustivity.EFCI.instBEqUFCIContext.beq }

def NeoGricean.Exhaustivity.EFCI.instReprUFCIContext.repr : UFCIContext → ℕ → Std.Format

Equations

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

instance NeoGricean.Exhaustivity.EFCI.instReprUFCIContext : Repr UFCIContext

Equations

• NeoGricean.Exhaustivity.EFCI.instReprUFCIContext = { reprPrec := NeoGricean.Exhaustivity.EFCI.instReprUFCIContext.repr }

def NeoGricean.Exhaustivity.EFCI.ufciGrammatical (ctx : UFCIContext) : Bool

Universal FCI grammaticality prediction.

Ungrammatical only in positive episodic (UE without rescue).

Equations

• NeoGricean.Exhaustivity.EFCI.ufciGrammatical NeoGricean.Exhaustivity.EFCI.UFCIContext.positiveEpisodic = false
• NeoGricean.Exhaustivity.EFCI.ufciGrammatical NeoGricean.Exhaustivity.EFCI.UFCIContext.negation = true
• NeoGricean.Exhaustivity.EFCI.ufciGrammatical NeoGricean.Exhaustivity.EFCI.UFCIContext.conditional_ant = true
• NeoGricean.Exhaustivity.EFCI.ufciGrammatical NeoGricean.Exhaustivity.EFCI.UFCIContext.deonticModal = true
• NeoGricean.Exhaustivity.EFCI.ufciGrammatical NeoGricean.Exhaustivity.EFCI.UFCIContext.epistemicModal = true
• NeoGricean.Exhaustivity.EFCI.ufciGrammatical NeoGricean.Exhaustivity.EFCI.UFCIContext.generic = true
• NeoGricean.Exhaustivity.EFCI.ufciGrammatical NeoGricean.Exhaustivity.EFCI.UFCIContext.question = true

def NeoGricean.Exhaustivity.EFCI.ufciReading (ctx : UFCIContext) : Option EFCIReading

Reading obtained by Universal FCI in context.

Equations

• NeoGricean.Exhaustivity.EFCI.ufciReading NeoGricean.Exhaustivity.EFCI.UFCIContext.positiveEpisodic = none
• NeoGricean.Exhaustivity.EFCI.ufciReading NeoGricean.Exhaustivity.EFCI.UFCIContext.negation = some NeoGricean.Exhaustivity.EFCI.EFCIReading.plainExistential
• NeoGricean.Exhaustivity.EFCI.ufciReading NeoGricean.Exhaustivity.EFCI.UFCIContext.conditional_ant = some NeoGricean.Exhaustivity.EFCI.EFCIReading.plainExistential
• NeoGricean.Exhaustivity.EFCI.ufciReading NeoGricean.Exhaustivity.EFCI.UFCIContext.deonticModal = some NeoGricean.Exhaustivity.EFCI.EFCIReading.freeChoice
• NeoGricean.Exhaustivity.EFCI.ufciReading NeoGricean.Exhaustivity.EFCI.UFCIContext.epistemicModal = some NeoGricean.Exhaustivity.EFCI.EFCIReading.freeChoice
• NeoGricean.Exhaustivity.EFCI.ufciReading NeoGricean.Exhaustivity.EFCI.UFCIContext.generic = some NeoGricean.Exhaustivity.EFCI.EFCIReading.freeChoice
• NeoGricean.Exhaustivity.EFCI.ufciReading NeoGricean.Exhaustivity.EFCI.UFCIContext.question = some NeoGricean.Exhaustivity.EFCI.EFCIReading.plainExistential

theorem NeoGricean.Exhaustivity.EFCI.any_in_de_is_existential : ufciReading UFCIContext.negation = some EFCIReading.plainExistential

In DE contexts, exhaustifying "any"'s alternatives yields entailments, so the exhaustification is vacuous and "any" = plain existential.

This explains the NPI distribution of "any".

theorem NeoGricean.Exhaustivity.EFCI.any_negation_plain : ufciReading UFCIContext.negation = some EFCIReading.plainExistential

"I didn't see any students" ≡ "I didn't see a student"

The "any" contributes no special meaning in DE contexts.

theorem NeoGricean.Exhaustivity.EFCI.any_modal_fc : ufciReading UFCIContext.deonticModal = some EFCIReading.freeChoice

Under modals, "any" yields free choice via exhaustification.

"You may read any book" = For each book x, you may read x

theorem NeoGricean.Exhaustivity.EFCI.any_rescued_by_modal : ufciGrammatical UFCIContext.deonticModal = true

Modal insertion is the rescue mechanism for Universal FCIs.

theorem NeoGricean.Exhaustivity.EFCI.any_positive_episodic_bad : ufciGrammatical UFCIContext.positiveEpisodic = false

"*There are any cookies" is ungrammatical.

Domain alternative exhaustification in UE episodic context yields contradiction.

theorem NeoGricean.Exhaustivity.EFCI.any_positive_contradiction : ufciReading UFCIContext.positiveEpisodic = none

The failure mechanism: exhaustification is G-contradictory. (See Core.Analyticity for G-triviality/L-analyticity)

Summary: Existential vs Universal FCIs

Property	Existential (irgendein)	Universal (any)
Base meaning	∃	∃
Domain alts	Relevance-gated	Obligatory
Root reading	Epistemic/Uniqueness	*(blocked)
Modal reading	Free choice	Free choice
DE reading	Plain ∃	Plain ∃ (NPI)

The key difference is whether domain alternatives are optional or obligatory. This single parameter derives the entire distribution difference.

theorem NeoGricean.Exhaustivity.EFCI.efci_allows_root : efciReading EFCIRescue.modalInsertion false none = some EFCIReading.epistemicIgnorance

Existential FCIs allow root readings

theorem NeoGricean.Exhaustivity.EFCI.ufci_blocks_root : ufciGrammatical UFCIContext.positiveEpisodic = false

Universal FCIs block root readings

theorem NeoGricean.Exhaustivity.EFCI.efci_ufci_fc_under_modal : efciReading EFCIRescue.modalInsertion false (some ModalFlavor.deontic) = some EFCIReading.freeChoice ∧ ufciReading UFCIContext.deonticModal = some EFCIReading.freeChoice

Both FCIs get FC under modals

structure NeoGricean.Exhaustivity.EFCI.AnyExample : Type

An "any" distribution example.

• sentence : String
• context : UFCIContext
• grammatical : Bool
• reading : Option String
• notes : String

instance NeoGricean.Exhaustivity.EFCI.instReprAnyExample : Repr AnyExample

Equations

• NeoGricean.Exhaustivity.EFCI.instReprAnyExample = { reprPrec := NeoGricean.Exhaustivity.EFCI.instReprAnyExample.repr }

def NeoGricean.Exhaustivity.EFCI.instReprAnyExample.repr : AnyExample → ℕ → Std.Format

Equations

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

def NeoGricean.Exhaustivity.EFCI.any_positive_bad : AnyExample

Equations

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

def NeoGricean.Exhaustivity.EFCI.any_negation_ok : AnyExample

Equations

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

def NeoGricean.Exhaustivity.EFCI.any_deontic_ok : AnyExample

Equations

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

def NeoGricean.Exhaustivity.EFCI.any_generic_ok : AnyExample

Equations

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

def NeoGricean.Exhaustivity.EFCI.any_question_ok : AnyExample

Equations

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

def NeoGricean.Exhaustivity.EFCI.any_conditional_ok : AnyExample

Equations

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

def NeoGricean.Exhaustivity.EFCI.anyExamples : List AnyExample

Equations

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