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 (W : Type u_2) : Type u_2

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 : Core.Logic.Intensional.ModalBase W

  Circumstantial modal base: facts holding at the evaluation world

• inertia : Core.Logic.Intensional.OrderingSource W

  Inertial ordering: propositions describing normal continuation

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

Extract Kratzer parameters from inertial parameters.

Equations

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

def Semantics.Modality.Inertia.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

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

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

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_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. Inherited from Kratzer.duality since inertial necessity/possibility are boxR/diamondR over the same Kratzer best-worlds relation.

See Kratzer/Operators.lean::duality docstring for the broader context: one of five modality-flavor theorem dualitys that would unify under a Core.Logic.Opposition.Square.fromBox instance once the Prop↔Bool coercion lands.

theorem Semantics.Modality.Inertia.empty_inertia_is_simple {W : Type u_1} (circ : Core.Logic.Intensional.ModalBase W) (prop : W → Prop) (w : W) : inertialNecessity { circumstances := circ, inertia := Core.Logic.Intensional.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