Iatridou (2000): The grammatical ingredients of counterfactuality

This file formalizes [Iat00]'s account of the past morphology of counterfactuals as an exclusion feature. The feature's skeletal meaning (49) is that the topic excludes what, for all the speaker knows, is the speaker's: over times the topic time excludes the utterance time, temporal past, and over worlds the topic worlds exclude the actual worlds, counterfactuality (Excludes). What is asserted is a relation to the topic, not to the situation, so the counterfactual inference is cancellable and John was in the classroom; in fact he still is is consistent (Claim.consistent_with_inclusion). The library's Modality.Exclusion.ExclF on context towers is the feature at a point-sized topic (exclF_iff_excludes).

One feature over worlds leaves the rest of the antecedent to be evaluated as with present tense, so the future less vivid and the present counterfactual readings are the future and present evaluation times of the predicate's Aktionsart: Table 1 is Table 2 (readings), and the pluperfect's second layer makes a past counterfactual whatever the predicate. Aspect and mood are not ingredients: the imperfective of Greek and French is absent from English (imperfective_not_universal), and the subjunctive appears in a counterfactual only where a past subjunctive paradigm lets it co-occur with the feature, so French, having lost its past subjunctive, keeps the past indicative (antecedent_french).

Implementation notes

• Exclusion is disjointness of sets of times or worlds, the speaker's coordinate being a set of epistemically accessible alternatives; the before of temporal past is TemporalPast.
• The counterfactual types keep the name CounterfactualType, which Mizuno2024 refers to.

References

• [Iat00]

The exclusion feature

def Iatridou2000.Excludes {X : Type u_1} (topic speaker : Set X) : Prop

(49): the topic excludes the speaker's, as sets of times or of worlds.

Equations

• Iatridou2000.Excludes topic speaker = Disjoint topic speaker

def Iatridou2000.TemporalPast {X : Type u_1} [Preorder X] (topic speaker : Set X) : Prop

Footnote 19: temporal past is exclusion augmented by before.

Equations

• Iatridou2000.TemporalPast topic speaker = ∀ t ∈ topic, ∀ u ∈ speaker, t < u

theorem Iatridou2000.excludes_of_temporalPast {X : Type u_1} [Preorder X] {topic speaker : Set X} (h : TemporalPast topic speaker) : Excludes topic speaker

structure Iatridou2000.Claim (X : Type u_2) : Type u_2

What the feature contributes to an assertion: the situation, the p-worlds or the situation time, holds throughout a topic that excludes the speaker's.

• topic : Set X
• speaker : Set X
• situation : Set X
• topic_subset : self.topic ⊆ self.situation
• excludes : Excludes self.topic self.speaker

theorem Iatridou2000.Claim.consistent_with_inclusion : ∃ (c : Claim Bool), c.speaker ⊆ c.situation ∧ c.topic.Nonempty ∧ c.speaker.Nonempty

(58)–(59): the claim leaves open whether the situation includes the speaker's worlds or times, so the counterfactual inference is an implicature and in fact, he still is is consistent.

theorem Iatridou2000.Claim.excludes_situation_iff {X : Type u_1} (c : Claim X) : Excludes c.situation c.speaker ↔ ∀ x ∈ c.speaker, x ∉ c.situation

The situation itself excludes the speaker's only when the speaker's coordinate lies outside it, which the feature does not assert.

theorem Iatridou2000.exclF_iff_excludes {W : Type u_2} {E : Type u_3} {P : Type u_4} {T : Type u_5} (tower : Reference.ContextTower (Reference.Context W E P T)) : (Modality.Exclusion.ExclF Modality.Exclusion.ExclDimension.temporal tower ↔ Excludes {tower.innermost.time} {tower.origin.time}) ∧ (Modality.Exclusion.ExclF Modality.Exclusion.ExclDimension.modal tower ↔ Excludes {tower.innermost.world} {tower.origin.world})

The library's exclusion feature on a context tower is the feature at a point-sized topic: the innermost coordinate against the origin's.

The three counterfactuals

inductive Iatridou2000.CounterfactualType : Type

The counterfactual conditionals of the paper: future less vivid, present counterfactual and past counterfactual.

• flv : CounterfactualType
• presCF : CounterfactualType
• pastCF : CounterfactualType

@[instance_reducible]

instance Iatridou2000.instDecidableEqCounterfactualType : DecidableEq CounterfactualType

Equations

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

@[instance_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.dimensions : CounterfactualType → Finset Modality.Exclusion.ExclDimension

The dimensions the exclusion features of a counterfactual range over: one over worlds, and for the past counterfactual the pluperfect's second layer over times.

Equations

• Iatridou2000.CounterfactualType.flv.dimensions = {Modality.Exclusion.ExclDimension.modal}
• Iatridou2000.CounterfactualType.presCF.dimensions = {Modality.Exclusion.ExclDimension.modal}
• Iatridou2000.CounterfactualType.pastCF.dimensions = {Modality.Exclusion.ExclDimension.modal, Modality.Exclusion.ExclDimension.temporal}

inductive Iatridou2000.Aktionsart : Type

The Aktionsart of the antecedent's predicate: telic, activity (footnote 24), individual-level stative or stage-level stative.

• telic : Aktionsart
• activity : Aktionsart
• ilStative : Aktionsart
• slStative : Aktionsart

@[instance_reducible]

instance Iatridou2000.instDecidableEqAktionsart : DecidableEq Aktionsart

Equations

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

def Iatridou2000.instReprAktionsart.repr : Aktionsart → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Iatridou2000.instReprAktionsart : Repr Aktionsart

Equations

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

inductive Iatridou2000.Evaluation : Type

The times at which an antecedent can be evaluated.

• future : Evaluation
• now : Evaluation

@[instance_reducible]

instance Iatridou2000.instDecidableEqEvaluation : DecidableEq Evaluation

Equations

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

def Iatridou2000.instReprEvaluation.repr : Evaluation → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Iatridou2000.instReprEvaluation : Repr Evaluation

Equations

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

def Iatridou2000.Aktionsart.evaluation : Aktionsart → Finset Evaluation

Table 2: the earliest evaluation of a present-tense antecedent by the predicate's Aktionsart, (65)–(67).

Equations

• Iatridou2000.Aktionsart.telic.evaluation = {Iatridou2000.Evaluation.future}
• Iatridou2000.Aktionsart.activity.evaluation = {Iatridou2000.Evaluation.future}
• Iatridou2000.Aktionsart.ilStative.evaluation = {Iatridou2000.Evaluation.now}
• Iatridou2000.Aktionsart.slStative.evaluation = {Iatridou2000.Evaluation.future, Iatridou2000.Evaluation.now}

def Iatridou2000.Evaluation.reading : Evaluation → CounterfactualType

After one feature has set up the topic worlds, evaluation in the future is the future less vivid and evaluation now the present counterfactual.

Equations

• Iatridou2000.Evaluation.future.reading = Iatridou2000.CounterfactualType.flv
• Iatridou2000.Evaluation.now.reading = Iatridou2000.CounterfactualType.presCF

def Iatridou2000.readings (a : Aktionsart) : Finset CounterfactualType

Table 1, derived from Table 2: the readings of a conditional with one exclusion feature on a predicate of the given Aktionsart.

Equations

• Iatridou2000.readings a = Finset.image Iatridou2000.Evaluation.reading a.evaluation

theorem Iatridou2000.readings_telic : readings Aktionsart.telic = {CounterfactualType.flv}

theorem Iatridou2000.readings_ilStative : readings Aktionsart.ilStative = {CounterfactualType.presCF}

theorem Iatridou2000.readings_slStative : readings Aktionsart.slStative = {CounterfactualType.flv, CounterfactualType.presCF}

(64): a stage-level stative yields either reading.

theorem Iatridou2000.pastCF_notMem_readings (a : Aktionsart) : CounterfactualType.pastCF ∉ readings a

A single feature never yields the past counterfactual.

theorem Iatridou2000.one_feature {W : Type u_2} {E : Type u_3} {P : Type u_4} {T : Type u_5} (c : Reference.Context W E P T) {w' : W} (hw : w' ≠ c.world) : Modality.Exclusion.ExclF Modality.Exclusion.ExclDimension.modal ((Reference.ContextTower.root c).push (Reference.worldShift w')) ∧ ¬Modality.Exclusion.ExclF Modality.Exclusion.ExclDimension.temporal ((Reference.ContextTower.root c).push (Reference.worldShift w'))

The one-feature conditionals: a world shift alone excludes on worlds and, keeping the time, not on times.

theorem Iatridou2000.two_features {W : Type u_2} {E : Type u_3} {P : Type u_4} {T : Type u_5} (c : Reference.Context W E P T) {w' : W} {t' : T} (hw : w' ≠ c.world) (ht : t' ≠ c.time) : Modality.Exclusion.ExclF Modality.Exclusion.ExclDimension.modal (((Reference.ContextTower.root c).push (Reference.worldShift w')).push (Reference.temporalShift t')) ∧ Modality.Exclusion.ExclF Modality.Exclusion.ExclDimension.temporal (((Reference.ContextTower.root c).push (Reference.worldShift w')).push (Reference.temporalShift t'))

The pluperfect's two layers: a world shift and a temporal shift exclude on both dimensions, the past counterfactual.

Aspect and mood

inductive Iatridou2000.CFAspect : Type

The grammatical aspect a language requires in its counterfactuals (Section 5): the imperfective, none, or either.

• imperfective : CFAspect
• none : CFAspect
• either : CFAspect

@[instance_reducible]

instance Iatridou2000.instDecidableEqCFAspect : DecidableEq CFAspect

Equations

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

@[instance_reducible]

instance Iatridou2000.instReprCFAspect : Repr CFAspect

Equations

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

def Iatridou2000.instReprCFAspect.repr : CFAspect → ℕ → Std.Format

Equations

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

inductive Iatridou2000.AspectLanguage : Type

The languages whose counterfactual morphology Section 5 compares.

• greek : AspectLanguage
• french : AspectLanguage
• english : AspectLanguage
• polish : AspectLanguage

@[instance_reducible]

instance Iatridou2000.instDecidableEqAspectLanguage : DecidableEq AspectLanguage

Equations

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

@[instance_reducible]

instance Iatridou2000.instReprAspectLanguage : Repr AspectLanguage

Equations

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

def Iatridou2000.instReprAspectLanguage.repr : AspectLanguage → ℕ → Std.Format

Equations

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

def Iatridou2000.AspectLanguage.cfAspect : AspectLanguage → CFAspect

Greek and French require the imperfective, English has no such requirement, and Polish allows either aspect.

Equations

• Iatridou2000.AspectLanguage.greek.cfAspect = Iatridou2000.CFAspect.imperfective
• Iatridou2000.AspectLanguage.french.cfAspect = Iatridou2000.CFAspect.imperfective
• Iatridou2000.AspectLanguage.english.cfAspect = Iatridou2000.CFAspect.none
• Iatridou2000.AspectLanguage.polish.cfAspect = Iatridou2000.CFAspect.either

theorem Iatridou2000.imperfective_not_universal : ¬∀ (l : AspectLanguage), l.cfAspect = CFAspect.imperfective

The imperfective is not an ingredient of counterfactuality.

inductive Iatridou2000.SubjunctiveParadigm : Type

Whether a language has a past subjunctive paradigm (Section 6.1).

• past : SubjunctiveParadigm
• nonpastOnly : SubjunctiveParadigm
• none : SubjunctiveParadigm

@[instance_reducible]

instance Iatridou2000.instDecidableEqSubjunctiveParadigm : DecidableEq SubjunctiveParadigm

Equations

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

@[instance_reducible]

instance Iatridou2000.instReprSubjunctiveParadigm : Repr SubjunctiveParadigm

Equations

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

def Iatridou2000.instReprSubjunctiveParadigm.repr : SubjunctiveParadigm → ℕ → Std.Format

Equations

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

def Iatridou2000.antecedentForm : SubjunctiveParadigm → Mood.SubjunctiveType ⊕ Unit

The form of a counterfactual antecedent: the feature on the subjunctive when a past subjunctive exists, else on the indicative; a nonpast subjunctive never expresses the feature, so it loses to the past indicative, the French choice of (99).

Equations

• Iatridou2000.antecedentForm Iatridou2000.SubjunctiveParadigm.past = Sum.inl Mood.SubjunctiveType.counterfactual
• Iatridou2000.antecedentForm Iatridou2000.SubjunctiveParadigm.nonpastOnly = Sum.inr ()
• Iatridou2000.antecedentForm Iatridou2000.SubjunctiveParadigm.none = Sum.inr ()

theorem Iatridou2000.subjunctive_of_antecedentForm {p : SubjunctiveParadigm} {s : Mood.SubjunctiveType} (h : antecedentForm p = Sum.inl s) : p = SubjunctiveParadigm.past

Section 6.1: a counterfactual carries the subjunctive only in a language with a past subjunctive paradigm.

theorem Iatridou2000.antecedent_french : antecedentForm SubjunctiveParadigm.nonpastOnly = Sum.inr ()

French has only a nonpast subjunctive, so its counterfactual antecedents carry the past indicative, (99).

theorem Iatridou2000.antecedent_german : antecedentForm SubjunctiveParadigm.past = Sum.inl Mood.SubjunctiveType.counterfactual

German and Italian have a past subjunctive and use it.