Inertial Modality @cite{dowty-1979}

@cite{fusco-sgrizzi-2026} @cite{kratzer-2012}

The inertial ordering source ranks accessible worlds by how well they match the "normal continuation" of the current state of affairs.

Kratzer Parameters

• Modal base: circumstantial (facts holding at the evaluation world)
• Ordering source: inertial (normal continuation without interruption)

Linguistic Application

Inertial modality underpins:

• Progressive aspect: "John was crossing the street" → in inertia worlds, John finishes crossing
• Intention readings: convincere a partire → in inertia worlds of the experiencer's rational attitude, the leaving comes about

structure Semantics.Modality.Inertia.InertialParams : Type

Inertial modal parameters: circumstantial base + inertial ordering.

@cite{dowty-1979}: 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 w'.

In Kratzer's framework, this is a circumstantial modal base paired with an ordering source whose propositions describe what holds when the current course of events continues normally.

• circumstances : Kratzer.ModalBase

  Circumstantial modal base: facts holding at the evaluation world

• inertia : Kratzer.OrderingSource

  Inertial ordering: propositions describing normal continuation

def Semantics.Modality.Inertia.InertialParams.toKratzer (p : InertialParams) : Kratzer.KratzerParams

Extract Kratzer parameters from inertial parameters.

Equations

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

def Semantics.Modality.Inertia.inertialNecessity (p : InertialParams) (prop : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

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

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

def Semantics.Modality.Inertia.inertialPossibility (p : InertialParams) (prop : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

Inertial possibility: p holds in some best (most inertial) circumstantially accessible world.

Equations

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

theorem Semantics.Modality.Inertia.inertial_isNormal (p : InertialParams) : (Kratzer.KratzerTheory p.toKratzer).isNormal

Inertial modality is a normal modal logic (inherits from Kratzer).

theorem Semantics.Modality.Inertia.empty_inertia_is_simple (circ : Kratzer.ModalBase) (prop : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : inertialNecessity { circumstances := circ, inertia := Kratzer.emptyBackground } prop w = Kratzer.simpleNecessity circ prop w

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

def Semantics.Modality.Inertia.InertialParams.flavorTag : Core.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

• Semantics.Modality.Inertia.InertialParams.flavorTag = Core.Modality.ModalFlavor.circumstantial