Choice functions #
A choice function picks a member of every nonempty property. For Reinhart and for Winter an
indefinite noun phrase denotes the value of such a function rather than an existential
quantifier, and it scopes where the function variable is bound rather than where a quantifier
would raise to. Kratzer gives the function implicit arguments, skolem indices that are bound like
pronouns, so a skolemized choice function is a family S → ChoiceFunction E; Mirrazi adds a world
argument that an intensional operator can bind, and Owusu feeds the same situation to the
function and to the restrictor. Closing the function variable existentially gives the existential
reading, and closing it when its index or its restrictor varies with a bound variable gives the
reading on which the indefinite scopes below the binder.
Main definitions #
Reference.ChoiceFunction: the choice functions over a domain, as functions from properties to individuals.
Main results #
ChoiceFunction.some_of_apply,ChoiceFunction.forall_apply_iff_some_iff: a choice function witnesses the existential reading, and agrees with it on every predicate only when the restrictor has a single member.ChoiceFunction.exists_apply_iff_some,ChoiceFunction.forall_apply_iff_every: quantifying over choice functions gives the existential and universal readings on a nonempty restrictor.ChoiceFunction.exists_forall_apply_iff: a choice function whose restrictor contains a bound variable takes no scope relative to the binder.ChoiceFunction.exists_forall_apply_iff_of_injective,ChoiceFunction.exists_pi_apply_iff: with distinct restrictors for distinct values of the bound variable, or with the bound variable as the skolem index, closing the function above the binder gives the reading with the existential below it.
References #
A choice function sends every nonempty property to one of its members.
- toFun : (E → Prop) → E
The individual picked from a property.
The pick of a nonempty property satisfies it.
Instances For
Equations
- Reference.ChoiceFunction.instFunLikeForallProp = { coe := Reference.ChoiceFunction.toFun, coe_injective := ⋯ }
The pick of a nonempty property satisfies it.
Hilbert's ε is a choice function.
Equations
- Reference.ChoiceFunction.epsilon = { toFun := Classical.epsilon, apply_of_exists' := ⋯ }
Instances For
Every member of a property is the pick of some choice function.
The existential reading #
A choice function witnesses the existential reading GQ.some on a nonempty restrictor, but the
two analyses are not equivalent: the existential reading asserts the existence of a witness, the
choice function commits to one, and distinct choice functions commit differently.
A choice function whose pick satisfies the predicate witnesses the existential reading.
A choice function agrees with the existential reading on every predicate exactly when its pick is the only member of the restrictor.
Existential quantification over choice functions is the existential reading.
Universal quantification over choice functions is the universal reading, on a nonempty restrictor.
On an empty restrictor a choice function is unconstrained, so universal quantification over choice functions ranges over the whole domain, where the universal reading is vacuous.
Scope relative to a binder #
A choice function applied to a restrictor that contains a bound variable takes no scope relative to the binder. Since the restrictor already varies with the variable, one choice function can be assembled from the pointwise choices.
When distinct values of a bound variable give distinct nonempty restrictors, closing a choice function above the binder gives the reading with the existential below it, even if the predicate also contains the variable.
Closing a skolemized choice function above a binder of its index gives the reading with the existential below the binder.