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.

inductive Core.Discourse.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

instance Core.Discourse.instDecidableEqGramMood : DecidableEq GramMood

Equations

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

instance Core.Discourse.instReprGramMood : Repr GramMood

Equations

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

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

Equations

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

instance Core.Discourse.instBEqGramMood : BEq GramMood

Equations

• Core.Discourse.instBEqGramMood = { beq := Core.Discourse.instBEqGramMood.beq }

def Core.Discourse.instBEqGramMood.beq : GramMood → GramMood → Bool

Equations

• Core.Discourse.instBEqGramMood.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Core.Discourse.instInhabitedGramMood.default : GramMood

Equations

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

instance Core.Discourse.instInhabitedGramMood : Inhabited GramMood

Equations

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

inductive Core.Discourse.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

instance Core.Discourse.instDecidableEqSubjunctiveType : DecidableEq SubjunctiveType

Equations

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

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

Equations

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

instance Core.Discourse.instReprSubjunctiveType : Repr SubjunctiveType

Equations

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

def Core.Discourse.instBEqSubjunctiveType.beq : SubjunctiveType → SubjunctiveType → Bool

Equations

• Core.Discourse.instBEqSubjunctiveType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Discourse.instBEqSubjunctiveType : BEq SubjunctiveType

Equations

• Core.Discourse.instBEqSubjunctiveType = { beq := Core.Discourse.instBEqSubjunctiveType.beq }

structure Core.Discourse.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})

instance Core.Discourse.instDecidableEqMoodEffect : DecidableEq MoodEffect

Equations

• Core.Discourse.instDecidableEqMoodEffect = Core.Discourse.instDecidableEqMoodEffect.decEq

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

Equations

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

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

Equations

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

instance Core.Discourse.instReprMoodEffect : Repr MoodEffect

Equations

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

instance Core.Discourse.instBEqMoodEffect : BEq MoodEffect

Equations

• Core.Discourse.instBEqMoodEffect = { beq := Core.Discourse.instBEqMoodEffect.beq }

def Core.Discourse.instBEqMoodEffect.beq : MoodEffect → MoodEffect → Bool

Equations

• Core.Discourse.instBEqMoodEffect.beq { introducesSituation := a, eventualityOpen := a_1 } { introducesSituation := b, eventualityOpen := b_1 } = (a == b && a_1 == b_1)
• Core.Discourse.instBEqMoodEffect.beq x✝¹ x✝ = false

def Core.Discourse.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.Discourse.GramMood.indicative.effect = { introducesSituation := false, eventualityOpen := false }
• Core.Discourse.GramMood.subjunctive.effect = { introducesSituation := true, eventualityOpen := true }

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

Indicative mood closes the eventuality argument.

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

Subjunctive mood leaves the eventuality argument open.

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

Indicative and subjunctive differ on both dimensions.