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 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

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

def 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.

Body uses an explicit 4-way if-chain to support split-based proofs in this file. The bridge theorem shouldEval_eq_distList (below) formalizes the equivalence with Core.Duality.distList for nonempty domains. Refactoring the body to call distList directly requires rewriting ~3 dense proof scripts; tracked as future work.

Equations

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

must is always bivalent

theorem 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 AghaJeretic2022.should_mixed : shouldEval [true, false] id = Core.Duality.Truth3.indet

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

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

In a uniform-true domain, should returns tt.

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

In a uniform-false domain, should returns ff.

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

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

theorem 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 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 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 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 AghaJeretic2022.shouldHomogeneity : Phenomena.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 AghaJeretic2022.haveToNoHomogeneity : Phenomena.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 AghaJeretic2022.should_has_gap : shouldHomogeneity.positiveInGap = Phenomena.Plurals.Homogeneity.HomogeneityJudgment.neitherTrueNorFalse

theorem AghaJeretic2022.haveTo_no_gap : haveToNoHomogeneity.negativeInGap = Phenomena.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 AghaJeretic2022.necessarilyRemovesModalHomogeneity : Phenomena.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 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

• AghaJeretic2022.shouldWithRemoval domain p = AghaJeretic2022.mustEval domain p

theorem 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 AghaJeretic2022.ModalExceptionDatum : Type

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

def AghaJeretic2022.instReprModalExceptionDatum.repr : ModalExceptionDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AghaJeretic2022.instReprModalExceptionDatum : Repr ModalExceptionDatum

Equations

• AghaJeretic2022.instReprModalExceptionDatum = { reprPrec := AghaJeretic2022.instReprModalExceptionDatum.repr }

def AghaJeretic2022.shouldExceptionTolerance : ModalExceptionDatum

Equations

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

def AghaJeretic2022.haveToExceptionTolerance : ModalExceptionDatum

Equations

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

theorem 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 AghaJeretic2022.IndeterminateResponseDatum : Type

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

@[implicit_reducible]

instance AghaJeretic2022.instReprIndeterminateResponseDatum : Repr IndeterminateResponseDatum

Equations

• AghaJeretic2022.instReprIndeterminateResponseDatum = { reprPrec := AghaJeretic2022.instReprIndeterminateResponseDatum.repr }

def AghaJeretic2022.instReprIndeterminateResponseDatum.repr : IndeterminateResponseDatum → ℕ → Std.Format

Equations

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

def AghaJeretic2022.shouldIndeterminateResponse : IndeterminateResponseDatum

Equations

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

def AghaJeretic2022.mustIndeterminateResponse : IndeterminateResponseDatum

Equations

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

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

theorem 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 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

• AghaJeretic2022.isWitness q w = q w

def 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

• AghaJeretic2022.isMinimalWitness q w = (AghaJeretic2022.isWitness q w && w.all fun (x : World) => !AghaJeretic2022.isWitness q (List.filter (fun (x_1 : World) => x_1 != x) w))

def 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

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

def 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

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

theorem 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 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 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

• AghaJeretic2022.applyX domain p = AghaJeretic2022.shouldEval domain p

theorem 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 AghaJeretic2022.WeakNecessityMorphology : Type

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

@[implicit_reducible]

instance AghaJeretic2022.instDecidableEqWeakNecessityMorphology : DecidableEq WeakNecessityMorphology

Equations

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

def AghaJeretic2022.instReprWeakNecessityMorphology.repr : WeakNecessityMorphology → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AghaJeretic2022.instReprWeakNecessityMorphology : Repr WeakNecessityMorphology

Equations

• AghaJeretic2022.instReprWeakNecessityMorphology = { reprPrec := AghaJeretic2022.instReprWeakNecessityMorphology.repr }

structure AghaJeretic2022.WeakNecessityMorphDatum : Type

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

@[implicit_reducible]

instance AghaJeretic2022.instReprWeakNecessityMorphDatum : Repr WeakNecessityMorphDatum

Equations

• AghaJeretic2022.instReprWeakNecessityMorphDatum = { reprPrec := AghaJeretic2022.instReprWeakNecessityMorphDatum.repr }

def AghaJeretic2022.instReprWeakNecessityMorphDatum.repr : WeakNecessityMorphDatum → ℕ → Std.Format

Equations

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

def AghaJeretic2022.english_should : WeakNecessityMorphDatum

Equations

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

def AghaJeretic2022.french_devrais : WeakNecessityMorphDatum

Equations

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

def AghaJeretic2022.javanese_mesthi : WeakNecessityMorphDatum

Equations

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

def AghaJeretic2022.spanish_deber : WeakNecessityMorphDatum

Equations

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

def AghaJeretic2022.hungarian_kell : WeakNecessityMorphDatum

Equations

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

def AghaJeretic2022.weakNecessityMorphData : List WeakNecessityMorphDatum

Equations

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

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

theorem 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 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).

@[reducible, inline]

abbrev AghaJeretic2022.BridgeWorld : Type

Local 4-world type for the bivalence demonstration.

Equations

• AghaJeretic2022.BridgeWorld = Fin 4

theorem AghaJeretic2022.directive_bivalent (f : Core.Logic.Intensional.ModalBase BridgeWorld) (g g' : Core.Logic.Intensional.OrderingSource BridgeWorld) (p : BridgeWorld → Prop) (w : BridgeWorld) : Semantics.Modality.Directive.weakNecessity f g g' p w ∨ ¬Semantics.Modality.Directive.weakNecessity f g g' p w

Directive.weakNecessity is bivalent: as a Prop, it is classically true or false — never indeterminate. This contrasts with shouldEval, which can return Truth3.indet.

theorem 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 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

@[implicit_reducible]

instance AghaJeretic2022.instReprDomainRestrictionPrediction : Repr DomainRestrictionPrediction

Equations

• AghaJeretic2022.instReprDomainRestrictionPrediction = { reprPrec := AghaJeretic2022.instReprDomainRestrictionPrediction.repr }

def AghaJeretic2022.instReprDomainRestrictionPrediction.repr : DomainRestrictionPrediction → ℕ → Std.Format

Equations

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

def AghaJeretic2022.domainRestrictionFails : DomainRestrictionPrediction

Equations

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

theorem 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 AghaJeretic2022.should_is_weak : (Fragments.English.Auxiliaries.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 AghaJeretic2022.ought_is_weak : (Fragments.English.Auxiliaries.ought.modalMeaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.weakNecessity) = true

ought is classified as weak necessity.

theorem AghaJeretic2022.must_is_strong_not_weak : (Fragments.English.Auxiliaries.must.modalMeaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.necessity) = true ∧ (Fragments.English.Auxiliaries.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 AghaJeretic2022.ScopelessnessDatum : Type

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

@[implicit_reducible]

instance AghaJeretic2022.instReprScopelessnessDatum : Repr ScopelessnessDatum

Equations

• AghaJeretic2022.instReprScopelessnessDatum = { reprPrec := AghaJeretic2022.instReprScopelessnessDatum.repr }

def AghaJeretic2022.instReprScopelessnessDatum.repr : ScopelessnessDatum → ℕ → Std.Format

Equations

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

def AghaJeretic2022.shouldScopeless : ScopelessnessDatum

Equations

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

def AghaJeretic2022.haveToNotScopeless : ScopelessnessDatum

Equations

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

theorem 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 AghaJeretic2022.conditional_parallel : Phenomena.Plurals.Homogeneity.conditionalExample.positiveInGap = shouldHomogeneity.positiveInGap ∧ Phenomena.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 AghaJeretic2022.PluralModalParallel : Type

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

@[implicit_reducible]

instance AghaJeretic2022.instReprPluralModalParallel : Repr PluralModalParallel

Equations

• AghaJeretic2022.instReprPluralModalParallel = { reprPrec := AghaJeretic2022.instReprPluralModalParallel.repr }

def AghaJeretic2022.instReprPluralModalParallel.repr : PluralModalParallel → ℕ → Std.Format

Equations

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

def AghaJeretic2022.sharedProperties : List PluralModalParallel

Equations

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

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

theorem AghaJeretic2022.five_parallels : sharedProperties.length = 5

Local vs Global Aggregation

The should/must contrast is an instance of the local/global aggregation distinction in Core.Duality. When modal sentences are embedded under quantifiers ("Every student should/must pass"):

• should (local): each individual's modal domain is mixed → .indet. The quantifier sees all gaps. By aggregate_replicate_indet, both ∃ and ∀ return .indet — quantifier strength is invisible.

• must (global): each individual's domain gives ofBool (Bool). The quantifier sees Bools. By aggregate_map_ofBool_mixed, mixed inputs yield .true for ∃ and .false for ∀ — the strength effect.

theorem AghaJeretic2022.shouldEval_indet {World : Type} (domain : List World) (p : World → Bool) (hne : domain.isEmpty = false) (h_not_all : domain.all p = false) (h_not_none : (domain.all fun (w : World) => !p w) = false) : shouldEval domain p = Core.Duality.Truth3.indet

shouldEval for a mixed nonempty domain produces .indet.

theorem AghaJeretic2022.should_erases_strength (n : ℕ) (hn : n > 0) (d : Core.Duality.ProjectionType) : Core.Duality.aggregate d (List.replicate n Core.Duality.Truth3.indet) = Core.Duality.Truth3.indet

should erases strength under embedding: when n individuals each have mixed modal domains, all produce .indet. Any quantifier aggregating these gaps returns .indet — strength is invisible.

theorem AghaJeretic2022.must_strength_effect (bs : List Bool) (h_some_true : bs.any id = true) (h_some_false : (bs.any fun (x : Bool) => !x) = true) : Core.Duality.aggregate Core.Duality.ProjectionType.disjunctive (List.map Core.Duality.Truth3.ofBool bs) = Core.Duality.Truth3.true ∧ Core.Duality.aggregate Core.Duality.ProjectionType.conjunctive (List.map Core.Duality.Truth3.ofBool bs) = Core.Duality.Truth3.false

must produces the strength effect under embedding: when n individuals each have their modal domain evaluated by mustEval (producing ofBool), mixed Bool results distinguish strong from weak quantifiers.

theorem AghaJeretic2022.must_always_determinate (d : Core.Duality.ProjectionType) (bs : List Bool) : Core.Duality.aggregate d (List.map Core.Duality.Truth3.ofBool bs) ≠ Core.Duality.Truth3.indet

must is always determinate under embedding: aggregation over ofBool values never produces a gap, regardless of duality type.

The Core Identity: should = DIST over worlds

The paper's central formal claim is that weak necessity IS plural predication. We prove this by showing shouldEval equals dist (the distributive operator for plural predication from Core.Duality) applied to the evaluation of each world in the domain.

dist results returns:

• .true if all results are true
• .false if all are false
• .gap otherwise

This is exactly what shouldEval computes, with results = domain.map p.

theorem AghaJeretic2022.shouldEval_eq_distList {World : Type} (domain : List World) (p : World → Bool) (hne : domain ≠ []) : shouldEval domain p = Core.Duality.distList domain fun (w : World) => p w = true

shouldEval = DIST over worlds.

shouldEval D p = distList D p for nonempty D — the canonical Core.Duality.distList (Fine super-truth specialized to a List domain with a Boolean predicate) IS what weak necessity computes.

This is the formal proof that weak necessity IS plural predication: the trivalent truth value of "should p" is determined by the DIST operator applied to the pointwise evaluation of p across the modal domain — exactly as "the Xs are P" is determined by DIST applied to the pointwise evaluation of P across the individuals.

The the/all : should/must parallel is not merely an analogy; it is a mathematical identity at the level of truth-value computation.

Hypothesis hne is required because shouldEval [] p = .false (Agha & Jeretič's empty-domain convention) while distList [] p = .true (vacuous super-truth, mathlib's empty-fold convention).

theorem AghaJeretic2022.mustEval_eq_ofBool {World : Type} (domain : List World) (p : World → Bool) : mustEval domain p = Core.Duality.Truth3.ofBool (domain.all p)

mustEval is ofBool ∘ List.all, confirming must stays bivalent.

Sufficient Truth (@cite{kriz-2016}, A&J Appendix 1)

Formalizes the mechanism by which indeterminate (★) sentences are rescued to "true enough" relative to an Question (= QUD). A sentence S is sufficiently true at w w.r.t. issue I iff:

1. S is not false at w: ⟦S⟧(w) ≠ 0
2. There exists an I-equivalent world u where S is true: ⟦S⟧(u) = 1

Condition 2 means the exceptions are in the same Question cell as a satisfying world — they are "irrelevant" to the QUD.

Addressing an Question (def 46): S cannot address issue I if any cell of I contains both worlds where S is true and worlds where S is false. In other words, S must not split any Question cell.

def AghaJeretic2022.sufficientTruth {W : Type} (S : W → Core.Duality.Truth3) (sameCell : W → W → Bool) (w : W) (worlds : List W) : Bool

Sufficient Truth (Križ 2016, A&J def 44). S is true enough at w w.r.t. issue I iff (i) S is not false at w, and (ii) some I-equivalent world makes S true.

Equations

• AghaJeretic2022.sufficientTruth S sameCell w worlds = (S w != Core.Duality.Truth3.false && worlds.any fun (u : W) => sameCell w u && S u == Core.Duality.Truth3.true)

theorem AghaJeretic2022.sufficient_truth_rescues_gap : sufficientTruth (fun (w : Fin 3) => if (w == 0) = true then Core.Duality.Truth3.true else if (w == 1) = true then Core.Duality.Truth3.indet else Core.Duality.Truth3.false) (fun (w u : Fin 3) => w != 2 && u != 2) 1 [0, 1, 2] = true

Sufficient truth rescues an indeterminate sentence when the exceptions are QUD-irrelevant. Example: "You should do every exercise" is ★ when doing most but not all suffices. Under QUD1 ("how to get a perfect grade?"), the exception-worlds (where you skip one exercise but still pass) are equivalent to the satisfying-worlds → rescued to "true enough." Under QUD2 ("what are the minimal requirements?"), they are in different cells → NOT rescued.

theorem AghaJeretic2022.strict_qud_blocks_rescue : sufficientTruth (fun (w : Fin 3) => if (w == 0) = true then Core.Duality.Truth3.true else if (w == 1) = true then Core.Duality.Truth3.indet else Core.Duality.Truth3.false) (fun (w u : Fin 3) => w == u) 1 [0, 1, 2] = false

The CF operator for French-type languages

The X operator (§5.1) requires a UNIQUE minimal witness set (via ι). This explains Javanese NE: ∀ has one minimal witness (the full domain), ∃ has many (each singleton), so NE only applies to necessity.

French counterfactual morphology is less restrictive: CF picks SOME witness set (not necessarily unique), so it applies to both necessity and possibility modals: devrais (necessity+CF) and pourrais (possibility+CF).

The difference: X = λM. ⊕ ιW[W ∈ WIT(M)] (unique, partial) CF = λM. ⊕ W for some W ∈ WIT(M) (existential, total)

def AghaJeretic2022.hasCFWitness {World : Type} [BEq World] (q : List World → Bool) (candidates : List (List World)) : Bool

CF operator: checks whether SOME minimal witness set exists. Unlike X (which requires uniqueness), CF is defined whenever at least one minimal witness exists — which is always, for any non-empty quantifier domain.

Equations

• AghaJeretic2022.hasCFWitness q candidates = candidates.any (AghaJeretic2022.isMinimalWitness q)

theorem AghaJeretic2022.cf_defined_for_universal : hasCFWitness (universalQ [0, 1]) [[0], [1], [0, 1]] = true

CF is defined for both ∀ and ∃ (both have minimal witnesses).

theorem AghaJeretic2022.cf_defined_for_existential : hasCFWitness (existentialQ [0, 1]) [[0], [1], [0, 1]] = true

def AghaJeretic2022.hasUniqueWitness {World : Type} [BEq World] (q : List World → Bool) (candidates : List (List World)) : Bool

X (unique minimal witness) is defined for ∀ but not ∃. Here "unique" means exactly one candidate is a minimal witness.

Equations

• AghaJeretic2022.hasUniqueWitness q candidates = ((List.filter (AghaJeretic2022.isMinimalWitness q) candidates).length == 1)

theorem AghaJeretic2022.x_defined_for_universal : hasUniqueWitness (universalQ [0, 1]) [[0], [1], [0, 1]] = true

theorem AghaJeretic2022.x_undefined_for_existential : hasUniqueWitness (existentialQ [0, 1]) [[0], [1], [0, 1]] = false

theorem AghaJeretic2022.typological_prediction : hasUniqueWitness (universalQ [0, 1]) [[0], [1], [0, 1]] = true ∧ hasUniqueWitness (existentialQ [0, 1]) [[0], [1], [0, 1]] = false ∧ hasCFWitness (universalQ [0, 1]) [[0], [1], [0, 1]] = true ∧ hasCFWitness (existentialQ [0, 1]) [[0], [1], [0, 1]] = true

The typological prediction: X (Javanese NE) restricts to necessity; CF (French counterfactual) applies to both.

Cross-linguistic fragment verification

Bridge theorems connecting the morphological data (§9) to the actual fragment entries, verifying that the linguistic analysis is reflected in the formal lexical entries.

theorem AghaJeretic2022.javanese_mesthi_strong : (Fragments.Javanese.Modals.mesthi.meaning.all fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.necessity) = true

mesthi is strong necessity in the Javanese fragment.

theorem AghaJeretic2022.javanese_mesthi_ne_weak : (Fragments.Javanese.Modals.mesthiNe.meaning.all fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.weakNecessity) = true

mesthi-ne is weak necessity — NE shifts strong to weak.

theorem AghaJeretic2022.javanese_ne_shifts_force : (Fragments.Javanese.Modals.mesthi.meaning.all fun (x : Core.Modality.ForceFlavor) => x.flavor == Core.Modality.ModalFlavor.epistemic) = true ∧ (Fragments.Javanese.Modals.mesthiNe.meaning.all fun (x : Core.Modality.ForceFlavor) => x.flavor == Core.Modality.ModalFlavor.epistemic) = true ∧ (Fragments.Javanese.Modals.mesthi.meaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.necessity) = true ∧ (Fragments.Javanese.Modals.mesthiNe.meaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.weakNecessity) = true

The NE morpheme shifts force: mesthi and mesthi-ne share epistemic flavor but differ in force.

theorem AghaJeretic2022.javanese_no_weak_possibility : (Fragments.Javanese.Modals.allExpressions.all fun (e : Semantics.Modality.Typology.ModalExpression) => (e.meaning.all fun (x : Core.Modality.ForceFlavor) => x.force != Core.Modality.ModalForce.weakNecessity) || e.meaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.weakNecessity) = true

iso (possibility) has NO -ne form: *iso-ne is ungrammatical. Verified by checking that no weak-possibility expression exists.

theorem AghaJeretic2022.javanese_kudu_ne_weak : (Fragments.Javanese.Modals.kudu1.meaning.all fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.necessity) = true ∧ (Fragments.Javanese.Modals.kudu1Ne.meaning.all fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.weakNecessity) = true

kudu strong → kudu-ne weak, paralleling mesthi → mesthi-ne.

theorem AghaJeretic2022.french_cf_weakens : Fragments.French.Modals.devoir.force = Core.Modality.ModalForce.necessity ∧ Fragments.French.Modals.devrais.force = Core.Modality.ModalForce.weakNecessity

French devoir is strong necessity; devrais (devoir+CF) is weak.

theorem AghaJeretic2022.french_devrais_same_flavors : Fragments.French.Modals.devrais.flavors = Fragments.French.Modals.devoir.flavors

Devrais preserves devoir's flavor polysemy: both are epistemic/deontic/circumstantial.