Grano 2024: Intention Reports and Event Abstraction [Gra24]

Cross-linguistic mood choice data and bridge theorems connecting [Gra24]'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 ([Sea83]; [Har76])
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' ([PR20])
• Event abstraction: 'intend', causatives, aspectuals (this paper)

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

structure Grano2024.MoodChoiceDatum : Type

A mood choice observation: whether a predicate in a language rejects indicative complements ([Gra24], 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

@[instance_reducible]

instance Grano2024.instDecidableEqMoodChoiceDatum : DecidableEq MoodChoiceDatum

Equations

• Grano2024.instDecidableEqMoodChoiceDatum = Grano2024.instDecidableEqMoodChoiceDatum.decEq

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

Equations

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

def Grano2024.instReprMoodChoiceDatum.repr : MoodChoiceDatum → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Grano2024.instReprMoodChoiceDatum : Repr MoodChoiceDatum

Equations

• Grano2024.instReprMoodChoiceDatum = { reprPrec := Grano2024.instReprMoodChoiceDatum.repr }

def Grano2024.spanish_want : MoodChoiceDatum

Equations

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

def Grano2024.french_want : MoodChoiceDatum

Equations

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

def Grano2024.portuguese_want : MoodChoiceDatum

Equations

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

def Grano2024.italian_want : MoodChoiceDatum

Equations

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

def Grano2024.greek_want : MoodChoiceDatum

Equations

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

def Grano2024.romanian_want : MoodChoiceDatum

Equations

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

def Grano2024.english_want : MoodChoiceDatum

Equations

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

def Grano2024.spanish_hope : MoodChoiceDatum

Equations

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

def Grano2024.french_hope : MoodChoiceDatum

Equations

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

def Grano2024.portuguese_hope : MoodChoiceDatum

Equations

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

def Grano2024.italian_hope : MoodChoiceDatum

Equations

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

def Grano2024.greek_hope : MoodChoiceDatum

Equations

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

def Grano2024.romanian_hope : MoodChoiceDatum

Equations

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

def Grano2024.english_hope : MoodChoiceDatum

Equations

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

def Grano2024.spanish_intend : MoodChoiceDatum

Equations

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

def Grano2024.portuguese_intend : MoodChoiceDatum

Equations

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

def Grano2024.greek_intend : MoodChoiceDatum

Equations

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

def Grano2024.romanian_intend : MoodChoiceDatum

Equations

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

def Grano2024.english_intend : MoodChoiceDatum

Equations

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

def Grano2024.spanish_make : MoodChoiceDatum

Equations

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

def Grano2024.french_make : MoodChoiceDatum

Equations

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

def Grano2024.portuguese_make : MoodChoiceDatum

Equations

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

def Grano2024.italian_make : MoodChoiceDatum

Equations

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

def Grano2024.greek_make : MoodChoiceDatum

Equations

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

def Grano2024.romanian_make : MoodChoiceDatum

Equations

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

def Grano2024.english_make : MoodChoiceDatum

Equations

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

def Grano2024.wantData : List MoodChoiceDatum

Equations

• Grano2024.wantData = [Grano2024.spanish_want, Grano2024.french_want, Grano2024.portuguese_want, Grano2024.italian_want, Grano2024.greek_want, Grano2024.romanian_want, Grano2024.english_want]

def Grano2024.hopeData : List MoodChoiceDatum

Equations

• Grano2024.hopeData = [Grano2024.spanish_hope, Grano2024.french_hope, Grano2024.portuguese_hope, Grano2024.italian_hope, Grano2024.greek_hope, Grano2024.romanian_hope, Grano2024.english_hope]

def Grano2024.intendData : List MoodChoiceDatum

Equations

• Grano2024.intendData = [Grano2024.spanish_intend, Grano2024.portuguese_intend, Grano2024.greek_intend, Grano2024.romanian_intend, Grano2024.english_intend]

def Grano2024.causativeData : List MoodChoiceDatum

Equations

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

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

'want' robustly rejects indicative across all 7 languages.

theorem 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 Grano2024.intend_robustly_rejects_ind : (intendData.all fun (x : MoodChoiceDatum) => x.rejectsIndicative) = true

'intend' robustly rejects indicative (where testable).

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

Causatives robustly reject indicative (§2.4).

theorem 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 ([Gra24], Table 1).

theorem 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 Grano2024.want_selector_matches_data : Noonan2007.deriveSelector English.Predicates.Verbal.want = Mood.Selector.subjunctiveSelecting ∧ (wantData.all fun (x : MoodChoiceDatum) => x.rejectsIndicative) = true

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

theorem Grano2024.hope_selector_matches_data : Noonan2007.deriveSelector English.Predicates.Verbal.hope = Mood.Selector.crossLinguisticallyVariable ∧ (hopeData.all fun (x : MoodChoiceDatum) => x.rejectsIndicative) = false

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

Causal self-reference and the two report types

CAUSE*(s, e, w): the attitude state s brings about event e in w "in the right way" — via the agent's intention-in-action, not a deviant causal chain ([Gra24] (79); [Sea83]; on deviance, [Har76] and [Chi66]: Betty's intention to shoot makes her nervous, the nervousness makes her pull the trigger — the intention caused the killing, but not in the right way, so she did not carry out her intention).

def Grano2024.intentionHolds {E : Type u_1} {W : Type u_2} {Time : Type u_3} [LinearOrder Time] (isIntention : Event Time → W → Prop) (holder : E → Event Time → W → Prop) (content : Event Time → Set (W × E)) (causeStar : Event Time → Event Time → W → Prop) (agent : E) (P : E → W → Event Time → Prop) (w : W) : Prop

Intention reports with causal self-reference ([Gra24], (79)): some stative intention state held by the agent, each of whose content pairs ⟨w', x⟩ supports an event that the state brings about in the right way and that satisfies the complement. The complement type E → W → Event Time → Prop keeps the event argument open — the formal correlate of Premise 3: indicative would existentially close it to W → Prop, which cannot compose with the causal self-reference relation.

Equations

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

def Grano2024.beliefHolds {E : Type u_1} {W : Type u_2} (dox : E → W → Set W) (agent : E) (P : W → Prop) (w : W) : Prop

Plain belief reports need no causal self-reference: the complement is a closed proposition evaluated over doxastic alternatives — which is why believe is indicative-selecting while intend selects subjunctive.

Equations

• Grano2024.beliefHolds dox agent P w = ∀ w' ∈ dox agent w, P w'

theorem Grano2024.ind_incompatible_with_eventuality_abstraction {E : Type u_1} (P : E → Prop) : Mood.Grammatical.eventDenotation P Mood.Grammatical.indicative = Mood.EventDenotation.closed (∃ (e : E), P e)

Indicative mood closes the eventuality argument: its event-level denotation lands in the closed constructor, so predicates requiring eventuality abstraction (CAUSE* binds the event variable) reject indicative complements.

This is the formal correlate of [Gra24]'s argument chain: Premise 2 (CAUSE* needs open event arg) + Premise 3 (IND closes it) → Conclusion (intention reports reject IND).

theorem Grano2024.subj_enables_eventuality_abstraction {E : Type u_1} (P : E → Prop) : Mood.Grammatical.eventDenotation P Mood.Grammatical.subjunctive = Mood.EventDenotation.abstracted P

Subjunctive mood leaves the eventuality argument open — its denotation lands in abstracted with the predicate intact — enabling CAUSE* to bind it. This is why 'intend' and causatives accept SBJV.

theorem Grano2024.grano_argument_chain : (∀ (P : Unit → Prop), Mood.Grammatical.eventDenotation P Mood.Grammatical.indicative = Mood.EventDenotation.closed (∃ (e : Unit), P e)) ∧ (∀ (P : Unit → Prop), Mood.Grammatical.eventDenotation P Mood.Grammatical.subjunctive = Mood.EventDenotation.abstracted P) ∧ (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 → Event Time → Prop (open event arg)
2. IND closes the event argument (eventDenotation lands in closed)
3. SBJV leaves it open (eventDenotation lands in abstracted) → intention reports require SBJV, reject IND

inductive Grano2024.DepartureKind : Type

[Gra24] §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; [PR20])
• Event 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_reducible]

instance Grano2024.instDecidableEqDepartureKind : DecidableEq DepartureKind

Equations

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

def Grano2024.instReprDepartureKind.repr : DepartureKind → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Grano2024.instReprDepartureKind : Repr DepartureKind

Equations

• Grano2024.instReprDepartureKind = { reprPrec := Grano2024.instReprDepartureKind.repr }

def Grano2024.DepartureKind.moodPrediction : DepartureKind → Mood.Selector

Map departure kind to mood selection prediction.

[Gra24] §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.
• Event 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

• Grano2024.DepartureKind.comparisonSimplifiable.moodPrediction = Mood.Selector.crossLinguisticallyVariable
• Grano2024.DepartureKind.comparisonNonSimplifiable.moodPrediction = Mood.Selector.subjunctiveSelecting
• Grano2024.DepartureKind.eventualityAbstraction.moodPrediction = Mood.Selector.subjunctiveSelecting
• Grano2024.DepartureKind.comparisonAndAbstraction.moodPrediction = Mood.Selector.subjunctiveSelecting

theorem Grano2024.eventuality_abstraction_robust : DepartureKind.eventualityAbstraction.moodPrediction = Mood.Selector.subjunctiveSelecting ∧ DepartureKind.comparisonAndAbstraction.moodPrediction = Mood.Selector.subjunctiveSelecting

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

theorem Grano2024.simplifiable_comparison_variable : DepartureKind.comparisonSimplifiable.moodPrediction = Mood.Selector.crossLinguisticallyVariable

Simplifiable comparison allows cross-linguistic variation (the 'hope' pattern). Per [PR20]: when two modal backgrounds can simplify to one, IND becomes available.

theorem Grano2024.nonsimplifiable_comparison_robust : DepartureKind.comparisonNonSimplifiable.moodPrediction = Mood.Selector.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 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 [FS26] 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 Grano2024.try_rejects_finite : English.Predicates.Verbal.try_.complementType = ComplementType.infinitival ∧ 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 Grano2024.persuade_is_hybrid : English.Predicates.Verbal.persuade.complementType = ComplementType.infinitival ∧ English.Predicates.Verbal.persuade.controlType = ControlType.objectControl

'persuade' is a hybrid predicate: nonfinite complement with object control → intention reading. This matches [Gra24] §6.2 (96).

theorem Grano2024.promise_is_hybrid : English.Predicates.Verbal.promise.complementType = ComplementType.infinitival ∧ English.Predicates.Verbal.promise.controlType = ControlType.subjectControl

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

theorem Grano2024.start_is_phasal : English.Predicates.Verbal.start.cosType.isSome = true ∧ English.Predicates.Verbal.start.complementType = 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 Grano2024.stop_is_phasal : English.Predicates.Verbal.stop.cosType.isSome = true ∧ English.Predicates.Verbal.stop.complementType = ComplementType.gerund

theorem Grano2024.begin_is_phasal : English.Predicates.Verbal.begin_.cosType.isSome = true ∧ English.Predicates.Verbal.begin_.complementType = ComplementType.gerund

theorem Grano2024.continue_is_phasal : English.Predicates.Verbal.continue_.cosType.isSome = true ∧ English.Predicates.Verbal.continue_.complementType = ComplementType.gerund

theorem Grano2024.see_is_factive_perception : English.Predicates.Verbal.see.factivePresup = true ∧ English.Predicates.Verbal.see.levinClass = some ArgumentStructure.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 Grano2024.decide_is_hybrid : English.Predicates.Verbal.decide_.complementType = ComplementType.infinitival ∧ English.Predicates.Verbal.decide_.altComplementType = some ComplementType.finiteClause ∧ English.Predicates.Verbal.decide_.controlType = ControlType.subjectControl

'decide' is a hybrid predicate: nonfinite complement → intention, finite complement → belief ([Gra24] §6.2, (96)–(97)). Like 'persuade' and 'convince', the complement type determines whether the reading is intentional or propositional.

theorem Grano2024.remember_is_implicative : English.Predicates.Verbal.remember.complementType = ComplementType.infinitival ∧ English.Predicates.Verbal.remember.implicative.isSome = true

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

theorem Grano2024.want_moodPrediction_agrees : DepartureKind.comparisonNonSimplifiable.moodPrediction = Noonan2007.deriveSelector English.Predicates.Verbal.want

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

theorem Grano2024.hope_moodPrediction_agrees : DepartureKind.comparisonSimplifiable.moodPrediction = Noonan2007.deriveSelector English.Predicates.Verbal.hope

'hope' involves simplifiable comparison (variable mood).

theorem Grano2024.intend_moodPrediction_agrees : DepartureKind.comparisonAndAbstraction.moodPrediction = Noonan2007.deriveSelector English.Predicates.Verbal.intend

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

theorem Grano2024.causative_moodPrediction_agrees : DepartureKind.eventualityAbstraction.moodPrediction = Noonan2007.deriveSelector English.Predicates.Verbal.make

Causatives involve eventuality abstraction (robust SBJV).

Per-verb closure of deriveSelector under Selector.toVerbalOp. The cross-linguistic mood-choice data (§3) flows through deriveSelector (§3) and into the State-typed verbal-mood operator (VerbalMood.lean). For robustly subjunctive predicates, the projection lands in some .subjunctive; for cross-linguistically variable predicates, in none. The chain verb → Selector → VerbalOp makes the lexical-class commitment of [Gra24] operationally ready to feed State-side glosses (ExpState.boxLe for subjunctive, ExpState.boxCs for indicative).

theorem Grano2024.want_verbalMood : (Noonan2007.deriveSelector English.Predicates.Verbal.want).toVerbalOp = some Mood.VerbalOp.subjunctive

'want' lifts to the subjunctive State operator.

theorem Grano2024.hope_verbalMood : (Noonan2007.deriveSelector English.Predicates.Verbal.hope).toVerbalOp = none

'hope' is cross-linguistically variable, so it lifts to none.

theorem Grano2024.want_target : Option.map (fun (x : Mood.VerbalOp) => Mood.HasTarget.target x) (Noonan2007.deriveSelector English.Predicates.Verbal.want).toVerbalOp = some Mood.Component.preferential

The robust subjunctive predicates (e.g. 'want') project to the preferential POSW component — they quantify over the best-ranked subset of the State via ExpState.boxLe. The composed projection (Selector → VerbalOp → Component) makes the operational target explicit.

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 deriveSelector returning .crossLinguisticallyVariable.

theorem Grano2024.greek_want_fragment_consistent : Greek.StandardModern.MoodChoice.thelo.levinClass = some ArgumentStructure.LevinClass.want ∧ greek_want.rejectsIndicative = true

theorem Grano2024.greek_hope_fragment_consistent : Greek.StandardModern.MoodChoice.elpizo.levinClass ≠ some ArgumentStructure.LevinClass.want ∧ greek_hope.rejectsIndicative = false

theorem Grano2024.greek_intend_fragment_consistent : Greek.StandardModern.MoodChoice.protithete.levinClass = some ArgumentStructure.LevinClass.want ∧ greek_intend.rejectsIndicative = true

theorem Grano2024.greek_make_fragment_consistent : Greek.StandardModern.MoodChoice.vazo.causative.isSome = true ∧ greek_make.rejectsIndicative = true

theorem Grano2024.romanian_want_fragment_consistent : Romanian.MoodChoice.a_vrea.levinClass = some ArgumentStructure.LevinClass.want ∧ romanian_want.rejectsIndicative = true

theorem Grano2024.romanian_hope_fragment_consistent : Romanian.MoodChoice.a_spera.levinClass ≠ some ArgumentStructure.LevinClass.want ∧ romanian_hope.rejectsIndicative = false

theorem Grano2024.romanian_intend_fragment_consistent : Romanian.MoodChoice.a_intentiona.levinClass = some ArgumentStructure.LevinClass.want ∧ romanian_intend.rejectsIndicative = true

theorem Grano2024.spanish_want_fragment_consistent : Spanish.MoodChoice.querer.levinClass = some ArgumentStructure.LevinClass.want ∧ spanish_want.rejectsIndicative = true

theorem Grano2024.spanish_intend_fragment_consistent : Spanish.MoodChoice.tener_la_intencion.levinClass = some ArgumentStructure.LevinClass.want ∧ spanish_intend.rejectsIndicative = true

theorem Grano2024.portuguese_want_fragment_consistent : Portuguese.MoodChoice.querer.levinClass = some ArgumentStructure.LevinClass.want ∧ portuguese_want.rejectsIndicative = true

theorem Grano2024.portuguese_intend_fragment_consistent : Portuguese.MoodChoice.pretender.levinClass = some ArgumentStructure.LevinClass.want ∧ portuguese_intend.rejectsIndicative = true