Grano (2024): Intention Reports and Eventuality Abstraction in a Theory of Mood Choice

This file formalizes [Gra24]'s account of why 'intend' accepts nonfinite and subjunctive complements but rejects indicative ones across Spanish, French, Portuguese, Italian, Greek, Romanian, and English, as 'want' does and as 'hope' does not (Table 1). Three premises carry the argument: intention reports have causally self-referential content ([Sea83], [Har76]), an intention being carried out only if it causes the outcome in the right way; encoding that content takes abstraction over the complement's eventuality argument, since causation relates eventualities (Event.causedClosure_factorsThrough_iff); and subjunctive and nonfinite clauses can leave that argument open where the indicative closes it (MoodHead). The pool of the paper's judged complements records each predicate's class, the complement type, and where it matters the reading, and abstraction_rejects_indicative checks the conclusion over every row that requires abstraction: intention reports, causatives, the intention-rigid aim and try, aspectual predicates, the intention readings of persuade, decide, promise, and plan, and the event readings of memory and perception reports. Section 3's case against [PR20] and [GM21] is intend_like_hope_in_logic: on realism, consistency, and monotonicity 'intend' patterns with 'hope', whose indicative those theories license by that very profile, yet every indicative row under 'intend' is rejected. The Hintikka semantics of (73) is the modal box over intention alternatives, and the three properties follow from their overlap with the doxastic alternatives (realism and its siblings); the verb entries of the language fragments record the finite moods the pool accepts (fragments_match_pool); and section 7's synthesis reads the availability of the indicative off the two departures from default clausal semantics, a pair of modal backgrounds and eventuality abstraction (indicative_possible_iff).

Implementation notes

The mood heads are those of section 5, (87) to (89): the subjunctive is ambiguous between a head that closes the eventuality argument as the indicative does and one that passes it up, so an open argument implies subjunctive or nonfinite form and not conversely. A head's clause denotes in a sum type, a proposition or a predicate of eventualities, the type mismatch under 'intend' being the absence of the second. Nonfinite complements carry the subjunctive's two heads, as the paper says without illustrating. sbjvCausal is the alternative of section 7, (134), which moves the quantification of 'intend' into the mood head. Whether a class needs eventuality abstraction is the paper's premise per class; for the hybrid, commissive, plan, memory, and perception predicates the reading of the row decides. The simplification condition of [PR20] is read off the consistency rows: a pair of backgrounds may collapse when the class rejects inconsistent prejacents. French faire with indicative complements, (43a) and (44b), which the paper leaves as open exceptions, is not in the pool, and the paper's remarks on nominal avoir l'intention and on French and Italian rejecting non-control complements under 'intend' altogether are recorded as rows without a theorem.

References

• [Gra24]
• [PR20]
• [GM21]
• [Sea83]
• [Har76]
• [Hei92]
• [Hig83]

The pool

inductive Grano2024.Class : Type

The predicate classes of the pool.

• want : Class
• hope : Class
• intend : Class
• causative : Class
• intentionRigid : Class

  aim, try, endeavor, strive, seek, section 6.1.

• hybrid : Class

  persuade, convince, decide: intention with a nonfinite or subjunctive complement, belief with an indicative one.

• commissive : Class

  promise, agree, pledge, swear: a commissive or an assertion by the same split.

• plan : Class
• aspectual : Class
• memory : Class
• perception : Class

@[instance_reducible]

instance Grano2024.instDecidableEqClass : DecidableEq Class

Equations

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

@[instance_reducible]

instance Grano2024.instReprClass : Repr Class

Equations

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

def Grano2024.instReprClass.repr : Class → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Grano2024.instReprClass.repr Grano2024.Class.want prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grano2024.Class.want")).group prec✝
• Grano2024.instReprClass.repr Grano2024.Class.hope prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grano2024.Class.hope")).group prec✝
• Grano2024.instReprClass.repr Grano2024.Class.intend prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grano2024.Class.intend")).group prec✝
• Grano2024.instReprClass.repr Grano2024.Class.causative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grano2024.Class.causative")).group prec✝
• Grano2024.instReprClass.repr Grano2024.Class.hybrid prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grano2024.Class.hybrid")).group prec✝
• Grano2024.instReprClass.repr Grano2024.Class.commissive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grano2024.Class.commissive")).group prec✝
• Grano2024.instReprClass.repr Grano2024.Class.plan prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grano2024.Class.plan")).group prec✝
• Grano2024.instReprClass.repr Grano2024.Class.aspectual prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grano2024.Class.aspectual")).group prec✝
• Grano2024.instReprClass.repr Grano2024.Class.memory prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grano2024.Class.memory")).group prec✝
• Grano2024.instReprClass.repr Grano2024.Class.perception prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grano2024.Class.perception")).group prec✝

@[instance_reducible]

instance Grano2024.instFintypeClass : Fintype Class

Equations

• Grano2024.instFintypeClass = { elems := { val := ↑Grano2024.Class.enumList, nodup := Grano2024.Class.enumList_nodup }, complete := Grano2024.instFintypeClass._proof_1 }

inductive Grano2024.Complement : Type

The complement types of the pool.

• indicative : Complement
• subjunctive : Complement
• infinitive : Complement
• forTo : Complement
• gerund : Complement
• bareInfinitive : Complement

@[instance_reducible]

instance Grano2024.instDecidableEqComplement : DecidableEq Complement

Equations

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

def Grano2024.instReprComplement.repr : Complement → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Grano2024.instReprComplement : Repr Complement

Equations

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

@[instance_reducible]

instance Grano2024.instFintypeComplement : Fintype Complement

Equations

• Grano2024.instFintypeComplement = { elems := { val := ↑Grano2024.Complement.enumList, nodup := Grano2024.Complement.enumList_nodup }, complete := Grano2024.instFintypeComplement._proof_1 }

Section 5: mood heads and the eventuality argument

inductive Grano2024.MoodHead : Type

The mood heads of section 5. The indicative and the first subjunctive close the eventuality argument of their clause and the second subjunctive passes it up; mood in nonfinite clauses patterns with the subjunctive.

• indic : MoodHead
• sbjv₁ : MoodHead
• sbjv₂ : MoodHead

@[instance_reducible]

instance Grano2024.instDecidableEqMoodHead : DecidableEq MoodHead

Equations

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

@[instance_reducible]

instance Grano2024.instReprMoodHead : Repr MoodHead

Equations

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

def Grano2024.instReprMoodHead.repr : MoodHead → ℕ → Std.Format

Equations

• Grano2024.instReprMoodHead.repr Grano2024.MoodHead.indic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grano2024.MoodHead.indic")).group prec✝
• Grano2024.instReprMoodHead.repr Grano2024.MoodHead.sbjv₁ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grano2024.MoodHead.sbjv₁")).group prec✝
• Grano2024.instReprMoodHead.repr Grano2024.MoodHead.sbjv₂ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grano2024.MoodHead.sbjv₂")).group prec✝

def Grano2024.MoodHead.mood : MoodHead → Mood.Grammatical

The morphological mood a head is spelled out as.

Equations

• Grano2024.MoodHead.indic.mood = Mood.Grammatical.indicative
• Grano2024.MoodHead.sbjv₁.mood = Mood.Grammatical.subjunctive
• Grano2024.MoodHead.sbjv₂.mood = Mood.Grammatical.subjunctive

def Grano2024.MoodHead.Opens (m : MoodHead) : Prop

The head passes the eventuality argument up.

Equations

• m.Opens = (m = Grano2024.MoodHead.sbjv₂)

@[instance_reducible]

instance Grano2024.instDecidablePredMoodHeadOpens : DecidablePred MoodHead.Opens

Equations

• Grano2024.instDecidablePredMoodHeadOpens m = Grano2024.instDecidablePredMoodHeadOpens._aux_1 m

def Grano2024.MoodHead.denote {W : Type u_1} {Ev : Type u_2} (m : MoodHead) (P : W → Ev → Prop) : (W → Prop) ⊕ (W → Ev → Prop)

The denotation of a mood head applied to its clause: a proposition once the eventuality argument is closed, the clause's own predicate of eventualities otherwise. The indicative and the first subjunctive denote alike, which is why section 7 adds a second departure from the default to keep the subjunctive out of indicative environments.

Equations

• m.denote P = if m.Opens then Sum.inr P else Sum.inl (Event.closure P)

theorem Grano2024.MoodHead.isRight_denote {W : Type u_1} {Ev : Type u_2} {m : MoodHead} {P : W → Ev → Prop} : (m.denote P).isRight = true ↔ m.Opens

A head's clause offers an open predicate of eventualities exactly when the head opens.

theorem Grano2024.MoodHead.denote_indic_eq_sbjv₁ {W : Type u_1} {Ev : Type u_2} (P : W → Ev → Prop) : indic.denote P = sbjv₁.denote P

(87a) and (88a): the indicative and the first subjunctive denote alike.

theorem Grano2024.MoodHead.mood_of_opens {m : MoodHead} (h : m.Opens) : m.mood = Mood.Grammatical.subjunctive

Premise 3, one direction: a clause with an open eventuality argument is not indicative.

theorem Grano2024.MoodHead.not_opens_sbjv₁ : ¬sbjv₁.Opens

The other direction fails: the first subjunctive closes the argument as the indicative does.

def Grano2024.Complement.heads : Complement → List MoodHead

The mood heads a complement type may carry.

Equations

• Grano2024.Complement.indicative.heads = [Grano2024.MoodHead.indic]
• x✝.heads = [Grano2024.MoodHead.sbjv₁, Grano2024.MoodHead.sbjv₂]

def Grano2024.Complement.Abstracts (c : Complement) : Prop

Premise 3 for complement types: some head of the complement leaves its eventuality argument open.

Equations

• c.Abstracts = ∃ m ∈ c.heads, m.Opens

@[instance_reducible]

instance Grano2024.instDecidableAbstracts (c : Complement) : Decidable c.Abstracts

Equations

• Grano2024.instDecidableAbstracts c = id inferInstance

theorem Grano2024.Complement.abstracts_iff {c : Complement} : c.Abstracts ↔ c ≠ indicative

inductive Grano2024.Reading : Type

The reading a row is judged on, where the predicate has more than one.

• intention : Reading
• belief : Reading
• assertion : Reading
• foresee : Reading

  plan as 'regard as fixed for planning purposes', section 6.1.

• event : Reading
• proposition : Reading

@[instance_reducible]

instance Grano2024.instDecidableEqReading : DecidableEq Reading

Equations

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

def Grano2024.instReprReading.repr : Reading → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Grano2024.instReprReading.repr Grano2024.Reading.intention prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grano2024.Reading.intention")).group prec✝
• Grano2024.instReprReading.repr Grano2024.Reading.belief prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grano2024.Reading.belief")).group prec✝
• Grano2024.instReprReading.repr Grano2024.Reading.assertion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grano2024.Reading.assertion")).group prec✝
• Grano2024.instReprReading.repr Grano2024.Reading.foresee prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grano2024.Reading.foresee")).group prec✝
• Grano2024.instReprReading.repr Grano2024.Reading.event prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grano2024.Reading.event")).group prec✝

@[instance_reducible]

instance Grano2024.instReprReading : Repr Reading

Equations

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

inductive Grano2024.Diagnostic : Type

The logical diagnostics of section 3: an impossible prejacent, two incompatible prejacents, and a prejacent with a rejected superset.

• realism : Diagnostic
• consistency : Diagnostic
• monotonicity : Diagnostic

@[instance_reducible]

instance Grano2024.instDecidableEqDiagnostic : DecidableEq Diagnostic

Equations

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

def Grano2024.instReprDiagnostic.repr : Diagnostic → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Grano2024.instReprDiagnostic : Repr Diagnostic

Equations

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

@[instance_reducible]

instance Grano2024.instFintypeDiagnostic : Fintype Diagnostic

Equations

• Grano2024.instFintypeDiagnostic = { elems := { val := ↑Grano2024.Diagnostic.enumList, nodup := Grano2024.Diagnostic.enumList_nodup }, complete := Grano2024.instFintypeDiagnostic._proof_1 }

structure Grano2024.Row : Type

A judged complement clause.

• language : Glottocode
• cls : Class
• complement : Complement
• reading : Option Reading
• diagnostic : Option Diagnostic
• judgment : Judgment

@[instance_reducible]

instance Grano2024.instDecidableEqRow : DecidableEq Row

Equations

• Grano2024.instDecidableEqRow = Grano2024.instDecidableEqRow.decEq

def Grano2024.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Grano2024.instReprRow : Repr Row

Equations

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

def Grano2024.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

def Grano2024.Row.ofDatum (ex : Datum) : Option Row

Equations

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

def Grano2024.rows : List Row

The paper's judged complements, sections 2, 3, 6, and 7.

Equations

• Grano2024.rows = List.filterMap Grano2024.Row.ofDatum Grano2024.Examples.all

theorem Grano2024.rows_length : rows.length = Examples.all.length

Every example of the paper is a row.

Premises 1 and 2 and the conclusion, over the pool

def Grano2024.Class.RequiresAbstraction (c : Class) : Prop

The classes whose semantics relates to an eventuality: intention through the causal self-reference of Premises 1 and 2, causation, the intention-rigid predicates, and aspect.

Equations

• c.RequiresAbstraction = (c = Grano2024.Class.intend ∨ c = Grano2024.Class.causative ∨ c = Grano2024.Class.intentionRigid ∨ c = Grano2024.Class.aspectual)

@[instance_reducible]

instance Grano2024.instDecidablePredClassRequiresAbstraction : DecidablePred Class.RequiresAbstraction

Equations

• Grano2024.instDecidablePredClassRequiresAbstraction c = id inferInstance

def Grano2024.Row.RequiresAbstraction (r : Row) : Prop

A row requires eventuality abstraction by its class or by an intention or event reading.

Equations

• r.RequiresAbstraction = (r.cls.RequiresAbstraction ∨ r.reading = some Grano2024.Reading.intention ∨ r.reading = some Grano2024.Reading.event)

@[instance_reducible]

instance Grano2024.instDecidablePredRowRequiresAbstraction : DecidablePred Row.RequiresAbstraction

Equations

• Grano2024.instDecidablePredRowRequiresAbstraction r = id inferInstance

theorem Grano2024.abstraction_rejects_indicative (r : Row) : r ∈ rows → r.RequiresAbstraction → r.complement = Complement.indicative → r.judgment ≠ Judgment.acceptable

The conclusion (72d) over the pool: wherever abstraction is required the indicative is rejected, and where the same predicate takes an indicative complement it is read as belief, assertion, foresight, or a proposition instead.

theorem Grano2024.abstraction_accepts_open (c : Class) : c.RequiresAbstraction → ∃ r ∈ rows, r.cls = c ∧ r.complement.Abstracts ∧ r.judgment = Judgment.acceptable

Each class that requires abstraction has an acceptable open complement in the pool.

theorem Grano2024.want_rejects_indicative (r : Row) : r ∈ rows → r.cls = Class.want → r.complement = Complement.indicative → r.judgment ≠ Judgment.acceptable

'want' rejects the indicative throughout, the idle desire of (128) included.

theorem Grano2024.hope_varies : (∃ r ∈ rows, r.cls = Class.hope ∧ r.complement = Complement.indicative ∧ r.judgment = Judgment.acceptable) ∧ ∃ r ∈ rows, r.cls = Class.hope ∧ r.complement = Complement.indicative ∧ r.judgment = Judgment.ungrammatical

'hope' varies: Spanish rejects the indicative, the other languages accept it.

Table 1 and the fragment entries

def Grano2024.Complement.coding? : Complement → Option Complement.Coding

The finite moods among the complement types, as codings of a clausal argument position.

Equations

• Grano2024.Complement.indicative.coding? = some Complement.Coding.indicative
• Grano2024.Complement.subjunctive.coding? = some Complement.Coding.subjunctive
• x✝.coding? = none

def Grano2024.verbOf : Glottocode → Class → Option Verb

The fragment verb for a language and a class of Table 1.

Equations

• Grano2024.verbOf "stan1288" Grano2024.Class.want = some Spanish.Verbs.querer
• Grano2024.verbOf "stan1288" Grano2024.Class.hope = some Spanish.Verbs.esperar
• Grano2024.verbOf "stan1288" Grano2024.Class.causative = some Spanish.Verbs.hacer
• Grano2024.verbOf "port1283" Grano2024.Class.want = some Portuguese.Verbs.querer
• Grano2024.verbOf "port1283" Grano2024.Class.hope = some Portuguese.Verbs.esperar
• Grano2024.verbOf "port1283" Grano2024.Class.intend = some Portuguese.Verbs.pretender
• Grano2024.verbOf "port1283" Grano2024.Class.causative = some Portuguese.Verbs.fazer
• Grano2024.verbOf "ital1282" Grano2024.Class.want = some Italian.Verbs.volere.toVerb
• Grano2024.verbOf "ital1282" Grano2024.Class.hope = some Italian.Verbs.sperare.toVerb
• Grano2024.verbOf "ital1282" Grano2024.Class.intend = some Italian.Verbs.intendere.toVerb
• Grano2024.verbOf "ital1282" Grano2024.Class.causative = some Italian.Verbs.fare.toVerb
• Grano2024.verbOf "mode1248" Grano2024.Class.want = some Greek.StandardModern.Verbs.thelo
• Grano2024.verbOf "mode1248" Grano2024.Class.hope = some Greek.StandardModern.Verbs.elpizo
• Grano2024.verbOf "mode1248" Grano2024.Class.intend = some Greek.StandardModern.Verbs.protitheme
• Grano2024.verbOf "mode1248" Grano2024.Class.causative = some Greek.StandardModern.Verbs.vazo
• Grano2024.verbOf "roma1327" Grano2024.Class.want = some Romanian.Verbs.a_vrea
• Grano2024.verbOf "roma1327" Grano2024.Class.hope = some Romanian.Verbs.a_spera
• Grano2024.verbOf "roma1327" Grano2024.Class.intend = some Romanian.Verbs.a_intentiona
• Grano2024.verbOf "roma1327" Grano2024.Class.causative = some Romanian.Verbs.a_face
• Grano2024.verbOf x✝¹ x✝ = none

def Grano2024.cells : List (Glottocode × Class)

The cells of Table 1 with a verb entry, and the causatives of section 2.2. Spanish 'intend' is the nominal tener la intención, and the French and English entries do not record finite mood.

Equations

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

theorem Grano2024.verbOf_isSome (c : Glottocode × Class) : c ∈ cells → (verbOf c.1 c.2).isSome = true

Every cell has its verb.

theorem Grano2024.fragments_match_pool (c : Glottocode × Class) : c ∈ cells → ∀ v ∈ verbOf c.1 c.2, ∀ (m : Complement), ∀ k ∈ m.coding?, k ∈ v.codings ↔ ∃ r ∈ rows, r.language = c.1 ∧ r.cls = c.2 ∧ r.complement = m ∧ r.diagnostic = none ∧ r.reading = none ∧ r.judgment = Judgment.acceptable

The fragment entries record the paper's judgments: in each cell the verb has a finite complement in a mood exactly when the pool has an acceptable complement in that mood, outside the rows that test a diagnostic or a second reading.

theorem Grano2024.esperar_varies : Complement.Coding.indicative ∈ Portuguese.Verbs.esperar.codings ∧ Complement.Coding.indicative ∉ Spanish.Verbs.esperar.codings

The variation of 'hope' in two entries with one form: Portuguese esperar takes the indicative and Spanish esperar does not.

Section 3: the logical profile of 'intend'

def Grano2024.Class.Fails (c : Class) (d : Diagnostic) : Prop

The class fails diagnostic d somewhere in the pool.

Equations

• c.Fails d = ∃ r ∈ Grano2024.rows, r.cls = c ∧ r.diagnostic = some d ∧ r.judgment ≠ Judgment.acceptable

@[instance_reducible]

instance Grano2024.instDecidableFails (c : Class) (d : Diagnostic) : Decidable (c.Fails d)

Equations

• Grano2024.instDecidableFails c d = id inferInstance

theorem Grano2024.intend_like_hope_in_logic : (∀ (d : Diagnostic), Class.hope.Fails d ∧ Class.intend.Fails d ∧ ¬Class.want.Fails d) ∧ (∃ r ∈ rows, r.cls = Class.hope ∧ r.complement = Complement.indicative ∧ r.judgment = Judgment.acceptable) ∧ ∀ r ∈ rows, r.cls = Class.intend → r.complement = Complement.indicative → r.judgment ≠ Judgment.acceptable

On realism, consistency, and monotonicity 'intend' patterns with 'hope' and against 'want', yet on mood with 'want': the theories that license the indicative under 'hope' by that profile, [PR20]'s simplification of consistent backgrounds and [GM21]'s optional nonveridicality, predict it under 'intend' as well.

The semantics of intention reports, section 4

(73) is necessity over the worlds compatible with the agent's intentions, □[int]. Its one substantive constraint is that those worlds overlap the worlds compatible with the agent's beliefs, ◇[int] (w ~[dox] ·) w, from which realism, consistency, and monotonicity follow. (78) moves to the de se triples of an intention state, and (79) adds the causal self-reference, closing the complement's eventuality argument over what the state causes.

theorem Grano2024.realism {W : Type u_1} {int dox : SetRel W W} {p : W → Prop} {w : W} (h : ModalLogic.Diamond int (fun (x : W) => (w, x) ∈ dox) w) (hp : ModalLogic.Box int p w) : ModalLogic.Diamond dox p w

Realism: what is intended is believed possible.

theorem Grano2024.consistency {W : Type u_1} {int dox : SetRel W W} {p q : W → Prop} {w : W} (h : ModalLogic.Diamond int (fun (x : W) => (w, x) ∈ dox) w) (hp : ModalLogic.Box int p w) (hq : ModalLogic.Box int q w) : ModalLogic.Diamond dox (fun (v : W) => p v ∧ q v) w

Consistency: two intentions are believed jointly possible, by realism for their conjunction.

theorem Grano2024.monotonicity {W : Type u_1} {int : SetRel W W} {p q : W → Prop} {w : W} (hpq : p ≤ q) (hp : ModalLogic.Box int p w) : ModalLogic.Box int q w

Monotonicity: intending the narrower prejacent is intending the wider.

structure Grano2024.IntentionFrame (E : Type u_1) (W : Type u_2) (T : Type u_3) (Ev : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

The ingredients of (78) and (79): intention states, their holders, their content as world, time, and individual triples, and causation in the right way between eventualities.

• intention : Ev → W → Prop
• holder : E → Ev → W → Prop
• content : Ev → Set (W × T × E)
• causeStar : Ev → Ev → W → Prop

def Grano2024.IntentionFrame.Report₃ {E : Type u_1} {W : Type u_2} {T : Type u_3} {Ev : Type u_4} [LT T] (F : IntentionFrame E W T Ev) (x : E) (Q : E → T → W → Prop) (w : W) : Prop

(78): x intends Q at w when some intention state of x has, at every triple of its content, a later time at which Q holds. The complement is a property of individuals, times, and worlds, which an indicative clause can supply.

Equations

• F.Report₃ x Q w = ∃ (s : Ev), F.intention s w ∧ F.holder x s w ∧ ∀ c ∈ F.content s, ∃ t > c.2.1, Q c.2.2 t c.1

def Grano2024.IntentionFrame.Report {E : Type u_1} {W : Type u_2} {T : Type u_3} {Ev : Type u_4} [LT T] (F : IntentionFrame E W T Ev) (x : E) (P : E → T → W → Ev → Prop) (w : W) : Prop

(79): as (78), but at every triple of its content the state causes in the right way an eventuality of the complement at a later time. The complement keeps its eventuality argument, closed here over what the state causes.

Equations

• F.Report x P w = ∃ (s : Ev), F.intention s w ∧ F.holder x s w ∧ ∀ c ∈ F.content s, Event.causedClosure F.causeStar s (fun (w' : W) (e : Ev) => ∃ t > c.2.1, P c.2.2 t w' e) c.1

theorem Grano2024.IntentionFrame.Report.mono {E : Type u_1} {W : Type u_2} {T : Type u_3} {Ev : Type u_4} [LT T] {F : IntentionFrame E W T Ev} {x : E} {P : E → T → W → Ev → Prop} {w : W} {Q : E → T → W → Ev → Prop} (hPQ : ∀ (y : E) (t : T) (w : W) (e : Ev), P y t w e → Q y t w e) (h : F.Report x P w) : F.Report x Q w

Monotonicity survives the causal self-reference: a report of the narrower complement is a report of the wider.

theorem Grano2024.IntentionFrame.Report.report₃ {E : Type u_1} {W : Type u_2} {T : Type u_3} {Ev : Type u_4} [LT T] {F : IntentionFrame E W T Ev} {x : E} {P : E → T → W → Ev → Prop} {w : W} (h : F.Report x P w) : F.Report₃ x (fun (y : E) (t : T) => Event.closure (P y t)) w

The causally self-referential report entails the report of the closed complement.

theorem Grano2024.IntentionFrame.report_iff_report₃ {E : Type u_1} {W : Type u_2} {T : Type u_3} {Ev : Type u_4} [LT T] {F : IntentionFrame E W T Ev} {x : E} {P : E → T → W → Ev → Prop} {w : W} (h : ∀ (s e : Ev) (w : W), F.causeStar s e w) : F.Report x P w ↔ F.Report₃ x (fun (y : E) (t : T) => Event.closure (P y t)) w

When every state causes every eventuality, (79) says no more than (78) of the closed complement. Otherwise its prejacent is not a function of the closed complement (Event.causedClosure_factorsThrough_iff).

def Grano2024.sbjvCausal {W : Type u_1} {Ev : Type u_2} (content : Ev → W → Prop) (causeStar : Ev → Ev → W → Prop) (P : W → Ev → Prop) (s : Ev) : Prop

The subjunctive of (134), for a theory that moves the modal quantification from 'intend' into the mood head: simple necessity over the content worlds of the attitude state, with the causally self-referential prejacent.

Equations

• Grano2024.sbjvCausal content causeStar P s = ∀ (w : W), content s w → Event.causedClosure causeStar s P w

Section 7: the two departures from default clausal semantics

def Grano2024.Class.TwoBackgrounds (c : Class) : Prop

A class whose reports carry two modal backgrounds, the doxastic-like and the bouletic ([PR20]); 'intend' is taken to carry one, the paper's footnote 50.

Equations

• c.TwoBackgrounds = (c = Grano2024.Class.want ∨ c = Grano2024.Class.hope)

@[instance_reducible]

instance Grano2024.instDecidablePredClassTwoBackgrounds : DecidablePred Class.TwoBackgrounds

Equations

• Grano2024.instDecidablePredClassTwoBackgrounds c = id inferInstance

def Grano2024.Class.Simplifiable (c : Class) : Prop

[PR20]'s simplification read off the pool: the pair may collapse to one background when the class requires its backgrounds to be consistent, that is, rejects inconsistent prejacents.

Equations

• c.Simplifiable = c.Fails Grano2024.Diagnostic.consistency

@[instance_reducible]

instance Grano2024.instDecidablePredClassSimplifiable : DecidablePred Class.Simplifiable

Equations

• Grano2024.instDecidablePredClassSimplifiable c = id inferInstance

def Grano2024.Class.IndicativePossible (c : Class) : Prop

The indicative is available when neither departure is in force: no eventuality abstraction, and a single background or a pair that may simplify.

Equations

• c.IndicativePossible = (¬c.RequiresAbstraction ∧ (¬c.TwoBackgrounds ∨ c.Simplifiable))

@[instance_reducible]

instance Grano2024.instDecidablePredClassIndicativePossible : DecidablePred Class.IndicativePossible

Equations

• Grano2024.instDecidablePredClassIndicativePossible c = id inferInstance

theorem Grano2024.indicative_possible_iff (c : Class) : c ∈ [Class.want, Class.hope, Class.intend, Class.causative] → (c.IndicativePossible ↔ ∃ r ∈ rows, r.cls = c ∧ r.complement = Complement.indicative ∧ r.judgment = Judgment.acceptable)

For the four classes of sections 2 and 3, the indicative is possible exactly when the pool has an acceptable indicative complement for the class.