Grammatical Mood

Morphological mood categories: indicative vs subjunctive (and subtypes).

This is the verb-morphological distinction, independent of:

• IllocutionaryMood (declarative/interrogative/imperative — speech act force)
• SAPMood (configurational mood from Speas & Tenny's 2×2 matrix)

The two dimensions are orthogonal: a clause can be [interrogative, indicative] ("Does he sleep?") or [interrogative, subjunctive] (Spanish "¿Que duerma?").

See Theories/Semantics/Mood/Basic.lean for the semantic operators (SUBJ, IND) that interpret these categories.

This file lives in Core/Mood/ alongside IllocutionaryMood.lean (force) and ClauseType.lean (force × mood); together they form the unified mood-category namespace Core.Mood. Discourse-act material (Searle classes, direction of fit, preparatory conditions, discourse roles) lives in Core/Discourse/IllocutionaryForce.lean.

inductive Core.Mood.GramMood : Type

Grammatical mood categories.

Following the typological literature:

• Indicative: The default, "realis" mood
• Subjunctive: Non-default, "irrealis" mood (covers many subtypes)

• indicative : GramMood
• subjunctive : GramMood

@[implicit_reducible]

instance Core.Mood.instDecidableEqGramMood : DecidableEq GramMood

Equations

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

def Core.Mood.instReprGramMood.repr : GramMood → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Mood.instReprGramMood : Repr GramMood

Equations

• Core.Mood.instReprGramMood = { reprPrec := Core.Mood.instReprGramMood.repr }

@[implicit_reducible]

instance Core.Mood.instInhabitedGramMood : Inhabited GramMood

Equations

• Core.Mood.instInhabitedGramMood = { default := Core.Mood.instInhabitedGramMood.default }

def Core.Mood.instInhabitedGramMood.default : GramMood

Equations

• Core.Mood.instInhabitedGramMood.default = Core.Mood.GramMood.indicative

inductive Core.Mood.SubjunctiveType : Type

Subjunctive subtypes (for finer-grained analysis).

Different languages grammaticalize different subjunctive functions:

• Counterfactual: contrary-to-fact conditionals
• Dubitative: epistemic uncertainty
• Optative: wishes and desires
• Potential: epistemic/circumstantial possibility

• counterfactual : SubjunctiveType
• dubitative : SubjunctiveType
• optative : SubjunctiveType
• potential : SubjunctiveType
• subordinateFuture : SubjunctiveType

@[implicit_reducible]

instance Core.Mood.instDecidableEqSubjunctiveType : DecidableEq SubjunctiveType

Equations

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

@[implicit_reducible]

instance Core.Mood.instReprSubjunctiveType : Repr SubjunctiveType

Equations

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

def Core.Mood.instReprSubjunctiveType.repr : SubjunctiveType → Nat → Std.Format

Equations

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

structure Core.Mood.MoodEffect : Type

The semantic effects of grammatical mood, connecting two independent dimensions:

• Situation-level (@cite{mendes-2025}): SUBJ introduces a new situation dref; IND retrieves an existing one
• Eventuality-level (@cite{grano-2024}): SBJV leaves the complement's eventuality argument open for abstraction; IND existentially closes it

These dimensions are complementary: situation introduction enables temporal anchoring (SF in Portuguese/Spanish), while eventuality openness enables abstraction over the event argument (required by causatives, intention reports, aspectual predicates, and memory/perception reports).

• introducesSituation : Bool

  SUBJ introduces a new situation dref (@cite{mendes-2025})

• eventualityOpen : Bool

  SBJV leaves the eventuality argument open for abstraction (@cite{grano-2024})

@[implicit_reducible]

instance Core.Mood.instDecidableEqMoodEffect : DecidableEq MoodEffect

Equations

• Core.Mood.instDecidableEqMoodEffect = Core.Mood.instDecidableEqMoodEffect.decEq

def Core.Mood.instDecidableEqMoodEffect.decEq (x✝ x✝¹ : MoodEffect) : Decidable (x✝ = x✝¹)

Equations

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

def Core.Mood.instReprMoodEffect.repr : MoodEffect → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Mood.instReprMoodEffect : Repr MoodEffect

Equations

• Core.Mood.instReprMoodEffect = { reprPrec := Core.Mood.instReprMoodEffect.repr }

def Core.Mood.GramMood.effect : GramMood → MoodEffect

Map grammatical mood to its semantic effects.

Indicative mood does neither: it retrieves an existing situation and existentially closes the eventuality argument.

Subjunctive mood does both: it introduces a new situation dref and leaves the eventuality argument open for abstraction.

Equations

• Core.Mood.GramMood.indicative.effect = { introducesSituation := false, eventualityOpen := false }
• Core.Mood.GramMood.subjunctive.effect = { introducesSituation := true, eventualityOpen := true }

theorem Core.Mood.ind_closes_eventuality : GramMood.indicative.effect.eventualityOpen = false

Indicative mood closes the eventuality argument.

theorem Core.Mood.subj_opens_eventuality : GramMood.subjunctive.effect.eventualityOpen = true

Subjunctive mood leaves the eventuality argument open.

theorem Core.Mood.mood_effects_differ : GramMood.indicative.effect ≠ GramMood.subjunctive.effect

Indicative and subjunctive differ on both dimensions.