Anderson Conditionals and Domain Expansion

@cite{condoravdi-2002}

Formalizes the connection between backward temporal shifts and domain expansion in conditionals, following Mizuno's argument: the historical present (HP) in conditional antecedents achieves domain expansion because moving time backward expands the set of historical alternatives.

Key Results

• andersonConditional — HP in antecedent pushes a temporal shift + domain expands
• hp_achieves_expansion — Mizuno's argument: backward time + domain monotonicity yields expansion
• Bridge to BranchingTime.historicalBase and Mood.SUBJ

Connection to ContextTower

The HP shift in the antecedent of an Anderson conditional is modeled as a tower push of an hpShift: a context shift that moves time backward and expands the domain. This connects the modal-temporal interaction in conditionals to the tower architecture.

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: the antecedent is evaluated at an HP-shifted context (backward time, expanded domain), and the consequent is evaluated at the original context.

The HP shift in the antecedent is what gives counterfactual conditionals their widened modal base — by shifting time backward, more futures branch, and the domain of quantification expands.

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 : BranchingTime.WorldHistory W T) (h_bc : history.backwardsClosed) (s₀ : Situation W T) (t' : T) (h_earlier : t' ≤ s₀.time) (w : W) (hw : w ∈ history s₀) : w ∈ history { world := s₀.world, time := t' }

Mizuno'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 domain monotonicity.

theorem Semantics.Tense.ConditionalShift.historicalBase_monotone {W : Type u_1} {T : Type u_2} [Preorder T] (history : BranchingTime.WorldHistory W T) (h_bc : history.backwardsClosed) (s₀ : Situation W T) (t' : T) (h_earlier : t' ≤ s₀.time) (s₁ : Situation W T) (h_s₁ : s₁ ∈ BranchingTime.historicalBase history s₀) (h_time : s₁.time ≥ t') : s₁ ∈ BranchingTime.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.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.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.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

Contrapositive: if a conditional over a domain is trivial and a superset is also trivial, then every world in the superset satisfies the consequent. This shows that triviality is monotone: 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 : BranchingTime.WorldHistory W T) (P : Situation W T → Situation W T → Prop) (s : Situation W T) (h : Mood.SUBJ history P s) : ∃ (s₁ : Situation 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.