Documentation

Linglib.Semantics.Mood.IllocutionaryMood

Illocutionary Mood — the Speech-Act Force Category #

The category of speech-act force a clause is associated with: declarative, interrogative, imperative, promissive, exclamative. This is the F in F(p).

Distinct from:

Semantics.Mood.GramMood (indicative/subjunctive morphology — see Basic.lean)
SpeasTenny2003.SAPMood (Speas & Tenny's 2×2 configuration)

The pair (IllocutionaryMood, GramMood) is Semantics.Mood.ClauseType.

This file contains only the category — the enum + its sole intrinsic property moodAuthority (which participant has epistemic authority). The act-side extensions (Searle classes, direction of fit, preparatory conditions) live in Discourse/SpeechAct.lean, which imports this file. The split keeps Semantics/Mood/ framework-agnostic and free of pragmatic-act commitments.

The DiscourseRole type lives in Discourse/Roles.lean because it is about discourse participants (speaker/addressee), not about mood.

inductive Semantics.Mood.IllocutionaryMood :

Illocutionary mood — the speech-act force of an utterance.

Distinct from GramMood (indicative/subjunctive morphology) and the Minimalist SAPMood (configurational). This classifies the pragmatic act performed — the F in F(p).

declarative : IllocutionaryMood
interrogative : IllocutionaryMood
imperative : IllocutionaryMood
promissive : IllocutionaryMood
exclamative : IllocutionaryMood

Instances For

@[implicit_reducible]

instance Semantics.Mood.instDecidableEqIllocutionaryMood :

DecidableEq IllocutionaryMood

Equations

Semantics.Mood.instDecidableEqIllocutionaryMood x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Mood.instReprIllocutionaryMood.repr :

IllocutionaryMood → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Semantics.Mood.instReprIllocutionaryMood :

Repr IllocutionaryMood

Equations

Semantics.Mood.instReprIllocutionaryMood = { reprPrec := Semantics.Mood.instReprIllocutionaryMood.repr }

@[implicit_reducible]

instance Semantics.Mood.instInhabitedIllocutionaryMood :

Inhabited IllocutionaryMood

Equations

Semantics.Mood.instInhabitedIllocutionaryMood = { default := Semantics.Mood.instInhabitedIllocutionaryMood.default }

@[implicit_reducible]

instance Semantics.Mood.instFintypeIllocutionaryMood :

Fintype IllocutionaryMood

Equations

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

def Semantics.Mood.moodAuthority :

IllocutionaryMood → Discourse.DiscourseRole

Which participant holds epistemic authority for a given illocutionary mood.

[Lak70]: in declaratives, imperatives, and promissives the speaker is the seat of knowledge; in interrogatives the addressee is.

Equations

Instances For