Weak Necessity Modals as Homogeneous Pluralities of Worlds

@cite{agha-jeretic-2022}

Proceedings of SALT 32: 831–851.

Core Proposal

Weak necessity modals like should are not quantificational. They denote definite pluralities of worlds, paralleling the relationship between plural definite nominals (the) and universal quantifiers (all/every):

• must p = all worlds in a given domain are p-worlds (∀ quantifier)
• should p = the worlds in a given domain are p-worlds (plural definite)

This gives weak necessity modals homogeneity as an intrinsic feature: they yield a truth-value gap (neither true nor false) when some but not all worlds in the domain satisfy the prejacent — exactly paralleling the behavior of plural definite DPs under negation.

Key Claims Formalized

1. Homogeneity (§3.1): Weak necessity modals take obligatory apparent wide scope over negation, unlike strong necessity modals which allow narrow scope.

2. Trivalent semantics (§4.2): should_D := ⊕D — evaluation is trivalent with symmetric negation (homogeneity gap preserved under ¬).

3. Homogeneity removal (§3.2): The adverb necessarily removes homogeneity from should, just as all removes it for plural definites.

4. QUD-sensitive exception tolerance (§3.3): Weak necessity modals tolerate exceptions when irrelevant to the QUD.

5. X operator (§5.1): Derives should from must compositionally via minimal witness sets. X only applies to universals (unique witness), explaining Javanese NE's restriction to necessity modals.

6. Critique of domain restriction (§6.1): The vFI 2008 analysis (Directive.weakNecessity) is bivalent — it cannot produce the truth-value gap that the empirical data require.

Independent Support

@cite{tieu-kriz-chemla-2019} find that children acquire homogeneity independently of scalar implicatures (HOM/−SI group), supporting the claim that homogeneity is intrinsic to plural predication rather than derived via exhaustification (@cite{magri-2014}).

Connection to @cite{agha-jeretic-2026}

The 2026 handbook chapter surveys this analysis as one of three competing accounts of weak necessity (alongside domain restriction and comparative semantics), and extends it to explain the neg-raising asymmetry between should and must.

Trivalent evaluation

should gets trivalent semantics via plural predication over worlds, while must remains bivalent (standard ∀ quantification).

We model the modal domain as a List World and use Core.Duality.Truth3 for the three-valued output.

def Phenomena.Modality.Studies.AghaJeretic2022.mustEval {World : Type} (domain : List World) (p : World → Bool) : Core.Duality.Truth3

Strong necessity: standard ∀ quantification over the modal domain. Bivalent — always true or false, never indeterminate. must_D := λp. ∀w ∈ D. p(w)

Equations

• Phenomena.Modality.Studies.AghaJeretic2022.mustEval domain p = Core.Duality.Truth3.ofBool (domain.all p)

def Phenomena.Modality.Studies.AghaJeretic2022.shouldEval {World : Type} (domain : List World) (p : World → Bool) : Core.Duality.Truth3

Weak necessity: trivalent plural predication over the modal domain. Returns tt if all worlds satisfy p, ff if none do, unk otherwise. should_D := ⊕D — the prejacent is predicated of the plurality of worlds, yielding homogeneity.

Equations

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

must is always bivalent

theorem Phenomena.Modality.Studies.AghaJeretic2022.must_bivalent {World : Type} (domain : List World) (p : World → Bool) : mustEval domain p = Core.Duality.Truth3.true ∨ mustEval domain p = Core.Duality.Truth3.false

must never returns the indeterminate value.

should is homogeneous: it can return ★

theorem Phenomena.Modality.Studies.AghaJeretic2022.should_mixed : shouldEval [true, false] id = Core.Duality.Truth3.indet

In a mixed domain, should returns ★ (indeterminate).

theorem Phenomena.Modality.Studies.AghaJeretic2022.should_all_true : shouldEval [true, true, true] id = Core.Duality.Truth3.true

In a uniform-true domain, should returns tt.

theorem Phenomena.Modality.Studies.AghaJeretic2022.should_all_false : shouldEval [false, false] id = Core.Duality.Truth3.false

In a uniform-false domain, should returns ff.

theorem Phenomena.Modality.Studies.AghaJeretic2022.must_mixed : mustEval [true, false] id = Core.Duality.Truth3.false

must returns ff in the mixed case (no gap).

theorem Phenomena.Modality.Studies.AghaJeretic2022.should_must_agree_positive {World : Type} (domain : List World) (p : World → Bool) (h : domain.all p = true) (hne : domain.isEmpty = false) : shouldEval domain p = mustEval domain p

When positive, should and must agree.

Negation symmetry

The paper's central formal claim: shouldEval produces symmetric truth conditions under negation. Affirming p of the plurality and denying ¬p are non-complementary — both can be indeterminate simultaneously. This is the formal content of homogeneity.

• shouldEval D p = tt → shouldEval D (¬p) = ff (no positive/negative overlap)
• shouldEval D p = ff → shouldEval D (¬p) = tt (symmetric falsity, non-empty D)
• shouldEval D p = unk → shouldEval D (¬p) = unk (the gap is symmetric)

Contrast: must has NO gap — it's always bivalent.

theorem Phenomena.Modality.Studies.AghaJeretic2022.shouldEval_tt_neg_ff {World : Type} (domain : List World) (p : World → Bool) (h : shouldEval domain p = Core.Duality.Truth3.true) : (shouldEval domain fun (w : World) => !p w) = Core.Duality.Truth3.false

If shouldEval D p = tt, then shouldEval D (¬p) = ff. No overlap between positive and negative extensions of the plurality.

theorem Phenomena.Modality.Studies.AghaJeretic2022.shouldEval_ff_neg_tt {World : Type} (domain : List World) (p : World → Bool) (h : shouldEval domain p = Core.Duality.Truth3.false) (hne : domain.isEmpty = false) : (shouldEval domain fun (w : World) => !p w) = Core.Duality.Truth3.true

If shouldEval D p = ff (non-empty D), then shouldEval D (¬p) = tt. Symmetric: universal denial of p means universal affirmation of ¬p.

theorem Phenomena.Modality.Studies.AghaJeretic2022.shouldEval_unk_symmetric {World : Type} (domain : List World) (p : World → Bool) (h : shouldEval domain p = Core.Duality.Truth3.indet) : (shouldEval domain fun (w : World) => !p w) = Core.Duality.Truth3.indet

If shouldEval D p = unk, then shouldEval D (¬p) = unk. The gap is symmetric under negation — the core homogeneity property.

Modal homogeneity parallels plural definite homogeneity

The paper demonstrates that weak necessity modals pattern exactly like plural definites with respect to negation. We encode the key data points using the HomogeneityDatum type from Plurals.Homogeneity.

def Phenomena.Modality.Studies.AghaJeretic2022.shouldHomogeneity : Plurals.Homogeneity.HomogeneityDatum

Should displays homogeneity: under negation, "shouldn't go" is incompatible with an existential followup "but you can" — just like "The guests aren't here" is incompatible with "but some of them are."

Paper examples (8)–(9).

Equations

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

def Phenomena.Modality.Studies.AghaJeretic2022.haveToNoHomogeneity : Plurals.Homogeneity.HomogeneityDatum

Have to does NOT display homogeneity: "don't have to go" is compatible with "but you are allowed to go" — narrow scope reading (¬□ = ◇¬) available, unlike should which only allows wide scope (□¬).

Paper example (9b).

Equations

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

theorem Phenomena.Modality.Studies.AghaJeretic2022.should_has_gap : shouldHomogeneity.positiveInGap = Plurals.Homogeneity.HomogeneityJudgment.neitherTrueNorFalse

theorem Phenomena.Modality.Studies.AghaJeretic2022.haveTo_no_gap : haveToNoHomogeneity.negativeInGap = Plurals.Homogeneity.HomogeneityJudgment.clearlyTrue

Homogeneity removal by "necessarily"

Inserting necessarily into a weak necessity modal sentence removes the homogeneity gap, just as all removes it from plural definites.

Paper examples (14)–(15):

• "You shouldn't go" → #but you can go
• "You shouldn't necessarily go" → ✓but you can go

This parallels:

• "The guests aren't here" → #but some are
• "The guests aren't all here" → ✓but some are

def Phenomena.Modality.Studies.AghaJeretic2022.necessarilyRemovesModalHomogeneity : Plurals.Homogeneity.HomogeneityRemovalDatum

Necessarily removes homogeneity from should, paralleling how all removes homogeneity from plural definites.

Equations

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

def Phenomena.Modality.Studies.AghaJeretic2022.shouldWithRemoval {World : Type} (domain : List World) (p : World → Bool) : Core.Duality.Truth3

shouldEval with homogeneity removal (= explicit quantifier insertion) reduces to mustEval — the gap disappears.

Equations

• Phenomena.Modality.Studies.AghaJeretic2022.shouldWithRemoval domain p = Phenomena.Modality.Studies.AghaJeretic2022.mustEval domain p

theorem Phenomena.Modality.Studies.AghaJeretic2022.removal_eliminates_gap : shouldWithRemoval [true, false] id = Core.Duality.Truth3.false

QUD-sensitive exception tolerance

Plural predication tolerates exceptions when they are irrelevant to the QUD. The paper shows the same pattern for weak necessity modals.

Paper example (17): Context: One can get a perfect grade by doing most exercises correctly; doing all gives extra credit. QUD1: What is a way to get a perfect grade? QUD2: What are the minimal requirements?

(a) "You should do every exercise." → QUD1: ✓; QUD2: # (b) "You have to do every exercise." → QUD1: #; QUD2: #

structure Phenomena.Modality.Studies.AghaJeretic2022.ModalExceptionDatum : Type

• modal : String
• sentence : String
• context : String
• qud1 : String
• qud2 : String
• acceptableUnderQUD1 : Bool
• acceptableUnderQUD2 : Bool

def Phenomena.Modality.Studies.AghaJeretic2022.instReprModalExceptionDatum.repr : ModalExceptionDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Modality.Studies.AghaJeretic2022.instReprModalExceptionDatum : Repr ModalExceptionDatum

Equations

• Phenomena.Modality.Studies.AghaJeretic2022.instReprModalExceptionDatum = { reprPrec := Phenomena.Modality.Studies.AghaJeretic2022.instReprModalExceptionDatum.repr }

def Phenomena.Modality.Studies.AghaJeretic2022.shouldExceptionTolerance : ModalExceptionDatum

Equations

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

def Phenomena.Modality.Studies.AghaJeretic2022.haveToExceptionTolerance : ModalExceptionDatum

Equations

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

theorem Phenomena.Modality.Studies.AghaJeretic2022.should_tolerates_exceptions : shouldExceptionTolerance.acceptableUnderQUD1 = true ∧ haveToExceptionTolerance.acceptableUnderQUD1 = false

Well-responses in borderline cases

In borderline cases (★), outright denial is infelicitous; well-responses are preferred. This parallels plural definites (@cite{kriz-2016}).

Paper example (19).

structure Phenomena.Modality.Studies.AghaJeretic2022.IndeterminateResponseDatum : Type

• sentence : String
• context : String
• noResponseFelicitous : Bool
• wellResponseFelicitous : Bool

instance Phenomena.Modality.Studies.AghaJeretic2022.instReprIndeterminateResponseDatum : Repr IndeterminateResponseDatum

Equations

• Phenomena.Modality.Studies.AghaJeretic2022.instReprIndeterminateResponseDatum = { reprPrec := Phenomena.Modality.Studies.AghaJeretic2022.instReprIndeterminateResponseDatum.repr }

def Phenomena.Modality.Studies.AghaJeretic2022.instReprIndeterminateResponseDatum.repr : IndeterminateResponseDatum → ℕ → Std.Format

Equations

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

def Phenomena.Modality.Studies.AghaJeretic2022.shouldIndeterminateResponse : IndeterminateResponseDatum

Equations

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

def Phenomena.Modality.Studies.AghaJeretic2022.mustIndeterminateResponse : IndeterminateResponseDatum

Equations

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

theorem Phenomena.Modality.Studies.AghaJeretic2022.should_well_not_no : shouldIndeterminateResponse.noResponseFelicitous = false ∧ shouldIndeterminateResponse.wellResponseFelicitous = true

theorem Phenomena.Modality.Studies.AghaJeretic2022.must_no_not_well : mustIndeterminateResponse.noResponseFelicitous = true ∧ mustIndeterminateResponse.wellResponseFelicitous = false

Compositional derivation via the X operator

X picks out the unique smallest set that makes a quantifier true and returns the mereological sum of its elements:

X := λM. ⊕ ιW[W ∈ WIT(M)]

Applied to must_D: the unique minimal witness set of ∀ over D is D itself (no proper subset suffices). So X(must_D) = ⊕D = should_D.

Applied to can_D: each singleton {w} for w ∈ D is a minimal witness of ∃. Multiple minimal witnesses → ι is undefined → X is undefined. This explains why Javanese NE (= X) only combines with necessity modals.

def Phenomena.Modality.Studies.AghaJeretic2022.isWitness {World : Type} (q : List World → Bool) (w : List World) : Bool

A witness set for a quantifier Q is a set W such that Q(W) holds.

Equations

• Phenomena.Modality.Studies.AghaJeretic2022.isWitness q w = q w

def Phenomena.Modality.Studies.AghaJeretic2022.isMinimalWitness {World : Type} [BEq World] (q : List World → Bool) (w : List World) : Bool

A minimal witness: a witness with no proper sub-witness. Removing any element makes it no longer a witness.

Equations

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

def Phenomena.Modality.Studies.AghaJeretic2022.universalQ {World : Type} [BEq World] (domain : List World) : List World → Bool

Universal quantifier as GQ: W witnesses ∀ over D iff D ⊆ W. This is the Barwise & Cooper (1981) witness set notion — the quantifier EVERY(D) = {P | D ⊆ P}, so W ∈ EVERY(D) iff D ⊆ W.

Equations

• Phenomena.Modality.Studies.AghaJeretic2022.universalQ domain w = domain.all fun (x : World) => w.contains x

def Phenomena.Modality.Studies.AghaJeretic2022.existentialQ {World : Type} [BEq World] (domain : List World) : List World → Bool

Existential quantifier as GQ: W witnesses ∃ over D iff D ∩ W ≠ ∅. SOME(D) = {P | D ∩ P ≠ ∅}, so W ∈ SOME(D) iff some element of D is in W.

Equations

• Phenomena.Modality.Studies.AghaJeretic2022.existentialQ domain w = domain.any fun (x : World) => w.contains x

theorem Phenomena.Modality.Studies.AghaJeretic2022.universal_unique_minimal_witness : isMinimalWitness (universalQ [0, 1]) [0, 1] = true ∧ isMinimalWitness (universalQ [0, 1]) [0] = false ∧ isMinimalWitness (universalQ [0, 1]) [1] = false

The full domain is the UNIQUE minimal witness for ∀. Since EVERY(D) = {P | D ⊆ P}, the only W ⊆ D with D ⊆ W is W = D. Removing any element breaks the subset condition. This is why X (requiring a unique minimal witness) applies to universals.

theorem Phenomena.Modality.Studies.AghaJeretic2022.existential_multiple_minimal_witnesses : isMinimalWitness (existentialQ [0, 1]) [0] = true ∧ isMinimalWitness (existentialQ [0, 1]) [1] = true ∧ isMinimalWitness (existentialQ [0, 1]) [0, 1] = false

Each singleton is a minimal witness for ∃, and the full domain is NOT minimal (proper subsets suffice). This is why X is undefined for ∃ — multiple minimal witnesses means ι (the uniqueness presupposition) fails. This explains Javanese NE's restriction to necessity modals.

def Phenomena.Modality.Studies.AghaJeretic2022.applyX {World : Type} (domain : List World) (p : World → Bool) : Core.Duality.Truth3

X applied to must yields the domain itself (= should's denotation). The resulting plurality is then subject to plural predication semantics.

Equations

• Phenomena.Modality.Studies.AghaJeretic2022.applyX domain p = Phenomena.Modality.Studies.AghaJeretic2022.shouldEval domain p

theorem Phenomena.Modality.Studies.AghaJeretic2022.x_must_eq_should {World : Type} (domain : List World) (p : World → Bool) : applyX domain p = shouldEval domain p

X(must) = should.

Morphological composition of weak necessity

Cross-linguistically, weak necessity is expressed in two ways:

1. Primitive lexical items (English should, ought): non-decomposable.
2. Morphological derivation from strong necessity: a. French: devoir+CF → weak necessity. CF picks a witness set without requiring uniqueness, so it applies to both ∀ (devrais) and ∃ (pourrais). b. Javanese: mesthi+NE → weak necessity. NE = X (requires unique minimal witness), so it only applies to ∀ (mesthi-ne), not ∃ (iso-ne is ungrammatical).

inductive Phenomena.Modality.Studies.AghaJeretic2022.WeakNecessityMorphology : Type

• primitive : WeakNecessityMorphology
• counterfactual : WeakNecessityMorphology
• dedicatedMarker : WeakNecessityMorphology

instance Phenomena.Modality.Studies.AghaJeretic2022.instDecidableEqWeakNecessityMorphology : DecidableEq WeakNecessityMorphology

Equations

• Phenomena.Modality.Studies.AghaJeretic2022.instDecidableEqWeakNecessityMorphology x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Modality.Studies.AghaJeretic2022.instReprWeakNecessityMorphology.repr : WeakNecessityMorphology → ℕ → Std.Format

Equations

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

instance Phenomena.Modality.Studies.AghaJeretic2022.instReprWeakNecessityMorphology : Repr WeakNecessityMorphology

Equations

• Phenomena.Modality.Studies.AghaJeretic2022.instReprWeakNecessityMorphology = { reprPrec := Phenomena.Modality.Studies.AghaJeretic2022.instReprWeakNecessityMorphology.repr }

structure Phenomena.Modality.Studies.AghaJeretic2022.WeakNecessityMorphDatum : Type

• language : String
• strongForm : String
• weakForm : String
• strategy : WeakNecessityMorphology
• appliesTo : String

def Phenomena.Modality.Studies.AghaJeretic2022.instReprWeakNecessityMorphDatum.repr : WeakNecessityMorphDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Modality.Studies.AghaJeretic2022.instReprWeakNecessityMorphDatum : Repr WeakNecessityMorphDatum

Equations

• Phenomena.Modality.Studies.AghaJeretic2022.instReprWeakNecessityMorphDatum = { reprPrec := Phenomena.Modality.Studies.AghaJeretic2022.instReprWeakNecessityMorphDatum.repr }

def Phenomena.Modality.Studies.AghaJeretic2022.english_should : WeakNecessityMorphDatum

Equations

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

def Phenomena.Modality.Studies.AghaJeretic2022.french_devrais : WeakNecessityMorphDatum

Equations

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

def Phenomena.Modality.Studies.AghaJeretic2022.javanese_mesthi : WeakNecessityMorphDatum

Equations

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

def Phenomena.Modality.Studies.AghaJeretic2022.spanish_deber : WeakNecessityMorphDatum

Equations

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

def Phenomena.Modality.Studies.AghaJeretic2022.hungarian_kell : WeakNecessityMorphDatum

Equations

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

def Phenomena.Modality.Studies.AghaJeretic2022.weakNecessityMorphData : List WeakNecessityMorphDatum

Equations

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

theorem Phenomena.Modality.Studies.AghaJeretic2022.three_strategies : (List.map (fun (x : WeakNecessityMorphDatum) => x.strategy) weakNecessityMorphData).eraseDups.length = 3

theorem Phenomena.Modality.Studies.AghaJeretic2022.javanese_necessity_only : javanese_mesthi.appliesTo = "necessity only (*iso-ne is ungrammatical)"

Javanese NE only applies to necessity; French CF applies to both. This follows from X requiring unique minimal witnesses (∀ only) vs CF accepting any witness (∀ and ∃).

theorem Phenomena.Modality.Studies.AghaJeretic2022.french_both_forces : french_devrais.appliesTo = "necessity + possibility (devrais/pourrais)"

Why domain restriction doesn't capture homogeneity

The @cite{von-fintel-iatridou-2008} analysis (formalized in Directive.lean) treats should as ∀ over a refined set of best worlds. Directive.weakNecessity returns Bool — it is bivalent by construction. A bivalent semantics cannot produce the truth-value gap that the empirical data require.

We make this critique computational by contrasting Directive.weakNecessity (always tt or ff) with shouldEval (can return unk).

theorem Phenomena.Modality.Studies.AghaJeretic2022.directive_bivalent (f : Semantics.Modality.Kratzer.ModalBase) (g g' : Semantics.Modality.Kratzer.OrderingSource) (p : BProp Semantics.Attitudes.Intensional.World) (w : Semantics.Attitudes.Intensional.World) : Core.Duality.Truth3.ofBool (Semantics.Modality.Directive.weakNecessity f g g' p w) = Core.Duality.Truth3.true ∨ Core.Duality.Truth3.ofBool (Semantics.Modality.Directive.weakNecessity f g g' p w) = Core.Duality.Truth3.false

Directive.weakNecessity is bivalent: it returns Bool, so wrapping in Truth3 can only yield true or false — never indet.

theorem Phenomena.Modality.Studies.AghaJeretic2022.shouldEval_can_gap : ∃ (D : List Bool) (p : Bool → Bool), shouldEval D p = Core.Duality.Truth3.indet

shouldEval CAN return unk — the gap that domain restriction misses.

structure Phenomena.Modality.Studies.AghaJeretic2022.DomainRestrictionPrediction : Type

The mismatch: domain restriction predicts existential followups are felicitous after negated should, but empirically they are not.

• sentence : String
• existentialFollowup : String
• domainRestrictionPredicts : Bool
• empiricallyObserved : Bool

instance Phenomena.Modality.Studies.AghaJeretic2022.instReprDomainRestrictionPrediction : Repr DomainRestrictionPrediction

Equations

• Phenomena.Modality.Studies.AghaJeretic2022.instReprDomainRestrictionPrediction = { reprPrec := Phenomena.Modality.Studies.AghaJeretic2022.instReprDomainRestrictionPrediction.repr }

def Phenomena.Modality.Studies.AghaJeretic2022.instReprDomainRestrictionPrediction.repr : DomainRestrictionPrediction → ℕ → Std.Format

Equations

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

def Phenomena.Modality.Studies.AghaJeretic2022.domainRestrictionFails : DomainRestrictionPrediction

Equations

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

theorem Phenomena.Modality.Studies.AghaJeretic2022.domain_restriction_wrong : domainRestrictionFails.domainRestrictionPredicts ≠ domainRestrictionFails.empiricallyObserved

English modal lexicon verification

Verify that the English fragment classifies should/ought as weak necessity and must as strong necessity, matching the paper's §2.1.

theorem Phenomena.Modality.Studies.AghaJeretic2022.should_is_weak : (Fragments.English.FunctionWords.should.modalMeaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.weakNecessity) = true

should is classified as weak necessity in the English fragment.

theorem Phenomena.Modality.Studies.AghaJeretic2022.ought_is_weak : (Fragments.English.FunctionWords.ought.modalMeaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.weakNecessity) = true

ought is classified as weak necessity.

theorem Phenomena.Modality.Studies.AghaJeretic2022.must_is_strong_not_weak : (Fragments.English.FunctionWords.must.modalMeaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.necessity) = true ∧ (Fragments.English.FunctionWords.must.modalMeaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.weakNecessity) = false

must is classified as strong necessity, not weak.

Scopelessness persists under higher negation

The apparent wide scope of should persists when negation is in a higher clause, paralleling plural definites:

• "I don't think the guests are here" → #but some are
• "I don't think you should go" → #but you are allowed to go
• "I don't think you have to go" → ✓but you are allowed to go

This is analyzed as scopelessness: the "wide scope" effect is a consequence of homogeneity, not syntactic movement.

structure Phenomena.Modality.Studies.AghaJeretic2022.ScopelessnessDatum : Type

• modal : String
• sentence : String
• existentialFollowup : String
• followupFelicitous : Bool

instance Phenomena.Modality.Studies.AghaJeretic2022.instReprScopelessnessDatum : Repr ScopelessnessDatum

Equations

• Phenomena.Modality.Studies.AghaJeretic2022.instReprScopelessnessDatum = { reprPrec := Phenomena.Modality.Studies.AghaJeretic2022.instReprScopelessnessDatum.repr }

def Phenomena.Modality.Studies.AghaJeretic2022.instReprScopelessnessDatum.repr : ScopelessnessDatum → ℕ → Std.Format

Equations

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

def Phenomena.Modality.Studies.AghaJeretic2022.shouldScopeless : ScopelessnessDatum

Equations

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

def Phenomena.Modality.Studies.AghaJeretic2022.haveToNotScopeless : ScopelessnessDatum

Equations

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

theorem Phenomena.Modality.Studies.AghaJeretic2022.scopelessness_contrast : shouldScopeless.followupFelicitous = false ∧ haveToNotScopeless.followupFelicitous = true

Weak necessity and its friends

The paper argues (§6.4) that the homogeneity pattern observed with weak necessity modals is part of a general phenomenon shared with bare conditionals, generics, and habituals — all analyzable as involving plural predication over different semantic domains.

Plurals.Homogeneity.conditionalExample already captures the conditional case: "They play soccer if the sun shines" displays the same gap as "The switches are on" and "You should go."

Examples (38)–(42): future conditionals, bare past conditionals, generics, and habituals all show homogeneity effects and homogeneity removal by explicit quantifiers (necessarily, always, all).

theorem Phenomena.Modality.Studies.AghaJeretic2022.conditional_parallel : Plurals.Homogeneity.conditionalExample.positiveInGap = shouldHomogeneity.positiveInGap ∧ Plurals.Homogeneity.conditionalExample.negativeInGap = shouldHomogeneity.negativeInGap

The existing conditionalExample from Homogeneity.lean shows the same gap pattern as shouldHomogeneity — both have ★ in the gap scenario. This structural parallel supports the unified plural predication analysis.

The Determiner–Modal Parallel

Nominal domain	Modal domain
the N (plural def.)	should (weak necessity)
all/every N (∀)	must/have to (strong)
homogeneous	homogeneous
scopeless	scopeless
exception-tolerant	exception-tolerant
all removes gap	necessarily removes gap
★ → "well" response	★ → "well" response

The proposal: weak necessity is to strong necessity what the is to all.

structure Phenomena.Modality.Studies.AghaJeretic2022.PluralModalParallel : Type

• property : String
• pluralDefiniteExample : String
• weakNecessityExample : String
• sharedBehavior : Bool

def Phenomena.Modality.Studies.AghaJeretic2022.instReprPluralModalParallel.repr : PluralModalParallel → ℕ → Std.Format

Equations

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

instance Phenomena.Modality.Studies.AghaJeretic2022.instReprPluralModalParallel : Repr PluralModalParallel

Equations

• Phenomena.Modality.Studies.AghaJeretic2022.instReprPluralModalParallel = { reprPrec := Phenomena.Modality.Studies.AghaJeretic2022.instReprPluralModalParallel.repr }

def Phenomena.Modality.Studies.AghaJeretic2022.sharedProperties : List PluralModalParallel

Equations

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

theorem Phenomena.Modality.Studies.AghaJeretic2022.all_properties_shared : (sharedProperties.all fun (x : PluralModalParallel) => x.sharedBehavior) = true

theorem Phenomena.Modality.Studies.AghaJeretic2022.five_parallels : sharedProperties.length = 5