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 Phenomena.Plurals.Studies.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

instance Phenomena.Plurals.Studies.Magri2014.instReprRole : Repr Role

Equations

• Phenomena.Plurals.Studies.Magri2014.instReprRole = { reprPrec := Phenomena.Plurals.Studies.Magri2014.instReprRole.repr }

def Phenomena.Plurals.Studies.Magri2014.instReprRole.repr : Role → Nat → Std.Format

Equations

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

instance Phenomena.Plurals.Studies.Magri2014.instDecidableEqRole : DecidableEq Role

Equations

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

instance Phenomena.Plurals.Studies.Magri2014.instBEqRole : BEq Role

Equations

• Phenomena.Plurals.Studies.Magri2014.instBEqRole = { beq := Phenomena.Plurals.Studies.Magri2014.instBEqRole.beq }

def Phenomena.Plurals.Studies.Magri2014.instBEqRole.beq : Role → Role → Bool

Equations

• Phenomena.Plurals.Studies.Magri2014.instBEqRole.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Plurals.Studies.Magri2014.instInhabitedRole.default : Role

Equations

• Phenomena.Plurals.Studies.Magri2014.instInhabitedRole.default = Phenomena.Plurals.Studies.Magri2014.Role.mystery

instance Phenomena.Plurals.Studies.Magri2014.instInhabitedRole : Inhabited Role

Equations

• Phenomena.Plurals.Studies.Magri2014.instInhabitedRole = { default := Phenomena.Plurals.Studies.Magri2014.instInhabitedRole.default }

def Phenomena.Plurals.Studies.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

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

theorem Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.Magri2014.strong_asymm_entails_weak : entails Role.strong Role.weak = true ∧ entails Role.weak Role.strong = false

STRONG asymmetrically entails WEAK.

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

STRONG asymmetrically entails MYSTERY.

def Phenomena.Plurals.Studies.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

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

theorem Phenomena.Plurals.Studies.Magri2014.mystery_not_mate_of_strong : hornMates Role.mystery Role.strong = false

theorem Phenomena.Plurals.Studies.Magri2014.strong_not_mate_of_mystery : hornMates Role.strong Role.mystery = false

theorem Phenomena.Plurals.Studies.Magri2014.weak_strong_mates : hornMates Role.weak Role.strong = true

theorem Phenomena.Plurals.Studies.Magri2014.weak_mystery_mates : hornMates Role.weak Role.mystery = true

def Phenomena.Plurals.Studies.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

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

theorem Phenomena.Plurals.Studies.Magri2014.some_excludes_all : innerExcludable Role.weak Role.strong = true

theorem Phenomena.Plurals.Studies.Magri2014.the_does_not_exclude_all : innerExcludable Role.mystery Role.strong = false

theorem Phenomena.Plurals.Studies.Magri2014.the_does_not_exclude_some : innerExcludable Role.mystery Role.weak = false

theorem Phenomena.Plurals.Studies.Magri2014.some_does_not_exclude_the : innerExcludable Role.weak Role.mystery = false

structure Phenomena.Plurals.Studies.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 : Nat

  Total number of individuals in the plurality

• satisfying : Nat

  Number satisfying the predicate

• valid : self.satisfying ≤ self.total

  satisfying <= total

instance Phenomena.Plurals.Studies.Magri2014.instReprScenario : Repr Scenario

Equations

• Phenomena.Plurals.Studies.Magri2014.instReprScenario = { reprPrec := Phenomena.Plurals.Studies.Magri2014.instReprScenario.repr }

def Phenomena.Plurals.Studies.Magri2014.instReprScenario.repr : Scenario → Nat → Std.Format

Equations

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

def Phenomena.Plurals.Studies.Magri2014.someMeaning (s : Scenario) : Bool

SOME / MYSTERY: at least one satisfies (existential)

Equations

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

def Phenomena.Plurals.Studies.Magri2014.allMeaning (s : Scenario) : Bool

ALL / STRONG: all satisfy (universal)

Equations

• Phenomena.Plurals.Studies.Magri2014.allMeaning s = (s.satisfying == s.total)

def Phenomena.Plurals.Studies.Magri2014.primalMeaning : Role → Scenario → Bool

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

Equations

• Phenomena.Plurals.Studies.Magri2014.primalMeaning Phenomena.Plurals.Studies.Magri2014.Role.mystery = Phenomena.Plurals.Studies.Magri2014.someMeaning
• Phenomena.Plurals.Studies.Magri2014.primalMeaning Phenomena.Plurals.Studies.Magri2014.Role.weak = Phenomena.Plurals.Studies.Magri2014.someMeaning
• Phenomena.Plurals.Studies.Magri2014.primalMeaning Phenomena.Plurals.Studies.Magri2014.Role.strong = Phenomena.Plurals.Studies.Magri2014.allMeaning

theorem Phenomena.Plurals.Studies.Magri2014.mystery_eq_weak_meaning : primalMeaning Role.mystery = primalMeaning Role.weak

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

theorem Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.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

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

theorem Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.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

• Phenomena.Plurals.Studies.Magri2014.notMeaning meaning s = !meaning s

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

def Phenomena.Plurals.Studies.Magri2014.isGap (s : Scenario) : Bool

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

Equations

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

theorem Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.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)

instance Phenomena.Plurals.Studies.Magri2014.instReprHomogeneityDomain : Repr HomogeneityDomain

Equations

• Phenomena.Plurals.Studies.Magri2014.instReprHomogeneityDomain = { reprPrec := Phenomena.Plurals.Studies.Magri2014.instReprHomogeneityDomain.repr }

def Phenomena.Plurals.Studies.Magri2014.instReprHomogeneityDomain.repr : HomogeneityDomain → Nat → Std.Format

Equations

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

instance Phenomena.Plurals.Studies.Magri2014.instDecidableEqHomogeneityDomain : DecidableEq HomogeneityDomain

Equations

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

instance Phenomena.Plurals.Studies.Magri2014.instBEqHomogeneityDomain : BEq HomogeneityDomain

Equations

• Phenomena.Plurals.Studies.Magri2014.instBEqHomogeneityDomain = { beq := Phenomena.Plurals.Studies.Magri2014.instBEqHomogeneityDomain.beq }

def Phenomena.Plurals.Studies.Magri2014.instBEqHomogeneityDomain.beq : HomogeneityDomain → HomogeneityDomain → Bool

Equations

• Phenomena.Plurals.Studies.Magri2014.instBEqHomogeneityDomain.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Phenomena.Plurals.Studies.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

instance Phenomena.Plurals.Studies.Magri2014.instReprDomainLabels : Repr DomainLabels

Equations

• Phenomena.Plurals.Studies.Magri2014.instReprDomainLabels = { reprPrec := Phenomena.Plurals.Studies.Magri2014.instReprDomainLabels.repr }

def Phenomena.Plurals.Studies.Magri2014.instReprDomainLabels.repr : DomainLabels → Nat → Std.Format

Equations

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

def Phenomena.Plurals.Studies.Magri2014.definiteLabels : DomainLabels

Equations

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

def Phenomena.Plurals.Studies.Magri2014.pluralMorphLabels : DomainLabels

Equations

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

def Phenomena.Plurals.Studies.Magri2014.conjunctionLabels : DomainLabels

Equations

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

def Phenomena.Plurals.Studies.Magri2014.allDomains : List DomainLabels

Equations

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

inductive Phenomena.Plurals.Studies.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

instance Phenomena.Plurals.Studies.Magri2014.instReprTheoryVariant : Repr TheoryVariant

Equations

• Phenomena.Plurals.Studies.Magri2014.instReprTheoryVariant = { reprPrec := Phenomena.Plurals.Studies.Magri2014.instReprTheoryVariant.repr }

def Phenomena.Plurals.Studies.Magri2014.instReprTheoryVariant.repr : TheoryVariant → Nat → Std.Format

Equations

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

instance Phenomena.Plurals.Studies.Magri2014.instDecidableEqTheoryVariant : DecidableEq TheoryVariant

Equations

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

def Phenomena.Plurals.Studies.Magri2014.instBEqTheoryVariant.beq : TheoryVariant → TheoryVariant → Bool

Equations

• Phenomena.Plurals.Studies.Magri2014.instBEqTheoryVariant.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Plurals.Studies.Magri2014.instBEqTheoryVariant : BEq TheoryVariant

Equations

• Phenomena.Plurals.Studies.Magri2014.instBEqTheoryVariant = { beq := Phenomena.Plurals.Studies.Magri2014.instBEqTheoryVariant.beq }

def Phenomena.Plurals.Studies.Magri2014.domainVariant : HomogeneityDomain → TheoryVariant

Equations

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

def Phenomena.Plurals.Studies.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

• Phenomena.Plurals.Studies.Magri2014.dualMeaning Phenomena.Plurals.Studies.Magri2014.Role.mystery = Phenomena.Plurals.Studies.Magri2014.allMeaning
• Phenomena.Plurals.Studies.Magri2014.dualMeaning Phenomena.Plurals.Studies.Magri2014.Role.weak = Phenomena.Plurals.Studies.Magri2014.someMeaning
• Phenomena.Plurals.Studies.Magri2014.dualMeaning Phenomena.Plurals.Studies.Magri2014.Role.strong = Phenomena.Plurals.Studies.Magri2014.allMeaning

theorem Phenomena.Plurals.Studies.Magri2014.primal_mystery_is_weak : primalMeaning Role.mystery = someMeaning

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

theorem Phenomena.Plurals.Studies.Magri2014.dual_mystery_is_strong : dualMeaning Role.mystery = allMeaning

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

theorem Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.Magri2014.effectiveInterpretation (variant : TheoryVariant) (pol : Core.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

• Phenomena.Plurals.Studies.Magri2014.effectiveInterpretation Phenomena.Plurals.Studies.Magri2014.TheoryVariant.primal Core.Polarity.positive = Phenomena.Plurals.Studies.Magri2014.Role.strong
• Phenomena.Plurals.Studies.Magri2014.effectiveInterpretation Phenomena.Plurals.Studies.Magri2014.TheoryVariant.primal Core.Polarity.negative = Phenomena.Plurals.Studies.Magri2014.Role.weak
• Phenomena.Plurals.Studies.Magri2014.effectiveInterpretation Phenomena.Plurals.Studies.Magri2014.TheoryVariant.dual Core.Polarity.positive = Phenomena.Plurals.Studies.Magri2014.Role.strong
• Phenomena.Plurals.Studies.Magri2014.effectiveInterpretation Phenomena.Plurals.Studies.Magri2014.TheoryVariant.dual Core.Polarity.negative = Phenomena.Plurals.Studies.Magri2014.Role.weak

theorem Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.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?

instance Phenomena.Plurals.Studies.Magri2014.instReprSloppyExistentialPrediction : Repr SloppyExistentialPrediction

Equations

• Phenomena.Plurals.Studies.Magri2014.instReprSloppyExistentialPrediction = { reprPrec := Phenomena.Plurals.Studies.Magri2014.instReprSloppyExistentialPrediction.repr }

def Phenomena.Plurals.Studies.Magri2014.instReprSloppyExistentialPrediction.repr : SloppyExistentialPrediction → Nat → Std.Format

Equations

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

def Phenomena.Plurals.Studies.Magri2014.sloppyPrediction (p : SloppyExistentialPrediction) : Bool

The prediction: these always agree.

Equations

• Phenomena.Plurals.Studies.Magri2014.sloppyPrediction p = (p.indefiniteTriggersSI == p.definiteUniversal)

def Phenomena.Plurals.Studies.Magri2014.classroomExample : SloppyExistentialPrediction

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

Equations

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

def Phenomena.Plurals.Studies.Magri2014.standardExample : SloppyExistentialPrediction

Standard predication: universal reading.

Equations

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

def Phenomena.Plurals.Studies.Magri2014.sloppyExamples : List SloppyExistentialPrediction

Equations

• Phenomena.Plurals.Studies.Magri2014.sloppyExamples = [Phenomena.Plurals.Studies.Magri2014.classroomExample, Phenomena.Plurals.Studies.Magri2014.standardExample]

theorem Phenomena.Plurals.Studies.Magri2014.sloppy_prediction_holds : sloppyExamples.all sloppyPrediction = true

def Phenomena.Plurals.Studies.Magri2014.switchesAll : Scenario

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

Equations

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

def Phenomena.Plurals.Studies.Magri2014.switchesNone : Scenario

Equations

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

def Phenomena.Plurals.Studies.Magri2014.switchesGap : Scenario

Equations

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

theorem Phenomena.Plurals.Studies.Magri2014.switches_all_true : doubleExh Role.mystery switchesAll = true

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

theorem Phenomena.Plurals.Studies.Magri2014.switches_none_false : doubleExh Role.mystery switchesNone = false

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

theorem Phenomena.Plurals.Studies.Magri2014.switches_none_neg_true : notMeaning someMeaning switchesNone = true

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

theorem Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.Magri2014.gap_matches_switches_data : Homogeneity.switchesExample.positiveInGap = Homogeneity.HomogeneityJudgment.neitherTrueNorFalse ∧ Homogeneity.switchesExample.negativeInGap = 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 Phenomena.Plurals.Studies.Magri2014.gap_matches_conjunction_data : Homogeneity.conjunctionExample.positiveInGap = Homogeneity.HomogeneityJudgment.neitherTrueNorFalse ∧ Homogeneity.conjunctionExample.negativeInGap = Homogeneity.HomogeneityJudgment.neitherTrueNorFalse

The conjunction domain also displays the same gap pattern.

theorem Phenomena.Plurals.Studies.Magri2014.full_pattern_matches_switches : Homogeneity.switchesExample.positiveInAll = Homogeneity.HomogeneityJudgment.clearlyTrue ∧ Homogeneity.switchesExample.negativeInAll = Homogeneity.HomogeneityJudgment.clearlyFalse ∧ Homogeneity.switchesExample.positiveInNone = Homogeneity.HomogeneityJudgment.clearlyFalse ∧ Homogeneity.switchesExample.negativeInNone = Homogeneity.HomogeneityJudgment.clearlyTrue ∧ Homogeneity.switchesExample.positiveInGap = Homogeneity.HomogeneityJudgment.neitherTrueNorFalse ∧ Homogeneity.switchesExample.negativeInGap = 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 Phenomena.Plurals.Studies.Magri2014.primal_matches_monotonicity_pattern : effectiveInterpretation TheoryVariant.primal Core.Polarity.positive = Role.strong ∧ effectiveInterpretation TheoryVariant.primal Core.Polarity.negative = Role.weak ∧ Multiplicity.pluralSingularParallel.arisesInUE = true ∧ 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 Phenomena.Plurals.Studies.Magri2014.dual_matches_conjunction_parallel : effectiveInterpretation TheoryVariant.dual Core.Polarity.positive = Role.strong ∧ effectiveInterpretation TheoryVariant.dual Core.Polarity.negative = Role.weak ∧ Multiplicity.orAndParallel.arisesInUE = true ∧ 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 Phenomena.Plurals.Studies.Magri2014.Sat : Type

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

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

def Phenomena.Plurals.Studies.Magri2014.instReprSat.repr : Sat → Nat → Std.Format

Equations

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

instance Phenomena.Plurals.Studies.Magri2014.instReprSat : Repr Sat

Equations

• Phenomena.Plurals.Studies.Magri2014.instReprSat = { reprPrec := Phenomena.Plurals.Studies.Magri2014.instReprSat.repr }

instance Phenomena.Plurals.Studies.Magri2014.instDecidableEqSat : DecidableEq Sat

Equations

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

instance Phenomena.Plurals.Studies.Magri2014.instBEqSat : BEq Sat

Equations

• Phenomena.Plurals.Studies.Magri2014.instBEqSat = { beq := Phenomena.Plurals.Studies.Magri2014.instBEqSat.beq }

def Phenomena.Plurals.Studies.Magri2014.instBEqSat.beq : Sat → Sat → Bool

Equations

• Phenomena.Plurals.Studies.Magri2014.instBEqSat.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

theorem Phenomena.Plurals.Studies.Magri2014.fox_inner_exh_the (w : Sat) : Exhaustification.InnocentExclusion.exhB Phenomena.Plurals.Studies.Magri2014.satDomain✝ Phenomena.Plurals.Studies.Magri2014.theAlts✝ Phenomena.Plurals.Studies.Magri2014.bSome✝ w = Phenomena.Plurals.Studies.Magri2014.bSome✝¹ w

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

theorem Phenomena.Plurals.Studies.Magri2014.fox_inner_exh_some (w : Sat) : Exhaustification.InnocentExclusion.exhB Phenomena.Plurals.Studies.Magri2014.satDomain✝ Phenomena.Plurals.Studies.Magri2014.someAlts✝ Phenomena.Plurals.Studies.Magri2014.bSome✝ w = (Phenomena.Plurals.Studies.Magri2014.bSome✝¹ w && !Phenomena.Plurals.Studies.Magri2014.bAll✝ w)

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

theorem Phenomena.Plurals.Studies.Magri2014.fox_double_exh_yields_all (w : Sat) : Exhaustification.InnocentExclusion.exhB Phenomena.Plurals.Studies.Magri2014.satDomain✝ Phenomena.Plurals.Studies.Magri2014.outerAltsForThe✝ Phenomena.Plurals.Studies.Magri2014.innerThe✝ w = Phenomena.Plurals.Studies.Magri2014.bAll✝ w

Bridge theorem: Fox's exhB 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 Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.Magri2014.ConjW : Type

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

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

def Phenomena.Plurals.Studies.Magri2014.instReprConjW.repr : ConjW → Nat → Std.Format

Equations

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

instance Phenomena.Plurals.Studies.Magri2014.instReprConjW : Repr ConjW

Equations

• Phenomena.Plurals.Studies.Magri2014.instReprConjW = { reprPrec := Phenomena.Plurals.Studies.Magri2014.instReprConjW.repr }

instance Phenomena.Plurals.Studies.Magri2014.instDecidableEqConjW : DecidableEq ConjW

Equations

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

def Phenomena.Plurals.Studies.Magri2014.instBEqConjW.beq : ConjW → ConjW → Bool

Equations

• Phenomena.Plurals.Studies.Magri2014.instBEqConjW.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Plurals.Studies.Magri2014.instBEqConjW : BEq ConjW

Equations

• Phenomena.Plurals.Studies.Magri2014.instBEqConjW = { beq := Phenomena.Plurals.Studies.Magri2014.instBEqConjW.beq }

def Phenomena.Plurals.Studies.Magri2014.conjDomain : List ConjW

Equations

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

def Phenomena.Plurals.Studies.Magri2014.cLeft : ConjW → Bool

Equations

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

def Phenomena.Plurals.Studies.Magri2014.cRight : ConjW → Bool

Equations

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

def Phenomena.Plurals.Studies.Magri2014.cOr : ConjW → Bool

Equations

• Phenomena.Plurals.Studies.Magri2014.cOr Phenomena.Plurals.Studies.Magri2014.ConjW.neither = false
• Phenomena.Plurals.Studies.Magri2014.cOr x✝ = true

def Phenomena.Plurals.Studies.Magri2014.cAnd : ConjW → Bool

Equations

• Phenomena.Plurals.Studies.Magri2014.cAnd Phenomena.Plurals.Studies.Magri2014.ConjW.both = true
• Phenomena.Plurals.Studies.Magri2014.cAnd x✝ = false

theorem Phenomena.Plurals.Studies.Magri2014.exh_andUnF (w : ConjW) : Exhaustification.InnocentExclusion.exhB conjDomain Phenomena.Plurals.Studies.Magri2014.andUnFAlts✝ cAnd w = cAnd w

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

theorem Phenomena.Plurals.Studies.Magri2014.exh_andF (w : ConjW) : Exhaustification.InnocentExclusion.exhB conjDomain Phenomena.Plurals.Studies.Magri2014.andFAlts✝ cAnd w = cAnd w

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

theorem Phenomena.Plurals.Studies.Magri2014.exh_left (w : ConjW) : Exhaustification.InnocentExclusion.exhB conjDomain Phenomena.Plurals.Studies.Magri2014.leftAlts✝ cLeft w = (cLeft w && !cRight w)

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

theorem Phenomena.Plurals.Studies.Magri2014.exh_right (w : ConjW) : Exhaustification.InnocentExclusion.exhB conjDomain Phenomena.Plurals.Studies.Magri2014.rightAlts✝ cRight w = (cRight w && !cLeft w)

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

def Phenomena.Plurals.Studies.Magri2014.nAnd : ConjW → Bool

Equations

• Phenomena.Plurals.Studies.Magri2014.nAnd w = !Phenomena.Plurals.Studies.Magri2014.cAnd w

def Phenomena.Plurals.Studies.Magri2014.nOr : ConjW → Bool

Equations

• Phenomena.Plurals.Studies.Magri2014.nOr w = !Phenomena.Plurals.Studies.Magri2014.cOr w

theorem Phenomena.Plurals.Studies.Magri2014.de_exh_notAndUnF (w : ConjW) : Exhaustification.InnocentExclusion.exhB conjDomain Phenomena.Plurals.Studies.Magri2014.nAndUnFAlts✝ nAnd w = nAnd w

(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 Phenomena.Plurals.Studies.Magri2014.de_exh_notAndF (w : ConjW) : Exhaustification.InnocentExclusion.exhB conjDomain Phenomena.Plurals.Studies.Magri2014.nAndFAlts✝ nAnd w = (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 Phenomena.Plurals.Studies.Magri2014.de_exh_notLeft (w : ConjW) : Exhaustification.InnocentExclusion.exhB conjDomain Phenomena.Plurals.Studies.Magri2014.nLeftAlts✝ Phenomena.Plurals.Studies.Magri2014.nLeft✝ w = (Phenomena.Plurals.Studies.Magri2014.nLeft✝¹ w && cOr w && cRight w)

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

theorem Phenomena.Plurals.Studies.Magri2014.de_exh_notRight (w : ConjW) : Exhaustification.InnocentExclusion.exhB conjDomain Phenomena.Plurals.Studies.Magri2014.nRightAlts✝ Phenomena.Plurals.Studies.Magri2014.nRight✝ w = (Phenomena.Plurals.Studies.Magri2014.nRight✝¹ w && cOr w && cLeft w)

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

def Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.Magri2014.innerNAndUnF : ConjW → Bool

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

Equations

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

theorem Phenomena.Plurals.Studies.Magri2014.de_double_exh_conjunction (w : ConjW) : Exhaustification.InnocentExclusion.exhB conjDomain outerNAndUnFAlts innerNAndUnF w = nOr w

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 Phenomena.Plurals.Studies.Magri2014.uniformResult (v : TheoryVariant) (pol : Core.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

• Phenomena.Plurals.Studies.Magri2014.uniformResult Phenomena.Plurals.Studies.Magri2014.TheoryVariant.primal Core.Polarity.positive = Phenomena.Plurals.Studies.Magri2014.allMeaning
• Phenomena.Plurals.Studies.Magri2014.uniformResult Phenomena.Plurals.Studies.Magri2014.TheoryVariant.primal Core.Polarity.negative = Phenomena.Plurals.Studies.Magri2014.someMeaning
• Phenomena.Plurals.Studies.Magri2014.uniformResult Phenomena.Plurals.Studies.Magri2014.TheoryVariant.dual Core.Polarity.positive = Phenomena.Plurals.Studies.Magri2014.allMeaning
• Phenomena.Plurals.Studies.Magri2014.uniformResult Phenomena.Plurals.Studies.Magri2014.TheoryVariant.dual Core.Polarity.negative = Phenomena.Plurals.Studies.Magri2014.someMeaning

theorem Phenomena.Plurals.Studies.Magri2014.uniform_primal_dual_agree (pol : Core.Polarity) : uniformResult TheoryVariant.primal pol = uniformResult TheoryVariant.dual pol

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

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

The primal UE result matches double_strengthening_yields_universal.

theorem Phenomena.Plurals.Studies.Magri2014.uniform_dual_ue (s : Scenario) : uniformResult TheoryVariant.dual Core.Polarity.positive s = dualMeaning Role.mystery s

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

theorem Phenomena.Plurals.Studies.Magri2014.uniform_primal_de (s : Scenario) : uniformResult TheoryVariant.primal Core.Polarity.negative s = primalMeaning Role.mystery s

The primal DE result matches the plain existential meaning.

theorem Phenomena.Plurals.Studies.Magri2014.uniform_gap (v : TheoryVariant) (s : Scenario) (_hn : s.total ≥ 1) (hgap : s.satisfying ≥ 1 ∧ s.satisfying < s.total) : uniformResult v Core.Polarity.positive s = false ∧ notMeaning (uniformResult v Core.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 Phenomena.Plurals.Studies.Magri2014.mysteryInQuestions (v : TheoryVariant) : Role

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

Equations

• Phenomena.Plurals.Studies.Magri2014.mysteryInQuestions Phenomena.Plurals.Studies.Magri2014.TheoryVariant.primal = Phenomena.Plurals.Studies.Magri2014.Role.weak
• Phenomena.Plurals.Studies.Magri2014.mysteryInQuestions Phenomena.Plurals.Studies.Magri2014.TheoryVariant.dual = Phenomena.Plurals.Studies.Magri2014.Role.strong

theorem Phenomena.Plurals.Studies.Magri2014.questions_differentiate : mysteryInQuestions TheoryVariant.primal ≠ mysteryInQuestions TheoryVariant.dual

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

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

Definites (primal) should have existential force in questions.

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

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

structure Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.Magri2014.instReprQuestionForceDatum.repr : QuestionForceDatum → Nat → Std.Format

Equations

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

instance Phenomena.Plurals.Studies.Magri2014.instReprQuestionForceDatum : Repr QuestionForceDatum

Equations

• Phenomena.Plurals.Studies.Magri2014.instReprQuestionForceDatum = { reprPrec := Phenomena.Plurals.Studies.Magri2014.instReprQuestionForceDatum.repr }

def Phenomena.Plurals.Studies.Magri2014.definitesQuestion : QuestionForceDatum

Equations

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

def Phenomena.Plurals.Studies.Magri2014.conjunctionQuestion : QuestionForceDatum

Equations

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

theorem Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.Magri2014.conj_gap_positive_false : (Phenomena.Plurals.Studies.Magri2014.conjGapWorlds✝.all fun (w : ConjW) => decide (cAnd w = false)) = true

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

theorem Phenomena.Plurals.Studies.Magri2014.conj_gap_dual_negative_false : (Phenomena.Plurals.Studies.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 Phenomena.Plurals.Studies.Magri2014.conj_gap_matches_empirical_data : Homogeneity.conjunctionExample.positiveInGap = Homogeneity.HomogeneityJudgment.neitherTrueNorFalse ∧ Homogeneity.conjunctionExample.negativeInGap = Homogeneity.HomogeneityJudgment.neitherTrueNorFalse

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

theorem Phenomena.Plurals.Studies.Magri2014.enriched_conjunction_end_to_end : (∀ (w : ConjW), Exhaustification.InnocentExclusion.exhB conjDomain outerNAndUnFAlts innerNAndUnF w = nOr w) ∧ cAnd ConjW.onlyA = false ∧ nOr ConjW.onlyA = false ∧ Homogeneity.conjunctionExample.positiveInGap = Homogeneity.HomogeneityJudgment.neitherTrueNorFalse ∧ Homogeneity.conjunctionExample.negativeInGap = Homogeneity.HomogeneityJudgment.neitherTrueNorFalse

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