The mood state

import Linglib.Semantics.Mood.State · namespace Mood

A mood state is Portner's partially ordered set of worlds, a context set with a preorder on worlds, together with a partition of the worlds that records the open question. The first two coordinates form an ordered information state DynamicSemantics.OrderedInformationState, with its updates assert and promote and its modals boxCs and boxLe. For interrogatives Portner (p. 237) offers two options: replace the context set with a partition of it, or add a question set as a third coordinate, as in the discourse contexts of Roberts and of his own earlier work. The mood state takes the second option, with the question set reduced to the meet of its partitions.

Each of the three updates meets one coordinate with a fixed content. The modal boxAns holds of what the open question settles within the context set.

Main definitions

Mood.State: an ordered information state together with an inquiry partition.
Mood.Component, Mood.Component.boxOn: the coordinates of a mood state and their modals, by which Portner classifies the mood-bearing categories.
Mood.State.inquire: the update that refines the inquiry with a question.
Mood.State.boxAns: answerhood, constancy on the inquiry cells within the context set.
Mood.stateAt: the ordered information state that a Kratzer pair induces at a world.

Main statements

Mood.State.boxAns_iff_le_relativeTo: boxAns p holds exactly when the current issue entails the polar question whether p relative to the context set.
Mood.State.isAdditive_assert, Mood.State.isAdditive_promote, Mood.State.isAdditive_inquire: the three updates are additive.
Mood.simpleNecessity_iff_boxCs, Mood.necessity_iff_boxLe: Kratzer's simple and human necessity are the two modals of the induced state, as Portner glosses his (3).

Implementation notes

The ?-update and boxAns are additions of this library; Portner leaves interrogatives open. Mari and Portner's discourse context likewise keeps the question under discussion as a component of its own beside the common ground.
The inquiry is a partition. Questions that are not partitions, such as mention-some questions, live in Question W, into which Question.fromSetoid embeds the partitions.

References

Portner 2018, Mood
Mari & Portner 2021, Mood Variation with Belief Predicates: Modal Comparison and the Raisability of Questions
Veltman 1996, Defaults in Update Semantics formalized
Roberts 1996, Information Structure in Discourse: Towards an Integrated Formal Theory of Pragmatics
Roberts 2012, Information Structure in Discourse: Towards an Integrated Formal Theory of Pragmatics formalized
Portner 2004, The Semantics of Imperatives within a Theory of Clause Types
Groenendijk & Stokhof 1984, Studies on the Semantics of Questions and the Pragmatics of Answers formalized
Kratzer 1981, The Notional Category of Modality formalized

Declarations

A mood state is an ordered information state together with an inquiry partition, the open question, where ⊤ is no question.

structure State L72–77

(W : Type u_1) extends DynamicSemantics.OrderedInformationState W :

Type u_1

info : Set W
order : Preorder W
inquiry : Setoid W
Two worlds are related when they answer the open question alike.

Used by State.ofOrderedInformationState, State.assert, State.promote, State.inquire, State.assert_toOrderedInformationState, State.assert_inquiry, State.promote_toOrderedInformationState, State.promote_inquiry, State.inquire_toOrderedInformationState, State.inquire_inquiry, State.assert_promote_comm, State.assert_inquire_comm, State.promote_inquire_comm, State.inquire_inquire_self, State.promote_eq_self_iff, State.foldl_assert_toOrderedInformationState, State.foldl_promote_toOrderedInformationState, State.instLE, State.instLT, State.instMax, State.instMin, State.instSupSet, State.instInfSet, State.instTop, State.instBot, State.instCompleteLattice, State.le_iff, State.isAdditive_assert, State.isAdditive_promote, State.isAdditive_inquire, State.le_inquire_iff, State.semiconj_assert, State.semiconj_inquire, State.boxAns, State.boxAns_iff_le_relativeTo, State.boxAns_of_decides, State.boxAns_iff_decides, State.boxAns_anti, State.boxAns_not, State.boxAns_and, State.boxAns_or, State.boxAns_imp, State.sepInquiry, State.boxAns_not_reducible_to_boxCs, Component.boxOn, boxOn_informational, boxOn_preferential, boxOn_inquisitive

Used in Semantics/Mood/Context, Semantics/Mood/SpeechEvent, Semantics/Mood/Verbal, CondoravdiLauer2012, PortnerRubinstein2020

L83–85

L87–89

L91–92

Updates

Assertion eliminates the worlds outside p from the context set.

def State.assert L96–98

{W : Type u_1} (c : State W) (p : W → Prop) :

State W

c.assert p = { toOrderedInformationState := c.assert p, inquiry := c.inquiry }

Built from

Used by State.assert_toOrderedInformationState, State.assert_inquiry, State.assert_promote_comm, State.assert_inquire_comm, State.foldl_assert_toOrderedInformationState, State.isAdditive_assert, State.semiconj_assert

Used in Semantics/Mood/Context, Semantics/Mood/SpeechEvent

Promotion refines the ordering with p.

def State.promote L100–102

{W : Type u_1} (c : State W) (p : W → Prop) :

State W

c.promote p = { toOrderedInformationState := c.promote p, inquiry := c.inquiry }

Built from

Used by State.promote_toOrderedInformationState, State.promote_inquiry, State.assert_promote_comm, State.promote_inquire_comm, State.promote_eq_self_iff, State.foldl_promote_toOrderedInformationState, State.isAdditive_promote

Used in Semantics/Mood/Context, Semantics/Mood/SpeechEvent

The ?-update refines the inquiry with the question q.

def State.inquire L104–106

{W : Type u_1} (c : State W) (q : Setoid W) :

State W

c.inquire q = { toOrderedInformationState := c.toOrderedInformationState, inquiry := c.inquiry ⊓ q }

Built from

Used by State.inquire_toOrderedInformationState, State.inquire_inquiry, State.assert_inquire_comm, State.promote_inquire_comm, State.inquire_inquire_self, State.isAdditive_inquire, State.le_inquire_iff, State.semiconj_inquire

Used in Semantics/Mood/Context

Order

Mood states are ordered componentwise, a more constrained state lying below a less constrained one. They form a complete lattice, the product of the lattice of ordered information states and the lattice of partitions, whose top is the state with no information, no expectations and no question.

theorem State.isAdditive_assert L193–195

{W : Type u_1} (p : W → Prop) :

DynamicSemantics.IsAdditive fun (x : State W) => x.assert p

Built from ,

theorem State.isAdditive_promote L197–199

{W : Type u_1} (p : W → Prop) :

DynamicSemantics.IsAdditive fun (x : State W) => x.promote p

Built from ,

theorem State.isAdditive_inquire L201–202

{W : Type u_1} (q : Setoid W) :

DynamicSemantics.IsAdditive fun (x : State W) => x.inquire q

Built from ,

L204–206

Discourse projections

L210–216

L218–223

Answerhood

The propositions a state settles are closed under the Boolean connectives.

Answerhood holds of p when p is constant on the part of each inquiry cell inside the context set. Unlike boxCs and boxLe it is not upward monotone in p.

def State.boxAns L227–230

{W : Type u_1} (c : State W) (p : W → Prop) :

Prop

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

Built from

Used by State.boxAns_iff_le_relativeTo, State.boxAns_of_decides, State.boxAns_iff_decides, State.boxAns_anti, State.boxAns_not, State.boxAns_and, State.boxAns_or, State.boxAns_imp, State.boxAns_not_reducible_to_boxCs, Component.boxOn, boxOn_inquisitive

A state settles p exactly when its issue entails the polar question whether p relative to the context set.

theorem State.boxAns_iff_le_relativeTo L232–252

{W : Type u_1} (c : State W) (p : W → Prop) :

c.boxAns p ↔ Question.fromSetoid c.inquiry ≤ (Question.polar {w : W | p w}).relativeTo c.info

Built from ,

Answerhood is not informational necessity

L286–290

L292–293

L295–298

Components

A coordinate of the mood state. Portner classifies a mood-bearing category by the coordinate that the context selecting it quantifies over: the indicative and the declarative relate to the context set, the subjunctive and the imperative to the ordering.

inductive Component L304–314

Type

informational : Component
The context set, State.info.
preferential : Component
The ordering, State.order.
inquisitive : Component
The inquiry, State.inquiry.

Derives DecidableEq, Repr, Fintype.

Used by Component.boxOn

Used in Semantics/Mood/Context, Semantics/Mood/SpeechEvent, Semantics/Mood/Verbal, PortnerRubinstein2020

The necessity modal of a component is boxCs, boxLe or boxAns.

def Component.boxOn L318–322

{W : Type u_1} :

Component → State W → (W → Prop) → Prop

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

Built from , ,

Used by boxOn_informational, boxOn_preferential, boxOn_inquisitive

Used in Semantics/Mood/SpeechEvent, Semantics/Mood/Verbal

L324–325

L327–328

L330–331

Kratzer backgrounds induce states

Portner glosses his (3): read as a modal base and an ordering source, the two coordinates make boxCs simple necessity and boxLe human necessity. Read the other way, a Kratzer pair is a world-indexed family of ordered information states.

The ordered information state that a modal base and an ordering source induce at a world.

def stateAt L343–345