Modal Force and its Realization across Languages

@cite{agha-jeretic-2026}

A handbook chapter surveying modal force phenomena:

• §1: Possibility vs necessity (standard ∀/∃ over possible worlds)
• §2: Weak necessity modals (ought, should) — three competing analyses: (1) domain restriction (@cite{von-fintel-iatridou-2008}, Directive.lean), (2) non-quantificational (@cite{agha-jeretic-2022}, AghaJeretic2022.lean), (3) comparative semantics (@cite{rubinstein-2014}, Rubinstein2014.lean)
• §3: Variable force modals — four cross-linguistic patterns
• §4: Covert variable force (conditionals, generics, imperatives)

Key Claims Formalized

1. Entailment asymmetry (§2.1): Strong necessity modals (must, have to) are mutually entailing (□₁φ ∧ ¬□₂φ is contradictory), but weak necessity modals (ought, should) are consistently weaker (□wφ ∧ ¬□φ is felicitous).

2. Strength ordering: □φ → □wφ → ◇φ (strong necessity entails weak necessity entails possibility).

3. Variable force typology (§3.2): Four patterns of polarity-sensitive variable force modals, distinguished by which readings are available in which environments.

4. Exhaustification analysis (§3.2): Polarity-sensitive variable force modals are underlyingly ◇, with necessity readings derived via EXH.

Connection to @cite{agha-jeretic-2022}

The paper's own prior work proposes that weak necessity modals are non-quantificational (plural predication over worlds), explaining neg-raising asymmetries between should and must.

@[reducible, inline]

abbrev AghaJeretic2026.World : Type

Equations

• AghaJeretic2026.World = Fin 4

Entailment tests from §2.1

Strong necessity modals are mutually entailing: "must" ≈ "have to" ≈ "be required to". But weak necessity modals are strictly weaker: "should φ" does not entail "must φ".

We verify this structurally via ModalForce.atLeastAsStrong.

theorem AghaJeretic2026.strong_entails_strong : Core.Modality.ModalForce.necessity.atLeastAsStrong Core.Modality.ModalForce.necessity = true

Strong necessity entails strong necessity (mutual entailment among "must", "have to", "be required to" — paper ex. 6-7).

theorem AghaJeretic2026.strong_entails_weak_force : Core.Modality.ModalForce.necessity.atLeastAsStrong Core.Modality.ModalForce.weakNecessity = true

Strong necessity entails weak necessity ("must φ" → "ought φ" — paper's key asymmetry).

theorem AghaJeretic2026.weak_not_entails_strong_force : Core.Modality.ModalForce.weakNecessity.atLeastAsStrong Core.Modality.ModalForce.necessity = false

Weak necessity does NOT entail strong necessity ("ought φ" ↛ "must φ" — paper ex. 8-9, 13).

theorem AghaJeretic2026.weak_entails_possibility : Core.Modality.ModalForce.weakNecessity.atLeastAsStrong Core.Modality.ModalForce.possibility = true

Weak necessity entails possibility ("ought φ" → "can φ").

theorem AghaJeretic2026.possibility_not_entails_weak : Core.Modality.ModalForce.possibility.atLeastAsStrong Core.Modality.ModalForce.weakNecessity = false

Possibility does NOT entail weak necessity ("can φ" ↛ "ought φ").

Verify that the English fragment correctly classifies modals by force, matching the paper's §2.1 categorization.

theorem AghaJeretic2026.must_is_strong_necessity : (Fragments.English.Auxiliaries.must.modalMeaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.necessity) = true

"must" is strong necessity (paper ex. 6-7, 11).

theorem AghaJeretic2026.should_is_weak_necessity : (Fragments.English.Auxiliaries.should.modalMeaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.weakNecessity) = true

"should" is weak necessity (paper ex. 8-9, 12-13).

theorem AghaJeretic2026.ought_is_weak_necessity : (Fragments.English.Auxiliaries.ought.modalMeaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.weakNecessity) = true

"ought" is weak necessity (paper ex. 8-9, 12-13).

theorem AghaJeretic2026.may_is_possibility : (Fragments.English.Auxiliaries.may.modalMeaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.possibility) = true

"may" is possibility (paper §1).

theorem AghaJeretic2026.might_is_possibility : (Fragments.English.Auxiliaries.might.modalMeaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.possibility) = true

"might" is possibility (paper §1).

theorem AghaJeretic2026.must_not_weak : (Fragments.English.Auxiliaries.must.modalMeaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.weakNecessity) = false

"must" is NOT classified as weak necessity.

theorem AghaJeretic2026.should_not_strong : (Fragments.English.Auxiliaries.should.modalMeaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.necessity) = false

"should" is NOT classified as strong necessity.

The von Fintel & Iatridou (2008) analysis, surveyed in §2.2.1: weak necessity = ∀ over a refined best-world set. We verify the entailment chain via the proven theorems in Directive.lean.

theorem AghaJeretic2026.must_entails_ought_kratzer (f : Core.Logic.Intensional.ModalBase World) (g g' : Core.Logic.Intensional.OrderingSource World) (p : World → Prop) : ∀ (x : DecidablePred p) (w : World), Semantics.Modality.Directive.strongNecessity f g p w → Semantics.Modality.Directive.weakNecessity f g g' p w

Re-export: strong necessity entails weak necessity (Directive.lean).

theorem AghaJeretic2026.ought_not_entails_must_kratzer : ¬∀ (W : Type) (f : Core.Logic.Intensional.ModalBase W) (g g' : Core.Logic.Intensional.OrderingSource W) (p : W → Prop) (w : W), Semantics.Modality.Directive.weakNecessity f g g' p w → Semantics.Modality.Directive.strongNecessity f g p w

Re-export: the converse fails (Directive.lean).

Polarity-sensitive variable force modals

The paper identifies four patterns (table on p. 26) of how force varies across three environments: unembedded, clausemate negation, and other downward-entailing (DE) contexts.

Key: ◇ = possibility available, □ = necessity available, □w = weak necessity.

Pattern	Language	Modal	Unembedded	Cl. Neg	Other DE
1	Nez Perce	o'qa	◇,□	◇	◇
2	Siona	ba'iji	□	◇	◇,□
3	Swedish	får	◇,□	◇	◇,□
4	Kinande	anga	◇,□w	◇	◇,□w

All four patterns share: under clausemate negation, only ◇ is available.

inductive AghaJeretic2026.ModalEnvironment : Type

The three syntactic environments relevant for variable force.

• unembedded : ModalEnvironment
• clausemateNegation : ModalEnvironment
• otherDE : ModalEnvironment

@[implicit_reducible]

instance AghaJeretic2026.instDecidableEqModalEnvironment : DecidableEq ModalEnvironment

Equations

• AghaJeretic2026.instDecidableEqModalEnvironment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance AghaJeretic2026.instReprModalEnvironment : Repr ModalEnvironment

Equations

• AghaJeretic2026.instReprModalEnvironment = { reprPrec := AghaJeretic2026.instReprModalEnvironment.repr }

def AghaJeretic2026.instReprModalEnvironment.repr : ModalEnvironment → ℕ → Std.Format

Equations

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

structure AghaJeretic2026.VariableForcePattern : Type

A variable force pattern: which forces are available in each environment.

• language : String
• modal : String
• unembedded : List Core.Modality.ModalForce
• clausemateNeg : List Core.Modality.ModalForce
• otherDE : List Core.Modality.ModalForce

def AghaJeretic2026.instReprVariableForcePattern.repr : VariableForcePattern → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AghaJeretic2026.instReprVariableForcePattern : Repr VariableForcePattern

Equations

• AghaJeretic2026.instReprVariableForcePattern = { reprPrec := AghaJeretic2026.instReprVariableForcePattern.repr }

def AghaJeretic2026.pattern1_nezPerce : VariableForcePattern

Pattern 1: Nez Perce o'qa (Deal 2011). Underlying ◇ modal, necessity via entailment in upward-entailing contexts. No scalar alternative → no "not have to" implicature → ◇ subsumes □.

Equations

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

def AghaJeretic2026.pattern2_siona : VariableForcePattern

Pattern 2: Ecuadorian Siona ba'iji (Jeretič 2021a,b). Underlying ◇, necessity via obligatory scaleless implicature (EXH). Unembedded: EXH obligatory → only □. Under negation: only ◇. Other DE: EXH optional → ◇ or □.

Equations

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

def AghaJeretic2026.pattern3_swedish : VariableForcePattern

Pattern 3: Swedish får (Jeretič 2021a). Underlying ◇ with optional scalar/scaleless implicature. Both readings available unembedded. Under negation: only ◇.

Equations

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

def AghaJeretic2026.pattern4_kinande : VariableForcePattern

Pattern 4: Kinande anga (Newkirk 2022a,b). Underlying ◇, can reach □w but never full □ (blocked by paswa). The secondary ordering source yields weak, not strong, necessity.

Equations

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

def AghaJeretic2026.variableForcePatterns : List VariableForcePattern

Equations

• AghaJeretic2026.variableForcePatterns = [AghaJeretic2026.pattern1_nezPerce, AghaJeretic2026.pattern2_siona, AghaJeretic2026.pattern3_swedish, AghaJeretic2026.pattern4_kinande]

theorem AghaJeretic2026.all_clausemate_neg_is_possibility : (variableForcePatterns.all fun (p : VariableForcePattern) => p.clausemateNeg == [Core.Modality.ModalForce.possibility]) = true

Universal generalization: under clausemate negation, all four variable force modals have only a possibility reading.

theorem AghaJeretic2026.all_have_possibility_everywhere : (variableForcePatterns.all fun (p : VariableForcePattern) => (p.unembedded.any fun (x : Core.Modality.ModalForce) => x == Core.Modality.ModalForce.possibility) || p.unembedded == [Core.Modality.ModalForce.necessity]) = true

All four patterns have possibility available in every environment.

theorem AghaJeretic2026.four_patterns : variableForcePatterns.length = 4

Four patterns, four languages.

EXH-based strengthening

The paper formalizes the exhaustification analysis for Siona ba'iji: ⟦ba'iji_M p⟧ = ∃w ∈ M. p(w) — underlying possibility Alt(ba'iji_M p) = {∃w ∈ M'. p(w) | M' ⊆ M} — subdomain alternatives ⟦EXH ba'iji_M p⟧ ≡ ∀w ∈ M. p(w) — strengthened to necessity

We model this as: EXH over subdomain alternatives of ◇ yields □.

def AghaJeretic2026.exhStrengthens (domain : List Bool) : Bool

Exhaustification of a possibility modal over subdomain alternatives yields necessity: negating all proper-subdomain existentials forces the prejacent to hold at every world in the domain.

Equations

• AghaJeretic2026.exhStrengthens domain = (domain.any id && domain.all id)

theorem AghaJeretic2026.exh_all_true : exhStrengthens [true, true, true] = true

EXH strengthening works: if all worlds satisfy p, exhaustification of ◇ over subdomain alternatives yields □.

theorem AghaJeretic2026.exh_mixed_false : exhStrengthens [true, false, true] = false

EXH fails when not all worlds satisfy p: ◇ holds but □ doesn't, so the exhaustified reading (= □) is false.

theorem AghaJeretic2026.exh_empty : exhStrengthens [] = false

Empty domain: both ◇ and □ vacuously fail.

Non-quantificational analysis

@cite{agha-jeretic-2022} observe that weak necessity modals are scopeless with respect to negation (like plural predication), while strong necessity modals (some of them) are neg-raisers:

• "should not go" = only □ > ¬ (wide scope)
• "must not go" = □ > ¬ (wide scope), but also available: ¬ > □ via neg-raising
• "have to not go" = only □ > ¬ (wide scope, no neg-raising)

Under higher-clause negation:

• "doesn't think Bill should go" = ✓ □ > ¬; * ¬ > □
• "doesn't think Bill must go" = * □ > ¬; ✓ ¬ > □

The weak necessity modal should never takes scope below negation, while the strong necessity modal must does (via neg-raising).

structure AghaJeretic2026.NegRaisingProfile : Type

Neg-raising availability for a modal operator.

• modal : String
• clausemateNeg_wideScope : Bool
• higherNeg_narrowScope : Bool

@[implicit_reducible]

instance AghaJeretic2026.instReprNegRaisingProfile : Repr NegRaisingProfile

Equations

• AghaJeretic2026.instReprNegRaisingProfile = { reprPrec := AghaJeretic2026.instReprNegRaisingProfile.repr }

def AghaJeretic2026.instReprNegRaisingProfile.repr : NegRaisingProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AghaJeretic2026.instBEqNegRaisingProfile : BEq NegRaisingProfile

Equations

• AghaJeretic2026.instBEqNegRaisingProfile = { beq := AghaJeretic2026.instBEqNegRaisingProfile.beq }

def AghaJeretic2026.instBEqNegRaisingProfile.beq : NegRaisingProfile → NegRaisingProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• AghaJeretic2026.instBEqNegRaisingProfile.beq x✝¹ x✝ = false

def AghaJeretic2026.shouldProfile : NegRaisingProfile

Equations

• AghaJeretic2026.shouldProfile = { modal := "should", clausemateNeg_wideScope := true, higherNeg_narrowScope := false }

def AghaJeretic2026.mustProfile : NegRaisingProfile

Equations

• AghaJeretic2026.mustProfile = { modal := "must", clausemateNeg_wideScope := true, higherNeg_narrowScope := true }

def AghaJeretic2026.haveToProfile : NegRaisingProfile

Equations

• AghaJeretic2026.haveToProfile = { modal := "have to", clausemateNeg_wideScope := true, higherNeg_narrowScope := false }

theorem AghaJeretic2026.should_no_neg_raising : shouldProfile.higherNeg_narrowScope = false

Weak necessity modals do not neg-raise; some strong necessity modals do. This asymmetry motivates the non-quantificational analysis.

theorem AghaJeretic2026.must_neg_raises : mustProfile.higherNeg_narrowScope = true