Clause Type: Force × Mood

[Hol16] [Riz97]

A clause type is a pair of independent dimensions:

• Force (IllocutionaryMood): declarative, interrogative, imperative, ...
• Mood (GramMood): indicative, subjunctive

These are orthogonal — [Hol16]'s analysis requires both: a polar question is [interrogative, indicative], while a deliberative subjunctive question is [interrogative, subjunctive].

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)

ClauseType lives in Semantics/Mood/ because the file is intrinsically about the mood-category cross-product. The discourse-act extensions of force (Searle classes, direction of fit, preparatory conditions) live in Discourse/SpeechAct.lean.

structure Semantics.Mood.ClauseType : Type

A clause's type: the independent pairing of illocutionary force with grammatical mood.

• force : IllocutionaryMood

  Illocutionary force: the speech act performed

• mood : GramMood

  Grammatical mood: verb morphology

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

Equations

• Semantics.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 ⋯

@[implicit_reducible]

instance Semantics.Mood.instDecidableEqClauseType : DecidableEq ClauseType

Equations

• Semantics.Mood.instDecidableEqClauseType = Semantics.Mood.instDecidableEqClauseType.decEq

@[implicit_reducible]

instance Semantics.Mood.instReprClauseType : Repr ClauseType

Equations

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

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

Equations

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

def Semantics.Mood.ClauseType.declInd : ClauseType

A standard declarative-indicative clause.

Equations

• Semantics.Mood.ClauseType.declInd = { force := Semantics.Mood.IllocutionaryMood.declarative, mood := Semantics.Mood.GramMood.indicative }

def Semantics.Mood.ClauseType.polarQuestion : ClauseType

A standard polar question (interrogative-indicative).

Equations

• Semantics.Mood.ClauseType.polarQuestion = { force := Semantics.Mood.IllocutionaryMood.interrogative, mood := Semantics.Mood.GramMood.indicative }

theorem Semantics.Mood.force_mood_independent : ClauseType.declInd.mood = ClauseType.polarQuestion.mood ∧ ClauseType.declInd.force ≠ ClauseType.polarQuestion.force

Force and mood are independent: changing one doesn't change the other.

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

Map from ClauseType to epistemic authority (via force, ignoring mood).

Equations

• ct.authority = Semantics.Mood.moodAuthority ct.force

theorem Semantics.Mood.polarQuestion_addressee_authority : ClauseType.polarQuestion.authority = Discourse.DiscourseRole.addressee

Polar questions have addressee authority regardless of mood.

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

Project a UD.Mood feature value to a Semantics.Mood.ClauseType.

UD.Mood is a flat enum that conflates illocutionary force (Imp, Jus, Adm) with grammatical mood (Ind, Sub) with finer irrealis subtypes (Cnd, Opt, Pot, Nec, Irr). The bridge picks the most defensible default cross-product:

UD.Mood	force	mood
Ind	declarative	indicative
Sub	declarative	subjunctive
Imp	imperative	indicative
Cnd	declarative	subjunctive
Opt	declarative	subjunctive
Jus	imperative	subjunctive
Pot	declarative	subjunctive
Qot	declarative	indicative
Adm	exclamative	indicative
Nec	declarative	subjunctive
Irr	declarative	subjunctive

The mapping is non-injective by design — UD.Mood draws finer distinctions on the irrealis side than (force × mood) records.

Equations

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

theorem UD.Mood.Imp_is_imperative : Imp.toClauseType.force = Semantics.Mood.IllocutionaryMood.imperative

The UD Imp mood projects to imperative force.

theorem UD.Mood.Sub_is_subjunctive : Sub.toClauseType.mood = Semantics.Mood.GramMood.subjunctive

The UD Sub mood projects to subjunctive grammatical mood.