[Miz24] — Strategies for Anderson Conditionals

Teruyuki Mizuno (2024), "Strategies for Anderson Conditionals: Their Implications for the Typology of O-Marking and X-Marking", Semantics and Pragmatics 17(8): 1–14. [And51] [Sch04b] [vFI23] [Iat00]

Anderson conditionals ([And51]) argue for the truth of their antecedent. English must X-mark them (O-marking is trivial); Japanese and Mandarin must O-mark them — their X-marking (Fake Past -ta: [Ogi14], [MK19]; perfective le) forces a counterfactual reading. Both strategies expand the modal domain D ⊂ D⁺; Mizuno adopts the expansion analysis (fn 6, [Mac15], [Mac19] contra [Iat00] / [Sch14] exclusion) and analyzes Japanese O-marking as a Historical-Present shift ([Sch04b], [AT18a], [AT18b]) expanding D backward under branching time.

Stimuli: Data/Examples/Mizuno2024.json (module Mizuno2024.Examples); #guards check observed directions on the named examples, row theorems quantify over Examples.all. Semantics: Semantics.Conditionals.strictImp over a HistoricalAlternatives base; Semantics.Modality.Exclusion supplies the X/O typology and exponent inventory.

Main results

• english_japanese_discrepancy — English X-marks, Japanese O-marks.
• inventory_prediction_fails_japanese — the §3.1 puzzle: Japanese has X-marking (ex. 3) yet must not deploy it; English validates the inventory prediction.
• anderson_judgments_match_strategy — every recorded judgment matches the strategy record.
• flv_anderson_correlation — Anderson X-marking ⇔ FLV X-marking, per row (§4.2).
• oMarking_anderson_trivial / xMarking_expands / consequent_open_over_xMarkedBase / expanded_anderson_informative — the triviality puzzle and its resolution.
• hp_expands_jones_domain / consequent_open_after_hp — the HP route to the same conclusions: §4.1 on [vFI23]'s uniformity hypothesis.

The per-language strategy record (§2–§4.2)

def Mizuno2024.andersonStrategy : Data.Examples.Glottocode → Option Semantics.Modality.Exclusion.MarkingStrategy

The felicitous Anderson marking per language: English X (§2, ex. 1a), Japanese O (§3, ex. 4a -ru), Mandarin O (§4.2, ex. 13a without le); none outside the sample.

Equations

• Mizuno2024.andersonStrategy "stan1293" = some Semantics.Modality.Exclusion.MarkingStrategy.xMarking
• Mizuno2024.andersonStrategy "nucl1643" = some Semantics.Modality.Exclusion.MarkingStrategy.oMarking
• Mizuno2024.andersonStrategy "mand1415" = some Semantics.Modality.Exclusion.MarkingStrategy.oMarking
• Mizuno2024.andersonStrategy x✝ = none

def Mizuno2024.flvXMarkingAvailable : Data.Examples.Glottocode → Option Bool

FLV X-marking availability (§4.2): English yes (ex. 8); Japanese -ta (ex. 10) and Mandarin le (ex. 12) induce strong counterfactuality instead.

Equations

• Mizuno2024.flvXMarkingAvailable "stan1293" = some true
• Mizuno2024.flvXMarkingAvailable "nucl1643" = some false
• Mizuno2024.flvXMarkingAvailable "mand1415" = some false
• Mizuno2024.flvXMarkingAvailable x✝ = none

theorem Mizuno2024.english_japanese_discrepancy : andersonStrategy "stan1293" ≠ andersonStrategy "nucl1643"

English and Japanese pick opposite Anderson strategies (§3).

The §3.1 puzzle: available X-marking that must not be deployed

Japanese has X-marking (Fake Past -ta, ex. 3; Japanese.Conditionals.xMarking), and §2 predicts it in Anderson conditionals — "strikingly, this is not borne out". Uniformity (§4.1) survives as a meaning/use split: uniform semantics, blocked deployment.

def Mizuno2024.xExponentOf : Data.Examples.Glottocode → Option Semantics.Modality.Exclusion.XMarkingExponent

X-marking exponents, routed from the Fragment inventory. Mandarin le is study-local: fn 15's single consultant is below the Fragment consensus bar.

Equations

• Mizuno2024.xExponentOf "stan1293" = English.Conditionals.xMarking
• Mizuno2024.xExponentOf "nucl1643" = Japanese.Conditionals.xMarking
• Mizuno2024.xExponentOf "mand1415" = some { form := "le", components := [Semantics.Modality.Exclusion.XMarkingHost.perfective] }
• Mizuno2024.xExponentOf x✝ = none

def Mizuno2024.inventoryPrediction (lang : Data.Examples.Glottocode) : Option Semantics.Modality.Exclusion.MarkingStrategy

The inventory-driven prediction: X-mark wherever the inventory provides X-marking (§2; a fortiori under fn 14's [Chi98]-style blocking).

Equations

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

theorem Mizuno2024.inventory_prediction_holds_english : inventoryPrediction "stan1293" = andersonStrategy "stan1293"

English validates the inventory prediction.

theorem Mizuno2024.inventory_prediction_fails_japanese : inventoryPrediction "nucl1643" ≠ andersonStrategy "nucl1643"

The §3.1 puzzle: Japanese has the X resource yet must not deploy it.

theorem Mizuno2024.inventory_prediction_fails_mandarin : inventoryPrediction "mand1415" ≠ andersonStrategy "mand1415"

Mandarin patterns with Japanese (§4.2).

The attested minimal pairs

Pairs live inside one numbered example: the felicitous primaryText (strategy m) plus the infelicitous alternatives entry (realizing m.other).

def Mizuno2024.isFelicitous : Features.Judgment → Bool

Felicitous iff fully acceptable.

Equations

• Mizuno2024.isFelicitous Features.Judgment.acceptable = true
• Mizuno2024.isFelicitous x✝ = false

def Mizuno2024.ofStrategyTag? : String → Option Semantics.Modality.Exclusion.MarkingStrategy

Parse the strategy tag.

Equations

• Mizuno2024.ofStrategyTag? "x-marking" = some Semantics.Modality.Exclusion.MarkingStrategy.xMarking
• Mizuno2024.ofStrategyTag? "o-marking" = some Semantics.Modality.Exclusion.MarkingStrategy.oMarking
• Mizuno2024.ofStrategyTag? x✝ = none

def Mizuno2024.andersonRowOK (e : Data.Examples.LinguisticExample) : Bool

One Anderson row against the record: primary judgment matches strategy m, each alternative matches m.other (§2: O-marking = absence of X-marking). Non-Anderson rows pass vacuously.

Equations

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

theorem Mizuno2024.anderson_judgments_match_strategy (e : Data.Examples.LinguisticExample) : e ∈ Examples.all → andersonRowOK e = true

Every recorded Anderson judgment matches the strategy record.

The Future-Less-Vivid correlation (§4.2)

def Mizuno2024.flvAvailableTag (e : Data.Examples.LinguisticExample) : Option Bool

The flv_xmarking tag.

Equations

• Mizuno2024.flvAvailableTag e = match e.feature? "flv_xmarking" with | some "available" => some true | some "unavailable" => some false | x => none

theorem Mizuno2024.flv_anderson_correlation (e : Data.Examples.LinguisticExample) : e ∈ Examples.all → Option.map Semantics.Modality.Exclusion.MarkingStrategy.hasXMarking (andersonStrategy e.language) = flvXMarkingAvailable e.language

§4.2: Anderson X-marking and FLV X-marking stand or fall together, for every sampled language. An empirical correlation of two independent records, not a definition; cf. Iatridou2000.CounterfactualType.flv (one ExclF layer).

The triviality puzzle and its resolution by domain expansion

§2: an Anderson consequent is an observed fact, true throughout the live domain D, so over D the conditional is trivial; both strategies expand D to a D⁺ containing a consequent-failing world. The Jones scenario as strictImp over a historical base: worlds are Bool (true = symptoms shown), the domain at an index is its live alternatives. D = the domain at utteranceIdx; D⁺ via X-marking (larger base, same index: xMarkedBase) or via HP (same base, earlier index: hpIdx) — same operator, same two conclusions on each route: §4.1's uniformity of meaning under varying use.

def Mizuno2024.showsSymptoms : Set Bool

The Anderson consequent: Jones shows the symptoms.

Equations

• Mizuno2024.showsSymptoms = {w : Bool | w = true}

def Mizuno2024.historyJones : HistoricalAlternatives Bool ℤ

A backward-closed history: live iff the index's own world, or its time is ≤ 0.

Equations

• Mizuno2024.historyJones s = {w : Bool | w = s.world ∨ s.time ≤ 0}

@[simp]

theorem Mizuno2024.mem_historyJones {w : Bool} {s : Intensional.WorldTimeIndex Bool ℤ} : w ∈ historyJones s ↔ w = s.world ∨ s.time ≤ 0

theorem Mizuno2024.historyJones_backwardsClosed : historyJones.backwardsClosed

def Mizuno2024.utteranceIdx : Intensional.WorldTimeIndex Bool ℤ

The utterance index; its domain is the paper's D.

Equations

• Mizuno2024.utteranceIdx = { world := true, time := 1 }

def Mizuno2024.hpIdx : Intensional.WorldTimeIndex Bool ℤ

The HP-shifted index (§3.3); its domain is D⁺ on the O-marking route.

Equations

• Mizuno2024.hpIdx = { world := true, time := 0 }

def Mizuno2024.xMarkedBase : HistoricalAlternatives Bool ℤ

The X-marked base: every world live at every index (§2, fn 6) — D⁺ on the X-marking route.

Equations

• Mizuno2024.xMarkedBase x✝ = Set.univ

theorem Mizuno2024.consequent_trivial_at_utterance : historyJones utteranceIdx ⊆ showsSymptoms

Over D the consequent is trivial: only the symptom world is live (§2).

theorem Mizuno2024.false_not_live : false ∉ historyJones utteranceIdx

The symptom-absent world is not live at the utterance index.

theorem Mizuno2024.oMarking_anderson_trivial (antecedent : Set Bool) : utteranceIdx ∈ Semantics.Conditionals.strictImp historyJones antecedent showsSymptoms

O-marking without expansion: trivially true for any antecedent — the infelicity of ex. (2).

theorem Mizuno2024.xMarking_expands : historyJones utteranceIdx ⊂ xMarkedBase utteranceIdx

X-marking's expansion is strict — the paper's D ⊂ D⁺ (§2).

theorem Mizuno2024.consequent_open_over_xMarkedBase : ¬xMarkedBase utteranceIdx ⊆ showsSymptoms

Over the X-marked D⁺ the consequent is left open (§2).

Japanese O-marking: HP expansion under branching time

§3.3: the HP shift moves the evaluation index backward; live possibilities shrink monotonically over time (the substrate's backwardsClosed, anchored on [Con02]), so the earlier index has a larger domain.

theorem Mizuno2024.hp_expands_jones_domain : historyJones utteranceIdx ⊂ historyJones hpIdx

The HP shift strictly enlarges the live domain (§3.3): subset by histEquiv_mono, strictness by the newly live symptom-absent world.

theorem Mizuno2024.consequent_open_after_hp : ¬historyJones hpIdx ⊆ showsSymptoms

Over the HP-shifted domain the consequent is left open — the conclusion consequent_open_over_xMarkedBase reaches by enlarging the base (§3.3, §4.1).

theorem Mizuno2024.expanded_anderson_informative (antecedent : Set Bool) (h : hpIdx ∈ Semantics.Conditionals.strictImp historyJones antecedent showsSymptoms) : ¬historyJones hpIdx ⊆ antecedent

The payoff (§2: "one can make a meaningful, contingent claim"): a true Anderson conditional at the HP index excludes a live world (Set.not_subset for the witness form).

Fragment marker connection