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).
• Auxiliaries.lean classifies English should/ought as weakNecessity and must as necessity, matching Rubinstein's force assignments.

@[reducible, inline]

abbrev Rubinstein2014.World : Type

Equations

• Rubinstein2014.World = Fin 4

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

@[implicit_reducible]

instance Rubinstein2014.instDecidableEqNegotiability : DecidableEq Negotiability

Equations

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

@[implicit_reducible]

instance Rubinstein2014.instReprNegotiability : Repr Negotiability

Equations

• Rubinstein2014.instReprNegotiability = { reprPrec := Rubinstein2014.instReprNegotiability.repr }

def Rubinstein2014.instReprNegotiability.repr : Negotiability → ℕ → Std.Format

Equations

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

structure 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 : Core.Logic.Intensional.ModalBase World

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

• nonNegotiable : Core.Logic.Intensional.ModalBase World

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

• negotiable : Core.Logic.Intensional.OrderingSource World

  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 Rubinstein2014.favoredWorlds (pt : PriorityTypology) (w : World) : Set World

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

Equations

• Rubinstein2014.favoredWorlds pt w = Core.Logic.Intensional.Premise.propIntersection (pt.circumstances w ++ pt.nonNegotiable w)

theorem Rubinstein2014.favored_no_promoted (f : Core.Logic.Intensional.ModalBase World) (g : Core.Logic.Intensional.OrderingSource World) (w : World) : favoredWorlds { circumstances := f, nonNegotiable := Core.Logic.Intensional.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 Rubinstein2014.strongNecessityR (pt : PriorityTypology) (p : World → Prop) (w : World) : Prop

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

• Rubinstein2014.strongNecessityR pt p w = ∀ w' ∈ Rubinstein2014.favoredWorlds pt w, p w'

def Rubinstein2014.weakNecessityR (pt : PriorityTypology) (p : World → Prop) (w : World) : Prop

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

• Rubinstein2014.weakNecessityR pt p w = ∀ w' ∈ Semantics.Modality.Kratzer.bestAmong (Rubinstein2014.favoredWorlds pt w) (pt.negotiable w), p w'

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 Rubinstein2014.strong_entails_weak_R (pt : PriorityTypology) (p : World → Prop) [DecidablePred p] (w : World) (h : strongNecessityR pt p w) : weakNecessityR pt p w

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.

@[implicit_reducible]

instance Rubinstein2014.instDecidablePredWorldCe_p : DecidablePred Rubinstein2014.ce_p✝

Equations

• Rubinstein2014.instDecidablePredWorldCe_p w = decEq w 1

theorem Rubinstein2014.weak_not_entails_strong_R : ¬∀ (pt : PriorityTypology) (p : World → Prop) [DecidablePred p] (w : World), weakNecessityR pt p w → strongNecessityR pt p w

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.

Concretely: with circumstances = nonNegotiable = ∅ and negotiable = [λw => w = (1 : World)], we have favoredWorlds ce_pt (0 : World) = Set.univ and bestAmong univ [λw => w = (1 : World)] = {(1 : World)}. Thus ce_p (which says w = (1 : World)) holds at all best worlds but not at all favored worlds.

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 Rubinstein2014.strongR_eq_simpleNecessity (f : Core.Logic.Intensional.ModalBase World) (p : World → Prop) [DecidablePred p] (w : World) : strongNecessityR { circumstances := f, nonNegotiable := Core.Logic.Intensional.emptyBackground, negotiable := Core.Logic.Intensional.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 Rubinstein2014.weakR_eq_necessity (f : Core.Logic.Intensional.ModalBase World) (g : Core.Logic.Intensional.OrderingSource World) (p : World → Prop) [DecidablePred p] (w : World) : weakNecessityR { circumstances := f, nonNegotiable := Core.Logic.Intensional.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 Rubinstein2014.strongR_eq_weakR_trivial (f : Core.Logic.Intensional.ModalBase World) (p : World → Prop) [DecidablePred p] (w : World) : strongNecessityR { circumstances := f, nonNegotiable := Core.Logic.Intensional.emptyBackground, negotiable := Core.Logic.Intensional.emptyBackground } p w ↔ weakNecessityR { circumstances := f, nonNegotiable := Core.Logic.Intensional.emptyBackground, negotiable := Core.Logic.Intensional.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 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

@[implicit_reducible]

instance Rubinstein2014.instDecidableEqPriorityExpression : DecidableEq PriorityExpression

Equations

• Rubinstein2014.instDecidableEqPriorityExpression = Rubinstein2014.instDecidableEqPriorityExpression.decEq

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

Equations

• One or more equations did not get rendered due to their size.
• Rubinstein2014.instDecidableEqPriorityExpression.decEq (Rubinstein2014.PriorityExpression.modal a) (Rubinstein2014.PriorityExpression.modal b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Rubinstein2014.instDecidableEqPriorityExpression.decEq (Rubinstein2014.PriorityExpression.modal name) (Rubinstein2014.PriorityExpression.evaluativeComp name_1) = isFalse ⋯
• Rubinstein2014.instDecidableEqPriorityExpression.decEq (Rubinstein2014.PriorityExpression.evaluativeComp name) (Rubinstein2014.PriorityExpression.modal name_1) = isFalse ⋯

@[implicit_reducible]

instance Rubinstein2014.instReprPriorityExpression : Repr PriorityExpression

Equations

• Rubinstein2014.instReprPriorityExpression = { reprPrec := Rubinstein2014.instReprPriorityExpression.repr }

def Rubinstein2014.instReprPriorityExpression.repr : PriorityExpression → ℕ → Std.Format

Equations

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

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

@[implicit_reducible]

instance Rubinstein2014.instReprComparativeClassMember : Repr ComparativeClassMember

Equations

• Rubinstein2014.instReprComparativeClassMember = { reprPrec := Rubinstein2014.instReprComparativeClassMember.repr }

def Rubinstein2014.instReprComparativeClassMember.repr : ComparativeClassMember → ℕ → Std.Format

Equations

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

def Rubinstein2014.shouldMember : ComparativeClassMember

Equations

• Rubinstein2014.shouldMember = { expression := Rubinstein2014.PriorityExpression.modal "should", passesTest1 := true, passesTest2 := true, negRaises := true, priorityOnly := false }

def Rubinstein2014.oughtMember : ComparativeClassMember

Equations

• Rubinstein2014.oughtMember = { expression := Rubinstein2014.PriorityExpression.modal "ought", passesTest1 := true, passesTest2 := true, negRaises := true, priorityOnly := false }

def 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

• Rubinstein2014.goodMember = { expression := Rubinstein2014.PriorityExpression.evaluativeComp "good", passesTest1 := true, passesTest2 := true, negRaises := true, priorityOnly := true }

def Rubinstein2014.betterMember : ComparativeClassMember

Equations

• Rubinstein2014.betterMember = { expression := Rubinstein2014.PriorityExpression.evaluativeComp "better", passesTest1 := true, passesTest2 := true, negRaises := true, priorityOnly := true }

def Rubinstein2014.preferableMember : ComparativeClassMember

Equations

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

def Rubinstein2014.worthwhileMember : ComparativeClassMember

Equations

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

def Rubinstein2014.mustMember : ComparativeClassMember

Equations

• Rubinstein2014.mustMember = { expression := Rubinstein2014.PriorityExpression.modal "must", passesTest1 := false, passesTest2 := false, negRaises := false, priorityOnly := false }

def Rubinstein2014.haveToMember : ComparativeClassMember

Equations

• Rubinstein2014.haveToMember = { expression := Rubinstein2014.PriorityExpression.modal "have to", passesTest1 := false, passesTest2 := false, negRaises := false, priorityOnly := false }

def 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

• Rubinstein2014.needMember = { expression := Rubinstein2014.PriorityExpression.modal "need", passesTest1 := false, passesTest2 := false, negRaises := false, priorityOnly := false }

def Rubinstein2014.comparativeClass : List ComparativeClassMember

Equations

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

def Rubinstein2014.strongNecessityModals : List ComparativeClassMember

Equations

• Rubinstein2014.strongNecessityModals = [Rubinstein2014.mustMember, Rubinstein2014.haveToMember, Rubinstein2014.needMember]

theorem 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 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 Rubinstein2014.strong_fails_tests : (strongNecessityModals.all fun (m : ComparativeClassMember) => !m.passesTest1 && !m.passesTest2) = true

No strong necessity modal passes the scalar tests.

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

No strong necessity modal supports neg-raising.

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

@[implicit_reducible]

instance Rubinstein2014.instReprNegRaisingClassification : Repr NegRaisingClassification

Equations

• Rubinstein2014.instReprNegRaisingClassification = { reprPrec := Rubinstein2014.instReprNegRaisingClassification.repr }

def Rubinstein2014.instReprNegRaisingClassification.repr : NegRaisingClassification → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Rubinstein2014.instBEqNegRaisingClassification : BEq NegRaisingClassification

Equations

• Rubinstein2014.instBEqNegRaisingClassification = { beq := Rubinstein2014.instBEqNegRaisingClassification.beq }

def Rubinstein2014.instBEqNegRaisingClassification.beq : NegRaisingClassification → NegRaisingClassification → Bool

Equations

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

def Rubinstein2014.rubinsteinNRClassification : List NegRaisingClassification

Equations

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

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

@[implicit_reducible]

instance Rubinstein2014.instDecidablePredWorldReportDomestic : DecidablePred Rubinstein2014.reportDomestic✝

Equations

• Rubinstein2014.instDecidablePredWorldReportDomestic w = id inferInstance

@[implicit_reducible]

instance Rubinstein2014.instDecidablePredWorldReportInternational : DecidablePred Rubinstein2014.reportInternational✝

Equations

• Rubinstein2014.instDecidablePredWorldReportInternational w = id inferInstance

@[implicit_reducible]

instance Rubinstein2014.instDecidablePredWorldReportAll : DecidablePred Rubinstein2014.reportAll✝

Equations

• Rubinstein2014.instDecidablePredWorldReportAll w = id inferInstance

theorem Rubinstein2014.tax_should_holds : weakNecessityR Rubinstein2014.taxScenarioA✝ Rubinstein2014.reportAll✝ 0

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

The single negotiable ideal reportInternational holds at (0 : World) (which is in favored worlds and satisfies all of reportInternational), so any "best" favored world must also satisfy it. The only favored world satisfying both is (0 : World), so reportAll holds at all best favored worlds.

theorem Rubinstein2014.tax_must_fails : ¬strongNecessityR Rubinstein2014.taxScenarioA✝ Rubinstein2014.reportAll✝ 0

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

(1 : World) is favored (satisfies reportDomestic) but does not satisfy reportInternational, so reportAll fails at (1 : World).

theorem Rubinstein2014.tax_must_holds_after_promotion : strongNecessityR Rubinstein2014.taxScenarioB✝ Rubinstein2014.reportAll✝ 0

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

With both reportDomestic and reportInternational non-negotiable, favored worlds must satisfy both, so reportAll holds trivially.

theorem Rubinstein2014.should_to_haveto_shift : ¬strongNecessityR Rubinstein2014.taxScenarioA✝ Rubinstein2014.reportAll✝ 0 ∧ strongNecessityR Rubinstein2014.taxScenarioB✝ Rubinstein2014.reportAll✝ 0

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

@[implicit_reducible]

instance Rubinstein2014.instDecidableEqWeakNecessityStrategy : DecidableEq WeakNecessityStrategy

Equations

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

@[implicit_reducible]

instance Rubinstein2014.instReprWeakNecessityStrategy : Repr WeakNecessityStrategy

Equations

• Rubinstein2014.instReprWeakNecessityStrategy = { reprPrec := Rubinstein2014.instReprWeakNecessityStrategy.repr }

def Rubinstein2014.instReprWeakNecessityStrategy.repr : WeakNecessityStrategy → ℕ → Std.Format

Equations

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

structure Rubinstein2014.WeakNecessityProfile : Type

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

def Rubinstein2014.instReprWeakNecessityProfile.repr : WeakNecessityProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Rubinstein2014.instReprWeakNecessityProfile : Repr WeakNecessityProfile

Equations

• Rubinstein2014.instReprWeakNecessityProfile = { reprPrec := Rubinstein2014.instReprWeakNecessityProfile.repr }

def Rubinstein2014.englishWN : WeakNecessityProfile

Equations

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

def Rubinstein2014.spanishWN : WeakNecessityProfile

Equations

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

def Rubinstein2014.hebrewWN : WeakNecessityProfile

Equations

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

theorem Rubinstein2014.hebrew_no_standard_wn : hebrewWN.hasLexicalWN = false ∧ hebrewWN.hasCompositionalWN = false

Hebrew lacks both standard routes to weak necessity.

theorem 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 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 Rubinstein2014.ComparisonCapability : Type

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

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

def Rubinstein2014.instReprComparisonCapability.repr : ComparisonCapability → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Rubinstein2014.instReprComparisonCapability : Repr ComparisonCapability

Equations

• Rubinstein2014.instReprComparisonCapability = { reprPrec := Rubinstein2014.instReprComparisonCapability.repr }

def Rubinstein2014.betterCapability : ComparisonCapability

Equations

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

def Rubinstein2014.goodCapability : ComparisonCapability

Equations

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

def Rubinstein2014.oughtCapability : ComparisonCapability

Equations

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

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

better supports pairwise comparison; ought and good do not.

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

The English fragment classifies ought as weak necessity.

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

The English fragment classifies must as strong necessity.

theorem Rubinstein2014.fragment_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 — confirming it is outside the evaluative comparative natural class.

theorem Rubinstein2014.fragment_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 — confirming the asymmetry: comparative class members have strictly weaker force.

theorem Rubinstein2014.fragment_need_strong : (Fragments.English.Auxiliaries.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 Rubinstein2014.fragment_need_not_weak : (Fragments.English.Auxiliaries.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).