@cite{iatridou-2000}: The Grammatical Ingredients of Counterfactuality

@cite{iatridou-2000} @cite{condoravdi-2002} @cite{deal-2020}Formalizes the core contribution of @cite{iatridou-2000}: the Exclusion Feature (ExclF), a single semantic predicate that unifies temporal past and counterfactual past. Past morphology signals exclusion of the topic situation's coordinate from the speaker's coordinate — on the temporal dimension for genuine past, on the modal dimension for counterfactuals.

Core Claim

Past morphology encodes exclusion:

• Temporal: T(topic) ≠ T(speaker)
• Modal: w(topic) ≠ w(speaker)

This maps directly onto the ContextTower's origin / innermost distinction: ExclF dim tower holds iff the relevant coordinate of tower.innermost differs from that of tower.origin.

Counterfactual Typology

Three counterfactual types arise from the number of ExclFs and predicate type:

• FLV (Future Less Vivid): 1 modal ExclF + telic predicate
• PresCF (Present Counterfactual): 1 modal ExclF + ILP/stative predicate
• PastCF (Past Counterfactual): 2 ExclFs (modal + temporal)

Tower Integration

ExclF stress-tests the tower because:

• ExclF is literally origin ≠ innermost on a coordinate
• subjShift produces modal ExclF when newWorld ≠ origin.world
• temporalShift produces temporal ExclF when newTime ≠ origin.time
• PastCF requires tower depth ≥ 2 (two mood-labeled shifts)

inductive Semantics.Conditionals.Iatridou.ExclDimension : Type

The two dimensions along which past morphology can exclude.

Iatridou's key insight: past morphology has a single semantic contribution (exclusion) that applies to different dimensions. The temporal/modal ambiguity of "past" is not lexical ambiguity — it is the same feature targeting different coordinates.

• temporal : ExclDimension

  Temporal: T(topic) ≠ T(speaker)

• modal : ExclDimension

  Modal: w(topic) ≠ w(speaker)

instance Semantics.Conditionals.Iatridou.instDecidableEqExclDimension : DecidableEq ExclDimension

Equations

• Semantics.Conditionals.Iatridou.instDecidableEqExclDimension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Conditionals.Iatridou.instReprExclDimension : Repr ExclDimension

Equations

• Semantics.Conditionals.Iatridou.instReprExclDimension = { reprPrec := Semantics.Conditionals.Iatridou.instReprExclDimension.repr }

def Semantics.Conditionals.Iatridou.instReprExclDimension.repr : ExclDimension → ℕ → Std.Format

Equations

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

def Semantics.Conditionals.Iatridou.instBEqExclDimension.beq : ExclDimension → ExclDimension → Bool

Equations

• Semantics.Conditionals.Iatridou.instBEqExclDimension.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Conditionals.Iatridou.instBEqExclDimension : BEq ExclDimension

Equations

• Semantics.Conditionals.Iatridou.instBEqExclDimension = { beq := Semantics.Conditionals.Iatridou.instBEqExclDimension.beq }

def Semantics.Conditionals.Iatridou.ExclF {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (dim : ExclDimension) (tower : Core.Context.ContextTower (Core.Context.KContext W E P T)) : Prop

The Exclusion Feature: past morphology signals that the topic coordinate differs from the speaker coordinate on the given dimension.

This is a predicate over context towers: ExclF dim tower holds iff the relevant coordinate of the innermost context (topic) differs from the origin context (speaker).

Equations

• Semantics.Conditionals.Iatridou.ExclF Semantics.Conditionals.Iatridou.ExclDimension.temporal tower = (tower.innermost.time ≠ tower.origin.time)
• Semantics.Conditionals.Iatridou.ExclF Semantics.Conditionals.Iatridou.ExclDimension.modal tower = (tower.innermost.world ≠ tower.origin.world)

theorem Semantics.Conditionals.Iatridou.exclF_temporal_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Core.Context.ContextTower (Core.Context.KContext W E P T)) : ExclF ExclDimension.temporal tower ↔ tower.innermost.time ≠ tower.origin.time

ExclF temporal unfolds to time inequality.

theorem Semantics.Conditionals.Iatridou.exclF_modal_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Core.Context.ContextTower (Core.Context.KContext W E P T)) : ExclF ExclDimension.modal tower ↔ tower.innermost.world ≠ tower.origin.world

ExclF modal unfolds to world inequality.

def Semantics.Conditionals.Iatridou.ExclDimension.toDealUse : ExclDimension → Tense.CounterfactualTense.PastMorphologyUse

Map ExclDimension to Deal's PastMorphologyUse.

This connects Iatridou's exclusion analysis to Deal's tense typology: temporal exclusion corresponds to temporal tense, modal exclusion corresponds to counterfactual tense.

Equations

• Semantics.Conditionals.Iatridou.ExclDimension.temporal.toDealUse = Semantics.Tense.CounterfactualTense.PastMorphologyUse.temporal
• Semantics.Conditionals.Iatridou.ExclDimension.modal.toDealUse = Semantics.Tense.CounterfactualTense.PastMorphologyUse.counterfactual

theorem Semantics.Conditionals.Iatridou.exclF_temporal_is_deal_temporal : ExclDimension.temporal.toDealUse = Tense.CounterfactualTense.PastMorphologyUse.temporal

Temporal ExclF maps to Deal's temporal use.

theorem Semantics.Conditionals.Iatridou.exclF_modal_is_deal_cf : ExclDimension.modal.toDealUse = Tense.CounterfactualTense.PastMorphologyUse.counterfactual

Modal ExclF maps to Deal's counterfactual use.

theorem Semantics.Conditionals.Iatridou.subjShift_produces_modal_exclF {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Core.Context.KContext W E P T) (w' : W) (t' : T) (h : w' ≠ c.world) : ExclF ExclDimension.modal ((Core.Context.ContextTower.root c).push (Mood.subjShift w' t'))

subjShift changes world → produces modal ExclF.

When a subjunctive clause introduces a new world that differs from the origin, the resulting tower has modal ExclF. This is the tower-level formalization of Iatridou's claim that counterfactual morphology signals world exclusion.

theorem Semantics.Conditionals.Iatridou.temporalShift_produces_temporal_exclF {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Core.Context.KContext W E P T) (t' : T) (h : t' ≠ c.time) : ExclF ExclDimension.temporal ((Core.Context.ContextTower.root c).push (Core.Context.temporalShift t'))

temporalShift changes time → produces temporal ExclF.

When an embedding shifts the evaluation time away from the speech time, the resulting tower has temporal ExclF. This is ordinary temporal past.

theorem Semantics.Conditionals.Iatridou.two_shifts_two_exclFs {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Core.Context.KContext W E P T) (w' : W) (t' t'' : T) (hw : w' ≠ c.world) (ht : t'' ≠ c.time) : have tower := ((Core.Context.ContextTower.root c).push (Mood.subjShift w' t')).push (Core.Context.temporalShift t''); ExclF ExclDimension.modal tower ∧ ExclF ExclDimension.temporal tower

Two shifts → both ExclFs.

PastCF requires two layers of past morphology: one modal ExclF (from subjunctive/counterfactual world shift) and one temporal ExclF (from the additional past morpheme). This produces a tower of depth ≥ 2 with both ExclFs active.

inductive Semantics.Conditionals.Iatridou.IatridouPredType : Type

Iatridou's predicate classification for counterfactual gating.

The distinction between FLV and PresCF (both with 1 modal ExclF) depends on the predicate type:

• ILPs and statives yield PresCF ("If he knew French,...")
• Telic predicates yield FLV ("If he were to leave tomorrow,...")

• ilp : IatridouPredType

  Individual-Level Predicate: "be tall", "know French"

• stative : IatridouPredType

  Stage-Level stative: "be sick", "be available"

• telic : IatridouPredType

  Telic predicate: "arrive", "build a house"

instance Semantics.Conditionals.Iatridou.instDecidableEqIatridouPredType : DecidableEq IatridouPredType

Equations

• Semantics.Conditionals.Iatridou.instDecidableEqIatridouPredType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Conditionals.Iatridou.instReprIatridouPredType : Repr IatridouPredType

Equations

• Semantics.Conditionals.Iatridou.instReprIatridouPredType = { reprPrec := Semantics.Conditionals.Iatridou.instReprIatridouPredType.repr }

def Semantics.Conditionals.Iatridou.instReprIatridouPredType.repr : IatridouPredType → ℕ → Std.Format

Equations

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

def Semantics.Conditionals.Iatridou.instBEqIatridouPredType.beq : IatridouPredType → IatridouPredType → Bool

Equations

• Semantics.Conditionals.Iatridou.instBEqIatridouPredType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Conditionals.Iatridou.instBEqIatridouPredType : BEq IatridouPredType

Equations

• Semantics.Conditionals.Iatridou.instBEqIatridouPredType = { beq := Semantics.Conditionals.Iatridou.instBEqIatridouPredType.beq }

def Semantics.Conditionals.Iatridou.VendlerClass.toIatridou : Tense.Aspect.LexicalAspect.VendlerClass → IatridouPredType

Map Vendler classes to Iatridou's predicate classification.

States and activities map to stative (both are atelic/non-dynamic enough for PresCF interpretation). Achievements and accomplishments map to telic (both have endpoints, triggering FLV interpretation).

Equations

• Semantics.Conditionals.Iatridou.VendlerClass.toIatridou Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state = Semantics.Conditionals.Iatridou.IatridouPredType.stative
• Semantics.Conditionals.Iatridou.VendlerClass.toIatridou Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity = Semantics.Conditionals.Iatridou.IatridouPredType.stative
• Semantics.Conditionals.Iatridou.VendlerClass.toIatridou Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement = Semantics.Conditionals.Iatridou.IatridouPredType.telic
• Semantics.Conditionals.Iatridou.VendlerClass.toIatridou Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment = Semantics.Conditionals.Iatridou.IatridouPredType.telic

inductive Semantics.Conditionals.Iatridou.CounterfactualType : Type

Iatridou's three counterfactual conditional types, distinguished by the number of ExclFs and predicate type.

• flv : CounterfactualType

  Future Less Vivid: 1 ExclF modal + telic predicate

• presCF : CounterfactualType

  Present Counterfactual: 1 ExclF modal + ILP/stative

• pastCF : CounterfactualType

  Past Counterfactual: 2 ExclFs (modal + temporal)

instance Semantics.Conditionals.Iatridou.instDecidableEqCounterfactualType : DecidableEq CounterfactualType

Equations

• Semantics.Conditionals.Iatridou.instDecidableEqCounterfactualType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Conditionals.Iatridou.instReprCounterfactualType.repr : CounterfactualType → ℕ → Std.Format

Equations

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

instance Semantics.Conditionals.Iatridou.instReprCounterfactualType : Repr CounterfactualType

Equations

• Semantics.Conditionals.Iatridou.instReprCounterfactualType = { reprPrec := Semantics.Conditionals.Iatridou.instReprCounterfactualType.repr }

def Semantics.Conditionals.Iatridou.instBEqCounterfactualType.beq : CounterfactualType → CounterfactualType → Bool

Equations

• Semantics.Conditionals.Iatridou.instBEqCounterfactualType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Conditionals.Iatridou.instBEqCounterfactualType : BEq CounterfactualType

Equations

• Semantics.Conditionals.Iatridou.instBEqCounterfactualType = { beq := Semantics.Conditionals.Iatridou.instBEqCounterfactualType.beq }

def Semantics.Conditionals.Iatridou.CounterfactualType.exclFCount : CounterfactualType → ℕ

The number of ExclFs required for each counterfactual type.

FLV and PresCF require 1 ExclF (modal only); PastCF requires 2 (modal + temporal). This corresponds to the number of past morpheme layers observed cross-linguistically.

Equations

• Semantics.Conditionals.Iatridou.CounterfactualType.flv.exclFCount = 1
• Semantics.Conditionals.Iatridou.CounterfactualType.presCF.exclFCount = 1
• Semantics.Conditionals.Iatridou.CounterfactualType.pastCF.exclFCount = 2

def Semantics.Conditionals.Iatridou.classifyCounterfactual (modalExcl temporalExcl : Bool) (predType : IatridouPredType) : Option CounterfactualType

Classify a counterfactual from its ExclF configuration and predicate type.

Returns none if there is no modal ExclF (a non-counterfactual sentence).

Equations

• Semantics.Conditionals.Iatridou.classifyCounterfactual true true predType = some Semantics.Conditionals.Iatridou.CounterfactualType.pastCF
• Semantics.Conditionals.Iatridou.classifyCounterfactual true false Semantics.Conditionals.Iatridou.IatridouPredType.telic = some Semantics.Conditionals.Iatridou.CounterfactualType.flv
• Semantics.Conditionals.Iatridou.classifyCounterfactual true false Semantics.Conditionals.Iatridou.IatridouPredType.ilp = some Semantics.Conditionals.Iatridou.CounterfactualType.presCF
• Semantics.Conditionals.Iatridou.classifyCounterfactual true false Semantics.Conditionals.Iatridou.IatridouPredType.stative = some Semantics.Conditionals.Iatridou.CounterfactualType.presCF
• Semantics.Conditionals.Iatridou.classifyCounterfactual false temporalExcl predType = none

theorem Semantics.Conditionals.Iatridou.telic_one_exclF_is_flv : classifyCounterfactual true false IatridouPredType.telic = some CounterfactualType.flv

Telic predicate + 1 modal ExclF = FLV.

theorem Semantics.Conditionals.Iatridou.ilp_one_exclF_is_presCF : classifyCounterfactual true false IatridouPredType.ilp = some CounterfactualType.presCF

ILP + 1 modal ExclF = PresCF.

theorem Semantics.Conditionals.Iatridou.stative_one_exclF_is_presCF : classifyCounterfactual true false IatridouPredType.stative = some CounterfactualType.presCF

Stative + 1 modal ExclF = PresCF.

theorem Semantics.Conditionals.Iatridou.two_exclFs_is_pastCF (pred : IatridouPredType) : classifyCounterfactual true true pred = some CounterfactualType.pastCF

Two ExclFs = PastCF regardless of predicate type.

theorem Semantics.Conditionals.Iatridou.no_modal_not_cf (temporalExcl : Bool) (pred : IatridouPredType) : classifyCounterfactual false temporalExcl pred = none

No modal ExclF = not a counterfactual.

theorem Semantics.Conditionals.Iatridou.root_no_temporal_exclF {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Core.Context.KContext W E P T) : ¬ExclF ExclDimension.temporal (Core.Context.ContextTower.root c)

A root tower (no shifts) has no temporal ExclF.

theorem Semantics.Conditionals.Iatridou.root_no_modal_exclF {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Core.Context.KContext W E P T) : ¬ExclF ExclDimension.modal (Core.Context.ContextTower.root c)

A root tower (no shifts) has no modal ExclF.

def Semantics.Conditionals.Iatridou.iatridouSubjGeneralization (hasPastSubj requiresSubj : Bool) : Prop

Iatridou's subjunctive generalization (42): "A CF can contain a subjunctive morpheme only if that subjunctive morpheme has a past tense form".

Strictly, the paper states this as a one-directional conditional (requires → has). We encode the biconditional because all languages in our data satisfy both directions: English and Greek lack past subjunctive and don't require subjunctive in CFs; Italian has past subjunctive and requires it.

Equations

• Semantics.Conditionals.Iatridou.iatridouSubjGeneralization hasPastSubj requiresSubj = (requiresSubj = hasPastSubj)

theorem Semantics.Conditionals.Iatridou.xMarking_produces_modal_exclF {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (rc : Core.Context.RichContext W E P T) (pastTime : T) (cfWorld : W) (expandedDomain : Set W) (h : cfWorld ≠ rc.base.world) : ((Core.Context.xMarkingShift pastTime cfWorld expandedDomain).apply rc).base.world ≠ rc.base.world

X-marking shift produces modal ExclF on RichContext towers.

The xMarkingShift (from Rich.lean) changes both world and time. When the counterfactual world differs from the origin, the resulting tower has modal ExclF.

theorem Semantics.Conditionals.Iatridou.pastCF_tower_depth {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Core.Context.KContext W E P T) (w' : W) (t' t'' : T) : (((Core.Context.ContextTower.root c).push (Mood.subjShift w' t')).push (Core.Context.temporalShift t'')).depth = 2

PastCF tower has depth 2.

A tower built with two mood shifts (for PastCF) has depth 2, corresponding to the two past morpheme layers observed cross-linguistically.