Bar-Lev (2021): An Implicature Account of Homogeneity and Non-Maximality

@cite{bar-lev-2021}

An Implicature Account of Homogeneity and Non-Maximality. Linguistics and Philosophy 44:1045–1097.

Core Contribution

Bar-Lev derives homogeneity, universality, and non-maximality for plural definites from a single mechanism: exhaustification with subdomain alternatives via the Exh^{IE+II} operator of @cite{bar-lev-fox-2020}.

The key ingredients:

1. ∃-PL (existential pluralization): The basic meaning of a plural definite like "the kids laughed" is existential: at least one kid laughed. This operator is defined in ExistentialPL.lean.

2. Subdomain alternatives: Replacing the domain variable D with subsets D' ⊆ D generates alternatives that are NOT closed under conjunction — structurally parallel to free choice disjunction (@cite{fox-2007}).

3. Exh^{IE+II}: The same exhaustivity operator that derives free choice from ◇(A ∨ B) derives universality from ∃-PL. Since the subdomain alternatives are not closed under ∧, no non-prejacent alternative is innocently excludable, and all are innocently includable.

Structural Parallel with Free Choice

This file proves that the Exh^{IE+II} derivation for homogeneity is structurally isomorphic to the free choice derivation in Phenomena/Modality/Studies/BarLevFox2020.lean:

Free Choice	Homogeneity
FCWorld (5 worlds)	HomWorld (4 worlds)
◇(A ∨ B) (prejacent)	someLaughed (∃-PL)
{◇(A∨B), ◇A, ◇B, ◇(A∧B)}	{someLaughed, kellyL, janeL}
◇A ∧ ◇B ∉ ALT	kellyL ∧ janeL ∉ ALT
IE = {◇(A∧B)}	IE = ∅
II = {◇A, ◇B}	II = {kellyL, janeL}
Free choice	Universal reading

Asymmetry of Positive and Negative

A key prediction: the positive and negative cases are not symmetric.

• Positive "the kids laughed": existential basic meaning, strengthened to universal by Exh^{IE+II} (implicature).
• Negative "the kids didn't laugh": ¬∃ = ∀¬ from basic semantics alone — no strengthening needed.

This asymmetry is derived in negative_universal below.

inductive BarLev2021.HomWorld : Type

Possible worlds for a two-atom plurality {Kelly, Jane} and a predicate P (e.g., "laughed").

• neither : HomWorld
• onlyKelly : HomWorld
• onlyJane : HomWorld
• both : HomWorld

@[implicit_reducible]

instance BarLev2021.instDecidableEqHomWorld : DecidableEq HomWorld

Equations

• BarLev2021.instDecidableEqHomWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BarLev2021.instReprHomWorld.repr : HomWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance BarLev2021.instReprHomWorld : Repr HomWorld

Equations

• BarLev2021.instReprHomWorld = { reprPrec := BarLev2021.instReprHomWorld.repr }

def BarLev2021.instInhabitedHomWorld.default : HomWorld

Equations

• BarLev2021.instInhabitedHomWorld.default = BarLev2021.HomWorld.neither

@[implicit_reducible]

instance BarLev2021.instInhabitedHomWorld : Inhabited HomWorld

Equations

• BarLev2021.instInhabitedHomWorld = { default := BarLev2021.instInhabitedHomWorld.default }

def BarLev2021.kellyLaughed : Set HomWorld

Kelly laughed (subdomain alternative for D = {Kelly}).

Equations

• BarLev2021.kellyLaughed BarLev2021.HomWorld.neither = False
• BarLev2021.kellyLaughed BarLev2021.HomWorld.onlyKelly = True
• BarLev2021.kellyLaughed BarLev2021.HomWorld.onlyJane = False
• BarLev2021.kellyLaughed BarLev2021.HomWorld.both = True

def BarLev2021.janeLaughed : Set HomWorld

Jane laughed (subdomain alternative for D = {Jane}).

Equations

• BarLev2021.janeLaughed BarLev2021.HomWorld.neither = False
• BarLev2021.janeLaughed BarLev2021.HomWorld.onlyKelly = False
• BarLev2021.janeLaughed BarLev2021.HomWorld.onlyJane = True
• BarLev2021.janeLaughed BarLev2021.HomWorld.both = True

def BarLev2021.someLaughed : Set HomWorld

The prejacent: ∃-PL_{D={Kelly,Jane}} P (the kids) = "some kid laughed." This is the basic existential meaning of "the kids laughed."

Equations

• BarLev2021.someLaughed BarLev2021.HomWorld.neither = False
• BarLev2021.someLaughed BarLev2021.HomWorld.onlyKelly = True
• BarLev2021.someLaughed BarLev2021.HomWorld.onlyJane = True
• BarLev2021.someLaughed BarLev2021.HomWorld.both = True

Grounding in ExistentialPL.lean

The propositions above are instances of the existPL operator from ExistentialPL.lean. We make this connection structural: each proposition is provably equivalent to existPL applied with the appropriate domain variable D.

inductive BarLev2021.Kid : Type

The two atoms of the plurality "the kids".

• kelly : Kid
• jane : Kid

@[implicit_reducible]

instance BarLev2021.instDecidableEqKid : DecidableEq Kid

Equations

• BarLev2021.instDecidableEqKid x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BarLev2021.instReprKid.repr : Kid → ℕ → Std.Format

Equations

• BarLev2021.instReprKid.repr BarLev2021.Kid.kelly prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BarLev2021.Kid.kelly")).group prec✝
• BarLev2021.instReprKid.repr BarLev2021.Kid.jane prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BarLev2021.Kid.jane")).group prec✝

@[implicit_reducible]

instance BarLev2021.instReprKid : Repr Kid

Equations

• BarLev2021.instReprKid = { reprPrec := BarLev2021.instReprKid.repr }

def BarLev2021.laughed : Kid → HomWorld → Prop

The predicate "laughed" as a function of atoms and worlds.

Equations

• BarLev2021.laughed BarLev2021.Kid.kelly = BarLev2021.kellyLaughed
• BarLev2021.laughed BarLev2021.Kid.jane = BarLev2021.janeLaughed

@[implicit_reducible]

instance BarLev2021.laughed.instDecidable (k : Kid) (w : HomWorld) : Decidable (laughed k w)

Equations

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

def BarLev2021.theKids : Finset Kid

The plurality "the kids" = {Kelly, Jane}.

Equations

• BarLev2021.theKids = {BarLev2021.Kid.kelly, BarLev2021.Kid.jane}

theorem BarLev2021.someLaughed_eq_existPL (w : HomWorld) : someLaughed w ↔ Semantics.Plurality.ExistentialPL.existPL theKids laughed theKids w

Grounding: someLaughed is the ∃-PL operator applied with full domain variable D = theKids.

theorem BarLev2021.kellyLaughed_eq_existPL (w : HomWorld) : kellyLaughed w ↔ Semantics.Plurality.ExistentialPL.existPL {Kid.kelly} laughed theKids w

Grounding: kellyLaughed is ∃-PL with singleton domain D = {Kelly}.

theorem BarLev2021.janeLaughed_eq_existPL (w : HomWorld) : janeLaughed w ↔ Semantics.Plurality.ExistentialPL.existPL {Kid.jane} laughed theKids w

Grounding: janeLaughed is ∃-PL with singleton domain D = {Jane}.

def BarLev2021.homAlt : Set (Set HomWorld)

The subdomain alternative set.

Full domain variable D = {Kelly, Jane}. Subdomain alternatives arise from D' ⊆ D:

• D' = {Kelly, Jane}: someLaughed (= prejacent)
• D' = {Kelly}: kellyLaughed
• D' = {Jane}: janeLaughed
• D' = ∅: trivially true (excluded as non-informative)

Crucially, the conjunction kellyLaughed ∧ janeLaughed is NOT in this set — the alternatives are not closed under ∧.

Equations

• BarLev2021.homAlt = {BarLev2021.someLaughed, BarLev2021.kellyLaughed, BarLev2021.janeLaughed}

def BarLev2021.homPrejacent : Set HomWorld

The prejacent: ∃-PL with full domain.

Equations

• BarLev2021.homPrejacent = BarLev2021.someLaughed

theorem BarLev2021.hom_not_closed : ¬∀ X ⊆ homAlt, ⋂₀ X ∈ homAlt

The subdomain alternatives are NOT closed under conjunction.

kellyLaughed ∧ janeLaughed (= "both laughed") is not equivalent to any member of homAlt. This is the structural property that enables the Exh^{IE+II} derivation, parallel to free choice.

IE Computation

For φ = someLaughed and ALT = {someLaughed, kellyLaughed, janeLaughed}:

There are two MC-sets (maximal sets of negated alternatives consistent with the prejacent):

• MC₁ = {φ, janeLaughedᶜ} — witness: onlyKelly
• MC₂ = {φ, kellyLaughedᶜ} — witness: onlyJane

The IE set is {a ∈ ALT : aᶜ ∈ every MC-set}. The intersection MC₁ ∩ MC₂ = {φ}, and since φᶜ is never in an MC-set (contradicts the prejacent), no alternative is innocently excludable.

More precisely: kellyLaughedᶜ ∉ MC₁ and janeLaughedᶜ ∉ MC₂, so neither individual alternative is in IE. And someLaughed = φ cannot be IE-excluded by definition.

This contrasts with free choice, where ◇(A ∧ B) IS IE-excludable. The difference: homAlt has only 3 elements (no conjunction member), while fcALT has 4 (including ◇(A ∧ B)).

theorem BarLev2021.nothing_ie (q : Set HomWorld) (hqIE : Exhaustification.IsInnocentlyExcludable homAlt homPrejacent q) : False

Nothing is innocently excludable in the homogeneity configuration.

This is the key difference from free choice, where ◇(A ∧ B) IS IE-excludable. Here, the alternatives lack a conjunction member entirely, so neither individual alternative can be consistently excluded from all MC-sets.

II Computation

Since IE = ∅ (nothing is excludable), the II constraint set is just {someLaughed} (the prejacent, with no IE negations).

All members of homAlt hold at .both, so adding any target to an II-compatible set R preserves II-compatibility (witness: .both).

Result: II = {kellyLaughed, janeLaughed} (and someLaughed, but the prejacent is already asserted).

theorem BarLev2021.kellyLaughed_ii : Exhaustification.IsInnocentlyIncludable homAlt homPrejacent kellyLaughed

kellyLaughed is innocently includable.

theorem BarLev2021.janeLaughed_ii : Exhaustification.IsInnocentlyIncludable homAlt homPrejacent janeLaughed

janeLaughed is innocently includable.

theorem BarLev2021.universality (w : HomWorld) : Exhaustification.exhIEII homAlt homPrejacent w → kellyLaughed w ∧ janeLaughed w

Universality from Exh^{IE+II}: exhaustified "the kids laughed" entails that both Kelly and Jane laughed.

Exh^{IE+II}(∃-PL_C(laughed)(the kids)) ⊢ ∀ x ∈ {K,J}. laughed(x)

This is the homogeneity derivation: the universal reading of a plural definite arises as an implicature, not from basic semantics.

Compare free_choice in Phenomena/Modality/Studies/BarLevFox2020.lean.

theorem BarLev2021.negative_universal (w : HomWorld) : ¬someLaughed w → ¬kellyLaughed w ∧ ¬janeLaughed w

Negative asymmetry: Under negation, the universal reading comes for free from the basic (existential) semantics: ¬∃x. laughed(x) ⊢ ∀x. ¬laughed(x).

No exhaustification needed — this is just the classical equivalence ¬∃ = ∀¬. This asymmetry between positive and negative is a key prediction that distinguishes the implicature account from trivalent theories (where both polarities are symmetric).

theorem BarLev2021.gap_both_false (w : HomWorld) : someLaughed w → ¬(kellyLaughed w ∧ janeLaughed w) → ¬Exhaustification.exhIEII homAlt homPrejacent w ∧ ¬¬someLaughed w

In a gap scenario (some but not all laughed), the positive sentence is false (universality fails) and the negative sentence is false (existence holds). This non-complementarity IS the homogeneity gap.

theorem BarLev2021.onlyKelly_is_gap : someLaughed HomWorld.onlyKelly ∧ ¬(kellyLaughed HomWorld.onlyKelly ∧ janeLaughed HomWorld.onlyKelly)

Witness: onlyKelly is a gap scenario.

theorem BarLev2021.onlyJane_is_gap : someLaughed HomWorld.onlyJane ∧ ¬(kellyLaughed HomWorld.onlyJane ∧ janeLaughed HomWorld.onlyJane)

Witness: onlyJane is a gap scenario.

Non-Maximality via Pruning

@cite{bar-lev-2021} §5 derives non-maximal readings via pruning: when context makes certain subdomain alternatives irrelevant, they are removed from ALT before exhaustification. With fewer alternatives, Exh^{IE+II} produces a weaker (non-maximal) reading.

The pruning spectrum for a 2-atom plurality {Kelly, Jane}:

ALT	Result
{φ, kellyL, janeL} (full)	Universal (both laughed)
{φ, janeL} (kelly pruned)	janeL excluded by IE
{φ, kellyL} (jane pruned)	kellyL excluded by IE
{φ} (fully pruned)	Existential (some kid laughed)

Note: with only 2 atoms, partial pruning yields exclusive readings (IE excludes the remaining alternative), not intermediate non-maximal readings. True non-maximality (e.g., "7 of 10 kids laughed" counting as "the kids laughed") requires ≥3 atoms, where pruning some but not all individual alternatives weakens the II result to something between existential and universal.

In the fire hazard context (NonMaximality.lean), the distinction between "all kids laughed" and "some kids laughed" is irrelevant, so ALL individual alternatives are pruned. Exh is then vacuous and the existential basic meaning surfaces directly.

def BarLev2021.prunedAlt : Set (Set HomWorld)

Fully pruned alternative set: only the prejacent remains.

Equations

• BarLev2021.prunedAlt = {BarLev2021.someLaughed}

theorem BarLev2021.pruned_existential (w : HomWorld) : Exhaustification.exhIEII prunedAlt homPrejacent w → someLaughed w

With a fully pruned alternative set, Exh^{IE+II} reduces to the basic existential meaning (no strengthening occurs).

theorem BarLev2021.existential_suffices_pruned (w : HomWorld) : someLaughed w → Exhaustification.exhIEII prunedAlt homPrejacent w

The converse: the basic meaning suffices for Exh with pruned alternatives.

theorem BarLev2021.pruning_weakens : (∀ (w : HomWorld), Exhaustification.exhIEII homAlt homPrejacent w → someLaughed w) ∧ ¬∀ (w : HomWorld), someLaughed w → Exhaustification.exhIEII homAlt homPrejacent w

Pruning strictly weakens the reading: the universal reading (full ALT) entails the existential reading (pruned ALT), but not vice versa.

def BarLev2021.partialPrunedAlt : Set (Set HomWorld)

Partially pruned alternative set: kellyLaughed removed, janeLaughed retained.

With this ALT = {φ, janeLaughed}, there is a single MC-set {φ, janeLaughedᶜ} (witness: onlyKelly). So janeLaughed ∈ IE, and Exh^{IE}(φ) = someLaughed ∧ ¬janeLaughed. The 2-atom case yields exclusive readings under partial pruning, not weakened universals. True non-maximal readings require ≥3 atoms.

Equations

• BarLev2021.partialPrunedAlt = {BarLev2021.someLaughed, BarLev2021.janeLaughed}

theorem BarLev2021.partial_pruning_not_universal : ¬∀ (w : HomWorld), Exhaustification.exhIEII partialPrunedAlt homPrejacent w → kellyLaughed w ∧ janeLaughed w

Partial pruning (removing kellyLaughed) does not yield universality.

Counterexample: .onlyKelly satisfies Exh^{IE+II} (janeLaughed is IE-excluded and someLaughed is II-included) but not the universal kellyLaughed ∧ janeLaughed.

theorem BarLev2021.matches_switches_data : Phenomena.Plurals.Homogeneity.switchesExample.positiveInAll = Phenomena.Plurals.Homogeneity.HomogeneityJudgment.clearlyTrue ∧ Phenomena.Plurals.Homogeneity.switchesExample.negativeInAll = Phenomena.Plurals.Homogeneity.HomogeneityJudgment.clearlyFalse ∧ Phenomena.Plurals.Homogeneity.switchesExample.positiveInNone = Phenomena.Plurals.Homogeneity.HomogeneityJudgment.clearlyFalse ∧ Phenomena.Plurals.Homogeneity.switchesExample.negativeInNone = Phenomena.Plurals.Homogeneity.HomogeneityJudgment.clearlyTrue ∧ Phenomena.Plurals.Homogeneity.switchesExample.positiveInGap = Phenomena.Plurals.Homogeneity.HomogeneityJudgment.neitherTrueNorFalse ∧ Phenomena.Plurals.Homogeneity.switchesExample.negativeInGap = Phenomena.Plurals.Homogeneity.HomogeneityJudgment.neitherTrueNorFalse

Bar-Lev's theory predicts the full truth-value pattern for the switches example: universal in ALL, denial in NONE, gap in between. This matches the empirical judgments in Homogeneity.lean.

theorem BarLev2021.is_implicature_account (t : Phenomena.Plurals.Multiplicity.PluralTheory) (h : t.usesSIMechanism = true) : t = Phenomena.Plurals.Multiplicity.PluralTheory.implicature

Bar-Lev's theory is an implicature account: any theory using the SI mechanism for multiplicity is uniquely identified as the implicature theory. Bar-Lev's exhaustification-based approach is precisely this.

Comparison with @cite{magri-2014}

Both Magri and Bar-Lev derive universality from exhaustification of an existential basic meaning. The key differences:

1. Magri: Uses double exhaustification (EXH(EXH(THE))) with non-transitive Horn-mateness to block THE from excluding ALL directly.

2. Bar-Lev: Uses single Exh^{IE+II} with subdomain alternatives. The key insight is that subdomain alternatives are not closed under ∧, which is what triggers II (Innocent Inclusion).

Bar-Lev's approach is more economical (one application of Exh, not two) and unifies homogeneity with free choice through a shared structural property (non-closure under ∧).

theorem BarLev2021.magri_agreement : Magri2014.primalMeaning Magri2014.Role.mystery = Magri2014.someMeaning ∧ Magri2014.effectiveInterpretation Magri2014.TheoryVariant.primal Features.Polarity.positive = Magri2014.Role.strong

Both theories agree that the basic meaning is existential and the strengthened meaning is universal. The key structural difference: Magri requires two applications of EXH (double exhaustification via non-transitive Horn-mateness), while Bar-Lev requires one application of Exh^{IE+II} (the richer operator compensates for fewer iterations). Bar-Lev's approach also unifies homogeneity with free choice through the shared structural property of non-closure under ∧.

How "All" Removes Homogeneity

@cite{bar-lev-2021} §8.3: "all the kids laughed" does not display homogeneity because all universally quantifies over the plurality, eliminating the domain variable D. Without D, there are no subdomain alternatives, so Exh^{IE+II} is vacuous — the universal reading is the basic meaning, not an implicature. Since it's not an implicature, it can't be weakened by pruning, which is why "all" blocks non-maximality.

This connects to Homogeneity.lean's HomogeneityRemover.all and to @cite{kriz-2016}'s removeGap (which collapses the truth-value gap into the negative extension — a different mechanism but the same empirical prediction).

theorem BarLev2021.all_removes_homogeneity_prediction : Phenomena.Plurals.Homogeneity.allRemovesHomogeneity.remover = Phenomena.Plurals.Homogeneity.HomogeneityRemover.all ∧ Phenomena.Plurals.Homogeneity.allRemovesHomogeneity.homogeneousJudgment = Phenomena.Plurals.Homogeneity.HomogeneityJudgment.neitherTrueNorFalse ∧ Phenomena.Plurals.Homogeneity.allRemovesHomogeneity.preciseJudgment = Phenomena.Plurals.Homogeneity.HomogeneityJudgment.clearlyFalse

Bar-Lev's theory predicts that "all" removes homogeneity: the allRemovesHomogeneity datum records that the gap scenario yields .clearlyFalse for "all the doors are open" (vs .neitherTrueNorFalse for the bare plural). This aligns with Bar-Lev's mechanism: "all" eliminates subdomain alternatives, making the universal reading semantic (not an implicature) and therefore non-cancelable.

theorem BarLev2021.all_exh_vacuous (w : HomWorld) : Exhaustification.exhIEII {homPrejacent} homPrejacent w ↔ someLaughed w

Without subdomain alternatives, exhaustification is vacuous: the prejacent passes through unchanged. This models the effect of all, which eliminates the domain variable D.

Comparison with @cite{kriz-2016} (Trivalent Account)

@cite{kriz-2016} and @cite{kriz-spector-2021} derive homogeneity from trivalent semantics: plural predication yields a three-valued denotation (true/false/gap), and non-maximality arises when the gap is pragmatically exploitable. The two accounts differ in:

Property	Bar-Lev (implicature)	Križ (trivalent)
Basic meaning	existential (∃-PL)	trivalent (T/F/gap)
Universal reading	implicature (Exh^{IE+II})	semantic (true extension)
Non-maximality	pruning alternatives	pragmatic gap exploitation
Positive/negative	asymmetric	symmetric
"All" removes gap	eliminates C variable	collapses gap (removeGap)

Key Distinguishing Prediction: Asymmetry

The most important empirical difference concerns the status of the universal inference under negation:

• Bar-Lev: Positive universality is an implicature (cancelable via pruning). Negative universality is semantic (¬∃ = ∀¬, no implicature involved). The two polarities are fundamentally asymmetric.

• Križ: Both positive and negative universality arise from the same source (gap collapse). The gap is symmetric: it exists for both "the kids laughed" and "the kids didn't laugh." Non-maximality is available for both polarities.

This asymmetry is captured by negative_universal above: under negation, the universal reading follows from basic semantics without exhaustification. Križ's trivalent account would instead derive both through the gap mechanism symmetrically.

theorem BarLev2021.positive_negative_asymmetry : (∃ (w : HomWorld), someLaughed w ∧ ¬(kellyLaughed w ∧ janeLaughed w)) ∧ ∀ (w : HomWorld), ¬someLaughed w → ¬kellyLaughed w ∧ ¬janeLaughed w

The positive–negative asymmetry: positive universality requires exhaustification, while negative universality does not.

This is a distinguishing prediction of the implicature account: universality needs the full Exh^{IE+II} machinery, but negative_universal is a simple logical entailment. In the trivalent account (@cite{kriz-2016}), both arise from the gap structure.

The §11 prose comparison is upgraded here to a kernel-checked divergence theorem: lift the BarLev Set HomWorld predicates into Bool-valued versions, instantiate Križ's barePluralTV over them, and demonstrate that at the gap-world onlyKelly:

• Križ's bare-plural is .indet (gap), and its Strong-Kleene negation is ALSO .indet (gap). So Križ's gap_enables_nonmax makes non-maximal use of the negation available in principle.
• Bar-Lev's negative_universal (above) makes ¬someLaughed straightforwardly bivalent — at onlyKelly it's FALSE (since some kid did laugh). No gap to exploit, so non-maximal use of negation is forbidden.

The two predictions cannot both be right: this is the kernel-visible form of the §11 polarities-symmetric vs. polarities-asymmetric disagreement.

theorem BarLev2021.kriz_bare_kids_onlyKelly_gap : Phenomena.Plurals.Studies.Kriz2016.barePluralTV laughed theKids HomWorld.onlyKelly = Core.Duality.Truth3.indet

At onlyKelly, Križ's bare-plural denotation of "the kids laughed" is a homogeneity gap (.indet) — Kelly laughed, Jane didn't.

theorem BarLev2021.kriz_neg_bare_kids_onlyKelly_gap : (Phenomena.Plurals.Studies.Kriz2016.barePluralTV laughed theKids HomWorld.onlyKelly).neg = Core.Duality.Truth3.indet

Križ's Strong-Kleene negation of a gap is also a gap. So the negation "the kids didn't laugh" at onlyKelly is .indet under Križ.

theorem BarLev2021.barlev_neg_someLaughed_onlyKelly_false : ¬¬someLaughed HomWorld.onlyKelly

Bar-Lev's negative_universal derives ¬someLaughed as bivalent: at onlyKelly, ¬someLaughed .onlyKelly is FALSE (Kelly laughed).

theorem BarLev2021.kriz_vs_barlev_negative_nonmax : (Phenomena.Plurals.Studies.Kriz2016.barePluralTV laughed theKids HomWorld.onlyKelly).neg = Core.Duality.Truth3.indet ∧ ¬¬someLaughed HomWorld.onlyKelly

Križ vs. Bar-Lev formal divergence on negative non-maximality. At the gap-world onlyKelly:

• Križ: negation of "the kids laughed" is .indet (Strong-Kleene preserves the gap). So gap_enables_nonmax makes non-maximal use of the negation in principle available — symmetric with the positive.
• Bar-Lev: ¬someLaughed is straightforwardly bivalent (¬∃ = ∀¬). At onlyKelly, ¬someLaughed is FALSE — no gap to exploit. The negation cannot be used non-maximally — asymmetric with positive.

The two clauses below cannot both be the right semantics for "the kids didn't laugh" at onlyKelly. The theorem's existence packages the formal disagreement that §11 §positive_negative_asymmetry describes in prose.