Exclusion features and X/O-marking strategies

@cite{iatridou-2000} @cite{condoravdi-2002} @cite{deal-2020} @cite{anderson-1951} @cite{schlenker-2004} @cite{von-fintel-iatridou-2023}

Framework primitives for the Exclusion Feature analysis of past morphology (@cite{iatridou-2000}) and the X-marking / O-marking typology of counterfactuality (@cite{von-fintel-iatridou-2023}).

This file provides the framework primitives — types, predicates, and bridge theorems usable by any study of counterfactuals or crosslinguistic conditional morphology. Paper-specific typologies and empirical claims live in the corresponding Studies/ files:

• Phenomena/Conditionals/Studies/Iatridou2000.lean — IatridouPredType / CounterfactualType / classifyCounterfactual (FLV/PresCF/PastCF taxonomy)
• Phenomena/Conditionals/Studies/Mizuno2024.lean — Anderson-conditional empirical observations (English X-marking, Japanese O-marking, FLV correlation)

Core claims

Past morphology encodes exclusion:

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

This maps onto the ContextTower's origin / innermost distinction: ExclF dim tower holds iff the relevant coordinate of tower.innermost differs from that of tower.origin.

The X-marking / O-marking distinction (per @cite{von-fintel-iatridou-2023}) is the typological label for whether a language uses counterfactual morphology (X-marking, produces ExclF) or some other strategy (O-marking, e.g., Japanese Historical Present) to grammatically distinguish live from non-live possibilities.

Bicontextual semantics

@cite{schlenker-2004} distinguishes the Context of Thought θ (speech-act context, anchors temporal indexicals) from the Context of Utterance v (can be shifted by HP). The ContextTower implements this distinction: tower.origin = θ, tower.innermost = v. The origin_stable theorem captures Schlenker's claim that θ-anchored indexicals are unaffected by HP/CF shifts.

inductive Semantics.Modality.Exclusion.ExclDimension : Type

The two dimensions along which past morphology can exclude.

@cite{iatridou-2000}'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 : Core.Context.ContextTower (Core.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).

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)

theorem Semantics.Modality.Exclusion.exclF_temporal_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Core.Context.ContextTower (Core.Context.KContext W E P T)) : ExclF ExclDimension.temporal tower ↔ tower.innermost.time ≠ tower.origin.time

ExclF temporal unfolds to time inequality.

theorem Semantics.Modality.Exclusion.exclF_modal_iff {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Core.Context.ContextTower (Core.Context.KContext W E P T)) : ExclF ExclDimension.modal tower ↔ tower.innermost.world ≠ tower.origin.world

ExclF modal unfolds to world inequality.

def Semantics.Modality.Exclusion.ExclDimension.toDealUse : ExclDimension → Tense.Counterfactual.PastMorphologyUse

Map ExclDimension to @cite{deal-2020}'s PastMorphologyUse.

This connects @cite{iatridou-2000}'s exclusion analysis to @cite{deal-2020}'s tense typology: temporal exclusion corresponds to temporal tense, modal exclusion corresponds to counterfactual tense.

Equations

• Semantics.Modality.Exclusion.ExclDimension.temporal.toDealUse = Semantics.Tense.Counterfactual.PastMorphologyUse.temporal
• Semantics.Modality.Exclusion.ExclDimension.modal.toDealUse = Semantics.Tense.Counterfactual.PastMorphologyUse.counterfactual

theorem Semantics.Modality.Exclusion.exclF_temporal_is_deal_temporal : ExclDimension.temporal.toDealUse = Tense.Counterfactual.PastMorphologyUse.temporal

theorem Semantics.Modality.Exclusion.exclF_modal_is_deal_cf : ExclDimension.modal.toDealUse = Tense.Counterfactual.PastMorphologyUse.counterfactual

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 : Core.Context.KContext W E P T) (w' : W) (t' : T) (h : w' ≠ c.world) : ExclF ExclDimension.modal ((Core.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 @cite{iatridou-2000}'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 : Core.Context.KContext W E P T) (t' : T) (h : t' ≠ c.time) : ExclF ExclDimension.temporal ((Core.Context.ContextTower.root c).push (Core.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 : Core.Context.KContext W E P T) (w' : W) (t' t'' : T) (hw : w' ≠ c.world) (ht : t'' ≠ c.time) : have tower := ((Core.Context.ContextTower.root c).push (Mood.subjShift w' t')).push (Core.Context.temporalShift t''); ExclF ExclDimension.modal tower ∧ ExclF ExclDimension.temporal tower

Two shifts → both ExclFs (the PastCF configuration).

theorem Semantics.Modality.Exclusion.root_no_temporal_exclF {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Core.Context.KContext W E P T) : ¬ExclF ExclDimension.temporal (Core.Context.ContextTower.root c)

theorem Semantics.Modality.Exclusion.root_no_modal_exclF {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Core.Context.KContext W E P T) : ¬ExclF ExclDimension.modal (Core.Context.ContextTower.root c)

theorem Semantics.Modality.Exclusion.xMarking_produces_modal_exclF {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (rc : Core.Context.RichContext W E P T) (pastTime : T) (cfWorld : W) (expandedDomain : Set W) (h : cfWorld ≠ rc.base.world) : ((Core.Context.xMarkingShift pastTime cfWorld expandedDomain).apply rc).base.world ≠ rc.base.world

X-marking shift produces modal ExclF on RichContext towers.

xMarkingShift (from Core.Context.Rich) changes both world and time. When the counterfactual world differs from the origin, the resulting tower has modal ExclF.

Kratzer-level counterpart: in @cite{kratzer-2012}'s modal semantics, the same X-marking operation corresponds to ∗-revision of the modal base (Semantics.Modality.Kratzer.XMarking.IsStarRevision): the expandedDomain parameter here maps to the widened accessible world set ∩f'(w) ⊇ ∩f(w). See @cite{ferreira-2023} for the full 2×2 square of necessities generated by X-marking on both modal base (Xf) and ordering source (Xg).

inductive Semantics.Modality.Exclusion.MarkingStrategy : Type

The two crosslinguistic strategies for grammatically distinguishing live from non-live possibilities (@cite{von-fintel-iatridou-2023}'s typological label).

Used by @cite{mizuno-2024} 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⁺. "Actually" in the consequent recovers the actual world via Kaplanian origin access. English: "If Jones had taken arsenic, he would have shown exactly the symptoms he is actually showing."

• oMarking : MarkingStrategy

  O-marking: Non-Past morphology triggers a perspectival shift analogous to the Historical Present (@cite{schlenker-2004}). The backward time shift expands the domain under branching time, avoiding triviality without counterfactual morphology. The actual world is directly accessible (no world shift, so no need for "actually"). Japanese: "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 ⋯

@[implicit_reducible]

instance Semantics.Modality.Exclusion.instReprMarkingStrategy : Repr MarkingStrategy

Equations

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

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

Equations

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

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

X-marking strategy uses counterfactual morphology; O-marking does not. The single primitive property of marking strategies; all others (producesExclF, requiresActuallyOperator) derive from it.

Equations

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

@[reducible, inline]

abbrev Semantics.Modality.Exclusion.MarkingStrategy.producesExclF (s : MarkingStrategy) : Bool

X-marking produces ExclF; O-marking does not.

X-marking is counterfactual morphology: subjShift changes the evaluation world, creating modal ExclF. O-marking leaves the tower at the root, so no ExclF arises. Definitionally equal to hasXMarking.

Equations

• s.producesExclF = s.hasXMarking

@[reducible, inline]

abbrev Semantics.Modality.Exclusion.MarkingStrategy.requiresActuallyOperator (s : MarkingStrategy) : Bool

X-marking requires "actually" to recover the actual world; O-marking does not. When X-marking produces ExclF, the actual world is excluded from the shifted evaluation; "actually" (Kaplanian origin access) reaches back through the shift. With O-marking, the evaluation world IS the actual world. Definitionally equal to hasXMarking.

Equations

• s.requiresActuallyOperator = s.hasXMarking

def Semantics.Modality.Exclusion.MarkingStrategy.exclDimension : MarkingStrategy → Option ExclDimension

Map marking strategies to the ExclDimension they produce.

Equations

• Semantics.Modality.Exclusion.MarkingStrategy.xMarking.exclDimension = some Semantics.Modality.Exclusion.ExclDimension.modal
• Semantics.Modality.Exclusion.MarkingStrategy.oMarking.exclDimension = none

def Semantics.Modality.Exclusion.MarkingStrategy.toDealUse : MarkingStrategy → Tense.Counterfactual.PastMorphologyUse

Map marking strategies to @cite{deal-2020}'s PastMorphologyUse.

Equations

• Semantics.Modality.Exclusion.MarkingStrategy.xMarking.toDealUse = Semantics.Tense.Counterfactual.PastMorphologyUse.counterfactual
• Semantics.Modality.Exclusion.MarkingStrategy.oMarking.toDealUse = Semantics.Tense.Counterfactual.PastMorphologyUse.temporal

theorem Semantics.Modality.Exclusion.xMarking_exclDimension : MarkingStrategy.xMarking.exclDimension = some ExclDimension.modal

theorem Semantics.Modality.Exclusion.oMarking_no_exclDimension : MarkingStrategy.oMarking.exclDimension = none

theorem Semantics.Modality.Exclusion.xMarking_is_deal_counterfactual : MarkingStrategy.xMarking.toDealUse = Tense.Counterfactual.PastMorphologyUse.counterfactual

theorem Semantics.Modality.Exclusion.oMarking_is_deal_temporal : MarkingStrategy.oMarking.toDealUse = Tense.Counterfactual.PastMorphologyUse.temporal

theorem Semantics.Modality.Exclusion.xMarking_excl_deal_consistent : Option.map ExclDimension.toDealUse MarkingStrategy.xMarking.exclDimension = some MarkingStrategy.xMarking.toDealUse

theorem Semantics.Modality.Exclusion.xMarking_produces_exclF {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) (h : w' ≠ c.world) : ExclF ExclDimension.modal ((Core.Context.ContextTower.root c).push (Mood.subjShift w' t'))

X-marking produces modal ExclF: subjunctive shift changes the world, creating world exclusion. Wraps subjShift_produces_modal_exclF.

theorem Semantics.Modality.Exclusion.actually_recovers_origin_after_shift {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) (σ : Core.Context.ContextShift (Core.Context.KContext W E P T)) : Reference.Kaplan.opActually_access.resolve (t.push σ) = Reference.Kaplan.opActually_access.resolve t

"Actually" recovers the origin world even after a tower shift.

In an X-marked Anderson conditional, the CF morphology pushes the tower (shifting the evaluation world). But "actually" — being a Kaplanian indexical with depth = .origin — resolves to the speech-act world regardless. Wraps opActually_shift_invariant.

theorem Semantics.Modality.Exclusion.oMarking_no_exclF {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Core.Context.KContext W E P T) : ¬ExclF ExclDimension.modal (Core.Context.ContextTower.root c)

O-marking has no modal ExclF: without CF morphology, the tower stays at the root. Wraps root_no_modal_exclF.

theorem Semantics.Modality.Exclusion.domain_expansion_avoids_triviality {W : Type u_1} (smallDomain expandedDomain : Set W) (consequent : W → Prop) (h_subset : smallDomain ⊆ expandedDomain) (h_trivial : Tense.ConditionalShift.trivialConsequent smallDomain consequent) (w : W) (hw : w ∈ expandedDomain) (hw_fails : ¬consequent w) : Tense.ConditionalShift.nonTrivialConsequent expandedDomain consequent

Both X-marking and O-marking avoid the triviality problem by expanding the domain. General pattern: if a domain expansion produces a world where the consequent fails, the conditional is non-trivial.

• X-marking achieves this via xMarkingShift (CF morphology → D⁺)
• O-marking achieves this via hpShift (HP → backward time → D⁺)

Wraps ConditionalShift.expansion_resolves_triviality.

theorem Semantics.Modality.Exclusion.oMarking_hpShift_expanding {W : Type u_5} {T : Type u_6} [Preorder T] (history : Core.Modality.HistoricalAlternatives.WorldHistory W T) (h_bc : history.backwardsClosed) (w₀ : W) (t₀ t' : T) (h_earlier : t' ≤ t₀) (D : Set W) (h_domain : D ⊆ history { world := w₀, time := t₀ }) : D ⊆ history { world := w₀, time := t' }

End-to-end O-marking domain expansion: backwards-closed history + backward time shift → the HP-shifted domain contains the original.

Connects three layers:

1. BranchingTime.WorldHistory.backwardsClosed (semantic property)
2. ConditionalShift.history_monotone_set (set-level monotonicity)
3. hpShift installs the expanded domain

theorem Semantics.Modality.Exclusion.oMarking_trivial {W : Type u_1} (domain : Set W) (antecedent consequent : W → Prop) (h_trivial : Tense.ConditionalShift.trivialConsequent domain consequent) : Tense.ConditionalShift.domainRestrictedConditional domain antecedent consequent

The O-marking triviality problem: without domain expansion, the Anderson conditional is vacuously true. The domainRestrictedConditional over the non-expanded domain D is trivially satisfied because the consequent (an observed fact) holds at every world in D.

theorem Semantics.Modality.Exclusion.expanded_conditional_informative {W : Type u_1} (expandedDomain : Set W) (antecedent consequent : W → Prop) (h_nontrivial : Tense.ConditionalShift.nonTrivialConsequent expandedDomain consequent) (h_cond : Tense.ConditionalShift.domainRestrictedConditional expandedDomain antecedent consequent) : ∃ w ∈ expandedDomain, ¬antecedent w

The X/O-marking payoff: when domain expansion makes the consequent non-trivial, the antecedent of a true conditional must exclude at least one world in D⁺. The Anderson conditional is informative — the antecedent restriction partitions D⁺ into consequent-satisfying worlds (selected by the conditional) and consequent-failing worlds (excluded by the antecedent).

theorem Semantics.Modality.Exclusion.oMarking_indexicals_at_origin {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (ap : Core.Context.AccessPattern (Core.Context.KContext W E P T) W) (hd : ap.depth = Core.Context.DepthSpec.origin) (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) (σ : Core.Context.ContextShift (Core.Context.KContext W E P T)) : ap.resolve (t.push σ) = ap.resolve t

In O-marking (HP) strategy, temporal indexicals still evaluate against the speech-act context (θ = origin), not the shifted context (v = innermost).

This explains why Japanese sakuya 'last night' in the antecedent of an HP-shifted O-marked conditional evaluates against the utterance time, paralleling the behavior of seventy-eight years ago in @cite{schlenker-2004}'s HP example.