@cite{iatridou-2000} — Morphological Data @cite{iatridou-2000}

Theory-neutral cross-linguistic data on counterfactual morphology from @cite{iatridou-2000} "The Grammatical Ingredients of Counterfactuality", Linguistic Inquiry 31(2): 231–270.

Key Empirical Generalizations

1. Past morphology is uniform: FLV, PresCF, and PastCF all use past morphology, but differ in the number of past layers.
2. Imperfective is not universal: languages that lack imperfective (e.g., English) omit it in CFs; languages with imperfective (e.g., Greek) use it in all CF types.
3. Subjunctive mirrors past subjunctive availability: a CF can contain subjunctive only if the language has a distinct past subjunctive form (generalization 42).

Data Sources

• Tables 1–2 of @cite{iatridou-2000}
• Example sentences from §2

See also

• Phenomena/Modality/Studies/CarianiSantorio2018.lean — selectional account where past morphology shifts the modal parameter rather than introducing a separate counterfactual operator. C&S §5.3.2 identifies would with morphological past will, dovetailing with Iatridou's past-morphology-as-modal-shift generalization.

inductive Iatridou2000.IatridouPredType : Type

@cite{iatridou-2000}'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"

@[implicit_reducible]

instance Iatridou2000.instDecidableEqIatridouPredType : DecidableEq IatridouPredType

Equations

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

@[implicit_reducible]

instance Iatridou2000.instReprIatridouPredType : Repr IatridouPredType

Equations

• Iatridou2000.instReprIatridouPredType = { reprPrec := Iatridou2000.instReprIatridouPredType.repr }

def Iatridou2000.instReprIatridouPredType.repr : IatridouPredType → ℕ → Std.Format

Equations

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

def Iatridou2000.VendlerClass.toIatridou : Features.VendlerClass → IatridouPredType

Map Vendler classes to @cite{iatridou-2000}'s predicate classification.

States and activities map to stative; achievements and accomplishments map to telic.

Equations

• Iatridou2000.VendlerClass.toIatridou Features.VendlerClass.state = Iatridou2000.IatridouPredType.stative
• Iatridou2000.VendlerClass.toIatridou Features.VendlerClass.activity = Iatridou2000.IatridouPredType.stative
• Iatridou2000.VendlerClass.toIatridou Features.VendlerClass.semelfactive = Iatridou2000.IatridouPredType.stative
• Iatridou2000.VendlerClass.toIatridou Features.VendlerClass.achievement = Iatridou2000.IatridouPredType.telic
• Iatridou2000.VendlerClass.toIatridou Features.VendlerClass.accomplishment = Iatridou2000.IatridouPredType.telic

inductive Iatridou2000.CounterfactualType : Type

@cite{iatridou-2000}'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)

@[implicit_reducible]

instance Iatridou2000.instDecidableEqCounterfactualType : DecidableEq CounterfactualType

Equations

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

@[implicit_reducible]

instance Iatridou2000.instReprCounterfactualType : Repr CounterfactualType

Equations

• Iatridou2000.instReprCounterfactualType = { reprPrec := Iatridou2000.instReprCounterfactualType.repr }

def Iatridou2000.instReprCounterfactualType.repr : CounterfactualType → ℕ → Std.Format

Equations

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

def Iatridou2000.CounterfactualType.exclFCount : CounterfactualType → ℕ

The number of ExclFs required for each counterfactual type.

Equations

• Iatridou2000.CounterfactualType.flv.exclFCount = 1
• Iatridou2000.CounterfactualType.presCF.exclFCount = 1
• Iatridou2000.CounterfactualType.pastCF.exclFCount = 2

def Iatridou2000.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

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

theorem Iatridou2000.telic_one_exclF_is_flv : classifyCounterfactual true false IatridouPredType.telic = some CounterfactualType.flv

Telic predicate + 1 modal ExclF = FLV.

theorem Iatridou2000.ilp_one_exclF_is_presCF : classifyCounterfactual true false IatridouPredType.ilp = some CounterfactualType.presCF

ILP + 1 modal ExclF = PresCF.

theorem Iatridou2000.stative_one_exclF_is_presCF : classifyCounterfactual true false IatridouPredType.stative = some CounterfactualType.presCF

Stative + 1 modal ExclF = PresCF.

theorem Iatridou2000.two_exclFs_is_pastCF (pred : IatridouPredType) : classifyCounterfactual true true pred = some CounterfactualType.pastCF

Two ExclFs = PastCF regardless of predicate type.

theorem Iatridou2000.no_modal_not_cf (temporalExcl : Bool) (pred : IatridouPredType) : classifyCounterfactual false temporalExcl pred = none

No modal ExclF = not a counterfactual.

def Iatridou2000.iatridouSubjGeneralization (hasPastSubj requiresSubj : Bool) : Prop

@cite{iatridou-2000}'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

• Iatridou2000.iatridouSubjGeneralization hasPastSubj requiresSubj = (requiresSubj = hasPastSubj)

def Iatridou2000.CounterfactualType.toSubjunctiveType : CounterfactualType → Core.Mood.SubjunctiveType

All three counterfactual types collapse to the framework-agnostic Core.Mood.SubjunctiveType.counterfactual tag.

Equations

• x✝.toSubjunctiveType = Core.Mood.SubjunctiveType.counterfactual

theorem Iatridou2000.all_counterfactuals_are_counterfactual (t : CounterfactualType) : t.toSubjunctiveType = Core.Mood.SubjunctiveType.counterfactual

Every @cite{iatridou-2000} counterfactual type maps to .counterfactual.

theorem Iatridou2000.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 (Semantics.Mood.subjShift w' t')).push (Core.Context.temporalShift t'')).depth = 2

PastCF tower has depth 2 — corresponding to the two past morpheme layers observed cross-linguistically.

(Tower-level corollary; uses the subjShift/temporalShift infrastructure from Semantics.Modality.Exclusion.)

structure Iatridou2000.CFMorphologyDatum : Type

A morphological datum for counterfactual conditionals.

Each datum records the verb morphology in the antecedent and consequent of a specific counterfactual type in a specific language.

• language : String

  Language name

• cfType : String

  Counterfactual type: "FLV", "PresCF", or "PastCF"

• antecedentForm : String

  Verb morphology in the antecedent

• consequentForm : String

  Verb morphology in the consequent

• hasPastMorph : Bool

  Whether past morphology is present

• hasImpfMorph : Bool

  Whether imperfective morphology is present

• hasSubjMorph : Bool

  Whether subjunctive morphology is present

• pastLayers : ℕ

  Number of past morpheme layers

• gloss : String

  Gloss of the example

def Iatridou2000.instReprCFMorphologyDatum.repr : CFMorphologyDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Iatridou2000.instReprCFMorphologyDatum : Repr CFMorphologyDatum

Equations

• Iatridou2000.instReprCFMorphologyDatum = { reprPrec := Iatridou2000.instReprCFMorphologyDatum.repr }

structure Iatridou2000.SubjRequirementDatum : Type

A datum for whether a language requires subjunctive in counterfactuals.

Iatridou's generalization: a language requires subjunctive in CFs iff it has a morphologically distinct past subjunctive.

• language : String

  Language name

• hasPastSubjunctive : Bool

  Whether the language has a distinct past subjunctive form

• cfRequiresSubjunctive : Bool

  Whether counterfactuals require subjunctive morphology

@[implicit_reducible]

instance Iatridou2000.instReprSubjRequirementDatum : Repr SubjRequirementDatum

Equations

• Iatridou2000.instReprSubjRequirementDatum = { reprPrec := Iatridou2000.instReprSubjRequirementDatum.repr }

def Iatridou2000.instReprSubjRequirementDatum.repr : SubjRequirementDatum → ℕ → Std.Format

Equations

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

def Iatridou2000.english_flv : CFMorphologyDatum

English FLV: "If he were to take the exam tomorrow,..."

Equations

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

def Iatridou2000.english_presCF : CFMorphologyDatum

English PresCF: "If he knew the answer,..."

Equations

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

def Iatridou2000.english_pastCF : CFMorphologyDatum

English PastCF: "If he had taken the exam,..."

Equations

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

def Iatridou2000.greek_flv : CFMorphologyDatum

Greek FLV: "An + past + impf, tha + past + impf"

Based on @cite{iatridou-2000}, example (6). Greek FLV and PresCF have identical morphological form; the FLV/PresCF distinction is made by predicate type and temporal adverbials, not by morphology.

Equations

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

def Iatridou2000.greek_presCF : CFMorphologyDatum

Greek PresCF: "An + past + impf, tha + past + impf"

Based on @cite{iatridou-2000}, example (6). Morphologically identical to FLV in Greek; the counterfactual reading arises from the stative predicate.

Equations

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

def Iatridou2000.greek_pastCF : CFMorphologyDatum

Greek PastCF: "An + past + past + impf, tha + past + past + impf"

Based on @cite{iatridou-2000}, example (6c). The additional past layer (the pluperfect ixe + participle) distinguishes PastCF from PresCF/FLV.

Equations

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

def Iatridou2000.french_flv : CFMorphologyDatum

French FLV: "imparfait, conditionnel"

Equations

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

def Iatridou2000.french_presCF : CFMorphologyDatum

French PresCF: "imparfait, conditionnel"

Equations

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

def Iatridou2000.french_pastCF : CFMorphologyDatum

French PastCF: "plus-que-parfait, conditionnel passé"

Equations

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

def Iatridou2000.english_subj : SubjRequirementDatum

English: no distinct past subjunctive, no subjunctive required.

Equations

• Iatridou2000.english_subj = { language := "English", hasPastSubjunctive := false, cfRequiresSubjunctive := false }

def Iatridou2000.greek_subj : SubjRequirementDatum

Greek: no past subjunctive, no subjunctive required in CFs.

Greek CFs use past + imperfective morphology (indicative), not subjunctive. Greek has a subjunctive-like particle (na), but this is not used in counterfactual conditionals.

Equations

• Iatridou2000.greek_subj = { language := "Greek", hasPastSubjunctive := false, cfRequiresSubjunctive := false }

def Iatridou2000.french_subj : SubjRequirementDatum

French: no productive past subjunctive, no subjunctive required in CFs.

French CFs use the indicative imparfait ("si j'avais..."), not the subjonctif. French has a literary past subjunctive (subjonctif imparfait), but it is not used productively in counterfactuals.

Equations

• Iatridou2000.french_subj = { language := "French", hasPastSubjunctive := false, cfRequiresSubjunctive := false }

def Iatridou2000.italian_subj : SubjRequirementDatum

Italian: has distinct past subjunctive, subjunctive required in CFs.

Italian CFs require the congiuntivo (subjunctive), which has a robust past form (congiuntivo trapassato). This is one of the positive cases for Iatridou's generalization (42): "A CF can contain a subjunctive morpheme only if that subjunctive morpheme has a past tense form."

Equations

• Iatridou2000.italian_subj = { language := "Italian", hasPastSubjunctive := true, cfRequiresSubjunctive := true }

theorem Iatridou2000.all_cfs_have_past : english_flv.hasPastMorph = true ∧ english_presCF.hasPastMorph = true ∧ english_pastCF.hasPastMorph = true ∧ greek_flv.hasPastMorph = true ∧ greek_presCF.hasPastMorph = true ∧ greek_pastCF.hasPastMorph = true ∧ french_flv.hasPastMorph = true ∧ french_presCF.hasPastMorph = true ∧ french_pastCF.hasPastMorph = true

All CF types use past morphology.

theorem Iatridou2000.pastCF_has_more_layers : english_pastCF.pastLayers > english_presCF.pastLayers ∧ greek_pastCF.pastLayers > greek_presCF.pastLayers ∧ french_pastCF.pastLayers > french_presCF.pastLayers

PastCF has more past layers than PresCF/FLV.

theorem Iatridou2000.english_flv_layers : english_flv.pastLayers = CounterfactualType.flv.exclFCount

English FLV: 1 past layer = 1 ExclF (FLV).

theorem Iatridou2000.english_presCF_layers : english_presCF.pastLayers = CounterfactualType.presCF.exclFCount

English PresCF: 1 past layer = 1 ExclF (PresCF).

theorem Iatridou2000.english_pastCF_layers : english_pastCF.pastLayers = CounterfactualType.pastCF.exclFCount

English PastCF: 2 past layers = 2 ExclFs (PastCF).

theorem Iatridou2000.greek_flv_layers : greek_flv.pastLayers = CounterfactualType.flv.exclFCount

Greek FLV: 1 past layer = 1 ExclF (FLV).

theorem Iatridou2000.greek_presCF_layers : greek_presCF.pastLayers = CounterfactualType.presCF.exclFCount

Greek PresCF: 1 past layer = 1 ExclF (PresCF).

theorem Iatridou2000.greek_pastCF_layers : greek_pastCF.pastLayers = CounterfactualType.pastCF.exclFCount

Greek PastCF: 2 past layers = 2 ExclFs (PastCF).

theorem Iatridou2000.french_flv_layers : french_flv.pastLayers = CounterfactualType.flv.exclFCount

French FLV: 1 past layer = 1 ExclF (FLV).

theorem Iatridou2000.french_presCF_layers : french_presCF.pastLayers = CounterfactualType.presCF.exclFCount

French PresCF: 1 past layer = 1 ExclF (PresCF).

theorem Iatridou2000.french_pastCF_layers : french_pastCF.pastLayers = CounterfactualType.pastCF.exclFCount

French PastCF: 2 past layers = 2 ExclFs (PastCF).

theorem Iatridou2000.english_subj_gen : iatridouSubjGeneralization english_subj.hasPastSubjunctive english_subj.cfRequiresSubjunctive

English: no past subjunctive, no CF subjunctive required.

theorem Iatridou2000.greek_subj_gen : iatridouSubjGeneralization greek_subj.hasPastSubjunctive greek_subj.cfRequiresSubjunctive

Greek: no past subjunctive, no CF subjunctive required.

theorem Iatridou2000.french_subj_gen : iatridouSubjGeneralization french_subj.hasPastSubjunctive french_subj.cfRequiresSubjunctive

French: no productive past subjunctive, no CF subjunctive required.

theorem Iatridou2000.italian_subj_gen : iatridouSubjGeneralization italian_subj.hasPastSubjunctive italian_subj.cfRequiresSubjunctive

Italian: has past subjunctive, CF requires subjunctive.

theorem Iatridou2000.knew_french_is_presCF : classifyCounterfactual true false IatridouPredType.ilp = some CounterfactualType.presCF

"If he knew French" (ILP + 1 modal ExclF) → PresCF.

theorem Iatridou2000.leave_tomorrow_is_flv : classifyCounterfactual true false IatridouPredType.telic = some CounterfactualType.flv

"If he were to leave" (telic + 1 modal ExclF) → FLV.

theorem Iatridou2000.had_left_is_pastCF : classifyCounterfactual true true IatridouPredType.telic = some CounterfactualType.pastCF

"If he had left" (telic + 2 ExclFs) → PastCF.

theorem Iatridou2000.were_sick_is_presCF : classifyCounterfactual true false IatridouPredType.stative = some CounterfactualType.presCF

"If he were sick" (stative + 1 modal ExclF) → PresCF.

theorem Iatridou2000.had_known_is_pastCF : classifyCounterfactual true true IatridouPredType.ilp = some CounterfactualType.pastCF

"If he had known" (ILP + 2 ExclFs) → PastCF.

theorem Iatridou2000.pastCF_exempt_from_ulc {T : Type u_1} [LE T] (R E : T) : Semantics.Tense.Counterfactual.refinedULC Semantics.Tense.Counterfactual.PastMorphologyUse.counterfactual R E

PastCF is exempt from ULC via Deal's refined ULC.

@[reducible, inline]

abbrev Iatridou2000.CFCtx : Type

Equations

• Iatridou2000.CFCtx = Core.Context.KContext Bool Unit Unit ℤ

def Iatridou2000.actualCtx : CFCtx

The actual context: world = true (actual), time = 0 (now).

Equations

• Iatridou2000.actualCtx = { agent := (), addressee := (), world := true, time := 0, position := () }

def Iatridou2000.actualTower : Core.Context.ContextTower CFCtx

Root tower: the actual speech-act context, depth 0.

Equations

• Iatridou2000.actualTower = Core.Context.ContextTower.root Iatridou2000.actualCtx

def Iatridou2000.presCFTower : Core.Context.ContextTower CFCtx

FLV/PresCF: one subjunctive shift to a counterfactual world. The counterfactual world (false) differs from the actual world (true).

Equations

• Iatridou2000.presCFTower = Iatridou2000.actualTower.push (Semantics.Mood.subjShift false 0)

theorem Iatridou2000.presCF_depth : presCFTower.depth = 1

The tower has depth 1 — matching 1 past morpheme layer.

theorem Iatridou2000.presCF_modal_exclF : Semantics.Modality.Exclusion.ExclF Semantics.Modality.Exclusion.ExclDimension.modal presCFTower

Modal ExclF holds: counterfactual world ≠ actual world.

theorem Iatridou2000.presCF_no_temporal_exclF : ¬Semantics.Modality.Exclusion.ExclF Semantics.Modality.Exclusion.ExclDimension.temporal presCFTower

Temporal ExclF does NOT hold: time is unchanged (0 = 0).

theorem Iatridou2000.flv_tower_depth_matches_data : presCFTower.depth = english_flv.pastLayers

Tower depth (1) matches English FLV past layers (1).

theorem Iatridou2000.presCF_tower_depth_matches_data : presCFTower.depth = english_presCF.pastLayers

Tower depth (1) matches English PresCF past layers (1).

def Iatridou2000.pastCFTower : Core.Context.ContextTower CFCtx

PastCF: two shifts — one modal (subjunctive, world shift) and one temporal (additional past layer, time shift to -5).

Equations

• Iatridou2000.pastCFTower = Iatridou2000.presCFTower.push (Core.Context.temporalShift (-5))

theorem Iatridou2000.pastCF_depth : pastCFTower.depth = 2

Tower depth is 2 — matching 2 past morpheme layers.

theorem Iatridou2000.pastCF_modal_exclF : Semantics.Modality.Exclusion.ExclF Semantics.Modality.Exclusion.ExclDimension.modal pastCFTower

Modal ExclF holds: counterfactual world ≠ actual world.

theorem Iatridou2000.pastCF_temporal_exclF : Semantics.Modality.Exclusion.ExclF Semantics.Modality.Exclusion.ExclDimension.temporal pastCFTower

Temporal ExclF holds: shifted time (-5) ≠ speech time (0).

theorem Iatridou2000.pastCF_tower_depth_matches_data : pastCFTower.depth = english_pastCF.pastLayers

Tower depth (2) matches English PastCF past layers (2).

theorem Iatridou2000.pastCF_tower_depth_matches_greek : pastCFTower.depth = greek_pastCF.pastLayers

Tower depth (2) matches Greek PastCF past layers (2).

theorem Iatridou2000.pastCF_origin_preserved : pastCFTower.origin = actualCtx

Even in a PastCF tower (depth 2), the origin context is preserved.