Mizuno (2024): Strategies for Anderson Conditionals

This file formalizes the account in [Miz24] of Anderson conditionals, conditionals whose consequent is an observed fact and which therefore argue for their antecedent ([And51]). English must X-mark them, since over the live domain the consequent is trivially true and O-marking says nothing, while Japanese and Mandarin must O-mark them: their X-marking, the fake past -ta and the perfective le, forces a counterfactual reading. The typological record and its attested minimal pairs are transferred from the paper's examples (andersonStrategy, anderson_judgments_match_strategy), and the correlation with future-less-vivid conditionals holds row by row (flv_anderson_correlation). Both strategies enlarge the modal domain to one containing a consequent-failing world, after the expansion analysis of [Mac15] and [Mac19]: X-marking by enlarging the base (xMarking_expands), Japanese O-marking by a historical-present shift of the evaluation index backward under branching time ([Sch04b]; hp_expands_jones_domain), and on either route the consequent is left open and a true Anderson conditional excludes a live world (expanded_anderson_informative).

Implementation notes

The Jones scenario is a strict conditional over a historical base whose worlds record whether the symptoms are shown; the marking typology and exponent inventory are those of Semantics/Modality/Exclusion, and the Mandarin exponent le is study-local, resting on the paper's single consultant.

References

• [Miz24]
• [And51]
• [Sch04b]
• [vFI23]
• [Iat00]
• [Mac15]
• [Mac19]
• [Con02]

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

def Mizuno2024.andersonStrategy : Glottocode → Option Modality.Exclusion.MarkingStrategy

The felicitous Anderson marking of each language is X for English (§2, ex. 1a), O for Japanese (§3, ex. 4a -ru) and O for Mandarin (§4.2, ex. 13a without le), and none outside the sample.

Equations

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

def Mizuno2024.flvXMarkingAvailable : 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 : Glottocode → Option 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 := [Modality.Exclusion.XMarkingHost.perfective] }
• Mizuno2024.xExponentOf x✝ = none

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

The inventory-driven prediction X-marks wherever the inventory provides X-marking (§2; a fortiori under the blocking of fn 14, after [Chi98]).

Equations

• Mizuno2024.inventoryPrediction lang = Option.map (fun (x : Modality.Exclusion.XMarkingExponent) => Modality.Exclusion.MarkingStrategy.xMarking) (Mizuno2024.xExponentOf lang)

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 (j : Judgment) : Prop

Felicitous when fully acceptable.

Equations

• Mizuno2024.IsFelicitous j = (j = Judgment.acceptable)

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

Parse the strategy tag.

Equations

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

def Mizuno2024.AndersonRowOK (e : Datum) : Prop

An Anderson row matches the record when its primary judgment matches strategy m and each alternative matches the other strategy, O-marking being the absence of X-marking.

Equations

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

@[instance_reducible]

instance Mizuno2024.instDecidablePredDatumAndersonRowOK : DecidablePred AndersonRowOK

Equations

• Mizuno2024.instDecidablePredDatumAndersonRowOK = id (id inferInstance)

theorem Mizuno2024.anderson_judgments_match_strategy (e : Datum) : e ∈ Examples.all → AndersonRowOK e

Every recorded Anderson judgment matches the strategy record.

The Future-Less-Vivid correlation (§4.2)

def Mizuno2024.flvAvailableTag (e : Datum) : 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 : Datum) : e ∈ Examples.all → Option.map 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, that Jones shows the symptoms.

Equations

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

def Mizuno2024.historyJones : HistoricalAlternatives Bool ℤ

A backward-closed history, on which a world is live at an index iff it is the index's own world or the index's time is at most 0.

Equations

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

@[simp]

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

theorem Mizuno2024.historyJones_antitone (w : Bool) : Antitone (historyJones.metaphysicalBase w)

def Mizuno2024.utteranceIdx : Reference.Index Bool ℤ

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

Equations

• Mizuno2024.utteranceIdx = (true, 1)

def Mizuno2024.hpIdx : Reference.Index Bool ℤ

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

Equations

• Mizuno2024.hpIdx = (true, 0)

def Mizuno2024.xMarkedBase : HistoricalAlternatives Bool ℤ

The X-marked base makes every world live at every index (§2, fn 6), the D⁺ of 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, since 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 ∈ Conditional.strictImp historyJones antecedent showsSymptoms

O-marking without expansion is 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 (historyJones_antitone, the backward closure of [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 antitonicity, 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 ∈ Conditional.strictImp historyJones antecedent showsSymptoms) : ¬historyJones hpIdx ⊆ antecedent

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

Fragment marker connection