On Necessity and Comparison

@cite{rubinstein-2014}

Pacific Philosophical Quarterly 95(4): 512–554.

Core Proposal

Weak necessity modals (ought, should) and evaluative comparative predicates (better, good, preferable, worthwhile) form a natural class: both have comparative semantics grounded in Kratzer's ordering sources, and both are associated with negotiable ideals — priorities not universally endorsed by all discourse participants.

This is the third of three competing analyses of weak necessity surveyed in @cite{agha-jeretic-2026} §2.2:

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}): this file

Key Claims Formalized

1. Two kinds of priorities (§3.2): Non-negotiable priorities are promoted to modal-base status (restricting accessible worlds); negotiable priorities remain as ordering source material (ranking worlds).

2. Favored worlds (§3.2, def 40): worlds compatible with facts and non-negotiable priorities, via Frank (1996) compatibility-restricted union.

3. Strong necessity (§3.2, def 41): ∀w' ∈ Fav(f,h,e). p(w') — universal quantification over favored worlds, NO ordering source.

4. Weak necessity (§3.2, def 42): ∀w' ∈ BEST(Fav(f,h,e), g(e)). p(w') — universal quantification over the best favored worlds, ordered by negotiable ideals. This IS the comparative component.

5. Negotiability (§3.3, def 49): A premise set is negotiable iff not all discourse participants are committed to it. BEST is only defined when the ordering source is negotiable.

6. Hebrew evidence (§2.1): Hebrew lacks a lexical weak necessity modal; comparative evaluatives (yoter tov, adif, kday) serve as translations.

7. Neg-raising (§2.2): Weak necessity modals and evaluative comparatives are neg-raisers; strong necessity modals are not.

Theoretical Disagreement with @cite{agha-jeretic-2022}

Both accounts agree on the data: "I don't think you should go" has a lower-negation reading, while "I don't think you have to go" does not (for most speakers). They disagree on the mechanism:

• Rubinstein: should genuinely neg-raises (pragmatic O→E strengthening, following @cite{horn-2001}). Strong necessity modals do NOT neg-raise.
• Agha & Jeretič: should's apparent neg-raising is scopelessness (homogeneity), not true neg-raising. must genuinely neg-raises.

Connection to Existing Infrastructure

• Directive.lean provides the @cite{von-fintel-iatridou-2008} analysis where weak necessity = ∀ over a refined best-world set (ordering refinement g ∪ g'). Rubinstein differs by promoting some priorities to modal-base status.
• Under the simplifying assumption that no priorities are promoted (h = ∅), Rubinstein's analysis reduces to standard Kratzer necessity (bridge below).
• FunctionWords.lean classifies English should/ought as weakNecessity and must as necessity, matching Rubinstein's force assignments.

Two kinds of priorities

Rubinstein argues that norms, ideals, and preferences — traditionally all ordering-source material in @cite{kratzer-1981}'s framework — come in two kinds:

• Non-negotiable: promoted to modal-base status. These restrict which worlds are "live possibilities" (the favored worlds).
• Negotiable: remain as ordering-source material. These rank the favored worlds but do not eliminate any from consideration.

Strong necessity modals quantify over all favored worlds (no ordering). Weak necessity modals quantify over the BEST favored worlds (with ordering).

inductive Phenomena.Modality.Studies.Rubinstein2014.Negotiability : Type

Whether a priority is negotiable among discourse participants. A priority is negotiable iff at least one discourse participant is not committed to it (§3.3, definition 49).

• negotiable : Negotiability
• nonNegotiable : Negotiability

instance Phenomena.Modality.Studies.Rubinstein2014.instDecidableEqNegotiability : DecidableEq Negotiability

Equations

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

instance Phenomena.Modality.Studies.Rubinstein2014.instReprNegotiability : Repr Negotiability

Equations

• Phenomena.Modality.Studies.Rubinstein2014.instReprNegotiability = { reprPrec := Phenomena.Modality.Studies.Rubinstein2014.instReprNegotiability.repr }

def Phenomena.Modality.Studies.Rubinstein2014.instReprNegotiability.repr : Negotiability → ℕ → Std.Format

Equations

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

def Phenomena.Modality.Studies.Rubinstein2014.instBEqNegotiability.beq : Negotiability → Negotiability → Bool

Equations

• Phenomena.Modality.Studies.Rubinstein2014.instBEqNegotiability.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Modality.Studies.Rubinstein2014.instBEqNegotiability : BEq Negotiability

Equations

• Phenomena.Modality.Studies.Rubinstein2014.instBEqNegotiability = { beq := Phenomena.Modality.Studies.Rubinstein2014.instBEqNegotiability.beq }

structure Phenomena.Modality.Studies.Rubinstein2014.PriorityTypology : Type

Rubinstein's reconceptualized modal backgrounds (§3.2).

In standard @cite{kratzer-1981}, there is one modal base f and one ordering source g. Rubinstein splits priorities into two components based on negotiability, promoting the non-negotiable part to modal-base status.

• circumstances : Semantics.Modality.Kratzer.ModalBase

  Factual circumstances: standard Kratzer modal base f(e).

• nonNegotiable : Semantics.Modality.Kratzer.ModalBase

  Non-negotiable priorities h(e): promoted to modal-base status. These are norms/ideals that all discourse participants endorse.

• negotiable : Semantics.Modality.Kratzer.OrderingSource

  Negotiable priorities g(e): remain as ordering source. These are ideals promoted by an opinionated assessor but not universally endorsed.

Compatibility-restricted union and favored worlds

The favored worlds are determined by combining factual circumstances with non-negotiable priorities. When priorities are consistent with circumstances, this is simply the intersection of both.

Full definition: Fav(f, h, e) = ∪{∩M : M ∈ f(e) + h(e)} where f(e) + h(e) is Frank (1996)'s compatibility-restricted union (def 39). When h(w) is consistent with f(w), this reduces to ∩(f(w) ∪ h(w)). We implement the consistent case, which covers the paper's examples.

def Phenomena.Modality.Studies.Rubinstein2014.favoredWorlds (pt : PriorityTypology) (w : Semantics.Attitudes.Intensional.World) : List Semantics.Attitudes.Intensional.World

Favored worlds (definition 40, consistent case): worlds satisfying both the factual circumstances f(w) and the non-negotiable priorities h(w).

Equations

• Phenomena.Modality.Studies.Rubinstein2014.favoredWorlds pt w = Semantics.Modality.Kratzer.propIntersection (pt.circumstances w ++ pt.nonNegotiable w)

theorem Phenomena.Modality.Studies.Rubinstein2014.favored_no_promoted (f : Semantics.Modality.Kratzer.ModalBase) (g : Semantics.Modality.Kratzer.OrderingSource) (w : Semantics.Attitudes.Intensional.World) : favoredWorlds { circumstances := f, nonNegotiable := Semantics.Modality.Kratzer.emptyBackground, negotiable := g } w = Semantics.Modality.Kratzer.accessibleWorlds f w

Favored worlds with no non-negotiable priorities reduce to standard Kratzer accessible worlds.

The must/ought split

Strong necessity quantifies over ALL favored worlds (no ordering). Weak necessity quantifies over the BEST favored worlds (ordered by negotiable priorities). This is where the comparative semantics enters: weak necessity uses world ranking, strong necessity does not.

def Phenomena.Modality.Studies.Rubinstein2014.strongNecessityR (pt : PriorityTypology) (p : BProp Semantics.Attitudes.Intensional.World) (w : Semantics.Attitudes.Intensional.World) : Bool

Strong necessity (definition 41): ⟦must⟧ = λpλe∀w'(w' ∈ Fav(f, h, e) → w' ∈ p)

Universal quantification over favored worlds. No ordering source is consulted — strong necessity is non-comparative.

Equations

• Phenomena.Modality.Studies.Rubinstein2014.strongNecessityR pt p w = (Phenomena.Modality.Studies.Rubinstein2014.favoredWorlds pt w).all p

def Phenomena.Modality.Studies.Rubinstein2014.weakNecessityR (pt : PriorityTypology) (p : BProp Semantics.Attitudes.Intensional.World) (w : Semantics.Attitudes.Intensional.World) : Bool

Weak necessity (definition 42): ⟦ought⟧ = λpλe∀w'(w' ∈ BEST(Fav(f, h, e), g(e)) → w' ∈ p)

Universal quantification over the best favored worlds, where "best" is determined by the negotiable ordering source g(e).

Equations

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

Strong necessity entails weak necessity

Since BEST(Fav, g) ⊆ Fav (the best worlds are a subset of all favored worlds), if p holds at all favored worlds, it a fortiori holds at all best favored worlds.

theorem Phenomena.Modality.Studies.Rubinstein2014.strong_entails_weak_R (pt : PriorityTypology) (p : BProp Semantics.Attitudes.Intensional.World) (w : Semantics.Attitudes.Intensional.World) (h : strongNecessityR pt p w = true) : weakNecessityR pt p w = true

Strong necessity entails weak necessity in Rubinstein's framework. Parallel to Directive.strong_entails_weak, but derived from the subset relation BEST(Fav, g) ⊆ Fav.

theorem Phenomena.Modality.Studies.Rubinstein2014.weak_not_entails_strong_R : ¬∀ (pt : PriorityTypology) (p : BProp Semantics.Attitudes.Intensional.World) (w : Semantics.Attitudes.Intensional.World), weakNecessityR pt p w = true → strongNecessityR pt p w = true

The converse fails: weak necessity does NOT entail strong necessity. If p holds at all BEST favored worlds but not at all favored worlds, weak necessity holds but strong necessity does not.

Reduction to standard Kratzer semantics

When no priorities are promoted to modal-base status (h = ∅), Rubinstein's strong necessity reduces to simple Kratzer necessity (no ordering), and her weak necessity reduces to standard Kratzer necessity with the negotiable ordering source.

theorem Phenomena.Modality.Studies.Rubinstein2014.strongR_eq_simpleNecessity (f : Semantics.Modality.Kratzer.ModalBase) (p : BProp Semantics.Attitudes.Intensional.World) (w : Semantics.Attitudes.Intensional.World) : strongNecessityR { circumstances := f, nonNegotiable := Semantics.Modality.Kratzer.emptyBackground, negotiable := Semantics.Modality.Kratzer.emptyBackground } p w = Semantics.Modality.Kratzer.simpleNecessity f p w

With no promoted priorities, Rubinstein's strong necessity equals simple Kratzer necessity (no ordering).

theorem Phenomena.Modality.Studies.Rubinstein2014.weakR_eq_necessity (f : Semantics.Modality.Kratzer.ModalBase) (g : Semantics.Modality.Kratzer.OrderingSource) (p : BProp Semantics.Attitudes.Intensional.World) (w : Semantics.Attitudes.Intensional.World) : weakNecessityR { circumstances := f, nonNegotiable := Semantics.Modality.Kratzer.emptyBackground, negotiable := g } p w = Semantics.Modality.Kratzer.necessity f g p w

With no promoted priorities, Rubinstein's weak necessity equals standard Kratzer necessity under the negotiable ordering.

This is not the same as Directive.weakNecessity — Rubinstein's "weak" with h=∅ equals Directive's "strong" (with g). The analyses differ structurally: Directive treats all priorities as ordering-source material; Rubinstein promotes some to modal-base status.

theorem Phenomena.Modality.Studies.Rubinstein2014.strongR_eq_weakR_trivial (f : Semantics.Modality.Kratzer.ModalBase) (p : BProp Semantics.Attitudes.Intensional.World) (w : Semantics.Attitudes.Intensional.World) : strongNecessityR { circumstances := f, nonNegotiable := Semantics.Modality.Kratzer.emptyBackground, negotiable := Semantics.Modality.Kratzer.emptyBackground } p w = weakNecessityR { circumstances := f, nonNegotiable := Semantics.Modality.Kratzer.emptyBackground, negotiable := Semantics.Modality.Kratzer.emptyBackground } p w

When no priorities are promoted AND no negotiable ordering exists, strong and weak necessity coincide (both = simple necessity).

Weak necessity modals and evaluative comparatives

The central empirical thesis: ought, should, good, better, preferable, and worthwhile share a semantic core — they all involve quantification over BEST worlds ranked by negotiable ordering sources.

In Hebrew, which lacks a lexical weak necessity modal, this natural class is expressed exclusively through comparative evaluative language.

The paper establishes class membership via two diagnostic tests:

• Test 1: "x E q, but doesn't have to q" is felicitous (non-contradictory). This shows E is weaker than strong necessity.
• Test 2: "y has to q, x only E q" sets up a felicitous scalar contrast. This shows E sits below strong necessity on the modal scale.

inductive Phenomena.Modality.Studies.Rubinstein2014.PriorityExpression : Type

A priority-type modal expression: either a modal verb or an evaluative comparative predicate.

• modal (name : String) : PriorityExpression
• evaluativeComp (name : String) : PriorityExpression

def Phenomena.Modality.Studies.Rubinstein2014.instDecidableEqPriorityExpression.decEq (x✝ x✝¹ : PriorityExpression) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Modality.Studies.Rubinstein2014.instDecidableEqPriorityExpression : DecidableEq PriorityExpression

Equations

• Phenomena.Modality.Studies.Rubinstein2014.instDecidableEqPriorityExpression = Phenomena.Modality.Studies.Rubinstein2014.instDecidableEqPriorityExpression.decEq

def Phenomena.Modality.Studies.Rubinstein2014.instReprPriorityExpression.repr : PriorityExpression → ℕ → Std.Format

Equations

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

instance Phenomena.Modality.Studies.Rubinstein2014.instReprPriorityExpression : Repr PriorityExpression

Equations

• Phenomena.Modality.Studies.Rubinstein2014.instReprPriorityExpression = { reprPrec := Phenomena.Modality.Studies.Rubinstein2014.instReprPriorityExpression.repr }

def Phenomena.Modality.Studies.Rubinstein2014.instBEqPriorityExpression.beq : PriorityExpression → PriorityExpression → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Modality.Studies.Rubinstein2014.instBEqPriorityExpression.beq x✝¹ x✝ = false

instance Phenomena.Modality.Studies.Rubinstein2014.instBEqPriorityExpression : BEq PriorityExpression

Equations

• Phenomena.Modality.Studies.Rubinstein2014.instBEqPriorityExpression = { beq := Phenomena.Modality.Studies.Rubinstein2014.instBEqPriorityExpression.beq }

structure Phenomena.Modality.Studies.Rubinstein2014.ComparativeClassMember : Type

Properties shared by the evaluative comparative natural class.

• expression : PriorityExpression
• passesTest1 : Bool

  Passes Test 1: "x E q, but doesn't have to q" is felicitous.

• passesTest2 : Bool

  Passes Test 2: "y has to q, x only E q" is felicitous.

• negRaises : Bool

  Supports neg-raising under higher negation (Horn 1978, 1989).

• priorityOnly : Bool

  Restricted to priority-type (non-epistemic) interpretation.

def Phenomena.Modality.Studies.Rubinstein2014.instReprComparativeClassMember.repr : ComparativeClassMember → ℕ → Std.Format

Equations

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

instance Phenomena.Modality.Studies.Rubinstein2014.instReprComparativeClassMember : Repr ComparativeClassMember

Equations

• Phenomena.Modality.Studies.Rubinstein2014.instReprComparativeClassMember = { reprPrec := Phenomena.Modality.Studies.Rubinstein2014.instReprComparativeClassMember.repr }

def Phenomena.Modality.Studies.Rubinstein2014.shouldMember : ComparativeClassMember

Equations

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

def Phenomena.Modality.Studies.Rubinstein2014.oughtMember : ComparativeClassMember

Equations

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

def Phenomena.Modality.Studies.Rubinstein2014.goodMember : ComparativeClassMember

Modal good (positive form): "it would be good that p" (p. 517). Distinct from better (comparative) — good picks the overall best like ought, while better supports pairwise comparison.

Equations

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

def Phenomena.Modality.Studies.Rubinstein2014.betterMember : ComparativeClassMember

Equations

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

def Phenomena.Modality.Studies.Rubinstein2014.preferableMember : ComparativeClassMember

Equations

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

def Phenomena.Modality.Studies.Rubinstein2014.worthwhileMember : ComparativeClassMember

Equations

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

def Phenomena.Modality.Studies.Rubinstein2014.mustMember : ComparativeClassMember

Equations

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

def Phenomena.Modality.Studies.Rubinstein2014.haveToMember : ComparativeClassMember

Equations

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

def Phenomena.Modality.Studies.Rubinstein2014.needMember : ComparativeClassMember

need fails Tests 1 and 2 (§2.1.2, examples 16, 18–19), aligning with strong necessity. Hebrew carix 'need' similarly aligns with xayav/muxrax 'must'/'obliged' in direct comparison. Note 14 confirms: "we can conclude that need is not a weak modal."

Equations

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

def Phenomena.Modality.Studies.Rubinstein2014.comparativeClass : List ComparativeClassMember

Equations

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

def Phenomena.Modality.Studies.Rubinstein2014.strongNecessityModals : List ComparativeClassMember

Equations

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

theorem Phenomena.Modality.Studies.Rubinstein2014.class_passes_both_tests : (comparativeClass.all fun (m : ComparativeClassMember) => m.passesTest1 && m.passesTest2) = true

All members of the evaluative comparative class pass both scalar tests.

theorem Phenomena.Modality.Studies.Rubinstein2014.class_neg_raises : (comparativeClass.all fun (x : ComparativeClassMember) => x.negRaises) = true

All members of the evaluative comparative class support neg-raising (following Horn's (1978, 1989) classification of weak obligation predicates).

theorem Phenomena.Modality.Studies.Rubinstein2014.strong_fails_tests : (strongNecessityModals.all fun (m : ComparativeClassMember) => !m.passesTest1 && !m.passesTest2) = true

No strong necessity modal passes the scalar tests.

theorem Phenomena.Modality.Studies.Rubinstein2014.strong_no_neg_raising : (strongNecessityModals.all fun (m : ComparativeClassMember) => !m.negRaises) = true

No strong necessity modal supports neg-raising.

theorem Phenomena.Modality.Studies.Rubinstein2014.evaluatives_priority_only : ((List.filter (fun (m : ComparativeClassMember) => match m.expression with | PriorityExpression.evaluativeComp name => true | x => false) comparativeClass).all fun (x : ComparativeClassMember) => x.priorityOnly) = true

Evaluative comparatives are restricted to priority-type interpretation; modal verbs are more flexible (can also be epistemic).

Negotiability explains neg-raising

Rubinstein connects the evaluative comparative class to neg-raising (§3.4): modals and predicates that use negotiable ordering sources have an "opinionated" alternative (□.¬p) available, enabling the excluded-middle inference that underlies neg-raising. Strong necessity modals, which quantify over favored worlds WITHOUT ordering, lack this alternative.

Theoretical disagreement

This classification disagrees with @cite{agha-jeretic-2022} / @cite{agha-jeretic-2026}, who analyze should's apparent neg-raising as homogeneity (scopelessness) and classify must as the genuine neg-raiser. The NegRaisingProfile structure in AghaJeretic2026.lean encodes their opposing classification.

structure Phenomena.Modality.Studies.Rubinstein2014.NegRaisingClassification : Type

Neg-raising availability for a modal or evaluative predicate, following Rubinstein's classification (paper's Table 2, after Horn 1989, p. 323).

• predicate : String
• isWeakNecessity : Bool
• negRaises : Bool

def Phenomena.Modality.Studies.Rubinstein2014.instReprNegRaisingClassification.repr : NegRaisingClassification → ℕ → Std.Format

Equations

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

instance Phenomena.Modality.Studies.Rubinstein2014.instReprNegRaisingClassification : Repr NegRaisingClassification

Equations

• Phenomena.Modality.Studies.Rubinstein2014.instReprNegRaisingClassification = { reprPrec := Phenomena.Modality.Studies.Rubinstein2014.instReprNegRaisingClassification.repr }

instance Phenomena.Modality.Studies.Rubinstein2014.instBEqNegRaisingClassification : BEq NegRaisingClassification

Equations

• Phenomena.Modality.Studies.Rubinstein2014.instBEqNegRaisingClassification = { beq := Phenomena.Modality.Studies.Rubinstein2014.instBEqNegRaisingClassification.beq }

def Phenomena.Modality.Studies.Rubinstein2014.instBEqNegRaisingClassification.beq : NegRaisingClassification → NegRaisingClassification → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Modality.Studies.Rubinstein2014.instBEqNegRaisingClassification.beq x✝¹ x✝ = false

def Phenomena.Modality.Studies.Rubinstein2014.rubinsteinNRClassification : List NegRaisingClassification

Equations

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

theorem Phenomena.Modality.Studies.Rubinstein2014.weak_necessity_iff_negRaises : (rubinsteinNRClassification.all fun (c : NegRaisingClassification) => c.isWeakNecessity == c.negRaises) = true

In Rubinstein's classification, weak necessity = neg-raising. (Compare AghaJeretic2026.shouldProfile.higherNeg_narrowScope = false, which represents the competing analysis where should does NOT neg-raise.)

Negotiable→non-negotiable promotion: should becomes have-to

The paper's central worked example (§3.3): An accountant says "We should report all our revenue" — promoting a negotiable ideal about international revenue. The law about domestic revenue is non-negotiable. Later, if the manager endorses the ideal, the international-revenue clause is promoted to non-negotiable status, making "We have to report all our revenue" appropriate.

We model this with two propositions:

• reportDomestic: a non-negotiable legal obligation (in h)
• reportInternational: a negotiable ideal promoted by the speaker (in g)
• reportAll: the conjunction (the prejacent of should/have-to)

theorem Phenomena.Modality.Studies.Rubinstein2014.tax_should_holds : weakNecessityR Phenomena.Modality.Studies.Rubinstein2014.taxScenarioA✝ Phenomena.Modality.Studies.Rubinstein2014.reportAll✝ Core.Proposition.World4.w0 = true

In scenario A, weak necessity holds: all BEST favored worlds satisfy reportAll (the ordering picks out worlds where international revenue is also reported).

theorem Phenomena.Modality.Studies.Rubinstein2014.tax_must_fails : strongNecessityR Phenomena.Modality.Studies.Rubinstein2014.taxScenarioA✝ Phenomena.Modality.Studies.Rubinstein2014.reportAll✝ Core.Proposition.World4.w0 = false

In scenario A, strong necessity FAILS: not all favored worlds satisfy reportAll (worlds reporting only domestic revenue survive).

theorem Phenomena.Modality.Studies.Rubinstein2014.tax_must_holds_after_promotion : strongNecessityR Phenomena.Modality.Studies.Rubinstein2014.taxScenarioB✝ Phenomena.Modality.Studies.Rubinstein2014.reportAll✝ Core.Proposition.World4.w0 = true

In scenario B (after promotion), strong necessity holds: all favored worlds now satisfy reportAll.

theorem Phenomena.Modality.Studies.Rubinstein2014.should_to_haveto_shift : strongNecessityR Phenomena.Modality.Studies.Rubinstein2014.taxScenarioA✝ Phenomena.Modality.Studies.Rubinstein2014.reportAll✝ Core.Proposition.World4.w0 = false ∧ strongNecessityR Phenomena.Modality.Studies.Rubinstein2014.taxScenarioB✝ Phenomena.Modality.Studies.Rubinstein2014.reportAll✝¹ Core.Proposition.World4.w0 = true

The should→have-to shift: the SAME proposition goes from weak-only to strong necessity when the negotiable ideal is promoted.

Hebrew: A language without lexical weak necessity

Hebrew lacks dedicated lexical items comparable to ought or should, and cannot derive weak necessity compositionally from strong necessity modals (unlike Spanish debería = deber+COND). The best translations use evaluative comparative language (§2.1.3, examples 21–22).

This supports the claim that weak necessity IS comparative: in a language where the comparative route is the ONLY route, it surfaces overtly.

inductive Phenomena.Modality.Studies.Rubinstein2014.WeakNecessityStrategy : Type

Strategies for expressing weak necessity crosslinguistically. Extends the typology in AghaJeretic2022.WeakNecessityMorphology with the evaluative comparative strategy.

• lexical : WeakNecessityStrategy
• compositional : WeakNecessityStrategy
• evaluativeComparative : WeakNecessityStrategy

instance Phenomena.Modality.Studies.Rubinstein2014.instDecidableEqWeakNecessityStrategy : DecidableEq WeakNecessityStrategy

Equations

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

instance Phenomena.Modality.Studies.Rubinstein2014.instReprWeakNecessityStrategy : Repr WeakNecessityStrategy

Equations

• Phenomena.Modality.Studies.Rubinstein2014.instReprWeakNecessityStrategy = { reprPrec := Phenomena.Modality.Studies.Rubinstein2014.instReprWeakNecessityStrategy.repr }

def Phenomena.Modality.Studies.Rubinstein2014.instReprWeakNecessityStrategy.repr : WeakNecessityStrategy → ℕ → Std.Format

Equations

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

def Phenomena.Modality.Studies.Rubinstein2014.instBEqWeakNecessityStrategy.beq : WeakNecessityStrategy → WeakNecessityStrategy → Bool

Equations

• Phenomena.Modality.Studies.Rubinstein2014.instBEqWeakNecessityStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Modality.Studies.Rubinstein2014.instBEqWeakNecessityStrategy : BEq WeakNecessityStrategy

Equations

• Phenomena.Modality.Studies.Rubinstein2014.instBEqWeakNecessityStrategy = { beq := Phenomena.Modality.Studies.Rubinstein2014.instBEqWeakNecessityStrategy.beq }

structure Phenomena.Modality.Studies.Rubinstein2014.WeakNecessityProfile : Type

• language : String
• hasLexicalWN : Bool
• hasCompositionalWN : Bool
• primaryStrategy : WeakNecessityStrategy
• examples : List (String × String)

instance Phenomena.Modality.Studies.Rubinstein2014.instReprWeakNecessityProfile : Repr WeakNecessityProfile

Equations

• Phenomena.Modality.Studies.Rubinstein2014.instReprWeakNecessityProfile = { reprPrec := Phenomena.Modality.Studies.Rubinstein2014.instReprWeakNecessityProfile.repr }

def Phenomena.Modality.Studies.Rubinstein2014.instReprWeakNecessityProfile.repr : WeakNecessityProfile → ℕ → Std.Format

Equations

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

def Phenomena.Modality.Studies.Rubinstein2014.englishWN : WeakNecessityProfile

Equations

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

def Phenomena.Modality.Studies.Rubinstein2014.spanishWN : WeakNecessityProfile

Equations

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

def Phenomena.Modality.Studies.Rubinstein2014.hebrewWN : WeakNecessityProfile

Equations

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

theorem Phenomena.Modality.Studies.Rubinstein2014.hebrew_no_standard_wn : hebrewWN.hasLexicalWN = false ∧ hebrewWN.hasCompositionalWN = false

Hebrew lacks both standard routes to weak necessity.

theorem Phenomena.Modality.Studies.Rubinstein2014.hebrew_uses_evaluative : hebrewWN.primaryStrategy = WeakNecessityStrategy.evaluativeComparative

Hebrew uses evaluative comparatives as its primary strategy.

Deontic necessity is not universally split into strong and weak

Narrog (2010, 2012) surveys 200 genealogically diverse languages. Only 62 (31%) have grammaticalized means for expressing weak deontic necessity. This casts doubt on the universality of weak necessity as a grammatical category, and supports Rubinstein's claim that it surfaces through evaluative comparison when dedicated grammatical means are absent.

Data imported from Core.Modality.DeonticNecessity.

theorem Phenomena.Modality.Studies.Rubinstein2014.weak_rarity : Core.Modality.DeonticNecessity.countOf Core.Modality.DeonticNecessity.DeonticNecessityType.weak = 62

Only 62 of 200 surveyed languages grammaticalize weak deontic necessity. The total exceeds 200 because some languages have modals of multiple types.

Better can do what ought cannot

When multiple alternatives are salient, the morphological comparative better can pairwise compare any two, while modal ought can only pick out the overall best. This follows from the degree semantics: better accesses the ordering directly (comparative), while ought quantifies over the maximal elements (positive/superlative).

Hebrew data (example 25) confirms: adif 'preferable' supports explicit than-clauses (adif ... me-asher 'preferable ... than-that'), making the comparative structure visible.

structure Phenomena.Modality.Studies.Rubinstein2014.ComparisonCapability : Type

Whether a priority expression supports explicit pairwise comparison (comparative morphology with a than-clause).

• expression : String
• supportsPairwiseComparison : Bool
• picksOverallBest : Bool

instance Phenomena.Modality.Studies.Rubinstein2014.instReprComparisonCapability : Repr ComparisonCapability

Equations

• Phenomena.Modality.Studies.Rubinstein2014.instReprComparisonCapability = { reprPrec := Phenomena.Modality.Studies.Rubinstein2014.instReprComparisonCapability.repr }

def Phenomena.Modality.Studies.Rubinstein2014.instReprComparisonCapability.repr : ComparisonCapability → ℕ → Std.Format

Equations

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

def Phenomena.Modality.Studies.Rubinstein2014.betterCapability : ComparisonCapability

Equations

• Phenomena.Modality.Studies.Rubinstein2014.betterCapability = { expression := "better", supportsPairwiseComparison := true, picksOverallBest := false }

def Phenomena.Modality.Studies.Rubinstein2014.goodCapability : ComparisonCapability

Equations

• Phenomena.Modality.Studies.Rubinstein2014.goodCapability = { expression := "good", supportsPairwiseComparison := false, picksOverallBest := true }

def Phenomena.Modality.Studies.Rubinstein2014.oughtCapability : ComparisonCapability

Equations

• Phenomena.Modality.Studies.Rubinstein2014.oughtCapability = { expression := "ought", supportsPairwiseComparison := false, picksOverallBest := true }

theorem Phenomena.Modality.Studies.Rubinstein2014.better_pairwise_ought_not : betterCapability.supportsPairwiseComparison = true ∧ oughtCapability.supportsPairwiseComparison = false ∧ goodCapability.supportsPairwiseComparison = false

better supports pairwise comparison; ought and good do not.

theorem Phenomena.Modality.Studies.Rubinstein2014.ought_best_better_pairwise : oughtCapability.picksOverallBest = true ∧ goodCapability.picksOverallBest = true ∧ betterCapability.picksOverallBest = false

ought and good (positive form) pick the overall best; better (comparative form) just compares pairs.

Fragment-layer verification

The English fragment in FunctionWords.lean independently classifies modals by force. We verify that these classifications match Rubinstein's force assignments: should/ought are weak necessity (comparative class), must is strong necessity (non-comparative).

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

The English fragment classifies should as weak necessity, matching its membership in the evaluative comparative class.

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

The English fragment classifies ought as weak necessity.

theorem Phenomena.Modality.Studies.Rubinstein2014.fragment_must_strong : (Fragments.English.FunctionWords.must.modalMeaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.necessity) = true

The English fragment classifies must as strong necessity.

theorem Phenomena.Modality.Studies.Rubinstein2014.fragment_must_not_weak : (Fragments.English.FunctionWords.must.modalMeaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.weakNecessity) = false

must is NOT classified as weak necessity — confirming it is outside the evaluative comparative natural class.

theorem Phenomena.Modality.Studies.Rubinstein2014.fragment_should_not_strong : (Fragments.English.FunctionWords.should.modalMeaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.necessity) = false

should is NOT classified as strong necessity — confirming the asymmetry: comparative class members have strictly weaker force.

theorem Phenomena.Modality.Studies.Rubinstein2014.fragment_need_strong : (Fragments.English.FunctionWords.need.modalMeaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.necessity) = true

need is classified as strong necessity — matching its exclusion from the evaluative comparative class (§2.1.2, note 14).

theorem Phenomena.Modality.Studies.Rubinstein2014.fragment_need_not_weak : (Fragments.English.FunctionWords.need.modalMeaning.any fun (x : Core.Modality.ForceFlavor) => x.force == Core.Modality.ModalForce.weakNecessity) = false

need is NOT classified as weak necessity — confirming it fails the scalar tests (examples 16, 18–19).