Expectation states

This file defines Veltman's expectation patterns and expectation states, the updates with normally φ and presumably φ, and the necessity modals that Portner reads off such states.

An expectation pattern is a preorder on worlds, where w ≤ v means that w conforms to every rule that v conforms to. Refining a pattern with a proposition removes the pairs that rank a world outside the proposition below a world inside it, which is the meet of the pattern with the preorder that a single proposition induces, so the laws of refinement are those of a meet-semilattice. A pattern respects a proposition when refining with it changes nothing; Veltman calls a nonempty such proposition a default in the pattern, and a pattern is determined by the propositions it respects. An expectation state pairs a pattern with the agent's information. Asserting a fact eliminates worlds, normally φ refines the pattern in favour of φ without eliminating anything, and presumably φ tests whether φ holds in the optimal worlds, the minimal worlds of the information under the pattern. Assertion and promotion are additive in the sense of Semantics/Dynamic/Consequence.lean. Defaults are dynamic: a promoted expectation persists under further assertions and promotions, conflicting defaults leave the agent agnostic, and compatible ones reinforce each other.

Read at the level of discourse, assertion and promotion are the two updates of Portner's account of mood, on the context set and on the To-Do List. Informational necessity □_cs is truth throughout the information and preferential necessity □_≤ is truth at the optimal worlds, and a state accepts an assertion or a presumption exactly when the corresponding necessity holds. Local necessity, the force Portner and Rubinstein give the subjunctive, is good possibility in ordering semantics over the information ranked by the pattern; it is preferential necessity when the information has a most normal world.

Main definitions

• DynamicSemantics.ExpState.crit, DynamicSemantics.ExpState.refine: the pattern induced by one proposition, and the refinement of a pattern with a proposition.
• DynamicSemantics.ExpState.Respects: refining the pattern with the proposition changes nothing.
• DynamicSemantics.ExpState: a pattern together with the agent's information, with init, optimal, assert and promote.
• DynamicSemantics.ExpState.presumablyTest, DynamicSemantics.ExpState.mightTest: the tests.
• DynamicSemantics.ExpState.boxCs, DynamicSemantics.ExpState.boxLe, DynamicSemantics.ExpState.localNecessity: informational, preferential and local necessity.

Main results

• refine_empty, refine_univ, refine_idem, refine_mono: the laws of refinement.
• le_iff_forall_respects: a pattern ranks w below v exactly when every proposition it respects that holds at v holds at w.
• isAdditive_assert, isAdditive_promote: assertion and promotion are additive.
• le_assert_iff, isFixedPt_presumablyTest_iff: a state accepts an assertion or a presumption exactly when it is informationally or preferentially necessary.
• normally_creates_respect, persistence_assert, persistence_normally: a promotion creates an expectation that later updates preserve.
• normally_presumably_succeeds, boxLe_of_respects: normally φ; presumably φ passes.
• conflicting_defaults_iff_agree, compatible_defaults_optimal: conflicting defaults yield agnosticism, and compatible ones reinforce each other.
• promote_respects_idempotent, promote_comm: promotion is idempotent and commutative.
• localNecessity_iff_boxLe: with a most normal world, local necessity is preferential necessity.

Implementation notes

Veltman's states have coherent patterns, and his update with normally φ crashes when no normal world of the pattern is a φ-world. Here promotion refines unconditionally and patterns need not be coherent, so a conflicting rule shows up as the failure of its acceptability condition rather than as a crash. The crashing update is the rule update of the section 4 system in Studies/Veltman1996.lean, where the restricted rules and expectation frames of that section live.

The preference structures of Condoravdi and Lauer order propositions, one type level above the ordering of worlds here.

References

• F. Veltman, Defaults in Update Semantics (1996)
• P. Portner, The Semantics of Imperatives within a Theory of Clause Types (2004)
• P. Portner, Mood (2018)
• R. C. Stalnaker, Assertion (1978)
• A. Kratzer, The Notional Category of Modality (1981)
• D. F. Farkas, Assertion, belief and mood choice (2003)
• C. Condoravdi and S. Lauer, Imperatives: Meaning and Illocutionary Force (2012)
• [PR20]

Expectation patterns

@[reducible]

def DynamicSemantics.ExpState.crit {W : Type u_1} (φ : W → Prop) : Preorder W

The criterion pattern of φ ranks w below v when φ v implies φ w. It is defined directly rather than through Preorder.ofCriteria, so that refinement reduces definitionally to a conjunction.

Equations

• DynamicSemantics.ExpState.crit φ = Preorder.ofLE (fun (w v : W) => φ v → φ w) ⋯ ⋯

theorem DynamicSemantics.ExpState.crit_le {W : Type u_1} {φ : W → Prop} {w v : W} : w ≤ v ↔ φ v → φ w

theorem DynamicSemantics.ExpState.crit_const {W : Type u_1} (b : Prop) : (crit fun (x : W) => b) = ⊤

@[reducible]

def DynamicSemantics.ExpState.refine {W : Type u_1} (p : Preorder W) (φ : W → Prop) : Preorder W

The refinement of the pattern p with φ keeps the pairs of p that do not rank a world outside φ below a world inside it. It is the meet of p with the criterion pattern of φ.

Equations

• DynamicSemantics.ExpState.refine p φ = p ⊓ DynamicSemantics.ExpState.crit φ

theorem DynamicSemantics.ExpState.refine_le {W : Type u_1} {p : Preorder W} {φ : W → Prop} {w v : W} : w ≤ v ↔ w ≤ v ∧ (φ v → φ w)

theorem DynamicSemantics.ExpState.refine_empty {W : Type u_1} (p : Preorder W) : (refine p fun (x : W) => False) = p

Refining with the contradiction changes nothing.

theorem DynamicSemantics.ExpState.refine_univ {W : Type u_1} (p : Preorder W) : (refine p fun (x : W) => True) = p

Refining with the tautology changes nothing.

theorem DynamicSemantics.ExpState.refine_idem {W : Type u_1} (p : Preorder W) (φ : W → Prop) : refine (refine p φ) φ = refine p φ

Refining twice with one proposition is refining once.

theorem DynamicSemantics.ExpState.refine_comm {W : Type u_1} (p : Preorder W) (φ ψ : W → Prop) : refine (refine p φ) ψ = refine (refine p ψ) φ

The order of two refinements is immaterial.

theorem DynamicSemantics.ExpState.refine_mono {W : Type u_1} {p q : Preorder W} (h : p ≤ q) (φ : W → Prop) : refine p φ ≤ refine q φ

Refinement preserves refinement of patterns.

def DynamicSemantics.ExpState.Respects {W : Type u_1} (p : Preorder W) (φ : W → Prop) : Prop

The pattern p respects φ when it never ranks a world outside φ below a world inside it, that is, when it refines the criterion pattern of φ.

Equations

• DynamicSemantics.ExpState.Respects p φ = (p ≤ DynamicSemantics.ExpState.crit φ)

theorem DynamicSemantics.ExpState.respects_iff {W : Type u_1} {p : Preorder W} {φ : W → Prop} : Respects p φ ↔ ∀ ⦃w v : W⦄, w ≤ v → φ v → φ w

theorem DynamicSemantics.ExpState.Respects.mono {W : Type u_1} {p q : Preorder W} {φ : W → Prop} (h : Respects q φ) (hpq : p ≤ q) : Respects p φ

A refinement of a pattern respects what the pattern respects.

theorem DynamicSemantics.ExpState.respects_refine {W : Type u_1} (p : Preorder W) (φ : W → Prop) : Respects (refine p φ) φ

The refinement with φ respects φ.

theorem DynamicSemantics.ExpState.refine_eq_self_iff {W : Type u_1} {p : Preorder W} {φ : W → Prop} : refine p φ = p ↔ Respects p φ

A pattern respects φ exactly when refining with φ changes nothing.

theorem DynamicSemantics.ExpState.le_iff_forall_respects {W : Type u_1} {p : Preorder W} {w v : W} : w ≤ v ↔ ∀ (φ : W → Prop), Respects p φ → φ v → φ w

A pattern ranks w below v exactly when every proposition it respects that holds at v holds at w.

theorem DynamicSemantics.ExpState.minimals_subset_of_respects {W : Type u_1} {p : Preorder W} {φ : W → Prop} {d : Set W} (hr : Respects p φ) (ht : Std.Total LE.le) (hex : ∃ w ∈ d, φ w) : p.minimals d ⊆ {w : W | w ∈ d ∧ φ w}

Under a total pattern that respects φ, the minimal worlds of a domain containing a φ-world are φ-worlds. Totality is needed, since a world outside φ may otherwise be minimal by being incomparable with every φ-world.

theorem DynamicSemantics.ExpState.minimals_refine_top {W : Type u_1} (φ : W → Prop) (d : Set W) (hex : ∃ w ∈ d, φ w) : (refine ⊤ φ).minimals d = {w : W | w ∈ d ∧ φ w}

Refining the pattern under which all worlds are equally normal with φ makes the minimal worlds of a domain containing a φ-world exactly its φ-worlds.

Expectation states

structure DynamicSemantics.ExpState (W : Type u_2) : Type u_2

An expectation state pairs the agent's information, the worlds compatible with what is known, with an expectation pattern on worlds.

• info : Set W

  The worlds compatible with the agent's information.

• order : Preorder W

  The expectation pattern.

theorem DynamicSemantics.ExpState.ext_iff {W : Type u_2} {x y : ExpState W} : x = y ↔ x.info = y.info ∧ x.order = y.order

theorem DynamicSemantics.ExpState.ext {W : Type u_2} {x y : ExpState W} (info : x.info = y.info) (order : x.order = y.order) : x = y

def DynamicSemantics.ExpState.init {W : Type u_1} : ExpState W

In the initial state all worlds are possible and equally normal.

Equations

• DynamicSemantics.ExpState.init = { info := Set.univ, order := ⊤ }

def DynamicSemantics.ExpState.optimal {W : Type u_1} (σ : ExpState W) : Set W

The optimal worlds of a state are the most normal worlds compatible with the agent's information.

Equations

• σ.optimal = σ.order.minimals σ.info

def DynamicSemantics.ExpState.boxCs {W : Type u_1} (σ : ExpState W) (p : W → Prop) : Prop

Informational necessity □_cs holds of p when p holds at every world of the information state. This is entailment by the Stalnakerian context set and Portner's semantics of believe.

Equations

• σ.boxCs p = ∀ w ∈ σ.info, p w

def DynamicSemantics.ExpState.boxLe {W : Type u_1} (σ : ExpState W) (p : W → Prop) : Prop

Preferential necessity □_≤ holds of p when p holds at every optimal world, the worlds with no better-ranked competitor. This is Portner's semantics of want, the Kratzerian deontic and bouletic necessity, and the condition that presumably tests.

Equations

• σ.boxLe p = ∀ w ∈ σ.optimal, p w

def DynamicSemantics.ExpState.localNecessity {W : Type u_1} (σ : ExpState W) (p : W → Prop) : Prop

Local necessity holds of p when some world of the information sees only p-worlds among the worlds of the information at least as normal as itself, so that p holds throughout a branch of the pattern. This is Portner and Rubinstein's force of the subjunctive.

Equations

• σ.localNecessity p = OrderingSemantics.IsGoodPossibility σ.order σ.info {v : W | p v}

Update operations

def DynamicSemantics.ExpState.assert {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : ExpState W

Assertion eliminates the worlds outside φ and leaves the pattern alone.

Equations

• σ.assert φ = { info := {w : W | w ∈ σ.info ∧ φ w}, order := σ.order }

def DynamicSemantics.ExpState.promote {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : ExpState W

Promotion, the update with normally φ, refines the pattern with φ and leaves the information alone, so the agent learns that φ is expected and not that it is true.

Equations

• σ.promote φ = { info := σ.info, order := DynamicSemantics.ExpState.refine σ.order φ }

noncomputable def DynamicSemantics.ExpState.presumablyTest {W : Type u_1} (φ : W → Prop) (σ : ExpState W) : ExpState W

The test presumably φ passes when every optimal world satisfies φ, and otherwise empties the information.

Equations

• DynamicSemantics.ExpState.presumablyTest φ σ = if ∀ w ∈ σ.optimal, φ w then σ else { info := ∅, order := σ.order }

noncomputable def DynamicSemantics.ExpState.mightTest {W : Type u_1} (φ : W → Prop) (σ : ExpState W) : ExpState W

The test might φ passes when the information contains a φ-world, and otherwise empties the information. The pattern plays no role.

Equations

• DynamicSemantics.ExpState.mightTest φ σ = if ∃ w ∈ σ.info, φ w then σ else { info := ∅, order := σ.order }

Basic properties

@[simp]

theorem DynamicSemantics.ExpState.assert_info {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : (σ.assert φ).info = {w : W | w ∈ σ.info ∧ φ w}

@[simp]

theorem DynamicSemantics.ExpState.assert_order {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : (σ.assert φ).order = σ.order

@[simp]

theorem DynamicSemantics.ExpState.promote_info {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : (σ.promote φ).info = σ.info

@[simp]

theorem DynamicSemantics.ExpState.promote_order {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : (σ.promote φ).order = refine σ.order φ

theorem DynamicSemantics.ExpState.assert_info_subset {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : (σ.assert φ).info ⊆ σ.info

Assertion can only shrink the information.

Expectation states are ordered componentwise, a more constrained state lying below a less constrained one, as finer setoids lie below coarser ones, and the minimal state init is the top. Veltman orients his order the other way, with weaker states below stronger ones, and the content is the same. Both updates are additive, meeting the input with the update of init, so they are deflationary, monotone, idempotent and persistent, and his acceptance of φ in σ, that updating σ with φ returns σ, is the fixpoint condition σ ≤ σ[φ].

@[instance_reducible]

instance DynamicSemantics.ExpState.instPartialOrder {W : Type u_1} : PartialOrder (ExpState W)

Equations

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

@[instance_reducible]

instance DynamicSemantics.ExpState.instSemilatticeInf {W : Type u_1} : SemilatticeInf (ExpState W)

Equations

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

@[instance_reducible]

instance DynamicSemantics.ExpState.instOrderTop {W : Type u_1} : OrderTop (ExpState W)

Equations

• DynamicSemantics.ExpState.instOrderTop = { top := DynamicSemantics.ExpState.init, le_top := ⋯ }

theorem DynamicSemantics.ExpState.le_iff {W : Type u_1} {σ τ : ExpState W} : σ ≤ τ ↔ σ.info ⊆ τ.info ∧ σ.order ≤ τ.order

theorem DynamicSemantics.ExpState.top_eq_init {W : Type u_1} : ⊤ = init

theorem DynamicSemantics.ExpState.isAdditive_assert {W : Type u_1} (φ : W → Prop) : IsAdditive fun (x : ExpState W) => x.assert φ

Assertion is additive, since asserting φ meets the state with the assertion of φ in the minimal state.

theorem DynamicSemantics.ExpState.isAdditive_promote {W : Type u_1} (φ : W → Prop) : IsAdditive fun (x : ExpState W) => x.promote φ

Promotion is additive, so rules are additive just like assertions of fact.

theorem DynamicSemantics.ExpState.assert_le_self {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : σ.assert φ ≤ σ

Assertion lands below the input.

theorem DynamicSemantics.ExpState.promote_le_self {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : σ.promote φ ≤ σ

Promotion lands below the input.

theorem DynamicSemantics.ExpState.assert_mono {W : Type u_1} {σ τ : ExpState W} (h : σ ≤ τ) (φ : W → Prop) : σ.assert φ ≤ τ.assert φ

theorem DynamicSemantics.ExpState.promote_mono {W : Type u_1} {σ τ : ExpState W} (h : σ ≤ τ) (φ : W → Prop) : σ.promote φ ≤ τ.promote φ

theorem DynamicSemantics.ExpState.mem_foldl_assert_info {W : Type u_1} (ps : List (W → Prop)) (σ : ExpState W) (v : W) : v ∈ (List.foldl assert σ ps).info ↔ v ∈ σ.info ∧ ∀ p ∈ ps, p v

After a sequence of assertions the information is the input's information filtered by every asserted proposition.

theorem DynamicSemantics.ExpState.foldl_promote_order_le {W : Type u_1} (ps : List (W → Prop)) (σ : ExpState W) (w v : W) : w ≤ v ↔ w ≤ v ∧ ∀ p ∈ ps, p v → p w

After a sequence of promotions the pattern is the input's pattern refined with every promoted proposition.

@[simp]

theorem DynamicSemantics.ExpState.foldl_promote_info {W : Type u_1} (ps : List (W → Prop)) (σ : ExpState W) : (List.foldl promote σ ps).info = σ.info

A sequence of promotions leaves the information fixed.

theorem DynamicSemantics.ExpState.le_assert_iff {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : σ ≤ σ.assert φ ↔ σ.boxCs φ

A state accepts the assertion of φ exactly when φ already holds throughout its information.

theorem DynamicSemantics.ExpState.le_promote_iff {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : σ ≤ σ.promote φ ↔ Respects σ.order φ

A state accepts the promotion of φ exactly when its pattern already respects φ. This is support for the preferential component, distinct from truth at the optimal worlds.

theorem DynamicSemantics.ExpState.presumably_isTest {W : Type u_1} (φ : W → Prop) (σ : ExpState W) : (presumablyTest φ σ).info = σ.info ∨ (presumablyTest φ σ).info = ∅

The test presumably φ either returns the state or empties the information.

theorem DynamicSemantics.ExpState.isFixedPt_presumablyTest_iff {W : Type u_1} {φ : W → Prop} {σ : ExpState W} : Function.IsFixedPt (presumablyTest φ) σ ↔ σ.boxLe φ

A state accepts presumably φ exactly when φ is preferentially necessary in it.

theorem DynamicSemantics.ExpState.might_isTest {W : Type u_1} (φ : W → Prop) (σ : ExpState W) : (mightTest φ σ).info = σ.info ∨ (mightTest φ σ).info = ∅

The test might φ either returns the state or empties the information.

theorem DynamicSemantics.ExpState.mightTest_preserves_order {W : Type u_1} (φ : W → Prop) (σ : ExpState W) : (mightTest φ σ).order = σ.order

The test might φ preserves the pattern.

theorem DynamicSemantics.ExpState.presumablyTest_preserves_order {W : Type u_1} (φ : W → Prop) (σ : ExpState W) : (presumablyTest φ σ).order = σ.order

The test presumably φ preserves the pattern.

"Normally p; presumably p" succeeds

theorem DynamicSemantics.ExpState.normally_presumably_succeeds {W : Type u_1} (φ : W → Prop) (d : Set W) (hex : ∃ w ∈ d, φ w) : have σ := { info := d, order := ⊤ }; presumablyTest φ (σ.promote φ) = σ.promote φ

After normally φ from a state with no expectations, the test presumably φ passes, provided the information contains a φ-world.

Persistence

theorem DynamicSemantics.ExpState.persistence_assert {W : Type u_1} (σ : ExpState W) (φ ψ : W → Prop) (h : Respects σ.order φ) : Respects (σ.assert ψ).order φ

Asserting any ψ preserves respect for φ, so learning new facts does not undo expectations.

theorem DynamicSemantics.ExpState.persistence_normally {W : Type u_1} (σ : ExpState W) (φ ψ : W → Prop) (h : Respects σ.order φ) : Respects (σ.promote ψ).order φ

Promoting any ψ preserves respect for φ, so later defaults do not undo earlier ones.

theorem DynamicSemantics.ExpState.normally_creates_respect {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : Respects (σ.promote φ).order φ

After normally φ the pattern respects φ. With persistence, the promotion creates a permanent expectation.

Idempotency and commutativity

theorem DynamicSemantics.ExpState.promote_respects_idempotent {W : Type u_1} (σ : ExpState W) (φ : W → Prop) (h : Respects σ.order φ) : σ.promote φ = σ

If the pattern already respects φ, promoting φ changes nothing.

theorem DynamicSemantics.ExpState.promote_promote_self {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : (σ.promote φ).promote φ = σ.promote φ

Promoting φ twice is promoting it once.

theorem DynamicSemantics.ExpState.promote_comm {W : Type u_1} (σ : ExpState W) (φ ψ : W → Prop) : (σ.promote φ).promote ψ = (σ.promote ψ).promote φ

The order of two promotions is immaterial.

Conflicting defaults

theorem DynamicSemantics.ExpState.conflicting_defaults_le {W : Type u_1} (φ : W → Prop) (w v : W) : w ≤ v ↔ (φ v → φ w) ∧ (¬φ v → ¬φ w)

After normally φ and normally not φ the pattern relates two worlds only when they agree on φ. Worlds inside and outside φ can then both be optimal, so neither presumably φ nor presumably not φ passes. This is the unconditional case of conflicting defaults; the Nixon diamond, where the conflict arises between conditional defaults, needs the expectation frames of the paper's section 4.

theorem DynamicSemantics.ExpState.conflicting_defaults_iff_agree {W : Type u_1} (φ : W → Prop) (w v : W) : w ≤ v ↔ (φ w ↔ φ v)

Under two conflicting defaults w is at least as normal as v exactly when they agree on φ.

Compatible defaults

theorem DynamicSemantics.ExpState.compatible_defaults_optimal {W : Type u_1} (φ ψ : W → Prop) (d : Set W) (hφψ : ∀ (w : W), φ w → ψ w) (hex : ∃ w ∈ d, φ w) : (refine (refine ⊤ ψ) φ).minimals d ⊆ {w : W | w ∈ d ∧ φ w}

When φ implies ψ, promoting both makes the φ-worlds optimal, so the two expectations reinforce each other.

Necessity modals

Portner's mood unification operates on a partially ordered set of worlds, a pair of a context set and an ordering. This is Veltman's expectation state read at the level of discourse, with info as the Stalnakerian context set and order as the Kratzerian ordering source. Veltman says that a state accepts a sentence when updating with it changes nothing, a condition that Portner, following Farkas, reformulates for believe and want: acceptance of an assertion is informational necessity (le_assert_iff), and acceptance of presumably φ is preferential necessity (isFixedPt_presumablyTest_iff).

theorem DynamicSemantics.ExpState.boxCs_mono {W : Type u_1} (σ : ExpState W) (p q : W → Prop) (h : ∀ (w : W), p w → q w) : σ.boxCs p → σ.boxCs q

□_cs is upward monotone.

theorem DynamicSemantics.ExpState.boxLe_mono {W : Type u_1} (σ : ExpState W) (p q : W → Prop) (h : ∀ (w : W), p w → q w) : σ.boxLe p → σ.boxLe q

□_≤ is upward monotone.

theorem DynamicSemantics.ExpState.boxCs_assert_self {W : Type u_1} (σ : ExpState W) (p : W → Prop) : (σ.assert p).boxCs p

After asserting p, p is informationally necessary, the Stalnakerian principle that asserting p makes p common ground.

theorem DynamicSemantics.ExpState.boxCs_anti {W : Type u_1} {σ τ : ExpState W} (h : σ ≤ τ) (p : W → Prop) : τ.boxCs p → σ.boxCs p

Refining the state strengthens informational necessity. boxLe admits no parallel result, since refinement changes which worlds are best, in either direction.

theorem DynamicSemantics.ExpState.boxLe_of_respects {W : Type u_1} (σ : ExpState W) (p : W → Prop) (hresp : Respects σ.order p) (hconn : Std.Total LE.le) (hex : ∃ w ∈ σ.info, p w) : σ.boxLe p

If the pattern respects p and is total and the information has a p-world, then p is preferentially necessary, so presumably p passes. This is Veltman's normally φ ⊩ presumably φ, and it connects Portner's fixpoint semantics for want with his modal semantics. The converse fails, and without totality so does this direction, as in Veltman's ambiguous states.

theorem DynamicSemantics.ExpState.localNecessity_mono {W : Type u_1} (σ : ExpState W) (p q : W → Prop) (h : ∀ (w : W), p w → q w) : σ.localNecessity p → σ.localNecessity q

theorem DynamicSemantics.ExpState.localNecessity_iff_boxLe {W : Type u_1} {σ : ExpState W} {b : W} (hb : b ∈ σ.info) (hleast : ∀ v ∈ σ.info, b ≤ v) (p : W → Prop) : σ.localNecessity p ↔ σ.boxLe p

When the information has a world at least as normal as all of its worlds, local necessity is preferential necessity. Without one they come apart: two incomparable optimal worlds can each make a different proposition locally necessary while neither is preferentially necessary.