Exclusion features and X/O-marking strategies

[Iat00] [vFI23] [And51] [Sch04b] [Miz24]

Framework primitives for the Exclusion Feature analysis of past morphology ([Iat00]) and the X-marking / O-marking typology of counterfactuality ([vFI23]). Paper-specific typologies and empirical claims live in the corresponding Studies/ files:

• Studies/Iatridou2000.lean — IatridouPredType / CounterfactualType / classifyCounterfactual (FLV/PresCF/PastCF taxonomy) and the tower-bridge theorems consuming ExclF
• Studies/Mizuno2024.lean — Anderson-conditional empirical observations (English X-marking, Japanese/Mandarin O-marking, FLV correlation)

Core claims

Past morphology encodes exclusion ([Iat00]):

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

This maps onto the ContextTower's origin / innermost distinction — [Sch04b]'s Context of Thought θ (= tower.origin) vs Context of Utterance υ (= tower.innermost): ExclF dim tower holds iff the relevant coordinate of tower.innermost differs from that of tower.origin. At a root tower the two coincide, so no ExclF holds; a subjunctive shift produces the modal feature and a temporal shift the temporal one (subjShift_produces_modal_exclF, temporalShift_produces_temporal_exclF).

The X-marking / O-marking distinction ([vFI23]) is the typological label for whether a language uses counterfactual morphology (X-marking) or some other strategy (O-marking, e.g., the Japanese Historical Present of [Miz24]) to grammatically distinguish live from non-live possibilities.

ExclF: the exclusion feature

inductive Semantics.Modality.Exclusion.ExclDimension : Type

The two dimensions along which past morphology can exclude.

[Iat00]'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)

@[implicit_reducible]

instance Semantics.Modality.Exclusion.instDecidableEqExclDimension : DecidableEq ExclDimension

Equations

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

def Semantics.Modality.Exclusion.instReprExclDimension.repr : ExclDimension → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Modality.Exclusion.instReprExclDimension : Repr ExclDimension

Equations

• Semantics.Modality.Exclusion.instReprExclDimension = { reprPrec := Semantics.Modality.Exclusion.instReprExclDimension.repr }

def Semantics.Modality.Exclusion.ExclF {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (dim : ExclDimension) (tower : Context.ContextTower (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). At a root tower innermost and origin coincide, so neither dimension's feature holds.

Equations

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

Shifts produce ExclF

theorem Semantics.Modality.Exclusion.subjShift_produces_modal_exclF {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Context.KContext W E P T) (w' : W) (t' : T) (h : w' ≠ c.world) : ExclF ExclDimension.modal ((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 [Iat00]'s claim that counterfactual morphology signals world exclusion.

theorem Semantics.Modality.Exclusion.temporalShift_produces_temporal_exclF {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Context.KContext W E P T) (t' : T) (h : t' ≠ c.time) : ExclF ExclDimension.temporal ((Context.ContextTower.root c).push (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.Modality.Exclusion.two_shifts_two_exclFs {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Context.KContext W E P T) (w' : W) (t' t'' : T) (hw : w' ≠ c.world) (ht : t'' ≠ c.time) : ExclF ExclDimension.modal (((Context.ContextTower.root c).push (Mood.subjShift w' t')).push (Context.temporalShift t'')) ∧ ExclF ExclDimension.temporal (((Context.ContextTower.root c).push (Mood.subjShift w' t')).push (Context.temporalShift t''))

Two shifts → both ExclFs: a subjunctive (world) shift followed by a temporal one yields modal and temporal exclusion together — the PastCF configuration of [Iat00] (two past layers).

X-marking / O-marking typology ([vFI23])

inductive Semantics.Modality.Exclusion.MarkingStrategy : Type

The two crosslinguistic strategies for grammatically distinguishing live from non-live possibilities ([vFI23]'s typological label).

Used by [Miz24] to characterize how different languages express Anderson conditionals: English uses X-marking (counterfactual morphology), Japanese uses O-marking (Non-Past + Historical Present).

• xMarking : MarkingStrategy

  X-marking: counterfactual morphology expands the domain from D to D⁺. English ([Miz24], ex. 1a): "If Jones had taken arsenic last night, he would show those symptoms which he is now showing."

• oMarking : MarkingStrategy

  O-marking: the absence of X-marking. In Japanese Anderson conditionals, Non-Past morphology triggers a perspectival shift analogous to the Historical Present ([Sch04b]); the backward time shift expands the domain under branching time, avoiding triviality without counterfactual morphology. Japanese ([Miz24], ex. 4a): "Jones-si-ga ... nom-eba, ... mise-ru hazuda."

@[implicit_reducible]

instance Semantics.Modality.Exclusion.instDecidableEqMarkingStrategy : DecidableEq MarkingStrategy

Equations

• Semantics.Modality.Exclusion.instDecidableEqMarkingStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Modality.Exclusion.instReprMarkingStrategy.repr : MarkingStrategy → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Modality.Exclusion.instReprMarkingStrategy : Repr MarkingStrategy

Equations

• Semantics.Modality.Exclusion.instReprMarkingStrategy = { reprPrec := Semantics.Modality.Exclusion.instReprMarkingStrategy.repr }

def Semantics.Modality.Exclusion.MarkingStrategy.hasXMarking : MarkingStrategy → Bool

X-marking strategy uses counterfactual morphology; O-marking does not.

Equations

• Semantics.Modality.Exclusion.MarkingStrategy.xMarking.hasXMarking = true
• Semantics.Modality.Exclusion.MarkingStrategy.oMarking.hasXMarking = false

def Semantics.Modality.Exclusion.MarkingStrategy.other : MarkingStrategy → MarkingStrategy

The complementary marking strategy. O-marking "is generally defined as the absence of X-marking" ([Miz24], §2), so the two strategies complement each other: in a minimal pair, the alternative realizes the other of the attested strategy.

Equations

• Semantics.Modality.Exclusion.MarkingStrategy.xMarking.other = Semantics.Modality.Exclusion.MarkingStrategy.oMarking
• Semantics.Modality.Exclusion.MarkingStrategy.oMarking.other = Semantics.Modality.Exclusion.MarkingStrategy.xMarking

@[simp]

theorem Semantics.Modality.Exclusion.MarkingStrategy.other_other (s : MarkingStrategy) : s.other.other = s

X-marking exponents ([vFI23] §2, "The form")

inductive Semantics.Modality.Exclusion.XMarkingHost : Type

The morphology realizing X-marking ([vFI23] §2): dedicated, or borrowed from past / imperfective / future / subjunctive; [Miz24] (§4.2) adds the Mandarin perfective.

• dedicated : XMarkingHost

  Dedicated X-morphology with no other use (Hungarian -nA).

• past : XMarkingHost

  Fake past ([Iat00]; English, Greek, Romance).

• imperfective : XMarkingHost

  Fake imperfective (Greek, Romance).

• future : XMarkingHost

  Future / woll (English would; the Greek and Romance consequent).

• subjunctive : XMarkingHost

  Past subjunctive (German, Icelandic).

• perfective : XMarkingHost

  Perfective ([Miz24], §4.2: Mandarin consequent-final le).

@[implicit_reducible]

instance Semantics.Modality.Exclusion.instDecidableEqXMarkingHost : DecidableEq XMarkingHost

Equations

• Semantics.Modality.Exclusion.instDecidableEqXMarkingHost x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Modality.Exclusion.instReprXMarkingHost : Repr XMarkingHost

Equations

• Semantics.Modality.Exclusion.instReprXMarkingHost = { reprPrec := Semantics.Modality.Exclusion.instReprXMarkingHost.repr }

def Semantics.Modality.Exclusion.instReprXMarkingHost.repr : XMarkingHost → ℕ → Std.Format

Equations

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

structure Semantics.Modality.Exclusion.XMarkingExponent : Type

A language's X-marking exponent: citation form and (possibly complex — Greek: past + imperfective) components. Option-valued xMarking entries live in Fragments/{Language}/Conditionals.lean; total uniformity ([vFI23] p. 1471) bets every language has one.

• form : String
• components : List XMarkingHost

def Semantics.Modality.Exclusion.instDecidableEqXMarkingExponent.decEq (x✝ x✝¹ : XMarkingExponent) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Semantics.Modality.Exclusion.instDecidableEqXMarkingExponent : DecidableEq XMarkingExponent

Equations

• Semantics.Modality.Exclusion.instDecidableEqXMarkingExponent = Semantics.Modality.Exclusion.instDecidableEqXMarkingExponent.decEq

@[implicit_reducible]

instance Semantics.Modality.Exclusion.instReprXMarkingExponent : Repr XMarkingExponent

Equations

• Semantics.Modality.Exclusion.instReprXMarkingExponent = { reprPrec := Semantics.Modality.Exclusion.instReprXMarkingExponent.repr }

def Semantics.Modality.Exclusion.instReprXMarkingExponent.repr : XMarkingExponent → ℕ → Std.Format

Equations

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