Anderson Conditionals and Domain Expansion

@cite{condoravdi-2002} @cite{mizuno-2024} @cite{schlenker-2004}

Formalizes the connection between backward temporal shifts and domain expansion in conditionals. @cite{mizuno-2024} argues that Japanese Anderson conditionals use the Historical Present (@cite{schlenker-2004}) to achieve domain expansion without X-marking: Non-Past morphology shifts the evaluation time backward, and under branching time (@cite{condoravdi-2002}), earlier times have more historical alternatives, so the domain expands.

Key Results

• andersonConditional — HP-shifted antecedent evaluated against expanded domain
• hp_achieves_expansion — backward time + domain monotonicity yields expansion
• trivialConsequent / nonTrivialConsequent — formalize the triviality puzzle
• expansion_resolves_triviality — domain expansion makes conditionals non-trivial
• Bridge to BranchingTime.historicalBase and Mood.SUBJ

Connection to ContextTower

The HP shift in an Anderson conditional is modeled as a tower push of an hpShift: a context shift that moves time backward and expands the domain. In @cite{schlenker-2004}'s terms, the push shifts the Context of Utterance v while preserving the Context of Thought θ (= tower.origin).

def Semantics.Tense.ConditionalShift.andersonConditional {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (antecedent consequent : Core.Context.RichContext W E P T → Prop) (hpTime : T) (expandedDomain : Set W) (rc : Core.Context.RichContext W E P T) : Prop

An Anderson conditional (context-level model): the antecedent is evaluated at an HP-shifted context (backward time, expanded domain), and the consequent is evaluated at the original context.

This models the HP shift's effect on a single evaluation point. The full Kratzer-style analysis — restricted universal quantification over the expanded domain D⁺ — is domainRestrictedConditional:

domainRestrictedConditional D⁺ antecedent consequent = ∀ w ∈ D⁺, antecedent(w) → consequent(w)

The domain expansion machinery here (hpShift, hp_achieves_expansion) provides the D⁺, and trivial_domainRestricted / nontrivial_conditional_excludes show why expansion matters.

Equations

• Semantics.Tense.ConditionalShift.andersonConditional antecedent consequent hpTime expandedDomain rc = (antecedent ((Core.Context.hpShift hpTime expandedDomain).apply rc) → consequent rc)

theorem Semantics.Tense.ConditionalShift.anderson_shifted_time {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (hpTime : T) (expandedDomain : Set W) (rc : Core.Context.RichContext W E P T) : ((Core.Context.hpShift hpTime expandedDomain).apply rc).time = hpTime

The HP-shifted context in an Anderson conditional has the shifted time.

theorem Semantics.Tense.ConditionalShift.hp_achieves_expansion {W : Type u_1} {T : Type u_2} [Preorder T] (history : Core.Modality.HistoricalAlternatives.WorldHistory W T) (h_bc : history.backwardsClosed) (s₀ : Core.WorldTimeIndex W T) (t' : T) (h_earlier : t' ≤ s₀.time) (w : W) (hw : w ∈ history s₀) : w ∈ history { world := s₀.world, time := t' }

@cite{mizuno-2024}'s argument: backward time + domain monotonicity yields expansion.

If the world history is backwards-closed (worlds that agree up to t also agree up to t' ≤ t), then the historical alternatives at an earlier time are a superset of those at a later time. This is why O-marking (Non-Past / HP) in Japanese Anderson conditionals expands the domain without X-marking.

theorem Semantics.Tense.ConditionalShift.history_monotone_set {W : Type u_1} {T : Type u_2} [Preorder T] (history : Core.Modality.HistoricalAlternatives.WorldHistory W T) (h_bc : history.backwardsClosed) (s₀ : Core.WorldTimeIndex W T) (t' : T) (h_earlier : t' ≤ s₀.time) : history s₀ ⊆ history { world := s₀.world, time := t' }

Set-level monotonicity: under backwards-closed history, the set of historical alternatives at an earlier time is a superset of those at a later time. This lifts hp_achieves_expansion (element-level) to Set.Subset (set-level), connecting it to DomainExpanding.

This is the formal core of @cite{mizuno-2024}'s argument: HP shifts the evaluation time backward, and backward time yields more historical alternatives, i.e., domain expansion.

theorem Semantics.Tense.ConditionalShift.historicalBase_monotone {W : Type u_1} {T : Type u_2} [Preorder T] (history : Core.Modality.HistoricalAlternatives.WorldHistory W T) (h_bc : history.backwardsClosed) (s₀ : Core.WorldTimeIndex W T) (t' : T) (h_earlier : t' ≤ s₀.time) (s₁ : Core.WorldTimeIndex W T) (h_s₁ : s₁ ∈ Core.Modality.HistoricalAlternatives.historicalBase history s₀) (h_time : s₁.time ≥ t') : s₁ ∈ Core.Modality.HistoricalAlternatives.historicalBase history { world := s₀.world, time := t' }

The historical base (set of situations) at an earlier time includes situations with the same worlds as the later base, plus potentially more. This is the situation-level version of domain expansion.

def Semantics.Tense.ConditionalShift.domainRestrictedConditional {W : Type u_1} (domain : Set W) (antecedent consequent : W → Prop) : Prop

Domain-restricted conditional: the standard Kratzer-style analysis of conditionals as restricted universal quantification over a modal domain.

∀ w ∈ D, antecedent(w) → consequent(w)

@cite{kratzer-1986}: if-clauses restrict the modal domain rather than functioning as binary connectives. This is the Prop-level counterpart of Semantics.Conditionals.Restrictor.conditionalNecessity (which operates over finite (World → Bool) for computation).

Both X-marking and O-marking strategies for Anderson conditionals work by expanding D to D⁺ ⊃ D, making this quantification non-trivial.

Equations

• Semantics.Tense.ConditionalShift.domainRestrictedConditional domain antecedent consequent = ∀ w ∈ domain, antecedent w → consequent w

def Semantics.Tense.ConditionalShift.trivialConsequent {W : Type u_1} (domain : Set W) (consequent : W → Prop) : Prop

A conditional is trivial when every world in the domain satisfies the consequent. The antecedent restriction does no work — the conditional is vacuously true regardless of what the antecedent says.

@cite{condoravdi-2002}: indicative conditionals with small domains can be trivial because every accessible world already satisfies the consequent. Domain expansion (via HP/X-marking) resolves this by adding worlds where the consequent may fail.

Equations

• Semantics.Tense.ConditionalShift.trivialConsequent domain consequent = ∀ w ∈ domain, consequent w

def Semantics.Tense.ConditionalShift.nonTrivialConsequent {W : Type u_1} (domain : Set W) (consequent : W → Prop) : Prop

A conditional is non-trivial when there exists a world in the domain where the consequent fails. This is the condition under which the antecedent restriction does meaningful work.

Equations

• Semantics.Tense.ConditionalShift.nonTrivialConsequent domain consequent = ∃ w ∈ domain, ¬consequent w

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

The triviality problem: when the consequent is trivial, the domain-restricted conditional is vacuously true regardless of the antecedent. This is why O-marked English Anderson conditionals are infelicitous — the consequent is an observed fact true at all worlds in D, so the conditional adds no information.

theorem Semantics.Tense.ConditionalShift.expansion_resolves_triviality {W : Type u_1} (smallDomain expandedDomain : Set W) (consequent : W → Prop) (_h_subset : smallDomain ⊆ expandedDomain) (_h_trivial : trivialConsequent smallDomain consequent) (w : W) (hw : w ∈ expandedDomain) (hw_fails : ¬consequent w) : nonTrivialConsequent expandedDomain consequent

Domain expansion resolves triviality: if the original domain makes the consequent trivial, but the expanded domain contains a world where the consequent fails, then the expanded conditional is non-trivial.

This completes the HP/X-marking argument:

1. hp_achieves_expansion — backward time shift expands the domain
2. expansion_resolves_triviality — expanded domain makes the conditional non-trivial

The counterfactual "If I had left earlier, I would have caught the train" is non-trivial precisely because the expanded domain (from X-marking's backward time shift) includes worlds where I didn't catch the train.

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

When the domain-restricted conditional holds over an expanded domain where the consequent is non-trivial, the antecedent must exclude at least one world. The antecedent restriction is doing genuine work — it is not vacuously satisfied.

This is the formal payoff of domain expansion: the conditional becomes informative because the antecedent partitions D⁺ into worlds where the consequent holds (via the conditional) and worlds where it fails (via non-triviality).

theorem Semantics.Tense.ConditionalShift.trivial_monotone {W : Type u_1} (smallDomain expandedDomain : Set W) (consequent : W → Prop) (h_subset : smallDomain ⊆ expandedDomain) (h_expanded_trivial : trivialConsequent expandedDomain consequent) : trivialConsequent smallDomain consequent

Triviality is monotone: if a superset domain is trivial, then so is any subset domain. Expanding the domain can only resolve triviality, never introduce it.

theorem Semantics.Tense.ConditionalShift.subj_subsumes_hp_expansion {W : Type u_1} {T : Type u_2} [Preorder T] (history : Core.Modality.HistoricalAlternatives.WorldHistory W T) (P : Core.WorldTimeIndex W T → Core.WorldTimeIndex W T → Prop) (s : Core.WorldTimeIndex W T) (h : Mood.SUBJ history P s) : ∃ (s₁ : Core.WorldTimeIndex W T), s₁.world ∈ history s ∧ P s₁ s

SUBJ's situation introduction can be decomposed into two steps:

1. Expand the domain (via backward time shift)
2. Existentially quantify over the expanded domain

When the history is backwards-closed, SUBJ at an earlier time introduces a situation whose world is in the expanded historical alternatives.