Sentential force over a discourse context

import Linglib.Semantics.Mood.Context

Portner's discourse context assigns each participant discourse commitments, a mood state, so a context is a function Role → State W. A sentential force updates one component of the states of some participants: assertion meets the speaker's context set with its content, and directing promotes the content in the addressee's ordering. Each force meets a context with a fixed content. Zanuttini, Pak and Portner's promissive adds its content to the speaker's To-Do List rather than the addressee's, so a promise and a directive with the same content coincide exactly when both participants' orderings already respect the content, so that promoting it changes neither.

Main definitions

Mood.Component.update: the update of one component of a mood state.
Discourse.SpeechAct.Force.target: the component a force updates, Portner's classification of the sentence moods.
Discourse.SpeechAct.Force.holders: the participants whose states a force updates.
Discourse.SpeechAct.Force.update: a force as an update of a discourse context.

Implementation notes

Portner states the updates of assertion and directing and leaves interrogatives open. A question here refines the inquiry of every participant, the question under discussion that the participants share in the discourse contexts of Roberts and of Portner's earlier work.
An exclamation has no component and updates nothing.

References

Portner 2018, Mood
Portner 2004, The Semantics of Imperatives within a Theory of Clause Types
Zanuttini et al. 2012, A Syntactic Analysis of Interpretive Restrictions on Imperative, Promissive, and Exhortative Subjects
Zanuttini & Portner 2003, Exclamative Clauses: At the Syntax-Semantics Interface
Roberts 2012, Information Structure in Discourse: Towards an Integrated Formal Theory of Pragmatics formalized
Gunlogson 2001, True to Form: Rising and Falling Declaratives as Questions in English formalized

Declarations

The update of a component of a mood state with φ: assertion for the context set, promotion for the ordering, and the polar question whether φ for the inquiry.

def Mood.Component.update L58–63

{W : Type u_1} :

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

Mood.Component.informational.update x✝¹ x✝ = x✝¹.assert x✝
Mood.Component.preferential.update x✝¹ x✝ = x✝¹.promote x✝
Mood.Component.inquisitive.update x✝¹ x✝ = x✝¹.inquire (Setoid.polar {w : W | x✝ w})

Used by Mood.Component.update_informational, Mood.Component.update_preferential, Mood.Component.update_inquisitive, Mood.Component.isAdditive_update, Discourse.SpeechAct.Force.update, Discourse.SpeechAct.Force.update_apply_of_mem, Discourse.SpeechAct.Force.foldl_update_apply_of_mem

The component of the mood state a force relates to, Portner's classification of the sentence moods: an assertion relates to the context set and a directive to the ordering. A promise is jussive like a directive, its content added to a To-Do List, and a question relates to the inquiry. An exclamation relates to none: its widening acts on the domain of its wh-operator (Zanuttini & Portner 2003).

def Discourse.SpeechAct.Force.target L87–96

Force → Option Mood.Component

Used by Discourse.SpeechAct.Force.target_eq_none_iff, Discourse.SpeechAct.Force.update, Discourse.SpeechAct.Force.update_apply_of_mem, Discourse.SpeechAct.Force.foldl_update_apply_of_mem

Used in Semantics/Mood/SpeechEvent

L98–99

The participants whose discourse commitments a force updates: the speaker's for an assertion and the addressee's for a directive, as in Portner's definitions of assertion and directing; the speaker's for a promise, whose content is a property of the speaker (Zanuttini et al. 2012, their (49)); every participant's for a question; and none for an exclamation.

def Discourse.SpeechAct.Force.holders L101–110

Force → Finset Role

Used by Discourse.SpeechAct.Force.update, Discourse.SpeechAct.Force.update_apply_of_mem, Discourse.SpeechAct.Force.update_apply_of_notMem, Discourse.SpeechAct.Force.foldl_update_apply_of_mem

Used in Semantics/Mood/SpeechEvent

A force with content φ updates the component it relates to in the state of each of its holders and leaves the other participants' states alone.

def Discourse.SpeechAct.Force.update L112–115

{W : Type u_1} (f : Force) (d : Role → Mood.State W) (φ : W → Prop) :

Role → Mood.State W

f.update d φ r = if r ∈ f.holders then f.target.elim (d r) fun (c : Mood.Component) => c.update (d r) φ else d r

Built from , ,

Used in Semantics/Mood/SpeechEvent, CondoravdiLauer2012

L119–121

L123–125

Every force meets a discourse context with a fixed content, so that for texts of forces the three consequence relations of dynamic semantics coincide (DynamicSemantics.tfae_entails).

theorem Discourse.SpeechAct.Force.isAdditive_update L127–138

{W : Type u_1} (f : Force) (φ : W → Prop) :

DynamicSemantics.IsAdditive fun (x : Role → Mood.State W) => f.update x φ

Built from

A promise and a directive with the same content coincide exactly when both participants' orderings already respect the content, since a promise promotes it for the speaker and a directive for the addressee (Zanuttini et al. 2012, their (49)).

theorem Discourse.SpeechAct.Force.update_promise_eq_directive_iff L166–173

{W : Type u_1} (d : Role → Mood.State W) (φ : W → Prop) :

promise.update d φ = directive.update d φ ↔ ∀ (r : Role), (d r).order ≤ Preorder.ofCriterion φ

Built from

L175–182