Kratzer & Shimoyama (2002): Indeterminate Pronouns

@cite{kratzer-shimoyama-2002}

"Indeterminate Pronouns: The View from Japanese." In C. Lee et al. (eds.), Contrastiveness in Information Structure, Alternatives and Scalar Implicatures, Studies in Natural Language and Linguistic Theory 91, 123-143.

Core Thesis

Hamblin alternative semantics, originally designed for questions, is the right architecture for all quantification. Indeterminate pronouns (Japanese dare, nani, doko...) denote sets of individual alternatives that expand pointwise via functional application until caught by an operator (∃, ∀, Neg, Q). Quantification is operator selection, not DP movement.

Formalized Contributions

1. Hamblin operators (§2): The four sentential operators over propositional alternative sets.
2. Pointwise FA = Set applicative (§3): K&S's Hamblin FA is exactly the set applicative from @cite{charlow-2020}, already formalized in Applicative.lean.
3. GQ as special case (§2): Determiner quantification falls out when alternatives are individuals — [∃]({P(x) : x ∈ A}) ↔ ∃x∈A, P(x).
4. Singleton collapse: When alternatives are a singleton (ordinary semantics), Hamblin modals reduce to standard Kripke modals.
5. Modal–indefinite interaction (§7): Possibility/necessity modals are sensitive to Hamblin alternatives in their scope.
6. Distribution requirement as implicature (§6, §8): The free choice effect is derived via Gricean reasoning, not semantic entailment.
7. End-to-end FC derivation: Hamblin T-content + implicature = FC.
8. Selectivity (§9): Non-selective (Japanese) vs. selective (Indo-European) indeterminate systems, with Beck effect data.
9. Cross-linguistic paradigm (§1): Latvian indeterminate series.

Integration Points

• §3 Hamblin FA bridges to setAp (Composition/Applicative.lean)
• Singleton collapse bridges Hamblin modals to Kripke semantics
• §8 free choice bridges to free_choice_forward (Exhaustification/FreeChoice.lean)
• Fragment data bridges to Japanese/Determiners.lean, German/ModalIndefinites.lean, and Latvian/IndeterminatePronouns.lean

§2-3: Hamblin Interpretation System

In a Hamblin semantics, all expressions denote sets of alternatives. Most lexical items denote singleton sets; indeterminate pronouns denote sets of individuals. Composition is pointwise functional application.

@[reducible, inline]

abbrev Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.HamblinDen (α : Type) : Type

A Hamblin denotation is a set of alternatives of type α. This is exactly the carrier of @cite{charlow-2020}'s set monad.

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.HamblinDen α = (α → Prop)

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.hamblinFA {A B : Type} (funSet : HamblinDen (A → B)) (argSet : HamblinDen A) : HamblinDen B

Hamblin Functional Application (§3): pointwise application of a set of functions to a set of arguments.

⟦α⟧ = {a ∈ Dσ : ∃b ∈ ⟦β⟧ ∃c ∈ ⟦γ⟧, a = c(b)}

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.hamblinFA funSet argSet b = ∃ (f : A → B), funSet f ∧ ∃ (x : A), argSet x ∧ f x = b

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.hamblinFA_eq_setAp {A B : Type} (m : HamblinDen (A → B)) (n : HamblinDen A) : hamblinFA m n = Semantics.Composition.Applicative.setAp m n

Bridge: Hamblin FA = the set applicative from Applicative.lean.

§2: Sentential Operators over Propositional Alternatives

The alternatives created by indeterminate phrases expand until caught by an operator. Where A is a set of propositions (p. 126-127):

• [∃](A) — true iff some proposition in A is true
• [∀](A) — true iff every proposition in A is true
• [Neg](A) — true iff no proposition in A is true
• [Q](A) — A itself (the Hamblin question denotation)

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.opExists {W : Type} (A : HamblinDen (W → Prop)) : W → Prop

[∃](A): existential closure over propositional alternatives.

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.opExists A w = ∃ (p : W → Prop), A p ∧ p w

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.opForall {W : Type} (A : HamblinDen (W → Prop)) : W → Prop

[∀](A): universal closure over propositional alternatives.

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.opForall A w = ∀ (p : W → Prop), A p → p w

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.opNeg {W : Type} (A : HamblinDen (W → Prop)) : W → Prop

[Neg](A): negative closure over propositional alternatives.

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.opNeg A w = ∀ (p : W → Prop), A p → ¬p w

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.opQ {W : Type} (A : HamblinDen (W → Prop)) : HamblinDen (W → Prop)

[Q](A): question operator — identity on propositional alternatives.

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.opQ A = A

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.opNeg_iff_not_opExists {W : Type} (A : HamblinDen (W → Prop)) (w : W) : opNeg A w ↔ ¬opExists A w

Neg is the pointwise negation of ∃: [Neg](A)(w) ↔ ¬[∃](A)(w).

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.opForall_entails_opExists {W : Type} (A : HamblinDen (W → Prop)) (hne : ∃ (p : W → Prop), A p) (w : W) (h : opForall A w) : opExists A w

∀ entails ∃ on non-empty alternative sets.

inductive Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.QuantOperator : Type

Map from operator tags to their semantic implementations.

• exists_ : QuantOperator
• forall_ : QuantOperator
• neg : QuantOperator
• question : QuantOperator

instance Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instDecidableEqQuantOperator : DecidableEq QuantOperator

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instDecidableEqQuantOperator x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instBEqQuantOperator : BEq QuantOperator

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instBEqQuantOperator = { beq := Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instBEqQuantOperator.beq }

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instBEqQuantOperator.beq : QuantOperator → QuantOperator → Bool

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instBEqQuantOperator.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instReprQuantOperator : Repr QuantOperator

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instReprQuantOperator = { reprPrec := Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instReprQuantOperator.repr }

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instReprQuantOperator.repr : QuantOperator → ℕ → Std.Format

Equations

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

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.QuantOperator.applyProp {W : Type} (op : QuantOperator) (A : HamblinDen (W → Prop)) : Option (W → Prop)

Semantic interpretation of a propositional quantificational operator. Returns none for .question, which produces an alternative set rather than a proposition.

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.QuantOperator.exists_.applyProp A = some (Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.opExists A)
• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.QuantOperator.forall_.applyProp A = some (Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.opForall A)
• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.QuantOperator.neg.applyProp A = some (Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.opNeg A)
• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.QuantOperator.question.applyProp A = none

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.question_returns_alternatives {W : Type} (A : HamblinDen (W → Prop)) : QuantOperator.question.applyProp A = none ∧ opQ A = A

The question operator returns the alternative set unchanged: [Q](A) = A. This is distinct from the propositional operators because it does not collapse alternatives to a truth value.

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.opExists_gq_special_case {E W : Type} (A : HamblinDen E) (P : E → W → Prop) (w : W) : opExists (fun (p : W → Prop) => ∃ (x : E), A x ∧ p = P x) w ↔ ∃ (x : E), A x ∧ P x w

Determiner quantification as special case (p. 126): "Determiner quantification falls out as a special case, the case where the alternatives are individuals."

When an indeterminate denotes a set of individuals A and a predicate lifts each individual to a proposition, sentential [∃] over the resulting propositional alternatives equals the standard GQ existential: [∃]({P(x) : x ∈ A})(w) ↔ ∃ x ∈ A, P(x)(w).

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.opForall_gq_special_case {E W : Type} (A : HamblinDen E) (P : E → W → Prop) (w : W) : opForall (fun (p : W → Prop) => ∃ (x : E), A x ∧ p = P x) w ↔ ∀ (x : E), A x → P x w

Universal counterpart: [∀] over individual alternatives = standard ∀. [∀]({P(x) : x ∈ A})(w) ↔ ∀ x ∈ A, P(x)(w).

Compositional Derivation of dare(-ga) nemutta

Japanese indeterminate pronouns denote sets of individuals. Composed with a predicate via pointwise FA, they produce propositional alternative sets. An operator then closes the set (p. 126):

• ⟦dare⟧^{w,g} = {x: human(x)(w)}
• ⟦nemutta⟧^{w,g} = {λxλw'. slept(x)(w')} (singleton)
• ⟦dare nemutta⟧^{w,g} = {p: ∃x[human(x)(w) & p = λw'. slept(x)(w')]}

We simplify by working extensionally (dropping the world parameter on the restrictor), which is faithful for the core point that operator selection = quantification.

inductive Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.Person : Type

• a : Person
• b : Person
• c : Person

instance Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instDecidableEqPerson : DecidableEq Person

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instDecidableEqPerson x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instBEqPerson.beq : Person → Person → Bool

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instBEqPerson.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instBEqPerson : BEq Person

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instBEqPerson = { beq := Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instBEqPerson.beq }

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instReprPerson.repr : Person → ℕ → Std.Format

Equations

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

instance Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instReprPerson : Repr Person

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instReprPerson = { reprPrec := Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instReprPerson.repr }

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.dare : HamblinDen Person

⟦dare⟧ = the set of all humans (extensional simplification).

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.dare x✝ = True

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.sleptPred (slept : Person → Prop) : HamblinDen (Person → Prop)

⟦nemutta⟧ = singleton set containing the sleep predicate.

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.sleptPred slept = Semantics.Composition.SetMonad.eta slept

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.dareNemutta (slept : Person → Prop) : HamblinDen Prop

⟦dare nemutta⟧ = {slept(a), slept(b), slept(c)} via Hamblin FA.

Equations

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

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.dare_ka_derivation (slept : Person → Prop) : (∃ (p : Prop), dareNemutta slept p ∧ p) ↔ ∃ (x : Person), slept x

dare-ka nemutta = [∃]({slept(a), slept(b), slept(c)}) = ∃x.slept(x)

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.dare_mo_derivation (slept : Person → Prop) : (∀ (p : Prop), dareNemutta slept p → p) ↔ ∀ (x : Person), slept x

dare-mo nemutta = [∀]({slept(a), slept(b), slept(c)}) = ∀x.slept(x)

§7: Modals over Hamblin Alternative Sets

The key insight: modals can be sensitive to the propositional alternatives introduced by indeterminate phrases in their scope (p. 132-133).

Possibility/necessity modals over an alternative set A:

⟦kann α⟧(w) = ∃w'[R(w,w') ∧ ∃p[p ∈ A ∧ p(w')]]
⟦muss α⟧(w) = ∀w'[R(w,w') → ∃p[p ∈ A ∧ p(w')]]

The distribution requirement (to be derived as implicature in §8):

∀p[p ∈ A → ∃w'[R(w,w') ∧ p(w')]]

distributes alternatives over accessible worlds.

Note: We use Prop-valued accessibility here (rather than the Bool-valued Core.ModalLogic.AccessRel) to stay in Prop throughout the Hamblin semantics. The singleton collapse theorem below shows these Hamblin modals reduce to standard Kripke modals when the alternative set is a singleton.

@[reducible, inline]

abbrev Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.HamblinAccessRel (W : Type) : Type

Prop-valued accessibility relation for Hamblin modal semantics. Named distinctly from Core.ModalLogic.AccessRel (which is Bool-valued) to avoid shadowing.

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.HamblinAccessRel W = (W → W → Prop)

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.hamblinPoss {W : Type} (R : HamblinAccessRel W) (A : HamblinDen (W → Prop)) (w : W) : Prop

Possibility modal over Hamblin alternatives (§7, p. 133): True at w iff some accessible world satisfies some alternative.

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.hamblinPoss R A w = ∃ (w' : W), R w w' ∧ ∃ (p : W → Prop), A p ∧ p w'

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.hamblinNec {W : Type} (R : HamblinAccessRel W) (A : HamblinDen (W → Prop)) (w : W) : Prop

Necessity modal over Hamblin alternatives (§7, p. 133): True at w iff every accessible world satisfies some alternative.

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.hamblinNec R A w = ∀ (w' : W), R w w' → ∃ (p : W → Prop), A p ∧ p w'

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.distribReq {W : Type} (R : HamblinAccessRel W) (A : HamblinDen (W → Prop)) (w : W) : Prop

The distribution requirement (§7, p. 133): for every alternative p in A, there exists an accessible world where p is true.

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.distribReq R A w = ∀ (p : W → Prop), A p → ∃ (w' : W), R w w' ∧ p w'

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.hamblinPoss_singleton {W : Type} (R : HamblinAccessRel W) (p : W → Prop) (w : W) : hamblinPoss R (Semantics.Composition.SetMonad.eta p) w ↔ ∃ (w' : W), R w w' ∧ p w'

Singleton collapse: when the alternative set is a singleton {p}, Hamblin possibility reduces to standard Kripke possibility. This is the paper's core architectural claim: ordinary semantics is the special case where all denotations are singletons.

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.hamblinNec_singleton {W : Type} (R : HamblinAccessRel W) (p : W → Prop) (w : W) : hamblinNec R (Semantics.Composition.SetMonad.eta p) w ↔ ∀ (w' : W), R w w' → p w'

Singleton collapse for necessity: when alternatives are a singleton, Hamblin necessity reduces to standard Kripke necessity.

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.hamblinNec_entails_hamblinPoss {W : Type} (R : HamblinAccessRel W) (A : HamblinDen (W → Prop)) (w : W) (h : hamblinNec R A w) (hacc : ∃ (w' : W), R w w') : hamblinPoss R A w

Necessity entails possibility (when some accessible world exists).

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.distrib_not_entailed_by_nec : ∃ (R : HamblinAccessRel Bool) (A : HamblinDen (Bool → Prop)) (w : Bool), hamblinNec R A w ∧ ¬distribReq R A w

The distribution requirement is NOT entailed by necessity (§6, p. 131). Necessity only requires some alternative per world, not that every alternative is witnessed. The distribution requirement is an implicature.

Countermodel: R reflexive-only, A = {p₁, p₂} where p₁ holds at true, p₂ holds at false. From w = true, only true is accessible: necessity holds (p₁ witnesses true) but distribution fails (p₂ is unwitnessed).

§7: Domain Widening

ein Mann denotes a contextually restricted subset of men (Schwarzschild 2000: singleton indefinites). irgendein Mann widens to the full set (p. 132).

This is the same mechanism as contextual domain restriction in DomainRestriction.lean: ein selects from a contextually restricted domain C ∩ P, while irgend- removes the restriction.

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.simpleIndef {E : Type} (D : Set E) (P : E → Prop) : Set E

A simple indefinite selects from a contextually restricted subset.

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.simpleIndef D P = {x : E | x ∈ D ∧ P x}

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.irgendIndef {E : Type} (P : E → Prop) : Set E

An irgend- indefinite widens to the full predicate extension.

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.irgendIndef P = {x : E | P x}

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.simple_entails_widened {E : Type} (D : Set E) (P Q : E → Prop) : (∃ x ∈ simpleIndef D P, Q x) → ∃ x ∈ irgendIndef P, Q x

Widening weakens existentials: restricted entails widened.

§6 & §8: Pragmatic Derivation of the Free Choice Implicature

§6 establishes that the distribution requirement is a conversational implicature: cancelable (ex. 11), disappears in DE contexts (ex. 12, 14).

§8 derives it via Gricean reasoning about why the speaker widened. Widening could serve: (a) strengthening, (b) avoiding a false claim, (c) avoiding a false exhaustivity inference (p. 134).

Three cases over alternatives {A, B}:

(16) Possibility: Du kannst dir irgendeins leihen

• T-content: ◇(A ∨ B)
• Implicature: ◇A ↔ ◇B
• Total: ◇A ∧ ◇B

(17) Necessity: Du musst dir irgendeins leihen

• T-content: □(A ∨ B)
• Implicature: □A ↔ □B
• Total: □(A ∨ B) ∧ ◇A ∧ ◇B

(18) Negated possibility: auf keinen Fall

• T-content: ¬◇(A ∨ B)
• No implicature: canceled (widening adds nothing in DE context)

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.fc_possibility (pA pB : Prop) (h_tcontent : pA ∨ pB) (h_implic : pA ↔ pB) : pA ∧ pB

(16) Possibility: T-content + implicature → FC. ◇(A ∨ B) with ◇A ↔ ◇B yields ◇A ∧ ◇B.

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.fc_necessity_total (nAB pA pB : Prop) (h_nAB : nAB) (h_nec_to_poss : nAB → pA ∨ pB) (h_poss_implic : pA ↔ pB) : nAB ∧ pA ∧ pB

(17) Necessity total meaning (p. 135). □(A∨B) → ◇(A∨B) → ◇A ∨ ◇B, combined with ◇A↔◇B, gives □(A∨B) ∧ ◇A ∧ ◇B.

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.fc_negated_no_implicature (pA pB : Prop) (h_neg : ¬(pA ∨ pB)) : ¬pA ∧ ¬pB

(18) Negated possibility: implicature canceled. ¬◇(A ∨ B) implies ¬◇A ∧ ¬◇B. Widening adds nothing.

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.fc_end_to_end_possibility {W : Type} (R : HamblinAccessRel W) (p q : W → Prop) (w : W) (h_tcontent : hamblinPoss R (fun (r : W → Prop) => r = p ∨ r = q) w) (h_implic : (∃ (w' : W), R w w' ∧ p w') ↔ ∃ (w' : W), R w w' ∧ q w') : (∃ (w' : W), R w w' ∧ p w') ∧ ∃ (w' : W), R w w' ∧ q w'

End-to-end FC derivation for (16): Given two propositional alternatives under a possibility modal, the T-content is exactly hamblinPoss, and applying the biconditional implicature yields FC.

This connects the modal semantics (§7) to the pragmatic derivation (§8) in a single theorem.

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.pragmatic_agrees_with_grammatical {W : Type} (a : Exhaustification.FreeChoice.FCAltSet W) (h : a.exh2) : a.freeChoice

Bridge to @cite{chierchia-2013}. K&S's pragmatic derivation (Gricean reasoning) and Chierchia's grammatical derivation (double exhaustification) both yield ◇A ∧ ◇B. Different mechanisms, same empirical prediction.

§9: Non-Selective vs. Selective Indeterminate Systems

Japanese: non-selective — same base (dare) + different particles (ka → ∃, mo → ∀, demo → FC). Base does not change shape.

Indo-European: selective — irgendein associates only with [∃], not [∀], [Neg], or [Q]. Explained via uninterpretable features (p. 138): selective indeterminates carry uninterpretable [∃] that must be checked against an interpretable counterpart via feature movement.

Beck Effects (§9, p. 139)

When feature movement of uninterpretable [∃] is blocked by an intervening scope-bearing element, ungrammaticality results:

• (23a) *Was hat sie nicht WEM gezeigt? — blocked by nicht ([Neg])
• (23b) *Was hat sie nie WEM gezeigt? — blocked by nie
• (23c) *Was hat niemand WEM gezeigt? — blocked by niemand
• (23d) *Was hat fast jeder WEM gezeigt? — blocked by fast jeder
• (23e) *Was hat (irgend)jemand WEM gezeigt? — blocked by jemand
• (23f) Was hat der Hans WEM gezeigt? — OK (definite: no scope feature)
• (23g) Was hat sie damals WEM gezeigt? — OK (adverb: no scope feature)

structure Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.IndeterminateParadigm : Type

An indeterminate pronoun paradigm: which operators it associates with, and whether its morphology changes per operator.

• language : String
• base : String
• associatesWith : List QuantOperator
• morphologicallyMarked : Bool

instance Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instReprIndeterminateParadigm : Repr IndeterminateParadigm

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instReprIndeterminateParadigm = { reprPrec := Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instReprIndeterminateParadigm.repr }

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instReprIndeterminateParadigm.repr : IndeterminateParadigm → ℕ → Std.Format

Equations

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

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.IndeterminateParadigm.isNonSelective (p : IndeterminateParadigm) : Bool

Equations

• p.isNonSelective = decide (p.associatesWith.length ≥ 3)

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.IndeterminateParadigm.isSelective (p : IndeterminateParadigm) : Bool

Equations

• p.isSelective = decide (p.associatesWith.length ≤ 2)

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.japaneseParadigm : IndeterminateParadigm

Japanese dare: non-selective. Associates with all four operators via different particles. Base form does not change.

Equations

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

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.japanese_non_selective : japaneseParadigm.isNonSelective = true

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.germanParadigm : IndeterminateParadigm

German irgend-: selective. Associates only with [∃] (§9, p. 137). Cannot associate with [∀] (ex. 20c), [Neg] (ex. 21), or [Q].

Equations

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

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.german_selective : germanParadigm.isSelective = true

structure Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.InterventionDatum : Type

An intervention datum: an element between a wh-phrase and its in-situ associate, and whether the result is grammatical.

• intervener : String
• gloss : String
• grammatical : Bool
• isScopeBearing : Bool

instance Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instReprInterventionDatum : Repr InterventionDatum

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instReprInterventionDatum = { reprPrec := Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instReprInterventionDatum.repr }

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instReprInterventionDatum.repr : InterventionDatum → ℕ → Std.Format

Equations

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

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instBEqInterventionDatum.beq : InterventionDatum → InterventionDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instBEqInterventionDatum.beq x✝¹ x✝ = false

instance Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instBEqInterventionDatum : BEq InterventionDatum

Equations

• Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instBEqInterventionDatum = { beq := Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.instBEqInterventionDatum.beq }

def Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.beckParadigm : List InterventionDatum

Beck effect paradigm (examples 23a-g): scope-bearing elements block feature movement of [∃]/[Q]; non-scope-bearing elements don't.

Pattern: *Was hat sie [INTERVENER] WEM gezeigt?

Equations

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

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.beck_scope_bearing_block : (List.filter (fun (x : InterventionDatum) => x.grammatical == false) beckParadigm).length = 5 ∧ (List.filter (fun (x : InterventionDatum) => x.grammatical == true) beckParadigm).length = 2

Scope-bearing elements block; non-scope-bearing elements don't.

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.beck_generalization : (beckParadigm.all fun (d : InterventionDatum) => d.isScopeBearing == !d.grammatical) = true

The generalization: scope-bearing = ungrammatical, non-scope-bearing = OK.

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.same_base_different_force : Fragments.Japanese.Determiners.dare_ka.indeterminate = Fragments.Japanese.Determiners.dare_mo.indeterminate ∧ Fragments.Japanese.Determiners.dare_ka.qforce ≠ Fragments.Japanese.Determiners.dare_mo.qforce

Same base (dare), different force via particle alternation.

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.dare_ka_existential_from_paradigm : Fragments.Japanese.Determiners.dare_ka.qforce = Fragments.English.Determiners.QForce.existential ∧ japaneseParadigm.associatesWith.contains QuantOperator.exists_ = true

dare-ka is existential; paradigm predicts ∃ association.

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.dare_mo_universal_from_paradigm : Fragments.Japanese.Determiners.dare_mo.qforce = Fragments.English.Determiners.QForce.universal ∧ japaneseParadigm.associatesWith.contains QuantOperator.forall_ = true

dare-mo is universal; paradigm predicts ∀ association.

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.irgendein_existential_only : germanParadigm.associatesWith = [QuantOperator.exists_] ∧ Fragments.German.ModalIndefinites.irgendeinEntry.status = Core.ModalIndefinite.ModalComponentStatus.notAtIssue

irgendein is existential-only + not-at-issue (domain widening).

§1: Indeterminate Pronoun Paradigms Cross-Linguistically

@cite{haspelmath-1997} (p. 277, diacritics omitted). The Latvian paradigm illustrates a selective system: each operator association is morphologically marked by a distinct prefix (kaut- existential, ne- under direct negation, jeb- indirect negation/comparatives/FC).

Latvian paradigm data imported from Fragments/Latvian/IndeterminatePronouns.lean.

theorem Phenomena.ModalIndefinites.Studies.KratzerShimoyama2002.selective_contrast : Fragments.Latvian.IndeterminatePronouns.paradigm.length = 6 ∧ japaneseParadigm.morphologicallyMarked = false

Latvian is morphologically marked (selective); Japanese is not.