Documentation

Linglib.Phenomena.Plurals.Studies.Kriz2016

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

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

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

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.

General Homogeneity Theory #

The general definitions (trivalent sentence denotations, supervaluation source, gap removal, pragmatic usability, communicated content) live in the Semantics.Homogeneity namespace within this file. They are domain-independent and apply to any homogeneity source:

The shared structure: supervaluation over specification points (@cite{fine-1975}).

Plural-Specific Instantiation #

The Phenomena.Plurals.Studies.Kriz2016 namespace adds plural-specific instantiations (barePluralTV, allPluralTV) and a concrete 4-world finite model demonstrating end-to-end predictions.

Key Definitions #

Finite Model #

A concrete 4-world model demonstrates end-to-end predictions: "the professors smiled" is usable at a gap-world under a coarse issue but not under a fine one, and adding "all" blocks non-maximal use entirely.

@[reducible, inline]

A trivalent sentence denotation: maps worlds to truth values. This is the general type for any sentence that may exhibit homogeneity.

Equations
Instances For

    Positive extension: worlds where the sentence is true.

    Equations
    Instances For

      Negative extension: worlds where the sentence is false.

      Equations
      Instances For

        Extension gap: worlds where the sentence is neither true nor false.

        Equations
        Instances For

          The three extensions partition the world space.

          The positive and negative extensions are disjoint.

          A sentence is homogeneous if its extension gap is non-empty. The gap is what enables non-maximal readings.

          Equations
          Instances For

            A sentence is bivalent if it has no extension gap. all, necessarily, and completely make sentences bivalent.

            Equations
            Instances For

              Bivalence and homogeneity are complementary: a sentence is bivalent iff it has no extension gap.

              Every supervaluation instance gives rise to a trivalent sentence. The specification points can be: - Atoms of a plurality (plural definites) - Accessible worlds (conditionals) - Spatial parts (summative predicates) - Subkinds (generics)

              The shared structure: TRUE iff the predicate holds at ALL spec points,
              FALSE iff it fails at ALL, GAP iff it holds at some but not all. 
              
              def Semantics.Homogeneity.supervaluationTV {Spec : Type u_2} {W : Type u_3} (eval : WSpecBool) (space : WSupervaluation.SpecSpace Spec) :

              Construct a trivalent sentence from a supervaluation instance. eval w gives the Bool predicate over spec points at world w, and space w gives the spec space at world w.

              Equations
              Instances For
                theorem Semantics.Homogeneity.supervaluationTV_true_iff {Spec : Type u_2} {W : Type u_3} (eval : WSpecBool) (space : WSupervaluation.SpecSpace Spec) (w : W) :
                supervaluationTV eval space w = Core.Duality.Truth3.true s(space w).admissible, eval w s = true

                A supervaluation sentence is true iff the predicate holds at all specs.

                theorem Semantics.Homogeneity.supervaluationTV_false_iff {Spec : Type u_2} {W : Type u_3} (eval : WSpecBool) (space : WSupervaluation.SpecSpace Spec) (w : W) :
                supervaluationTV eval space w = Core.Duality.Truth3.false s(space w).admissible, eval w s = false

                A supervaluation sentence is false iff the predicate fails at all specs.

                theorem Semantics.Homogeneity.supervaluationTV_gap_iff {Spec : Type u_2} {W : Type u_3} (eval : WSpecBool) (space : WSupervaluation.SpecSpace Spec) (w : W) :
                supervaluationTV eval space w = Core.Duality.Truth3.gap (∃ s(space w).admissible, eval w s = true) s(space w).admissible, eval w s = false

                A supervaluation sentence is gapped iff witnesses exist on both sides.

                A homogeneity remover is any operation that eliminates the extension gap, making the sentence bivalent. Linguistically:

                | Domain      | Remover         | Example                          |
                |-------------|-----------------|----------------------------------|
                | Plurals     | `all`           | "All the professors smiled"      |
                | Conditionals| `necessarily`   | "If Mary comes, John will nec…"  |
                | Spatial     | `completely`    | "The flag is completely blue"     |
                | Spatial     | `whole`         | "The whole wall is painted"       |
                
                Semantically, removal collapses the gap into the negative extension:
                gap-worlds become false-worlds, preserving the positive extension. 
                

                Remove homogeneity: collapse gap into negative extension. The positive extension is preserved; gap and false both become false.

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

                  Removal produces a bivalent sentence.

                  Removal preserves the positive extension.

                  Removal absorbs the gap into the negative extension.

                  Removed sentences are never homogeneous.

                  The pragmatic mechanism that derives non-maximal readings from the homogeneity gap. Two independent principles interact:

                  1. **Sufficient Truth**: weakens Quality to "true enough for current purposes"
                  2. **Addressing an Issue**: restricts which sentences can be used for which
                     issues, based on alignment between truth-value boundaries and issue cells
                  
                  Together, they predict that a sentence can be used at a gap-world iff
                  (i) a literally-true world is in the same issue cell, and (ii) no cell
                  straddles the true/false boundary. 
                  
                  def Semantics.Homogeneity.sufficientlyTrue {W : Type u_1} (q : QUD W) (S : SentenceTV W) (w : W) :

                  Sufficient Truth: S is "true enough" at world w relative to issue I iff there is a world w' that is I-equivalent to w where S is literally true.

                  This weakens the standard maxim of quality: a speaker need not assert something literally true, only something equivalent to something true for current purposes.

                  Equations
                  Instances For

                    Literal truth implies sufficient truth (for any issue).

                    Addressing an Issue: S may be used to address issue I only if no cell of I overlaps with both the positive and the negative extension.

                    Gap-worlds are invisible: a cell containing true-worlds and gap-worlds is fine. Only a cell straddling the true/false boundary is problematic.

                    Equations
                    Instances For
                      def Semantics.Homogeneity.usable {W : Type u_1} (q : QUD W) (S : SentenceTV W) (w : W) :

                      A sentence may be used at w iff: (1) S is not false at w, (2) S is sufficiently true at w, and (3) S addresses the issue.

                      Equations
                      Instances For

                        For bivalent sentences, usability reduces to literal truth + addressing. Sufficient Truth adds nothing because there are no gap-worlds.

                        The communicated content of S relative to issue I: the set of worlds the hearer considers possible after hearing S.

                        This is the union of all issue cells that overlap with ⟦S⟧⁺. The hearer infers not that S is literally true, but that the actual world is indistinguishable (relative to current purposes) from one where S is literally true.

                        Equations
                        Instances For

                          Literal truth is always communicated.

                          For bivalent sentences that address the issue, communicated content equals the positive extension — no pragmatic weakening is possible.

                          This is the key consequence of gap removal: all/necessarily/completely force literal truth to be communicated.

                          theorem Semantics.Homogeneity.communicatedContent_antitone {W : Type u_1} (q q' : QUD W) (S : SentenceTV W) (hRef : ∀ (w₁ w₂ : W), q'.sameAnswer w₁ w₂ = trueq.sameAnswer w₁ w₂ = true) :

                          Communicated content is antitone in issue refinement: coarser issues (bigger cells) communicate more content. If q' refines q (q' is finer), then everything communicated under q' is also communicated under q.

                          This is @cite{kriz-2016}'s key prediction: coarser QUDs enable more non-maximal use. The finite model in Kriz2016.lean demonstrates this: coarseQ communicates smithNeutral but fineQ does not.

                          Extract the Bool truth predicate from a bivalent sentence. Used to bridge between the trivalent Addressing constraint and bivalent strong-relevance filtering (Križ & Spector 2021).

                          Equations
                          Instances For

                            @cite{kriz-2016} §6.4: Conditionals are the modal analogue of plural definites. "If P, Q" universally quantifies over closest P-worlds, just as "the Xs are Q" universally quantifies over atoms. The conditional excluded middle (CEM) — the observation that "if P, Q" seems neither true nor false when Q holds at some but not all closest P-worlds — IS homogeneity.

                            | Plural domain | Conditional domain  |
                            |---------------|---------------------|
                            | atoms         | closest P-worlds    |
                            | `all`         | `necessarily`       |
                            | bare plural   | bare conditional    |
                            | gap (some)    | CEM (some worlds)   |
                            
                            @cite{stalnaker-1981} @cite{von-fintel-1999} 
                            
                            def Semantics.Homogeneity.conditionalTV {W : Type u_2} (closestPWorlds : WFinset W) (Q : WBool) :

                            A bare conditional "if P, Q" as a trivalent sentence. The spec points are the closest P-worlds; the eval function is Q. TRUE if Q holds at all closest P-worlds, FALSE if Q fails at all, GAP otherwise (conditional excluded middle).

                            This is the same computation as selectionalCounterfactual in Conditionals/Counterfactual.lean, which proves the equivalence with superTrue via selectional_as_supervaluation. The two formalizations use different input representations (Finset vs List) but compute the same three-valued truth value.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              def Semantics.Homogeneity.strictConditionalTV {W : Type u_2} (closestPWorlds : WFinset W) (Q : WBool) :

                              A strict conditional "if P, necessarily Q" — the all of conditionals. Defined as gap removal on the bare conditional: necessarily collapses the homogeneity gap, just as all does for plurals.

                              Equations
                              Instances For
                                theorem Semantics.Homogeneity.strictConditionalTV_bivalent {W : Type u_2} (closestPWorlds : WFinset W) (Q : WBool) :
                                isBivalent (strictConditionalTV closestPWorlds Q)

                                Strict conditionals are bivalent — necessarily removes the gap, just as all removes homogeneity for plurals.

                                theorem Semantics.Homogeneity.conditionalTV_posExt_eq {W : Type u_2} (closestPWorlds : WFinset W) (Q : WBool) :
                                posExt (conditionalTV closestPWorlds Q) = posExt (strictConditionalTV closestPWorlds Q)

                                Positive extensions agree: the bare conditional and the strict conditional are true in the same worlds. Parallel to all_posExt_eq for plurals.

                                theorem Semantics.Homogeneity.necessarily_prevents_nonmax {W : Type u_2} (q : QUD W) (closestPWorlds : WFinset W) (Q : WBool) (w : W) (h : usable q (strictConditionalTV closestPWorlds Q) w) (hne : (closestPWorlds w).Nonempty) (w' : W) :
                                w' closestPWorlds wQ w' = true

                                necessarily prevents non-maximal use of conditionals, just as all does for plurals. If a strict conditional is usable at w, Q holds at all closest P-worlds (when they exist).

                                @cite{kriz-2016} §5.1, Definition (45): Homogeneity for collective predicates is defined via mereological overlap, not individual atoms. A predicate P is undefined of plurality a if a is not in P's positive extension but overlaps with some plurality that is.

                                For distributive predicates, this reduces to the atom-based definition
                                in `Distributivity.lean`: the overlapping witness is a singleton {x}
                                where x ∈ a and P(x).
                                
                                For collective predicates like "perform Hamlet", the overlapping witness
                                can be a larger group: "the boys" overlaps with "all the students", and
                                if all the students are performing Hamlet, the boys' predication is
                                undefined (not false). 
                                
                                def Semantics.Homogeneity.overlaps {Atom : Type u_2} [DecidableEq Atom] (a b : Finset Atom) :

                                Two pluralities overlap if they share at least one individual.

                                Equations
                                Instances For
                                  def Semantics.Homogeneity.generalisedTV {Atom : Type u_2} [DecidableEq Atom] (P : Finset AtomBool) (domain : Finset (Finset Atom)) (a : Finset Atom) :

                                  Generalised homogeneity: trivalent truth for predicates on pluralities. Handles both distributive and collective predicates uniformly.

                                  • TRUE: P holds of a
                                  • GAP: P doesn't hold of a, but some overlapping plurality in domain satisfies P
                                  • FALSE: no overlapping plurality in domain satisfies P

                                  domain is the set of all relevant pluralities (e.g., all subgroups of the universe of discourse). For distributive predicates, singletons suffice; for collective predicates, larger groups are needed.

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

                                    Generalised homogeneity is a genuine three-way partition.

                                    theorem Semantics.Homogeneity.generalisedTV_true_of_holds {Atom : Type u_2} [DecidableEq Atom] (P : Finset AtomBool) (domain : Finset (Finset Atom)) (a : Finset Atom) (h : P a = true) :

                                    If P holds of a, the generalised truth value is TRUE.

                                    theorem Semantics.Homogeneity.overlaps_self {Atom : Type u_2} [DecidableEq Atom] (a : Finset Atom) (hne : a.Nonempty) :

                                    Overlap is reflexive for nonempty pluralities.

                                    theorem Semantics.Homogeneity.overlaps_symm {Atom : Type u_2} [DecidableEq Atom] (a b : Finset Atom) :

                                    Overlap is symmetric.

                                    theorem Semantics.Homogeneity.overlaps_exists_mem {Atom : Type u_2} [DecidableEq Atom] {a b : Finset Atom} (h : overlaps a b = true) :
                                    ya, y b

                                    If two pluralities overlap, they share a member.

                                    theorem Semantics.Homogeneity.overlaps_singleton_of_mem {Atom : Type u_2} [DecidableEq Atom] {a : Finset Atom} {x : Atom} (hx : x a) :

                                    A singleton of a member overlaps with the plurality.

                                    theorem Semantics.Homogeneity.generalisedTV_distributive_reduction {Atom : Type u_2} [DecidableEq Atom] (pred : AtomBool) (a : Finset Atom) (hne : a.Nonempty) (domain : Finset (Finset Atom)) (hdomain : xa, {x} domain) :
                                    generalisedTV (fun (s : Finset Atom) => decide (∀ xs, pred x = true)) domain a = Supervaluation.superTrue (fun (x : Atom) => pred x) { admissible := a, nonempty := hne }

                                    For distributive predicates, the generalised definition coincides with supervaluation over atoms when the domain includes all singletons of members. The distributive predicate ∀ x ∈ s, pred x is checked against each sub-plurality; the overlap condition reduces to checking individual atoms of a.

                                    The central insight of @cite{kriz-2016}: all homogeneity phenomena share the same pragmatic mechanism. Once a domain has been identified as exhibiting homogeneity (via any of the sources above), the SAME sufficientlyTrue + addressesIssue mechanism derives non-maximal readings, and the SAME removeGap operation explains why removers (all, necessarily, completely, whole) block them.

                                    The following theorems are domain-independent consequences. 
                                    

                                    Any bivalent sentence (one whose gap has been removed) forces literal truth for usability. This is the general form of the headline result: homogeneity removers prevent non-maximal use.

                                    theorem Semantics.Homogeneity.gap_enables_nonmax {W : Type u_2} (q : QUD W) (S : SentenceTV W) (w w' : W) (hGap : S w = Core.Duality.Truth3.gap) (hEquiv : q.sameAnswer w w' = true) (hTrue : S w' = Core.Duality.Truth3.true) (hAddr : addressesIssue q S) :
                                    usable q S w

                                    The gap enables non-maximal use: if S is gapped at w and w's cell contains a true-world, then S is usable at w (assuming addressing).

                                    Gap-worlds are never false, so they satisfy the first usability condition.

                                    pluralTruthValue from Distributivity.lean is an instance of supervaluationTV with atoms as specification points. This bridge makes the general gap-manipulation machinery (§3, §8) applicable to plural predication.

                                    theorem Semantics.Homogeneity.pluralTruthValue_eq_supervaluationTV {Atom : Type u_2} {W : Type u_3} (P : AtomWBool) (x : Finset Atom) (hne : x.Nonempty) (w : W) :
                                    Lexical.Plural.Distributivity.pluralTruthValue P x w = supervaluationTV (fun (w : W) (a : Atom) => P a w) (fun (x_1 : W) => { admissible := x, nonempty := hne }) w

                                    pluralTruthValue is supervaluationTV with atoms as spec points.

                                    Gap removal on a plural sentence is true iff all atoms satisfy P. This is the formal content of "all removes homogeneity."

                                    def Phenomena.Plurals.Studies.Kriz2016.barePluralTV {Atom : Type u_1} {W : Type u_2} (P : AtomWBool) (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 : AtomWBool) (x : Finset Atom) :

                                      The all-sentence "all the Xs are P" as a bivalent sentence. all removes homogeneity: the truth value is always true or false.

                                      Equations
                                      Instances For

                                        all IS gap removal: the all-sentence is the bare plural with its extension gap collapsed into the negative extension.

                                        This is the central structural claim of @cite{kriz-2016}: the semantic contribution of all is not to add universal quantification (the bare plural already universally quantifies), but to remove homogeneity.

                                        theorem Phenomena.Plurals.Studies.Kriz2016.all_no_gap {Atom : Type u_1} {W : Type u_2} (P : AtomWBool) (x : Finset Atom) :

                                        all eliminates the extension gap.

                                        all removes homogeneity: the all-sentence is never homogeneous. Corresponds to HomogeneityRemover.all in Homogeneity.lean.

                                        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.

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

                                        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.

                                        theorem Phenomena.Plurals.Studies.Kriz2016.all_bivalent {Atom : Type u_1} {W : Type u_2} (P : AtomWBool) (x : Finset Atom) :

                                        all-sentences are bivalent.

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

                                        This is the headline result of the paper's analysis of all. The bare plural "the Xs are P" can be used non-maximally (at gap-worlds where some but not all Xs satisfy P), but "all the Xs are P" cannot — usability forces literal truth.

                                        theorem Phenomena.Plurals.Studies.Kriz2016.all_exceptions_unmentionable {Atom : Type u_1} {W : Type u_2} (q : QUD W) (P : AtomWBool) (x : Finset Atom) (w : W) (a : Atom) (ha : a x) (h : Semantics.Homogeneity.usable q (allPluralTV P x) w) :
                                        P a w = true

                                        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 : AtomWBool) (x : Finset Atom) (w w' : W) (hGap : barePluralTV P x w = Core.Duality.Truth3.gap) (hEquiv : q.sameAnswer w w' = true) (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:

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

                                                Did this professor smile in this world?

                                                Equations
                                                Instances For

                                                  Reception grade for the coarse QUD.

                                                  Instances For

                                                    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.

                                                        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 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 two independent literatures:
                                                        - @cite{fine-1975}: varying the *threshold* for vague predicates
                                                        - @cite{kriz-2016}: varying the *atom* for plural predicates
                                                        
                                                        Both are instances of `Semantics.Supervaluation.superTrue`. The `dist`
                                                        operator in `Core.Duality` is a third implementation of the same pattern
                                                        over `List Bool`; `selectional_eq_dist` in `Counterfactual.lean` proves
                                                        yet another instance for closest worlds. 
                                                        
                                                        theorem Phenomena.Plurals.Studies.Kriz2016.barePluralTV_eq_superTrue {Atom : Type u_1} {W : Type u_2} (P : AtomWBool) (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 : AtomWBool) (x : Finset Atom) (hne : x.Nonempty) (w : W) (hgap : barePluralTV P x w = Core.Duality.Truth3.gap) :
                                                        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 : AtomWBool) (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.