Documentation

Linglib.Theories.Semantics.Conditionals.Anderson

Anderson Conditionals: Crosslinguistic Marking Strategies #

@cite{mizuno-2024} @cite{anderson-1951}Formalizes the crosslinguistic typology of Anderson conditionals from @cite{iatridou-2000} @cite{mizuno-2024} "Strategies for Anderson Conditionals", Semantics and Pragmatics 17(8): 1–14.

Anderson Conditionals #

Anderson conditionals are counterfactuals where the speaker believes the antecedent is actually true:

"If Jones had taken arsenic, he would have shown exactly the symptoms he is actually showing."

The speaker believes Jones did take arsenic, and uses the conditional to argue from the observed symptoms to that conclusion. The challenge: how does the consequent describe the actual world when the conditional morphology shifts evaluation to counterfactual alternatives?

Two Marking Strategies #

Mizuno identifies two crosslinguistic strategies:

Connection to Existing Infrastructure #

FLV Correlation #

The availability of X-marking for Anderson conditionals correlates with its availability for Future Less Vivid conditionals:

source
inductive Semantics.Conditionals.Anderson.MarkingStrategy :
Type

The two crosslinguistic marking strategies for Anderson conditionals.

@cite{mizuno-2024}: languages differ in whether they use X-marking (counterfactual morphology) or O-marking (indicative/non-past) to express Anderson conditionals. English requires X-marking; Japanese requires O-marking.

  • xMarking : MarkingStrategy

    X-marking: CF morphology in antecedent + "actually" recovers actual world. English: "If Jones had taken arsenic, he would have shown exactly the symptoms he is actually showing."

  • oMarking : MarkingStrategy

    O-marking: Non-Past/Historical Present — no CF morphology, actual world directly accessible. Japanese: "Jones-ga... nom-eba,... mise-ru (hazuda)."

Instances For
    source
    instance Semantics.Conditionals.Anderson.instDecidableEqMarkingStrategy :
    DecidableEq MarkingStrategy
    Equations
    source
    instance Semantics.Conditionals.Anderson.instReprMarkingStrategy :
    Repr MarkingStrategy
    Equations
    source
    def Semantics.Conditionals.Anderson.instReprMarkingStrategy.repr :
    MarkingStrategy → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Semantics.Conditionals.Anderson.instBEqMarkingStrategy.beq :
      MarkingStrategy → MarkingStrategy → Bool
      Equations
      Instances For
        source
        instance Semantics.Conditionals.Anderson.instBEqMarkingStrategy :
        BEq MarkingStrategy
        Equations
        source
        def Semantics.Conditionals.Anderson.MarkingStrategy.hasXMarking :
        MarkingStrategy → Bool

        X-marking strategy uses counterfactual morphology; O-marking does not.

        This is the single primitive property of marking strategies. All other properties (ExclF production, "actually" requirement, FLV availability) are derived from it — they are abbrevs equal to hasXMarking, with docstrings explaining why the correlation holds.

        Both strategies access the actual world in the consequent — X-marking via Kaplanian "actually" (origin access through shifted tower), O-marking directly (no world shift). This is universal, not a distinguishing property.

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev Semantics.Conditionals.Anderson.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 (origin.world ≠ innermost.world). O-marking leaves the tower at the root, so no ExclF arises.

          Definitionally equal to hasXMarking — the correlation holds because ExclF is the mechanism of X-marking.

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev Semantics.Conditionals.Anderson.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) is needed to reach back through the shift. With O-marking, the evaluation world IS the actual world, so no recovery operator is needed.

            Definitionally equal to hasXMarking — the "actually" requirement is a direct consequence of ExclF.

            Equations
            Instances For
              source
              theorem Semantics.Conditionals.Anderson.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) :
              Iatridou.ExclF Iatridou.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 (origin.world ≠ innermost.world).

              This is why English Anderson conditionals use CF morphology: the X-marking shifts the evaluation world away from the actual world, setting up the need for "actually" to recover it.

              Wraps Iatridou.subjShift_produces_modal_exclF.

              source
              theorem Semantics.Conditionals.Anderson.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 X-marking shift.

              In an Anderson conditional with X-marking, 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. This is what makes Anderson conditionals felicitous despite the counterfactual morphology: "actually" reaches through the CF layer to access the actual world.

              Wraps Kaplan.opActually_shift_invariant.

              source
              theorem Semantics.Conditionals.Anderson.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) :
              ¬Iatridou.ExclF Iatridou.ExclDimension.modal (Core.Context.ContextTower.root c)

              O-marking has no modal ExclF: without CF morphology, the tower stays at the root, and origin.world = innermost.world.

              This is why Japanese Anderson conditionals use O-marking: no world shift means the actual world is directly accessible without "actually".

              Wraps Iatridou.root_no_modal_exclF.

              source
              @[reducible, inline]
              abbrev Semantics.Conditionals.Anderson.MarkingStrategy.flvXMarkingAvailable (s : MarkingStrategy) :
              Bool

              X-marking is available for FLV where it's available for Anderson.

              @cite{mizuno-2024}: "the availability of X-marking for Anderson conditionals and the availability of X-marking for Future Less Vivid conditionals seem to stand or fall together."

              English (X-marking for Anderson) → X-marking available for FLV. Japanese (O-marking for Anderson) → X-marking NOT available for FLV.

              Definitionally equal to hasXMarking — an empirical generalization over English, Japanese, and Mandarin, not a logical necessity.

              Equations
              Instances For