Mood Categories

A clause carries two independent mood dimensions: an illocutionary force (the speech-act type — the F in F(p)) and a grammatical mood (the indicative/subjunctive verb morphology). The dimensions cross freely ([Hol16]): a polar question is [interrogative, indicative], while the Spanish deliberative "¿Que duerma?" is [interrogative, subjunctive]. This file defines the two category enums, their pairing ClauseType, the mood-selection classes of embedding predicates, and the bridge from the UD Mood feature.

Main declarations

• Grammatical, SubjunctiveType — verb-morphological mood.
• Illocutionary, Illocutionary.authority — speech-act force and its epistemic-authority assignment.
• ClauseType — force × mood.
• Selector — mood selection by embedding predicate class.
• Component, HasTarget — [Por18]'s classification: the coordinate of the mood state each category operates on.
• UD.Mood.toClauseType — corpus bridge.

The Searle-class and direction-of-fit API for Illocutionary is in Discourse/SpeechAct.lean.

Grammatical mood

inductive Mood.Grammatical : Type

Grammatical (verb-morphological) mood.

• indicative : Grammatical

  The default, "realis" mood.

• subjunctive : Grammatical

  The non-default, "irrealis" mood.

@[implicit_reducible]

instance Mood.instDecidableEqGrammatical : DecidableEq Grammatical

Equations

• Mood.instDecidableEqGrammatical x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Mood.instReprGrammatical.repr : Grammatical → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Mood.instReprGrammatical.repr Mood.Grammatical.indicative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mood.Grammatical.indicative")).group prec✝

@[implicit_reducible]

instance Mood.instReprGrammatical : Repr Grammatical

Equations

• Mood.instReprGrammatical = { reprPrec := Mood.instReprGrammatical.repr }

@[implicit_reducible]

instance Mood.instInhabitedGrammatical : Inhabited Grammatical

Equations

• Mood.instInhabitedGrammatical = { default := Mood.instInhabitedGrammatical.default }

inductive Mood.SubjunctiveType : Type

The subjunctive functions that individual languages grammaticalize.

• counterfactual : SubjunctiveType

  Contrary-to-fact conditionals.

• dubitative : SubjunctiveType

  Epistemic uncertainty.

• optative : SubjunctiveType

  Wishes and desires.

• potential : SubjunctiveType

  Epistemic or circumstantial possibility.

• subordinateFuture : SubjunctiveType

  [Men25]'s Subordinate Future: present morphology, future reference.

@[implicit_reducible]

instance Mood.instDecidableEqSubjunctiveType : DecidableEq SubjunctiveType

Equations

• Mood.instDecidableEqSubjunctiveType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Mood.instReprSubjunctiveType : Repr SubjunctiveType

Equations

• Mood.instReprSubjunctiveType = { reprPrec := Mood.instReprSubjunctiveType.repr }

def Mood.instReprSubjunctiveType.repr : SubjunctiveType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

Illocutionary force

inductive Mood.Illocutionary : Type

Illocutionary mood: the speech-act force of an utterance — the F in F(p).

• declarative : Illocutionary
• interrogative : Illocutionary
• imperative : Illocutionary
• promissive : Illocutionary
• exclamative : Illocutionary

@[implicit_reducible]

instance Mood.instDecidableEqIllocutionary : DecidableEq Illocutionary

Equations

• Mood.instDecidableEqIllocutionary x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Mood.instReprIllocutionary : Repr Illocutionary

Equations

• Mood.instReprIllocutionary = { reprPrec := Mood.instReprIllocutionary.repr }

def Mood.instReprIllocutionary.repr : Illocutionary → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Mood.instInhabitedIllocutionary : Inhabited Illocutionary

Equations

• Mood.instInhabitedIllocutionary = { default := Mood.instInhabitedIllocutionary.default }

@[implicit_reducible]

instance Mood.instFintypeIllocutionary : Fintype Illocutionary

Equations

• Mood.instFintypeIllocutionary = { elems := { val := ↑Mood.Illocutionary.enumList, nodup := Mood.Illocutionary.enumList_nodup }, complete := Mood.instFintypeIllocutionary._proof_1 }

def Mood.Illocutionary.authority : Illocutionary → Discourse.DiscourseRole

The participant with epistemic authority for each force ([Lak70]): the addressee for interrogatives, the speaker otherwise.

Equations

• Mood.Illocutionary.declarative.authority = Discourse.DiscourseRole.speaker
• Mood.Illocutionary.interrogative.authority = Discourse.DiscourseRole.addressee
• Mood.Illocutionary.imperative.authority = Discourse.DiscourseRole.speaker
• Mood.Illocutionary.promissive.authority = Discourse.DiscourseRole.speaker
• Mood.Illocutionary.exclamative.authority = Discourse.DiscourseRole.speaker

Clause type: force × mood

Force	Mood	Example
declarative	indicative	"John sleeps."
declarative	subjunctive	"Long live the king!"
interrogative	indicative	"Does John sleep?"
interrogative	subjunctive	"¿Que duerma?" (Sp. deliberative)
imperative	—	"Sleep!" (mood often neutralized)

structure Mood.ClauseType : Type

A clause type: the independent pairing of illocutionary force with grammatical mood ([Hol16], [Riz97]).

• force : Illocutionary

  The illocutionary force: the speech act performed.

• mood : Grammatical

  The grammatical mood: verb morphology.

@[implicit_reducible]

instance Mood.instDecidableEqClauseType : DecidableEq ClauseType

Equations

• Mood.instDecidableEqClauseType = Mood.instDecidableEqClauseType.decEq

def Mood.instDecidableEqClauseType.decEq (x✝ x✝¹ : ClauseType) : Decidable (x✝ = x✝¹)

Equations

• Mood.instDecidableEqClauseType.decEq { force := a, mood := a_1 } { force := b, mood := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Mood.instReprClauseType.repr : ClauseType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Mood.instReprClauseType : Repr ClauseType

Equations

• Mood.instReprClauseType = { reprPrec := Mood.instReprClauseType.repr }

def Mood.ClauseType.declInd : ClauseType

A standard declarative-indicative clause.

Equations

• Mood.ClauseType.declInd = { force := Mood.Illocutionary.declarative, mood := Mood.Grammatical.indicative }

def Mood.ClauseType.polarQuestion : ClauseType

A standard polar question (interrogative-indicative).

Equations

• Mood.ClauseType.polarQuestion = { force := Mood.Illocutionary.interrogative, mood := Mood.Grammatical.indicative }

def Mood.ClauseType.authority (ct : ClauseType) : Discourse.DiscourseRole

The epistemic authority of a clause type, via its force.

Equations

• ct.authority = ct.force.authority

Mood components

inductive Mood.Component : Type

The component of the mood state that a mood-bearing object operates on ([Por18], Ch. 4).

• informational : Component

  The information coordinate (State.info).

• preferential : Component

  The ordering coordinate (State.order).

• inquisitive : Component

  The inquiry coordinate (State.inquiry).

@[implicit_reducible]

instance Mood.instDecidableEqComponent : DecidableEq Component

Equations

• Mood.instDecidableEqComponent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Mood.instReprComponent : Repr Component

Equations

• Mood.instReprComponent = { reprPrec := Mood.instReprComponent.repr }

def Mood.instReprComponent.repr : Component → ℕ → Std.Format

Equations

• Mood.instReprComponent.repr Mood.Component.informational prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mood.Component.informational")).group prec✝
• Mood.instReprComponent.repr Mood.Component.preferential prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mood.Component.preferential")).group prec✝
• Mood.instReprComponent.repr Mood.Component.inquisitive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mood.Component.inquisitive")).group prec✝

class Mood.HasTarget (M : Type u_1) : Type u_1

The class of mood-bearing types: target m is the component the context selecting m quantifies over, not an operation m performs.

• target : M → Component

@[implicit_reducible]

instance Mood.instHasTargetIllocutionary : HasTarget Illocutionary

Sentence-mood targets ([Por18], Ch. 3). Promissive and exclamative are linglib extensions; the exclamative assignment conflicts with its null direction of fit (Discourse/SpeechAct.lean) and is a conjectural placeholder.

Equations

• One or more equations did not get rendered due to their size.

Mood selection by predicate class

inductive Mood.Selector : Type

The mood-selection class of an embedding predicate; the projection onto the semantic operators is Selector.toVerbalOp (Semantics/Mood/Verbal.lean).

• indicativeSelecting : Selector

  Indicative-selecting: know, see, believe.

• subjunctiveSelecting : Selector

  Robustly subjunctive-selecting: want, wish, demand, intend.

• crossLinguisticallyVariable : Selector

  Variable across languages: hope, expect ([Gra24], Table 1).

• moodNeutral : Selector

  Pragmatically flexible: say, think.

@[implicit_reducible]

instance Mood.instDecidableEqSelector : DecidableEq Selector

Equations

• Mood.instDecidableEqSelector x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Mood.instReprSelector : Repr Selector

Equations

• Mood.instReprSelector = { reprPrec := Mood.instReprSelector.repr }

def Mood.instReprSelector.repr : Selector → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Mood.instReprSelector.repr Mood.Selector.moodNeutral prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mood.Selector.moodNeutral")).group prec✝

Bridge to UD.Mood

def UD.Mood.toClauseType : Mood → Mood.ClauseType

The default ClauseType for a UD.Mood value. The UD feature is a flat enum conflating force with mood, so the map is a non-injective default cross-product.

Equations

• UD.Mood.Ind.toClauseType = { force := Mood.Illocutionary.declarative, mood := Mood.Grammatical.indicative }
• UD.Mood.Sub.toClauseType = { force := Mood.Illocutionary.declarative, mood := Mood.Grammatical.subjunctive }
• UD.Mood.Imp.toClauseType = { force := Mood.Illocutionary.imperative, mood := Mood.Grammatical.indicative }
• UD.Mood.Cnd.toClauseType = { force := Mood.Illocutionary.declarative, mood := Mood.Grammatical.subjunctive }
• UD.Mood.Opt.toClauseType = { force := Mood.Illocutionary.declarative, mood := Mood.Grammatical.subjunctive }
• UD.Mood.Jus.toClauseType = { force := Mood.Illocutionary.imperative, mood := Mood.Grammatical.subjunctive }
• UD.Mood.Pot.toClauseType = { force := Mood.Illocutionary.declarative, mood := Mood.Grammatical.subjunctive }
• UD.Mood.Qot.toClauseType = { force := Mood.Illocutionary.declarative, mood := Mood.Grammatical.indicative }
• UD.Mood.Adm.toClauseType = { force := Mood.Illocutionary.exclamative, mood := Mood.Grammatical.indicative }
• UD.Mood.Nec.toClauseType = { force := Mood.Illocutionary.declarative, mood := Mood.Grammatical.subjunctive }
• UD.Mood.Irr.toClauseType = { force := Mood.Illocutionary.declarative, mood := Mood.Grammatical.subjunctive }