inductive AlonsoOvalleMoghiseh2025.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

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025.instDecidableEqAlternativeType : DecidableEq AlternativeType

Equations

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

def AlonsoOvalleMoghiseh2025.instReprAlternativeType.repr : AlternativeType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025.instReprAlternativeType : Repr AlternativeType

Equations

• AlonsoOvalleMoghiseh2025.instReprAlternativeType = { reprPrec := AlonsoOvalleMoghiseh2025.instReprAlternativeType.repr }

structure AlonsoOvalleMoghiseh2025.EFCIAlternative (World : Type u_1) : Type u_1

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

• content : Set 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 AlonsoOvalleMoghiseh2025.Domain (Entity : Type u_3) : Type u_3

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

Equations

• AlonsoOvalleMoghiseh2025.Domain Entity = Set Entity

def AlonsoOvalleMoghiseh2025.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

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

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

• AlonsoOvalleMoghiseh2025.existsInDomain D P w = ∃ d ∈ D, P d w

def AlonsoOvalleMoghiseh2025.singletonAlt {World : Type u_1} {Entity : Type u_2} (d : Entity) (P : Entity → Set World) : Set World

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

Equations

• AlonsoOvalleMoghiseh2025.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 AlonsoOvalleMoghiseh2025.preExhaustify {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (d : Entity) (P : Entity → Set World) : Set 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

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

def AlonsoOvalleMoghiseh2025.preExhDomainAlts {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (P : Entity → Set World) : Set (Set World)

The set of pre-exhaustified domain alternatives.

Equations

• AlonsoOvalleMoghiseh2025.preExhDomainAlts D P = {φ : Set World | ∃ d ∈ D, φ = AlonsoOvalleMoghiseh2025.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 AlonsoOvalleMoghiseh2025.universalAlt {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (P : Entity → Set World) : Set World

The universal (scalar) alternative to an existential.

Equations

• AlonsoOvalleMoghiseh2025.universalAlt D P w = ∀ d ∈ D, P d w

def AlonsoOvalleMoghiseh2025.scalarAlts {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (P : Entity → Set World) : Set (Set World)

The scalar alternative set for an existential.

Equations

• AlonsoOvalleMoghiseh2025.scalarAlts D P = {AlonsoOvalleMoghiseh2025.universalAlt D P}

def AlonsoOvalleMoghiseh2025.efciAlternatives {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (P : Entity → Set World) : Set (Set World)

The full EFCI alternative set combines:

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

Equations

• AlonsoOvalleMoghiseh2025.efciAlternatives D P = {AlonsoOvalleMoghiseh2025.existsInDomain D P} ∪ AlonsoOvalleMoghiseh2025.scalarAlts D P ∪ AlonsoOvalleMoghiseh2025.preExhDomainAlts D P

def AlonsoOvalleMoghiseh2025.scalarOnlyAlts {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (P : Entity → Set World) : Set (Set World)

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

Equations

• AlonsoOvalleMoghiseh2025.scalarOnlyAlts D P = {AlonsoOvalleMoghiseh2025.existsInDomain D P} ∪ AlonsoOvalleMoghiseh2025.scalarAlts D P

def AlonsoOvalleMoghiseh2025.domainOnlyAlts {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (P : Entity → Set World) : Set (Set World)

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

Equations

• AlonsoOvalleMoghiseh2025.domainOnlyAlts D P = {AlonsoOvalleMoghiseh2025.existsInDomain D P} ∪ AlonsoOvalleMoghiseh2025.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 AlonsoOvalleMoghiseh2025.simpleExh {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) : Set World

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

Equations

• AlonsoOvalleMoghiseh2025.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 AlonsoOvalleMoghiseh2025.isContradictory {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) : Prop

Check if an alternative set leads to contradiction when exhaustified.

Equations

• AlonsoOvalleMoghiseh2025.isContradictory ALT φ = ∀ (w : World), ¬AlonsoOvalleMoghiseh2025.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 AlonsoOvalleMoghiseh2025.covertEpi {World : Type u_1} (φ : Set World) : Set World

Covert epistemic modal (possibility).

Equations

• AlonsoOvalleMoghiseh2025.covertEpi φ x✝ = ∃ (w : World), φ w

def AlonsoOvalleMoghiseh2025.withModalInsertion {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (P : Entity → Set World) : Set World

Modal insertion: wrap existential in covert epistemic.

Equations

• AlonsoOvalleMoghiseh2025.withModalInsertion D P = AlonsoOvalleMoghiseh2025.covertEpi (AlonsoOvalleMoghiseh2025.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 AlonsoOvalleMoghiseh2025.partialExhDomainOnly {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (P : Entity → Set World) : Set World

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

Equations

• AlonsoOvalleMoghiseh2025.partialExhDomainOnly D P = AlonsoOvalleMoghiseh2025.simpleExh (AlonsoOvalleMoghiseh2025.domainOnlyAlts D P) (AlonsoOvalleMoghiseh2025.existsInDomain D P)

def AlonsoOvalleMoghiseh2025.partialExhScalarOnly {World : Type u_1} {Entity : Type u_2} (D : Domain Entity) (P : Entity → Set World) : Set World

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

Equations

• AlonsoOvalleMoghiseh2025.partialExhScalarOnly D P = AlonsoOvalleMoghiseh2025.simpleExh (AlonsoOvalleMoghiseh2025.scalarOnlyAlts D P) (AlonsoOvalleMoghiseh2025.existsInDomain D P)

inductive AlonsoOvalleMoghiseh2025.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

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025.instDecidableEqEFCIRescue : DecidableEq EFCIRescue

Equations

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

def AlonsoOvalleMoghiseh2025.instReprEFCIRescue.repr : EFCIRescue → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025.instReprEFCIRescue : Repr EFCIRescue

Equations

• AlonsoOvalleMoghiseh2025.instReprEFCIRescue = { reprPrec := AlonsoOvalleMoghiseh2025.instReprEFCIRescue.repr }

def AlonsoOvalleMoghiseh2025.rootBehavior : EFCIRescue → String

EFCI type determines root context behavior.

Equations

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

def AlonsoOvalleMoghiseh2025.vreunType : EFCIRescue

EFCI type for vreun (Romanian).

Equations

• AlonsoOvalleMoghiseh2025.vreunType = AlonsoOvalleMoghiseh2025.EFCIRescue.none

def AlonsoOvalleMoghiseh2025.irgendeinType : EFCIRescue

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

Equations

• AlonsoOvalleMoghiseh2025.irgendeinType = AlonsoOvalleMoghiseh2025.EFCIRescue.both

def AlonsoOvalleMoghiseh2025.yekiType : EFCIRescue

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

Equations

• AlonsoOvalleMoghiseh2025.yekiType = AlonsoOvalleMoghiseh2025.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 AlonsoOvalleMoghiseh2025.ModalFlavor : Type

Modal flavor type.

• deontic : ModalFlavor
• epistemic : ModalFlavor

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025.instDecidableEqModalFlavor : DecidableEq ModalFlavor

Equations

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

def AlonsoOvalleMoghiseh2025.instReprModalFlavor.repr : ModalFlavor → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025.instReprModalFlavor : Repr ModalFlavor

Equations

• AlonsoOvalleMoghiseh2025.instReprModalFlavor = { reprPrec := AlonsoOvalleMoghiseh2025.instReprModalFlavor.repr }

inductive AlonsoOvalleMoghiseh2025.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)

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025.instDecidableEqEFCIReading : DecidableEq EFCIReading

Equations

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

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025.instReprEFCIReading : Repr EFCIReading

Equations

• AlonsoOvalleMoghiseh2025.instReprEFCIReading = { reprPrec := AlonsoOvalleMoghiseh2025.instReprEFCIReading.repr }

def AlonsoOvalleMoghiseh2025.instReprEFCIReading.repr : EFCIReading → ℕ → Std.Format

Equations

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

def AlonsoOvalleMoghiseh2025.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.
• AlonsoOvalleMoghiseh2025.efciReading AlonsoOvalleMoghiseh2025.EFCIRescue.none isDE none = if isDE = true then some AlonsoOvalleMoghiseh2025.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 AlonsoOvalleMoghiseh2025.yeki_root_uniqueness : efciReading yekiType false none = some EFCIReading.uniqueness

Yek-i in root yields uniqueness

theorem AlonsoOvalleMoghiseh2025.irgendein_root_uniqueness : efciReading irgendeinType false none = some EFCIReading.uniqueness

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

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

Under deontic modal: free choice

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

Under epistemic modal: modal variation

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

In DE context: plain existential

Cross-FCI Comparison

The Universal FCIs (English any, Italian qualunque) and their characteristic distribution are formalized in Phenomena/Polarity/Studies/Chierchia2013.lean (Section "Universal Free Choice Items"). The contrast theorems below pair the existential-FCI behaviour modeled here with the universal-FCI behaviour modeled there.

inductive AlonsoOvalleMoghiseh2025.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

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025.instDecidableEqFCIFlavor : DecidableEq FCIFlavor

Equations

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

def AlonsoOvalleMoghiseh2025.instReprFCIFlavor.repr : FCIFlavor → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025.instReprFCIFlavor : Repr FCIFlavor

Equations

• AlonsoOvalleMoghiseh2025.instReprFCIFlavor = { reprPrec := AlonsoOvalleMoghiseh2025.instReprFCIFlavor.repr }

theorem AlonsoOvalleMoghiseh2025.efci_allows_root : efciReading EFCIRescue.modalInsertion false none = some EFCIReading.epistemicIgnorance

Existential FCIs allow root readings

theorem AlonsoOvalleMoghiseh2025.ufci_blocks_root : Phenomena.Polarity.Studies.Chierchia2013.ufciGrammatical Phenomena.Polarity.Studies.Chierchia2013.UFCIContext.positiveEpisodic = false

Universal FCIs block root readings (defined in Chierchia2013)

theorem AlonsoOvalleMoghiseh2025.efci_ufci_fc_under_modal : efciReading EFCIRescue.modalInsertion false (some ModalFlavor.deontic) = some EFCIReading.freeChoice ∧ Phenomena.Polarity.Studies.Chierchia2013.ufciReading Phenomena.Polarity.Studies.Chierchia2013.UFCIContext.deonticModal = some Phenomena.Polarity.Studies.Chierchia2013.UFCIReading.freeChoice

Both FCIs get FC under modals