Partially Ordered Set of Worlds (POSW)

@cite{portner-2018} @cite{kratzer-1981} @cite{stalnaker-1978} @cite{farkas-2003} @cite{condoravdi-lauer-2012}

@cite{portner-2018} (Ch. 4) argues that the apparently disparate "mood" phenomena — verbal mood (indicative/subjunctive selection by attitudes), sentence mood (declarative/imperative/interrogative force), and modal flavor (epistemic/deontic/bouletic) — all share a single mathematical substrate: a partially ordered set of worlds that the relevant linguistic objects update or quantify over. The pair-of-information-and- ordering structure with +/⋆ updates predates @cite{portner-2018}; @cite{farkas-2003} introduces it for assertion-vs-direction, and the Stalnakerian context-set/Kratzerian ordering-source decomposition behind it goes back to @cite{stalnaker-1978} and @cite{kratzer-1981}. @cite{condoravdi-lauer-2012} works out the preferential-modal side (desire predicates over orderings) in detail. Caveat: C&L's preference structures are strict partial orders on propositions (Set (Set W)), one type level above POSW's preorder on worlds (W → W → Prop); see Core.Order.PreferenceStructure. The two connect via the maximal-element-induced world preorder (Core.Order.PreferenceStructure.maxInducedLe) — POSW consumes the output of C&L's machinery rather than instantiating it. The "preferential-modal side" framing is thematic, not structural.

A POSW is a pair c = ⟨cs_c, ≤_c⟩ where:

• cs_c ⊆ W is a non-empty set of worlds (the "context set" — the informational component, à la @cite{stalnaker-1978});
• ≤_c is a reflexive transitive preorder on cs_c (the "ordering source" component, à la @cite{kratzer-1981}). @cite{portner-2018} writes this < and reads it "at-least-as-good as", which is the reflexive ≤ reading; we use le for mathlib alignment.

There are two canonical updates:

• +-update refines cs by intersection: c + p keeps only cs-worlds where p holds. Targets the informational component.
• ⋆-update refines ≤ by promoting p-worlds: in c ⋆ p, the ordering on cs is the original ordering plus the constraint that any world satisfying p is at least as good as one that doesn't. Targets the preferential component.

There are two canonical necessity modals:

• □_cs p — informational necessity: p holds at every world in cs.
• □_≤ p — preferential necessity: p holds at every ≤-best world in cs.

Portner's central architectural insight is that what differs across mood-and-modality phenomena is which POSW component is targeted, not the substrate itself. Belief vs. desire is □_cs vs. □_≤ over the same agent's POSW; assertion vs. directive is + vs. ⋆ over the discourse POSW; epistemic vs. deontic modal flavor is the same split again.

The + and ⋆ updates target disjoint POSW components — that is the content of updates_target_disjoint_components below, which is the mathematical core of Portner's unification thesis.

Notes

• We work with W → Prop (classical propositions) rather than W → Bool (decidable propositions) because POSW is the foundational substrate; decidability concerns belong downstream.
• @cite{portner-2018} (Ch. 4, footnote 3) flags a strict-typing wart: on his definition c + p is technically not a POSW because the ordering is not restricted to the new (smaller) cs. We inherit the same wart (our plus keeps c.le unchanged), and the same workaround: read the le_refl / le_trans axioms as conditioned on cs-membership, so behaviour outside cs is irrelevant.
• We use a reflexive partial preorder le matching the partition / Setoid lattice convention (finer ≤ coarser).

Lattice unification (linglib extension)

@cite{portner-2018} writes eq. (2a) as set intersection and eq. (2b) via Condoravdi-Lauer ordering refinement; the ?-update (our extension) is naturally a Setoid meet. All three updates turn out to be inf in three parallel mathlib lattices, none of which appear in @cite{portner-2018}:

update	acts on	lattice	identity
+	cs	Pi.instLattice over Prop	(c + p).cs = c.cs ⊓ p (plus_cs_eq_inf)
⋆	le	Pi.instLattice over Prop	(c ⋆ p).le = c.le ⊓ promote p (star_le_eq_inf)
?	inquiry	Setoid.completeLattice	(c ? q).inquiry = c.inquiry ⊓ q (POSWQ)

The unified picture: each of the three POSW(Q) components carries an already-mathlib'd lattice, and each update is meet in its component's lattice. Commutativity (star_star_comm_le), idempotency (star_star_self_le), and the corresponding theorems on the other two updates all collapse to one-line invocations of inf_right_comm / inf_idem in the appropriate lattice. The K-axiom for boxCs / boxLe (§8) is the universal-quantification-preserves-inf pattern.

structure Core.Mood.POSW (W : Type u) : Type u

A partially ordered set of worlds (POSW): a non-empty subset cs of worlds equipped with a reflexive transitive ordering le on cs. @cite{portner-2018} (Ch. 4) writes the ordering < (at-least-as-good); we use le for mathlib alignment. The underlying pair structure appears already in @cite{farkas-2003}.

Non-emptiness is not enforced at the type level — empty POSWs are pathological but algebraically permitted (e.g., the result of +-updating with an inconsistent proposition). Operations make sense regardless.

• cs : W → Prop

  The context set: worlds compatible with the POSW's information.

• le : W → W → Prop

  The ordering: le w v means w is at least as good as v. Reflexive on cs, transitive on cs.

• le_refl (w : W) : self.cs w → self.le w w

  Reflexivity on the context set.

• le_trans (w u v : W) : self.cs w → self.cs u → self.cs v → self.le w u → self.le u v → self.le w v

  Transitivity on the context set.

§1. Updates: + and ⋆

def Core.Mood.POSW.plus {W : Type u} (c : POSW W) (p : W → Prop) : POSW W

+-update (@cite{portner-2018}, Ch. 4 §4.1; @cite{farkas-2003}): refine cs by intersection with p. Leaves ≤ untouched.

Used by assertion (Stalnakerian context-set update) and by □_cs modals' restriction.

Footnote 3 wart: the resulting le is not strictly restricted to the new cs, but the structure satisfies the (cs-conditioned) POSW axioms.

Equations

• c.plus p = { cs := fun (w : W) => c.cs w ∧ p w, le := c.le, le_refl := ⋯, le_trans := ⋯ }

def Core.Mood.POSW.star {W : Type u} (c : POSW W) (p : W → Prop) : POSW W

⋆-update (@cite{portner-2018}, Ch. 4 §4.1; @cite{farkas-2003}): refine ≤ by promoting p-worlds. The new ordering keeps the old ordering and additionally requires that whenever the upper world satisfies p, the lower world does too.

Used by directives (To-Do List update à la @cite{portner-2004}) and by □_≤ modals' refinement (@cite{condoravdi-lauer-2012}).

Equations

• c.star p = { cs := c.cs, le := fun (w v : W) => c.le w v ∧ (p v → p w), le_refl := ⋯, le_trans := ⋯ }

§2. Modals: □_cs and □_≤

def Core.Mood.POSW.best {W : Type u} (c : POSW W) (w : W) : Prop

A world is best in c if it is in cs and at least as good as every other cs-world. The quantification domain of @cite{portner-2018}'s preferential necessity modal □_≤.

Equations

• c.best w = (c.cs w ∧ ∀ (v : W), c.cs v → c.le v w)

def Core.Mood.POSW.boxCs {W : Type u} (c : POSW W) (p : W → Prop) : Prop

Informational necessity □_cs (@cite{portner-2018}, Ch. 4 §4.1): p holds at every world in the context set. The semantics of believe and the Stalnakerian context-set entailment.

Equations

• c.boxCs p = ∀ (w : W), c.cs w → p w

def Core.Mood.POSW.boxLe {W : Type u} (c : POSW W) (p : W → Prop) : Prop

Preferential necessity □_≤ (@cite{portner-2018}, Ch. 4 §4.1): p holds at every ≤-best world in the context set. The semantics of want and Kratzerian deontic/bouletic modals (@cite{kratzer-1981}, @cite{condoravdi-lauer-2012}).

Equations

• c.boxLe p = ∀ (w : W), c.best w → p w

@[reducible, inline, deprecated Core.Mood.POSW.boxLe (since := "2026-04-18")]

abbrev Core.Mood.POSW.boxLt {W : Type u} (c : POSW W) (p : W → Prop) : Prop

Equations

• c.boxLt p = c.boxLe p

§3. Algebraic facts

@[simp]

theorem Core.Mood.POSW.plus_cs {W : Type u} (c : POSW W) (p : W → Prop) (w : W) : (c.plus p).cs w ↔ c.cs w ∧ p w

@[simp]

theorem Core.Mood.POSW.plus_le {W : Type u} (c : POSW W) (p : W → Prop) : (c.plus p).le = c.le

@[simp]

theorem Core.Mood.POSW.star_cs {W : Type u} (c : POSW W) (p : W → Prop) : (c.star p).cs = c.cs

@[simp]

theorem Core.Mood.POSW.star_le {W : Type u} (c : POSW W) (p : W → Prop) (w v : W) : (c.star p).le w v ↔ c.le w v ∧ (p v → p w)

Lattice characterization of +-update

+-update on cs is meet in the Heyting algebra W → Prop: the new context set is the pointwise conjunction of the old context set and the asserted proposition. The identity is definitional — no proof obligation. This puts the @cite{portner-2018} eq. (2a) "c + ϕ = ⟨cs_c ∩ ⟦ϕ⟧^c, <_c⟩" on the same algebraic footing as the Setoid meet that defines POSWQ.inquire and the relation meet that defines star (§6). The mathlib instance chain is Prop.instDistribLattice → Pi.instLattice.

@[simp]

theorem Core.Mood.POSW.plus_cs_eq_inf {W : Type u} (c : POSW W) (p : W → Prop) : (c.plus p).cs = c.cs ⊓ p

+-update on cs is meet in W → Prop. The Heyting characterization of @cite{portner-2018} eq. (2a) — c + ϕ intersects cs with ϕ.

theorem Core.Mood.POSW.updates_target_disjoint_components {W : Type u} (c : POSW W) (p : W → Prop) : (c.plus p).le = c.le ∧ (c.star p).cs = c.cs

Portner's central insight: the two updates target disjoint POSW components. + revises cs and leaves le alone; ⋆ revises le and leaves cs alone.

This is the mathematical content of @cite{portner-2018}'s unification thesis (Ch. 4): the surface diversity of mood phenomena reduces to which component of the same substrate gets touched.

theorem Core.Mood.POSW.plus_cs_mono {W : Type u} (c : POSW W) (p q : W → Prop) (h : ∀ (w : W), p w → q w) (w : W) : (c.plus p).cs w → (c.plus q).cs w

+-update is monotone in the proposition (intersection lemma).

theorem Core.Mood.POSW.plus_top_cs {W : Type u} (c : POSW W) (w : W) : (c.plus fun (x : W) => True).cs w ↔ c.cs w

+-update with a tautology is the identity on cs.

theorem Core.Mood.POSW.boxCs_mono {W : Type u} (c : POSW W) (p q : W → Prop) (h : ∀ (w : W), p w → q w) : c.boxCs p → c.boxCs q

□_cs is upward monotone.

theorem Core.Mood.POSW.boxLe_mono {W : Type u} (c : POSW W) (p q : W → Prop) (h : ∀ (w : W), p w → q w) : c.boxLe p → c.boxLe q

□_≤ is upward monotone.

@[deprecated Core.Mood.POSW.boxLe_mono (since := "2026-04-18")]

theorem Core.Mood.POSW.boxLt_mono {W : Type u} (c : POSW W) (p q : W → Prop) (h : ∀ (w : W), p w → q w) : c.boxLe p → c.boxLe q

theorem Core.Mood.POSW.boxCs_plus_self {W : Type u} (c : POSW W) (p : W → Prop) : (c.plus p).boxCs p

After +-updating with p, p becomes informationally necessary. The Stalnakerian assertion principle: asserting p makes p common ground. @cite{stalnaker-1978}, @cite{portner-2018} (Ch. 4).

§4. Refinement preorder

A POSW is more refined than another when it carries strictly more information: a smaller context set, and a smaller (i.e., more discriminating) ordering relation. In the @cite{portner-2018} update algebra, both +-update and ⋆-update produce a refinement of the input POSW — refinement is what update means.

The order convention follows the partition / Setoid lattice in mathlib: finer ≤ coarser, more constrained ≤ less constrained. The trivial POSW (cs = ⊤, le = ⊤) sits at the top; a fully informative POSW (smaller cs, smaller le) sits below.

The boxCs_anti lemma gives the modal counterpart: refining the POSW strengthens informational necessity. boxLe admits no parallel result in general — refinement can change which worlds are best.

(The componentwise refinement preorder is not stated in @cite{portner-2018}; it is our linglib addition, packaging the "update means refine" intuition into a Preorder instance so the update lemmas factor through ≤ and downstream Setoid-style machinery composes.)

@[implicit_reducible]

instance Core.Mood.POSW.instPreorder {W : Type u} : Preorder (POSW W)

Refinement order on POSWs: c₁ ≤ c₂ iff c₁ is at least as constrained as c₂ — its context set is a subset of c₂'s, and its ordering relation is a subset of c₂'s (fewer pairs are "at-least-as-good as" each other under c₁ than under c₂). Both POSW updates land in the input's lower set.

Equations

• Core.Mood.POSW.instPreorder = { le := fun (c₁ c₂ : Core.Mood.POSW W) => (∀ (w : W), c₁.cs w → c₂.cs w) ∧ ∀ (w v : W), c₁.le w v → c₂.le w v, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem Core.Mood.POSW.le_iff {W : Type u} (c₁ c₂ : POSW W) : c₁ ≤ c₂ ↔ (∀ (w : W), c₁.cs w → c₂.cs w) ∧ ∀ (w v : W), c₁.le w v → c₂.le w v

theorem Core.Mood.POSW.plus_le_self {W : Type u} (c : POSW W) (p : W → Prop) : c.plus p ≤ c

+-update lands below the input: refining cs by intersection with p can only constrain the POSW further.

theorem Core.Mood.POSW.star_le_self {W : Type u} (c : POSW W) (p : W → Prop) : c.star p ≤ c

⋆-update lands below the input: refining le with the p-promotion constraint can only constrain the POSW further.

theorem Core.Mood.POSW.plus_mono {W : Type u} {c₁ c₂ : POSW W} (h : c₁ ≤ c₂) (p : W → Prop) : c₁.plus p ≤ c₂.plus p

+-update is monotone in the underlying POSW: refining c₁ against c₂ is preserved by adding the same +-update on top.

theorem Core.Mood.POSW.star_mono {W : Type u} {c₁ c₂ : POSW W} (h : c₁ ≤ c₂) (p : W → Prop) : c₁.star p ≤ c₂.star p

⋆-update is monotone in the underlying POSW.

theorem Core.Mood.POSW.boxCs_anti {W : Type u} (c₁ c₂ : POSW W) (h : c₁ ≤ c₂) (p : W → Prop) : c₂.boxCs p → c₁.boxCs p

Refining the POSW strengthens informational necessity: if c₁ is more refined than c₂ and p is informationally necessary at c₂, then p is informationally necessary at c₁ too.

boxLe does not admit a parallel anti-monotonicity result: refining the POSW changes which worlds are best, and the change can move p-satisfying worlds either into or out of the best set.

§5. Subtype Preorder

POSW W is not a Preorder W (the le axioms are conditioned on cs-membership). But it is a Preorder (Subtype c.cs) — the cs-restricted subtype carries an unconditional reflexive transitive preorder, courtesy of le_refl and le_trans. This makes mathlib's Preorder API (transitivity tactics, le_trans, le_refl, …) available on the in-context portion.

@[implicit_reducible]

instance Core.Mood.POSW.instPreorderSubtype {W : Type u} (c : POSW W) : Preorder { w : W // c.cs w }

The cs-restricted subtype carries a reflexive transitive preorder: the conditioning on cs-membership becomes unconditional once we work in the subtype. Gives access to mathlib's Preorder API on the in-context worlds.

Equations

• c.instPreorderSubtype = { le := fun (w v : { w : W // c.cs w }) => c.le ↑w ↑v, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

§6. The promote preorder and ⋆-update as relation meet

⋆-update has a clean lattice-theoretic identity: it is meet in the relation lattice W → W → Prop of the existing preorder with the promotion preorder of p, where promote p w v says "if p holds at the lower world it holds at the higher one too". This is the relation-side analogue of plus_cs_eq_inf (§3): +-update is meet in W → Prop, ⋆-update is meet in W → W → Prop. Both reduce their respective updates to the same mathematical operation — Pi.instLattice over Prop.instDistribLattice — and inherit inf_comm, inf_assoc, inf_idem for free, which closes the commutativity / idempotency theorems below in one line each.

The relation-meet identity also explains why ⋆-update is not a literal monoid action of (W → Prop, ∧, ⊤) on POSW W: promote (p ∧ q) is in general strictly finer than promote p ⊓ promote q (a world where p holds and q doesn't witnesses the gap). What we get is weaker than a monoid action, but the relation-lattice meet is exactly the right level of abstraction for the algebraic theorems below.

def Core.Mood.POSW.promote {W : Type u} (p : W → Prop) (w v : W) : Prop

The promotion preorder of a proposition: w is at least as p-good as v iff p-truth at v carries to p-truth at w. The structural content of ⋆-update on the ordering: one ⋆-application meets c.le with promote p in W → W → Prop.

Equations

• Core.Mood.POSW.promote p w v = (p v → p w)

theorem Core.Mood.POSW.promote_refl {W : Type u} (p : W → Prop) (w : W) : promote p w w

theorem Core.Mood.POSW.promote_trans {W : Type u} (p : W → Prop) (w u v : W) : promote p w u → promote p u v → promote p w v

@[simp]

theorem Core.Mood.POSW.star_le_eq_inf {W : Type u} (c : POSW W) (p : W → Prop) : (c.star p).le = c.le ⊓ promote p

⋆-update is meet in W → W → Prop: (c ⋆ p).le = c.le ⊓ promote p. The relation-side analogue of plus_cs_eq_inf — both updates are inf in the appropriate Pi-over-Prop lattice. Definitional.

@[simp]

theorem Core.Mood.POSW.star_le_eq {W : Type u} (c : POSW W) (p : W → Prop) (w v : W) : (c.star p).le w v ↔ c.le w v ∧ promote p w v

Pointwise restatement of star_le_eq_inf.

theorem Core.Mood.POSW.star_star_comm_le {W : Type u} (c : POSW W) (p q : W → Prop) : ((c.star p).star q).le = ((c.star q).star p).le

⋆-update commutes with itself (relation level): applying two ⋆-updates in either order produces the same ordering relation. One-line corollary of inf_right_comm in W → W → Prop.

theorem Core.Mood.POSW.star_star_self_le {W : Type u} (c : POSW W) (p : W → Prop) : ((c.star p).star p).le = (c.star p).le

⋆-update is idempotent (relation level): applying the same ⋆-update twice produces the same ordering as once. One-line corollary of inf_assoc + inf_idem in W → W → Prop.

§7. Farkas-style update fixed-point

@cite{farkas-2003}'s eq. 11 alternative to the @cite{portner-2018} Indicative/Subjunctive Principles characterizes mood selection by update type: declarative +-update vs. directive ⋆-update, rather than by the matrix operator. The mathematical core is the update-fixedpoint characterization: an update adds nothing exactly when its content is already consequential at the input.

For +-update on cs: c already implies p (i.e. c.boxCs p) iff c ≤ c.plus p (i.e. c.plus p doesn't shrink cs).

theorem Core.Mood.POSW.le_plus_iff_boxCs {W : Type u} (c : POSW W) (p : W → Prop) : c ≤ c.plus p ↔ c.boxCs p

Farkas update-fixedpoint for +: the input refines the +-update iff the proposition is already informationally necessary. Formal content of @cite{farkas-2003}'s eq. 11 distinction between consequential and merely-redundant assertions.

§8. Normal modality structure

boxCs and boxLe are both normal modalities in the sense of modal logic: each satisfies necessitation (□⊤) and the K-axiom (□(p→q) → □p → □q). The K-axiom is one shape of the general inf-preservation pattern that ∀ over any subset enjoys: (∀ w ∈ S, p w → q w) ∧ (∀ w ∈ S, p w) → (∀ w ∈ S, q w). So both boxCs (= ∀_{c.cs}) and boxLe (= ∀_{c.best}) inherit normality from Pi.instLattice on Prop — the same lattice that underlies + and ⋆ updates (cf. file docstring "Lattice unification" table).

The third modal boxAns is not normal — it does not satisfy K. A counterexample: with cs = {a, b, c}, inquiry partition {{a, b}, {c}}, take p false on {a, b} and q true at a, false at b. Then boxAns p (vacuously, since p is false on the cell), boxAns (p → q) (vacuously, since p → q is true on the cell when p is false), but not boxAns q. boxAns instead has its own closure structure: it is closed under boolean operations on the proposition (POSWQ.boxAns_not / and / or / imp), which makes it a different kind of constancy modality.

The NormalModality typeclass packages N + K and exposes them by TC inference, so any future code that abstracts over a normal box can dispatch to boxCs and boxLe uniformly.

class Core.Mood.POSW.NormalModality (W : Type u) (box : (W → Prop) → Prop) : Prop

A normal modality in the sense of basic modal logic: quantifies a unary box over W → Prop predicates, satisfying necessitation (box ⊤) and the K-axiom (box (p → q) → box p → box q). The two POSW universal modalities boxCs and boxLe are normal; POSWQ.boxAns is not (see the section docstring).

• 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 Core.Mood.POSW.instNormalModalityBoxCs {W : Type u} (c : POSW W) : NormalModality W c.boxCs

instance Core.Mood.POSW.instNormalModalityBoxLe {W : Type u} (c : POSW W) : NormalModality W c.boxLe