Necessity modals over expectation states

[Por18]'s partially ordered set of worlds — the pair ⟨cs, ≤⟩ his mood unification operates on — is [Vel96]'s ExpState read at the discourse level: info is the Stalnakerian context set ([Sta78]), order the Kratzerian ordering source ([Kra81]). This file adds the modal half of that API: the necessity modals over the two components, and the comparison of each with its update's acceptance fixpoint ([Vel96]'s σ ⊩ φ iff σ[φ] = σ, reformulated by [Por18] for believe and want following [Far03]).

Main definitions

• ExpState.boxCs: informational necessity □_cs — truth throughout the information state (Portner's believe).
• ExpState.boxLe: preferential necessity □_≤ — truth at all optimal worlds (Portner's want, Kratzerian deontic/bouletic modals ([CL12]), and the test condition of [Vel96]'s presumably).
• NormalModality: necessitation plus the K-axiom.

Main results

• le_assert_iff_boxCs: support of assert is boxCs — the fixpoint [Far03] uses to characterize indicative-licensing contexts.
• boxLe_of_respects: support of promote (Normality.respects) implies boxLe on connected orders with a witness — [Vel96]'s normally φ ⊩ presumably φ. The converse fails, and disconnected orders (Veltman's ambiguous states) break this direction too.

[CL12]'s preference structures order propositions, one type level above the world ordering here; POSW-style states consume Core.Order.PreferenceStructure.maxInducedLe rather than instantiating them.

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

Informational necessity □_cs ([Por18]): p holds at every world in the information state — the Stalnakerian context-set entailment, and Portner's semantics of believe.

Equations

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

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

Preferential necessity □_≤ ([Por18]): p holds at every optimal (best-ranked) world of the information state — Portner's best-world set is ExpState.optimal, the worlds with no higher-ranked competitors. The semantics of want and Kratzerian deontic/bouletic modals ([Kra81], [CL12]); also exactly the test condition of [Vel96]'s presumably (presumablyTest).

Equations

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

theorem UpdateSemantics.Default.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 UpdateSemantics.Default.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 UpdateSemantics.Default.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 assertion principle: asserting p makes p common ground. [Sta78]; [Por18].

theorem UpdateSemantics.Default.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: refinement changes which worlds are best, in either direction.

theorem UpdateSemantics.Default.ExpState.le_assert_iff_boxCs {W : Type u_1} (σ : ExpState W) (p : W → Prop) : σ ≤ σ.assert p ↔ σ.boxCs p

Assertive fixed-point: the input refines its own assertion iff the proposition is already informationally necessary — [Vel96]'s acceptance for the +-update, and the formal core of [Far03]'s assertive characterization of indicative-licensing contexts.

theorem UpdateSemantics.Default.ExpState.boxLe_of_respects {W : Type u_1} (σ : ExpState W) (p : W → Prop) (hresp : Core.Order.Normality.respects σ.order p) (hconn : Core.Order.Normality.connected σ.order) (hex : ∃ w ∈ σ.info, p w) : σ.boxLe p

Support implies preferential necessity on connected orders ([Vel96]'s normally φ ⊩ presumably φ, and the bridge between [Por18]'s fixpoint semantics for want and his modal semantics): if the ordering already respects p (the promote-support condition, ExpState.le_promote_iff) and is connected, and the information state has a p-world, then p holds at every optimal world. The converse fails, and without connectedness so does this direction — Veltman's ambiguous states.

Normal modality structure

boxCs and boxLe are both normal modalities — one shape of the inf-preservation pattern that ∀ over any subset enjoys. The third State modal boxAns is not normal (see Semantics/Mood/State.lean); it has its own closure structure under boolean operations instead.

class UpdateSemantics.Default.NormalModality (W : Type u_2) (box : (W → Prop) → Prop) : Prop

A normal modality in the sense of basic modal logic: a unary box over W → Prop predicates satisfying necessitation (box ⊤) and the K-axiom (box (p → q) → box p → box q).

• necessitation : box fun (x : W) => True

  Necessitation: the box always holds for ⊤.

• K (p q : W → Prop) : (box fun (w : W) => p w → q w) → box p → box q

  The K-axiom: distribution of the box over implication.

instance UpdateSemantics.Default.instNormalModalityBoxCs {W : Type u_1} (σ : ExpState W) : NormalModality W σ.boxCs

instance UpdateSemantics.Default.instNormalModalityBoxLe {W : Type u_1} (σ : ExpState W) : NormalModality W σ.boxLe