German Distributive Expressions

Fragment entries for German distributive items grounded in the theory-layer operators from Theories/Semantics/Lexical/Plural/Distributivity.lean.

Inventory

Form	Gloss	Syntactic use	Semantics	±dist	±max
jeder	every/each	DP + distance	distMaximal	+	+
jeweils	each/resp.	distance only	distTolerant	+	-
alle	all	DP only	allViaForallH	-	+

The key contrast: jeder and jeweils are both obligatorily distributive, but differ in maximality. jeder uses identity tolerance (forces maximality); jeweils uses a contextually provided tolerance (permits non-maximality for some speakers). @cite{haslinger-etal-2025}.

Grounding

Each entry's semantics is defined by direct reference to theory-layer operators, following the compositional grounding principle: Fragment entries import and use Theory definitions, never stipulating their own meaning functions.

def Fragments.German.Distributives.jederSem {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] : Finset Atom → W → Prop

⟦jeder⟧ = distMaximal: distribute P to every atom, no exceptions.

Equivalent to distTolerant with identity tolerance (distMaximal_eq_identity). On atoms, reduces to P itself (distMaximal_singleton).

@cite{haslinger-etal-2025} examples (1), (22b-c).

Equations

• Fragments.German.Distributives.jederSem P = Semantics.Plurality.Distributivity.distMaximal P

def Fragments.German.Distributives.jeweilsSem {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (tol : Semantics.Plurality.Distributivity.Tolerance Atom) : Finset Atom → W → Prop

⟦jeweils⟧ = distTolerant: distribute P to atoms within a tolerant sub-plurality. The tolerance relation ≤ is contextually provided.

For speakers who accept jeweils in non-maximal contexts, the tolerance parameter allows exceptions irrelevant to the QUD.

@cite{haslinger-etal-2025} eq. (25), examples (22a), (23b), (24b).

Equations

• Fragments.German.Distributives.jeweilsSem P tol = Semantics.Plurality.Distributivity.distTolerant P tol

def Fragments.German.Distributives.alleSem {Atom : Type u_1} {W : Type u_2} [Fintype Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : Prop

⟦alle⟧ = universal quantification over the tolerance parameter.

alle does not itself force distributivity — it removes the tolerance parameter that would otherwise permit non-maximal readings. The predicate's own dist/non-dist nature is preserved.

Formally: ⟦alle P⟧ = λw.λx.∀≤'[≤' tolerance → ⟦P⟧^≤'(x)] This is equivalent to allSatisfy by allViaForallH_iff_allSatisfy.

@cite{haslinger-etal-2025} eq. (20b); @cite{kriz-spector-2021} §5.3.

Equations

• Fragments.German.Distributives.alleSem P x w = Semantics.Plurality.Distributivity.allViaForallH P x w

structure Fragments.German.Distributives.DistributiveEntry : Type

German distributive expression with grounded semantics.

• form : String

  Surface form

• gloss : String

  English gloss

• hasDPUse : Bool

  Has a DP-internal (determiner) use?

• hasDistanceUse : Bool

  Has a distance-distributive (adverbial) use?

• distMaxClass : Semantics.Plurality.Distributivity.DistMaxClass

  Classification

def Fragments.German.Distributives.instReprDistributiveEntry.repr : DistributiveEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.German.Distributives.instReprDistributiveEntry : Repr DistributiveEntry

Equations

• Fragments.German.Distributives.instReprDistributiveEntry = { reprPrec := Fragments.German.Distributives.instReprDistributiveEntry.repr }

def Fragments.German.Distributives.jederEntry : DistributiveEntry

Equations

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

def Fragments.German.Distributives.jeweilsEntry : DistributiveEntry

Equations

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

def Fragments.German.Distributives.alleEntry : DistributiveEntry

Equations

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

theorem Fragments.German.Distributives.jeder_eq_distMaximal {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] : jederSem P = Semantics.Plurality.Distributivity.distMaximal P

jeder's semantics IS distMaximal

theorem Fragments.German.Distributives.jeder_iff_identity_tolerant {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (hne : x.Nonempty) : jederSem P x w ↔ Semantics.Plurality.Distributivity.distTolerant P Semantics.Plurality.Distributivity.Tolerance.identity x w

jeder ↔ distTolerant with identity tolerance (on nonempty pluralities)

theorem Fragments.German.Distributives.jeweils_identity_iff_jeder {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (hne : x.Nonempty) : jeweilsSem P Semantics.Plurality.Distributivity.Tolerance.identity x w ↔ jederSem P x w

jeweils with identity tolerance ↔ jeder (on nonempty pluralities)

theorem Fragments.German.Distributives.alle_iff_allSatisfy {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] [Fintype Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : alleSem P x w ↔ Semantics.Plurality.Distributivity.allSatisfy P x w

alle reduces to simple universal check on atoms

theorem Fragments.German.Distributives.dp_use_implies_maximal_for_attested : jederEntry.hasDPUse = true ∧ jederEntry.distMaxClass.isMaximal = true ∧ alleEntry.hasDPUse = true ∧ alleEntry.distMaxClass.isMaximal = true ∧ jeweilsEntry.hasDPUse = false ∧ jeweilsEntry.distMaxClass.isMaximal = false

The DP-use / maximality correlation from @cite{haslinger-etal-2025} §4: items with a DP-internal use (jeder, alle) enforce maximality; items without one (jeweils) permit non-maximality.

This is a descriptive correlation, not a theorem — the paper notes that jeder* (eq. 27) would be a counterexample if attested.