Rubinstein (2014): On Necessity and Comparison

This file formalizes [Rub14]'s account of weak necessity as comparison. Following [Slo70], the priorities of [Kra81b]'s ordering source are split by negotiability ((48)–(49)): the priorities every participant is committed to are promoted to the modal base and, with the circumstances, delimit the favored worlds through [Fra96]'s compatibility-restricted union ((39)–(40)), while the negotiable priorities an opinionated assessor promotes remain an ordering source. Strong necessity is simple necessity over the favored worlds (41), weak necessity is human necessity over them under the negotiable ordering (42), and the ordering source of a weak necessity presupposes negotiability (50). The tax-report dialogue is the shift from should to have to as an ideal stops being negotiable ((46), (51)), and neg-raising follows from the choice between a negotiable ideal and its negation (§3.4.2). Weak necessity modals form a natural class with the evaluative comparatives good, better, preferable and worthwhile, diagnosed by the strength tests of §2.1 and by neg-raising after [Hor78], and Hebrew reaches weak necessity through the comparatives alone.

Main definitions

• Backgrounds, extensions, favoredWorlds: the circumstances, the promoted priorities and the negotiable ordering source; the maximal consistent sets of promoted priorities; and Frank's union over them.
• strongNecessity, weakNecessity: (41) and (42).
• Negotiable: (49), a list of ideals some participant is not committed to.

Main results

• favoredWorlds_eq_bestWorlds: Frank's compatibility-restricted union is Kratzer's best worlds under the promoted priorities, a best world being one whose verified priorities form a maximal consistent set (verified_mem_extensions, mem_bestWorlds_of_extension), so the two necessities are [vFI08]'s strong and weak necessity with the split ordering source (strongNecessity_iff, weakNecessity_iff); the analyses differ only in the negotiability presupposition.
• tax_shift: the negotiable ideal makes should true and have to false, and its endorsement leaves it non-negotiable and makes have to true.
• weakNecessity_ideal, weakNecessity_neg_of_not: a choice of ideal is a choice of weak necessities, from which the neg-raising inference for the ideal follows.
• negRaising_iff_comparative, carix_negRaises, strength_tests: over the paper's English, Hebrew and Spanish rows, neg-raising and the strength tests pick out the weak necessities, with carix the paper's apparent exception.

Implementation notes

• Commitment (48) is data, a finite set of ideals per participant, and an ideal list is negotiable when some participant is not committed to one of its members. The presupposition (50) is stated through the negotiability conjuncts of tax_shift rather than as a partial operator. Backgrounds are relative to worlds, not to the paper's events.
• The neg-raising rows of [Hor78] carry Horn's page numbers as their source labels. Narrog's survey (Table 1) and the tentative possibility semantics for preferable are not formalized.

References

• [Rub14]
• [Kra81b]
• [Fra96]
• [Slo70]
• [Hor78]
• [vFI08]

Favored worlds ((39)–(40))

structure Rubinstein2014.Backgrounds (W : Type u_2) : Type u_2

Modal backgrounds with the ordering source split by negotiability.

• circumstances : Modality.Background W

  The circumstances, the modal base proper.

• nonNegotiable : Modality.Background W

  The non-negotiable priorities, promoted to the modal base.

• negotiable : Modality.Background W

  The negotiable priorities, which remain an ordering source.

def Rubinstein2014.ConsistentWith {W : Type u_1} (b : Backgrounds W) (w : W) (X : Set (W → Prop)) : Prop

A set of priorities is consistent with the circumstances at w when some accessible world verifies all of them.

Equations

• Rubinstein2014.ConsistentWith b w X = ∃ v ∈ b.circumstances.accessibleWorlds w, ∀ q ∈ X, q v

def Rubinstein2014.extensions {W : Type u_1} (b : Backgrounds W) (w : W) : Set (Set (W → Prop))

The maximal sets of promoted priorities consistent with the circumstances (39), the sets [Fra96]'s compatibility-restricted union adds to the circumstances.

Equations

• Rubinstein2014.extensions b w = {X : Set (W → Prop) | Maximal (fun (Y : Set (W → Prop)) => Y ⊆ {q : W → Prop | q ∈ b.nonNegotiable w} ∧ Rubinstein2014.ConsistentWith b w Y) X}

def Rubinstein2014.favoredWorlds {W : Type u_1} (b : Backgrounds W) (w : W) : Set W

The favored worlds (40), the accessible worlds verifying some maximal consistent set of promoted priorities.

Equations

• Rubinstein2014.favoredWorlds b w = ⋃ X ∈ Rubinstein2014.extensions b w, {u : W | u ∈ b.circumstances.accessibleWorlds w ∧ ∀ q ∈ X, q u}

def Rubinstein2014.verified {W : Type u_1} (b : Backgrounds W) (w u : W) : Set (W → Prop)

The promoted priorities a world verifies.

Equations

• Rubinstein2014.verified b w u = Preorder.satisfied (fun (v : W) (q : W → Prop) => q v) {q : W → Prop | q ∈ b.nonNegotiable w} u

theorem Rubinstein2014.atLeastAsGoodAs_iff_verified_subset {W : Type u_1} {b : Backgrounds W} {w u v : W} : v ≤ u ↔ verified b w u ⊆ verified b w v

A world is at least as good as another under the promoted priorities when it verifies every priority the other verifies.

theorem Rubinstein2014.verified_mem_extensions {W : Type u_1} {b : Backgrounds W} {w u : W} (hu : u ∈ Modality.bestWorlds b.circumstances b.nonNegotiable w) : verified b w u ∈ extensions b w

The priorities a best world verifies form a maximal consistent extension.

theorem Rubinstein2014.mem_bestWorlds_of_extension {W : Type u_1} {b : Backgrounds W} {w : W} {X : Set (W → Prop)} {u : W} (hX : X ∈ extensions b w) (hu : u ∈ b.circumstances.accessibleWorlds w) (huX : ∀ q ∈ X, q u) : u ∈ Modality.bestWorlds b.circumstances b.nonNegotiable w

A world verifying a maximal consistent extension is best.

theorem Rubinstein2014.favoredWorlds_eq_bestWorlds {W : Type u_1} (b : Backgrounds W) (w : W) : favoredWorlds b w = Modality.bestWorlds b.circumstances b.nonNegotiable w

Frank's union is Kratzer's best worlds under the promoted priorities.

The two necessities ((41)–(42))

def Rubinstein2014.strongNecessity {W : Type u_1} (b : Backgrounds W) (p : W → Prop) (w : W) : Prop

Strong necessity (41) is simple necessity over the favored worlds.

Equations

• Rubinstein2014.strongNecessity b p w = ∀ v ∈ Rubinstein2014.favoredWorlds b w, p v

def Rubinstein2014.weakNecessity {W : Type u_1} (b : Backgrounds W) (p : W → Prop) (w : W) : Prop

Weak necessity (42) is human necessity over the favored worlds under the negotiable ordering source.

Equations

• Rubinstein2014.weakNecessity b p w = ∀ v ∈ (Modality.premisePreorder (b.negotiable w)).minimals (Rubinstein2014.favoredWorlds b w), p v

theorem Rubinstein2014.strongNecessity_iff {W : Type u_1} {b : Backgrounds W} {p : W → Prop} {w : W} : strongNecessity b p w ↔ Modality.Directive.strongNecessity b.circumstances b.nonNegotiable p w

Strong necessity is [vFI08]'s, with the promoted priorities as the ordering source.

theorem Rubinstein2014.weakNecessity_iff {W : Type u_1} {b : Backgrounds W} {p : W → Prop} {w : W} : weakNecessity b p w ↔ Modality.Directive.weakNecessity b.circumstances b.nonNegotiable b.negotiable p w

Weak necessity is [vFI08]'s, with the promoted priorities as the primary and the negotiable ones as the secondary ordering source: the truth conditions of the two analyses coincide, and only the presupposition (50) separates them.

theorem Rubinstein2014.strong_entails_weak {W : Type u_1} {b : Backgrounds W} {p : W → Prop} {w : W} (h : strongNecessity b p w) : weakNecessity b p w

Strong necessity entails weak necessity.

theorem Rubinstein2014.weak_not_entails_strong : ¬∀ (W : Type) (b : Backgrounds W) (p : W → Prop) (w : W), weakNecessity b p w → strongNecessity b p w

Weak necessity does not entail strong necessity.

theorem Rubinstein2014.weakNecessity_iff_strongNecessity {W : Type u_1} {b : Backgrounds W} {p : W → Prop} {w : W} (hg : b.negotiable w = ∅) : weakNecessity b p w ↔ strongNecessity b p w

Without negotiable priorities the two necessities coincide.

Negotiability ((48)–(50))

def Rubinstein2014.Negotiable {ι : Type u_2} {κ : Type u_3} [DecidableEq κ] (commitment : ι → Finset κ) (ideals : List κ) : Prop

A list of ideals is negotiable (49) when some participant is not committed to one of them, commitment (48) being the ideals a participant is prepared to argue for.

Equations

• Rubinstein2014.Negotiable commitment ideals = ∃ (a : ι), ∃ i ∈ ideals, i ∉ commitment a

@[instance_reducible]

instance Rubinstein2014.instDecidableNegotiableOfFintype {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq κ] (commitment : ι → Finset κ) (ideals : List κ) : Decidable (Negotiable commitment ideals)

Equations

• Rubinstein2014.instDecidableNegotiableOfFintype commitment ideals = { decide := decide (∃ a ∈ Finset.univ, (fun (a : ι) => ∃ i ∈ ideals, i ∉ commitment a) a), reflects_decide := ⋯ }

theorem Rubinstein2014.weakNecessity_ideal {W : Type u_1} {b : Backgrounds W} {w : W} {γ : W → Prop} (hγ : b.negotiable w = {γ}) (hlive : ∃ v ∈ favoredWorlds b w, γ v) : weakNecessity b γ w ∧ ¬weakNecessity b (fun (v : W) => ¬γ v) w

A choice of ideal is a choice of weak necessities (§3.4.2): with γ the negotiable ideal and γ live among the favored worlds, should γ holds and should ¬γ fails.

theorem Rubinstein2014.weakNecessity_neg_of_not {W : Type u_1} {b : Backgrounds W} {w : W} {γ : W → Prop} (hchoice : b.negotiable w = {γ} ∨ b.negotiable w = {fun (v : W) => ¬γ v}) (hγ : ∃ v ∈ favoredWorlds b w, γ v) (hnγ : ∃ v ∈ favoredWorlds b w, ¬γ v) (h : ¬weakNecessity b γ w) : weakNecessity b (fun (v : W) => ¬γ v) w

The neg-raising inference for the ideal: when the negotiable ideal is γ or its negation and both are live, not should γ yields should ¬γ.

The tax report ((45)–(46), (51))

inductive Rubinstein2014.Ideal : Type

The clauses of the tax law, reporting domestic and reporting international revenue.

• domestic : Ideal

  Report domestic revenue.

• international : Ideal

  Report international revenue.

@[instance_reducible]

instance Rubinstein2014.instDecidableEqIdeal : DecidableEq Ideal

Equations

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

@[instance_reducible]

instance Rubinstein2014.instReprIdeal : Repr Ideal

Equations

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

def Rubinstein2014.instReprIdeal.repr : Ideal → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev Rubinstein2014.Revenue : Type

A world of the scenario records whether domestic and whether international revenue is reported.

Equations

• Rubinstein2014.Revenue = (Bool × Bool)

def Rubinstein2014.Ideal.holds : Ideal → Revenue → Prop

The content of a clause.

Equations

• Rubinstein2014.Ideal.domestic.holds x✝ = (x✝.1 = true)
• Rubinstein2014.Ideal.international.holds x✝ = (x✝.2 = true)

inductive Rubinstein2014.Participant : Type

The participants of the dialogue (46).

• accountant : Participant

  The accountant, who proposes reporting all revenue.

• manager : Participant

  The manager, who endorses it.

@[instance_reducible]

instance Rubinstein2014.instDecidableEqParticipant : DecidableEq Participant

Equations

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

@[instance_reducible]

instance Rubinstein2014.instReprParticipant : Repr Participant

Equations

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

def Rubinstein2014.instReprParticipant.repr : Participant → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Rubinstein2014.instFintypeParticipant : Fintype Participant

Equations

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

def Rubinstein2014.ofIdeals (h g : List Ideal) : Backgrounds Revenue

Backgrounds with no circumstances, the promoted clauses h and the negotiable clauses g.

Equations

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

def Rubinstein2014.commitmentBefore : Participant → Finset Ideal

Before the endorsement the manager is committed to the domestic clause only (51a).

Equations

• Rubinstein2014.commitmentBefore Rubinstein2014.Participant.accountant = {Rubinstein2014.Ideal.domestic, Rubinstein2014.Ideal.international}
• Rubinstein2014.commitmentBefore Rubinstein2014.Participant.manager = {Rubinstein2014.Ideal.domestic}

def Rubinstein2014.commitmentAfter : Participant → Finset Ideal

After the endorsement both participants are committed to both clauses (51b).

Equations

• Rubinstein2014.commitmentAfter x✝ = {Rubinstein2014.Ideal.domestic, Rubinstein2014.Ideal.international}

def Rubinstein2014.reportAll (v : Revenue) : Prop

Reporting all revenue.

Equations

• Rubinstein2014.reportAll v = (v.1 = true ∧ v.2 = true)

theorem Rubinstein2014.tax_shift (w : Revenue) : (Negotiable commitmentBefore [Ideal.international] ∧ weakNecessity (ofIdeals [Ideal.domestic] [Ideal.international]) reportAll w ∧ ¬strongNecessity (ofIdeals [Ideal.domestic] [Ideal.international]) reportAll w) ∧ ¬Negotiable commitmentAfter [Ideal.international] ∧ strongNecessity (ofIdeals [Ideal.domestic, Ideal.international] []) reportAll w

In (46) and (51), before the endorsement the international clause is negotiable, we should report all our revenue holds and we have to does not; after it the clause is no longer negotiable and we have to holds.

The comparative class in the data (§2)

def Rubinstein2014.WeakInFragment (modal : String) : Prop

The English fragment assigns the modal verb weak necessity.

Equations

• Rubinstein2014.WeakInFragment modal = ∃ a ∈ English.Auxiliaries.modals, a.form = modal ∧ Modality.ModalForce.weakNecessity ∈ a.toModalItem.forces

@[instance_reducible]

instance Rubinstein2014.instDecidablePredStringWeakInFragment : DecidablePred WeakInFragment

Equations

• Rubinstein2014.instDecidablePredStringWeakInFragment x✝ = Rubinstein2014.instDecidablePredStringWeakInFragment._aux_1 x✝

def Rubinstein2014.InComparativeClass (e : Datum) : Prop

An item belongs to the comparative class when it is an evaluative comparative or a modal verb the fragment marks as weak necessity.

Equations

• Rubinstein2014.InComparativeClass e = (e.feature? "category" = some "evaluativeComparative" ∨ ∃ m ∈ e.feature? "modal", Rubinstein2014.WeakInFragment m)

@[instance_reducible]

instance Rubinstein2014.instDecidablePredDatumInComparativeClass : DecidablePred InComparativeClass

Equations

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

def Rubinstein2014.negRaisingRows : List Datum

The neg-raising stimuli.

Equations

• Rubinstein2014.negRaisingRows = List.filter (fun (e : Datum) => decide (e.feature? "diagnostic" = some "negRaising")) Rubinstein2014.Examples.all

theorem Rubinstein2014.negRaising_iff_comparative (e : Datum) : e ∈ negRaisingRows → e.feature? "hybrid" ≠ some "true" → (List.lookup "lowerNeg" e.readings = some Judgment.acceptable ↔ InComparativeClass e)

In (30)–(33), the lower-negation reading of a negated attitude is available exactly for the comparative class, the weak necessity verbs and the evaluative comparatives, and not for the strong modals, the hybrid carix aside.

theorem Rubinstein2014.carix_negRaises : ∃ e ∈ negRaisingRows, e.feature? "modal" = some "carix" ∧ List.lookup "lowerNeg" e.readings = some Judgment.acceptable ∧ ¬InComparativeClass e

The hybrid carix 'need' (57) neg-raises although it is no comparative, the paper's apparent exception to the rule.

inductive Rubinstein2014.Strategy : Type

The routes to weak necessity are a dedicated item, a strong modal with weakening morphology, and evaluative comparative language.

• lexical : Strategy

  A dedicated weak necessity modal, English ought.

• compositional : Strategy

  A strong necessity modal with counterfactual morphology, Spanish debería.

• evaluativeComparative : Strategy

  An evaluative comparative, Hebrew yoter tov.

@[instance_reducible]

instance Rubinstein2014.instDecidableEqStrategy : DecidableEq Strategy

Equations

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

@[instance_reducible]

instance Rubinstein2014.instReprStrategy : Repr Strategy

Equations

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

def Rubinstein2014.instReprStrategy.repr : Strategy → ℕ → Std.Format

Equations

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

def Rubinstein2014.strategy? (e : Datum) : Option Strategy

The strategy a row exemplifies.

Equations

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

theorem Rubinstein2014.strength_tests (e : Datum) : e ∈ Examples.all → e.feature? "diagnostic" ∈ [some "test1", some "test2"] → (e.judgment = Judgment.acceptable ↔ (strategy? e).isSome = true)

The strength tests of (8), (16), (19) and (21), denying strong necessity after the expression or opposing it to strong necessity with an exclusive, are felicitous exactly for the items that reach weak necessity by some strategy.

theorem Rubinstein2014.hebrew_comparative_only (e : Datum) : e ∈ Examples.all → e.language = "hebr1245" → ∀ s ∈ strategy? e, s = Strategy.evaluativeComparative

Hebrew has neither a lexical nor a compositional weak necessity (§2.1), its route being the evaluative comparative.