Iatridou (2000): The Grammatical Ingredients of Counterfactuality [Iat00]

Theory-neutral cross-linguistic data and the ExclF analysis from [Iat00] "The Grammatical Ingredients of Counterfactuality", Linguistic Inquiry 31(2): 231–270.

Iatridou's central claim: the morphology we call "past tense" provides a skeletal exclusion feature (ExclF), T(x) excludes C(x) — the topic x excludes the speaker's x. Over times it yields temporal past; over worlds it yields counterfactuality. A counterfactual is built from ExclF, an aspectual component (imperfective in some languages), and mood.

Key empirical generalizations

1. Past morphology is uniform: FLV, PresCF, and PastCF all use past morphology, differing in the number of ExclF layers (1, 1, 2).
2. Imperfective is not universal: languages with imperfective (Greek, French) use it in CFs; languages without it (English) omit it.
3. Subjunctive mirrors past-subjunctive availability (§6.1): a CF uses subjunctive only in languages with a past-subjunctive paradigm — German and Italian do; French and Indo-Aryan have only a nonpast subjunctive and don't.

See also

• Studies/CarianiSantorio2018.lean — selectional account where past morphology shifts the modal parameter rather than introducing a separate CF operator.

Iatridou's counterfactual typology

inductive Iatridou2000.CounterfactualType : Type

[Iat00]'s three counterfactual conditional types, distinguished by the number of ExclFs and (in the one-ExclF cases) the predicate's Aktionsart.

• flv : CounterfactualType

  Future Less Vivid: one ExclF (over worlds) + telic/activity predicate.

• presCF : CounterfactualType

  Present Counterfactual: one ExclF (over worlds) + individual-level stative.

• pastCF : CounterfactualType

  Past Counterfactual: two ExclFs — one over worlds, one over times.

@[implicit_reducible]

instance Iatridou2000.instDecidableEqCounterfactualType : DecidableEq CounterfactualType

Equations

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

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

Equations

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

@[implicit_reducible]

instance Iatridou2000.instReprCounterfactualType : Repr CounterfactualType

Equations

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

def Iatridou2000.CounterfactualType.exclFCount : CounterfactualType → ℕ

ExclF count per type. PresCF/FLV have one (over worlds); PastCF has two — the pluperfect's two past layers, one fake (modal) and one real (temporal) ([Iat00] §4, p. 252).

Equations

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

inductive Iatridou2000.IatridouPredType : Type

Predicate Aktionsart relevant to the FLV/PresCF split ([Iat00], Tables 1–2). The individual-level vs stage-level distinction among statives is not recoverable from Vendler class (both are "states"), so it is encoded directly rather than derived from a VendlerClass.

• telic : IatridouPredType

  Telic: arrive, build a house (evaluated in the future → FLV).

• activity : IatridouPredType

  Activity: run, push the cart — patterns with telics ([Iat00], fn 24).

• ilp : IatridouPredType

  Individual-level stative: be tall, know French (holds also now → PresCF).

• slp : IatridouPredType

  Stage-level stative: be sick, be drunk (future or now → FLV or PresCF).

@[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.classifyCounterfactual : Bool → Bool → IatridouPredType → Finset CounterfactualType

Classify a counterfactual from its ExclF configuration and predicate type, returning the set of licensed CF readings (∅ if there is no modal ExclF).

Faithful to [Iat00] Table 1: with one (modal) ExclF, a telic or activity predicate yields FLV, an individual-level stative yields PresCF, and a stage-level stative yields both (FLV with a future adverbial, PresCF otherwise — ex (64)). Two ExclFs yield PastCF regardless of predicate.

Equations

• Iatridou2000.classifyCounterfactual false x✝¹ x✝ = ∅
• Iatridou2000.classifyCounterfactual true true x✝ = {Iatridou2000.CounterfactualType.pastCF}
• Iatridou2000.classifyCounterfactual true false Iatridou2000.IatridouPredType.telic = {Iatridou2000.CounterfactualType.flv}
• Iatridou2000.classifyCounterfactual true false Iatridou2000.IatridouPredType.activity = {Iatridou2000.CounterfactualType.flv}
• Iatridou2000.classifyCounterfactual true false Iatridou2000.IatridouPredType.ilp = {Iatridou2000.CounterfactualType.presCF}
• Iatridou2000.classifyCounterfactual true false Iatridou2000.IatridouPredType.slp = {Iatridou2000.CounterfactualType.flv, Iatridou2000.CounterfactualType.presCF}

theorem Iatridou2000.telic_one_exclF : classifyCounterfactual true false IatridouPredType.telic = {CounterfactualType.flv}

Telic + one modal ExclF → FLV.

theorem Iatridou2000.activity_one_exclF : classifyCounterfactual true false IatridouPredType.activity = {CounterfactualType.flv}

Activity + one modal ExclF → FLV ([Iat00], fn 24).

theorem Iatridou2000.ilp_one_exclF : classifyCounterfactual true false IatridouPredType.ilp = {CounterfactualType.presCF}

Individual-level stative + one modal ExclF → PresCF only.

theorem Iatridou2000.slp_one_exclF : classifyCounterfactual true false IatridouPredType.slp = {CounterfactualType.flv, CounterfactualType.presCF}

Stage-level stative + one modal ExclF → both FLV and PresCF ([Iat00], Table 1, ex (64)): "If he were drunk at next week's meeting" (FLV) vs "If he were drunk, he would be louder" (PresCF).

theorem Iatridou2000.two_exclFs_pastCF (pred : IatridouPredType) : classifyCounterfactual true true pred = {CounterfactualType.pastCF}

Two ExclFs → PastCF, regardless of predicate type.

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

No modal ExclF → not a counterfactual.

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

[Iat00]'s subjunctive prediction (§6.1, p. 264): a CF uses subjunctive only in languages that have a past-subjunctive paradigm.

The paper states it one-directionally (uses → has); we encode the biconditional, which all languages in the data satisfy: English, Greek, and French lack a productive past subjunctive and use none in CFs; Italian has one and requires it.

Equations

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

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

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

Equations

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

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

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

A PastCF tower has depth 2 — the two past morpheme layers (one fake/modal, one real/temporal).

Datum structures

structure Iatridou2000.SubjRequirementDatum : Type

Whether a language requires subjunctive in CFs, and whether it has a distinct past subjunctive.

• language : String
• hasPastSubjunctive : Bool
• cfRequiresSubjunctive : Bool

@[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.

Per-language imperfective ([Iat00], generalization 2)

The CF-type layer counts (generalization 1) are language-neutral properties of CounterfactualType.exclFCount — see the data theorems below — so there is no per-(language × CF-type) morphology table. The one morphological ingredient that varies cross-linguistically is the imperfective: a per-language fact.

inductive Iatridou2000.CFLanguage : Type

The languages [Iat00] draws CF morphology from.

• english : CFLanguage
• greek : CFLanguage
• french : CFLanguage

@[implicit_reducible]

instance Iatridou2000.instDecidableEqCFLanguage : DecidableEq CFLanguage

Equations

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

def Iatridou2000.instReprCFLanguage.repr : CFLanguage → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Iatridou2000.instReprCFLanguage : Repr CFLanguage

Equations

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

def Iatridou2000.usesImperfectiveInCF : CFLanguage → Bool

Whether a language uses imperfective morphology in counterfactuals: Greek and French do, English does not. Uniform across CF types within a language. Grounded in the impf tags of Data/Examples/Iatridou2000.json by imperfective_grounded below.

Equations

• Iatridou2000.usesImperfectiveInCF Iatridou2000.CFLanguage.english = false
• Iatridou2000.usesImperfectiveInCF Iatridou2000.CFLanguage.greek = true
• Iatridou2000.usesImperfectiveInCF Iatridou2000.CFLanguage.french = true

Subjunctive-requirement data ([Iat00], §6.1)

def Iatridou2000.english_subj : SubjRequirementDatum

English: no productive past subjunctive (vestigial were aside), none required.

Equations

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

def Iatridou2000.greek_subj : SubjRequirementDatum

Greek: na-clauses are not CF subjunctive ([Iat00], fn 37); none required.

Equations

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

def Iatridou2000.french_subj : SubjRequirementDatum

French: no productive past subjunctive (only the dubitative); CFs use the past indicative ([Iat00], §6.1, ex (99)).

Equations

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

def Iatridou2000.italian_subj : SubjRequirementDatum

Italian: has a past subjunctive (congiuntivo trapassato) and requires it in CFs — a positive case for [Iat00]'s §6.1 prediction.

Equations

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

def Iatridou2000.allSubjData : List SubjRequirementDatum

All subjunctive-requirement data.

Equations

• Iatridou2000.allSubjData = [Iatridou2000.english_subj, Iatridou2000.greek_subj, Iatridou2000.french_subj, Iatridou2000.italian_subj]

Data theorems

theorem Iatridou2000.cf_has_past_layer (t : CounterfactualType) : 1 ≤ t.exclFCount

Generalization 1 ([Iat00]): every CF type carries past morphology — it has at least one ExclF (past) layer. A property of the CounterfactualType taxonomy, not a per-row stipulation.

theorem Iatridou2000.flv_presCF_fewer_layers : CounterfactualType.flv.exclFCount < CounterfactualType.pastCF.exclFCount ∧ CounterfactualType.presCF.exclFCount < CounterfactualType.pastCF.exclFCount

The pluperfect's extra layer ([Iat00] §3): PastCF carries strictly more ExclF layers than the one-layer FLV and PresCF.

theorem Iatridou2000.imperfective_not_universal : (∃ (l : CFLanguage), usesImperfectiveInCF l = true) ∧ ∃ (l : CFLanguage), usesImperfectiveInCF l = false

Generalization 2 ([Iat00]): the imperfective is not a universal ingredient of counterfactuality — some languages use it, others do not.

theorem Iatridou2000.subj_generalization (d : SubjRequirementDatum) : d ∈ allSubjData → iatridouSubjGeneralization d.hasPastSubjunctive d.cfRequiresSubjunctive

Each language satisfies [Iat00]'s subjunctive generalization (§6.1).

Grounding in the glossed stimuli

The generalizations are grounded in the verified glossed sentences of Data/Examples/Iatridou2000.json (generated Iatridou2000.Examples): all three CF types are attested, and the per-language imperfective fact matches the examples' impf tags.

def Iatridou2000.impfTag (e : Data.Examples.LinguisticExample) : Option Bool

The impf tag read as a Bool.

Equations

• Iatridou2000.impfTag e = match e.feature? "impf" with | some "yes" => some true | some "no" => some false | x => none

theorem Iatridou2000.cf_types_attested : Examples.en_flv.feature? "cf_type" = some "flv" ∧ Examples.en_presCF.feature? "cf_type" = some "presCF" ∧ Examples.en_pastCF.feature? "cf_type" = some "pastCF"

All three CF types are attested in the English stimuli.

theorem Iatridou2000.imperfective_grounded : impfTag Examples.en_flv = some (usesImperfectiveInCF CFLanguage.english) ∧ impfTag Examples.gr_flv = some (usesImperfectiveInCF CFLanguage.greek) ∧ impfTag Examples.fr_flv = some (usesImperfectiveInCF CFLanguage.french)

usesImperfectiveInCF matches the example impf tags — English (no), Greek (yes), French (yes). Flipping a JSON tag or the generalization breaks this.

ContextTower bridge

@[reducible, inline]

abbrev Iatridou2000.CFCtx : Type

Equations

• Iatridou2000.CFCtx = Semantics.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 : Semantics.Context.ContextTower CFCtx

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

Equations

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

def Iatridou2000.presCFTower : Semantics.Context.ContextTower CFCtx

FLV/PresCF: one subjunctive shift to a counterfactual world (false ≠ 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 one past morpheme layer.

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

Modal ExclF holds: the counterfactual world ≠ the actual world.

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

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

theorem Iatridou2000.presCF_depth_matches_data : presCFTower.depth = CounterfactualType.presCF.exclFCount

Tower depth (1) matches the PresCF ExclF-layer count (1).

def Iatridou2000.pastCFTower : Semantics.Context.ContextTower CFCtx

PastCF: a modal shift (subjunctive, world) plus a temporal shift (an extra past layer, time → -5).

Equations

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

theorem Iatridou2000.pastCF_depth : pastCFTower.depth = 2

The tower has depth 2 — matching two past morpheme layers.

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

Modal ExclF holds: the counterfactual world ≠ the actual world. The modal+temporal pair is the substrate's PastCF configuration (two_shifts_two_exclFs).

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

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

theorem Iatridou2000.pastCF_depth_matches_data : pastCFTower.depth = CounterfactualType.pastCF.exclFCount

Tower depth (2) matches the PastCF ExclF-layer count (2).

theorem Iatridou2000.pastCF_origin_preserved : pastCFTower.origin = actualCtx

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

theorem Iatridou2000.cf_diagnostics_examples : Examples.ex2a.feature? "cf_type" = some "presCF" ∧ Examples.ex2b.feature? "cf_type" = some "pastCF" ∧ presCFTower.depth = 1 ∧ pastCFTower.depth = 2

The present/past-CF ExclF diagnostics are witnessed by Iatridou's (2a)/(2b): (2a) is a PresCF (one modal ExclF, tower depth 1), (2b) a PastCF (two ExclFs, depth 2). Ties the glossed (2)-stimuli to the ContextTower model.