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

[Kri15b] [Kri16] [Fin75]

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

This file is the plural instantiation of the general homogeneity substrate in Semantics.Homogeneity.Basic. It connects [Kri16]'s plural-definite analysis (atoms as specification points; all as gap remover) to the substrate operators (removeGap, addressesIssue, usable, communicatedContent).

Related literature engaged

[Las99] (the "townspeople asleep" original observation), [Bri98] (non-maximality terminology + but/although exception diagnostics), [Sch13] (processing evidence that maximal is the default reading), [Mal12] (decision-theoretic precursor with issue partitions, criticised in Appendix A.3 of the paper), [Spe13] (embedded-plural projection), [KC15] (companion experimental data), [Mag14] (alternative gap-derivation via double EXH), [CERvR12] (Tolerant/Classical/Strict trivalence; Appendix A.2), [Gaj05] (homogeneity-as-presupposition view, rejected in §4.4), [Rob96] (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

[Kri16] §4.4 argues against the [Gaj05] (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 [Rob96] QUD-stack notion. [Kri16] §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

[Kri16] §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

• barePluralTV, allPluralTV: plural-specific instantiations
• Theorems linking gap-removal to all semantics
• A 5-world finite model demonstrating end-to-end predictions (including §4.2 angry-Smith vs. neutral-Smith distinction)
• §5/§6 bridges to the typed switches data in Data.Examples.Kriz2015 and the pooled Generalizations.HomogeneityGap observations
• §7 connection back to the supervaluation framework

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 [Kri16] §4.2's distinctive prediction. Adding "all" blocks non-maximal use entirely.

def Kriz2016.barePluralTV {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) : Semantics.Homogeneity.SentenceTV W

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

Equations

• Kriz2016.barePluralTV P x w = Semantics.Plurality.Trivalent.pluralTruthValue P x w

def Kriz2016.allPluralTV {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) : Semantics.Homogeneity.SentenceTV W

The all-sentence "all the Xs are P". Per [Kri16] §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

• Kriz2016.allPluralTV P x = Semantics.Homogeneity.removeGap (Kriz2016.barePluralTV P x)

theorem Kriz2016.allPluralTV_eq_removeGap {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) : allPluralTV P x = Semantics.Homogeneity.removeGap (barePluralTV P x)

all IS gap removal — by definition, after the [Kri16] §3.1 refactor. Retained as a named lemma for readability.

theorem Kriz2016.all_no_gap {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) : Semantics.Homogeneity.gapExt (allPluralTV P x) = ∅

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

theorem Kriz2016.all_not_homogeneous {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) : ¬Semantics.Homogeneity.isHomogeneous (allPluralTV P x)

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

theorem Kriz2016.bare_plural_homogeneous {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (hGap : barePluralTV P x w = Core.Duality.Truth3.indet) : Semantics.Homogeneity.isHomogeneous (barePluralTV P x)

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 Kriz2016.all_posExt_eq {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) : Semantics.Homogeneity.posExt (allPluralTV P x) = Semantics.Homogeneity.posExt (barePluralTV P x)

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

theorem Kriz2016.all_negExt_eq {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) : Semantics.Homogeneity.negExt (barePluralTV P x) ∪ Semantics.Homogeneity.gapExt (barePluralTV P x) = Semantics.Homogeneity.negExt (allPluralTV P x)

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 Kriz2016.all_bivalent {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) : Semantics.Homogeneity.isBivalent (allPluralTV P x)

all-sentences are bivalent. Substrate consequence of removeGap_bivalent.

theorem Kriz2016.removeGap_plural_true_iff {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) (_hne : x.Nonempty) (w : W) : Semantics.Homogeneity.removeGap (fun (w : W) => Semantics.Plurality.Trivalent.pluralTruthValue P x w) w = Core.Duality.Truth3.true ↔ Semantics.Plurality.allSatisfy P x 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 Kriz2016.bivalentPred_allPluralTV_eq_allSatisfy {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) : Semantics.Homogeneity.bivalentPred (allPluralTV P x) w = true ↔ Semantics.Plurality.allSatisfy P x 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 Kriz2016.all_prevents_nonmax {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (q : QUD W) (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (h : Semantics.Homogeneity.usable q (allPluralTV P x) w) : Semantics.Plurality.allSatisfy 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 Kriz2016.all_blocked_by_wide_issue {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (q : QUD W) (P : Atom → W → Prop) [(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.allSatisfy P x w₁ ∧ ¬Semantics.Plurality.allSatisfy P x w₂) : ¬Semantics.Homogeneity.addressesIssue q (allPluralTV P x)

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 [Kri16] §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 Kriz2016.all_exceptions_unmentionable {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (q : QUD W) (P : Atom → W → Prop) [(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 Kriz2016.plural_gap_enables_nonmax {Atom : Type u_1} {W : Type u_2} (q : QUD W) (P : Atom → W → Prop) [(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)) : Semantics.Homogeneity.usable q (barePluralTV P x) w

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

World	Smith	Jones	Lee	Bare plural	All
allSmiled	✓	✓	✓	TRUE	true
smithNeutral	✗	✓	✓	GAP	false
onlyLeeSmiled	✗	✗	✓	GAP	false
noneSmiled	✗	✗	✗	FALSE	false

Two QUDs:

• Coarse ("Was the talk well-received?"): groups allSmiled ≈ smithNeutral
• Fine ("Did every professor smile?"): each world in its own cell

Predictions:

• Bare plural usable at smithNeutral under coarse QUD (non-maximal reading)
• Bare plural NOT usable at smithNeutral under fine QUD (maximal only)
• all-sentence never usable at smithNeutral (forces literal truth)

inductive Kriz2016.ProfWorld : Type

Worlds in the 5-world finite model. The split between smithNeutral and smithAngry captures [Kri16] §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).

• allSmiled : ProfWorld
• smithNeutral : ProfWorld
• smithAngry : ProfWorld
• onlyLeeSmiled : ProfWorld
• noneSmiled : ProfWorld

@[implicit_reducible]

instance Kriz2016.instDecidableEqProfWorld : DecidableEq ProfWorld

Equations

• Kriz2016.instDecidableEqProfWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Kriz2016.instReprProfWorld : Repr ProfWorld

Equations

• Kriz2016.instReprProfWorld = { reprPrec := Kriz2016.instReprProfWorld.repr }

def Kriz2016.instReprProfWorld.repr : ProfWorld → ℕ → Std.Format

Equations

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

inductive Kriz2016.Prof : Type

• smith : Prof
• jones : Prof
• lee : Prof

@[implicit_reducible]

instance Kriz2016.instDecidableEqProf : DecidableEq Prof

Equations

• Kriz2016.instDecidableEqProf x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Kriz2016.instReprProf : Repr Prof

Equations

• Kriz2016.instReprProf = { reprPrec := Kriz2016.instReprProf.repr }

def Kriz2016.instReprProf.repr : Prof → ℕ → Std.Format

Equations

• Kriz2016.instReprProf.repr Kriz2016.Prof.smith prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kriz2016.Prof.smith")).group prec✝
• Kriz2016.instReprProf.repr Kriz2016.Prof.jones prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kriz2016.Prof.jones")).group prec✝
• Kriz2016.instReprProf.repr Kriz2016.Prof.lee prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kriz2016.Prof.lee")).group prec✝

@[implicit_reducible]

instance Kriz2016.instFintypeProfWorld : Fintype ProfWorld

Equations

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

@[implicit_reducible]

instance Kriz2016.instFintypeProf : Fintype Prof

Equations

• Kriz2016.instFintypeProf = { elems := {Kriz2016.Prof.smith, Kriz2016.Prof.jones, Kriz2016.Prof.lee}, complete := Kriz2016.instFintypeProf._proof_1 }

def Kriz2016.smiled : Prof → ProfWorld → Prop

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

• Kriz2016.smiled Kriz2016.Prof.smith Kriz2016.ProfWorld.allSmiled = True
• Kriz2016.smiled Kriz2016.Prof.smith Kriz2016.ProfWorld.smithNeutral = False
• Kriz2016.smiled Kriz2016.Prof.smith Kriz2016.ProfWorld.smithAngry = False
• Kriz2016.smiled Kriz2016.Prof.smith Kriz2016.ProfWorld.onlyLeeSmiled = False
• Kriz2016.smiled Kriz2016.Prof.smith Kriz2016.ProfWorld.noneSmiled = False
• Kriz2016.smiled Kriz2016.Prof.jones Kriz2016.ProfWorld.allSmiled = True
• Kriz2016.smiled Kriz2016.Prof.jones Kriz2016.ProfWorld.smithNeutral = True
• Kriz2016.smiled Kriz2016.Prof.jones Kriz2016.ProfWorld.smithAngry = True
• Kriz2016.smiled Kriz2016.Prof.jones Kriz2016.ProfWorld.onlyLeeSmiled = False
• Kriz2016.smiled Kriz2016.Prof.jones Kriz2016.ProfWorld.noneSmiled = False
• Kriz2016.smiled Kriz2016.Prof.lee Kriz2016.ProfWorld.allSmiled = True
• Kriz2016.smiled Kriz2016.Prof.lee Kriz2016.ProfWorld.smithNeutral = True
• Kriz2016.smiled Kriz2016.Prof.lee Kriz2016.ProfWorld.smithAngry = True
• Kriz2016.smiled Kriz2016.Prof.lee Kriz2016.ProfWorld.onlyLeeSmiled = True
• Kriz2016.smiled Kriz2016.Prof.lee Kriz2016.ProfWorld.noneSmiled = False

@[implicit_reducible]

instance Kriz2016.smiled.instDecidable (p : Prof) (w : ProfWorld) : Decidable (smiled p w)

Equations

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

def Kriz2016.profs : Finset Prof

All three professors.

Equations

• Kriz2016.profs = Finset.univ

inductive Kriz2016.Reception : Type

Reception grade for the coarse QUD. Per [Kri16] §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.

• positive : Reception
• mixed : Reception
• negative : Reception

@[implicit_reducible]

instance Kriz2016.instDecidableEqReception : DecidableEq Reception

Equations

• Kriz2016.instDecidableEqReception x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Kriz2016.receptionGrade : ProfWorld → Reception

Equations

• Kriz2016.receptionGrade Kriz2016.ProfWorld.allSmiled = Kriz2016.Reception.positive
• Kriz2016.receptionGrade Kriz2016.ProfWorld.smithNeutral = Kriz2016.Reception.positive
• Kriz2016.receptionGrade Kriz2016.ProfWorld.smithAngry = Kriz2016.Reception.mixed
• Kriz2016.receptionGrade Kriz2016.ProfWorld.onlyLeeSmiled = Kriz2016.Reception.mixed
• Kriz2016.receptionGrade Kriz2016.ProfWorld.noneSmiled = Kriz2016.Reception.negative

def Kriz2016.coarseQ : QUD ProfWorld

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

Equations

• Kriz2016.coarseQ = QUD.ofDecEq Kriz2016.receptionGrade

def Kriz2016.fineQ : QUD ProfWorld

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

Equations

• Kriz2016.fineQ = QUD.ofDecEq id

theorem Kriz2016.bare_allSmiled : barePluralTV smiled profs ProfWorld.allSmiled = Core.Duality.Truth3.true

theorem Kriz2016.bare_smithNeutral : barePluralTV smiled profs ProfWorld.smithNeutral = Core.Duality.Truth3.indet

theorem Kriz2016.bare_onlyLeeSmiled : barePluralTV smiled profs ProfWorld.onlyLeeSmiled = Core.Duality.Truth3.indet

theorem Kriz2016.bare_noneSmiled : barePluralTV smiled profs ProfWorld.noneSmiled = Core.Duality.Truth3.false

theorem Kriz2016.bare_profs_homogeneous : Semantics.Homogeneity.isHomogeneous (barePluralTV smiled profs)

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

theorem Kriz2016.smithNeutral_usable_coarse : Semantics.Homogeneity.usable coarseQ (barePluralTV smiled profs) ProfWorld.smithNeutral

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

theorem Kriz2016.smithNeutral_not_usable_fine : ¬Semantics.Homogeneity.usable fineQ (barePluralTV smiled profs) ProfWorld.smithNeutral

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.

theorem Kriz2016.all_not_usable_smithNeutral (q : QUD ProfWorld) (h : Semantics.Homogeneity.usable q (allPluralTV smiled profs) ProfWorld.smithNeutral) : False

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

theorem Kriz2016.smith_exception_unmentionable (q : QUD ProfWorld) (w : ProfWorld) (h : Semantics.Homogeneity.usable q (allPluralTV smiled profs) w) : smiled Prof.smith w

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.

theorem Kriz2016.coarse_communicates_gap : ProfWorld.smithNeutral ∈ Semantics.Homogeneity.communicatedContent coarseQ (barePluralTV smiled profs)

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

theorem Kriz2016.fine_does_not_communicate_gap : ProfWorld.smithNeutral ∉ Semantics.Homogeneity.communicatedContent fineQ (barePluralTV smiled profs)

Communicated content under the fine QUD does NOT include smithNeutral.

[Kri16] §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. 

theorem Kriz2016.bare_smithAngry : barePluralTV smiled profs ProfWorld.smithAngry = Core.Duality.Truth3.indet

theorem Kriz2016.bare_smithAngry_not_usable_coarse : ¬Semantics.Homogeneity.usable coarseQ (barePluralTV smiled profs) ProfWorld.smithAngry

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

theorem Kriz2016.kriz_4_2_distinctive_prediction : Semantics.Homogeneity.usable coarseQ (barePluralTV smiled profs) ProfWorld.smithNeutral ∧ ¬Semantics.Homogeneity.usable coarseQ (barePluralTV smiled profs) ProfWorld.smithAngry

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 typed switches data in Data.Examples.Kriz2015. "Oh no, the switches are on!" is acceptable under the existential issue (fire risk from any switch — the all/some distinction is irrelevant) and unacceptable under the universal issue (fire risk only if all are on), corresponding to smithNeutral_usable_coarse vs smithNeutral_not_usable_fine. The "all the switches" variant is unacceptable even in the permissive context, corresponding to all_not_usable_smithNeutral.

theorem Kriz2016.switches_nonmax_contrast : Kriz2015.Examples.switches_nonmax_existential.judgment = Features.Judgment.acceptable ∧ Kriz2015.Examples.switches_nonmax_universal.judgment = Features.Judgment.unacceptable

Non-maximality context contrast: the same gap-scenario sentence is acceptable under the existential issue, unacceptable under the universal.

theorem Kriz2016.switches_all_blocks : Kriz2015.Examples.switches_nonmax_existential.alternatives = [("Oh no, all the switches are on!", Features.Judgment.unacceptable)]

all blocks non-maximality even in the permissive existential-issue context: the "all the switches" variant of the acceptable row is unacceptable.

The switches gap rows of Data.Examples.Kriz2015 lift to .indet observations in the cross-paper Generalizations.HomogeneityGap pool — the value barePluralTV assigns at the model's gap-world (bare_smithNeutral). The gap-removal effect of all (gap absorbed into the negative extension, so the gap scenario comes out clearly false) is proved structurally by all_no_gap, all_negExt_eq, and all_not_homogeneous.

theorem Kriz2016.switches_gap_observed_indet : Option.map (fun (x : Generalizations.HomogeneityGap.GapDatum) => x.observed) (Generalizations.HomogeneityGap.fromExample Kriz2015.Examples.switches_pos_gap) = some Core.Duality.Truth3.indet ∧ Option.map (fun (x : Generalizations.HomogeneityGap.GapDatum) => x.observed) (Generalizations.HomogeneityGap.fromExample Kriz2015.Examples.switches_neg_gap) = some Core.Duality.Truth3.indet

Both switches gap rows (positive and negated) observe the trivalent gap value .indet: the gap is symmetric under negation.

theorem Kriz2016.model_matches_gap_row : Option.map (fun (x : Generalizations.HomogeneityGap.GapDatum) => x.observed) (Generalizations.HomogeneityGap.fromExample Kriz2015.Examples.switches_pos_gap) = some (barePluralTV smiled profs ProfWorld.smithNeutral)

The finite model matches the data: the bare plural's truth value at the gap-world smithNeutral is exactly the value the positive gap row observes.

Plural predication is an instance of supervaluation ([Fin75]). 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:

- [fine-1975]: varying the *threshold* for vague predicates
- [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
- [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
  `Studies/HaugDalrymple2020.lean`'s
  `quantifiedReciprocalTV_iff_supervaluation`. 

theorem Kriz2016.barePluralTV_eq_superTrue {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(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 Kriz2016.homogeneity_gap_is_indefiniteness {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(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 Kriz2016.all_removes_supervaluation_gap {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : allPluralTV P x w ≠ Core.Duality.Truth3.indet

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.

[Kri16] §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 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; conj_modeled_as_plural_predicts_nonmax makes the overgenerated prediction kernel-visible.

inductive Kriz2016.ConjAtom : Type

• bert : ConjAtom
• claire : ConjAtom
• dora : ConjAtom

@[implicit_reducible]

instance Kriz2016.instDecidableEqConjAtom : DecidableEq ConjAtom

Equations

• Kriz2016.instDecidableEqConjAtom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Kriz2016.instReprConjAtom : Repr ConjAtom

Equations

• Kriz2016.instReprConjAtom = { reprPrec := Kriz2016.instReprConjAtom.repr }

def Kriz2016.instReprConjAtom.repr : ConjAtom → ℕ → Std.Format

Equations

• Kriz2016.instReprConjAtom.repr Kriz2016.ConjAtom.bert prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kriz2016.ConjAtom.bert")).group prec✝
• Kriz2016.instReprConjAtom.repr Kriz2016.ConjAtom.claire prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kriz2016.ConjAtom.claire")).group prec✝
• Kriz2016.instReprConjAtom.repr Kriz2016.ConjAtom.dora prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kriz2016.ConjAtom.dora")).group prec✝

inductive Kriz2016.ConjWorld : Type

• allWent : ConjWorld
• dorasMissing : ConjWorld
• onlyBert : ConjWorld
• noneWent : ConjWorld

@[implicit_reducible]

instance Kriz2016.instDecidableEqConjWorld : DecidableEq ConjWorld

Equations

• Kriz2016.instDecidableEqConjWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Kriz2016.instReprConjWorld : Repr ConjWorld

Equations

• Kriz2016.instReprConjWorld = { reprPrec := Kriz2016.instReprConjWorld.repr }

def Kriz2016.instReprConjWorld.repr : ConjWorld → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Kriz2016.instReprConjWorld.repr Kriz2016.ConjWorld.allWent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kriz2016.ConjWorld.allWent")).group prec✝

@[implicit_reducible]

instance Kriz2016.instFintypeConjAtom : Fintype ConjAtom

Equations

• Kriz2016.instFintypeConjAtom = { elems := {Kriz2016.ConjAtom.bert, Kriz2016.ConjAtom.claire, Kriz2016.ConjAtom.dora}, complete := Kriz2016.instFintypeConjAtom._proof_1 }

@[implicit_reducible]

instance Kriz2016.instFintypeConjWorld : Fintype ConjWorld

Equations

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

def Kriz2016.wentThere : ConjAtom → ConjWorld → Prop

Equations

• Kriz2016.wentThere Kriz2016.ConjAtom.bert Kriz2016.ConjWorld.allWent = True
• Kriz2016.wentThere Kriz2016.ConjAtom.bert Kriz2016.ConjWorld.dorasMissing = True
• Kriz2016.wentThere Kriz2016.ConjAtom.bert Kriz2016.ConjWorld.onlyBert = True
• Kriz2016.wentThere Kriz2016.ConjAtom.bert Kriz2016.ConjWorld.noneWent = False
• Kriz2016.wentThere Kriz2016.ConjAtom.claire Kriz2016.ConjWorld.allWent = True
• Kriz2016.wentThere Kriz2016.ConjAtom.claire Kriz2016.ConjWorld.dorasMissing = True
• Kriz2016.wentThere Kriz2016.ConjAtom.claire Kriz2016.ConjWorld.onlyBert = False
• Kriz2016.wentThere Kriz2016.ConjAtom.claire Kriz2016.ConjWorld.noneWent = False
• Kriz2016.wentThere Kriz2016.ConjAtom.dora Kriz2016.ConjWorld.allWent = True
• Kriz2016.wentThere Kriz2016.ConjAtom.dora Kriz2016.ConjWorld.dorasMissing = False
• Kriz2016.wentThere Kriz2016.ConjAtom.dora Kriz2016.ConjWorld.onlyBert = False
• Kriz2016.wentThere Kriz2016.ConjAtom.dora Kriz2016.ConjWorld.noneWent = False

@[implicit_reducible]

instance Kriz2016.wentThere.instDecidable (a : ConjAtom) (w : ConjWorld) : Decidable (wentThere a w)

Equations

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

def Kriz2016.threeCoworkers : Finset ConjAtom

Equations

• Kriz2016.threeCoworkers = Finset.univ

inductive Kriz2016.ConjPartition : Type

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

• someWent : ConjPartition
• noneWent : ConjPartition

@[implicit_reducible]

instance Kriz2016.instDecidableEqConjPartition : DecidableEq ConjPartition

Equations

• Kriz2016.instDecidableEqConjPartition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Kriz2016.someWentPartition : ConjWorld → ConjPartition

Equations

• Kriz2016.someWentPartition Kriz2016.ConjWorld.allWent = Kriz2016.ConjPartition.someWent
• Kriz2016.someWentPartition Kriz2016.ConjWorld.dorasMissing = Kriz2016.ConjPartition.someWent
• Kriz2016.someWentPartition Kriz2016.ConjWorld.onlyBert = Kriz2016.ConjPartition.someWent
• Kriz2016.someWentPartition Kriz2016.ConjWorld.noneWent = Kriz2016.ConjPartition.noneWent

def Kriz2016.coarseConjQ : QUD ConjWorld

Equations

• Kriz2016.coarseConjQ = QUD.ofDecEq Kriz2016.someWentPartition

theorem Kriz2016.conj_dorasMissing_gap : barePluralTV wentThere threeCoworkers ConjWorld.dorasMissing = Core.Duality.Truth3.indet

theorem Kriz2016.conj_modeled_as_plural_predicts_nonmax : Semantics.Homogeneity.usable coarseConjQ (barePluralTV wentThere threeCoworkers) ConjWorld.dorasMissing

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.

[Mag14] 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.

[Kri16]'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 (the Data.Examples.Kriz2015 switches gap rows) gets two incompatible derivations, and the formalization makes the incompatibility kernel-checked.

def Kriz2016.magriGapScenario : Magri2014.Scenario

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

• Kriz2016.magriGapScenario = { total := 3, satisfying := 2, valid := Kriz2016.magriGapScenario._proof_2 }

theorem Kriz2016.magriGapScenario_isGap : Magri2014.isGap magriGapScenario = true

theorem Kriz2016.magri_2of3_gap_is_bivalent_false : Magri2014.doubleExh Magri2014.Role.mystery magriGapScenario = false

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

theorem Kriz2016.kriz_vs_magri_alternative_geometry : Magri2014.doubleExh Magri2014.Role.mystery magriGapScenario = false ∧ barePluralTV smiled profs ProfWorld.smithNeutral = Core.Duality.Truth3.indet ∧ Semantics.Homogeneity.usable coarseQ (barePluralTV smiled profs) ProfWorld.smithNeutral

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.

[Kri16] §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 Semantics.Homogeneity.Basic substrate docstring records this as a candidate spec-point instantiation.

However, 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.