Kratzer and Shimoyama (2002): Indeterminate Pronouns: The View from Japanese

This file formalizes the paper's Hamblin semantics for indeterminate pronouns and its application to German irgendein. Every expression denotes a set of alternatives; an indeterminate pronoun denotes a set of individuals, composition is pointwise functional application, and the alternatives expand until an operator, existential, universal, negative, or interrogative, closes them. Since closure returns a single proposition, alternatives are caught by the nearest operator, which is the paper's locality constraint on association. Determiner quantification is the special case in which the alternatives are individuals. Irgendein widens a domain-restricted indefinite to the whole extension of its noun, and modals are sensitive to the propositional alternatives in their scope; their truth conditions are weak, and the distribution requirement behind the free-choice effect, that every alternative be realised at some accessible world, is not entailed by them but derived as a conversational implicature from the reasons a speaker could have for widening, present under kann and muss and cancelled under negated possibility. The paper closes with the selectivity of Indo-European indeterminates, irgendein associating only with existential closure, and the Beck effects, in which an intervening operator blocks the in situ wh-phrase.

The paper's sentences with irgendein are acceptable exactly in the environments the fragment entry German.PolarityItems.irgendein lists (rows_irgendein). Under a negative operator selectivity decides: niemand and auf keinen Fall close their scope with [∃] and admit the item, while the inflectional negation nicht carries [Neg] and does not (rows_irgendein_selective). Strength does not decide it, since the licensing table licenses the item under the downward-entailing nicht (negation_licenses_irgendein). Haspelmath's map agrees: the environments the entry lists realize functions of his irgend- series, and inflectional negation realizes direct negation, which the series lacks (irgendein_haspelmath).

Implementation notes

Hamblin functional application is mathlib's Set.seq, and singleton denotations are {f}; the four sentential operators return singleton sets, as in the paper, so that closure is idle on an already closed set. The existential and universal operators are what the coordinators ka and mo denote on the set of alternatives (opExists_eq_denote_ka, opForall_eq_denote_mo), and on individual alternatives they give the readings of the indeterminate quantifiers in Fragments/Japanese/Determiners.lean (denote_image_eq_reading), an identification of ka and mo with the coordinators that the fragment makes and the paper does not. The modal semantics is stated for an accessibility relation on any type of worlds, and the free-choice computations are the paper's three tables with the derived implicature as a hypothesis. The Beck-effect paradigm and its scrambled counterpart are example rows, keyed by the intervener's interpretable feature, and so is the paradigm of irgendein, keyed by its licensing environment. Locators follow the 2002 manuscript, whose numbering the published chapter keeps.

References

• [KS17]
• [Ham73] — alternative semantics for questions
• [Has97] — the Latvian and Japanese series
• [KL93] — widening for a reason
• [Bec96] — intervention effects

Hamblin composition (§2, §3)

theorem KratzerShimoyama2002.seq_singleton {W : Type u_1} {E : Type u_2} (f : E → W → Prop) (A : Set E) : {f}.seq A = f '' A

A singleton set of functions applies pointwise as an image, as when the verb of dare nemutta introduces one alternative and the indeterminate a set of individuals.

def KratzerShimoyama2002.opExists {W : Type u_1} (A : Set (W → Prop)) : Set (W → Prop)

opExists A is existential closure, the single proposition true where some alternative is.

Equations

• KratzerShimoyama2002.opExists A = {fun (w : W) => ∃ p ∈ A, p w}

def KratzerShimoyama2002.opForall {W : Type u_1} (A : Set (W → Prop)) : Set (W → Prop)

opForall A is universal closure, the single proposition true where every alternative is.

Equations

• KratzerShimoyama2002.opForall A = {fun (w : W) => ∀ p ∈ A, p w}

def KratzerShimoyama2002.opNeg {W : Type u_1} (A : Set (W → Prop)) : Set (W → Prop)

opNeg A is negative closure, the single proposition true where no alternative is.

Equations

• KratzerShimoyama2002.opNeg A = {fun (w : W) => ∀ p ∈ A, ¬p w}

def KratzerShimoyama2002.opQ {W : Type u_1} (A : Set (W → Prop)) : Set (W → Prop)

The question operator returns the alternatives themselves.

Equations

• KratzerShimoyama2002.opQ A = A

theorem KratzerShimoyama2002.opNeg_eq {W : Type u_1} (A : Set (W → Prop)) : opNeg A = {fun (w : W) => ¬∃ p ∈ A, p w}

Negative closure is the negation of existential closure.

theorem KratzerShimoyama2002.opExists_singleton {W : Type u_1} (p : W → Prop) : opExists {p} = {p}

theorem KratzerShimoyama2002.opForall_singleton {W : Type u_1} (p : W → Prop) : opForall {p} = {p}

theorem KratzerShimoyama2002.opForall_opExists {W : Type u_1} (A : Set (W → Prop)) : opForall (opExists A) = opExists A

Alternatives are caught by the nearest operator (4), since a closed set has a single member and a higher operator finds nothing left to quantify over.

theorem KratzerShimoyama2002.opExists_opForall {W : Type u_1} (A : Set (W → Prop)) : opExists (opForall A) = opForall A

theorem KratzerShimoyama2002.opExists_image {W : Type u_1} {E : Type u_2} (P : E → W → Prop) (A : Set E) : opExists (P '' A) = {fun (w : W) => ∃ x ∈ A, P x w}

Determiner quantification is the special case with individual alternatives (§2), so that existential closure over the propositions a predicate yields from a set of individuals is the ordinary existential quantifier.

theorem KratzerShimoyama2002.opForall_image {W : Type u_1} {E : Type u_2} (P : E → W → Prop) (A : Set E) : opForall (P '' A) = {fun (w : W) => ∀ x ∈ A, P x w}

theorem KratzerShimoyama2002.opExists_eq_denote_ka {W : Type u_1} (A : Set (W → Prop)) : opExists A = {Japanese.Coordination.ka.denote A}

Existential closure is what the disjunctive ka denotes on the alternatives.

theorem KratzerShimoyama2002.opForall_eq_denote_mo {W : Type u_1} (A : Set (W → Prop)) : opForall A = {Japanese.Coordination.mo.denote A}

Universal closure is what the conjunctive mo denotes on the alternatives.

theorem KratzerShimoyama2002.opNeg_eq_denote {W : Type u_1} {c : Coordinator} (hc : c.role = Coordinator.Role.negative) (A : Set (W → Prop)) : opNeg A = {c.denote A}

Negative closure is what a negative coordinator denotes on the alternatives.

theorem KratzerShimoyama2002.denote_image_eq_reading {W : Type u_1} {E : Type u_2} [Fintype E] (q : IndeterminateQuantifier) (P : E → W → Prop) (A : Set E) : q.particle.denote (P '' A) = fun (w : W) => q.reading E (fun (x : E) => x ∈ A) fun (x : E) => P x w

The coordination an indeterminate's particle applies to the propositions a predicate yields from a set of individuals is, at each world, the indeterminate quantifier's reading, IndeterminateQuantifier.reading, so the determiner readings are the special case of the paper's closure with individual alternatives (§2).

Dare(-ga) nemutta (§2)

def KratzerShimoyama2002.dare {W : Type u_1} {E : Type u_2} (human : E → W → Prop) (w : W) : Set E

dare human w is dare 'who', the humans at the evaluation world.

Equations

• KratzerShimoyama2002.dare human w = {x : E | human x w}

def KratzerShimoyama2002.nemutta {W : Type u_1} {E : Type u_2} (slept : E → W → Prop) : Set (E → W → Prop)

nemutta slept is nemutta 'slept', a single alternative.

Equations

• KratzerShimoyama2002.nemutta slept = {slept}

theorem KratzerShimoyama2002.dare_nemutta {W : Type u_1} {E : Type u_2} (human slept : E → W → Prop) (w : W) : (nemutta slept).seq (dare human w) = {p : W → Prop | ∃ (x : E), human x w ∧ p = slept x}

Dare nemutta denotes a proposition for each human.

theorem KratzerShimoyama2002.dare_ka {W : Type u_1} {E : Type u_2} (human slept : E → W → Prop) (w : W) : opExists ((nemutta slept).seq (dare human w)) = {fun (w' : W) => ∃ (x : E), human x w ∧ slept x w'}

Dare-ka nemutta says that someone slept.

theorem KratzerShimoyama2002.dare_mo {W : Type u_1} {E : Type u_2} (human slept : E → W → Prop) (w : W) : opForall ((nemutta slept).seq (dare human w)) = {fun (w' : W) => ∀ (x : E), human x w → slept x w'}

Dare-mo nemutta says that everyone slept.

Widening and modals (§7)

def KratzerShimoyama2002.ein {E : Type u_2} (man : E → Prop) (D : Set E) : Set E

ein man D is ein Mann with the contextual domain D, a subset of the men.

Equations

• KratzerShimoyama2002.ein man D = {x : E | man x ∧ x ∈ D}

def KratzerShimoyama2002.irgend {E : Type u_2} (den : Set E → Set E) : Set E

irgend- widens over every value of the domain variable.

Equations

• KratzerShimoyama2002.irgend den = ⋃ (D : Set E), den D

theorem KratzerShimoyama2002.irgend_ein {E : Type u_2} (man : E → Prop) : irgend (ein man) = {x : E | man x}

irgendein Mann denotes all the men.

theorem KratzerShimoyama2002.subset_irgend {E : Type u_2} (den : Set E → Set E) (D : Set E) : den D ⊆ irgend den

The restricted indefinite is included in its widening.

def KratzerShimoyama2002.kann {W : Type u_1} (R : SetRel W W) (A : Set (W → Prop)) : Set (W → Prop)

kann R A is kann over the propositional alternatives A, the possibility that some alternative holds.

Equations

• KratzerShimoyama2002.kann R A = {ModalLogic.Diamond R fun (w : W) => ∃ p ∈ A, p w}

def KratzerShimoyama2002.muss {W : Type u_1} (R : SetRel W W) (A : Set (W → Prop)) : Set (W → Prop)

muss R A is muss over the propositional alternatives A, the necessity that some alternative holds.

Equations

• KratzerShimoyama2002.muss R A = {ModalLogic.Box R fun (w : W) => ∃ p ∈ A, p w}

def KratzerShimoyama2002.distribution {W : Type u_1} (R : SetRel W W) (A : Set (W → Prop)) (w : W) : Prop

distribution R A w is the distribution requirement, that every alternative is possible.

Equations

• KratzerShimoyama2002.distribution R A w = ∀ p ∈ A, ModalLogic.Diamond R p w

theorem KratzerShimoyama2002.kann_singleton {W : Type u_1} (R : SetRel W W) (p : W → Prop) : kann R {p} = {ModalLogic.Diamond R p}

On a single alternative the modals are the Kripke modals.

theorem KratzerShimoyama2002.muss_singleton {W : Type u_1} (R : SetRel W W) (p : W → Prop) : muss R {p} = {ModalLogic.Box R p}

theorem KratzerShimoyama2002.not_distribution_of_muss : ∃ (R : SetRel Bool Bool) (A : Set (Bool → Prop)) (w : Bool), (∀ q ∈ muss R A, q w) ∧ ¬distribution R A w

The distribution requirement is not entailed by muss (§6). With two alternatives and a single accessible world verifying one of them, necessity holds and distribution fails.

The free-choice implicature (§8)

Widening is for a reason: strengthening, avoiding a false claim, or avoiding a false exhaustivity inference. For (16), had the speaker chosen the narrower set with one alternative, the exhaustivity inference would have excluded the other; the only reason to widen is that this inference is false, so each alternative's possibility implies the other's. The same reasoning yields the implicature of (17); under the negated possibility of (18) every such reason is already entailed by what was said, and the implicature is cancelled.

theorem KratzerShimoyama2002.kann_pair {W : Type u_1} (R : SetRel W W) (A B : W → Prop) (w : W) : (∀ q ∈ kann R {A, B}, q w) ↔ ModalLogic.Diamond R (fun (w : W) => A w ∨ B w) w

Kann over the two alternatives is the possibility of their disjunction.

theorem KratzerShimoyama2002.muss_pair {W : Type u_1} (R : SetRel W W) (A B : W → Prop) (w : W) : (∀ q ∈ muss R {A, B}, q w) ↔ ModalLogic.Box R (fun (w : W) => A w ∨ B w) w

Muss over the two alternatives is the necessity of their disjunction.

theorem KratzerShimoyama2002.total_kann {W : Type u_1} (R : SetRel W W) (A B : W → Prop) (w : W) (hT : ModalLogic.Diamond R (fun (w : W) => A w ∨ B w) w) (hI : ModalLogic.Diamond R A w ↔ ModalLogic.Diamond R B w) : ModalLogic.Diamond R A w ∧ ModalLogic.Diamond R B w

In (16) the truth-conditional content with the implicature yields free choice.

theorem KratzerShimoyama2002.total_muss {W : Type u_1} (R : SetRel W W) (A B : W → Prop) (w : W) (hT : ModalLogic.Box R (fun (w : W) => A w ∨ B w) w) (hI : ModalLogic.Box R A w ↔ ModalLogic.Box R B w) (hser : ∃ (w' : W), (w, w') ∈ R) : ModalLogic.Diamond R A w ∧ ModalLogic.Diamond R B w

In (17) the total meaning implies both possibilities once some world is accessible.

theorem KratzerShimoyama2002.total_neg_kann {W : Type u_1} (R : SetRel W W) (A B : W → Prop) (w : W) (hT : ¬ModalLogic.Diamond R (fun (w : W) => A w ∨ B w) w) : ¬ModalLogic.Diamond R A w ∧ ¬ModalLogic.Diamond R B w

In (18), under negated possibility, every reason for widening is already entailed, so no strengthening is available.

Selectivity and intervention (§9)

theorem KratzerShimoyama2002.japanese_same_base : Japanese.Determiners.dare_ka.indeterminate = Japanese.Determiners.dare_mo.indeterminate ∧ Semantics.Denotes.denote Japanese.Determiners.dare_ka ≠ Semantics.Denotes.denote Japanese.Determiners.dare_mo

Japanese indeterminates do not change shape (§9). Dare-ka and dare-mo share their indeterminate and differ in their readings, which their particles' coordinations supply.

theorem KratzerShimoyama2002.latvian_selective : List.Pairwise (fun (x1 x2 : Haspelmath1997.Series) => Disjoint x1.functions x2.functions) Haspelmath1997.latvian

The Latvian series are selective (§1, §9). In [Has97]'s figure the kaut-series is existential, the ne-series confined to the direct scope of negation and the jeb-series to indirect negation, comparatives and free choice, so that no function of the map is served by two series.

theorem KratzerShimoyama2002.japanese_series_disjoint : List.Pairwise (fun (x1 x2 : Haspelmath1997.Series) => Disjoint x1.functions x2.functions) Haspelmath1997.japanese

The Japanese series of [Has97] are as disjoint as the Latvian ones, so the contrast the paper draws between the two systems is one of shape and not of distribution, the Latvian marker sitting on the pronoun, while the Japanese indeterminate keeps its shape under each particle (japanese_same_base).

theorem KratzerShimoyama2002.rows_beck (r : Datum) : r ∈ Examples.all → (r.feature? "order").isSome = true → (r.judgment = Judgment.ungrammatical ↔ r.feature? "order" = some "intervener-first" ∧ r.feature? "feature" ≠ some "none")

In the Beck effects (23) and their scrambled counterparts (24), a multiple question with the second wh-phrase in situ is ungrammatical iff an operator bearing an interpretable feature, inflectional negation or the existential closure of a quantifier, intervenes between the wh-phrase and the complementiser.

The distribution of irgendein (§6, §9)

def KratzerShimoyama2002.contextOf? (r : Datum) : Option PolarityItem.LicensingContext

contextOf? r is the licensing environment a row of the irgendein paradigm names.

Equations

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

theorem KratzerShimoyama2002.rows_irgendein (r : Datum) : r ∈ Examples.all → ∀ c ∈ contextOf? r, r.judgment = Judgment.acceptable ↔ c ∈ German.PolarityItems.irgendein.licensingContexts

A sentence with irgendein is acceptable exactly in the environments the fragment entry lists, (12), (13), (16)–(18), (21) and (22).

theorem KratzerShimoyama2002.rows_irgendein_selective (r : Datum) : r ∈ Examples.all → (contextOf? r).isSome = true → ∀ f ∈ r.feature? "feature", r.judgment = Judgment.acceptable ↔ f = "exists"

Under a negative operator irgendein is acceptable exactly when the operator closes its scope with [∃] and not with [Neg], so under niemand and auf keinen Fall and not under nicht, (12), (18) and (21).

theorem KratzerShimoyama2002.negation_licenses_irgendein : PolarityItem.LicensingContext.negation.licenser.Licenses German.PolarityItems.irgendein ∧ Examples.ex21.judgment = Judgment.ungrammatical

The licensing theory licenses irgendein under inflectional negation, which is downward entailing, and (21) is ungrammatical, so strength does not exclude the item there and selectivity does.

theorem KratzerShimoyama2002.irgendein_haspelmath (s : Haspelmath1997.Series) : s ∈ Haspelmath1997.german → s.toSeries = German.Indefinites.irgendSeries → (∀ c ∈ German.PolarityItems.irgendein.licensingContexts, ∀ f ∈ c.haspelmath, f ∈ s.functions) ∧ ∀ f ∈ PolarityItem.LicensingContext.negation.haspelmath, f ∉ s.functions

Haspelmath's map agrees with the paper. Every environment the entry lists realizes a function of the irgend- series, and inflectional negation realizes direct negation, which the series lacks.