The mood state

The mood state of [Por18] — his posw ⟨cs, ≤⟩, [Vel96]'s expectation state under a modal reading — extended with a third coordinate recording the open question: inquiry : Setoid W partitions worlds into answers ([GS84]'s partition theory, the QUD tradition of [Rob12]). Portner considers two interrogative extensions: his pposw (his (10)) replaces the context set with a partition of it, while a separate question-set coordinate — the design here — is the alternative he credits to [Rob96] and [Por04]. The separate coordinate preserves the disjoint-target architecture: assert, promote, and inquire each touch one coordinate, each update is meet in its coordinate's lattice, and the commutation and acceptance facts are one-line inf-facts.

Main declarations

• State — an ExpState plus inquiry : Setoid W.
• inquire, State.assert, State.promote — the single-coordinate updates.
• boxAns — the third modal: settled by the question.
• polarSetoid — the partition a single proposition contributes.
• stateAt — the state a Kratzer pair induces at a world.

Main statements

• le_inquire_iff — acceptance for ?: support iff the inquiry already refines the question.
• boxAns_of_inquiry_le_polarSetoid, inquiry_le_polarSetoid_iff_boxAns_of_univ — support vs answerhood.
• boxAns_not_reducible_to_boxCs — the inquiry coordinate does genuine work.
• simpleNecessity_iff_boxCs, necessity_iff_boxLe — [Por18]'s (3a)/(3b): Kratzer necessity as the state modals.

Implementation notes

The ?-update, boxAns, and the interrogative column are this library's extensions; they do not appear in [Por18]. Inquiry is a partition, not a general inquisitive content: non-partition phenomena (mention-some, intermediate exhaustivity — [TRA18], Studies/TheilerRoelofsenAloni2018.lean) live in Question W, with Question.fromSetoid (Semantics/Questions/Partition/Basic.lean) as the faithful embedding.

structure Mood.State (W : Type u_1) extends UpdateSemantics.Default.ExpState W : Type u_1

The mood state: an ExpState enriched with an inquiry partition recording the open question (⊤ is "no question").

• info : Set W
• order : Preorder W
• inquiry : Setoid W

  The inquiry partition: inquiry.r w v means worlds w and v are indistinguishable answers to the open question.

Constructors

def Mood.State.ofExpState {W : Type u_1} (σ : UpdateSemantics.Default.ExpState W) : State W

The State with no question under discussion.

Equations

• Mood.State.ofExpState σ = { toExpState := σ, inquiry := ⊤ }

@[simp]

theorem Mood.State.ofExpState_toExpState {W : Type u_1} (σ : UpdateSemantics.Default.ExpState W) : (ofExpState σ).toExpState = σ

@[simp]

theorem Mood.State.ofExpState_inquiry {W : Type u_1} (σ : UpdateSemantics.Default.ExpState W) : (ofExpState σ).inquiry = ⊤

def Mood.State.polarSetoid {W : Type u_1} (q : W → Prop) : Setoid W

The polar Setoid of a proposition: worlds are equivalent iff they agree on q. Distinct from Setoid.ker q, which uses = on propositions rather than ↔.

Equations

• Mood.State.polarSetoid q = { r := fun (w v : W) => q w ↔ q v, iseqv := ⋯ }

@[simp]

theorem Mood.State.polarSetoid_r {W : Type u_1} (q : W → Prop) (w v : W) : (polarSetoid q) w v ↔ (q w ↔ q v)

@[simp]

theorem Mood.State.polarSetoid_top {W : Type u_1} : (polarSetoid fun (x : W) => True) = ⊤

The third update: ? (inquiry refinement)

def Mood.State.inquire {W : Type u_1} (c : State W) (q : Setoid W) : State W

The ?-update: refine the inquiry partition by meet with q, touching no other coordinate.

Equations

• c.inquire q = { toExpState := c.toExpState, inquiry := c.inquiry ⊓ q }

@[simp]

theorem Mood.State.inquire_toExpState {W : Type u_1} (c : State W) (q : Setoid W) : (c.inquire q).toExpState = c.toExpState

@[simp]

theorem Mood.State.inquire_info {W : Type u_1} (c : State W) (q : Setoid W) : (c.inquire q).info = c.info

@[simp]

theorem Mood.State.inquire_order {W : Type u_1} (c : State W) (q : Setoid W) : (c.inquire q).order = c.order

@[simp]

theorem Mood.State.inquire_inquiry_eq_inf {W : Type u_1} (c : State W) (q : Setoid W) : (c.inquire q).inquiry = c.inquiry ⊓ q

The ?-update is meet in the Setoid lattice.

The third modal: boxAns (informational answerhood)

def Mood.State.boxAns {W : Type u_1} (c : State W) (p : W → Prop) : Prop

Informational answerhood: p is settled by the question iff it has a constant truth value on every inquiry cell within info ([GS84]-style answerhood). Not upward-monotone in p, unlike boxCs and boxLe; the natural monotonicity is boxAns_anti in the state.

Equations

• c.boxAns p = ∀ (w v : W), w ∈ c.info → v ∈ c.info → c.inquiry w v → (p w ↔ p v)

Refinement preorder

@[implicit_reducible]

instance Mood.State.instPreorder {W : Type u_1} : Preorder (State W)

Equations

• Mood.State.instPreorder = { le := fun (c₁ c₂ : Mood.State W) => c₁.toExpState ≤ c₂.toExpState ∧ c₁.inquiry ≤ c₂.inquiry, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem Mood.State.le_iff {W : Type u_1} (c₁ c₂ : State W) : c₁ ≤ c₂ ↔ c₁.toExpState ≤ c₂.toExpState ∧ c₁.inquiry ≤ c₂.inquiry

theorem Mood.State.inquire_le_self {W : Type u_1} (c : State W) (q : Setoid W) : c.inquire q ≤ c

The ?-update lands below the input.

theorem Mood.State.inquire_mono {W : Type u_1} {c₁ c₂ : State W} (h : c₁ ≤ c₂) (q : Setoid W) : c₁.inquire q ≤ c₂.inquire q

?-update is monotone in the underlying State.

theorem Mood.State.le_inquire_iff {W : Type u_1} (c : State W) (q : Setoid W) : c ≤ c.inquire q ↔ c.inquiry ≤ q

Acceptance for ?: the input refines its own update iff its inquiry already refines the question ([Vel96]'s acceptance at the third coordinate).

theorem Mood.State.boxAns_of_inquiry_le_polarSetoid {W : Type u_1} (c : State W) (p : W → Prop) (h : c.inquiry ≤ polarSetoid p) : c.boxAns p

Support implies answerhood: an inquiry refining p's polar partition settles p.

theorem Mood.State.inquiry_le_polarSetoid_iff_boxAns_of_univ {W : Type u_1} (c : State W) (p : W → Prop) (h : c.info = Set.univ) : c.inquiry ≤ polarSetoid p ↔ c.boxAns p

With total information, answerhood is polar-partition support: the info-guards are the only gap.

theorem Mood.State.boxAns_anti {W : Type u_1} (c₁ c₂ : State W) (h : c₁ ≤ c₂) (p : W → Prop) : c₂.boxAns p → c₁.boxAns p

Refining the state strengthens answerhood (the counterpart of ExpState.boxCs_anti).

Closure properties of boxAns

Constant-on-cell propositions are closed under the Boolean operations: answers combine like ordinary propositions.

theorem Mood.State.boxAns_not {W : Type u_1} (c : State W) (p : W → Prop) : c.boxAns p → c.boxAns fun (w : W) => ¬p w

Negation preserves answerhood.

theorem Mood.State.boxAns_and {W : Type u_1} (c : State W) (p q : W → Prop) : c.boxAns p → c.boxAns q → c.boxAns fun (w : W) => p w ∧ q w

Conjunction preserves answerhood.

theorem Mood.State.boxAns_or {W : Type u_1} (c : State W) (p q : W → Prop) : c.boxAns p → c.boxAns q → c.boxAns fun (w : W) => p w ∨ q w

Disjunction preserves answerhood.

theorem Mood.State.boxAns_imp {W : Type u_1} (c : State W) (p q : W → Prop) : c.boxAns p → c.boxAns q → c.boxAns fun (w : W) => p w → q w

Material implication preserves answerhood.

Three-coordinate update disjointness

def Mood.State.assert {W : Type u_1} (c : State W) (p : W → Prop) : State W

The inquiry-preserving lift of ExpState.assert.

Equations

• c.assert p = { toExpState := c.assert p, inquiry := c.inquiry }

def Mood.State.promote {W : Type u_1} (c : State W) (p : W → Prop) : State W

The inquiry-preserving lift of ExpState.promote.

Equations

• c.promote p = { toExpState := c.promote p, inquiry := c.inquiry }

@[simp]

theorem Mood.State.assert_toExpState {W : Type u_1} (c : State W) (p : W → Prop) : (c.assert p).toExpState = c.assert p

@[simp]

theorem Mood.State.assert_inquiry {W : Type u_1} (c : State W) (p : W → Prop) : (c.assert p).inquiry = c.inquiry

@[simp]

theorem Mood.State.promote_toExpState {W : Type u_1} (c : State W) (p : W → Prop) : (c.promote p).toExpState = c.promote p

@[simp]

theorem Mood.State.promote_inquiry {W : Type u_1} (c : State W) (p : W → Prop) : (c.promote p).inquiry = c.inquiry

@[simp]

theorem Mood.State.assert_promote_comm {W : Type u_1} (c : State W) (p q : W → Prop) : (c.assert p).promote q = (c.promote q).assert p

assert and promote commute.

@[simp]

theorem Mood.State.assert_inquire_comm {W : Type u_1} (c : State W) (p : W → Prop) (s : Setoid W) : (c.assert p).inquire s = (c.inquire s).assert p

assert and inquire commute.

@[simp]

theorem Mood.State.promote_inquire_comm {W : Type u_1} (c : State W) (p : W → Prop) (s : Setoid W) : (c.promote p).inquire s = (c.inquire s).promote p

promote and inquire commute.

theorem Mood.State.inquire_inquire_self {W : Type u_1} (c : State W) (s : Setoid W) : ((c.inquire s).inquire s).inquiry = (c.inquire s).inquiry

The ?-update is idempotent.

Separation: boxAns is not boxCs

def Mood.State.sepInquiry : State Bool

A two-cell inquiry over Bool with total information and the discrete inquiry.

Equations

• Mood.State.sepInquiry = { info := Set.univ, order := Core.Order.Normality.total, inquiry := ⊥ }

def Mood.State.sepProp : Bool → Prop

A proposition constant on each cell but not throughout info.

Equations

• Mood.State.sepProp w = (w = false)

theorem Mood.State.boxAns_sepInquiry_sepProp : sepInquiry.boxAns sepProp

theorem Mood.State.not_boxCs_sepInquiry_sepProp : ¬sepInquiry.boxCs sepProp

theorem Mood.State.boxAns_not_reducible_to_boxCs : ∃ (c : State Bool) (p : Bool → Prop), c.boxAns p ∧ ¬c.boxCs p

The inquiry coordinate does genuine work: boxAns holds where boxCs fails.

The modal projection

def Mood.Component.boxOn {W : Type u_1} : Component → State W → (W → Prop) → Prop

The necessity modal quantifying over a component — boxCs, boxLe, or boxAns. Mood interpretations factor through it as boxOn ∘ target (VerbalOp.interp, SpeechEvent.modal).

Equations

• Mood.Component.informational.boxOn x✝¹ x✝ = x✝¹.boxCs x✝
• Mood.Component.preferential.boxOn x✝¹ x✝ = x✝¹.boxLe x✝
• Mood.Component.inquisitive.boxOn x✝¹ x✝ = x✝¹.boxAns x✝

@[simp]

theorem Mood.boxOn_informational {W : Type u_1} (c : State W) (p : W → Prop) : Component.informational.boxOn c p = c.boxCs p

@[simp]

theorem Mood.boxOn_preferential {W : Type u_1} (c : State W) (p : W → Prop) : Component.preferential.boxOn c p = c.boxLe p

@[simp]

theorem Mood.boxOn_inquisitive {W : Type u_1} (c : State W) (p : W → Prop) : Component.inquisitive.boxOn c p = c.boxAns p

Kratzer backgrounds induce states

[Por18]'s gloss on his (3): reading the mood state's components as a modal base and ordering source ([Kra81]), □_cs expresses simple necessity and □_≤ human necessity. stateAt is that identification read in the other direction — a Kratzer pair is a world-indexed family of expectation states — and the theorems below are his (3a)/(3b).

def Mood.stateAt {W : Type u_1} (f : Semantics.Modality.Kratzer.ModalBase W) (g : Semantics.Modality.Kratzer.OrderingSource W) (w : W) : UpdateSemantics.Default.ExpState W

The expectation state a modal base and ordering source induce at a world: accessible worlds as information, the ordering-source ranking as pattern.

Equations

• Mood.stateAt f g w = { info := Semantics.Modality.Kratzer.accessibleWorlds f w, order := Semantics.Modality.Kratzer.kratzerNormality (g w) }

@[simp]

theorem Mood.stateAt_info {W : Type u_1} (f : Semantics.Modality.Kratzer.ModalBase W) (g : Semantics.Modality.Kratzer.OrderingSource W) (w : W) : (stateAt f g w).info = Semantics.Modality.Kratzer.accessibleWorlds f w

@[simp]

theorem Mood.stateAt_order {W : Type u_1} (f : Semantics.Modality.Kratzer.ModalBase W) (g : Semantics.Modality.Kratzer.OrderingSource W) (w : W) : (stateAt f g w).order = Semantics.Modality.Kratzer.kratzerNormality (g w)

theorem Mood.bestWorlds_eq_optimal {W : Type u_1} (f : Semantics.Modality.Kratzer.ModalBase W) (g : Semantics.Modality.Kratzer.OrderingSource W) (w : W) : Semantics.Modality.Kratzer.bestWorlds f g w = (stateAt f g w).optimal

Kratzer's best worlds are the induced state's optimal worlds.

theorem Mood.simpleNecessity_iff_boxCs {W : Type u_1} (f : Semantics.Modality.Kratzer.ModalBase W) (g : Semantics.Modality.Kratzer.OrderingSource W) (p : W → Prop) (w : W) : Semantics.Modality.Kratzer.simpleNecessity f p w ↔ (stateAt f g w).boxCs p

Simple necessity is informational necessity over the induced state (the ordering source is irrelevant) — [Por18]'s (3a).

theorem Mood.necessity_iff_boxLe {W : Type u_1} (f : Semantics.Modality.Kratzer.ModalBase W) (g : Semantics.Modality.Kratzer.OrderingSource W) (p : W → Prop) (w : W) : Semantics.Modality.Kratzer.necessity f g p w ↔ (stateAt f g w).boxLe p

Kratzer necessity is preferential necessity over the induced state — human necessity as □_≤, [Por18]'s (3b).

theorem Mood.le_assert_iff_simpleNecessity {W : Type u_1} (f : Semantics.Modality.Kratzer.ModalBase W) (g : Semantics.Modality.Kratzer.OrderingSource W) (p : W → Prop) (w : W) : stateAt f g w ≤ (stateAt f g w).assert p ↔ Semantics.Modality.Kratzer.simpleNecessity f p w

Veltman acceptance at a Kratzer state: the induced state supports asserting p iff p is a simple necessity.

theorem Mood.isRealistic_iff_mem_stateAt_info {W : Type u_1} (f : Semantics.Modality.Kratzer.ModalBase W) (g : Semantics.Modality.Kratzer.OrderingSource W) : Semantics.Modality.Kratzer.isRealistic f ↔ ∀ (w : W), w ∈ (stateAt f g w).info

Kratzer realism is fiber-reflexivity: a modal base is realistic iff every world belongs to its own induced information state.