@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

structure Phenomena.Conditionals.Studies.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

instance Phenomena.Conditionals.Studies.Iatridou2000.instReprCFMorphologyDatum : Repr CFMorphologyDatum

Equations

• Phenomena.Conditionals.Studies.Iatridou2000.instReprCFMorphologyDatum = { reprPrec := Phenomena.Conditionals.Studies.Iatridou2000.instReprCFMorphologyDatum.repr }

def Phenomena.Conditionals.Studies.Iatridou2000.instReprCFMorphologyDatum.repr : CFMorphologyDatum → ℕ → Std.Format

Equations

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

structure Phenomena.Conditionals.Studies.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

instance Phenomena.Conditionals.Studies.Iatridou2000.instReprSubjRequirementDatum : Repr SubjRequirementDatum

Equations

• Phenomena.Conditionals.Studies.Iatridou2000.instReprSubjRequirementDatum = { reprPrec := Phenomena.Conditionals.Studies.Iatridou2000.instReprSubjRequirementDatum.repr }

def Phenomena.Conditionals.Studies.Iatridou2000.instReprSubjRequirementDatum.repr : SubjRequirementDatum → ℕ → Std.Format

Equations

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

def Phenomena.Conditionals.Studies.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 Phenomena.Conditionals.Studies.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 Phenomena.Conditionals.Studies.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 Phenomena.Conditionals.Studies.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 Phenomena.Conditionals.Studies.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 Phenomena.Conditionals.Studies.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 Phenomena.Conditionals.Studies.Iatridou2000.french_flv : CFMorphologyDatum

French FLV: "imparfait, conditionnel"

Equations

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

def Phenomena.Conditionals.Studies.Iatridou2000.french_presCF : CFMorphologyDatum

French PresCF: "imparfait, conditionnel"

Equations

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

def Phenomena.Conditionals.Studies.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 Phenomena.Conditionals.Studies.Iatridou2000.english_subj : SubjRequirementDatum

English: no distinct past subjunctive, no subjunctive required.

Equations

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

def Phenomena.Conditionals.Studies.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

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

def Phenomena.Conditionals.Studies.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

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

def Phenomena.Conditionals.Studies.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

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

theorem Phenomena.Conditionals.Studies.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 Phenomena.Conditionals.Studies.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 Phenomena.Conditionals.Studies.Iatridou2000.english_flv_layers : english_flv.pastLayers = Semantics.Conditionals.Iatridou.CounterfactualType.flv.exclFCount

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.english_presCF_layers : english_presCF.pastLayers = Semantics.Conditionals.Iatridou.CounterfactualType.presCF.exclFCount

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.english_pastCF_layers : english_pastCF.pastLayers = Semantics.Conditionals.Iatridou.CounterfactualType.pastCF.exclFCount

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.greek_flv_layers : greek_flv.pastLayers = Semantics.Conditionals.Iatridou.CounterfactualType.flv.exclFCount

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.greek_presCF_layers : greek_presCF.pastLayers = Semantics.Conditionals.Iatridou.CounterfactualType.presCF.exclFCount

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.greek_pastCF_layers : greek_pastCF.pastLayers = Semantics.Conditionals.Iatridou.CounterfactualType.pastCF.exclFCount

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.french_flv_layers : french_flv.pastLayers = Semantics.Conditionals.Iatridou.CounterfactualType.flv.exclFCount

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.french_presCF_layers : french_presCF.pastLayers = Semantics.Conditionals.Iatridou.CounterfactualType.presCF.exclFCount

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.french_pastCF_layers : french_pastCF.pastLayers = Semantics.Conditionals.Iatridou.CounterfactualType.pastCF.exclFCount

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.english_subj_gen : Semantics.Conditionals.Iatridou.iatridouSubjGeneralization english_subj.hasPastSubjunctive english_subj.cfRequiresSubjunctive

English: no past subjunctive, no CF subjunctive required.

theorem Phenomena.Conditionals.Studies.Iatridou2000.greek_subj_gen : Semantics.Conditionals.Iatridou.iatridouSubjGeneralization greek_subj.hasPastSubjunctive greek_subj.cfRequiresSubjunctive

Greek: no past subjunctive, no CF subjunctive required.

theorem Phenomena.Conditionals.Studies.Iatridou2000.french_subj_gen : Semantics.Conditionals.Iatridou.iatridouSubjGeneralization french_subj.hasPastSubjunctive french_subj.cfRequiresSubjunctive

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.italian_subj_gen : Semantics.Conditionals.Iatridou.iatridouSubjGeneralization italian_subj.hasPastSubjunctive italian_subj.cfRequiresSubjunctive

Italian: has past subjunctive, CF requires subjunctive.

theorem Phenomena.Conditionals.Studies.Iatridou2000.knew_french_is_presCF : Semantics.Conditionals.Iatridou.classifyCounterfactual true false Semantics.Conditionals.Iatridou.IatridouPredType.ilp = some Semantics.Conditionals.Iatridou.CounterfactualType.presCF

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.leave_tomorrow_is_flv : Semantics.Conditionals.Iatridou.classifyCounterfactual true false Semantics.Conditionals.Iatridou.IatridouPredType.telic = some Semantics.Conditionals.Iatridou.CounterfactualType.flv

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.had_left_is_pastCF : Semantics.Conditionals.Iatridou.classifyCounterfactual true true Semantics.Conditionals.Iatridou.IatridouPredType.telic = some Semantics.Conditionals.Iatridou.CounterfactualType.pastCF

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.were_sick_is_presCF : Semantics.Conditionals.Iatridou.classifyCounterfactual true false Semantics.Conditionals.Iatridou.IatridouPredType.stative = some Semantics.Conditionals.Iatridou.CounterfactualType.presCF

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.had_known_is_pastCF : Semantics.Conditionals.Iatridou.classifyCounterfactual true true Semantics.Conditionals.Iatridou.IatridouPredType.ilp = some Semantics.Conditionals.Iatridou.CounterfactualType.pastCF

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

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

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

@[reducible, inline]

abbrev Phenomena.Conditionals.Studies.Iatridou2000.CFCtx : Type

Equations

• Phenomena.Conditionals.Studies.Iatridou2000.CFCtx = Core.Context.KContext Bool Unit Unit ℤ

def Phenomena.Conditionals.Studies.Iatridou2000.actualCtx : CFCtx

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

Equations

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

def Phenomena.Conditionals.Studies.Iatridou2000.actualTower : Core.Context.ContextTower CFCtx

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

Equations

• Phenomena.Conditionals.Studies.Iatridou2000.actualTower = Core.Context.ContextTower.root Phenomena.Conditionals.Studies.Iatridou2000.actualCtx

def Phenomena.Conditionals.Studies.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

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.presCF_depth : presCFTower.depth = 1

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.presCF_modal_exclF : Semantics.Conditionals.Iatridou.ExclF Semantics.Conditionals.Iatridou.ExclDimension.modal presCFTower

Modal ExclF holds: counterfactual world ≠ actual world.

theorem Phenomena.Conditionals.Studies.Iatridou2000.presCF_no_temporal_exclF : ¬Semantics.Conditionals.Iatridou.ExclF Semantics.Conditionals.Iatridou.ExclDimension.temporal presCFTower

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.flv_tower_depth_matches_data : presCFTower.depth = english_flv.pastLayers

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.presCF_tower_depth_matches_data : presCFTower.depth = english_presCF.pastLayers

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

def Phenomena.Conditionals.Studies.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

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.pastCF_depth : pastCFTower.depth = 2

Tower depth is 2 — matching 2 past morpheme layers.

theorem Phenomena.Conditionals.Studies.Iatridou2000.pastCF_modal_exclF : Semantics.Conditionals.Iatridou.ExclF Semantics.Conditionals.Iatridou.ExclDimension.modal pastCFTower

Modal ExclF holds: counterfactual world ≠ actual world.

theorem Phenomena.Conditionals.Studies.Iatridou2000.pastCF_temporal_exclF : Semantics.Conditionals.Iatridou.ExclF Semantics.Conditionals.Iatridou.ExclDimension.temporal pastCFTower

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.pastCF_tower_depth_matches_data : pastCFTower.depth = english_pastCF.pastLayers

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.pastCF_tower_depth_matches_greek : pastCFTower.depth = greek_pastCF.pastLayers

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

theorem Phenomena.Conditionals.Studies.Iatridou2000.pastCF_origin_preserved : pastCFTower.origin = actualCtx

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