Agha and Jeretič (2026): Modal force and its realization across languages

This file formalizes the tests and typologies of [AJ26]'s survey of modal force. Weak necessity is weaker than strong necessity: a strong necessity conjoined with the denial of another over one domain is contradictory and the conjunction of two is trivial, while should φ but you don't have to is consistent and should φ, and in fact you must is informative ((6), (8), (11), (12)); the decided paradigm of [Fer23] derives this from the force scale, and the chapter's rows exhibit it across languages. Of the three analyses the chapter surveys, domain restriction ([vFI08]), comparison ([Rub14]) and plural predication ([AJ22]), the first neg-raises only over a decided domain. Polarity-sensitive variable-force modals are possibility modals whose necessity readings arise from what they project ([Dea11], [Jer21b], [New22]): the projections of Nez Perce o'qa, Siona ba'iji, Swedish får and Kinande anga license the readings of the chapter's table in each environment, and exhaustifying a possibility modal over its subdomain alternatives yields necessity ([BLF20]). The scope of the necessity modals under negation and the determiner–modal generalization for infinitival relatives ([HN99a]) are stated over the rows.

Main definitions

• Projection, Available: what a possibility modal projects, and the readings a projection licenses in an environment.

Main results

• contradiction_tests, triviality_tests, tests_predicted, crosslinguistic_tests: (6), (8), (11) and (12) from the force scale, and the chapter's judgments row by row.
• vfiWeak_negRaises_iff: domain-restriction weak necessity neg-raises for every prejacent at once only in the one-world limit of its domain.
• projection_matches_table, readings_licensed: the four projections license exactly the readings of the chapter's table, and every reading of its examples.
• exh_subdomain: (50), exhaustification over the subdomain alternatives is necessity over the domain.
• weak_never_narrow, must_narrow_iff_higher, haveTo_always_narrow, strong_determiner_should: the scope and infinitival-relative generalizations over the rows.

Implementation notes

• Available transcribes the chapter's reasoning about each cell of its table; only the exhaustification step is derived. anga's prunable bit is idle, since its secondary ordering already yields weak necessity; why anga cannot prune paswa as får prunes behöva is the question the chapter leaves open.
• On must under higher negation the chapter and the rows of [Rub14] agree: both reject the reading with the negation inside the modal's scope.

TODO

• The discourse-sensitive variable-force modals, the overt exhaustifiers, collapse variable force and the covert modals of the final section have no formal counterpart.

References

• [AJ26]
• [AJ22]
• [Fer23]
• [vFI08]
• [Rub14]
• [Hor01]
• [Dea11]
• [Jer21a]
• [Jer21b]
• [New22]
• [BLF20]
• [HN99a]
• [WH24]

Weak and strong necessity (§2.1)

theorem AghaJeretic2026.contradiction_tests : { first := { force := Modality.ModalForce.necessity, negModal := false, negPrejacent := false }, second := { force := Modality.ModalForce.necessity, negModal := true, negPrejacent := false } }.Contradictory ∧ { first := { force := Modality.ModalForce.weakNecessity, negModal := false, negPrejacent := false }, second := { force := Modality.ModalForce.necessity, negModal := true, negPrejacent := false } }.Consistent

A strong necessity conjoined with the denial of a strong necessity over one domain is contradictory, and a weak necessity conjoined with it is consistent, (6) and (8).

theorem AghaJeretic2026.triviality_tests : { force := Modality.ModalForce.necessity, negModal := false, negPrejacent := false }.Entails { force := Modality.ModalForce.necessity, negModal := false, negPrejacent := false } ∧ ¬{ force := Modality.ModalForce.weakNecessity, negModal := false, negPrejacent := false }.Entails { force := Modality.ModalForce.necessity, negModal := false, negPrejacent := false }

A strong necessity after a strong necessity is trivial, and after a weak necessity informative, (11) and (12).

def AghaJeretic2026.forceTable : List (String × Modality.ModalForce)

The force a row names.

Equations

• AghaJeretic2026.forceTable = [("strong", Modality.ModalForce.necessity), ("weak", Modality.ModalForce.weakNecessity)]

theorem AghaJeretic2026.tests_covered (e : Datum) : e ∈ Examples.all → (e.feature? "test").isSome = true → (e.feature? "first").isSome = true ∧ (e.feature? "second").isSome = true ∨ (e.feature? "force").isSome = true

Every row of a test names the forces of its conjuncts, or the force of its modal.

theorem AghaJeretic2026.tests_predicted (e : Datum) : e ∈ Examples.all → ∀ f₁ ∈ e.parse? "first" forceTable, ∀ f₂ ∈ e.parse? "second" forceTable, (e.feature? "test" = some "contradiction" → (e.judgment = Judgment.unacceptable ↔ { first := { force := f₁, negModal := false, negPrejacent := false }, second := { force := f₂, negModal := true, negPrejacent := false } }.Contradictory)) ∧ (e.feature? "test" = some "triviality" → (e.judgment = Judgment.unacceptable ↔ { force := f₁, negModal := false, negPrejacent := false }.Entails { force := f₂, negModal := false, negPrejacent := false }))

In the chapter's English tests, □₁ φ ∧ ¬□₂ φ is contradictory and □₁ φ ∧ □₂ φ trivial exactly when the first force entails the second.

theorem AghaJeretic2026.crosslinguistic_tests (e : Datum) : e ∈ Examples.all → e.feature? "test" = some "contradiction" → ∀ φ ∈ e.parse? "force" forceTable, e.judgment = Judgment.acceptable ↔ { first := { force := φ, negModal := false, negPrejacent := false }, second := { force := Modality.ModalForce.necessity, negModal := true, negPrejacent := false } }.Consistent

Across languages, a necessity modal survives the denial of strong necessity exactly when its force is weak, (15)–(17), (26) and (28).

theorem AghaJeretic2026.vfiWeak_negRaises_iff {W : Type u_1} (f g g' : Modality.Background W) (w : W) : (∀ (p : W → Prop), ¬Modality.Directive.weakNecessity f g g' p w → Modality.Directive.weakNecessity f g g' (fun (w' : W) => ¬p w') w) ↔ ((Modality.premisePreorder (g' w)).minimals (Modality.bestWorlds f g w)).Subsingleton

Domain-restriction weak necessity neg-raises for every prejacent at once exactly when its nested best-world domain has at most one world, the dichotomous limit [Hor01] excludes from neg-raising: a library observation, where the chapter's §2.5 only remarks that a non-quantificational semantics may fare better on the neg-raising facts.

Scope under negation ((18)–(20))

theorem AghaJeretic2026.weak_never_narrow (e : Datum) : e ∈ Examples.all → e.feature? "force" = some "weak" → (e.feature? "negation").isSome = true → List.lookup "wide" e.readings = some Judgment.acceptable ∧ List.lookup "narrow" e.readings = some Judgment.unacceptable

A weak necessity modal never takes scope below negation.

theorem AghaJeretic2026.must_narrow_iff_higher (e : Datum) : e ∈ Examples.all → e.feature? "modal" = some "must" → (List.lookup "narrow" e.readings = some Judgment.acceptable ↔ e.feature? "negation" = some "higher")

Must takes scope below negation exactly when the negation is in a higher clause.

theorem AghaJeretic2026.haveTo_always_narrow (e : Datum) : e ∈ Examples.all → e.feature? "modal" = some "have to" → List.lookup "narrow" e.readings = some Judgment.acceptable ∧ List.lookup "wide" e.readings = some Judgment.unacceptable

Have to takes scope below negation wherever the negation is.

Polarity-sensitive variable force (§3)

inductive AghaJeretic2026.Environment : Type

The environments the typology distinguishes.

• unembedded : Environment

  An unembedded clause.

• clausemateNegation : Environment

  Under a clausemate negation.

• otherDE : Environment

  Another downward-entailing context.

@[instance_reducible]

instance AghaJeretic2026.instDecidableEqEnvironment : DecidableEq Environment

Equations

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

def AghaJeretic2026.instReprEnvironment.repr : Environment → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AghaJeretic2026.instReprEnvironment : Repr Environment

Equations

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

structure AghaJeretic2026.Projection : Type

What a possibility modal projects ([Jer21a], [Jer21b], [New22]).

• subdomain : Bool

  Subdomain alternatives.

• scalemate : Bool

  A strong-necessity scalemate.

• prunable : Bool

  The scalemate can be pruned.

• secondaryOrdering : Bool

  The domain is restricted by a secondary ordering source.

@[instance_reducible]

instance AghaJeretic2026.instDecidableEqProjection : DecidableEq Projection

Equations

• AghaJeretic2026.instDecidableEqProjection = AghaJeretic2026.instDecidableEqProjection.decEq

def AghaJeretic2026.instDecidableEqProjection.decEq (x✝ x✝¹ : Projection) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance AghaJeretic2026.instReprProjection : Repr Projection

Equations

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

def AghaJeretic2026.instReprProjection.repr : Projection → ℕ → Std.Format

Equations

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

def AghaJeretic2026.Available (π : Projection) : Environment → Modality.ModalForce → Prop

The readings a projection licenses in an environment. Unembedded, obligatory exhaustification of subdomain alternatives removes the possibility reading unless a scalemate supplies it, and strengthens to strong or weak necessity according to the domain; under clausemate negation there is no clause boundary for the exhaustifier, and the necessity reading is no special case of possibility; in other downward-entailing contexts exhaustification is optional.

Equations

• One or more equations did not get rendered due to their size.
• AghaJeretic2026.Available π AghaJeretic2026.Environment.unembedded Modality.ModalForce.possibility = (¬π.subdomain = true ∨ π.scalemate = true)
• AghaJeretic2026.Available π AghaJeretic2026.Environment.unembedded Modality.ModalForce.weakNecessity = (π.subdomain = true ∧ π.secondaryOrdering = true)
• AghaJeretic2026.Available π AghaJeretic2026.Environment.clausemateNegation x✝ = (x✝ = Modality.ModalForce.possibility)
• AghaJeretic2026.Available π AghaJeretic2026.Environment.otherDE Modality.ModalForce.possibility = True
• AghaJeretic2026.Available π AghaJeretic2026.Environment.otherDE Modality.ModalForce.necessity = (π.subdomain = true ∧ ¬π.secondaryOrdering = true)
• AghaJeretic2026.Available π AghaJeretic2026.Environment.otherDE Modality.ModalForce.weakNecessity = (π.subdomain = true ∧ π.secondaryOrdering = true)

@[instance_reducible]

instance AghaJeretic2026.instDecidableAvailable (π : Projection) (env : Environment) (r : Modality.ModalForce) : Decidable (Available π env r)

Equations

• One or more equations did not get rendered due to their size.
• AghaJeretic2026.instDecidableAvailable π AghaJeretic2026.Environment.clausemateNegation x✝ = AghaJeretic2026.instDecidableAvailable._aux_4 π x✝
• AghaJeretic2026.instDecidableAvailable π AghaJeretic2026.Environment.otherDE Modality.ModalForce.possibility = { decide := true, reflects_decide := ⋯ }

def AghaJeretic2026.oqa : Projection

Nez Perce o'qa projects nothing ([Dea11]).

Equations

• AghaJeretic2026.oqa = { subdomain := false, scalemate := false, prunable := false, secondaryOrdering := false }

def AghaJeretic2026.baiji : Projection

Siona ba'iji projects subdomain alternatives and has no scalemate.

Equations

• AghaJeretic2026.baiji = { subdomain := true, scalemate := false, prunable := false, secondaryOrdering := false }

def AghaJeretic2026.får : Projection

Swedish får projects subdomain alternatives and a prunable scalemate, behöva.

Equations

• AghaJeretic2026.får = { subdomain := true, scalemate := true, prunable := true, secondaryOrdering := false }

def AghaJeretic2026.anga : Projection

Kinande anga projects subdomain alternatives, has the scalemate paswa, and quantifies over a doubly restricted domain.

Equations

• AghaJeretic2026.anga = { subdomain := true, scalemate := true, prunable := false, secondaryOrdering := true }

def AghaJeretic2026.projection? (e : Datum) : Option Projection

The projection a row concerns.

Equations

• AghaJeretic2026.projection? e = e.parse? "modal" [("o'qa", AghaJeretic2026.oqa), ("ba'iji", AghaJeretic2026.baiji), ("får", AghaJeretic2026.får), ("anga", AghaJeretic2026.anga)]

def AghaJeretic2026.environment? (e : Datum) : Option Environment

The environment a row concerns.

Equations

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

def AghaJeretic2026.forceKey : Modality.ModalForce → String

The key under which a row records a force's reading.

Equations

• AghaJeretic2026.forceKey Modality.ModalForce.possibility = "possibility"
• AghaJeretic2026.forceKey Modality.ModalForce.necessity = "necessity"
• AghaJeretic2026.forceKey Modality.ModalForce.weakNecessity = "weak necessity"

theorem AghaJeretic2026.projection_matches_table (e : Datum) : e ∈ Examples.all → e.feature? "table" = some "true" → ∀ π ∈ projection? e, ∀ env ∈ environment? e, ∀ (r : Modality.ModalForce), List.lookup (forceKey r) e.readings = some Judgment.acceptable ↔ Available π env r

The projections license exactly the readings the chapter's table records.

theorem AghaJeretic2026.readings_licensed (e : Datum) : e ∈ Examples.all → ∀ π ∈ projection? e, ∀ env ∈ environment? e, ∀ (r : Modality.ModalForce), (List.lookup (forceKey r) e.readings = some Judgment.acceptable → Available π env r) ∧ (List.lookup (forceKey r) e.readings = some Judgment.unacceptable → ¬Available π env r)

Every reading the chapter's examples record is licensed, and every reading they exclude is not.

Exhaustification of subdomain alternatives (§3.2)

theorem AghaJeretic2026.exh_subdomain {ι : Type u_2} [DecidableEq ι] (M : Finset ι) (hM : M.Nonempty) : Exhaustification.exhIEII (supClosure ((fun (i : ι) => {s : ι → Bool | s i = true}) '' ↑M)) (⋃ i ∈ M, {s : ι → Bool | s i = true}) = ⋂ i ∈ M, {s : ι → Bool | s i = true}

Over a nonempty domain, exhaustifying the possibility modal, the disjunction of the prejacent over the domain, against its subdomain alternatives yields necessity, the prejacent at every world of the domain, (50). Worlds are the states recording where the prejacent holds.

Covert modality (§4)

theorem AghaJeretic2026.strong_determiner_should (e : Datum) : e ∈ Examples.all → e.feature? "construction" = some "infinitival relative" → List.lookup "should" e.readings = some Judgment.acceptable ∧ (List.lookup "could" e.readings = some Judgment.acceptable ↔ e.feature? "determiner" = some "weak")

In infinitival relatives a strong determiner forces the should reading and excludes the could reading, where a weak determiner allows both, (90)–(92).