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).
Related literature engaged #
@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:
Homogeneity (semantic): plural predication yields a three-valued truth value — true (all satisfy), false (none satisfy), or gap (some but not all).
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 #
barePluralTV,allPluralTV: plural-specific instantiations- Theorems linking gap-removal to
allsemantics - A 5-world finite model demonstrating end-to-end predictions (including §4.2 angry-Smith vs. neutral-Smith distinction)
- §5/§6 bridges to data records in
Plurals.NonMaximalityandPlurals.Homogeneity - §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 @cite{kriz-2016} §4.2's distinctive prediction. Adding "all" blocks non-maximal use entirely.
The bare plural sentence "the Xs are P" as a trivalent sentence.
Equations
Instances For
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
all IS gap removal — by definition, after the @cite{kriz-2016} §3.1
refactor. Retained as a named lemma for readability.
all eliminates the extension gap. Direct consequence of
removeGap_not_homogeneous from the substrate.
all removes homogeneity: the all-sentence is never homogeneous.
Direct consequence of substrate removeGap_not_homogeneous.
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. Substrate consequence of removeGap_posExt_eq.
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.
all-sentences are bivalent. Substrate consequence of removeGap_bivalent.
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).
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.
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).
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.
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.
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)
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).
- allSmiled : ProfWorld
- smithNeutral : ProfWorld
- smithAngry : ProfWorld
- onlyLeeSmiled : ProfWorld
- noneSmiled : ProfWorld
Instances For
Equations
- Phenomena.Plurals.Studies.Kriz2016.instDecidableEqProfWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Phenomena.Plurals.Studies.Kriz2016.instDecidableEqProf x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
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? 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
- Phenomena.Plurals.Studies.Kriz2016.smiled Phenomena.Plurals.Studies.Kriz2016.Prof.smith Phenomena.Plurals.Studies.Kriz2016.ProfWorld.allSmiled = True
- Phenomena.Plurals.Studies.Kriz2016.smiled Phenomena.Plurals.Studies.Kriz2016.Prof.smith Phenomena.Plurals.Studies.Kriz2016.ProfWorld.smithNeutral = False
- Phenomena.Plurals.Studies.Kriz2016.smiled Phenomena.Plurals.Studies.Kriz2016.Prof.smith Phenomena.Plurals.Studies.Kriz2016.ProfWorld.smithAngry = False
- Phenomena.Plurals.Studies.Kriz2016.smiled Phenomena.Plurals.Studies.Kriz2016.Prof.smith Phenomena.Plurals.Studies.Kriz2016.ProfWorld.onlyLeeSmiled = False
- Phenomena.Plurals.Studies.Kriz2016.smiled Phenomena.Plurals.Studies.Kriz2016.Prof.smith Phenomena.Plurals.Studies.Kriz2016.ProfWorld.noneSmiled = False
- Phenomena.Plurals.Studies.Kriz2016.smiled Phenomena.Plurals.Studies.Kriz2016.Prof.jones Phenomena.Plurals.Studies.Kriz2016.ProfWorld.allSmiled = True
- Phenomena.Plurals.Studies.Kriz2016.smiled Phenomena.Plurals.Studies.Kriz2016.Prof.jones Phenomena.Plurals.Studies.Kriz2016.ProfWorld.smithNeutral = True
- Phenomena.Plurals.Studies.Kriz2016.smiled Phenomena.Plurals.Studies.Kriz2016.Prof.jones Phenomena.Plurals.Studies.Kriz2016.ProfWorld.smithAngry = True
- Phenomena.Plurals.Studies.Kriz2016.smiled Phenomena.Plurals.Studies.Kriz2016.Prof.jones Phenomena.Plurals.Studies.Kriz2016.ProfWorld.onlyLeeSmiled = False
- Phenomena.Plurals.Studies.Kriz2016.smiled Phenomena.Plurals.Studies.Kriz2016.Prof.jones Phenomena.Plurals.Studies.Kriz2016.ProfWorld.noneSmiled = False
- Phenomena.Plurals.Studies.Kriz2016.smiled Phenomena.Plurals.Studies.Kriz2016.Prof.lee Phenomena.Plurals.Studies.Kriz2016.ProfWorld.allSmiled = True
- Phenomena.Plurals.Studies.Kriz2016.smiled Phenomena.Plurals.Studies.Kriz2016.Prof.lee Phenomena.Plurals.Studies.Kriz2016.ProfWorld.smithNeutral = True
- Phenomena.Plurals.Studies.Kriz2016.smiled Phenomena.Plurals.Studies.Kriz2016.Prof.lee Phenomena.Plurals.Studies.Kriz2016.ProfWorld.smithAngry = True
- Phenomena.Plurals.Studies.Kriz2016.smiled Phenomena.Plurals.Studies.Kriz2016.Prof.lee Phenomena.Plurals.Studies.Kriz2016.ProfWorld.onlyLeeSmiled = True
- Phenomena.Plurals.Studies.Kriz2016.smiled Phenomena.Plurals.Studies.Kriz2016.Prof.lee Phenomena.Plurals.Studies.Kriz2016.ProfWorld.noneSmiled = False
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- Phenomena.Plurals.Studies.Kriz2016.instDecidableEqReception x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- Phenomena.Plurals.Studies.Kriz2016.receptionGrade Phenomena.Plurals.Studies.Kriz2016.ProfWorld.allSmiled = Phenomena.Plurals.Studies.Kriz2016.Reception.positive
- Phenomena.Plurals.Studies.Kriz2016.receptionGrade Phenomena.Plurals.Studies.Kriz2016.ProfWorld.smithNeutral = Phenomena.Plurals.Studies.Kriz2016.Reception.positive
- Phenomena.Plurals.Studies.Kriz2016.receptionGrade Phenomena.Plurals.Studies.Kriz2016.ProfWorld.smithAngry = Phenomena.Plurals.Studies.Kriz2016.Reception.mixed
- Phenomena.Plurals.Studies.Kriz2016.receptionGrade Phenomena.Plurals.Studies.Kriz2016.ProfWorld.onlyLeeSmiled = Phenomena.Plurals.Studies.Kriz2016.Reception.mixed
- Phenomena.Plurals.Studies.Kriz2016.receptionGrade Phenomena.Plurals.Studies.Kriz2016.ProfWorld.noneSmiled = Phenomena.Plurals.Studies.Kriz2016.Reception.negative
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.
Communicated content under the fine QUD does NOT include smithNeutral.
@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 non-maximal use is acceptable.
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.
The homogeneity data lists all as a remover.
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.
Outside the gap, judgments are clear: all switches on → clearly true.
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`.
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).
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.
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.
Equations
- Phenomena.Plurals.Studies.Kriz2016.instDecidableEqConjAtom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Phenomena.Plurals.Studies.Kriz2016.instDecidableEqConjWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
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.
Equations
- Phenomena.Plurals.Studies.Kriz2016.wentThere Phenomena.Plurals.Studies.Kriz2016.ConjAtom.bert Phenomena.Plurals.Studies.Kriz2016.ConjWorld.allWent = True
- Phenomena.Plurals.Studies.Kriz2016.wentThere Phenomena.Plurals.Studies.Kriz2016.ConjAtom.bert Phenomena.Plurals.Studies.Kriz2016.ConjWorld.dorasMissing = True
- Phenomena.Plurals.Studies.Kriz2016.wentThere Phenomena.Plurals.Studies.Kriz2016.ConjAtom.bert Phenomena.Plurals.Studies.Kriz2016.ConjWorld.onlyBert = True
- Phenomena.Plurals.Studies.Kriz2016.wentThere Phenomena.Plurals.Studies.Kriz2016.ConjAtom.bert Phenomena.Plurals.Studies.Kriz2016.ConjWorld.noneWent = False
- Phenomena.Plurals.Studies.Kriz2016.wentThere Phenomena.Plurals.Studies.Kriz2016.ConjAtom.claire Phenomena.Plurals.Studies.Kriz2016.ConjWorld.allWent = True
- Phenomena.Plurals.Studies.Kriz2016.wentThere Phenomena.Plurals.Studies.Kriz2016.ConjAtom.claire Phenomena.Plurals.Studies.Kriz2016.ConjWorld.dorasMissing = True
- Phenomena.Plurals.Studies.Kriz2016.wentThere Phenomena.Plurals.Studies.Kriz2016.ConjAtom.claire Phenomena.Plurals.Studies.Kriz2016.ConjWorld.onlyBert = False
- Phenomena.Plurals.Studies.Kriz2016.wentThere Phenomena.Plurals.Studies.Kriz2016.ConjAtom.claire Phenomena.Plurals.Studies.Kriz2016.ConjWorld.noneWent = False
- Phenomena.Plurals.Studies.Kriz2016.wentThere Phenomena.Plurals.Studies.Kriz2016.ConjAtom.dora Phenomena.Plurals.Studies.Kriz2016.ConjWorld.allWent = True
- Phenomena.Plurals.Studies.Kriz2016.wentThere Phenomena.Plurals.Studies.Kriz2016.ConjAtom.dora Phenomena.Plurals.Studies.Kriz2016.ConjWorld.dorasMissing = False
- Phenomena.Plurals.Studies.Kriz2016.wentThere Phenomena.Plurals.Studies.Kriz2016.ConjAtom.dora Phenomena.Plurals.Studies.Kriz2016.ConjWorld.onlyBert = False
- Phenomena.Plurals.Studies.Kriz2016.wentThere Phenomena.Plurals.Studies.Kriz2016.ConjAtom.dora Phenomena.Plurals.Studies.Kriz2016.ConjWorld.noneWent = False
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- Phenomena.Plurals.Studies.Kriz2016.threeCoworkers = Finset.univ
Instances For
Coarse "did anyone go?" issue: groups all worlds where someone went into a single cell, vs. the noneWent cell.
- someWent : ConjPartition
- noneWent : ConjPartition
Instances For
Equations
- Phenomena.Plurals.Studies.Kriz2016.instDecidableEqConjPartition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- Phenomena.Plurals.Studies.Kriz2016.someWentPartition Phenomena.Plurals.Studies.Kriz2016.ConjWorld.allWent = Phenomena.Plurals.Studies.Kriz2016.ConjPartition.someWent
- Phenomena.Plurals.Studies.Kriz2016.someWentPartition Phenomena.Plurals.Studies.Kriz2016.ConjWorld.dorasMissing = Phenomena.Plurals.Studies.Kriz2016.ConjPartition.someWent
- Phenomena.Plurals.Studies.Kriz2016.someWentPartition Phenomena.Plurals.Studies.Kriz2016.ConjWorld.onlyBert = Phenomena.Plurals.Studies.Kriz2016.ConjPartition.someWent
- Phenomena.Plurals.Studies.Kriz2016.someWentPartition Phenomena.Plurals.Studies.Kriz2016.ConjWorld.noneWent = Phenomena.Plurals.Studies.Kriz2016.ConjPartition.noneWent
Instances For
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
- Phenomena.Plurals.Studies.Kriz2016.magriGapScenario = { total := 3, satisfying := 2, valid := Phenomena.Plurals.Studies.Kriz2016.magriGapScenario._proof_2 }
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 .mysteryreturns FALSE — the gap is collapsed semantically by alternative-exhaustification, pre-pragmatics. False sentences are unutterable (violate Quality). - Križ:
barePluralTVreturns 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.