Choice Functions for Indefinite Determiners

[Rei97] [Kra98b] [Win97]

Choice functions provide an alternative to existential quantification for the semantics of indefinite NPs. A choice function selects a single individual from a non-empty set, yielding a referential (type e) meaning for the indefinite DP.

Motivation

The standard ∃-quantifier analysis of indefinites predicts scope via QR or alternative mechanisms. Choice functions predict scope via the binding site of the choice function variable itself:

• Free CF variable (Reinhart): existentially closed at any scope site → flexible scope (wide, intermediate, narrow)
• Contextually bound CF (Kratzer): situation parameter determines scope → scope fixed by situation binding

World-Skolemized Choice Functions

[Mir24] proposes that indefinite determiners can introduce a world variable into the choice function, yielding type ⟨s, ⟨⟨e,t⟩, e⟩⟩. When this world variable is bound by an intensional operator, the CF picks possibly different individuals in different worlds (de dicto), while the existential closure over the CF itself can sit above negation (wide pseudo-scope). When the world variable is free, the CF is evaluated at the actual world (de re). This is captured by connecting SkolemCF to Intensional.SitVarStatus.

Application to African Languages

[Zim08] analyses Hausa wani/wata as a standard ∃-quantifier, predicting flexible scope via QR.

[Owu22] analyses Akan bí as an unambiguous choice function whose situation pronoun ties the CF and the NP to a single index (SkolemCF), explaining why bí takes obligatory wide scope under negation: the contextually-given CF is fixed before negation applies, and negation binds no situation variable that could shift it.

Choice Functions

def Quantification.ChoiceFunction.CF (E : Type u_1) : Type u_1

A choice function selects an individual from a property. [Rei97]: type ⟨⟨e,t⟩, e⟩.

Equations

• Quantification.ChoiceFunction.CF E = ((E → Prop) → E)

def Quantification.ChoiceFunction.CF.isCorrect {E : Type u_1} (f : CF E) : Prop

A choice function is correct if it always selects a member of the input set (when non-empty).

Equations

• f.isCorrect = ∀ (P : E → Prop), (∃ (x : E), P x) → P (f P)

def Quantification.ChoiceFunction.cfIndefSem {E : Type u_1} (f : CF E) (nounProp : E → Prop) : E

An indefinite DP with choice function semantics denotes an individual: the result of applying the CF to the NP-property.

⟦a/some N⟧^f = f(⟦N⟧)

Equations

• Quantification.ChoiceFunction.cfIndefSem f nounProp = f nounProp

Skolemized Choice Functions

def Quantification.ChoiceFunction.SkolemCF (S : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A situation-indexed (skolemized) choice function.

[Kra98b] introduced contextually-given CFs with pronoun-like skolem indices (individual arguments); [Owu22] adds a situation index shared by the CF and its NP argument, and [Mir24] a world index. [Owu22]'s entry:

⟦bí⟧ = λs.λP : CH(f_s). f_s(P(s))

Scope is determined by the binding site of s:

• s bound by a higher operator → wide scope
• s bound locally (e.g., under a modal) → narrow scope
• s free (contextually resolved) → specific/wide scope

Equations

• Quantification.ChoiceFunction.SkolemCF S E = (S → Quantification.ChoiceFunction.CF E)

def Quantification.ChoiceFunction.SkolemCF.apply {S : Type u_1} {E : Type u_2} (f : SkolemCF S E) (s : S) (nounProp : E → Prop) : E

Apply a skolemized CF at a particular situation.

Equations

• f.apply s nounProp = f s nounProp

def Quantification.ChoiceFunction.SkolemCF.isCorrect {S : Type u_1} {E : Type u_2} (f : SkolemCF S E) : Prop

A skolemized CF is correct if it is correct at every situation.

Equations

• f.isCorrect = ∀ (s : S), (f s).isCorrect

Indefinite Analysis Type

inductive Quantification.ChoiceFunction.IndefType : Type

The two main semantic analyses of indefinite determiners.

The analysis type structurally determines scope potential:

• ∃-quantifiers scope via QR/alternative mechanisms → flexible
• Choice functions scope via situation variable binding → obligatory wide scope under non-intensional operators

[Rei97]: the key empirical distinction is scope under negation. ∃-quantifiers allow narrow scope (¬ > ∃); choice functions force wide scope (∃ > ¬) because negation cannot shift the situation variable.

Cross-linguistic evidence: Hausa wani/wata (∃) vs Akan bí (CF) ([Zim26]).

• existential : IndefType
• choiceFunction : IndefType

@[implicit_reducible]

instance Quantification.ChoiceFunction.instDecidableEqIndefType : DecidableEq IndefType

Equations

• Quantification.ChoiceFunction.instDecidableEqIndefType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Quantification.ChoiceFunction.instReprIndefType : Repr IndefType

Equations

• Quantification.ChoiceFunction.instReprIndefType = { reprPrec := Quantification.ChoiceFunction.instReprIndefType.repr }

def Quantification.ChoiceFunction.instReprIndefType.repr : IndefType → ℕ → Std.Format

Equations

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

def Quantification.ChoiceFunction.IndefType.canPseudoDeDicto (t : IndefType) (hasWorldVar : Bool) : Bool

Whether wide pseudo-scope de dicto readings are predicted.

[Mir24] §3: the pseudo-de dicto reading requires BOTH: (1) CF semantics — to separate ∃-closure (above negation) from descriptive content (below the intensional operator) (2) A world variable on the determiner — so the CF's output varies across worlds, yielding de dicto construal

This DERIVES the cross-linguistic variation: Farsi (CF + world var) ✓, German/French (no world var on indefinite determiners) ✗. [Sch12c].

Equations

• Quantification.ChoiceFunction.IndefType.choiceFunction.canPseudoDeDicto hasWorldVar = hasWorldVar
• Quantification.ChoiceFunction.IndefType.existential.canPseudoDeDicto hasWorldVar = false

Scope via Situation Binding

theorem Quantification.ChoiceFunction.cf_wide_scope_specific {E : Type u_1} (f : CF E) (hf : f.isCorrect) {N VP : E → Prop} (hN : ∃ (x : E), N x) (h : ¬VP (f N)) : ∃ (x : E), N x ∧ ¬VP x

The wide-scope (∃ > ¬) reading of a CF-indefinite under negation, ⟦¬[bí N VP]⟧ = ¬VP(f(N)), is specific: a correct CF selects a restrictor member, so ¬VP(f(N)) entails the witnessed ∃x[N(x) ∧ ¬VP(x)] — without entailing the narrow-scope ¬∃x[N(x) ∧ VP(x)] (the readings diverge whenever N is not VP-uniform). Contrast ⟦¬[wani N VP]⟧ = ¬∃x[N(x) ∧ VP(x)].

theorem Quantification.ChoiceFunction.cf_wide_scope_under_negation {E : Type u_1} (f : CF E) (hf : f.isCorrect) (N VP : E → Prop) (hNonEmpty : ∃ (x : E), N x) (hAll : ∀ (x : E), N x → VP x) : VP (f N)

A correct CF's output satisfies VP whenever every restrictor member does — the degenerate case in which the wide (∃ > ¬) and narrow (¬ > ∃) readings coincide. The CF-essential content of the wide-scope reading is cf_wide_scope_specific.

theorem Quantification.ChoiceFunction.exists_narrow_scope_under_negation {E : Type u_1} (N VP : E → Prop) (hNoMatch : ∀ (x : E), N x → ¬VP x) : ¬∃ (x : E), N x ∧ VP x

An ∃-quantifier can take narrow scope under negation: ¬∃x[N(x) ∧ VP(x)] is satisfiable even when N is non-empty.

World Variable and De Re / De Dicto

def Quantification.ChoiceFunction.SkolemCF.evalAt {S : Type u_1} {E : Type u_2} (f : SkolemCF S E) (status : Intensional.SitVarStatus.SitVarStatus) (w₀ wBound : S) (nounProp : E → Prop) : E

Evaluate a skolemized CF according to the status of its world variable.

• SitVarStatus.free: evaluate at w₀ (the actual world) → de re
• SitVarStatus.bound: evaluate at the bound world w' → de dicto

[Mir24] §3: this is the mechanism that produces wide pseudo-scope de dicto readings. The ∃-closure over f sits above negation (wide scope), while the world argument is bound by the intensional operator (de dicto).

Equations

• f.evalAt Intensional.SitVarStatus.SitVarStatus.free w₀ wBound nounProp = f w₀ nounProp
• f.evalAt Intensional.SitVarStatus.SitVarStatus.bound w₀ wBound nounProp = f wBound nounProp

theorem Quantification.ChoiceFunction.SkolemCF.cross_world_variation {S : Type u_1} {E : Type u_2} (f : SkolemCF S E) (w₁ w₂ : S) (P : E → Prop) (hVary : f w₁ P ≠ f w₂ P) : f.evalAt Intensional.SitVarStatus.SitVarStatus.bound w₁ w₂ P ≠ f.evalAt Intensional.SitVarStatus.SitVarStatus.bound w₂ w₁ P

A world-skolemized CF can return different individuals at different worlds — this is what solves the fixed-set problem.

[Mir24] ex. (45): even when the NP extension is rigid (the same set at every world), a world-skolemized CF f(w', P) can pick different members at different worlds because f is a function of w'.

Intensional restrictors and construal collapse

[Owu22]'s entry (67) — ⟦bí⟧ = λs.λP : CH(f_s). f_s(P(s)) — feeds one situation s to both the CF's skolem index and the restrictor. Here the restrictor is a genuine intension Intensional.Intension S (E → Prop). Curry note: Owusu types P as ⟨e,st⟩ (entity-first) and writes P(s) informally for the s-extension {x | P(x)(s)}; applyIntension takes the situation-first transpose so that P s is that extension literally.

The collapse/divergence pair formalizes [Zim26]'s gloss of the account — "as negation is not an intensional operator, the situational skolem argument of the choice function cannot be shifted away from the actual resource situation … resulting in wide scope only": operators extensional at the matrix situation (Intensional.IsExtensionalAt) neutralize the free/bound distinction for the situation pronoun (bound_free_collapse), while situation quantifiers (box: conditionals, attitudes) separate the construals (bound_free_diverge_box). The content-side dual — rigid restrictors collapse the readings under any operator — is [Mir24]'s fixed-set observation (Studies/Mirrazi2024's deRe_eq_pseudoDeDicto_when_rigid).

Scope notes: the dichotomy classifies situation-index construals under a single operator. Mixed towers (negation over a modal) correctly do not collapse — narrow readings under the modal remain available — and the individual skolem index carrying [Owu22]'s functional readings is beyond this fragment.

def Quantification.ChoiceFunction.SkolemCF.applyIntension {S : Type u_1} {E : Type u_2} (f : SkolemCF S E) (s : S) (P : Intensional.Intension S (E → Prop)) : E

Apply a skolemized CF at s to an intensional restrictor, evaluating both at the same index — [Owu22]'s f_s(P(s)) (entry (67), modulo currying; see the section docstring).

Equations

• f.applyIntension s P = f s (P s)

theorem Quantification.ChoiceFunction.SkolemCF.applyIntension_rigid {S : Type u_1} {E : Type u_2} (f : SkolemCF S E) (s : S) (N : E → Prop) : f.applyIntension s (Intensional.Intension.rigid N) = f.apply s N

On rigid restrictors, applyIntension is the extensional apply.

def Quantification.ChoiceFunction.SkolemCF.applyIntensionAt {S : Type u_1} {E : Type u_2} (f : SkolemCF S E) (status : Intensional.SitVarStatus.SitVarStatus) (sOp s₀ : S) (P : Intensional.Intension S (E → Prop)) : E

SitVarStatus-dispatched intensional application: the free construal anchors the CF and restrictor to the context situation s₀; the bound construal rides the local index sOp supplied by a scope-taking operator. The intensional generalization of evalAt.

Equations

• f.applyIntensionAt Intensional.SitVarStatus.SitVarStatus.free sOp s₀ P = f.applyIntension s₀ P
• f.applyIntensionAt Intensional.SitVarStatus.SitVarStatus.bound sOp s₀ P = f.applyIntension sOp P

theorem Quantification.ChoiceFunction.SkolemCF.evalAt_eq_applyIntensionAt {S : Type u_1} {E : Type u_2} (f : SkolemCF S E) (status : Intensional.SitVarStatus.SitVarStatus) (w₀ wBound : S) (N : E → Prop) : f.evalAt status w₀ wBound N = f.applyIntensionAt status wBound w₀ (Intensional.Intension.rigid N)

evalAt is applyIntensionAt on a rigid restrictor.

theorem Quantification.ChoiceFunction.bound_free_collapse {S : Type u_1} {E : Type u_2} {O : (S → Prop) → S → Prop} {s₀ : S} (hO : Intensional.IsExtensionalAt O s₀) (f : SkolemCF S E) (P : Intensional.Intension S (E → Prop)) (VP : E → S → Prop) : O (fun (s : S) => VP (f.applyIntensionAt Intensional.SitVarStatus.SitVarStatus.bound s s₀ P) s) s₀ ↔ O (fun (s : S) => VP (f.applyIntensionAt Intensional.SitVarStatus.SitVarStatus.free s s₀ P) s) s₀

Construal collapse: under any operator extensional at the matrix situation s₀, the bound and free construals of the situation pronoun are truth-conditionally indistinguishable — for any CF and any intensional restrictor. Instantiated at pointwise negation (Intensional.IsExtensionalAt.neg) this derives wide-scope-only under negation; see Studies/Zimmermann2026.

theorem Quantification.ChoiceFunction.bound_free_diverge_box : ∃ (S : Type) (E : Type) (R : Core.Logic.Modal.AccessRel S) (f : SkolemCF S E) (P : Intensional.Intension S (E → Prop)) (VP : E → S → Prop) (s₀ : S), Core.Logic.Modal.box R (fun (s : S) => VP (f.applyIntensionAt Intensional.SitVarStatus.SitVarStatus.bound s s₀ P) s) s₀ ∧ ¬Core.Logic.Modal.box R (fun (s : S) => VP (f.applyIntensionAt Intensional.SitVarStatus.SitVarStatus.free s s₀ P) s) s₀

Construal divergence: a situation quantifier (box) separates the bound and free construals — two situations, a restrictor whose extension varies, a CF tracking its index.

theorem Quantification.ChoiceFunction.box_not_extensionalAt : ∃ (S : Type) (R : Core.Logic.Modal.AccessRel S) (s₀ : S), ¬Intensional.IsExtensionalAt (Core.Logic.Modal.box R) s₀

box is not extensional: the operator side of the dichotomy is genuine.

Bridge to B&C existential semantics

The Reinhart 1997 vs B&C 1981 schism: indefinites can be analyzed as referential (CF, type e) or quantificational (some_sem, type ⟨⟨e,t⟩,⟨⟨e,t⟩,t⟩⟩).

The two analyses agree on the simple case (one-way bridge below) but diverge on island-escape and pseudo-de-dicto readings. The asymmetry is deliberately exposed, not collapsed: that visibility is the linglib thesis.

theorem Quantification.ChoiceFunction.cfIndefSem_implies_some_sem {α : Type u_1} (f : CF α) (hf : f.isCorrect) (N VP : α → Prop) (hN : ∃ (x : α), N x) : VP (cfIndefSem f N) → some_sem N VP

Forward bridge: a correct CF, applied to the noun property, witnesses the corresponding some_sem reading whenever the restrictor is non-empty. The CF-output f N is in N (by correctness) and satisfies VP (by hypothesis), so it witnesses ∃ x, N x ∧ VP x.

theorem Quantification.ChoiceFunction.correct_cfs_disagree_on_some_sem : ∃ (f₁ : CF Bool) (f₂ : CF Bool), f₁.isCorrect ∧ f₂.isCorrect ∧ ∃ (N : Bool → Prop) (VP : Bool → Prop), some_sem N VP ∧ VP (cfIndefSem f₁ N) ∧ ¬VP (cfIndefSem f₂ N)

Different correct CFs make different some_sem-predictions on the same noun/VP pair. The CF must commit in advance to a specific element; this commitment can disagree with the existential reading's witness.

Witness: domain Bool, with noun N = ⊤ (both inhabitants count) and VP = (· = true). The CF f₁ (prefer-true) hits the witness; the CF f₂ (prefer-false) does not. Both are correct.

This makes the framework asymmetry visible at the propositional level: some_sem is existence-of-witness; CF is commitment-to-witness, and multiple correct CFs commit differently. The deeper divergence — island-escape and pseudo-de-dicto under intensional operators — is out of scope here but motivated by the same structural gap.