Magri (2014): Homogeneity Effects via Double Strengthening

@cite{magri-2014}

An account for the homogeneity effects triggered by plural definites and conjunction based on double strengthening. In Pragmatics, Semantics and the Case of Scalar Implicatures, ed. S. Pistoia Reda (Palgrave Macmillan), 99-145.

Core Idea

Plural definites like the boys have a plain existential semantics, equivalent to the indefinite some boys. Their universal reading arises through double strengthening modeled on @cite{spector-2007}:

1. The indefinite some boys triggers the "only-some" scalar implicature
2. The definite the boys triggers the implicature that this "only-some" implicature is false
3. The universal reading thus arises as a "not-only-some" implicature

No strengthening occurs in DE environments, where definites reveal their plain existential semantics --- producing homogeneity effects.

Formal Structure

The theory reduces to a three-element alternative configuration:

• MYSTERY: the item displaying homogeneity (THE / PL / AND_unF)
• WEAK: its semantically equivalent alternative (SOME / SING / OR)
• STRONG: the stronger alternative (ALL / TWO / BOTH)

The crucial asymmetry: MYSTERY and WEAK are Horn-mates, WEAK and STRONG are Horn-mates, but MYSTERY is NOT a Horn-mate of STRONG. Horn-mateness is non-transitive.

Double Exhaustification

The universal reading arises via two layers of EXH:

1. Inner EXH: SOME excludes ALL (standard SI), but THE has no excludable alternatives (ALL is not a Horn-mate, SOME is equivalent). So EXH(THE) = THE = SOME, EXH(SOME) = SOME AND NOT ALL.

2. Outer EXH: At the second level, EXH(SOME) = SOME AND NOT ALL is strictly stronger than EXH(THE) = SOME. Since SOME is a Horn-mate of THE, it becomes excludable at the outer level: EXH(EXH(THE)) = SOME AND NOT(SOME AND NOT ALL) = ALL.

Primal vs Dual

• Primal theory: MYSTERY has weak plain meaning, strengthened to STRONG in UE. Applies to definites and plural morphology.
• Dual theory: MYSTERY has strong plain meaning, weakened to WEAK in DE. Applies to unfocused conjunction.

Both derive the same net result: MYSTERY behaves as STRONG in UE, MYSTERY behaves as WEAK in DE.

Relationship to @cite{spector-2007}

Magri extends Spector's exhaustivity-based account of plural morphology (PL/SING/TWO) to plural definites (THE/SOME/ALL) and unfocused conjunction (AND_unF/OR/BOTH). The key technical innovation is assumption (19): using iterated exhaustification where the strengthened alternatives (not just plain meanings) determine outer-level excludability. Spector's single-EXH result Max(P) = {Exhaust(P)} is formalized in ScalarImplicatures/Studies/Spector2007.lean.

inductive Magri2014.Role : Type

The three items in a double-strengthening configuration.

Each concrete domain (definites, plural morphology, conjunction) provides a different instantiation.

• mystery : Role
• weak : Role
• strong : Role

def Magri2014.instReprRole.repr : Role → ℕ → Std.Format

Equations

• Magri2014.instReprRole.repr Magri2014.Role.mystery prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Magri2014.Role.mystery")).group prec✝
• Magri2014.instReprRole.repr Magri2014.Role.weak prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Magri2014.Role.weak")).group prec✝
• Magri2014.instReprRole.repr Magri2014.Role.strong prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Magri2014.Role.strong")).group prec✝

@[implicit_reducible]

instance Magri2014.instReprRole : Repr Role

Equations

• Magri2014.instReprRole = { reprPrec := Magri2014.instReprRole.repr }

@[implicit_reducible]

instance Magri2014.instDecidableEqRole : DecidableEq Role

Equations

• Magri2014.instDecidableEqRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Magri2014.instInhabitedRole.default : Role

Equations

• Magri2014.instInhabitedRole.default = Magri2014.Role.mystery

@[implicit_reducible]

instance Magri2014.instInhabitedRole : Inhabited Role

Equations

• Magri2014.instInhabitedRole = { default := Magri2014.instInhabitedRole.default }

def Magri2014.entails : Role → Role → Bool

Entailment structure between the three items. STRONG asymmetrically entails both WEAK and MYSTERY. MYSTERY and WEAK are semantically equivalent (mutual entailment).

Equations

• Magri2014.entails Magri2014.Role.strong x✝ = true
• Magri2014.entails Magri2014.Role.mystery Magri2014.Role.mystery = true
• Magri2014.entails Magri2014.Role.mystery Magri2014.Role.weak = true
• Magri2014.entails Magri2014.Role.weak Magri2014.Role.mystery = true
• Magri2014.entails Magri2014.Role.weak Magri2014.Role.weak = true
• Magri2014.entails x✝¹ x✝ = false

theorem Magri2014.mystery_equiv_weak : entails Role.mystery Role.weak = true ∧ entails Role.weak Role.mystery = true

MYSTERY and WEAK are semantically equivalent (mutual entailment).

theorem Magri2014.strong_asymm_entails_weak : entails Role.strong Role.weak = true ∧ entails Role.weak Role.strong = false

STRONG asymmetrically entails WEAK.

theorem Magri2014.strong_asymm_entails_mystery : entails Role.strong Role.mystery = true ∧ entails Role.mystery Role.strong = false

STRONG asymmetrically entails MYSTERY.

def Magri2014.hornMates : Role → Role → Bool

Horn-mateness: the non-transitive relation that determines which alternatives are relevant for exhaustification.

WEAK <-> STRONG: Horn-mates (standard scalar pair) WEAK <-> MYSTERY: Horn-mates (the definite competes with the indefinite) MYSTERY x STRONG: NOT Horn-mates (the crucial asymmetry!)

Equations

• Magri2014.hornMates Magri2014.Role.weak Magri2014.Role.strong = true
• Magri2014.hornMates Magri2014.Role.strong Magri2014.Role.weak = true
• Magri2014.hornMates Magri2014.Role.weak Magri2014.Role.mystery = true
• Magri2014.hornMates Magri2014.Role.mystery Magri2014.Role.weak = true
• Magri2014.hornMates x✝¹ x✝ = false

theorem Magri2014.mystery_not_mate_of_strong : hornMates Role.mystery Role.strong = false

theorem Magri2014.strong_not_mate_of_mystery : hornMates Role.strong Role.mystery = false

theorem Magri2014.weak_strong_mates : hornMates Role.weak Role.strong = true

theorem Magri2014.weak_mystery_mates : hornMates Role.weak Role.mystery = true

def Magri2014.innerExcludable (prejacent alt : Role) : Bool

The set of excludable alternatives at the inner (first) EXH level.

An alternative psi is excludable w.r.t. prejacent phi when:

1. psi is a Horn-mate of phi
2. psi asymmetrically entails phi (i.e., psi entails phi but phi does not entail psi)

Equations

• Magri2014.innerExcludable prejacent alt = (Magri2014.hornMates prejacent alt && Magri2014.entails alt prejacent && !Magri2014.entails prejacent alt)

theorem Magri2014.some_excludes_all : innerExcludable Role.weak Role.strong = true

theorem Magri2014.the_does_not_exclude_all : innerExcludable Role.mystery Role.strong = false

theorem Magri2014.the_does_not_exclude_some : innerExcludable Role.mystery Role.weak = false

theorem Magri2014.some_does_not_exclude_the : innerExcludable Role.weak Role.mystery = false

structure Magri2014.Scenario : Type

The semantic value of an item, in an abstract Boolean domain.

We model the "world" as having n individuals in a plurality, and a predicate P that holds of a given number of them. This lets us reason about SOME (>= 1), ALL (= n), and THE (= SOME by assumption).

• total : ℕ

  Total number of individuals in the plurality

• satisfying : ℕ

  Number satisfying the predicate

• valid : self.satisfying ≤ self.total

  satisfying <= total

@[implicit_reducible]

instance Magri2014.instReprScenario : Repr Scenario

Equations

• Magri2014.instReprScenario = { reprPrec := Magri2014.instReprScenario.repr }

def Magri2014.instReprScenario.repr : Scenario → ℕ → Std.Format

Equations

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

def Magri2014.someMeaning (s : Scenario) : Bool

SOME / MYSTERY: at least one satisfies (existential)

Equations

• Magri2014.someMeaning s = decide (s.satisfying ≥ 1)

def Magri2014.allMeaning (s : Scenario) : Bool

ALL / STRONG: all satisfy (universal)

Equations

• Magri2014.allMeaning s = (s.satisfying == s.total)

def Magri2014.primalMeaning : Role → Scenario → Bool

Plain meanings for each role in the PRIMAL theory (definites)

Equations

• Magri2014.primalMeaning Magri2014.Role.mystery = Magri2014.someMeaning
• Magri2014.primalMeaning Magri2014.Role.weak = Magri2014.someMeaning
• Magri2014.primalMeaning Magri2014.Role.strong = Magri2014.allMeaning

theorem Magri2014.mystery_eq_weak_meaning : primalMeaning Role.mystery = primalMeaning Role.weak

THE and SOME have the same plain meaning (the core assumption).

theorem Magri2014.strong_entails_weak (s : Scenario) (hn : s.total ≥ 1) : allMeaning s = true → someMeaning s = true

ALL entails SOME (if all satisfy, then at least one satisfies).

def Magri2014.exh (prejacent : Role) (s : Scenario) : Bool

EXH applied to a prejacent: assert the prejacent and negate all innerExcludable alternatives (@cite{spector-2007}, definition 18).

EXH(phi) = phi AND AND{NOT psi : psi innerExcludable w.r.t. phi}

Equations

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

theorem Magri2014.exh_some (s : Scenario) : exh Role.weak s = (someMeaning s && !allMeaning s)

EXH(SOME) = SOME AND NOT ALL

The standard "only some" scalar implicature: some but not all.

theorem Magri2014.exh_the (s : Scenario) : exh Role.mystery s = someMeaning s

EXH(THE) = THE = SOME

The definite has no innerExcludable alternatives (STRONG is not a Horn-mate, and WEAK is equivalent), so EXH is vacuous.

def Magri2014.outerExcludable : Role → Role → Bool

At the outer (second) EXH level, excludability uses Horn-mateness but checks entailment of STRENGTHENED meanings rather than plain meanings.

In the three-element configuration, the only outer-excludable pair is (MYSTERY, WEAK): EXH(SOME) = SOME AND NOT ALL is strictly stronger than EXH(THE) = SOME, and they are Horn-mates.

This is a derived fact, verified by exh_weak_strictly_stronger.

Equations

• Magri2014.outerExcludable Magri2014.Role.mystery Magri2014.Role.weak = true
• Magri2014.outerExcludable x✝¹ x✝ = false

theorem Magri2014.exh_weak_strictly_stronger : (∀ (s : Scenario), exh Role.weak s = true → exh Role.mystery s = true) ∧ ∃ (s : Scenario), exh Role.mystery s = true ∧ exh Role.weak s = false

EXH(WEAK) is strictly stronger than EXH(MYSTERY): EXH(SOME) = SOME ∧ ¬ALL entails EXH(THE) = SOME, but not vice versa.

This justifies outerExcludable .mystery .weak = true.

theorem Magri2014.outerExcludable_justified : hornMates Role.mystery Role.weak = true ∧ (∀ (s : Scenario), exh Role.weak s = true → exh Role.mystery s = true) ∧ ∃ (s : Scenario), exh Role.mystery s = true ∧ exh Role.weak s = false

The outer excludability assignment is justified by Horn-mateness plus asymmetric strengthened entailment.

def Magri2014.doubleExh (prejacent : Role) (s : Scenario) : Bool

Iterated EXH (assumption 19 in @cite{magri-2014}, extending @cite{spector-2007}): the strengthened meaning is computed through double exhaustification with outer-level excludability. The key innovation over @cite{spector-2007}'s single EXH is that the strengthened meanings of alternatives (not just plain meanings) determine excludability at the outer level.

doubleExh(phi) = EXH(phi) AND AND{NOT EXH(psi) : psi outerExcludable w.r.t. phi}

Equations

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

theorem Magri2014.double_strengthening_yields_universal (s : Scenario) (hn : s.total ≥ 1) : doubleExh Role.mystery s = allMeaning s

The main theorem: double exhaustification of THE yields ALL (given a non-vacuous plurality).

doubleExh(THE) = EXH(EXH(THE)) = EXH(THE) AND NOT EXH(SOME) -- outer EXH negates the Horn-mate = THE AND NOT(SOME AND NOT ALL) -- unpack inner EXH = SOME AND NOT(SOME AND NOT ALL) -- THE = SOME = SOME AND (NOT SOME OR ALL) -- De Morgan = ALL -- since SOME is asserted

The hypothesis s.total >= 1 excludes the vacuous case (empty plurality), where allMeaning is vacuously true but someMeaning is false. Vacuous definites ("the boys" when there are no boys) are presupposition failures.

def Magri2014.notMeaning (meaning : Scenario → Bool) (s : Scenario) : Bool

In DE environments (negation, restrictor of every, etc.), no strengthening occurs. The definite reveals its plain existential semantics.

NOT THE = NOT SOME

This is because in DE environments, the resulting matrix sentence already has the strongest meaning, so EXH is vacuous.

Equations

• Magri2014.notMeaning meaning s = !meaning s

theorem Magri2014.de_no_strengthening (s : Scenario) : notMeaning (primalMeaning Role.mystery) s = notMeaning (primalMeaning Role.weak) s

def Magri2014.isGap (s : Scenario) : Bool

A GAP scenario: some but not all individuals satisfy the predicate.

Equations

• Magri2014.isGap s = (Magri2014.someMeaning s && !Magri2014.allMeaning s)

theorem Magri2014.gap_positive_false (s : Scenario) (h : isGap s = true) : doubleExh Role.mystery s = false

In a GAP scenario, the strengthened meaning of the positive sentence (THE = ALL after double strengthening) is FALSE.

theorem Magri2014.gap_negative_false (s : Scenario) (h : isGap s = true) : notMeaning someMeaning s = false

In a GAP scenario, the strengthened meaning of the negative sentence (NOT THE = NOT SOME = NOT EXISTS) is also FALSE (since some DO satisfy).

theorem Magri2014.homogeneity_from_double_strengthening (s : Scenario) (h : isGap s = true) : doubleExh Role.mystery s = false ∧ notMeaning someMeaning s = false

Homogeneity derived: In GAP scenarios, both the positive and negative descriptions are false. The positive is false because ALL fails; the negative is false because SOME succeeds. This non-complementarity IS the homogeneity gap --- the definite is "neither clearly true nor clearly false."

inductive Magri2014.HomogeneityDomain : Type

The three domains unified by the double strengthening account.

• definites : HomogeneityDomain

  Plural definites: THE <-> SOME, ALL (primal)

• pluralMorphology : HomogeneityDomain

  Bare plural morphology: PL <-> SING, TWO (primal)

• conjunction : HomogeneityDomain

  Unfocused conjunction: AND_unF <-> OR, BOTH (dual)

@[implicit_reducible]

instance Magri2014.instReprHomogeneityDomain : Repr HomogeneityDomain

Equations

• Magri2014.instReprHomogeneityDomain = { reprPrec := Magri2014.instReprHomogeneityDomain.repr }

def Magri2014.instReprHomogeneityDomain.repr : HomogeneityDomain → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Magri2014.instDecidableEqHomogeneityDomain : DecidableEq HomogeneityDomain

Equations

• Magri2014.instDecidableEqHomogeneityDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Magri2014.DomainLabels : Type

The correspondence table from the paper: each domain instantiates the same three-element alternative structure.

MYSTERY	WEAK	STRONG
the boys	some boys	all/each of the boys
books (PL)	a book (SING)	two books (TWO)
Adam and Bill	Adam or Bill	both Adam and Bill

• domain : HomogeneityDomain
• mysteryLabel : String
• weakLabel : String
• strongLabel : String

def Magri2014.instReprDomainLabels.repr : DomainLabels → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Magri2014.instReprDomainLabels : Repr DomainLabels

Equations

• Magri2014.instReprDomainLabels = { reprPrec := Magri2014.instReprDomainLabels.repr }

def Magri2014.definiteLabels : DomainLabels

Equations

• Magri2014.definiteLabels = { domain := Magri2014.HomogeneityDomain.definites, mysteryLabel := "the boys", weakLabel := "some (of the) boys", strongLabel := "all/each of the boys" }

def Magri2014.pluralMorphLabels : DomainLabels

Equations

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

def Magri2014.conjunctionLabels : DomainLabels

Equations

• Magri2014.conjunctionLabels = { domain := Magri2014.HomogeneityDomain.conjunction, mysteryLabel := "Adam and_unF Bill", weakLabel := "Adam or Bill", strongLabel := "(both) Adam and_F Bill" }

def Magri2014.allDomains : List DomainLabels

Equations

• Magri2014.allDomains = [Magri2014.definiteLabels, Magri2014.pluralMorphLabels, Magri2014.conjunctionLabels]

inductive Magri2014.TheoryVariant : Type

Whether the domain uses the primal or dual version of the theory.

• Primal: MYSTERY starts weak (existential), gets strengthened to STRONG in UE
• Dual: MYSTERY starts strong (conjunctive), gets weakened to WEAK in DE

• primal : TheoryVariant
• dual : TheoryVariant

@[implicit_reducible]

instance Magri2014.instReprTheoryVariant : Repr TheoryVariant

Equations

• Magri2014.instReprTheoryVariant = { reprPrec := Magri2014.instReprTheoryVariant.repr }

def Magri2014.instReprTheoryVariant.repr : TheoryVariant → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Magri2014.instDecidableEqTheoryVariant : DecidableEq TheoryVariant

Equations

• Magri2014.instDecidableEqTheoryVariant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Magri2014.domainVariant : HomogeneityDomain → TheoryVariant

Equations

• Magri2014.domainVariant Magri2014.HomogeneityDomain.definites = Magri2014.TheoryVariant.primal
• Magri2014.domainVariant Magri2014.HomogeneityDomain.pluralMorphology = Magri2014.TheoryVariant.primal
• Magri2014.domainVariant Magri2014.HomogeneityDomain.conjunction = Magri2014.TheoryVariant.dual

def Magri2014.dualMeaning : Role → Scenario → Bool

Plain meanings in the DUAL theory (conjunction). In the dual, MYSTERY (AND_unF) starts with strong (conjunctive) plain meaning.

Equations

• Magri2014.dualMeaning Magri2014.Role.mystery = Magri2014.allMeaning
• Magri2014.dualMeaning Magri2014.Role.weak = Magri2014.someMeaning
• Magri2014.dualMeaning Magri2014.Role.strong = Magri2014.allMeaning

theorem Magri2014.primal_mystery_is_weak : primalMeaning Role.mystery = someMeaning

In the primal, MYSTERY starts weak and requires double EXH to reach STRONG.

theorem Magri2014.dual_mystery_is_strong : dualMeaning Role.mystery = allMeaning

In the dual, MYSTERY starts strong directly (no EXH needed in UE).

theorem Magri2014.primal_needs_exh_dual_doesnt (s : Scenario) (hn : s.total ≥ 1) : doubleExh Role.mystery s = allMeaning s ∧ dualMeaning Role.mystery s = allMeaning s

The primal requires double exhaustification to reach ALL, while the dual starts there directly. Both agree on the UE result.

def Magri2014.effectiveInterpretation (variant : TheoryVariant) (pol : Features.Polarity) : Role

The effective interpretation of MYSTERY in each polarity context.

In the primal theory (definites, plural morphology):

• UE: double strengthening yields STRONG (universal/plurality)
• DE: no strengthening, MYSTERY reveals WEAK (existential/singular)

In the dual theory (conjunction):

• UE: MYSTERY reveals STRONG (conjunctive) directly
• DE: double strengthening yields WEAK (disjunctive)

Equations

• Magri2014.effectiveInterpretation Magri2014.TheoryVariant.primal Features.Polarity.positive = Magri2014.Role.strong
• Magri2014.effectiveInterpretation Magri2014.TheoryVariant.primal Features.Polarity.negative = Magri2014.Role.weak
• Magri2014.effectiveInterpretation Magri2014.TheoryVariant.dual Features.Polarity.positive = Magri2014.Role.strong
• Magri2014.effectiveInterpretation Magri2014.TheoryVariant.dual Features.Polarity.negative = Magri2014.Role.weak

theorem Magri2014.primal_dual_agree : effectiveInterpretation TheoryVariant.primal = effectiveInterpretation TheoryVariant.dual

Both variants produce the same net result: MYSTERY behaves as STRONG in UE and as WEAK in DE.

structure Magri2014.SloppyExistentialPrediction : Type

Magri's conjecture: a matrix plural definite has a universal (existential) reading in a conversational context if and only if the corresponding indefinite triggers (does not trigger) the "only-some" scalar implicature.

A matrix definite THE has universal force <-> the indefinite SOME triggers SI

When the indefinite triggers no "only-some" implicature, there is nothing for the definite's second-order implicature to negate, so no strengthening occurs and the definite reveals its plain existential meaning.

• context : String

  Context description

• indefiniteTriggersSI : Bool

  Does the indefinite trigger "only-some" in this context?

• definiteUniversal : Bool

  Does the definite receive universal force?

@[implicit_reducible]

instance Magri2014.instReprSloppyExistentialPrediction : Repr SloppyExistentialPrediction

Equations

• Magri2014.instReprSloppyExistentialPrediction = { reprPrec := Magri2014.instReprSloppyExistentialPrediction.repr }

def Magri2014.instReprSloppyExistentialPrediction.repr : SloppyExistentialPrediction → ℕ → Std.Format

Equations

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

def Magri2014.sloppyPrediction (p : SloppyExistentialPrediction) : Bool

The prediction: these always agree.

Equations

• Magri2014.sloppyPrediction p = (p.indefiniteTriggersSI == p.definiteUniversal)

def Magri2014.classroomExample : SloppyExistentialPrediction

Classroom context: sloppy existential reading. Example attributed to Schlenker (p.c.) in @cite{gajewski-2005}.

Equations

• Magri2014.classroomExample = { context := "Three girls raise their hands. 'Wait, the girls have a question!'", indefiniteTriggersSI := false, definiteUniversal := false }

def Magri2014.standardExample : SloppyExistentialPrediction

Standard predication: universal reading.

Equations

• Magri2014.standardExample = { context := "Ten girls in a team each solve the problem. 'The girls solved the problem.'", indefiniteTriggersSI := true, definiteUniversal := true }

def Magri2014.sloppyExamples : List SloppyExistentialPrediction

Equations

• Magri2014.sloppyExamples = [Magri2014.classroomExample, Magri2014.standardExample]

theorem Magri2014.sloppy_prediction_holds : sloppyExamples.all sloppyPrediction = true

def Magri2014.switchesAll : Scenario

Concrete scenario instances for the switches example (10 switches).

Equations

• Magri2014.switchesAll = { total := 10, satisfying := 10, valid := Magri2014.switchesAll._proof_2 }

def Magri2014.switchesNone : Scenario

Equations

• Magri2014.switchesNone = { total := 10, satisfying := 0, valid := Magri2014.switchesNone._proof_2 }

def Magri2014.switchesGap : Scenario

Equations

• Magri2014.switchesGap = { total := 10, satisfying := 5, valid := Magri2014.switchesGap._proof_2 }

theorem Magri2014.switches_all_true : doubleExh Role.mystery switchesAll = true

In the ALL scenario, double strengthening gives the universal reading.

theorem Magri2014.switches_none_false : doubleExh Role.mystery switchesNone = false

In the NONE scenario, double strengthening fails (no individuals satisfy).

theorem Magri2014.switches_none_neg_true : notMeaning someMeaning switchesNone = true

In the NONE scenario, negation of existential gives true (none satisfy).

theorem Magri2014.switches_gap_homogeneity : doubleExh Role.mystery switchesGap = false ∧ notMeaning someMeaning switchesGap = false

In the GAP scenario, both positive (double-strengthened) and negative (plain existential under negation) are false --- the homogeneity gap.

theorem Magri2014.gap_matches_switches_data : Phenomena.Plurals.Homogeneity.switchesExample.positiveInGap = Phenomena.Plurals.Homogeneity.HomogeneityJudgment.neitherTrueNorFalse ∧ Phenomena.Plurals.Homogeneity.switchesExample.negativeInGap = Phenomena.Plurals.Homogeneity.HomogeneityJudgment.neitherTrueNorFalse

The gap derivation matches the empirical judgments in Homogeneity.lean: in the gap scenario, both positive and negative sentences are judged "neither true nor false."

theorem Magri2014.gap_matches_conjunction_data : Phenomena.Plurals.Homogeneity.conjunctionExample.positiveInGap = Phenomena.Plurals.Homogeneity.HomogeneityJudgment.neitherTrueNorFalse ∧ Phenomena.Plurals.Homogeneity.conjunctionExample.negativeInGap = Phenomena.Plurals.Homogeneity.HomogeneityJudgment.neitherTrueNorFalse

The conjunction domain also displays the same gap pattern.

theorem Magri2014.full_pattern_matches_switches : 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

Magri's theory accounts for the full truth-value pattern in the switches example: universal in ALL, denial in NONE, gap in between.

theorem Magri2014.primal_matches_monotonicity_pattern : effectiveInterpretation TheoryVariant.primal Features.Polarity.positive = Role.strong ∧ effectiveInterpretation TheoryVariant.primal Features.Polarity.negative = Role.weak ∧ Phenomena.Plurals.Multiplicity.pluralSingularParallel.arisesInUE = true ∧ Phenomena.Plurals.Multiplicity.pluralSingularParallel.arisesInDE = false

Magri's primal theory predicts strengthening in UE but not DE, matching the monotonicity pattern documented in Multiplicity.lean: the inference arises in UE (positive) contexts but not DE (negative).

theorem Magri2014.dual_matches_conjunction_parallel : effectiveInterpretation TheoryVariant.dual Features.Polarity.positive = Role.strong ∧ effectiveInterpretation TheoryVariant.dual Features.Polarity.negative = Role.weak ∧ Phenomena.Plurals.Multiplicity.orAndParallel.arisesInUE = true ∧ Phenomena.Plurals.Multiplicity.orAndParallel.arisesInDE = false

Magri's conjunction (dual) domain corresponds to the or/and monotonicity parallel in Multiplicity.lean.

Connection to @cite{fox-2007}'s Computable Algorithm

The abstract three-role computation above uses hand-coded innerExcludable and outerExcludable. Here we verify that Fox's computable innocent exclusion algorithm (exhB from InnocentExclusion.lean) applied twice produces the same result: double exhaustification yields the universal reading.

The key subtlety: exhB treats all alternatives in its list uniformly, so non-transitive Horn-mateness must be encoded in which alternatives are included in the list. THE and SOME get different alternative lists:

• THE's alternatives: [bSome] (only SOME is a Horn-mate; ALL is not)
• SOME's alternatives: [bSome, bAll] (both THE and ALL are Horn-mates)

inductive Magri2014.Sat : Type

Three worlds for a two-member plurality: none, one, or all satisfy.

• none : Sat
• one : Sat
• all : Sat

@[implicit_reducible]

instance Magri2014.instReprSat : Repr Sat

Equations

• Magri2014.instReprSat = { reprPrec := Magri2014.instReprSat.repr }

def Magri2014.instReprSat.repr : Sat → ℕ → Std.Format

Equations

• Magri2014.instReprSat.repr Magri2014.Sat.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Magri2014.Sat.none")).group prec✝
• Magri2014.instReprSat.repr Magri2014.Sat.one prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Magri2014.Sat.one")).group prec✝
• Magri2014.instReprSat.repr Magri2014.Sat.all prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Magri2014.Sat.all")).group prec✝

@[implicit_reducible]

instance Magri2014.instDecidableEqSat : DecidableEq Sat

Equations

• Magri2014.instDecidableEqSat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Magri2014.instFintypeSat : Fintype Sat

Equations

• Magri2014.instFintypeSat = { elems := { val := ↑Magri2014.Sat.enumList, nodup := Magri2014.Sat.enumList_nodup }, complete := Magri2014.instFintypeSat._proof_1 }

theorem Magri2014.fox_inner_exh_the : Exhaustification.innocent.exh (Exhaustification.altsFromPreds Magri2014.theAlts✝) (Exhaustification.predToFinset Magri2014.bSome✝) = Exhaustification.predToFinset Magri2014.bSome✝

Inner EXH(THE) = SOME: THE has no excludable alternatives because its only Horn-mate (SOME) is equivalent, not strictly stronger.

theorem Magri2014.fox_inner_exh_some : Exhaustification.innocent.exh (Exhaustification.altsFromPreds Magri2014.someAlts✝) (Exhaustification.predToFinset Magri2014.bSome✝) = Exhaustification.predToFinset fun (w : Sat) => Magri2014.bSome✝ w && !Magri2014.bAll✝ w

Inner EXH(SOME) = SOME ∧ ¬ALL: the standard "only some" SI.

theorem Magri2014.fox_double_exh_yields_all : Exhaustification.innocent.exh (Exhaustification.altsFromPreds Magri2014.outerAltsForThe✝) (Exhaustification.predToFinset Magri2014.innerThe✝) = Exhaustification.predToFinset Magri2014.bAll✝

Bridge theorem: Fox's exhaustification applied twice with the correct Horn-mate-restricted alternative sets yields the universal reading, matching double_strengthening_yields_universal.

EXH(EXH(THE)) = EXH(THE) ∧ ¬EXH(SOME) = SOME ∧ ¬(SOME ∧ ¬ALL) = ALL

Dual Theory: UE Is Trivial, DE Reveals Weak Meaning

In the dual theory (§5.5.2), MYSTERY (AND_unF) has a strong plain meaning (conjunction ≡ STRONG). In UE environments, the strong meaning is already maximal — no strengthening occurs (computation 55b: |||MYSTERY||| = [[MYSTERY]]).

In DE environments, the strong plain meaning under negation yields a weak global meaning. The abstract computation (55a) shows that double exhaustification of not·MYSTERY is vacuous:

|||not·MYSTERY||| = EXH(EXH(not·MYSTERY)) = not·MYSTERY = not·STRONG (since MYSTERY ≡ STRONG)

The vacuousness at the abstract level arises because MYSTERY ≡ STRONG means not·MYSTERY ≡ not·STRONG — there is no strictly stronger alternative to exclude. The concrete dual DE computation (61)/(72), which enriches the alternative set with atomic conjuncts LEFT and RIGHT, IS non-vacuous and derives not·OR. That computation is in Section 11.

This section verifies the abstract-level properties: inner EXH is vacuous for the dual MYSTERY, and gap scenarios show the expected pattern.

def Magri2014.dualExh (prejacent : Role) (s : Scenario) : Bool

Inner EXH in the dual theory.

Note: This reuses innerExcludable from the primal theory. The abstract three-role innerExcludable uses primal entailment (MYSTERY ≡ WEAK), while in the dual MYSTERY ≡ STRONG. However, the inner EXH results are the same for both theories at the abstract level: MYSTERY has no excludable alternatives, and WEAK excludes STRONG. The primal innerExcludable gives the right answer because neither theory allows MYSTERY to exclude anything at the inner level.

Equations

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

theorem Magri2014.dual_exh_mystery (s : Scenario) : dualExh Role.mystery s = allMeaning s

In the dual, EXH is vacuous for MYSTERY: no alternative is both a Horn-mate and asymmetrically stronger. This matches computation (55b): |||MYSTERY||| = [[MYSTERY]] = ALL.

theorem Magri2014.dual_exh_weak (s : Scenario) : dualExh Role.weak s = (someMeaning s && !allMeaning s)

In the dual, EXH(WEAK) = SOME ∧ ¬ALL (WEAK excludes STRONG). OR triggers "not-both" SI just as SOME triggers "not-all".

theorem Magri2014.dual_not_mystery_eq_not_strong (s : Scenario) : notMeaning (dualMeaning Role.mystery) s = notMeaning (dualMeaning Role.strong) s

NOT·MYSTERY in the dual = NOT·STRONG (since MYSTERY ≡ STRONG).

theorem Magri2014.dual_de_reveals_weak (s : Scenario) (_hn : s.total ≥ 1) (hgap : s.satisfying ≥ 1 ∧ s.satisfying < s.total) : notMeaning allMeaning s = true ∧ notMeaning someMeaning s = false

In a gap scenario, the dual DE reveals the weak meaning. not·MYSTERY = ¬ALL is true (not all satisfy), while not·SOME = ¬∃ is false (some do satisfy).

Enriched Alternatives for Conjunction (§A.7)

§A.7 adds the atomic conjuncts LEFT and RIGHT to the alternative set for unfocused conjunction, using @cite{fox-2007}'s definition of excludable alternatives. The crucial asymmetry (69b): AND_F has OR among its alternatives, but AND_unF does NOT. Non-transitive Horn-mateness is encoded by giving each prejacent its own alternative list.

This derives computation (72): in DE environments, unfocused conjunction behaves as disjunction: |||not·AND_unF||| = not·OR.

inductive Magri2014.ConjW : Type

Four worlds for two atomic propositions (saw Adam, saw Bill).

• neither : ConjW
• onlyA : ConjW
• onlyB : ConjW
• both : ConjW

@[implicit_reducible]

instance Magri2014.instReprConjW : Repr ConjW

Equations

• Magri2014.instReprConjW = { reprPrec := Magri2014.instReprConjW.repr }

def Magri2014.instReprConjW.repr : ConjW → ℕ → Std.Format

Equations

• Magri2014.instReprConjW.repr Magri2014.ConjW.neither prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Magri2014.ConjW.neither")).group prec✝
• Magri2014.instReprConjW.repr Magri2014.ConjW.onlyA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Magri2014.ConjW.onlyA")).group prec✝
• Magri2014.instReprConjW.repr Magri2014.ConjW.onlyB prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Magri2014.ConjW.onlyB")).group prec✝
• Magri2014.instReprConjW.repr Magri2014.ConjW.both prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Magri2014.ConjW.both")).group prec✝

@[implicit_reducible]

instance Magri2014.instDecidableEqConjW : DecidableEq ConjW

Equations

• Magri2014.instDecidableEqConjW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Magri2014.instFintypeConjW : Fintype ConjW

Equations

• Magri2014.instFintypeConjW = { elems := { val := ↑Magri2014.ConjW.enumList, nodup := Magri2014.ConjW.enumList_nodup }, complete := Magri2014.instFintypeConjW._proof_1 }

def Magri2014.cLeft : ConjW → Bool

Equations

• Magri2014.cLeft Magri2014.ConjW.onlyA = true
• Magri2014.cLeft Magri2014.ConjW.both = true
• Magri2014.cLeft x✝ = false

def Magri2014.cRight : ConjW → Bool

Equations

• Magri2014.cRight Magri2014.ConjW.onlyB = true
• Magri2014.cRight Magri2014.ConjW.both = true
• Magri2014.cRight x✝ = false

def Magri2014.cOr : ConjW → Bool

Equations

• Magri2014.cOr Magri2014.ConjW.neither = false
• Magri2014.cOr x✝ = true

def Magri2014.cAnd : ConjW → Bool

Equations

• Magri2014.cAnd Magri2014.ConjW.both = true
• Magri2014.cAnd x✝ = false

theorem Magri2014.exh_andUnF : Exhaustification.innocent.exh (Exhaustification.altsFromPreds Magri2014.andUnFAlts✝) (Exhaustification.predToFinset cAnd) = Exhaustification.predToFinset cAnd

EXH(AND_unF) = AND (vacuous: all alts are entailed by AND).

theorem Magri2014.exh_andF : Exhaustification.innocent.exh (Exhaustification.altsFromPreds Magri2014.andFAlts✝) (Exhaustification.predToFinset cAnd) = Exhaustification.predToFinset cAnd

EXH(AND_F) = AND (same: AND entails everything in its alt list).

theorem Magri2014.exh_left : Exhaustification.innocent.exh (Exhaustification.altsFromPreds Magri2014.leftAlts✝) (Exhaustification.predToFinset cLeft) = Exhaustification.predToFinset fun (w : ConjW) => cLeft w && !cRight w

EXH(LEFT) = LEFT ∧ ¬RIGHT (RIGHT is the only IE alternative).

theorem Magri2014.exh_right : Exhaustification.innocent.exh (Exhaustification.altsFromPreds Magri2014.rightAlts✝) (Exhaustification.predToFinset cRight) = Exhaustification.predToFinset fun (w : ConjW) => cRight w && !cLeft w

EXH(RIGHT) = RIGHT ∧ ¬LEFT (symmetric).

def Magri2014.nAnd : ConjW → Bool

Equations

• Magri2014.nAnd w = !Magri2014.cAnd w

def Magri2014.nOr : ConjW → Bool

Equations

• Magri2014.nOr w = !Magri2014.cOr w

theorem Magri2014.de_exh_notAndUnF : Exhaustification.innocent.exh (Exhaustification.altsFromPreds Magri2014.nAndUnFAlts✝) (Exhaustification.predToFinset nAnd) = Exhaustification.predToFinset nAnd

(71b) EXH(not·AND_unF) = not·AND (vacuous inner EXH). Neither not·LEFT nor not·RIGHT is IE: excluding one forces including the other, since ¬AND ∧ LEFT ∧ RIGHT is inconsistent.

theorem Magri2014.de_exh_notAndF : Exhaustification.innocent.exh (Exhaustification.altsFromPreds Magri2014.nAndFAlts✝) (Exhaustification.predToFinset nAnd) = Exhaustification.predToFinset fun (w : ConjW) => nAnd w && cOr w

(71a) EXH(not·AND_F) = not·AND ∧ ¬not·OR = not·AND ∧ OR. not·OR is IE (the only alternative not entailed by not·AND_F that can be consistently excluded).

theorem Magri2014.de_exh_notLeft : Exhaustification.innocent.exh (Exhaustification.altsFromPreds Magri2014.nLeftAlts✝) (Exhaustification.predToFinset Magri2014.nLeft✝) = Exhaustification.predToFinset fun (w : ConjW) => Magri2014.nLeft✝ w && cOr w && cRight w

(71c) EXH(not·LEFT) = not·LEFT ∧ OR ∧ RIGHT.

theorem Magri2014.de_exh_notRight : Exhaustification.innocent.exh (Exhaustification.altsFromPreds Magri2014.nRightAlts✝) (Exhaustification.predToFinset Magri2014.nRight✝) = Exhaustification.predToFinset fun (w : ConjW) => Magri2014.nRight✝ w && cOr w && cLeft w

(71d) EXH(not·RIGHT) = not·RIGHT ∧ OR ∧ LEFT.

def Magri2014.outerNAndUnFAlts : List (ConjW → Bool)

Outer-level alternatives for not·AND_unF: the exhaustified forms of its Horn-mates {not·AND_F, not·LEFT, not·RIGHT}.

Equations

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

def Magri2014.innerNAndUnF : ConjW → Bool

The inner EXH result for not·AND_unF (= not·AND, vacuous).

Equations

• Magri2014.innerNAndUnF w = decide (w ∈ Exhaustification.innocent.exh (Exhaustification.altsFromPreds Magri2014.nAndUnFAlts✝) (Exhaustification.predToFinset Magri2014.nAnd))

theorem Magri2014.de_double_exh_conjunction : Exhaustification.innocent.exh (Exhaustification.altsFromPreds outerNAndUnFAlts) (Exhaustification.predToFinset innerNAndUnF) = Exhaustification.predToFinset nOr

Computation (72): Double exhaustification of not·AND_unF yields not·OR.

|||not·AND_unF||| = EXH(EXH(not·AND_unF)) = not·AND ∧ ¬EXH(not·AND_F) ∧ ¬EXH(not·LEFT) ∧ ¬EXH(not·RIGHT) = not·AND ∧ ¬(not·AND ∧ OR) ∧ ... = not·AND ∧ (AND ∨ ¬OR) ∧ ... = not·AND ∧ ¬OR (since not·AND is asserted) = not·OR

Unfocused conjunction in DE environments behaves as disjunction.

Uniform Double Strengthening over Theory Variants

The primal and dual theories share the same abstract mechanism — a three-element alternative configuration with non-transitive Horn-mateness. We unify them into a single uniformResult function that takes a TheoryVariant and returns the effective meaning in each polarity.

def Magri2014.uniformResult (v : TheoryVariant) (pol : Features.Polarity) : Scenario → Bool

The effective meaning of MYSTERY in each polarity, parameterized by theory variant. Both variants produce the same result: STRONG (= ALL) in UE, WEAK (= SOME) in DE.

Equations

• Magri2014.uniformResult Magri2014.TheoryVariant.primal Features.Polarity.positive = Magri2014.allMeaning
• Magri2014.uniformResult Magri2014.TheoryVariant.primal Features.Polarity.negative = Magri2014.someMeaning
• Magri2014.uniformResult Magri2014.TheoryVariant.dual Features.Polarity.positive = Magri2014.allMeaning
• Magri2014.uniformResult Magri2014.TheoryVariant.dual Features.Polarity.negative = Magri2014.someMeaning

theorem Magri2014.uniform_primal_dual_agree (pol : Features.Polarity) : uniformResult TheoryVariant.primal pol = uniformResult TheoryVariant.dual pol

Primal and dual give the same effective meaning in both polarities.

theorem Magri2014.uniform_primal_ue (s : Scenario) (hn : s.total ≥ 1) : uniformResult TheoryVariant.primal Features.Polarity.positive s = doubleExh Role.mystery s

The primal UE result matches double_strengthening_yields_universal.

theorem Magri2014.uniform_dual_ue (s : Scenario) : uniformResult TheoryVariant.dual Features.Polarity.positive s = dualMeaning Role.mystery s

The dual UE result matches the plain meaning of MYSTERY in the dual.

theorem Magri2014.uniform_primal_de (s : Scenario) : uniformResult TheoryVariant.primal Features.Polarity.negative s = primalMeaning Role.mystery s

The primal DE result matches the plain existential meaning.

theorem Magri2014.uniform_gap (v : TheoryVariant) (s : Scenario) (_hn : s.total ≥ 1) (hgap : s.satisfying ≥ 1 ∧ s.satisfying < s.total) : uniformResult v Features.Polarity.positive s = false ∧ notMeaning (uniformResult v Features.Polarity.negative) s = false

The homogeneity pattern: in gap scenarios, MYSTERY is false under both polarities regardless of theory variant.

Questions: A Testable Distinction (§5.5.4)

Benjamin Spector (p.c., cited in §5.5.4) observes that questions provide an environment where no strengthening occurs — they do not license scalar implicatures. Under this assumption:

• Primal MYSTERY has weak plain meaning (existential) → questions should reveal existential force for definites.
• Dual MYSTERY has strong plain meaning (conjunctive) → questions should reveal conjunctive force for unfocused conjunction.

The paper offers preliminary data supporting this prediction: definites in questions allow existential answers (62b), while unfocused conjunction in questions resists disjunctive answers (63b).

def Magri2014.mysteryInQuestions (v : TheoryVariant) : Role

In questions (no strengthening), the theory variant determines what force MYSTERY displays: primal → weak, dual → strong.

Equations

• Magri2014.mysteryInQuestions Magri2014.TheoryVariant.primal = Magri2014.Role.weak
• Magri2014.mysteryInQuestions Magri2014.TheoryVariant.dual = Magri2014.Role.strong

theorem Magri2014.questions_differentiate : mysteryInQuestions TheoryVariant.primal ≠ mysteryInQuestions TheoryVariant.dual

Questions differentiate the theories: primal MYSTERY shows WEAK, dual MYSTERY shows STRONG.

theorem Magri2014.definites_existential_in_questions : mysteryInQuestions (domainVariant HomogeneityDomain.definites) = Role.weak

Definites (primal) should have existential force in questions.

theorem Magri2014.conjunction_conjunctive_in_questions : mysteryInQuestions (domainVariant HomogeneityDomain.conjunction) = Role.strong

Unfocused conjunction (dual) should have conjunctive force in questions.

structure Magri2014.QuestionForceDatum : Type

Datum: "Did you talk to the students?" admits existential answer.

• question : String
• domain : HomogeneityDomain
• variant : TheoryVariant
• predictedForce : Role
• supported : Bool

  Data point: is the prediction borne out?

def Magri2014.instReprQuestionForceDatum.repr : QuestionForceDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Magri2014.instReprQuestionForceDatum : Repr QuestionForceDatum

Equations

• Magri2014.instReprQuestionForceDatum = { reprPrec := Magri2014.instReprQuestionForceDatum.repr }

def Magri2014.definitesQuestion : QuestionForceDatum

Equations

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

def Magri2014.conjunctionQuestion : QuestionForceDatum

Equations

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

theorem Magri2014.question_data_supports : ([definitesQuestion, conjunctionQuestion].all fun (x : QuestionForceDatum) => x.supported) = true

Both question data points support the primal/dual distinction.

Connecting Enriched Conjunction to Empirical Data

The de_double_exh_conjunction theorem (Section 11) shows that unfocused conjunction under negation behaves as disjunction on the ConjW domain. Here we verify that this result matches the gap pattern documented in Homogeneity.lean's conjunctionExample: in the gap scenario (Ann has red hair, Bert doesn't), both the positive conjunction and its negation are "neither true nor false."

theorem Magri2014.conj_gap_positive_false : (Magri2014.conjGapWorlds✝.all fun (w : ConjW) => decide (cAnd w = false)) = true

In the gap, positive conjunction (AND) is false.

theorem Magri2014.conj_gap_dual_negative_false : (Magri2014.conjGapWorlds✝.all fun (w : ConjW) => decide (nOr w = false)) = true

In the gap, negative conjunction with enriched dual theory gives not·OR (= "saw neither"). This is FALSE in the gap (she DID see one of them), producing the homogeneity gap.

theorem Magri2014.conj_gap_matches_empirical_data : Phenomena.Plurals.Homogeneity.conjunctionExample.positiveInGap = Phenomena.Plurals.Homogeneity.HomogeneityJudgment.neitherTrueNorFalse ∧ Phenomena.Plurals.Homogeneity.conjunctionExample.negativeInGap = Phenomena.Plurals.Homogeneity.HomogeneityJudgment.neitherTrueNorFalse

This matches the empirical data: conjunction gap is neither-true-nor-false for both polarities.

theorem Magri2014.enriched_conjunction_end_to_end : Exhaustification.innocent.exh (Exhaustification.altsFromPreds outerNAndUnFAlts) (Exhaustification.predToFinset innerNAndUnF) = Exhaustification.predToFinset nOr ∧ cAnd ConjW.onlyA = false ∧ nOr ConjW.onlyA = false ∧ Phenomena.Plurals.Homogeneity.conjunctionExample.positiveInGap = Phenomena.Plurals.Homogeneity.HomogeneityJudgment.neitherTrueNorFalse ∧ Phenomena.Plurals.Homogeneity.conjunctionExample.negativeInGap = Phenomena.Plurals.Homogeneity.HomogeneityJudgment.neitherTrueNorFalse

Full end-to-end: the enriched conjunction computation produces truth values that correspond to the homogeneity gap pattern.