Inertial modality for Italian non-finite belief/action readings

[FS26] [Dow79] [Kra12]

[FS26] analyse the belief/action ambiguity of Italian non-finite complements (convincere a + INF, promettere di + INF) via inertial modality in the [Dow79] sense, recast as a Kratzer circumstantial-base + inertial-ordering pair.

Main declarations

• InertialParams: bundles a circumstantial modal base with an inertial ordering source.
• inertialNecessity, inertialPossibility: □/◇ over the best-inertial-continuation worlds.
• inertial_duality: modal duality, delegated to Kratzer.duality.
• empty_inertia_is_simple: with an empty ordering source, inertial necessity collapses to circumstantial simpleNecessity.
• CausativeAttitude: the single denotation of convincere-type verbs (their ex. 24), with beliefReading/intentionReading the two complement-size construals and the reading diagnostics.

Implementation notes

[Dow79]: w' is an inertia world of w iff w' matches w up to the reference time and the course of events in w continues without interruption. In Kratzer's framework this is a circumstantial modal base paired with an ordering source whose propositions describe normal continuation.

Readings from complement size

The paper's structural hypothesis: a single rational attitude semantics whose belief or intention construal is fixed by complement size. A phase-sized (CP) complement is existentially closed into a proposition and evaluated against doxastic content; a smaller complement leaves the event variable open and is evaluated against inertial continuation.

inductive FuscoSgrizzi2026.Reading : Type

The two construals of a rational attitude verb: propositional belief, evaluated against doxastic content, or sub-propositional intention, evaluated against inertial continuation.

• belief : Reading
• intention : Reading

@[instance_reducible]

instance FuscoSgrizzi2026.instDecidableEqReading : DecidableEq Reading

Equations

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

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

Equations

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

@[instance_reducible]

instance FuscoSgrizzi2026.instReprReading : Repr Reading

Equations

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

def FuscoSgrizzi2026.readingFromSize (cs : Minimalist.ComplementSize) : Reading

The construal determined by complement size: a phase-sized (CP) complement is read as belief, a smaller one as intention.

Equations

• FuscoSgrizzi2026.readingFromSize cs = if cs.isPhaseSized = true then FuscoSgrizzi2026.Reading.belief else FuscoSgrizzi2026.Reading.intention

theorem FuscoSgrizzi2026.readingFromSize_eq_belief_iff (cs : Minimalist.ComplementSize) : readingFromSize cs = Reading.belief ↔ Minimalist.fValue Minimalist.Cat.C ≤ cs.fLevel

Complement size determines the construal, with the CP phase boundary as the threshold.

The Italian di/a alternation

The paper's core data: di-infinitives are CP-sized (their ex. 22 places a-infinitives at aP, mapped here to the nearest available ComplementSize below the CP threshold), so the di/a choice deterministically fixes the reading of convincere-type verbs. The lexical entries live in Fragments/Italian/Predicates.lean.

def FuscoSgrizzi2026.InfComplementizer.complementSize : Italian.Predicates.InfComplementizer → Minimalist.ComplementSize

The complement size selected by each Italian infinitival complementizer.

Equations

• FuscoSgrizzi2026.InfComplementizer.complementSize Italian.Predicates.InfComplementizer.di = Minimalist.ComplementSize.cP
• FuscoSgrizzi2026.InfComplementizer.complementSize Italian.Predicates.InfComplementizer.a_ = Minimalist.ComplementSize.vP

def FuscoSgrizzi2026.InfComplementizer.reading : Italian.Predicates.InfComplementizer → Reading

The reading derived from each complementizer.

Equations

• FuscoSgrizzi2026.InfComplementizer.reading = FuscoSgrizzi2026.readingFromSize ∘ FuscoSgrizzi2026.InfComplementizer.complementSize

theorem FuscoSgrizzi2026.di_yields_belief : InfComplementizer.reading Italian.Predicates.InfComplementizer.di = Reading.belief

di-infinitives yield belief readings.

theorem FuscoSgrizzi2026.a_yields_intention : InfComplementizer.reading Italian.Predicates.InfComplementizer.a_ = Reading.intention

a-infinitives yield intention readings.

theorem FuscoSgrizzi2026.convincere_dual_reading : List.map InfComplementizer.reading Italian.Predicates.convincere.infComplements = [Reading.belief, Reading.intention]

convincere supports both readings, one per complementizer.

theorem FuscoSgrizzi2026.credere_belief_only : List.map InfComplementizer.reading Italian.Predicates.credere.infComplements = [Reading.belief]

credere supports only the belief reading.

theorem FuscoSgrizzi2026.convincere_alternation_is_structural : InfComplementizer.complementSize Italian.Predicates.InfComplementizer.di ≠ InfComplementizer.complementSize Italian.Predicates.InfComplementizer.a_ ∧ InfComplementizer.reading Italian.Predicates.InfComplementizer.di ≠ InfComplementizer.reading Italian.Predicates.InfComplementizer.a_

The di/a alternation in convincere is structurally grounded: the two complementizers select different complement sizes, which deterministically map to different readings.

structure FuscoSgrizzi2026.InertialParams (W : Type u_2) : Type u_2

Inertial modal parameters: circumstantial base + inertial ordering.

• circumstances : Modality.Kratzer.ModalBase W

  Circumstantial modal base: facts holding at the evaluation world.

• inertia : Modality.Kratzer.OrderingSource W

  Inertial ordering: propositions describing normal continuation.

def FuscoSgrizzi2026.InertialParams.toKratzer {W : Type u_1} (p : InertialParams W) : Modality.Kratzer.KratzerParams W

Extract Kratzer parameters from inertial parameters.

Equations

• p.toKratzer = { base := p.circumstances, ordering := p.inertia }

def FuscoSgrizzi2026.inertialNecessity {W : Type u_1} (p : InertialParams W) (prop : W → Prop) (w : W) : Prop

Inertial necessity: p holds in all best (most inertial) circumstantially accessible worlds. For intention readings: in all worlds where the experiencer's current course of action continues uninterrupted, the intended event obtains.

Equations

• FuscoSgrizzi2026.inertialNecessity p prop w = Modality.Kratzer.necessity p.circumstances p.inertia prop w

def FuscoSgrizzi2026.inertialPossibility {W : Type u_1} (p : InertialParams W) (prop : W → Prop) (w : W) : Prop

Inertial possibility: p holds in some best circumstantially accessible world.

Equations

• FuscoSgrizzi2026.inertialPossibility p prop w = Modality.Kratzer.possibility p.circumstances p.inertia prop w

theorem FuscoSgrizzi2026.inertial_duality {W : Type u_1} (p : InertialParams W) (prop : W → Prop) (w : W) : inertialNecessity p prop w ↔ ¬inertialPossibility p (fun (w' : W) => ¬prop w') w

Inertial modality satisfies modal duality: □p ↔ ¬◇¬p.

theorem FuscoSgrizzi2026.empty_inertia_is_simple {W : Type u_1} (circ : Modality.Kratzer.ModalBase W) (prop : W → Prop) (w : W) : inertialNecessity { circumstances := circ, inertia := Modality.Kratzer.emptyBackground } prop w ↔ Modality.Kratzer.simpleNecessity circ prop w

With empty inertial ordering, inertial modality reduces to simple circumstantial necessity (no preference among accessible worlds).

def FuscoSgrizzi2026.InertialParams.flavorTag : Modality.ModalFlavor

Inertial modality maps to the circumstantial flavor tag. Both inertial and teleological modality concern what happens given the facts — they differ only in ordering source, not modal base.

Equations

• FuscoSgrizzi2026.InertialParams.flavorTag = Modality.ModalFlavor.circumstantial

The single denotation of convincere (ex. 24)

⟦convincere⟧ = λP.λx.λy.λe. ∃e'. Convince(e) ∧ Agent(e,y) ∧ Patient(e,x) ∧ CAUSE(e,e') ∧ RATIONAL-ATTITUDE(e') ∧ Experiencer(x,e') ∧ P(e'). The parameter P is supplied by the complement: a di-infinitive (CP) is existentially closed, yielding the belief reading; an a-infinitive (aP) leaves the event variable open, yielding the intention reading. The belief/intention split is compositional — one verb, two complement sizes.

structure FuscoSgrizzi2026.CausativeAttitude (E : Type u_2) (Time : Type u_3) [LinearOrder Time] : Type (max u_2 u_3)

A causative attitude verb: the agent causes the experiencer to enter a rational attitude state whose content is the complement predicate.

• verbPred : Event Time → Prop

  The verb's descriptive predicate (Convince).

• agent : E

  The agent of the matrix event.

• experiencer : E

  The patient of the matrix event and experiencer of the attitude.

• isAgent : Event Time → E → Prop

  Agent thematic role.

• isPatient : Event Time → E → Prop

  Patient thematic role.

• isExperiencer : Event Time → E → Prop

  Experiencer thematic role, on the attitude event.

• cause : Event Time → Event Time → Prop

  The matrix event causally brings about the attitude state.

def FuscoSgrizzi2026.CausativeAttitude.denote {E : Type u_2} {Time : Type u_3} [LinearOrder Time] (v : CausativeAttitude E Time) (P : Event Time → Prop) : Prop

The verb applied to a complement predicate P: some matrix event causes a stative rational-attitude event satisfying P.

Equations

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

def FuscoSgrizzi2026.CausativeAttitude.beliefReading {E : Type u_2} {Time : Type u_3} [LinearOrder Time] (v : CausativeAttitude E Time) (embeddedVP : Event Time → Prop) : Prop

Belief reading: the CP complement is existentially closed into a proposition, evaluated against doxastic content.

Equations

• v.beliefReading embeddedVP = v.denote fun (x : Event Time) => ∃ (e : Event Time), embeddedVP e

def FuscoSgrizzi2026.CausativeAttitude.intentionReading {E : Type u_2} {Time : Type u_3} [LinearOrder Time] (v : CausativeAttitude E Time) (embeddedVP : Event Time → Prop) : Prop

Intention reading: the sub-CP complement is applied directly as an event predicate, evaluated against inertial continuation.

Equations

• v.intentionReading embeddedVP = v.denote embeddedVP

theorem FuscoSgrizzi2026.CausativeAttitude.readings_from_single_denote {E : Type u_2} {Time : Type u_3} [LinearOrder Time] (v : CausativeAttitude E Time) (VP : Event Time → Prop) : (v.beliefReading VP = v.denote fun (x : Event Time) => ∃ (e : Event Time), VP e) ∧ v.intentionReading VP = v.denote VP

The paper's central claim (ex. 24): both readings are the one denote applied to different complement predicates — the belief/intention split is compositional, not lexical.

Reading diagnostics

The paper's empirical differentiators of the two construals: belief readings are truth-assessable and host modal auxiliaries; intention readings are obligatorily future-oriented and object-control.

def FuscoSgrizzi2026.truthAssessable : Reading → Bool

"It's true/false" can felicitously evaluate a belief but not an intention.

Equations

• FuscoSgrizzi2026.truthAssessable FuscoSgrizzi2026.Reading.belief = true
• FuscoSgrizzi2026.truthAssessable FuscoSgrizzi2026.Reading.intention = false

def FuscoSgrizzi2026.allowsModalAux : Reading → Bool

CP complements host modal auxiliary heads; sub-CP complements lack the structural space.

Equations

• FuscoSgrizzi2026.allowsModalAux FuscoSgrizzi2026.Reading.belief = true
• FuscoSgrizzi2026.allowsModalAux FuscoSgrizzi2026.Reading.intention = false

def FuscoSgrizzi2026.forcedFutureOrientation : Reading → Bool

The intended event is projected into inertia worlds, so intention readings are obligatorily future-oriented.

Equations

• FuscoSgrizzi2026.forcedFutureOrientation FuscoSgrizzi2026.Reading.belief = false
• FuscoSgrizzi2026.forcedFutureOrientation FuscoSgrizzi2026.Reading.intention = true

def FuscoSgrizzi2026.objectControlOnly : Reading → Bool

The experiencer must be the agent of the intended event, so intention readings are obligatorily object-control.

Equations

• FuscoSgrizzi2026.objectControlOnly FuscoSgrizzi2026.Reading.belief = false
• FuscoSgrizzi2026.objectControlOnly FuscoSgrizzi2026.Reading.intention = true

Connection to Grano 2024: size → reading → mood

[Gra24]'s hybrid-predicate analysis (his §6.2) and this paper's complement-size analysis make the same prediction: the complement's structural size determines whether the reading is intentional (requiring eventuality abstraction, hence subjunctive) or propositional (existentially closed, hence indicative-compatible). readingFromSize composed with readingToDeparture and Grano2024.DepartureKind.moodPrediction gives the end-to-end chain complement size → reading → departure kind → mood prediction.

def FuscoSgrizzi2026.readingToDeparture : Reading → Option Grano2024.DepartureKind

Map a reading to a [Gra24] departure kind: intention readings require eventuality abstraction; belief readings are the default clausal semantics, no departure.

Equations

• FuscoSgrizzi2026.readingToDeparture FuscoSgrizzi2026.Reading.intention = some Grano2024.DepartureKind.eventualityAbstraction
• FuscoSgrizzi2026.readingToDeparture FuscoSgrizzi2026.Reading.belief = none

theorem FuscoSgrizzi2026.intention_predicts_subjunctive : Option.map Grano2024.DepartureKind.moodPrediction (readingToDeparture Reading.intention) = some Mood.Selector.subjunctiveSelecting

Intention readings predict robust subjunctive selection.

theorem FuscoSgrizzi2026.belief_predicts_no_departure : readingToDeparture Reading.belief = none

Belief readings predict no departure (default indicative).

theorem FuscoSgrizzi2026.subcp_to_subjunctive : readingFromSize Minimalist.ComplementSize.vP = Reading.intention ∧ readingToDeparture (readingFromSize Minimalist.ComplementSize.vP) = some Grano2024.DepartureKind.eventualityAbstraction ∧ Option.map Grano2024.DepartureKind.moodPrediction (readingToDeparture (readingFromSize Minimalist.ComplementSize.vP)) = some Mood.Selector.subjunctiveSelecting

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

theorem FuscoSgrizzi2026.cp_to_indicative : readingFromSize Minimalist.ComplementSize.cP = Reading.belief ∧ readingToDeparture (readingFromSize Minimalist.ComplementSize.cP) = none

End-to-end: CP complement → belief → no departure.