Grano 2024: Intention Reports and Eventuality Abstraction @cite{grano-2024}

Cross-linguistic mood choice data and bridge theorems connecting @cite{grano-2024}'s analysis of intention reports to the mood and attitude infrastructure.

Core Proposal (three premises → conclusion)

1. Premise 1: Intention reports encode causally self-referential content (@cite{searle-1983}; Harman 1976)
2. Premise 2: Encoding causal self-reference requires abstraction over the complement clause's eventuality argument (CAUSE* binds it)
3. Premise 3: Only subjunctive and nonfinite clauses enable eventuality abstraction; indicative clauses existentially close the event argument
4. Conclusion: 'intend' accepts subjunctive/nonfinite but rejects indicative complements cross-linguistically

Table 1: Cross-Linguistic Mood Choice

The central empirical finding: 'intend' patterns with 'want' (not 'hope') in robustly rejecting indicative complements. 'hope' exhibits cross-linguistic and language-internal variation; 'intend' does not.

Independent support comes from causative predicates ('make'), intention-rigid predicates ('aim', 'try'), belief–intention hybrid predicates ('decide', 'convince'), aspectual predicates ('begin'), and memory/perception reports ('remember', 'see'). All pattern alike: subjunctive/nonfinite required, indicative rejected.

Unified Theory (§7)

Subjunctive mood uniformly signals a departure from the default clausal semantics of unembedded assertions. Two kinds of departure:

• Comparison (ordering semantics): 'want', 'hope' (@cite{portner-rubinstein-2020})
• Eventuality abstraction: 'intend', causatives, aspectuals (this paper)

When neither departure is present, only indicative mood is possible.

structure Phenomena.Complementation.Studies.Grano2024.MoodChoiceDatum : Type

A mood choice observation: whether a predicate in a language rejects indicative complements (@cite{grano-2024}, Table 1).

This is the key variable: 'want' and 'intend' robustly reject IND across languages, while 'hope' does not.

• language : String
• predicate : String
• rejectsIndicative : Bool

def Phenomena.Complementation.Studies.Grano2024.instDecidableEqMoodChoiceDatum.decEq (x✝ x✝¹ : MoodChoiceDatum) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Complementation.Studies.Grano2024.instDecidableEqMoodChoiceDatum : DecidableEq MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.instDecidableEqMoodChoiceDatum = Phenomena.Complementation.Studies.Grano2024.instDecidableEqMoodChoiceDatum.decEq

def Phenomena.Complementation.Studies.Grano2024.instBEqMoodChoiceDatum.beq : MoodChoiceDatum → MoodChoiceDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Complementation.Studies.Grano2024.instBEqMoodChoiceDatum.beq x✝¹ x✝ = false

instance Phenomena.Complementation.Studies.Grano2024.instBEqMoodChoiceDatum : BEq MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.instBEqMoodChoiceDatum = { beq := Phenomena.Complementation.Studies.Grano2024.instBEqMoodChoiceDatum.beq }

instance Phenomena.Complementation.Studies.Grano2024.instReprMoodChoiceDatum : Repr MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.instReprMoodChoiceDatum = { reprPrec := Phenomena.Complementation.Studies.Grano2024.instReprMoodChoiceDatum.repr }

def Phenomena.Complementation.Studies.Grano2024.instReprMoodChoiceDatum.repr : MoodChoiceDatum → ℕ → Std.Format

Equations

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

def Phenomena.Complementation.Studies.Grano2024.spanish_want : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.spanish_want = { language := "Spanish", predicate := "querer", rejectsIndicative := true }

def Phenomena.Complementation.Studies.Grano2024.french_want : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.french_want = { language := "French", predicate := "vouloir", rejectsIndicative := true }

def Phenomena.Complementation.Studies.Grano2024.portuguese_want : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.portuguese_want = { language := "Portuguese", predicate := "querer", rejectsIndicative := true }

def Phenomena.Complementation.Studies.Grano2024.italian_want : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.italian_want = { language := "Italian", predicate := "volere", rejectsIndicative := true }

def Phenomena.Complementation.Studies.Grano2024.greek_want : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.greek_want = { language := "Greek", predicate := "thélo", rejectsIndicative := true }

def Phenomena.Complementation.Studies.Grano2024.romanian_want : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.romanian_want = { language := "Romanian", predicate := "a vrea", rejectsIndicative := true }

def Phenomena.Complementation.Studies.Grano2024.english_want : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.english_want = { language := "English", predicate := "want", rejectsIndicative := true }

def Phenomena.Complementation.Studies.Grano2024.spanish_hope : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.spanish_hope = { language := "Spanish", predicate := "esperar", rejectsIndicative := true }

def Phenomena.Complementation.Studies.Grano2024.french_hope : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.french_hope = { language := "French", predicate := "espérer", rejectsIndicative := false }

def Phenomena.Complementation.Studies.Grano2024.portuguese_hope : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.portuguese_hope = { language := "Portuguese", predicate := "esperar", rejectsIndicative := false }

def Phenomena.Complementation.Studies.Grano2024.italian_hope : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.italian_hope = { language := "Italian", predicate := "sperare", rejectsIndicative := false }

def Phenomena.Complementation.Studies.Grano2024.greek_hope : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.greek_hope = { language := "Greek", predicate := "elpízo", rejectsIndicative := false }

def Phenomena.Complementation.Studies.Grano2024.romanian_hope : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.romanian_hope = { language := "Romanian", predicate := "a spera", rejectsIndicative := false }

def Phenomena.Complementation.Studies.Grano2024.english_hope : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.english_hope = { language := "English", predicate := "hope", rejectsIndicative := false }

def Phenomena.Complementation.Studies.Grano2024.spanish_intend : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.spanish_intend = { language := "Spanish", predicate := "tener la intención", rejectsIndicative := true }

def Phenomena.Complementation.Studies.Grano2024.portuguese_intend : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.portuguese_intend = { language := "Portuguese", predicate := "pretender", rejectsIndicative := true }

def Phenomena.Complementation.Studies.Grano2024.greek_intend : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.greek_intend = { language := "Greek", predicate := "protíthete", rejectsIndicative := true }

def Phenomena.Complementation.Studies.Grano2024.romanian_intend : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.romanian_intend = { language := "Romanian", predicate := "a intenționa", rejectsIndicative := true }

def Phenomena.Complementation.Studies.Grano2024.english_intend : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.english_intend = { language := "English", predicate := "intend", rejectsIndicative := true }

def Phenomena.Complementation.Studies.Grano2024.spanish_make : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.spanish_make = { language := "Spanish", predicate := "hacer", rejectsIndicative := true }

def Phenomena.Complementation.Studies.Grano2024.french_make : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.french_make = { language := "French", predicate := "faire", rejectsIndicative := true }

def Phenomena.Complementation.Studies.Grano2024.portuguese_make : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.portuguese_make = { language := "Portuguese", predicate := "fazer", rejectsIndicative := true }

def Phenomena.Complementation.Studies.Grano2024.italian_make : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.italian_make = { language := "Italian", predicate := "fare", rejectsIndicative := true }

def Phenomena.Complementation.Studies.Grano2024.greek_make : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.greek_make = { language := "Greek", predicate := "vázo", rejectsIndicative := true }

def Phenomena.Complementation.Studies.Grano2024.romanian_make : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.romanian_make = { language := "Romanian", predicate := "a face", rejectsIndicative := true }

def Phenomena.Complementation.Studies.Grano2024.english_make : MoodChoiceDatum

Equations

• Phenomena.Complementation.Studies.Grano2024.english_make = { language := "English", predicate := "make", rejectsIndicative := true }

def Phenomena.Complementation.Studies.Grano2024.wantData : List MoodChoiceDatum

Equations

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

def Phenomena.Complementation.Studies.Grano2024.hopeData : List MoodChoiceDatum

Equations

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

def Phenomena.Complementation.Studies.Grano2024.intendData : List MoodChoiceDatum

Equations

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

def Phenomena.Complementation.Studies.Grano2024.causativeData : List MoodChoiceDatum

Equations

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

theorem Phenomena.Complementation.Studies.Grano2024.want_robustly_rejects_ind : (wantData.all fun (x : MoodChoiceDatum) => x.rejectsIndicative) = true

'want' robustly rejects indicative across all 7 languages.

theorem Phenomena.Complementation.Studies.Grano2024.hope_does_not_robustly_reject_ind : (hopeData.all fun (x : MoodChoiceDatum) => x.rejectsIndicative) = false

'hope' does NOT robustly reject indicative — it varies (IND accepted in French, Portuguese, Italian, Greek, Romanian, English).

theorem Phenomena.Complementation.Studies.Grano2024.intend_robustly_rejects_ind : (intendData.all fun (x : MoodChoiceDatum) => x.rejectsIndicative) = true

'intend' robustly rejects indicative (where testable).

theorem Phenomena.Complementation.Studies.Grano2024.causatives_robustly_reject_ind : (causativeData.all fun (x : MoodChoiceDatum) => x.rejectsIndicative) = true

Causatives robustly reject indicative (§2.4).

theorem Phenomena.Complementation.Studies.Grano2024.intend_patterns_with_want : ((intendData.all fun (x : MoodChoiceDatum) => x.rejectsIndicative) = wantData.all fun (x : MoodChoiceDatum) => x.rejectsIndicative) ∧ (intendData.all fun (x : MoodChoiceDatum) => x.rejectsIndicative) ≠ hopeData.all fun (x : MoodChoiceDatum) => x.rejectsIndicative

'intend' patterns with 'want', not 'hope', on indicative rejection. This is the central empirical finding (@cite{grano-2024}, Table 1).

theorem Phenomena.Complementation.Studies.Grano2024.causatives_pattern_with_intend : (causativeData.all fun (x : MoodChoiceDatum) => x.rejectsIndicative) = intendData.all fun (x : MoodChoiceDatum) => x.rejectsIndicative

Causatives pattern with 'intend' and 'want' (not 'hope'). Independent support for the eventuality abstraction analysis (§2.4).

theorem Phenomena.Complementation.Studies.Grano2024.want_selector_matches_data : Bridge.deriveMoodSelector Fragments.English.Predicates.Verbal.want = Semantics.Mood.MoodSelector.subjunctiveSelecting ∧ (wantData.all fun (x : MoodChoiceDatum) => x.rejectsIndicative) = true

The deriveMoodSelector function correctly classifies 'want' as robustly subjunctive-selecting, matching the cross-linguistic data.

theorem Phenomena.Complementation.Studies.Grano2024.hope_selector_matches_data : Bridge.deriveMoodSelector Fragments.English.Predicates.Verbal.hope = Semantics.Mood.MoodSelector.crossLinguisticallyVariable ∧ (hopeData.all fun (x : MoodChoiceDatum) => x.rejectsIndicative) = false

The deriveMoodSelector function correctly classifies 'hope' as cross-linguistically variable, matching the data showing variation.

theorem Phenomena.Complementation.Studies.Grano2024.ind_incompatible_with_eventuality_abstraction : Core.Discourse.GramMood.indicative.effect.eventualityOpen = false

Indicative mood closes the eventuality argument. Therefore, predicates requiring eventuality abstraction (CAUSE* binds the event variable) reject indicative complements.

This is the formal correlate of @cite{grano-2024}'s argument chain: Premise 2 (CAUSE* needs open event arg) + Premise 3 (IND closes it) → Conclusion (intention reports reject IND).

theorem Phenomena.Complementation.Studies.Grano2024.subj_enables_eventuality_abstraction : Core.Discourse.GramMood.subjunctive.effect.eventualityOpen = true

Subjunctive mood leaves the eventuality argument open, enabling CAUSE* to bind it. This is why 'intend' and causatives accept SBJV.

theorem Phenomena.Complementation.Studies.Grano2024.grano_argument_chain : Core.Discourse.GramMood.indicative.effect.eventualityOpen = false ∧ Core.Discourse.GramMood.subjunctive.effect.eventualityOpen = true ∧ (intendData.all fun (x : MoodChoiceDatum) => x.rejectsIndicative) = true ∧ (causativeData.all fun (x : MoodChoiceDatum) => x.rejectsIndicative) = true

The three-premise argument chain:

1. intentionHolds requires P : E → W → Ev Time → Prop (open event arg)
2. IND closes the event argument (eventualityOpen = false)
3. SBJV leaves it open (eventualityOpen = true) → intention reports require SBJV, reject IND

inductive Phenomena.Complementation.Studies.Grano2024.DepartureKind : Type

@cite{grano-2024} §7 proposes that subjunctive mood uniformly signals a departure from the default clausal semantics of unembedded assertions. Two kinds of departure trigger SBJV:

• Comparison: ordering semantics with two modal backgrounds (want, hope; @cite{portner-rubinstein-2020})
• Eventuality abstraction: open event argument for CAUSE* or aspect (intend, causatives, aspectuals; this paper)

Predicates like 'hope' involve comparison only (variable mood). Predicates like 'want' involve comparison (robust SBJV: simplification blocked because 'want' does not allow inconsistent prejacents). Predicates like 'intend' involve both comparison and eventuality abstraction (robust SBJV: IND is type-incompatible with CAUSE*). Predicates like 'believe' involve neither → indicative only.

• comparisonSimplifiable : DepartureKind
• comparisonNonSimplifiable : DepartureKind
• eventualityAbstraction : DepartureKind
• comparisonAndAbstraction : DepartureKind

instance Phenomena.Complementation.Studies.Grano2024.instDecidableEqDepartureKind : DecidableEq DepartureKind

Equations

• Phenomena.Complementation.Studies.Grano2024.instDecidableEqDepartureKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Complementation.Studies.Grano2024.instBEqDepartureKind.beq : DepartureKind → DepartureKind → Bool

Equations

• Phenomena.Complementation.Studies.Grano2024.instBEqDepartureKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Complementation.Studies.Grano2024.instBEqDepartureKind : BEq DepartureKind

Equations

• Phenomena.Complementation.Studies.Grano2024.instBEqDepartureKind = { beq := Phenomena.Complementation.Studies.Grano2024.instBEqDepartureKind.beq }

def Phenomena.Complementation.Studies.Grano2024.instReprDepartureKind.repr : DepartureKind → ℕ → Std.Format

Equations

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

instance Phenomena.Complementation.Studies.Grano2024.instReprDepartureKind : Repr DepartureKind

Equations

• Phenomena.Complementation.Studies.Grano2024.instReprDepartureKind = { reprPrec := Phenomena.Complementation.Studies.Grano2024.instReprDepartureKind.repr }

def Phenomena.Complementation.Studies.Grano2024.DepartureKind.moodPrediction : DepartureKind → Semantics.Mood.MoodSelector

Map departure kind to mood selection prediction.

@cite{grano-2024} §7: both comparison and eventuality abstraction are departures from the default clausal semantics that trigger SBJV. The key empirical difference:

• Comparison alone: SBJV is expected, but Portner & Rubinstein's simplification of two modal backgrounds into one can license IND in some languages (French espérer). This yields cross-linguistic variation for 'hope'-type verbs.
• Eventuality abstraction (± comparison): SBJV is robust because IND existentially closes the event argument, making it type-incompatible with CAUSE* / aspect / perception. No simplification can rescue IND here.

Equations

• Phenomena.Complementation.Studies.Grano2024.DepartureKind.comparisonSimplifiable.moodPrediction = Semantics.Mood.MoodSelector.crossLinguisticallyVariable
• Phenomena.Complementation.Studies.Grano2024.DepartureKind.comparisonNonSimplifiable.moodPrediction = Semantics.Mood.MoodSelector.subjunctiveSelecting
• Phenomena.Complementation.Studies.Grano2024.DepartureKind.eventualityAbstraction.moodPrediction = Semantics.Mood.MoodSelector.subjunctiveSelecting
• Phenomena.Complementation.Studies.Grano2024.DepartureKind.comparisonAndAbstraction.moodPrediction = Semantics.Mood.MoodSelector.subjunctiveSelecting

theorem Phenomena.Complementation.Studies.Grano2024.eventuality_abstraction_robust : DepartureKind.eventualityAbstraction.moodPrediction = Semantics.Mood.MoodSelector.subjunctiveSelecting ∧ DepartureKind.comparisonAndAbstraction.moodPrediction = Semantics.Mood.MoodSelector.subjunctiveSelecting

Eventuality abstraction robustly predicts subjunctive selection (IND is type-incompatible with open event argument).

theorem Phenomena.Complementation.Studies.Grano2024.simplifiable_comparison_variable : DepartureKind.comparisonSimplifiable.moodPrediction = Semantics.Mood.MoodSelector.crossLinguisticallyVariable

Simplifiable comparison allows cross-linguistic variation (the 'hope' pattern). Per @cite{portner-rubinstein-2020}: when two modal backgrounds can simplify to one, IND becomes available.

theorem Phenomena.Complementation.Studies.Grano2024.nonsimplifiable_comparison_robust : DepartureKind.comparisonNonSimplifiable.moodPrediction = Semantics.Mood.MoodSelector.subjunctiveSelecting

Non-simplifiable comparison robustly predicts SBJV (the 'want' pattern). 'want' blocks simplification: it does not tolerate inconsistent prejacents ((50), (60)), so both modal backgrounds must remain.

theorem Phenomena.Complementation.Studies.Grano2024.intend_patterns_with_want_not_hope : DepartureKind.comparisonAndAbstraction.moodPrediction = DepartureKind.comparisonNonSimplifiable.moodPrediction ∧ DepartureKind.comparisonAndAbstraction.moodPrediction ≠ DepartureKind.comparisonSimplifiable.moodPrediction

'intend' (comparison + abstraction) patterns with 'want' (non-simplifiable comparison), not with 'hope' (simplifiable comparison). This is the central prediction: all three involve comparison, but eventuality abstraction independently blocks IND.

§6.1 Intention-Rigid Predicates

Predicates that obligatorily encode intention: aim, try, endeavor, strive, seek. All share 'intend's causally self-referential, goal-oriented property and, as predicted, reject indicative complements ((90)–(91)).

§6.2 Belief-Intention Hybrid Predicates

Predicates like 'decide', 'convince', 'persuade' report either belief or intention formation depending on complement type ((96)–(97)):

• Nonfinite complement → intention reading → requires SBJV/nonfinite
• Finite complement → belief reading → allows IND

This is exactly the complement-size-driven alternation that @cite{fusco-sgrizzi-2026} formalizes for Italian convincere.

§6.3 Aspectual Predicates

Aspect is inherently event-related and requires eventuality abstraction. Aspectual predicates (begin, start, stop, continue) accept nonfinite/SBJV complements but reject finite indicative complements ((115)–(119)).

§6.4 Memory and Perception Reports

'remember' + gerund = event construal (eventuality abstraction); 'remember' + that-clause = propositional construal (no abstraction). 'see' + bare infinitive = event perception; 'see' + that-clause = indirect evidence. ((120)–(127))

theorem Phenomena.Complementation.Studies.Grano2024.try_rejects_finite : Fragments.English.Predicates.Verbal.try_.complementType = Core.Verbs.ComplementType.infinitival ∧ Fragments.English.Predicates.Verbal.try_.altComplementType = none

Intention-rigid predicates reject IND like 'intend' (§6.1, (91)). 'try' is in the English fragment; it takes infinitival complements and has no alternate finite complement type.

theorem Phenomena.Complementation.Studies.Grano2024.persuade_is_hybrid : Fragments.English.Predicates.Verbal.persuade.complementType = Core.Verbs.ComplementType.infinitival ∧ Fragments.English.Predicates.Verbal.persuade.controlType = Core.Verbs.ControlType.objectControl

'persuade' is a hybrid predicate: nonfinite complement with object control → intention reading. This matches @cite{grano-2024} §6.2 (96).

theorem Phenomena.Complementation.Studies.Grano2024.promise_is_hybrid : Fragments.English.Predicates.Verbal.promise.complementType = Core.Verbs.ComplementType.infinitival ∧ Fragments.English.Predicates.Verbal.promise.controlType = Core.Verbs.ControlType.subjectControl

'promise' is a hybrid predicate: nonfinite complement with subject control → intention (commissive). Matches §6.2 (98a).

theorem Phenomena.Complementation.Studies.Grano2024.start_is_phasal : Fragments.English.Predicates.Verbal.start.cosType.isSome = true ∧ Fragments.English.Predicates.Verbal.start.complementType = Core.Verbs.ComplementType.gerund

Aspectual predicates are phasal (cosType.isSome) and take gerund complements in English, consistent with requiring eventuality abstraction (§6.3, (115)–(116)). In Romance, these take infinitival or subjunctive complements ((117)–(119)).

theorem Phenomena.Complementation.Studies.Grano2024.stop_is_phasal : Fragments.English.Predicates.Verbal.stop.cosType.isSome = true ∧ Fragments.English.Predicates.Verbal.stop.complementType = Core.Verbs.ComplementType.gerund

theorem Phenomena.Complementation.Studies.Grano2024.begin_is_phasal : Fragments.English.Predicates.Verbal.begin_.cosType.isSome = true ∧ Fragments.English.Predicates.Verbal.begin_.complementType = Core.Verbs.ComplementType.gerund

theorem Phenomena.Complementation.Studies.Grano2024.continue_is_phasal : Fragments.English.Predicates.Verbal.continue_.cosType.isSome = true ∧ Fragments.English.Predicates.Verbal.continue_.complementType = Core.Verbs.ComplementType.gerund

theorem Phenomena.Complementation.Studies.Grano2024.see_is_factive_perception : Fragments.English.Predicates.Verbal.see.factivePresup = true ∧ Fragments.English.Predicates.Verbal.see.levinClass = some LevinClass.see

'see' takes NP complements primarily (bare perception), with factive presupposition. The bare infinitive (eventive, §6.4 (124)) vs that-clause (propositional, §6.4 (125)) alternation tracks eventuality abstraction.

theorem Phenomena.Complementation.Studies.Grano2024.decide_is_hybrid : Fragments.English.Predicates.Verbal.decide_.complementType = Core.Verbs.ComplementType.infinitival ∧ Fragments.English.Predicates.Verbal.decide_.altComplementType = some Core.Verbs.ComplementType.finiteClause ∧ Fragments.English.Predicates.Verbal.decide_.controlType = Core.Verbs.ControlType.subjectControl

'decide' is a hybrid predicate: nonfinite complement → intention, finite complement → belief (@cite{grano-2024} §6.2, (96)–(97)). Like 'persuade' and 'convince', the complement type determines whether the reading is intentional or propositional.

theorem Phenomena.Complementation.Studies.Grano2024.remember_is_implicative : Fragments.English.Predicates.Verbal.remember.complementType = Core.Verbs.ComplementType.infinitival ∧ Fragments.English.Predicates.Verbal.remember.implicativeBuilder.isSome = true

'remember' takes infinitival (implicative/eventive, §6.4 (120)). The gerund construal enables event memory; the that-clause enables propositional memory ((120)–(121)).

Complement Size → Reading → Mood

@cite{grano-2024}'s hybrid predicate analysis (§6.2) and @cite{fusco-sgrizzi-2026}'s complement-size analysis make the same prediction: the complement's structural size determines whether the reading is intentional (requiring eventuality abstraction → SBJV) or propositional (existentially closed → IND-compatible).

The connection: Fusco & Sgrizzi's readingFromSize maps complement sizes to readings; Grano's DepartureKind maps readings to mood predictions. Together they form an end-to-end chain:

complement size → reading → departure kind → mood prediction

def Phenomena.Complementation.Studies.Grano2024.readingToDeparture : Semantics.Attitudes.RationalAttitude.Reading → Option DepartureKind

Map a rational attitude reading to a departure kind.

Intention readings require eventuality abstraction (CAUSE* binds the event argument). Belief readings involve neither comparison nor eventuality abstraction — they are the default clausal semantics.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Complementation.Studies.Grano2024.readingToDeparture Semantics.Attitudes.RationalAttitude.Reading.belief = none

theorem Phenomena.Complementation.Studies.Grano2024.intention_predicts_subjunctive : Option.map DepartureKind.moodPrediction (readingToDeparture Semantics.Attitudes.RationalAttitude.Reading.intention) = some Semantics.Mood.MoodSelector.subjunctiveSelecting

Intention readings predict robust subjunctive selection.

theorem Phenomena.Complementation.Studies.Grano2024.belief_predicts_no_departure : readingToDeparture Semantics.Attitudes.RationalAttitude.Reading.belief = none

Belief readings predict no departure (default = indicative).

theorem Phenomena.Complementation.Studies.Grano2024.subcp_to_subjunctive : have reading := Semantics.Attitudes.RationalAttitude.readingFromSize Minimalism.ComplementSize.vP; have departure := readingToDeparture reading; have mood := Option.map DepartureKind.moodPrediction departure; reading = Semantics.Attitudes.RationalAttitude.Reading.intention ∧ departure = some DepartureKind.eventualityAbstraction ∧ mood = some Semantics.Mood.MoodSelector.subjunctiveSelecting

End-to-end: sub-CP complement → intention → eventuality abstraction → robust subjunctive selection.

theorem Phenomena.Complementation.Studies.Grano2024.cp_to_indicative : have reading := Semantics.Attitudes.RationalAttitude.readingFromSize Minimalism.ComplementSize.cP; have departure := readingToDeparture reading; reading = Semantics.Attitudes.RationalAttitude.Reading.belief ∧ departure = none

End-to-end: CP complement → belief → no departure → no SBJV requirement (default = indicative).

theorem Phenomena.Complementation.Studies.Grano2024.want_moodPrediction_agrees : DepartureKind.comparisonNonSimplifiable.moodPrediction = Bridge.deriveMoodSelector Fragments.English.Predicates.Verbal.want

'want' involves non-simplifiable comparison (robust SBJV).

theorem Phenomena.Complementation.Studies.Grano2024.hope_moodPrediction_agrees : DepartureKind.comparisonSimplifiable.moodPrediction = Bridge.deriveMoodSelector Fragments.English.Predicates.Verbal.hope

'hope' involves simplifiable comparison (variable mood).

theorem Phenomena.Complementation.Studies.Grano2024.intend_moodPrediction_agrees : DepartureKind.comparisonAndAbstraction.moodPrediction = Bridge.deriveMoodSelector Fragments.English.Predicates.Verbal.intend

'intend' involves both comparison and eventuality abstraction (robust SBJV).

theorem Phenomena.Complementation.Studies.Grano2024.causative_moodPrediction_agrees : DepartureKind.eventualityAbstraction.moodPrediction = Bridge.deriveMoodSelector Fragments.English.Predicates.Verbal.make

Causatives involve eventuality abstraction (robust SBJV).

Fragment Entry ↔ Datum Consistency

The cross-linguistic fragment files encode verb properties that should be consistent with the mood choice data. For predicates in the want-class (levinClass = .want), the datum should have rejectsIndicative = true. For predicates NOT in the want-class (like 'hope'), the mood variability is captured by deriveMoodSelector returning .crossLinguisticallyVariable.

theorem Phenomena.Complementation.Studies.Grano2024.greek_want_fragment_consistent : Fragments.Greek.MoodChoice.thelo.levinClass = some LevinClass.want ∧ greek_want.rejectsIndicative = true

theorem Phenomena.Complementation.Studies.Grano2024.greek_hope_fragment_consistent : Fragments.Greek.MoodChoice.elpizo.levinClass ≠ some LevinClass.want ∧ greek_hope.rejectsIndicative = false

theorem Phenomena.Complementation.Studies.Grano2024.greek_intend_fragment_consistent : Fragments.Greek.MoodChoice.protithete.levinClass = some LevinClass.want ∧ greek_intend.rejectsIndicative = true

theorem Phenomena.Complementation.Studies.Grano2024.greek_make_fragment_consistent : Fragments.Greek.MoodChoice.vazo.causativeBuilder.isSome = true ∧ greek_make.rejectsIndicative = true

theorem Phenomena.Complementation.Studies.Grano2024.romanian_want_fragment_consistent : Fragments.Romanian.MoodChoice.a_vrea.levinClass = some LevinClass.want ∧ romanian_want.rejectsIndicative = true

theorem Phenomena.Complementation.Studies.Grano2024.romanian_hope_fragment_consistent : Fragments.Romanian.MoodChoice.a_spera.levinClass ≠ some LevinClass.want ∧ romanian_hope.rejectsIndicative = false

theorem Phenomena.Complementation.Studies.Grano2024.romanian_intend_fragment_consistent : Fragments.Romanian.MoodChoice.a_intentiona.levinClass = some LevinClass.want ∧ romanian_intend.rejectsIndicative = true

theorem Phenomena.Complementation.Studies.Grano2024.spanish_want_fragment_consistent : Fragments.Spanish.MoodChoice.querer.levinClass = some LevinClass.want ∧ spanish_want.rejectsIndicative = true

theorem Phenomena.Complementation.Studies.Grano2024.spanish_intend_fragment_consistent : Fragments.Spanish.MoodChoice.tener_la_intencion.levinClass = some LevinClass.want ∧ spanish_intend.rejectsIndicative = true

theorem Phenomena.Complementation.Studies.Grano2024.portuguese_want_fragment_consistent : Fragments.Portuguese.MoodChoice.querer.levinClass = some LevinClass.want ∧ portuguese_want.rejectsIndicative = true

theorem Phenomena.Complementation.Studies.Grano2024.portuguese_intend_fragment_consistent : Fragments.Portuguese.MoodChoice.pretender.levinClass = some LevinClass.want ∧ portuguese_intend.rejectsIndicative = true