Verbal Mood as POSWQ Component Selection

@cite{portner-2018} @cite{groenendijk-stokhof-1984}

Verbal mood — the indicative/subjunctive contrast visible in the complement clauses of attitude verbs (Romance, Greek, Balkan, …) — reduces, on @cite{portner-2018}'s account, to which component of the embedding attitude's POSW the mood operator quantifies over. We extend that account to a third operator targeting the inquiry component for question-embedding predicates.

@cite{portner-2018} (Ch. 2) identifies two main intuitions about what distinguishes indicative from subjunctive complementation:

• Truth intuition (Farkas 1985, Portner 1997 tradition): indicative is selected for clauses true throughout a designated modal base. Subjunctive is selected when this universal-truth pattern fails.
• Comparison intuition (Giorgi & Pianesi 1997 tradition): subjunctive is selected when the embedding predicate involves ordering or comparison among alternatives — preference, doxastic ranking, intention.

@cite{portner-2018}'s unification of these two: both intuitions are correct because they target two different POSW components. The information component (cs) underwrites Truth-style universal quantification (POSW.boxCs); the preference component (le) underwrites Comparison-style quantification over the best-ranked subset (POSW.boxLe).

We add a third operator .interrogative for question-embedding predicates (wonder, ask, investigate), which select for clauses settled by the open question — clauses with constant truth value within each cell of the inquiry partition (POSWQ.boxAns, @cite{groenendijk-stokhof-1984} answerhood). Question embedding is not part of @cite{portner-2018}'s verbal-mood unification proper, which is restricted to declarative complementation; we plug it into the same POSWQ substrate to give all three operators a uniform type.

This file formalizes the selection as the interp function on a three-element VerbalMoodOp, with signature POSWQ W → (W → Prop) → Prop. The split is type-driven: boxCs, boxLe, and boxAns operate on the same POSWQ and the same proposition; only which component they consult differs.

Connection to sentence mood

The sentence-mood / discourse-update side of the same unification lives in Core/Discourse/Scoreboard.lean:

layer	declarative	imperative	interrogative
sentence mood	assertion (+-update on cs)	direction (⋆-update on le)	interrogation (? on inq)
modal necessity	boxCs (informational)	boxLe (preferential)	boxAns (answerhood)
verbal mood	interp .indicative	interp .subjunctive	interp .interrogative

The first two columns are @cite{portner-2018}'s; the third column is this library's extension (see Core/Mood/POSWQ.lean). The shared substrate is POSWQ. Verbal mood is the modal row read as a complementizer-domain selector triggered by lexical class of the matrix predicate (MoodSelector for declarative-embedders; QuestionEmbedder for question-embedders).

inductive Semantics.Mood.VerbalMoodOp : Type

The three verbal-mood operators on POSWQ. The .indicative and .subjunctive cases are @cite{portner-2018}'s; .interrogative is our extension to question-embedding predicates. The crossLinguistic and neutral cases of MoodSelector (Mood/Basic.lean) project to none via MoodSelector.toVerbalMood because their selection pattern is not committed to a single POSWQ component by lexical class alone.

• indicative : VerbalMoodOp

  Indicative: universal quantification over the informational component of the embedding POSWQ. The Truth intuition.

• subjunctive : VerbalMoodOp

  Subjunctive: universal quantification over the preferential component (best-ranked subset). The Comparison intuition.

• interrogative : VerbalMoodOp

  Interrogative: answerhood with respect to the inquiry component (constant truth value per cell), à la @cite{groenendijk-stokhof-1984}. Selected by question-embedding predicates (wonder, ask, investigate). Our extension — not part of @cite{portner-2018}'s verbal-mood unification.

@[implicit_reducible]

instance Semantics.Mood.instDecidableEqVerbalMoodOp : DecidableEq VerbalMoodOp

Equations

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

def Semantics.Mood.instReprVerbalMoodOp.repr : VerbalMoodOp → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Mood.instReprVerbalMoodOp : Repr VerbalMoodOp

Equations

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

def Semantics.Mood.VerbalMoodOp.interp {W : Type u} : VerbalMoodOp → Core.Mood.POSWQ W → (W → Prop) → Prop

Compositional interpretation of a verbal-mood operator against an embedding POSWQ and an embedded proposition. The three cases consult disjoint POSWQ components: .indicative ↦ POSW.boxCs, .subjunctive ↦ POSW.boxLe, .interrogative ↦ POSWQ.boxAns.

Equations

• Semantics.Mood.VerbalMoodOp.indicative.interp x✝¹ x✝ = x✝¹.boxCs x✝
• Semantics.Mood.VerbalMoodOp.subjunctive.interp x✝¹ x✝ = x✝¹.boxLe x✝
• Semantics.Mood.VerbalMoodOp.interrogative.interp x✝¹ x✝ = x✝¹.boxAns x✝

§1. Definitional equalities

@[simp]

theorem Semantics.Mood.interp_indicative {W : Type u} (c : Core.Mood.POSWQ W) (p : W → Prop) : VerbalMoodOp.indicative.interp c p = c.boxCs p

@[simp]

theorem Semantics.Mood.interp_subjunctive {W : Type u} (c : Core.Mood.POSWQ W) (p : W → Prop) : VerbalMoodOp.subjunctive.interp c p = c.boxLe p

@[simp]

theorem Semantics.Mood.interp_interrogative {W : Type u} (c : Core.Mood.POSWQ W) (p : W → Prop) : VerbalMoodOp.interrogative.interp c p = c.boxAns p

§2. Operator-specific monotonicity

boxCs and boxLe are upward-monotone in the embedded proposition: strengthening the modal base preserves universal truth there. boxAns is not upward-monotone — a strengthening of p can break the constant-truth-per-cell property. The natural monotonicity for boxAns is anti-monotone in the inquiry partition (covered by POSWQ.boxAns_anti).

This asymmetry is itself a content claim of @cite{portner-2018}'s unification: the three operators have different natural ordering behaviors precisely because they consult different POSWQ components, which carry different lattice structures.

theorem Semantics.Mood.interp_indicative_mono {W : Type u} (c : Core.Mood.POSWQ W) (p q : W → Prop) (h : ∀ (w : W), p w → q w) : VerbalMoodOp.indicative.interp c p → VerbalMoodOp.indicative.interp c q

theorem Semantics.Mood.interp_subjunctive_mono {W : Type u} (c : Core.Mood.POSWQ W) (p q : W → Prop) (h : ∀ (w : W), p w → q w) : VerbalMoodOp.subjunctive.interp c p → VerbalMoodOp.subjunctive.interp c q

§3. Distinctness witnesses

The three mood operators are pairwise non-equivalent — each consults a disjoint POSWQ component. We exhibit concrete witnesses showing that no operator can be defined in terms of the others on the POSWQ substrate alone.

def Semantics.Mood.sepPOSW : Core.Mood.POSW Bool

Separation POSW: cs = ⊤ over Bool, with le w v = (w = false → v = false). Under this ordering false is the unique element w such that every v satisfies le v w, so false is the unique world picked out by POSW.best.

Equations

• Semantics.Mood.sepPOSW = { cs := fun (x : Bool) => True, le := fun (w v : Bool) => w = false → v = false, le_refl := ⋯, le_trans := Semantics.Mood.sepPOSW._proof_1 }

def Semantics.Mood.sepPOSWQ_triv : Core.Mood.POSWQ Bool

Lift of sepPOSW to a POSWQ with trivial inquiry. Used to distinguish indicative from subjunctive without engaging the inquiry component.

Equations

• Semantics.Mood.sepPOSWQ_triv = Core.Mood.POSWQ.ofPOSW Semantics.Mood.sepPOSW

def Semantics.Mood.sepProp : Bool → Prop

Separation proposition: only false satisfies it.

Equations

• Semantics.Mood.sepProp w = (w = false)

theorem Semantics.Mood.subjunctive_accepts_separation : VerbalMoodOp.subjunctive.interp sepPOSWQ_triv sepProp

The subjunctive operator accepts (sepPOSWQ_triv, sepProp).

theorem Semantics.Mood.indicative_rejects_separation : ¬VerbalMoodOp.indicative.interp sepPOSWQ_triv sepProp

The indicative operator rejects (sepPOSWQ_triv, sepProp).

theorem Semantics.Mood.indicative_ne_subjunctive : ∃ (c : Core.Mood.POSWQ Bool) (p : Bool → Prop), VerbalMoodOp.subjunctive.interp c p ∧ ¬VerbalMoodOp.indicative.interp c p

Indicative ≠ subjunctive. The two mood operators are distinguishable: there exists a POSWQ and a proposition on which they disagree. The Truth/Comparison split is genuine, not a notational variant.

theorem Semantics.Mood.interrogative_ne_indicative : ∃ (c : Core.Mood.POSWQ Bool) (p : Bool → Prop), VerbalMoodOp.interrogative.interp c p ∧ ¬VerbalMoodOp.indicative.interp c p

Interrogative ≠ indicative. Reuses the witness from POSWQ.boxAns_not_reducible_to_boxCs: a POSWQ where the inquiry component partitions worlds finely enough that some p has constant truth value per cell (so boxAns p) yet fails to be universally true on cs (so not boxCs p).

§4. Operational POSWTarget projection

Each verbal-mood operator selects exactly one POSWQ component. That selection is the HasPOSWTarget instance below, packaged as the same typeclass that GramMood and IllocutionaryMood use in Core/Mood/POSWTarget.lean. With this in hand, interp factors as boxOn ∘ target — the verbal mood's interpretation is exactly "run the target component's necessity modal on the embedded proposition".

@[implicit_reducible]

instance Semantics.Mood.instHasPOSWTargetVerbalMoodOp : Core.Mood.HasPOSWTarget VerbalMoodOp

Equations

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

@[simp]

theorem Semantics.Mood.target_indicative : Core.Mood.target VerbalMoodOp.indicative = Core.Mood.POSWTarget.informational

@[simp]

theorem Semantics.Mood.target_subjunctive : Core.Mood.target VerbalMoodOp.subjunctive = Core.Mood.POSWTarget.preferential

@[simp]

theorem Semantics.Mood.target_interrogative : Core.Mood.target VerbalMoodOp.interrogative = Core.Mood.POSWTarget.partition

@[simp]

theorem Semantics.Mood.interp_eq_target_boxOn {W : Type u} (m : VerbalMoodOp) (c : Core.Mood.POSWQ W) (p : W → Prop) : m.interp c p = (Core.Mood.target m).boxOn c p

Operational factoring: the verbal-mood interpretation is exactly the necessity modal selected by the operator's POSW target. Says that target is not just a typological label — it determines interp definitionally.

Verbal-mood biconditional characterization

VerbalMoodOp is in bijection with POSWTarget: each operator exactly picks out one POSW component, and conversely each component is targeted by exactly one operator. The biconditionals below are the type-level shadow of @cite{portner-2018}'s Indicative / Subjunctive Principles extended to interrogative — at the verbal-mood layer, mood selection and POSWQ-component selection are the same thing.

theorem Semantics.Mood.verbal_mood_target_informational_iff_indicative (m : VerbalMoodOp) : Core.Mood.target m = Core.Mood.POSWTarget.informational ↔ m = VerbalMoodOp.indicative

theorem Semantics.Mood.verbal_mood_target_preferential_iff_subjunctive (m : VerbalMoodOp) : Core.Mood.target m = Core.Mood.POSWTarget.preferential ↔ m = VerbalMoodOp.subjunctive

theorem Semantics.Mood.verbal_mood_target_partition_iff_interrogative (m : VerbalMoodOp) : Core.Mood.target m = Core.Mood.POSWTarget.partition ↔ m = VerbalMoodOp.interrogative

§5. Bridge to MoodSelector

The MoodSelector enum (Mood/Basic.lean, taxonomic by predicate class — knowledge/belief, preference/desire, etc.) projects onto VerbalMoodOp for the predicate classes that select the same mood across @cite{portner-2018}'s indicative/subjunctive languages. Cross-linguistically variable selectors and mood-neutral predicates project to none — they are not committed to either quantification scheme by lexical-class membership alone.

Question-embedding predicates (wonder, ask, investigate) are a different lexical dimension — they're question-embedders, not mood-selectors-on-declarative-complements — and so are not in MoodSelector's scope. The .interrogative operator is reachable by direct construction; a future predicate-class enum specific to question-embedders can project into it.

def Semantics.Mood.MoodSelector.toVerbalMood : MoodSelector → Option VerbalMoodOp

Project a MoodSelector to its VerbalMoodOp, when the lexical class is committed to a single mood cross-linguistically. MoodSelector covers declarative-complement-taking predicates; question-embedders project to .interrogative via a separate dimension.

Equations

• Semantics.Mood.MoodSelector.indicativeSelecting.toVerbalMood = some Semantics.Mood.VerbalMoodOp.indicative
• Semantics.Mood.MoodSelector.subjunctiveSelecting.toVerbalMood = some Semantics.Mood.VerbalMoodOp.subjunctive
• Semantics.Mood.MoodSelector.crossLinguisticallyVariable.toVerbalMood = none
• Semantics.Mood.MoodSelector.moodNeutral.toVerbalMood = none

theorem Semantics.Mood.prefersSubjunctive_eq_subjunctive (m : MoodSelector) : prefersSubjunctive m = true ↔ m.toVerbalMood = some VerbalMoodOp.subjunctive

The prefersSubjunctive boolean (Mood/Basic.lean) and the toVerbalMood projection agree on whether the result is the subjunctive operator. Two surface representations of the same lexical-class commitment, equivalent by construction.

theorem Semantics.Mood.toVerbalMood_ne_interrogative (m : MoodSelector) : m.toVerbalMood ≠ some VerbalMoodOp.interrogative

MoodSelector.toVerbalMood never projects to .interrogative: the declarative-complement classification is closed under the indicative/subjunctive split. Question-embedding lives elsewhere — see QuestionEmbedder below.

§6. Bridge to QuestionEmbedder

MoodSelector covers declarative-complement-taking predicates only; its toVerbalMood projection cannot land in .interrogative (toVerbalMood_ne_interrogative above). The dual lexical class — question-embedding predicates like wonder, ask, know-Q, investigate — gets its own enum here, with the inverse projection property: every QuestionEmbedder projects to .interrogative, never to .indicative or .subjunctive.

The factive/non-factive split (Karttunen 1977 tradition) is the standard subdivision of question embedders; we record it for future expansion (e.g., a finer projection that distinguishes factive-Q embedders' presupposition profile) without committing to particular semantic consequences here.

inductive Semantics.Mood.QuestionEmbedder : Type

Question-embedding predicate class. Disjoint from MoodSelector, which covers only declarative-complement embedders. The factive/non-factive split follows Karttunen's typology.

• factive : QuestionEmbedder

  Factive question-embedders: know-Q, discover-Q, realize-Q.

• nonfactive : QuestionEmbedder

  Non-factive question-embedders: wonder, ask, investigate.

@[implicit_reducible]

instance Semantics.Mood.instDecidableEqQuestionEmbedder : DecidableEq QuestionEmbedder

Equations

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

@[implicit_reducible]

instance Semantics.Mood.instReprQuestionEmbedder : Repr QuestionEmbedder

Equations

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

def Semantics.Mood.instReprQuestionEmbedder.repr : QuestionEmbedder → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Mood.instInhabitedQuestionEmbedder : Inhabited QuestionEmbedder

Equations

• Semantics.Mood.instInhabitedQuestionEmbedder = { default := Semantics.Mood.instInhabitedQuestionEmbedder.default }

def Semantics.Mood.instInhabitedQuestionEmbedder.default : QuestionEmbedder

Equations

• Semantics.Mood.instInhabitedQuestionEmbedder.default = Semantics.Mood.QuestionEmbedder.factive

def Semantics.Mood.QuestionEmbedder.toVerbalMood : QuestionEmbedder → VerbalMoodOp

Every QuestionEmbedder projects to the interrogative verbal-mood operator. The dual of MoodSelector.toVerbalMood: where MoodSelector ranges over the indicative/subjunctive split, QuestionEmbedder ranges over the inquiry-component column.

Equations

• x✝.toVerbalMood = Semantics.Mood.VerbalMoodOp.interrogative

@[simp]

theorem Semantics.Mood.QuestionEmbedder.toVerbalMood_eq (q : QuestionEmbedder) : q.toVerbalMood = VerbalMoodOp.interrogative

theorem Semantics.Mood.QuestionEmbedder.toVerbalMood_target (q : QuestionEmbedder) : Core.Mood.target q.toVerbalMood = Core.Mood.POSWTarget.partition

QuestionEmbedder.toVerbalMood always lands in .interrogative — the inverse of toVerbalMood_ne_interrogative for MoodSelector. Together these say: the indicative/subjunctive column and the interrogative column are reached by disjoint lexical-class enums, with no overlap and no gap.