Fusco and Sgrizzi (2026): Belief or Action? Semantic Ambiguity in the Italian Non-finite Domain

This file formalizes [FS26]'s account of the belief and intention readings of Italian convincere 'convince' with its two infinitival complements: Marco ha convinto Gianni di avere un figlio reports a belief, Marco ha convinto Gianni a avere un figlio an intention. Where [Gra24] ties the alternation to mood and finiteness, the paper ties it to the size of the complement. The di-infinitive is a CP: it hosts modal auxiliaries, allows subject as well as object control, and can be assessed for truth. The a-infinitive stops below tense and above vP: it hosts negation, passive and low aspectual verbs and forms a temporal domain of its own, but blocks clitic climbing and subject control and cannot be assessed for truth. The readings follow from the size through one lexical entry: convincere causes a rational-attitude state with the property its complement supplies (Frame.convincere, the paper's (24)). A di-complement closes the eventuality argument of the bare infinitive into a proposition, which di quantifies over the state's content worlds; an a-complement keeps it open, and a, anchored to the state, quantifies over the state's inertia worlds and binds the event to the state by the causal relation (aP). Both heads are Kratzer necessity over backgrounds the state projects, the event-relative modality of [Hac10]: di over a content background, a over a circumstantial base ordered by inertia ([Dow79], [Kra13]). This is the causal self-referentiality of intention ([Sea83]): in every inertia world the intended event is caused by the attitude state, hence later than it, the future orientation of a-infinitives ([Wur14]; intention_future). Complement size is the extended projection's ComplementSize, ordered by functional level; the reading is read off the CP threshold, and the diagnostics of sections 3 and 3.1 are predicted by the heads the complement reaches (rows_predicted).

Implementation notes

• The a-infinitive is recorded with negation as its highest head, the highest the paper places inside it. The functional sequence does not separate negation from tense and modal heads, so the absence of modal auxiliaries ((9) and (10)) and the ban on past-oriented complements ((5)) stay in the prose and in intention_future.
• The two heads are stated over abstract eventualities and worlds, with the content background, the circumstantial base and the inertial ordering as anchoring functions of the state. The closure head (23b) is Event.closure and the prejacent of a is Event.causedClosure, the operators of [Gra24]'s account, so a complement takes its world before its eventuality.
• The examples are Data.Examples.FuscoSgrizzi2026; the lexical entries are those of Fragments/Romance/Italian/Verbs.lean.

References

• [FS26]
• [Gra24]
• [Sea83]
• [Wur14]
• [Dow79]
• [Kra13]
• [Hac10]
• [Riz97]

def FuscoSgrizzi2026.aP {V : Type u_2} {W : Type u_3} (circumstances inertia : V → Modality.Background W) (causeStar : V → V → W → Prop) (P : W → V → Prop) (s : V) (w : W) : Prop

The head a (25), anchored to the attitude state, is necessity over the state's inertia worlds, the best worlds of a circumstantial base under an inertial ordering ([Dow79], [Kra13]), with the eventuality argument of its complement closed over what the state causes.

Equations

• FuscoSgrizzi2026.aP circumstances inertia causeStar P s w = Modality.necessity (circumstances s) (inertia s) (Event.causedClosure causeStar s P) w

theorem FuscoSgrizzi2026.aP_bot {V : Type u_2} {W : Type u_3} (circumstances : V → Modality.Background W) (causeStar : V → V → W → Prop) (P : W → V → Prop) (s : V) (w : W) : aP circumstances (fun (x : V) => ⊥) causeStar P s w ↔ Grano2024.sbjvCausal (fun (s : V) (w' : W) => (w, w') ∈ (circumstances s).accessible) causeStar P s

The head a is the causal subjunctive of [Gra24]'s (134) with an inertial ordering added: with no ordering it is simple necessity of the same prejacent over the circumstantially accessible worlds.

def FuscoSgrizzi2026.diP {V : Type u_2} {W : Type u_3} (content : V → Modality.Background W) (Q : W → Prop) (s : V) (w : W) : Prop

The head di (26) is necessity over the state's content worlds of a proposition.

Equations

• FuscoSgrizzi2026.diP content Q s w = Modality.simpleNecessity (content s) Q w

structure FuscoSgrizzi2026.Frame (I : Type u_4) (V : Type u_5) (W : Type u_6) : Type (max (max u_4 u_5) u_6)

The relations the denotation (24) draws on, convincing events, the thematic relations, causation between eventualities, and the class of rational attitudes.

• convince : V → W → Prop
• agent : V → I → W → Prop
• patient : V → I → W → Prop
• cause : V → V → Prop
• rationalAttitude : V → Prop
• experiencer : I → V → Prop

def FuscoSgrizzi2026.Frame.convincere {I : Type u_1} {V : Type u_2} {W : Type u_3} (F : Frame I V W) (P : V → Prop) (x y : I) (e : V) (w : W) : Prop

⟦convincere⟧ (24) holds when an event of y convincing x causes a rational-attitude state of x with the property P the complement supplies.

Equations

• F.convincere P x y e w = ∃ (s : V), F.convince e w ∧ F.agent e y w ∧ F.patient e x w ∧ F.cause e s ∧ F.rationalAttitude s ∧ F.experiencer x s ∧ P s

def FuscoSgrizzi2026.beliefReport {I : Type u_1} {V : Type u_2} {W : Type u_3} (F : Frame I V W) (content : V → Modality.Background W) (P : W → V → Prop) (x y : I) (e : V) (w : W) : Prop

The belief report is convincere with the di-complement, whose closure head (23b) turns the bare infinitive into a proposition held at the state's content worlds.

Equations

• FuscoSgrizzi2026.beliefReport F content P x y e w = F.convincere (fun (s : V) => FuscoSgrizzi2026.diP content (Event.closure P) s w) x y e w

def FuscoSgrizzi2026.intentionReport {I : Type u_1} {V : Type u_2} {W : Type u_3} (F : Frame I V W) (circumstances inertia : V → Modality.Background W) (causeStar : V → V → W → Prop) (P : W → V → Prop) (x y : I) (e : V) (w : W) : Prop

The intention report is convincere with the a-complement.

Equations

• FuscoSgrizzi2026.intentionReport F circumstances inertia causeStar P x y e w = F.convincere (fun (s : V) => FuscoSgrizzi2026.aP circumstances inertia causeStar P s w) x y e w

theorem FuscoSgrizzi2026.intention_causal {I : Type u_1} {V : Type u_2} {W : Type u_3} (F : Frame I V W) (circumstances inertia : V → Modality.Background W) (causeStar : V → V → W → Prop) (P : W → V → Prop) (x y : I) (e : V) (w : W) (h : intentionReport F circumstances inertia causeStar P x y e w) : ∃ (s : V), F.cause e s ∧ ∀ (w' : W), (w, w') ∈ Modality.bestAccessible (circumstances s) (inertia s) → Event.causedClosure causeStar s P w'

Causal self-referentiality: an intention report puts the attitude state in a causal chain to the intended event throughout the state's inertia worlds.

theorem FuscoSgrizzi2026.intention_future {I : Type u_1} {V : Type u_2} {W : Type u_3} (F : Frame I V W) (circumstances inertia : V → Modality.Background W) (causeStar : V → V → W → Prop) (P : W → V → Prop) (x y : I) (e : V) (w : W) {T : Type u_4} [Preorder T] (τ : V → T) (hτ : ∀ (s e' : V) (w' : W), causeStar s e' w' → τ s < τ e') (h : intentionReport F circumstances inertia causeStar P x y e w) : ∃ (s : V), F.cause e s ∧ ∀ (w' : W), (w, w') ∈ Modality.bestAccessible (circumstances s) (inertia s) → ∃ (e' : V), τ s < τ e' ∧ P w' e'

Future orientation follows when causes precede their effects. The intended event of an intention report lies after the attitude state in every inertia world, which excludes a past-oriented complement, as in (5b).

Readings from complement size

inductive FuscoSgrizzi2026.Reading : Type

The two construals of a rational attitude.

• 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 reading a complement size yields, belief for a phase-sized complement, which carries the closure head, and intention for a smaller one.

Equations

• FuscoSgrizzi2026.readingFromSize cs = if Minimalist.ComplementSize.cP ≤ cs then FuscoSgrizzi2026.Reading.belief else FuscoSgrizzi2026.Reading.intention

def FuscoSgrizzi2026.diSize : Minimalist.ComplementSize

The di-infinitive is a CP (21).

Equations

• FuscoSgrizzi2026.diSize = Minimalist.ComplementSize.cP

def FuscoSgrizzi2026.aSize : Minimalist.ComplementSize

The a-infinitive is a projection below tense with negation as its highest head (22).

Equations

• FuscoSgrizzi2026.aSize = { highestHead := Minimalist.Cat.Neg }

def FuscoSgrizzi2026.sizeOf (z : Complementizer) : Option Minimalist.ComplementSize

The complement an infinitival complementizer of the fragment selects.

Equations

• FuscoSgrizzi2026.sizeOf z = if z = Italian.Verbs.di then some FuscoSgrizzi2026.diSize else if z = Italian.Verbs.a then some FuscoSgrizzi2026.aSize else none

def FuscoSgrizzi2026.readings (v : Italian.Verb) : List Reading

The readings a verb's complementizers yield, in the order the fragment lists them.

Equations

• FuscoSgrizzi2026.readings v = List.filterMap (fun (z : Complementizer) => Option.map FuscoSgrizzi2026.readingFromSize (FuscoSgrizzi2026.sizeOf z)) v.clauseTypers

theorem FuscoSgrizzi2026.convincere_pensare_readings : readings Italian.Verbs.convincere = [Reading.belief, Reading.intention] ∧ readings Italian.Verbs.pensare = [Reading.belief, Reading.intention]

convincere has both readings, one per complementizer (4), and pensare alternates the same way.

The diagnostics of sections 3 and 3.1

inductive FuscoSgrizzi2026.Diagnostic : Type

A property of an infinitival complement the paper tests.

• belief : Diagnostic
• intention : Diagnostic
• truthAssessable : Diagnostic
• subjectControl : Diagnostic
• passive : Diagnostic
• aspectual : Diagnostic
• negation : Diagnostic
• independentTime : Diagnostic
• cliticClimbing : Diagnostic

@[instance_reducible]

instance FuscoSgrizzi2026.instDecidableEqDiagnostic : DecidableEq Diagnostic

Equations

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

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

Equations

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

@[instance_reducible]

instance FuscoSgrizzi2026.instReprDiagnostic : Repr Diagnostic

Equations

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

def FuscoSgrizzi2026.Diagnostic.Predicted : Diagnostic → Minimalist.ComplementSize → Prop

What complement size predicts for a diagnostic, the readings by the phase threshold; truth assessment by propositionality; subject control by the finiteness head that hosts the logophoric centre ([Riz97]); passive, low aspectual verbs and negation by the Voice, v and negation heads; a temporal domain of its own by structure above vP; clitic climbing by a complement no larger than vP.

Equations

• FuscoSgrizzi2026.Diagnostic.belief.Predicted x✝ = (FuscoSgrizzi2026.readingFromSize x✝ = FuscoSgrizzi2026.Reading.belief)
• FuscoSgrizzi2026.Diagnostic.intention.Predicted x✝ = (FuscoSgrizzi2026.readingFromSize x✝ = FuscoSgrizzi2026.Reading.intention)
• FuscoSgrizzi2026.Diagnostic.truthAssessable.Predicted x✝ = (Minimalist.ComplementSize.cP ≤ x✝)
• FuscoSgrizzi2026.Diagnostic.subjectControl.Predicted x✝ = (Minimalist.ComplementSize.finP ≤ x✝)
• FuscoSgrizzi2026.Diagnostic.passive.Predicted x✝ = ({ highestHead := Minimalist.Cat.Voice } ≤ x✝)
• FuscoSgrizzi2026.Diagnostic.aspectual.Predicted x✝ = (Minimalist.ComplementSize.vP ≤ x✝)
• FuscoSgrizzi2026.Diagnostic.negation.Predicted x✝ = ({ highestHead := Minimalist.Cat.Neg } ≤ x✝)
• FuscoSgrizzi2026.Diagnostic.independentTime.Predicted x✝ = (Minimalist.ComplementSize.vP < x✝)
• FuscoSgrizzi2026.Diagnostic.cliticClimbing.Predicted x✝ = (x✝ ≤ Minimalist.ComplementSize.vP)

@[instance_reducible]

instance FuscoSgrizzi2026.instDecidablePredicted (d : Diagnostic) (cs : Minimalist.ComplementSize) : Decidable (d.Predicted cs)

Equations

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

structure FuscoSgrizzi2026.Row : Type

A sentence of the paper carries the size of its infinitival complement, the diagnostic it tests and whether it is grammatical.

• size : Minimalist.ComplementSize
• diagnostic : Diagnostic
• grammatical : Bool

@[instance_reducible]

instance FuscoSgrizzi2026.instDecidableEqRow : DecidableEq Row

Equations

• FuscoSgrizzi2026.instDecidableEqRow = FuscoSgrizzi2026.instDecidableEqRow.decEq

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

Equations

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

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

Equations

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

def FuscoSgrizzi2026.rows : List Row

Equations

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

theorem FuscoSgrizzi2026.rows_predicted (r : Row) : r ∈ rows → (r.grammatical = true ↔ r.diagnostic.Predicted r.size)

The paper's sentences are grammatical exactly where complement size predicts.