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.

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.

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

Inertial modal parameters: circumstantial base + inertial ordering.

• circumstances : Semantics.Modality.Kratzer.ModalBase W

  Circumstantial modal base: facts holding at the evaluation world.

• inertia : Semantics.Modality.Kratzer.OrderingSource W

  Inertial ordering: propositions describing normal continuation.

def FuscoSgrizzi2026.InertialParams.toKratzer {W : Type u_1} (p : InertialParams W) : Semantics.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 = Semantics.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 = Semantics.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 : Semantics.Modality.Kratzer.ModalBase W) (prop : W → Prop) (w : W) : inertialNecessity { circumstances := circ, inertia := Semantics.Modality.Kratzer.emptyBackground } prop w ↔ Semantics.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 : Semantics.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 = Semantics.Modality.ModalFlavor.circumstantial