theorem NeoGricean.Exhaustivity.EFCIClosure.scalar_alts_structure {World : Type u_1} {Entity : Type u_2} (D : EFCI.Domain Entity) (P : Entity → Prop' World) : EFCI.universalAlt D P = fun (w : World) => ∀ d ∈ D, P d w

The prejacent and scalar alternative set is "almost closed" under conjunction. The universal is the conjunction of all singleton assertions.

theorem NeoGricean.Exhaustivity.EFCIClosure.preExh_pairwise_inconsistent {World : Type u_1} {Entity : Type u_2} (D : EFCI.Domain Entity) (d₁ d₂ : Entity) (P : Entity → Prop' World) (_hd₁ : d₁ ∈ D) (hd₂ : d₂ ∈ D) (hne : d₁ ≠ d₂) (w : World) : ¬(EFCI.preExhaustify D d₁ P w ∧ EFCI.preExhaustify D d₂ P w)

Pre-exhaustified domain alternatives are pairwise inconsistent. For distinct d₁, d₂ ∈ D: preExh(d₁) ∧ preExh(d₂) = ⊥

You can't have "exactly d₁ satisfies P" AND "exactly d₂ satisfies P".

theorem NeoGricean.Exhaustivity.EFCIClosure.preExh_all_inconsistent {World : Type u_1} {Entity : Type u_2} (D : EFCI.Domain Entity) (P : Entity → Prop' World) (d₁ d₂ : Entity) (hd₁ : d₁ ∈ D) (hd₂ : d₂ ∈ D) (hne : d₁ ≠ d₂) (w : World) : ¬∀ φ ∈ EFCI.preExhDomainAlts D P, φ w

The conjunction of ALL pre-exhaustified domain alternatives is ⊥ (when |D| ≥ 2).

theorem NeoGricean.Exhaustivity.EFCIClosure.efci_not_closed_witness {World : Type u_1} {Entity : Type u_2} (D : EFCI.Domain Entity) (P : Entity → Prop' World) (d₁ d₂ : Entity) (hd₁ : d₁ ∈ D) (hd₂ : d₂ ∈ D) (hne : d₁ ≠ d₂) : have X := {EFCI.preExhaustify D d₁ P, EFCI.preExhaustify D d₂ P}; X ⊆ EFCI.efciAlternatives D P ∧ ∀ (w : World), ¬⋀ X w

The EFCI alternative set fails closure under conjunction when |D| ≥ 2. The witness: {preExh(d₁), preExh(d₂)} ⊆ ALT but ⋀{preExh(d₁), preExh(d₂)} = ⊥.

Connection to Spector's Theorem 9

Spector's main result: When ALT is closed under conjunction, exh_mw ≡ exh_ie.

For EFCI:

1. The full alternative set is not closed (theorem above)
2. Therefore Theorem 9 doesn't directly apply
3. Rescue mechanisms (modal insertion, partial exhaustification) can be understood as restoring consistency by pruning the alternative set

theorem NeoGricean.Exhaustivity.EFCIClosure.scalar_only_contains_universal {World : Type u_1} {Entity : Type u_2} (D : EFCI.Domain Entity) (P : Entity → Prop' World) : EFCI.universalAlt D P ∈ EFCI.scalarOnlyAlts D P

Pruning to scalar-only alternatives may restore closure properties. The universal is in the scalar alt set.

theorem NeoGricean.Exhaustivity.EFCIClosure.domain_only_still_not_closed {World : Type u_1} {Entity : Type u_2} (D : EFCI.Domain Entity) (P : Entity → Prop' World) (d₁ d₂ : Entity) (hd₁ : d₁ ∈ D) (hd₂ : d₂ ∈ D) (hne : d₁ ≠ d₂) : have X := {EFCI.preExhaustify D d₁ P, EFCI.preExhaustify D d₂ P}; X ⊆ EFCI.domainOnlyAlts D P ∧ ∀ (w : World), ¬⋀ X w

Domain-only alternatives (scalar pruned) still have the inconsistency. But under innocent exclusion, not all can be negated together.

The Root of the EFCI Explanation

The deep explanation for EFCI behavior has three parts:

1. Why Full Exhaustification Causes Contradiction

Pre-exhaustified domain alternatives are mutually exclusive:

• preExh(d) = "d is the unique satisfier"
• Two things can't both be the unique satisfier
• So ⋀_d preExh(d) = ⊥ for |D| ≥ 2

When we add scalar negation (¬∀), we get XOR. XOR combined with the equivalence from domain negations yields ⊥.

2. Why Rescue Mechanisms Work

Modal insertion (irgendein):

• Insert ◇ above the existential
• Now ◇[preExh(d₁)] and ◇[preExh(d₂)] are compatible
• "Possibly only d₁, possibly only d₂" is consistent
• Result: Modal variation (at least two possibilities)

Partial exhaustification (yek-i):

• Prune scalar alternatives → only domain alternatives remain
• Under innocent exclusion: can't negate all domain alts
• (Negating preExh(d) for ALL d makes the prejacent false)
• Result: No negations added; uniqueness via pragmatic reasoning

3. Why Uniqueness Emerges in Root Contexts

For yek-i in root (no modal):

• Partial exh with domain-only yields: ∃x. P(x) (no negations)
• But the ALTERNATIVE SET still includes preExh(d) for each d
• Pragmatic reasoning: "Why did the speaker use yek-i (activating domain alternatives) if not to convey that exactly one satisfies P?"
• This is a secondary pragmatic inference, not from exhaustification

Summary

The root explanation is mutual exclusivity of pre-exhaustified alternatives:

1. Full exhaustification → contradiction (because preExh alts conflict)
2. Modal insertion → compatibility under possibility
3. Partial exhaustification → no negations (IE can't negate consistently)
4. Uniqueness → pragmatic reasoning about alternative activation

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

The negation of a pre-exhaustified alternative. ¬preExh(d) = "d is not the unique satisfier" = "either ¬P(d) or ∃y≠d. P(y)"

Equations

• NeoGricean.Exhaustivity.EFCIClosure.notPreExh D d P w = ¬NeoGricean.Exhaustivity.EFCI.preExhaustify D d P w

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

The conjunction of negated pre-exhaustified alternatives. This says "NO element is the unique satisfier" = "either none or ≥2 satisfy P".

Equations

• NeoGricean.Exhaustivity.EFCIClosure.allNotPreExh D P w = ∀ d ∈ D, NeoGricean.Exhaustivity.EFCIClosure.notPreExh D d P w

theorem NeoGricean.Exhaustivity.EFCIClosure.unique_witness_falsifies_allNotPreExh {World : Type u_1} {Entity : Type u_2} (D : EFCI.Domain Entity) (P : Entity → Prop' World) (d₀ : Entity) (hd₀ : d₀ ∈ D) (hPd₀ : ∀ (w : World), P d₀ w) (hunique : ∀ (w : World), ∀ d ∈ D, d ≠ d₀ → ¬P d w) (w : World) : ¬allNotPreExh D P w

allNotPreExh is false when exactly one element satisfies P.

If exactly d₀ satisfies P, then preExh(d₀) is TRUE (d₀ is unique), so notPreExh(d₀) is FALSE, so allNotPreExh is FALSE.

This is why innocent exclusion can't negate ALL domain alternatives while keeping the prejacent (∃x. P(x)) true with a unique witness.