Documentation

Linglib.Phenomena.Plurals.Studies.Kriz2016

Križ (2016): Homogeneity, Non-Maximality, and All — Plural Instantiation #

@cite{kriz-2015} @cite{kriz-2016} @cite{fine-1975}

Homogeneity, Non-Maximality, and All. Journal of Semantics 33(3): 493-539.

This file is the plural instantiation of the general homogeneity substrate in Theories.Semantics.Homogeneity.Basic. It connects @cite{kriz-2016}'s plural-definite analysis (atoms as specification points; all as gap remover) to the substrate operators (removeGap, addressesIssue, usable, communicatedContent).

@cite{lasersohn-1999} (the "townspeople asleep" original observation), @cite{brisson-1998} (non-maximality terminology + but/although exception diagnostics), @cite{schwarz-2013} (processing evidence that maximal is the default reading), @cite{malamud-2012} (decision-theoretic precursor with issue partitions, criticised in Appendix A.3 of the paper), @cite{spector-2013} (embedded-plural projection), @cite{kriz-chemla-2015} (companion experimental data), @cite{magri-2014} (alternative gap-derivation via double EXH), @cite{cobreros-etal-2012} (Tolerant/Classical/Strict trivalence; Appendix A.2), @cite{gajewski-2005} (homogeneity-as-presupposition view, rejected in §4.4), @cite{roberts-1996} (QUD-stack tradition the §4.5 caveat distinguishes from).

Core Contributions #

Non-maximal readings of plural definites ("The professors smiled" true even if Smith didn't) arise from the interaction of two independent components:

  1. Homogeneity (semantic): plural predication yields a three-valued truth value — true (all satisfy), false (none satisfy), or gap (some but not all).

  2. Weakened Quality (pragmatic): the maxim of quality is weakened to "say only what is true enough for current purposes," where "current purposes" are formalized as an issue (partition of possible worlds).

The semantic effect of all is to remove the extension gap, making positive and negative extensions complementary. This prevents non-maximal readings because the pragmatic mechanism (Sufficient Truth + Addressing) has no gap to exploit.

§4.4 caveat — homogeneity is NOT a presupposition #

@cite{kriz-2016} §4.4 argues against the @cite{gajewski-2005} (and Schwarzschild 1994, Löbner 2000) view that the homogeneity gap is a presupposition. Križ's arguments include local accommodation behaviour and projection from conditional antecedents differing from standard presupposition behaviour. This file adopts the trivalent-but-not-presuppositional reading: gap-worlds are "between" true and false, not undefined-in-the-presupposition sense.

§4.5 caveat — current issue ≠ immediate-last QUD #

The variable name QUD W here is a substrate convenience and is NOT the @cite{roberts-1996} QUD-stack notion. @cite{kriz-2016} §4.5 is explicit (eq. 39, 40 examples) that identifying the current issue with the immediate-last question on the stack makes wrong predictions. Križ instead treats the current issue as referring to overarching goals of participants, underdetermined by linguistic material and not directly manipulable. The coarseQ/fineQ partitions in our finite model are pedagogical constructions; they are NOT meant as a commitment to the manipulable-QUD theory the paper rejects.

§4.6 puzzle — numerals block non-maximality #

@cite{kriz-2016} §4.6 flags as an unsolved puzzle that "the ten professors smiled" cannot get non-maximal readings, even though "the professors smiled" can. The paper offers only speculation. Križ also notes (43a-b) that French patterns differently. We do not address this puzzle here.

Contents #

Finite Model #

A concrete 5-world model demonstrates end-to-end predictions: "the professors smiled" is usable at a gap-world (smithNeutral) under a coarse issue but not under a fine one, AND not at a gap-world (smithAngry) where Smith's anger is issue-relevant — capturing @cite{kriz-2016} §4.2's distinctive prediction. Adding "all" blocks non-maximal use entirely.

def Phenomena.Plurals.Studies.Kriz2016.barePluralTV {Atom : Type u_1} {W : Type u_2} (P : AtomWProp) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) :

The bare plural sentence "the Xs are P" as a trivalent sentence.

Equations
Instances For
    def Phenomena.Plurals.Studies.Kriz2016.allPluralTV {Atom : Type u_1} {W : Type u_2} (P : AtomWProp) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) :

    The all-sentence "all the Xs are P". Per @cite{kriz-2016} §3.1, all's semantic contribution IS gap removal — it adds nothing on top of the bare plural's universal truth conditions, only collapses the gap into the negative extension. So we derive allPluralTV from the bare plural via removeGap, rather than stipulating its semantics. Bivalence and the truth-conditional behavior then follow from substrate lemmas.

    Equations
    Instances For
      theorem Phenomena.Plurals.Studies.Kriz2016.allPluralTV_eq_removeGap {Atom : Type u_1} {W : Type u_2} (P : AtomWProp) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) :

      all IS gap removal — by definition, after the @cite{kriz-2016} §3.1 refactor. Retained as a named lemma for readability.

      theorem Phenomena.Plurals.Studies.Kriz2016.all_no_gap {Atom : Type u_1} {W : Type u_2} (P : AtomWProp) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) :

      all eliminates the extension gap. Direct consequence of removeGap_not_homogeneous from the substrate.

      theorem Phenomena.Plurals.Studies.Kriz2016.all_not_homogeneous {Atom : Type u_1} {W : Type u_2} (P : AtomWProp) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) :

      all removes homogeneity: the all-sentence is never homogeneous. Direct consequence of substrate removeGap_not_homogeneous.

      theorem Phenomena.Plurals.Studies.Kriz2016.bare_plural_homogeneous {Atom : Type u_1} {W : Type u_2} (P : AtomWProp) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (hGap : barePluralTV P x w = Core.Duality.Truth3.indet) :

      A bare plural is homogeneous whenever a gap-world exists: the existence of a world where some-but-not-all atoms satisfy P makes the sentence homogeneous, enabling non-maximal readings via Sufficient Truth.

      theorem Phenomena.Plurals.Studies.Kriz2016.all_posExt_eq {Atom : Type u_1} {W : Type u_2} (P : AtomWProp) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) :

      Positive extensions agree: bare plural and all-sentence are true in the same worlds. Substrate consequence of removeGap_posExt_eq.

      theorem Phenomena.Plurals.Studies.Kriz2016.all_negExt_eq {Atom : Type u_1} {W : Type u_2} (P : AtomWProp) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) :

      all absorbs the gap into the negative extension: the negative extension of the all-sentence equals the union of the bare plural's negative extension and gap. Substrate consequence of removeGap_negExt_eq.

      theorem Phenomena.Plurals.Studies.Kriz2016.all_bivalent {Atom : Type u_1} {W : Type u_2} (P : AtomWProp) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) :

      all-sentences are bivalent. Substrate consequence of removeGap_bivalent.

      theorem Phenomena.Plurals.Studies.Kriz2016.removeGap_plural_true_iff {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : AtomWProp) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (_hne : x.Nonempty) (w : W) :

      Gap removal on a plural sentence is true iff all atoms satisfy P. Substrate-side bridge between removeGap and the allSatisfy predicate. Used by all_blocked_by_wide_issue and downstream consumers (KrizSpector2021.removeGap_iff_forallH). The _hne hypothesis is retained for compatibility with consumers; the proof itself doesn't need it (the empty case is vacuously true on both sides).

      theorem Phenomena.Plurals.Studies.Kriz2016.bivalentPred_allPluralTV_eq_allSatisfy {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : AtomWProp) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) :

      bivalentPred of an all-sentence is true iff allSatisfy holds. Bridge between the trivalent encoding of allPluralTV and the Prop-valued allSatisfy predicate K&S 2021's strong-relevance machinery works on. Used by KrizSpector2021.all_addressing_iff_relevant.

      theorem Phenomena.Plurals.Studies.Kriz2016.all_prevents_nonmax {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (q : QUD W) (P : AtomWProp) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (h : Semantics.Homogeneity.usable q (allPluralTV P x) w) :

      all prevents non-maximal use: if an all-sentence is usable at w, then all atoms literally satisfy P at w.

      The proof factors through the substrate: by removeGap_bivalent and usability's S w ≠ .false clause, the all-sentence is literally true at w; by removeGap_posExt_eq, the bare plural is also literally true at w; by pluralTruthValue_eq_true_iff, all atoms satisfy P. The addressesIssue clause of usable does no work in this direction — it's what blocks all-sentences from being USED at all in wide-issue contexts (see all_blocked_by_wide_issue).

      theorem Phenomena.Plurals.Studies.Kriz2016.all_blocked_by_wide_issue {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (q : QUD W) (P : AtomWProp) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (hne : x.Nonempty) (hWide : ∃ (w₁ : W) (w₂ : W), q.r w₁ w₂ Semantics.Plurality.Distributivity.allSatisfy P x w₁ ¬Semantics.Plurality.Distributivity.allSatisfy P x w₂) :

      all-sentences cannot be used in "wide" issues — issues whose cells straddle the all/not-all boundary. This is the complementary work done by addressesIssue: while bivalence forces literal truth (all_prevents_nonmax), addressing forces relevance — the all-sentence can only be uttered at all if every QUD cell agrees on whether allSatisfy holds. This is the @cite{kriz-2016} §3.4 wide-issue blocking that completes the picture: bivalence alone does not derive Križ's headline finding; Addressing also has to do work, in this complementary direction.

      theorem Phenomena.Plurals.Studies.Kriz2016.all_exceptions_unmentionable {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (q : QUD W) (P : AtomWProp) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (a : Atom) (ha : a x) (h : Semantics.Homogeneity.usable q (allPluralTV P x) w) :
      P a w

      Unmentionability of exceptions (§4.1): if the all-sentence is usable at w, there are no exceptions to mention. "#Although all the professors smiled, Smith didn't" is contradictory — all forces literal truth, so any exception makes the sentence false, and false sentences cannot be used.

      theorem Phenomena.Plurals.Studies.Kriz2016.plural_gap_enables_nonmax {Atom : Type u_1} {W : Type u_2} (q : QUD W) (P : AtomWProp) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w w' : W) (hGap : barePluralTV P x w = Core.Duality.Truth3.indet) (hEquiv : q.r w w') (hTrue : barePluralTV P x w' = Core.Duality.Truth3.true) (hAddr : Semantics.Homogeneity.addressesIssue q (barePluralTV P x)) :

      The gap enables non-maximal use: if the bare plural has a gap at w and w's cell contains a positive-extension world, then the bare plural is usable at w (assuming addressing is satisfied). This is the mechanism Križ 2016 identifies for non-maximality: gap-worlds can be "true enough" without being literally true.

      This is an instance of the general Semantics.Homogeneity.gap_enables_nonmax.

      A concrete 4-world model demonstrates the theory's predictions end-to-end. Three professors attend Sue's talk; the predicate is "smiled."

      WorldSmithJonesLeeBare pluralAll
      allSmiledTRUEtrue
      smithNeutralGAPfalse
      onlyLeeSmiledGAPfalse
      noneSmiledFALSEfalse

      Two QUDs:

      Predictions:

      Worlds in the 5-world finite model. The split between smithNeutral and smithAngry captures @cite{kriz-2016} §4.2: in both worlds Smith fails to smile, but his behavior differs in QUD-relevance. Smith looking neutral is irrelevant to "was the talk well-received"; Smith looking visibly angry is relevant (it pulls reception down).

      Instances For
        @[implicit_reducible]
        Equations
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Instances For
            @[implicit_reducible]
            Equations
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[implicit_reducible]
              Equations
              • One or more equations did not get rendered due to their size.
              @[implicit_reducible]
              Equations
              • One or more equations did not get rendered due to their size.

              Did this professor smile in this world? Note that Smith fails to smile in BOTH smithNeutral and smithAngry; the worlds differ only in what Smith does instead, which matters to QUD relevance (§4.2).

              Equations
              Instances For
                @[implicit_reducible]
                Equations
                • One or more equations did not get rendered due to their size.

                All three professors.

                Equations
                Instances For

                  Reception grade for the coarse QUD. Per @cite{kriz-2016} §4.2, Smith's anger pulls reception down to mixed; Smith's neutrality leaves it positive. This single QUD captures Križ's distinctive prediction that what Smith does instead of smiling matters.

                  Instances For
                    @[implicit_reducible]
                    Equations

                    Coarse QUD: "Was Sue's talk well-received?" Groups allSmiled with smithNeutral (both = positive reception).

                    Equations
                    Instances For

                      Fine QUD: "Did every professor smile?" Each world is its own cell.

                      Equations
                      Instances For

                        The bare plural sentence about the professors IS homogeneous — smithNeutral is in the extension gap.

                        The bare plural IS usable at smithNeutral under the coarse QUD. Smith's failure to smile is irrelevant to whether the talk was well-received, so the sentence is "true enough."

                        The bare plural is NOT usable at smithNeutral under the fine QUD. The fine QUD distinguishes allSmiled from smithNeutral, so there is no literally-true world in smithNeutral's cell.

                        The all-sentence is never usable at smithNeutral (under any QUD), because Smith didn't smile. Concrete instance of all_prevents_nonmax.

                        Concrete instance of all_exceptions_unmentionable: Smith's exception cannot be mentioned because Smith did smile in every world where the all-sentence is usable.

                        Communicated content under the coarse QUD includes the gap-world smithNeutral — the non-maximal reading is communicated.

                        @cite{kriz-2016} §4.2 makes a distinctive prediction beyond the basic homogeneity-gap analysis: it matters not only whether an exception is tolerated but also what the exception does instead. Smith looking neutral is irrelevant to whether the talk was well-received; Smith looking visibly angry IS relevant. The model captures this by placing smithNeutral and smithAngry in different cells of coarseQ (positive vs. mixed reception).

                        This is a competing-theory differentiator: theories that locate
                        non-maximality in restricted reference (Brisson) or alternative geometry
                        (Magri) cannot easily express that *what Smith does instead* changes
                        the judgment, because they don't have an issue parameter that interacts
                        with individual behavior. 
                        

                        §4.2 distinctive prediction: bare plural is NOT usable at smithAngry under the coarse QUD, even though it IS usable at smithNeutral under the same QUD. The difference is which cell each world inhabits: smithNeutral shares its cell with allSmiled (positive reception); smithAngry sits in the mixed cell with onlyLeeSmiled, neither of which is in the bare plural's positive extension.

                        Together, smithNeutral_usable_coarse and bare_smithAngry_not_usable_coarse demonstrate Križ §4.2: the SAME bare plural sentence under the SAME QUD is usable at one gap-world and not at another, depending on what the exception does. Theories of non-maximality lacking an issue/cell parameter cannot express this contrast.

                        The finite model captures the same pattern as the theory-neutral data in NonMaximality.lean. The switches scenario records that "the switches are on" is acceptable in a non-maximal context (fire risk from any switch) but not in a maximal one (fire risk only if all on). This corresponds to smithNeutral_usable_coarse vs smithNeutral_not_usable_fine.

                        Similarly, switchesAllBlocks records that "all the switches are on" is unacceptable even in the permissive context, corresponding to all_not_usable_smithNeutral.

                        The switches datum records maximal use is not acceptable (in gap scenario).

                        "All" blocks non-maximality even in permissive contexts.

                        The coarse issue makes the all/some distinction irrelevant, which is the precondition for non-maximal readings.

                        Bridge to the theory-neutral homogeneity data in Homogeneity.lean. The data records all as a homogeneity remover and specifies that gap scenarios yield .neitherTrueNorFalse for homogeneous sentences but .clearlyFalse for all-sentences. The structural theorems all_no_gap and all_not_homogeneous prove this mechanism, and the finite model demonstrates it concretely via bare_profs_homogeneous.

                        Gap scenarios yield .neitherTrueNorFalse for homogeneous sentences: the signature of the extension gap that enables non-maximal readings.

                        Adding all makes the gap-scenario sentence clearly false — the gap is absorbed into the negative extension.

                        The switches datum records homogeneity in the gap: positive sentence is neither true nor false when some-but-not-all switches are on.

                        Plural predication is an instance of supervaluation (@cite{fine-1975}). Each atom in the plurality is a specification point: the predicate is super-true iff satisfied by all atoms, super-false iff by none, and indefinite when some-but-not-all satisfy it (the homogeneity gap).

                        This unifies several independent literatures, each contributing a
                        different specification-space sort:
                        
                        - @cite{fine-1975}: varying the *threshold* for vague predicates
                        - @cite{kriz-2016}: varying the *atom* for plural predicates
                        - `dist` in `Core.Duality`: a third implementation of the same pattern
                          over `List Bool`
                        - `selectional_eq_dist` in `Counterfactual.lean`: closest worlds
                        - @cite{haug-dalrymple-2020} §5 (paper eq 109): varying the
                          *precisification of the reciprocal's restrictor* (maximal-set vs
                          reference-set) for quantified-antecedent reciprocals — see
                          `Phenomena/Anaphora/Studies/HaugDalrymple2020.lean`'s
                          `quantifiedReciprocalTV_iff_supervaluation`. 
                        
                        theorem Phenomena.Plurals.Studies.Kriz2016.barePluralTV_eq_superTrue {Atom : Type u_1} {W : Type u_2} (P : AtomWProp) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (hne : x.Nonempty) (w : W) :
                        barePluralTV P x w = Semantics.Supervaluation.superTrue (fun (a : Atom) => P a w) { admissible := x, nonempty := hne }

                        Plural predication = supervaluation over atoms. The bare plural "the Xs are P" at world w has the same truth value as superTrue with atoms as specification points and P(·,w) as the evaluation function.

                        This is the structural identity connecting homogeneity gaps to vagueness gaps: both arise from disagreement across specification points (atoms vs thresholds vs comparison classes).

                        theorem Phenomena.Plurals.Studies.Kriz2016.homogeneity_gap_is_indefiniteness {Atom : Type u_1} {W : Type u_2} (P : AtomWProp) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (hne : x.Nonempty) (w : W) (hgap : barePluralTV P x w = Core.Duality.Truth3.indet) :
                        Semantics.Supervaluation.superTrue (fun (a : Atom) => P a w) { admissible := x, nonempty := hne } = Core.Duality.Truth3.indet

                        Corollary: homogeneity (gap existence) is exactly supervaluation indefiniteness. If the bare plural is gapped at w, then superTrue returns .indet — witnesses exist on both sides.

                        theorem Phenomena.Plurals.Studies.Kriz2016.all_removes_supervaluation_gap {Atom : Type u_1} {W : Type u_2} (P : AtomWProp) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) :

                        Corollary: all removes homogeneity by collapsing the specification space to a single point (the universal check). This corresponds to Fine's fidelity theorem: singleton specification spaces are classical.

                        @cite{kriz-2016} §6.2 considers (and explicitly offers no resolution for) the puzzle that conjunctions of proper names exhibit homogeneity but resist non-maximal readings. If we model "Bert, Claire and Dora went there" as a plural-style supervaluation over atoms {Bert, Claire, Dora}, Križ's gap_enables_nonmax predicts non-maximal use at a gap-world that's QUD-equivalent to a true-world. Empirically (cf. Phenomena.Plurals.Homogeneity.coworkersExample.conjunctionPermitsNonMax), this prediction fails — the conjunction sentence does NOT permit non-maximality in the same gap context where the corresponding plural definite does.

                        Križ acknowledges this in §6.2 and speculates about "team credit" but offers no formalization. The theorem kriz_overgenerates_conjunction_nonmax below makes the divergence kernel-visible: a Lean prediction (the plural-style model says non-maximal IS usable) and the empirical record (it isn't) co-existing in a single statement.

                        @[implicit_reducible]
                        Equations
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Instances For
                            @[implicit_reducible]
                            Equations
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[implicit_reducible]
                              Equations
                              • One or more equations did not get rendered due to their size.
                              @[implicit_reducible]
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Equations
                              Instances For
                                @[implicit_reducible]
                                Equations
                                • One or more equations did not get rendered due to their size.

                                Coarse "did anyone go?" issue: groups all worlds where someone went into a single cell, vs. the noneWent cell.

                                Instances For
                                  @[implicit_reducible]
                                  Equations

                                  Lean prediction: if we model the conjunction "Bert, Claire and Dora went" as a plural over {Bert, Claire, Dora}, Križ's machinery predicts usability at the gap-world dorasMissing (where Dora missed but the others went), under the coarse "did someone go?" issue.

                                  Križ overgenerates non-maximality for conjunctions (kernel-checked divergence theorem). The Lean prediction (conj_modeled_as_plural_predicts_nonmax) asserts non-maximal usability at the gap-world; the empirical record (coworkersExample.conjunctionPermitsNonMax = false) asserts it is unacceptable. Both clauses hold simultaneously in this conjunction; the theorem's existence is the formal disagreement. @cite{kriz-2016} §6.2 acknowledges the puzzle and speculates about "team credit" but provides no formalization.

                                  @cite{magri-2014} derives homogeneity from double-strengthening on alternative geometry (MYSTERY/WEAK/STRONG roles, Horn-mate structure). Magri's doubleExh .mystery on a gap scenario is FALSE (theorem Magri2014.gap_positive_false). This is bivalent-FALSE: the gap is collapsed to the negative extension by the alternative-exhaustification machinery, before any pragmatics applies.

                                  @cite{kriz-2016}'s barePluralTV on the same gap pattern returns .indet (homogeneity gap), and the gap is then PRAGMATICALLY recoverable via gap_enables_nonmax under a coarse QUD. This is the central Križ vs. Magri disagreement: Magri puts the gap-collapse INSIDE the semantics (via doubleExh); Križ keeps the gap and lets pragmatics (sufficient truth + addressing) decide whether non-maximal use is licensed.

                                  Empirically Križ has the upper hand: non-maximal readings DO occur (see the finite model's smithNeutral_usable_coarse). Under Magri's bivalent-FALSE, the sentence at the gap is unutterable in standard Gricean terms (false sentences violate Quality); to recover non-maximal readings, Magri needs additional downstream pragmatic machinery beyond what the alternative- geometry account itself provides.

                                  This is the cross-framework reconciler's core point: the SAME empirical gap data (Phenomena.Plurals.Homogeneity.switchesExample) gets two incompatible derivations, and the formalization makes the incompatibility kernel-checked.

                                  A 3-atom Magri scenario where 2 of 3 atoms satisfy the predicate — the count-abstraction analogue of the smithNeutral world (Smith didn't smile, Jones and Lee did).

                                  Equations
                                  Instances For

                                    Magri's doubleExh .mystery returns FALSE on a 2-of-3 gap. This is the bivalent-FALSE assignment: the gap is collapsed semantically.

                                    Križ vs. Magri formal divergence on the gap's status.

                                    On the same 2-of-3 gap pattern:

                                    • Magri: doubleExh .mystery returns FALSE — the gap is collapsed semantically by alternative-exhaustification, pre-pragmatics. False sentences are unutterable (violate Quality).
                                    • Križ: barePluralTV returns INDET (bare_smithNeutral), and the bare plural IS USABLE under a coarse QUD (smithNeutral_usable_coarse). The gap is preserved and pragmatically recoverable.

                                    Both predictions cannot be right about the empirical fact that non-maximal readings exist for plural definites at gap-worlds. The theorem packages the disagreement as a kernel-checked conjunction; its existence is the formal incompatibility between alternative-geometry derivations and supervaluation derivations of homogeneity.

                                    @cite{kriz-2016} §6.3 claims the homogeneity-plus-pragmatics machinery extends to bare-plural generics ("Israelis live on the coastal plain" — true despite exceptions), with subkinds as the specification points. The Theories.Semantics.Homogeneity.Basic substrate docstring records this as a candidate spec-point instantiation.

                                    However, Phenomena.Generics.Studies.Cohen1999 uses the word "homogeneity" for a different equation: presupposition failure when conditional probabilities diverge across partitions of the domain. Cohen's homogeneity returns "undefined" via presupposition failure; Križ's returns Truth3.indet via supervaluation gap on subkinds.

                                    A formal kriz_vs_cohen_generic_homogeneity divergence theorem would require lifting Cohen's presupposition-style machinery into the Truth3 framework — not done here. The substrate docstring's claim that "the framework extends to generics" should be read with this caveat: it extends to a Križ-style treatment of generics, which is NOT what Cohen1999 formalizes.