Choice Functions for Indefinite Determiners

@cite{reinhart-1997} @cite{kratzer-1998} @cite{winter-1997}

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

@cite{mirrazi-2024} 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 Core.SitVarStatus.

Application to African Languages

@cite{zimmermann-2008} analyses Hausa wani/wata as a standard ∃-quantifier, predicting flexible scope via QR.

@cite{owusu-2022} analyses Akan bí as a skolemized choice function with a situation parameter (SkolemCF), explaining why bí takes obligatory wide scope under negation: the choice function is evaluated relative to the resource situation, which negation cannot shift.

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

A choice function selects an individual from a property. @cite{reinhart-1997}: type ⟨⟨e,t⟩, e⟩.

Equations

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

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

• Semantics.Quantification.ChoiceFunction.cfIndefSem f nounProp = f nounProp

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

A situation-indexed (skolemized) choice function.

@cite{kratzer-1998}: the CF is parameterized by a situation s, making the selected individual depend on the evaluation situation.

⟦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

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

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

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

@cite{reinhart-1997}: 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). @cite{zimmermann-2026} §3.3.

• existential : IndefType
• choiceFunction : IndefType

@[implicit_reducible]

instance Semantics.Quantification.ChoiceFunction.instDecidableEqIndefType : DecidableEq IndefType

Equations

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

@[implicit_reducible]

instance Semantics.Quantification.ChoiceFunction.instReprIndefType : Repr IndefType

Equations

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

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

Equations

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

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

Whether wide pseudo-scope de dicto readings are predicted.

@cite{mirrazi-2024} §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) ✗. @cite{schwarz-2012}.

Equations

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

theorem Semantics.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)

When the situation variable is bound to the resource situation (not shifted by an intensional operator), the CF yields wide scope.

This is the key structural property that distinguishes CF-based indefinites (Akan bí) from ∃-based indefinites (Hausa wani): negation is not an intensional operator, so it cannot shift the situation variable, forcing wide scope.

⟦¬[bí N VP]⟧ = ¬VP(f_{s₀}(N)) — wide scope: ∃ > ¬ ⟦¬[wani N VP]⟧ = ¬∃x[N(x) ∧ VP(x)] — narrow scope: ¬ > ∃

theorem Semantics.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.

def Semantics.Quantification.ChoiceFunction.SkolemCF.evalAt {S : Type u_1} {E : Type u_2} (f : SkolemCF S E) (status : Core.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

@cite{mirrazi-2024} §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 Core.SitVarStatus.SitVarStatus.free w₀ wBound nounProp = f w₀ nounProp
• f.evalAt Core.SitVarStatus.SitVarStatus.bound w₀ wBound nounProp = f wBound nounProp

theorem Semantics.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 Core.SitVarStatus.SitVarStatus.bound w₁ w₂ P ≠ f.evalAt Core.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.

@cite{mirrazi-2024} 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'.