Agha and Jeretič (2022): Weak Necessity Modals as Homogeneous Pluralities of Worlds

Weak necessity modals take obligatory apparent wide scope over negation: you shouldn't go cannot be continued by but you are allowed to go, where you don't have to go can. Agha and Jeretič propose that should is to must what the is to all: strong necessity quantifies universally over the best worlds, while weak necessity predicates the prejacent of their plurality, which is neither true nor false when some best worlds satisfy it and some do not. Weak necessity is derived from strong necessity by an operator picking out the unique minimal set of a quantifier, which possibility lacks.

Main results

• should_eq_zero_iff, should_not: the gap arises exactly in mixed domains, and negation is symmetric and hence scopeless.
• not_exists_of_should_not, must_false_of_indet: a true negated should contradicts the existential continuation, where a negated must does not.
• must_eq_metaAssert_should, necessarily_removes_gap: necessarily removes the gap as all does.
• exception_tolerance, two_doors: Križ's usability gives the exception tolerance of the perfect-grade scenario and the indeterminacy of the two-doors scenario.
• x_must, possibility_witnesses: the derivation of weak necessity applies to necessity only.
• should_matches_grid, domainRestriction_fails_exactly_gap: over the paper's grid of judgments the plural semantics fits every cell, and domain restriction fails exactly the gaps.

Implementation notes

should D p is Križ's plural predication with the best worlds D w as atoms. The grid reads each example row as a cell (Cell.ofDatum): its polarity, its scenario, and the value judged, the classical value the polarity fixes where all or no best worlds satisfy the prejacent, and the gap or the recorded classical value in the mixed scenario. The proportional and degree-based rivals, and the conditionals, generics and habituals of the closing section, are not formalized.

References

• [AJ22]
• [Kri16]
• [Kra81b]
• [vFI08]
• [VKH20]
• [BC81]
• [Sch04b]

Weak necessity as plural predication over worlds

def AghaJeretic2022.should {W : Type u_1} (D : W → Finset W) (p : W → Prop) [DecidablePred p] : W → SignType

Weak necessity should D p predicates the prejacent of the plurality of best worlds D w.

Equations

• AghaJeretic2022.should D p w = SignType.supervaluation (D w) p

def AghaJeretic2022.must {W : Type u_1} (D : W → Finset W) (p : W → Prop) [DecidablePred p] : W → SignType

Strong necessity must D p holds when the prejacent holds in every best world.

Equations

• AghaJeretic2022.must D p w = SignType.ofProp (∀ w' ∈ D w, p w')

theorem AghaJeretic2022.should_eq_one_iff {W : Type u_1} (D : W → Finset W) (p : W → Prop) [DecidablePred p] (w : W) : should D p w = 1 ↔ ∀ w' ∈ D w, p w'

theorem AghaJeretic2022.should_eq_neg_one_iff {W : Type u_1} (D : W → Finset W) (p : W → Prop) [DecidablePred p] (w : W) : should D p w = -1 ↔ (D w).Nonempty ∧ ∀ w' ∈ D w, ¬p w'

theorem AghaJeretic2022.should_eq_zero_iff {W : Type u_1} (D : W → Finset W) (p : W → Prop) [DecidablePred p] (w : W) : should D p w = 0 ↔ (∃ w' ∈ D w, p w') ∧ ∃ w' ∈ D w, ¬p w'

The sentence has a gap when some best worlds satisfy the prejacent and some do not.

theorem AghaJeretic2022.should_not {W : Type u_1} (D : W → Finset W) (p : W → Prop) [DecidablePred p] (w : W) (hne : (D w).Nonempty) : should D (fun (w' : W) => ¬p w') w = -should D p w

Over a nonempty domain negating the prejacent negates the modal sentence, so the gap is symmetric and negation is scopeless.

theorem AghaJeretic2022.not_exists_of_should_not {W : Type u_1} (D : W → Finset W) (p : W → Prop) [DecidablePred p] (w : W) (h : should D (fun (w' : W) => ¬p w') w = 1) : ¬∃ w' ∈ D w, p w'

A true negated weak necessity leaves no best world for the existential continuation.

theorem AghaJeretic2022.must_false_of_indet {W : Type u_1} (D : W → Finset W) (p : W → Prop) [DecidablePred p] (w : W) (h : should D p w = 0) : must D p w = -1 ∧ ∃ w' ∈ D w, p w'

In a mixed domain a negated strong necessity is true and the existential continuation holds with it.

Homogeneity removal

theorem AghaJeretic2022.must_eq_metaAssert_should {W : Type u_1} (D : W → Finset W) (p : W → Prop) [DecidablePred p] : must D p = (fun (v : SignType) => SignType.ofProp (v = 1)) ∘ should D p

Must is should with its gap removed, the universal quantifier being the meta-assertion of the plural predication, as all is of the.

theorem AghaJeretic2022.isBivalent_must {W : Type u_1} (D : W → Finset W) (p : W → Prop) [DecidablePred p] : Trivalent.IsBivalent (must D p)

theorem AghaJeretic2022.necessarily_removes_gap {W : Type u_1} (D : W → Finset W) (p : W → Prop) [DecidablePred p] (w : W) (h : should D p w = 0) : should D (fun (w' : W) => ¬p w') w ≠ 1 ∧ -SignType.ofProp (should D p w = 1) = 1 ∧ ∃ w' ∈ D w, p w'

In a mixed domain the negated bare should is not true, while the negated necessarily should is true and compatible with the existential continuation.

Borderline cases and exception tolerance

inductive AghaJeretic2022.Door : Type

The two doors to the living room.

• left : Door
• right : Door

@[instance_reducible]

instance AghaJeretic2022.instDecidableEqDoor : DecidableEq Door

Equations

• AghaJeretic2022.instDecidableEqDoor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AghaJeretic2022.instFintypeDoor : Fintype Door

Equations

• AghaJeretic2022.instFintypeDoor = { elems := { val := ↑AghaJeretic2022.Door.enumList, nodup := AghaJeretic2022.Door.enumList_nodup }, complete := AghaJeretic2022.instFintypeDoor._proof_1 }

def AghaJeretic2022.doors : Door → Finset Door

Both doors are equally good, so both worlds are best.

Equations

• AghaJeretic2022.doors x✝ = {AghaJeretic2022.Door.left, AghaJeretic2022.Door.right}

@[reducible, inline]

abbrev AghaJeretic2022.strict : Setoid Door

The issue that separates every world from every other.

Equations

• AghaJeretic2022.strict = ⊥

theorem AghaJeretic2022.two_doors (w : Door) : should doors (fun (x : Door) => x = Door.right) w = 0 ∧ ¬Homogeneity.usable strict (should doors fun (x : Door) => x = Door.right) w ∧ must doors (fun (x : Door) => x = Door.right) w = -1

Taking the right door should be taken is neither true nor false — neither assertible nor deniable — while that it must be taken is false.

inductive AghaJeretic2022.Grade : Type

In a world of the perfect-grade scenario the rules require every exercise or only most, and the addressee does every exercise or only most.

• strictAll : Grade
• strictMost : Grade
• lenientAll : Grade
• lenientMost : Grade

@[instance_reducible]

instance AghaJeretic2022.instDecidableEqGrade : DecidableEq Grade

Equations

• AghaJeretic2022.instDecidableEqGrade x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AghaJeretic2022.instFintypeGrade : Fintype Grade

Equations

• AghaJeretic2022.instFintypeGrade = { elems := { val := ↑AghaJeretic2022.Grade.enumList, nodup := AghaJeretic2022.Grade.enumList_nodup }, complete := AghaJeretic2022.instFintypeGrade._proof_1 }

def AghaJeretic2022.grade : Grade → Finset Grade

The perfect-grade worlds under a world's rules.

Equations

• AghaJeretic2022.grade AghaJeretic2022.Grade.strictAll = {AghaJeretic2022.Grade.strictAll}
• AghaJeretic2022.grade AghaJeretic2022.Grade.strictMost = {AghaJeretic2022.Grade.strictAll}
• AghaJeretic2022.grade AghaJeretic2022.Grade.lenientAll = {AghaJeretic2022.Grade.lenientAll, AghaJeretic2022.Grade.lenientMost}
• AghaJeretic2022.grade AghaJeretic2022.Grade.lenientMost = {AghaJeretic2022.Grade.lenientAll, AghaJeretic2022.Grade.lenientMost}

def AghaJeretic2022.everyExercise (w : Grade) : Prop

Doing every exercise.

Equations

• AghaJeretic2022.everyExercise w = (w = AghaJeretic2022.Grade.strictAll ∨ w = AghaJeretic2022.Grade.lenientAll)

@[instance_reducible]

instance AghaJeretic2022.instDecidablePredGradeEveryExercise : DecidablePred everyExercise

Equations

• AghaJeretic2022.instDecidablePredGradeEveryExercise x✝ = { decide := decide (x✝ = AghaJeretic2022.Grade.strictAll) || decide (x✝ = AghaJeretic2022.Grade.lenientAll), reflects_decide := ⋯ }

@[reducible, inline]

abbrev AghaJeretic2022.wayQUD : Setoid Grade

What is a way to get a perfect grade? — every world answers alike.

Equations

• AghaJeretic2022.wayQUD = ⊤

@[reducible, inline]

abbrev AghaJeretic2022.minimalQUD : Setoid Grade

What are the minimal requirements? — worlds are grouped by their rules.

Equations

• AghaJeretic2022.minimalQUD = Setoid.ker AghaJeretic2022.grade

theorem AghaJeretic2022.exception_tolerance : Homogeneity.usable wayQUD (should grade everyExercise) Grade.lenientAll ∧ ¬Homogeneity.usable minimalQUD (should grade everyExercise) Grade.lenientAll ∧ ¬Homogeneity.usable wayQUD (must grade everyExercise) Grade.lenientAll ∧ ¬Homogeneity.usable minimalQUD (must grade everyExercise) Grade.lenientAll

Where most exercises suffice, you should do every exercise is usable under the first question but not the second, and you have to do every exercise under neither.

Domain restriction

theorem AghaJeretic2022.domainRestriction_no_contradiction {W : Type u_1} {D' D : Finset W} (h : D' ⊂ D) : ∃ (q : W → Prop), (∀ w ∈ D', ¬q w) ∧ ∃ w ∈ D, q w

If weak necessity quantifies over a proper subset of the domain of allowed, the negated modal and the existential continuation are jointly satisfiable.

Deriving weak from strong necessity

The quantifiers are families of sets of worlds, and the operator deriving weak necessity picks out a minimal set in the family. For the universal quantifier (D ⊆ ·) that is mathlib's minimal_ge_iff; the existential quantifier needs the lemma below.

theorem AghaJeretic2022.minimal_inter_nonempty_iff {E : Type u_2} [DecidableEq E] {s X : Finset E} : Minimal (fun (X : Finset E) => (s ∩ X).Nonempty) X ↔ ∃ w ∈ s, X = {w}

The minimal sets in the existential quantifier over s are the singletons of its elements.

theorem AghaJeretic2022.exists_minimal_inter_nonempty {E : Type u_2} [DecidableEq E] {s : Finset E} (h : s.Nonempty) : ∃ (X : Finset E), Minimal (fun (X : Finset E) => (s ∩ X).Nonempty) X

The existential quantifier over a nonempty s has a minimal set.

theorem AghaJeretic2022.not_existsUnique_minimal_inter_nonempty {E : Type u_2} [DecidableEq E] {s : Finset E} (h : 1 < s.card) : ¬∃! X : Finset E, Minimal (fun (X : Finset E) => (s ∩ X).Nonempty) X

The existential quantifier over an s with two or more elements has no unique minimal set.

theorem AghaJeretic2022.x_must {W : Type u_1} (D : W → Finset W) (w : W) : (∃! X : Finset W, Minimal (fun (x : Finset W) => D w ⊆ x) X) ∧ ∀ (X : Finset W), Minimal (fun (x : Finset W) => D w ⊆ x) X ↔ X = D w

Strong necessity, as a quantifier over sets of worlds, has the domain as its unique minimal set, so picking that set out yields the plurality weak necessity denotes.

theorem AghaJeretic2022.possibility_witnesses {W : Type u_1} (D : W → Finset W) (w : W) [DecidableEq W] (h : 1 < (D w).card) : (∃ (X : Finset W), Minimal (fun (X : Finset W) => (D w ∩ X).Nonempty) X) ∧ ¬∃! X : Finset W, Minimal (fun (X : Finset W) => (D w ∩ X).Nonempty) X

Possibility over two or more best worlds has minimal sets but no unique one, so a marker that needs only some minimal set applies to it and one that needs the unique minimal set does not.

The data

inductive AghaJeretic2022.Scenario : Type

In the scenarios of the grid all, none, or some but not all of the best worlds satisfy the prejacent.

• all : Scenario
• none : Scenario
• gap : Scenario

@[instance_reducible]

instance AghaJeretic2022.instDecidableEqScenario : DecidableEq Scenario

Equations

• AghaJeretic2022.instDecidableEqScenario x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AghaJeretic2022.instReprScenario.repr : Scenario → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AghaJeretic2022.instReprScenario : Repr Scenario

Equations

• AghaJeretic2022.instReprScenario = { reprPrec := AghaJeretic2022.instReprScenario.repr }

structure AghaJeretic2022.Cell : Type

A cell of the grid records the polarity of a sentence, its scenario and the value judged.

• polarity : Polarity

  The polarity of the sentence.

• scenario : Scenario

  The scenario.

• observed : SignType

  The value judged.

@[instance_reducible]

instance AghaJeretic2022.instDecidableEqCell : DecidableEq Cell

Equations

• AghaJeretic2022.instDecidableEqCell = AghaJeretic2022.instDecidableEqCell.decEq

def AghaJeretic2022.instDecidableEqCell.decEq (x✝ x✝¹ : Cell) : Decidable (x✝ = x✝¹)

Equations

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

def AghaJeretic2022.Cell.ofDatum (e : Datum) : Option Cell

A row reads as a cell from its polarity and scenario. The value judged is the one the polarity fixes where all or no best worlds satisfy the prejacent, and in the mixed scenario the gap where the paper reports one and the recorded classical value otherwise.

Equations

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

def AghaJeretic2022.shouldGrid : List Cell

The polarity-by-scenario grid for should.

Equations

• AghaJeretic2022.shouldGrid = List.filterMap AghaJeretic2022.Cell.ofDatum (List.filter (fun (x : Datum) => x.feature? "modal" == some "should") AghaJeretic2022.Examples.all)

def AghaJeretic2022.scenarioDomain : Scenario → Finset Bool

A representative domain for each scenario, a world being the prejacent's truth value at it.

Equations

• AghaJeretic2022.scenarioDomain AghaJeretic2022.Scenario.all = {true}
• AghaJeretic2022.scenarioDomain AghaJeretic2022.Scenario.none = {false}
• AghaJeretic2022.scenarioDomain AghaJeretic2022.Scenario.gap = {true, false}

def AghaJeretic2022.shouldPredict (pol : Polarity) (s : Scenario) : SignType

The plural semantics' value at a cell predicates the negated prejacent at negative polarity.

Equations

• AghaJeretic2022.shouldPredict Polarity.positive s = AghaJeretic2022.should (fun (x : Bool) => AghaJeretic2022.scenarioDomain s) (fun (x : Bool) => x = true) true
• AghaJeretic2022.shouldPredict Polarity.negative s = AghaJeretic2022.should (fun (x : Bool) => AghaJeretic2022.scenarioDomain s) (fun (x : Bool) => x = false) true

def AghaJeretic2022.domainRestrictionPredict (pol : Polarity) (s : Scenario) : SignType

Domain restriction's value at a cell is universal quantification, negated by strong Kleene negation.

Equations

• AghaJeretic2022.domainRestrictionPredict Polarity.positive s = AghaJeretic2022.must (fun (x : Bool) => AghaJeretic2022.scenarioDomain s) (fun (x : Bool) => x = true) true
• AghaJeretic2022.domainRestrictionPredict Polarity.negative s = -AghaJeretic2022.must (fun (x : Bool) => AghaJeretic2022.scenarioDomain s) (fun (x : Bool) => x = true) true

theorem AghaJeretic2022.should_matches_grid (d : Cell) : d ∈ shouldGrid → shouldPredict d.polarity d.scenario = d.observed

The plural semantics reproduces every cell of the should grid.

theorem AghaJeretic2022.domainRestriction_fails_exactly_gap (d : Cell) : d ∈ shouldGrid → (domainRestrictionPredict d.polarity d.scenario = d.observed ↔ d.scenario ≠ Scenario.gap)

Domain restriction matches the classical cells and fails exactly the gap cells.

theorem AghaJeretic2022.weak_negated_contradicts (e : Datum) : e ∈ Examples.all → e.feature? "force" = some "weak" → (e.feature? "negation").isSome = true → e.feature? "remover" = none → e.feature? "continuation_felicity" = some "infelicitous"

A negated weak necessity modal, however the negation is placed, rejects the existential continuation.

theorem AghaJeretic2022.strong_extraclausal_compatible (e : Datum) : e ∈ Examples.all → e.feature? "force" = some "strong" → e.feature? "negation" = some "extra-clausal" → e.feature? "continuation_felicity" = some "felicitous"

A strong necessity modal under extra-clausal negation accepts it.

theorem AghaJeretic2022.necessarily_licenses_continuation (e : Datum) : e ∈ Examples.all → e.feature? "remover" = some "necessarily" → e.feature? "continuation_felicity" = some "felicitous"

Necessarily licenses the continuation wherever it is inserted.

theorem AghaJeretic2022.ne_only_necessity (e : Datum) : e ∈ Examples.all → (e.feature? "derivation" = some "NE" → e.feature? "base" = some "possibility" → e.judgment = Judgment.ungrammatical) ∧ (e.feature? "derivation" = some "CF" → e.judgment = Judgment.acceptable)

NE on a possibility base is ungrammatical; counterfactual marking is grammatical on either base.