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 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

• KratzerShimoyama2002.HamblinDen α = (α → Prop)

def 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

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

theorem 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 KratzerShimoyama2002.opExists {W : Type} (A : HamblinDen (W → Prop)) : W → Prop

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

• KratzerShimoyama2002.opQ A = A

theorem 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 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 KratzerShimoyama2002.QuantOperator : Type

Map from operator tags to their semantic implementations.

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

@[implicit_reducible]

instance KratzerShimoyama2002.instDecidableEqQuantOperator : DecidableEq QuantOperator

Equations

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

def KratzerShimoyama2002.instReprQuantOperator.repr : QuantOperator → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KratzerShimoyama2002.instReprQuantOperator : Repr QuantOperator

Equations

• KratzerShimoyama2002.instReprQuantOperator = { reprPrec := KratzerShimoyama2002.instReprQuantOperator.repr }

def 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

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

theorem 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 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 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 KratzerShimoyama2002.Person : Type

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

@[implicit_reducible]

instance KratzerShimoyama2002.instDecidableEqPerson : DecidableEq Person

Equations

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

def KratzerShimoyama2002.instReprPerson.repr : Person → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KratzerShimoyama2002.instReprPerson : Repr Person

Equations

• KratzerShimoyama2002.instReprPerson = { reprPrec := KratzerShimoyama2002.instReprPerson.repr }

def KratzerShimoyama2002.dare : HamblinDen Person

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

Equations

• KratzerShimoyama2002.dare x✝ = True

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

⟦nemutta⟧ = singleton set containing the sleep predicate.

Equations

• KratzerShimoyama2002.sleptPred slept = Semantics.Composition.SetMonad.eta slept

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

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

Equations

• KratzerShimoyama2002.dareNemutta slept = KratzerShimoyama2002.hamblinFA (KratzerShimoyama2002.sleptPred slept) KratzerShimoyama2002.dare

theorem 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 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.Logic.Intensional.BAccessRel) 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 KratzerShimoyama2002.HamblinAccessRel (W : Type) : Type

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

Equations

• KratzerShimoyama2002.HamblinAccessRel W = (W → W → Prop)

def 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

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

def 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

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

def 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

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

theorem 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 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 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 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 KratzerShimoyama2002.simpleIndef {E : Type} (D : Set E) (P : E → Prop) : Set E

A simple indefinite selects from a contextually restricted subset.

Equations

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

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

An irgend- indefinite widens to the full predicate extension.

Equations

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

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

@[implicit_reducible]

instance KratzerShimoyama2002.instReprIndeterminateParadigm : Repr IndeterminateParadigm

Equations

• KratzerShimoyama2002.instReprIndeterminateParadigm = { reprPrec := KratzerShimoyama2002.instReprIndeterminateParadigm.repr }

def KratzerShimoyama2002.instReprIndeterminateParadigm.repr : IndeterminateParadigm → ℕ → Std.Format

Equations

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

def KratzerShimoyama2002.IndeterminateParadigm.isNonSelective (p : IndeterminateParadigm) : Bool

Equations

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

def KratzerShimoyama2002.IndeterminateParadigm.isSelective (p : IndeterminateParadigm) : Bool

Equations

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

def 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 KratzerShimoyama2002.japanese_non_selective : japaneseParadigm.isNonSelective = true

def KratzerShimoyama2002.germanParadigm : IndeterminateParadigm

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

Equations

• KratzerShimoyama2002.germanParadigm = { language := "German", base := "irgend-", associatesWith := [KratzerShimoyama2002.QuantOperator.exists_], morphologicallyMarked := true }

theorem KratzerShimoyama2002.german_selective : germanParadigm.isSelective = true

structure 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

def KratzerShimoyama2002.instReprInterventionDatum.repr : InterventionDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KratzerShimoyama2002.instReprInterventionDatum : Repr InterventionDatum

Equations

• KratzerShimoyama2002.instReprInterventionDatum = { reprPrec := KratzerShimoyama2002.instReprInterventionDatum.repr }

@[implicit_reducible]

instance KratzerShimoyama2002.instBEqInterventionDatum : BEq InterventionDatum

Equations

• KratzerShimoyama2002.instBEqInterventionDatum = { beq := KratzerShimoyama2002.instBEqInterventionDatum.beq }

def KratzerShimoyama2002.instBEqInterventionDatum.beq : InterventionDatum → InterventionDatum → Bool

Equations

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

def 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 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 KratzerShimoyama2002.beck_generalization : (beckParadigm.all fun (d : InterventionDatum) => d.isScopeBearing == !d.grammatical) = true

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

theorem 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 KratzerShimoyama2002.dare_ka_existential_from_paradigm : Fragments.Japanese.Determiners.dare_ka.qforce = Theories.Semantics.Quantification.Lexicon.QForce.existential ∧ japaneseParadigm.associatesWith.contains QuantOperator.exists_ = true

dare-ka is existential; paradigm predicts ∃ association.

theorem KratzerShimoyama2002.dare_mo_universal_from_paradigm : Fragments.Japanese.Determiners.dare_mo.qforce = Theories.Semantics.Quantification.Lexicon.QForce.universal ∧ japaneseParadigm.associatesWith.contains QuantOperator.forall_ = true

dare-mo is universal; paradigm predicts ∀ association.

theorem KratzerShimoyama2002.irgendein_existential_only : germanParadigm.associatesWith = [QuantOperator.exists_] ∧ Fragments.German.ModalIndefinites.irgendeinEntry.status = Features.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 KratzerShimoyama2002.selective_contrast : Fragments.Latvian.IndeterminatePronouns.paradigm.length = 6 ∧ japaneseParadigm.morphologicallyMarked = false

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