Alonso-Ovalle & Moghiseh 2025: Existential Free Choice Items

[AOM25a]

Existential free choice items: The case of Farsi yek-i DPs. Semantics & Pragmatics 18, Article 4.

Farsi yek-i DPs pattern with other EFCIs in DE and modal contexts but are grammatical, modality-free, and uniqueness-conveying in root contexts. The paper derives this profile from split exhaustification: scalar and domain alternatives are targeted by independent operators, with scalar exhaustification clause-bounded below the modal.

Main declarations

Computational verification (decide-checked on finite world types)

• root_full_innocent_vacuous — full IE on the 2-book root alternative set is vacuous (3 MCEs, no shared alt; IE = ∅).
• root_full_tolerant_contradiction — Chierchia's tolerant operator yields ⊥ on the same set (paper eq. 92).
• root_scalar_only_uniqueness — yek-i's partial scalar exhaustification gives uniqueness (eq. 93a).
• root_domain_only_conjunction — partial domain exhaustification gives conjunction (eq. 93b), blocked by Chierchia's Economy Principle.
• deontic_poss_split_exh — split exh under ◇ derives FC + embedded uniqueness (eq. 119).
• deontic_nec_split_exh — split exh under □ (eq. 120).
• de_scalar_exh_weakens — scalar exh inside a DE conditional strictly weakens the matrix (cf. eq. 129–135).
• single_exh_no_fc, above_only_all_alts_too_strong, two_ie_above_below_too_strong — three non-split architectures fail.

Project contributions beyond the paper (Abstract sub-namespace)

The Abstract block carries content that the paper's worked example doesn't formalize but that the structural framework supports:

• Abstract.full_exh_consistent_three — the root contradiction is specifically a |D|=2 artifact; for |D|≥3, the premises that contradict on 2-book Fin 2 are jointly satisfiable.
• Abstract.modal_split_exh_fc, Abstract.modal_split_exh_full — Kripke-frame lift of the deontic-possibility split-exh result; FC and embedded uniqueness hold over arbitrary Acc : W → Prop and Q : D → W → Prop, not just the specific PermW encoding.
• Abstract.modal_full_exh_contradiction, Abstract.modal_uniqueness_not_fc, Abstract.modal_split_compatible_with_joint, Abstract.modal_split_full_compatible_with_joint — Kripke-frame versions of the architecture-comparison results (single-vs-split exh, witness countermodels).

Table 2 typology is canonicalized in Farsi.Determiners (EFCIRescue enum, per-item yeki/irgendein_de/vreun_ro entries, per-item root-reading theorems). See the EFCI Typology section below.

Implementation notes

Two passes over the same content:

1. Concrete computation (top-level): three finite world types (PQWorld 4 worlds, PermW 8 worlds, CondW 8 worlds). Theorems close by decide over Finset substrate; the paper-equation-labelled ones derive from structural lemmas in Linglib.Semantics.Exhaustification.Structural.
2. Abstract (Abstract sub-namespace): proofs the substrate can't express — the |D|≥3 paper-scope finding (full_exh_consistent_three) and the Kripke-frame modal lifts (modal_split_exh_fc and friends). Note: paper-claim restatements at the Type level were removed during cleanup since they duplicated the substrate-derived top-level theorems on the worked 2-book example.

The computational layer uses α → Bool rather than α → Prop to enable decide on Finset coercions via the substrate's predToFinset and altsFromPreds helpers.

The 2-book root case exposes a counting subtlety: the paper's (101) lists 2 MCEs for the full alternative set, but there are actually 3 ({b₁∧b₂, b₁∧¬b₂}, {b₁∧b₂, b₂∧¬b₁}, {b₁∧¬b₂, b₂∧¬b₁}), so IE = ∅ and innocent.exh is vacuous (see root_full_innocent_vacuous). The paper's result (103) requires applying operators separately — exactly the split-exhaustification architecture.

Root Contexts (§4)

With a domain D = {b₁, b₂}, the assertion of unembedded yek-i is b₁ ∨ b₂ ("Forood bought a book"). PQWorld enumerates the four possible book-buying configurations.

The three alternative classes:

• Scalar: {b₁ ∧ b₂} (bought ≥ 2, from replacing numeral yek)
• Domain: {b₁, b₂} (restricting quantification to subdomains)
• Pre-exhaustified domain: {b₁ ∧ ¬b₂, b₂ ∧ ¬b₁}

inductive AlonsoOvalleMoghiseh2025.PQWorld : Type

Four book-buying configurations: each book independently bought or not.

• pOnly : PQWorld
• qOnly : PQWorld
• both : PQWorld
• neither : PQWorld

def AlonsoOvalleMoghiseh2025.instReprPQWorld.repr : PQWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025.instReprPQWorld : Repr PQWorld

Equations

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

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025.instDecidableEqPQWorld : DecidableEq PQWorld

Equations

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

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025.instFintypePQWorld : Fintype PQWorld

Equations

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

theorem AlonsoOvalleMoghiseh2025.preExhDom_from_innocent_root : Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.domAlts✝ (Exhaustification.predToFinset AlonsoOvalleMoghiseh2025.pProp✝) = Exhaustification.predToFinset AlonsoOvalleMoghiseh2025.preExhDomAlt1✝ ∧ Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.domAlts✝ (Exhaustification.predToFinset AlonsoOvalleMoghiseh2025.qProp✝) = Exhaustification.predToFinset AlonsoOvalleMoghiseh2025.preExhDomAlt2✝

Pre-exhaustified domain alternatives are derived from IE, not stipulated. innocent.exh({b₁,b₂})(b₁) = b₁ ∧ ¬b₂ and dually for b₂.

Result 1: Full exhaustification yields contradiction

theorem AlonsoOvalleMoghiseh2025.root_full_tolerant_contradiction : Exhaustification.tolerant.exh AlonsoOvalleMoghiseh2025.allAltsF✝ AlonsoOvalleMoghiseh2025.assertionF✝ = ∅

Theorem (eq. 92): Chierchia's contradiction-tolerating operator applied to all alternatives yields ⊥ — the assertion conjoined with negation of all non-entailed alternatives is unsatisfiable.

(b₁∨b₂) ∧ ¬(b₁∧b₂) ∧ ¬(b₁∧¬b₂) ∧ ¬(b₂∧¬b₁) ⟺ ⊥.

Derived from the structural substrate theorem tolerant_exh_eq_empty_of_covered: every assertionF-world (each of pOnly, qOnly, both) belongs to some non-entailed alternative (preExhDomAlt1F, preExhDomAlt2F, or scalarAltF respectively), so tolerant exhaustification has no surviving witness.

theorem AlonsoOvalleMoghiseh2025.root_full_innocent_vacuous : Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.allAltsF✝ AlonsoOvalleMoghiseh2025.assertionF✝ = AlonsoOvalleMoghiseh2025.assertionF✝

With Fox's IE, full exhaustification is vacuous (IE = ∅, no alternative is in every MCE).

Note on MCE count: The paper's (101) lists 2 MCEs for this alternative set, but there are actually 3 — {b₁∧b₂, b₁∧¬b₂}, {b₁∧b₂, b₂∧¬b₁}, and {b₁∧¬b₂, b₂∧¬b₁}. Since no alternative appears in all 3, IE = ∅ and Fox's operator is vacuous. The paper's result (103) = uniqueness requires IE = {b₁∧b₂}, which holds when the operators are applied separately (scalar-only IE correctly excludes b₁∧b₂ — see root_scalar_only_uniqueness).

Innocent vs tolerant: For this specific alternative set, tolerant yields ⊥ while innocent is vacuous — they differ maximally. The split exhaustification architecture (O_σ and O_EXH-D as independent operators) means the paper's predictions go through innocent on each operator separately, not tolerant on the combined set.

Derived from innocent_exh_eq_phi_of_innocentlyExcludable_empty (the substrate's IE-vacuity lemma): the IE algorithm returns the empty set on this 3-alt configuration, so exhaustification reduces to the identity.

Result 2: Scalar-only exhaustification yields uniqueness

theorem AlonsoOvalleMoghiseh2025.root_scalar_only_uniqueness : Exhaustification.innocent.exh (Exhaustification.altsFromPreds [AlonsoOvalleMoghiseh2025.scalarAlt✝]) AlonsoOvalleMoghiseh2025.assertionF✝ = AlonsoOvalleMoghiseh2025.assertionF✝ \ AlonsoOvalleMoghiseh2025.scalarAltF✝

Theorem (eq. 93a): O_σ (scalar-only exhaustification) yields uniqueness: (b₁ ∨ b₂) ∧ ¬(b₁ ∧ b₂) = "exactly one book."

This is yek-i's reading in root contexts via partial exhaustification.

Derived from innocent_exh_singleton_proper: when ALT is the singleton {scalarAltF} and scalarAltF ⊊ assertionF (i.e., {both} ⊊ {pOnly, qOnly, both}), the substrate gives innocent.exh = assertionF \ scalarAltF.

theorem AlonsoOvalleMoghiseh2025.root_scalar_only_contingent : PQWorld.pOnly ∈ Exhaustification.innocent.exh (Exhaustification.altsFromPreds [AlonsoOvalleMoghiseh2025.scalarAlt✝]) AlonsoOvalleMoghiseh2025.assertionF✝ ∧ PQWorld.both ∉ Exhaustification.innocent.exh (Exhaustification.altsFromPreds [AlonsoOvalleMoghiseh2025.scalarAlt✝]) AlonsoOvalleMoghiseh2025.assertionF✝

Uniqueness is contingent (not contradictory).

Result 3: Domain-only exhaustification yields conjunction

theorem AlonsoOvalleMoghiseh2025.root_domain_only_conjunction : Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.preExhDomAltsF✝ AlonsoOvalleMoghiseh2025.assertionF✝ = Exhaustification.predToFinset AlonsoOvalleMoghiseh2025.pAndQ✝

Theorem (eq. 93b): O_EXH-D (domain-only exhaustification) yields conjunction: (b₁ ∨ b₂) ∧ (b₁ ↔ b₂) ⟺ b₁ ∧ b₂.

This is blocked by Chierchia's Economy Principle (the result is equivalent to the scalar alternative).

Derived from innocent_exh_pairwise_disjoint_partial: the two pre-exhaustified domain alternatives ({pOnly} and {qOnly}) are pairwise-disjoint singletons both ⊆ assertionF, with witness both ∈ assertionF \ (alt₁ ∪ alt₂). The substrate returns assertionF \ ({pOnly} ∪ {qOnly}) = {both} = predToFinset pAndQ.

theorem AlonsoOvalleMoghiseh2025.domain_exh_equiv_scalar_alt : Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.preExhDomAltsF✝ AlonsoOvalleMoghiseh2025.assertionF✝ = AlonsoOvalleMoghiseh2025.scalarAltF✝

Domain-only result is equivalent to the scalar alternative → blocked by the Exhaustification Economy Principle.

Deontic Possibility (§5, eq. 114–119)

LF: O_EXH-D ◇ O_σ [IP ye book-i ... Forood buy t₁]

Step 1: O_σ on IP → (b₁∨b₂) ∧ ¬(b₁∧b₂) = "exactly one book" Step 2: ◇ applied → ◇(b₁⊻b₂) = "permitted to buy exactly one" Step 3: O_EXH-D negates pre-exhaustified domain alternatives

The result is FC + embedded uniqueness: ◇b₁ ∧ ◇b₂ ∧ ◇(b₁⊻b₂), meaning each book is a permitted option and in each permitted world exactly one book is bought.

World Type

Worlds are parameterized by which atomic modal propositions hold: ◇(b₁∧¬b₂), ◇(b₂∧¬b₁), ◇(b₁∧b₂). This gives 8 possible states.

inductive AlonsoOvalleMoghiseh2025.PermW : Type

Modal worlds for the EFCI analysis. Each world represents a permission state parameterized by three atomic modal propositions: ◇(b₁∧¬b₂), ◇(b₂∧¬b₁), ◇(b₁∧b₂). Named by which are true (1) or false (0) in order.

• w000 : PermW
• w100 : PermW
• w010 : PermW
• w110 : PermW
• w001 : PermW
• w101 : PermW
• w011 : PermW
• w111 : PermW

def AlonsoOvalleMoghiseh2025.instReprPermW.repr : PermW → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025.instReprPermW : Repr PermW

Equations

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

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025.instDecidableEqPermW : DecidableEq PermW

Equations

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

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025.instFintypePermW : Fintype PermW

Equations

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

theorem AlonsoOvalleMoghiseh2025.preExhDom_from_innocent : Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.modalDomAltsF✝ (Exhaustification.predToFinset AlonsoOvalleMoghiseh2025.canB1✝) = Exhaustification.predToFinset AlonsoOvalleMoghiseh2025.modalPreExhDomAlt1✝ ∧ Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.modalDomAltsF✝ (Exhaustification.predToFinset AlonsoOvalleMoghiseh2025.canB2✝) = Exhaustification.predToFinset AlonsoOvalleMoghiseh2025.modalPreExhDomAlt2✝

Pre-exhaustified domain alts are correctly computed by applying innocent.exh to each domain alternative w.r.t. the domain alternative set.

theorem AlonsoOvalleMoghiseh2025.deontic_poss_split_exh : Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.modalPreExhDomAltsF✝ AlonsoOvalleMoghiseh2025.canExOrF✝ = {w ∈ AlonsoOvalleMoghiseh2025.canExOrF✝ | (AlonsoOvalleMoghiseh2025.canB1✝ w == AlonsoOvalleMoghiseh2025.canB2✝ w) = true}

Theorem (eq. 119): Split exhaustification under ◇ derives FC + embedded uniqueness: ◇(b₁⊻b₂) ∧ (◇b₁ ↔ ◇b₂)

Equivalently: ◇(b₁⊻b₂) ∧ ◇b₁ ∧ ◇b₂ — each book is a permitted option, and in each permitted world exactly one book is bought.

Derived from innocent_exh_pairwise_disjoint_partial: the two pre-exhaustified modal domain alternatives (canB1 ∧ ¬canB2 and canB2 ∧ ¬canB1) are pairwise-disjoint subsets of canExOrF, with worlds satisfying both canB1 and canB2 (e.g. w111) surviving as the partial-cover witness. The set-difference RHS then equals the filter RHS by Finset extensionality.

theorem AlonsoOvalleMoghiseh2025.deontic_poss_fc (w : PermW) (h : w ∈ Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.modalPreExhDomAltsF✝ AlonsoOvalleMoghiseh2025.canExOrF✝) : AlonsoOvalleMoghiseh2025.canB1✝ w = true ∧ AlonsoOvalleMoghiseh2025.canB2✝ w = true

FC component: the result entails ◇b₁ ∧ ◇b₂ whenever true.

theorem AlonsoOvalleMoghiseh2025.deontic_poss_embedded_uniqueness (w : PermW) (h : w ∈ Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.modalPreExhDomAltsF✝ AlonsoOvalleMoghiseh2025.canExOrF✝) : AlonsoOvalleMoghiseh2025.canExOr✝ w = true

Embedded uniqueness: the assertion ◇(b₁⊻b₂) means in every permitted world exactly one book is bought (the ⊻ is under ◇).

theorem AlonsoOvalleMoghiseh2025.deontic_poss_compatible_with_joint : PermW.w111 ∈ Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.modalPreExhDomAltsF✝ AlonsoOvalleMoghiseh2025.canExOrF✝

The result is compatible with ◇(b₁∧b₂) being true: Forood may be permitted to buy more than one book (paper main text near eq. 60, p. 21: "compatible with a scenario where he is allowed to buy one book and he is allowed to buy more than one book").

Without split: no FC

theorem AlonsoOvalleMoghiseh2025.single_exh_no_fc : Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.unsplitModalAltsF✝ AlonsoOvalleMoghiseh2025.canBuyAnyF✝ = {w ∈ AlonsoOvalleMoghiseh2025.canBuyAnyF✝ | (!AlonsoOvalleMoghiseh2025.canJoint✝ w) = true}

Theorem: Single IE on ◇(b₁∨b₂) without split gives ◇(b₁∨b₂) ∧ ¬◇(b₁∧b₂) — anti-conjunction at the modal level (only ◇(b₁∧b₂) is innocently excludable), but NOT free choice.

This shows split exhaustification is necessary for yek-i's distinctive FC + embedded uniqueness profile.

theorem AlonsoOvalleMoghiseh2025.single_exh_not_fc_witness : PermW.w100 ∈ Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.unsplitModalAltsF✝ AlonsoOvalleMoghiseh2025.canBuyAnyF✝ ∧ AlonsoOvalleMoghiseh2025.canB1✝ PermW.w100 = true ∧ AlonsoOvalleMoghiseh2025.canB2✝ PermW.w100 = false

The single-exh result is NOT free choice: there exists a world satisfying the exhaustified assertion where ◇b₁ but ¬◇b₂.

Why Split Exhaustification Is Necessary

The paper argues that only split exhaustification — two independent operators targeting different alternative classes — derives the correct result. Three alternative architectures all fail:

1. Single operator below ◇ (eq. 143): gives ◇(uniqueness), too weak
2. Single operator above ◇ (eq. 146): gives FC + unwanted ¬◇(b₁∧b₂)
3. Two operators above+below (eq. 144): same as (2) — too strong

Only split exh (O_EXH-D above ◇, O_σ below ◇) avoids negating the modal scalar alternative, producing FC + uniqueness without ¬◇(b₁∧b₂).

theorem AlonsoOvalleMoghiseh2025.below_modal_only_no_fc : AlonsoOvalleMoghiseh2025.canExOr✝ PermW.w100 = true ∧ AlonsoOvalleMoghiseh2025.canB1✝ PermW.w100 = true ∧ AlonsoOvalleMoghiseh2025.canB2✝ PermW.w100 = false

Single operator below ◇ too weak (eq. 143): after scalar exhaustification below the modal gives ◇(b₁⊻b₂), the result is compatible with only one book being permitted — no FC emerges without domain exhaustification above the modal.

theorem AlonsoOvalleMoghiseh2025.above_only_all_alts_too_strong : Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.allModalAltsF✝ AlonsoOvalleMoghiseh2025.canBuyAnyF✝ = {w ∈ AlonsoOvalleMoghiseh2025.canBuyAnyF✝ | (AlonsoOvalleMoghiseh2025.canB1✝ w == AlonsoOvalleMoghiseh2025.canB2✝ w && !AlonsoOvalleMoghiseh2025.canJoint✝ w) = true}

Single operator above ◇ too strong (eq. 146): a single IE operator above ◇ with all alternatives on the unexhaustified assertion ◇(b₁∨b₂) gives FC (from domain alts) BUT ALSO ¬◇(b₁∧b₂) (from scalar alt).

Compare with split exh (deontic_poss_split_exh): the only difference is && !canJoint w. Split exh allows ◇(b₁∧b₂), this forbids it.

theorem AlonsoOvalleMoghiseh2025.two_ie_above_below_too_strong : Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.allModalAltsF✝ AlonsoOvalleMoghiseh2025.canExOrF✝ = {w ∈ AlonsoOvalleMoghiseh2025.canExOrF✝ | (AlonsoOvalleMoghiseh2025.canB1✝ w == AlonsoOvalleMoghiseh2025.canB2✝ w && !AlonsoOvalleMoghiseh2025.canJoint✝ w) = true}

Two operators above+below ◇ too strong (eq. 144-145): two IE operators (O_σ below gives ◇(b₁⊻b₂), then full IE above) produces FC + embedded uniqueness BUT ALSO ¬◇(b₁∧b₂).

Compare with split exh: identical result except for && !canJoint w. The scalar alternative ◇(b₁∧b₂) is innocently excludable because it is non-entailed and consistently negatable alongside domain-alt negations.

theorem AlonsoOvalleMoghiseh2025.two_ie_strictly_stronger : Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.allModalAltsF✝ AlonsoOvalleMoghiseh2025.canExOrF✝ ⊆ Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.modalPreExhDomAltsF✝ AlonsoOvalleMoghiseh2025.canExOrF✝ ∧ PermW.w111 ∈ Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.modalPreExhDomAltsF✝ AlonsoOvalleMoghiseh2025.canExOrF✝ ∧ PermW.w111 ∉ Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.allModalAltsF✝ AlonsoOvalleMoghiseh2025.canExOrF✝

Two-IE exhaustification is strictly stronger than split: it entails the split result but not vice versa. The difference is exactly ¬◇(b₁∧b₂) — split exh never negates the modal scalar alternative.

theorem AlonsoOvalleMoghiseh2025.split_allows_joint_two_ie_forbids : (PermW.w111 ∈ Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.modalPreExhDomAltsF✝ AlonsoOvalleMoghiseh2025.canExOrF✝ ∧ AlonsoOvalleMoghiseh2025.canJoint✝ PermW.w111 = true) ∧ ∀ w ∈ Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.allModalAltsF✝ AlonsoOvalleMoghiseh2025.canExOrF✝, AlonsoOvalleMoghiseh2025.canJoint✝ w = false

The distinguishing case: split exh allows ◇(b₁∧b₂) (compatible with Forood buying both), while any architecture targeting the scalar alternative at the modal level forbids it.

Deontic Necessity (§5, eq. 120)

LF: O_EXH-D □ O_σ [IP ye book-i ... Forood buy t₁]

The same split exhaustification structure under □ instead of ◇.

Step 1: O_σ on IP → b₁⊻b₂ (as before) Step 2: □ applied → □(b₁⊻b₂) = "must buy exactly one" Step 3: O_EXH-D negates pre-exhaustified domain alternatives under □

Box Operators (reusing PermW)

□b₁ = ¬◇(b₂∧¬b₁) = ¬canExB2: every accessible world has b₁. □b₂ = ¬◇(b₁∧¬b₂) = ¬canExB1: every accessible world has b₂. □(b₁⊻b₂) = ¬◇(b₁∧b₂) = ¬canJoint: no joint-purchase world accessible.

Box operators derived from PermW's possibility atoms. The encodings rely on the implicit constraint □(b₁∨b₂) — every accessible world has at least one book bought — which holds by construction of PermW since worlds with neither book are not in the state space. Under that constraint:

• □b₁ = ¬◇(b₂ ∧ ¬b₁), and
• □(b₁⊻b₂) collapses to ¬◇(b₁∧b₂), since the only way to violate exactly-one-per-world is via a joint-purchase world.

theorem AlonsoOvalleMoghiseh2025.preExhDom_from_innocent_nec : Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.boxDomAltsF✝ (Exhaustification.predToFinset AlonsoOvalleMoghiseh2025.boxB1✝) = Exhaustification.predToFinset AlonsoOvalleMoghiseh2025.necPreExhDomAlt1✝ ∧ Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.boxDomAltsF✝ (Exhaustification.predToFinset AlonsoOvalleMoghiseh2025.boxB2✝) = Exhaustification.predToFinset AlonsoOvalleMoghiseh2025.necPreExhDomAlt2✝

Pre-exhaustified domain alts under □ are derived from IE.

theorem AlonsoOvalleMoghiseh2025.deontic_nec_split_exh : Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.necPreExhDomAltsF✝ AlonsoOvalleMoghiseh2025.boxExOrF✝ = {w ∈ AlonsoOvalleMoghiseh2025.boxExOrF✝ | (AlonsoOvalleMoghiseh2025.boxB1✝ w == AlonsoOvalleMoghiseh2025.boxB2✝ w) = true}

Theorem (eq. 120): Split exhaustification under □ derives FC + embedded uniqueness: □(b₁⊻b₂) ∧ (□b₁ ↔ □b₂).

"Must buy exactly one book, and neither book is predetermined" — each book remains a possible choice within the obligation.

Derived from innocent_exh_pairwise_disjoint_partial, analogous to deontic_poss_split_exh under □: with boxExOrF \ ALT.sup id non-empty (joint-allowing worlds outside both alts), every alternative is innocently excludable. Note the alts here are not subsets of boxExOrF — a world like w101 (joint allowed, boxB1 ∧ ¬boxB2 holds) lies in necPreExhDomAlt1 but outside boxExOrF. The substrate's φ \ ALT.sup id formulation handles this by intersecting alts with φ automatically.

theorem AlonsoOvalleMoghiseh2025.deontic_nec_fc (w : PermW) (h : w ∈ Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.necPreExhDomAltsF✝ AlonsoOvalleMoghiseh2025.boxExOrF✝) (hne : AlonsoOvalleMoghiseh2025.canExB1✝ w = true ∨ AlonsoOvalleMoghiseh2025.canExB2✝ w = true) : AlonsoOvalleMoghiseh2025.boxB1✝ w = false ∧ AlonsoOvalleMoghiseh2025.boxB2✝ w = false

FC component under □: ¬□b₁ ∧ ¬□b₂ (neither book is obligatory) whenever the exhaustified assertion holds non-vacuously.

theorem AlonsoOvalleMoghiseh2025.deontic_nec_embedded_uniqueness (w : PermW) (h : w ∈ Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.necPreExhDomAltsF✝ AlonsoOvalleMoghiseh2025.boxExOrF✝) : AlonsoOvalleMoghiseh2025.canJoint✝ w = false

Embedded uniqueness under □: no joint-purchase world is accessible.

DE Contexts (§5, eq. 129–135)

In DE contexts (e.g., conditional antecedents), scalar exhaustification below the operator is blocked by Maximize Strength: it globally weakens the matrix sentence.

"If Forood reads ye book-i, he gets a gift"

• Without O_σ: (b₁ ∨ b₂) → g
• With O_σ: ((b₁ ∨ b₂) ∧ ¬(b₁ ∧ b₂)) → g ← strictly weaker!

Since weakening is detected, O_σ is blocked, and the EFCI contributes plain existential force.

inductive AlonsoOvalleMoghiseh2025.CondW : Type

Worlds for the conditional: b₁, b₂, g (gift).

• b1g : CondW
• b2g : CondW
• bg : CondW
• b1 : CondW
• b2 : CondW
• b : CondW
• g : CondW
• none : CondW

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025.instReprCondW : Repr CondW

Equations

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

def AlonsoOvalleMoghiseh2025.instReprCondW.repr : CondW → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025.instDecidableEqCondW : DecidableEq CondW

Equations

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

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025.instFintypeCondW : Fintype CondW

Equations

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

theorem AlonsoOvalleMoghiseh2025.de_scalar_exh_weakens : AlonsoOvalleMoghiseh2025.condNoExhF✝ ⊂ AlonsoOvalleMoghiseh2025.condWithExhF✝

Theorem (eq. 131–134): Scalar exhaustification inside a conditional antecedent strictly weakens the matrix.

condNoExhF ⊂ condWithExhF: the exhaustified version is true in strictly more worlds, so it carries less information.

theorem AlonsoOvalleMoghiseh2025.de_no_exh_stronger : AlonsoOvalleMoghiseh2025.condNoExhF✝ ⊆ AlonsoOvalleMoghiseh2025.condWithExhF✝

Without exhaustification, the conditional is stronger: every condNoExh-world is a condWithExh-world.

theorem AlonsoOvalleMoghiseh2025.de_exh_weaker_witness : ∃ w ∈ AlonsoOvalleMoghiseh2025.condWithExhF✝, w ∉ AlonsoOvalleMoghiseh2025.condNoExhF✝

With exhaustification, there's a world satisfying condWithExh but not condNoExh.

theorem AlonsoOvalleMoghiseh2025.de_domain_exh_vacuous : Exhaustification.innocent.exh AlonsoOvalleMoghiseh2025.condPreExhDomAltsF✝ AlonsoOvalleMoghiseh2025.condNoExhF✝ = AlonsoOvalleMoghiseh2025.condNoExhF✝

Theorem: In DE contexts, domain exhaustification on the conditional is vacuous: innocent.exh = condNoExhF. The pre-exhaustified domain alternatives (b₁→g) ∧ ¬(b₂→g) and (b₂→g) ∧ ¬(b₁→g) are inconsistent with the full-domain conditional, so any IE-excluded alt is disjoint from condNoExhF — excluding it removes nothing from the prejacent's support, and innocent.exh reduces to the identity.

This means even without Maximize Strength blocking O_σ, O_EXH-D alone contributes nothing in DE contexts — the plain existential reading emerges regardless.

EFCI Typology (Table 2)

[AOM25a] Table 2: EFCIs vary along two parameters — modal insertion and partial exhaustification.

Type	Modal insertion	Partial exh	Lexicon entry
vreun	−	−	Farsi.Determiners.vreun_ro
irgendein	+	−	Farsi.Determiners.irgendein_de
yek-i	−	+	Farsi.Determiners.yeki

The typology is canonicalized in Farsi.Determiners.EFCIRescue (re-exported above), and the per-item root-reading predictions are checked there:

• Farsi.Determiners.yeki_root : getReading yeki rootContext = some .uniqueness
• Farsi.Determiners.irgendein_root : getReading irgendein_de rootContext = some .epistemicIgnorance
• Farsi.Determiners.vreun_root_ungrammatical : getReading vreun_ro rootContext = none

Structural Prop-level proofs (Abstract)

These lift the paper claims to arbitrary D : Type* with P : D → Prop, plus arbitrary Kripke frames via Acc : W → Prop + Q : D → W → Prop. The computational sections above verify the algorithm computes the right answers on the paper's worked 2-book domain; this section proves why the results hold at full generality.

Internal scaffolding

Two pure-logic lemmas used by the Kripke-frame lifts below. scalar_exh_uniqueness, antecedent_weakening, de_domain_alt_entailed and similar paper-claim restatements were removed during a cleanup pass: the top-level computational layer captures them via substrate-derived proofs on the worked example, so the Type-level versions in this namespace would duplicate. The two lemmas kept here are the ones the Kripke-frame modal lifts (modal_split_exh_fc, modal_full_exh_contradiction) genuinely depend on.

theorem AlonsoOvalleMoghiseh2025.Abstract.fc_two_element (P : Fin 2 → Prop) (hExist : ∃ (d : Fin 2), P d) (hNegExcl : ∀ (d : Fin 2), ¬(P d ∧ ∀ (e : Fin 2), e ≠ d → ¬P e)) (d : Fin 2) : P d

Two-element free choice: for a two-element domain, existence plus negation of all exclusive alternatives forces every element to satisfy P.

theorem AlonsoOvalleMoghiseh2025.Abstract.root_full_exh_contradiction (P : Fin 2 → Prop) (hExist : ∃ (d : Fin 2), P d) (hNotAll : ¬∀ (d : Fin 2), P d) (hNegExcl : ∀ (d : Fin 2), ¬(P d ∧ ∀ (e : Fin 2), e ≠ d → ¬P e)) : False

Root contradiction: asserting ∃d P d, negating ∀d P d (scalar), and negating both exclusive domain alternatives yields ⊥ for a two-element domain.

Paper-scope finding

full_exh_consistent_three shows the root contradiction is specifically a |D|=2 artifact: for any |D|≥3, the three premises that contradict on 2-book Fin 2 are jointly satisfiable. This is the project's contribution beyond the paper's worked example.

theorem AlonsoOvalleMoghiseh2025.Abstract.full_exh_consistent_three : ∃ (P : Fin 3 → Prop), (∃ (d : Fin 3), P d) ∧ (¬∀ (d : Fin 3), P d) ∧ ∀ (d : Fin 3), ¬(P d ∧ ∀ (e : Fin 3), e ≠ d → ¬P e)

Full exh consistent for 3-element domain: unlike the 2-element case, for |D|=3 we can simultaneously have (∃d P d), ¬(∀d P d), and (∀d ¬exclusive(d)). The root contradiction is |D|=2-specific.

Modal split exhaustification (Kripke-frame lift)

All root-level results lift to arbitrary Kripke frames by instantiating P : D → Prop with fun d => ∃ w, Acc w ∧ Q d w where Acc : W → Prop is the accessibility predicate and Q : D → W → Prop is the base property. Modal operators: ◇φ ≡ ∃ w, Acc w ∧ φ w; □φ ≡ ∀ w, Acc w → φ w.

theorem AlonsoOvalleMoghiseh2025.Abstract.diamond_preserves_exist {W : Type u_1} {D : Type u_2} (Acc : W → Prop) (Q : D → W → Prop) (h : ∃ (w : W), Acc w ∧ ∃ (d : D), Q d w) : ∃ (d : D) (w : W), Acc w ∧ Q d w

◇ preserves existential: if some accessible world satisfies ∃x, Q x, then ∃d, ◇(Q d).

theorem AlonsoOvalleMoghiseh2025.Abstract.diamond_uniqueness_implies_exist {W : Type u_1} {D : Type u_2} (Acc : W → Prop) (Q : D → W → Prop) (h : ∃ (w : W), Acc w ∧ ∃ (d : D), Q d w ∧ ∀ (e : D), Q e w → e = d) : ∃ (d : D) (w : W), Acc w ∧ Q d w

◇ preserves existence from uniqueness: ◇(∃!d, Q d) entails ∃d, ◇(Q d).

theorem AlonsoOvalleMoghiseh2025.Abstract.modal_domain_exh_plurality {W : Type u_1} {D : Type u_2} (Acc : W → Prop) (Q : D → W → Prop) (hExist : ∃ (d : D) (w : W), Acc w ∧ Q d w) (hNegExcl : ∀ (d : D), ¬((∃ (w : W), Acc w ∧ Q d w) ∧ ∀ (e : D), e ≠ d → ¬∃ (w : W), Acc w ∧ Q e w)) : ∃ (d₁ : D) (d₂ : D), d₁ ≠ d₂ ∧ (∃ (w : W), Acc w ∧ Q d₁ w) ∧ ∃ (w : W), Acc w ∧ Q d₂ w

Modal domain-exh gives plurality: for any domain D, if ◇(∃x, Q x) and domain-exh negates all exclusive modal alternatives, then at least two domain elements are possible.

theorem AlonsoOvalleMoghiseh2025.Abstract.modal_split_exh_fc {W : Type u_1} (Acc : W → Prop) (Q : Fin 2 → W → Prop) (hExist : ∃ (d : Fin 2) (w : W), Acc w ∧ Q d w) (hNegExcl : ∀ (d : Fin 2), ¬((∃ (w : W), Acc w ∧ Q d w) ∧ ∀ (e : Fin 2), e ≠ d → ¬∃ (w : W), Acc w ∧ Q e w)) (d : Fin 2) : ∃ (w : W), Acc w ∧ Q d w

Modal split exh gives FC (|D|=2): for a 2-element domain, domain-exh above ◇ gives full free choice: every element is permitted.

theorem AlonsoOvalleMoghiseh2025.Abstract.modal_split_exh_full {W : Type u_1} (Acc : W → Prop) (Q : Fin 2 → W → Prop) (hUniq : ∃ (w : W), Acc w ∧ ∃ (d : Fin 2), Q d w ∧ ∀ (e : Fin 2), Q e w → e = d) (hNegExcl : ∀ (d : Fin 2), ¬((∃ (w : W), Acc w ∧ Q d w) ∧ ∀ (e : Fin 2), e ≠ d → ¬∃ (w : W), Acc w ∧ Q e w)) : (∀ (d : Fin 2), ∃ (w : W), Acc w ∧ Q d w) ∧ ∃ (w : W), Acc w ∧ ∃ (d : Fin 2), Q d w ∧ ∀ (e : Fin 2), Q e w → e = d

Full split exh composition: O_σ below ◇ gives uniqueness; domain-exh above ◇ gives FC. Together: FC + embedded uniqueness.

theorem AlonsoOvalleMoghiseh2025.Abstract.modal_uniqueness_not_fc : ∃ (W : Type) (Acc : W → Prop) (Q : Fin 2 → W → Prop), (∃ (w : W), Acc w ∧ ∃ (d : Fin 2), Q d w ∧ ∀ (e : Fin 2), Q e w → e = d) ∧ ¬∀ (d : Fin 2), ∃ (w : W), Acc w ∧ Q d w

◇(uniqueness) doesn't entail FC: countermodel where only d=0 satisfies Q in the unique accessible world.

theorem AlonsoOvalleMoghiseh2025.Abstract.modal_full_exh_contradiction {W : Type u_1} (Acc : W → Prop) (Q : Fin 2 → W → Prop) (hExist : ∃ (d : Fin 2) (w : W), Acc w ∧ Q d w) (hNotAll : ¬∀ (d : Fin 2), ∃ (w : W), Acc w ∧ Q d w) (hNegExcl : ∀ (d : Fin 2), ¬((∃ (w : W), Acc w ∧ Q d w) ∧ ∀ (e : Fin 2), e ≠ d → ¬∃ (w : W), Acc w ∧ Q e w)) : False

Full exh above ◇ contradicts FC (|D|=2): adding scalar negation ¬(∀d, ◇(Q d)) to domain-exh yields ⊥.

theorem AlonsoOvalleMoghiseh2025.Abstract.modal_exclusive_false_of_universal {W : Type u_1} {D : Type u_2} {a b : D} (hab : a ≠ b) (Acc : W → Prop) (Q : D → W → Prop) (hAll : ∀ (d : D), ∃ (w : W), Acc w ∧ Q d w) (d : D) : ¬((∃ (w : W), Acc w ∧ Q d w) ∧ ∀ (e : D), e ≠ d → ¬∃ (w : W), Acc w ∧ Q e w)

∀d ◇(Q d) negates all exclusives: if every element is possible, then no element is exclusively possible.

theorem AlonsoOvalleMoghiseh2025.Abstract.modal_split_compatible_with_joint : ∃ (W : Type) (Acc : W → Prop) (Q : Fin 2 → W → Prop), (∃ (d : Fin 2) (w : W), Acc w ∧ Q d w) ∧ (∀ (d : Fin 2), ¬((∃ (w : W), Acc w ∧ Q d w) ∧ ∀ (e : Fin 2), e ≠ d → ¬∃ (w : W), Acc w ∧ Q e w)) ∧ (∀ (d : Fin 2), ∃ (w : W), Acc w ∧ Q d w) ∧ ∃ (w : W), Acc w ∧ ∀ (d : Fin 2), Q d w

Split exh compatible with ◇(∀d Q d): domain-exh premises, FC, and the modal scalar ◇(∀d Q d) hold simultaneously.

theorem AlonsoOvalleMoghiseh2025.Abstract.modal_split_full_compatible_with_joint : ∃ (W : Type) (Acc : W → Prop) (Q : Fin 2 → W → Prop), (∃ (w : W), Acc w ∧ ∃ (d : Fin 2), Q d w ∧ ∀ (e : Fin 2), Q e w → e = d) ∧ (∀ (d : Fin 2), ¬((∃ (w : W), Acc w ∧ Q d w) ∧ ∀ (e : Fin 2), e ≠ d → ¬∃ (w : W), Acc w ∧ Q e w)) ∧ (∀ (d : Fin 2), ∃ (w : W), Acc w ∧ Q d w) ∧ ∃ (w : W), Acc w ∧ ∀ (d : Fin 2), Q d w

Full split exh with joint compatibility: FC + embedded uniqueness

• ◇(∀d Q d) all hold simultaneously.