Documentation

Linglib.Phenomena.Modality.Studies.Kratzer2012Conditionals

§2.9 Conditionals — @cite{kratzer-2012} #

@cite{kratzer-2012} §2.9 ("Conditionals", pp. 65-68) presents the if-clause-as- modal-base-restrictor schema [[if α β]]^{f,g} = [[β]]^{f⁺, g} where f⁺(w) = f(w) ∪ {[[α]]^{f,g}}, plus a "Sketch of proof" showing the four conditional types (material, strict, counterfactual, deontic-ordering) fall out of varying f and g. The chapter's only concrete worked example in §2.9 is the German deontic scenario at p. 67 (examples 59-61).

Sections #

  1. The §2.9 four-conditional recipe (abstract over predicates): material and strict implication theorems. Counterfactual case defers to Ch. 3.
  2. Deontic scenario from p. 67: injustice / amended / rewarded propositions over a 4-world model, with morally-good ordering source.
  3. Predictions on the deontic scenario (Kratzer's analysis of (59)-(61)).
  4. Headline argument — Kratzer's analysis differentiates (60) from (61); the traditional □(α → β) analysis collapses them to vacuous truth.

Kratzer's text (p. 67, paraphrased) #

(59) Jedem Menschen muss Gerechtigkeit widerfahren. "Justice must be done to every person." (60) Wenn jemand ungerecht behandelt wurde, muss das Unrecht gesühnt werden. "If someone was treated unjustly, the injustice must be amended." (61) Wenn jemand ungerecht behandelt wurde, muss das Unrecht belohnt werden. "If someone was treated unjustly, the injustice must be rewarded."

"Traditional approaches ... would have to analyze (60) and (61) as modalized material implications and assign them the logical form necessarily (α→β). This leads to trouble. ... if there is no injustice in any morally accessible world, anything you like is true in morally accessible worlds where there is injustice." (p. 67)

"On this analysis [Kratzer's], it is possible for the first two propositions [(59) and (60)] to be true, and the third one [(61)] to be false. For us, a world where injustice is amended for is not good (since there is no injustice in a good world). But it is still closer to what is good than any world where injustice is rewarded." (p. 67)

§1. Four-conditional recipe (abstract) #

source
def Phenomena.Modality.Studies.Kratzer2012Conditionals.pointwiseRealisticBg (W : Type u_1) [DecidableEq W] :
Core.Logic.Intensional.ModalBase W

Pointwise-realistic modal base: f(w) = [(= w)], so ⋂f(w) = {w}.

NB: This is the trivial collapse where one proposition already IS the singleton {w}. @cite{kratzer-2012} distinguishes this from totally-realistic backgrounds proper (isTotallyRealistic in Core/Logic/Intensional/ConversationalBackground.lean), which carry many propositions — facts about w — whose intersection is {w}. The lumping/dividing of those propositions does theoretical work in counterfactuals (Ch. 3 §3.1). For the §2.9 recipe only ⋂f(w) = {w} matters, so the collapse is sound here — but it is NOT Kratzer's totally-realistic notion.

Equations
Instances For
    source
    theorem Phenomena.Modality.Studies.Kratzer2012Conditionals.material_implication_recipe {W : Type u_1} [DecidableEq W] (p q : W → Prop) [DecidablePred p] (w : W) :
    Semantics.Modality.Kratzer.necessity (Semantics.Modality.Kratzer.restrictedBase (pointwiseRealisticBg W) p) Core.Logic.Intensional.emptyBackground q w ↔ p w → q w

    Material implication recipe (Kratzer 2012 §2.9, p. 65-66 "Sketch of proof", Case one). With a pointwise-realistic modal base and empty ordering source, the conditional (if p) (necessarily q) reduces to material implication p w → q w at the evaluation world.

    source
    theorem Phenomena.Modality.Studies.Kratzer2012Conditionals.strict_implication_recipe {W : Type u_1} (p q : W → Prop) [DecidablePred p] (w : W) :
    Semantics.Modality.Kratzer.necessity (Semantics.Modality.Kratzer.restrictedBase Core.Logic.Intensional.emptyBackground p) Core.Logic.Intensional.emptyBackground q w ↔ ∀ (w' : W), p w' → q w'

    Strict implication recipe (Kratzer 2012 §2.9, p. 66 "Sketch of proof" for strict implication). With an empty modal base and empty ordering source, the conditional (if p) (necessarily q) reduces to logical implication: q must hold at every p-world.

    §2. Deontic scenario (Kratzer 2012 §2.9 p. 67, ex. 59-61) #

    Four worlds:

    WorldinjusticeamendedrewardedNotes
    w0non/an/a"Morally good" — no injustice exists
    w1yesyesnoInjustice amended for
    w2yesnoyesInjustice rewarded
    w3yesnonoInjustice neither amended nor rewarded
    source
    @[reducible, inline]
    abbrev Phenomena.Modality.Studies.Kratzer2012Conditionals.World :
    Type
    Equations
    Instances For
      source
      def Phenomena.Modality.Studies.Kratzer2012Conditionals.injustice :
      World → Prop

      "Someone was treated unjustly" — true at w1, w2, w3.

      Equations
      Instances For
        source
        @[implicit_reducible]
        instance Phenomena.Modality.Studies.Kratzer2012Conditionals.instDecidablePredWorldInjustice :
        DecidablePred injustice
        Equations
        source
        def Phenomena.Modality.Studies.Kratzer2012Conditionals.amended :
        World → Prop

        "The injustice was amended" — true at w1 only.

        Equations
        Instances For
          source
          @[implicit_reducible]
          instance Phenomena.Modality.Studies.Kratzer2012Conditionals.instDecidablePredWorldAmended :
          DecidablePred amended
          Equations
          source
          def Phenomena.Modality.Studies.Kratzer2012Conditionals.rewarded :
          World → Prop

          "The injustice was rewarded" — true at w2 only.

          Equations
          Instances For
            source
            @[implicit_reducible]
            instance Phenomena.Modality.Studies.Kratzer2012Conditionals.instDecidablePredWorldRewarded :
            DecidablePred rewarded
            Equations
            source
            def Phenomena.Modality.Studies.Kratzer2012Conditionals.morallyGood :
            Core.Logic.Intensional.OrderingSource World

            Morally-good ordering source. Two propositions track moral goodness: no-injustice (the ideal), and if-injustice-then-amended (the corrective ideal). Their joint pattern induces:

            • w0 satisfies both (no injustice; vacuously amends)
            • w1 satisfies only the corrective ideal (injustice + amended)
            • w2, w3 satisfy neither (injustice without amends)

            So w0 < w1 < {w2, w3} in the at-least-as-good ordering. Kratzer's "morally good" ordering source is left informal in §2.9; this is a minimal encoding sufficient for the (60)/(61) contrast.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Phenomena.Modality.Studies.Kratzer2012Conditionals.traditionalMoralBase :
              Core.Logic.Intensional.ModalBase World

              Traditional analysis modal base (the foil Kratzer is arguing against, p. 67). Treats "morally accessible worlds" as a single modal base — only the morally good world (w0) is accessible. Under this analysis, □(α → β) becomes vacuously true at the actual world whenever the antecedent is false in all accessible worlds.

              Equations
              Instances For

                §3. Predictions on the deontic scenario #

                source
                theorem Phenomena.Modality.Studies.Kratzer2012Conditionals.ex59_holds (w : World) :
                Semantics.Modality.Kratzer.necessity Core.Logic.Intensional.emptyBackground morallyGood (fun (w' : World) => ¬injustice w') w

                (59) "Justice must be done" under Kratzer's analysis. With empty modal base + morally-good ordering, the only best world is w0 (no injustice). So necessity of ¬ injustice holds.

                source
                theorem Phenomena.Modality.Studies.Kratzer2012Conditionals.ex60_holds (w : World) :
                Semantics.Modality.Kratzer.necessity (Semantics.Modality.Kratzer.restrictedBase Core.Logic.Intensional.emptyBackground injustice) morallyGood amended w

                (60) "If injustice, must be amended" under Kratzer's analysis succeeds. With empty modal base restricted by injustice + morally-good ordering, the only best world is w1 (amended is closer to the moral ideal than rewarded or unredressed). So necessity of amended holds.

                source
                theorem Phenomena.Modality.Studies.Kratzer2012Conditionals.ex61_fails (w : World) :
                ¬Semantics.Modality.Kratzer.necessity (Semantics.Modality.Kratzer.restrictedBase Core.Logic.Intensional.emptyBackground injustice) morallyGood rewarded w

                (61) "If injustice, must be rewarded" under Kratzer's analysis fails. The best injustice-world is w1, but w1 is NOT rewarded.

                §4. Headline: Kratzer differentiates (60) and (61); traditional analysis collapses them. #

                source
                theorem Phenomena.Modality.Studies.Kratzer2012Conditionals.kratzer_distinguishes_60_61 :
                (∀ (w : World), Semantics.Modality.Kratzer.necessity (Semantics.Modality.Kratzer.restrictedBase Core.Logic.Intensional.emptyBackground injustice) morallyGood amended w) ∧ ∀ (w : World), ¬Semantics.Modality.Kratzer.necessity (Semantics.Modality.Kratzer.restrictedBase Core.Logic.Intensional.emptyBackground injustice) morallyGood rewarded w

                Kratzer's analysis differentiates (60) and (61). Per @cite{kratzer-2012} p. 67: "On this analysis, it is possible for the first two propositions [(59) and (60)] to be true, and the third one [(61)] to be false."

                source
                theorem Phenomena.Modality.Studies.Kratzer2012Conditionals.traditional_60_vacuously_true :
                Semantics.Modality.Kratzer.necessity traditionalMoralBase Core.Logic.Intensional.emptyBackground (fun (w' : World) => injustice w' → amended w') 0

                Traditional □(α → β) analysis collapses (60) and (61) at the actual world (where actual = w0, the morally good world). When morally accessible worlds = {w0} and w0 has no injustice, both injustice → amended and injustice → rewarded are vacuously true at every accessible world. This is the "vacuous truth" problem Kratzer flags on p. 67.

                source
                theorem Phenomena.Modality.Studies.Kratzer2012Conditionals.traditional_61_vacuously_true :
                Semantics.Modality.Kratzer.necessity traditionalMoralBase Core.Logic.Intensional.emptyBackground (fun (w' : World) => injustice w' → rewarded w') 0
                source
                theorem Phenomena.Modality.Studies.Kratzer2012Conditionals.traditional_collapses_kratzer_distinguishes :
                (Semantics.Modality.Kratzer.necessity traditionalMoralBase Core.Logic.Intensional.emptyBackground (fun (w' : World) => injustice w' → amended w') 0 ∧ Semantics.Modality.Kratzer.necessity traditionalMoralBase Core.Logic.Intensional.emptyBackground (fun (w' : World) => injustice w' → rewarded w') 0) ∧ Semantics.Modality.Kratzer.necessity (Semantics.Modality.Kratzer.restrictedBase Core.Logic.Intensional.emptyBackground injustice) morallyGood amended 0 ∧ ¬Semantics.Modality.Kratzer.necessity (Semantics.Modality.Kratzer.restrictedBase Core.Logic.Intensional.emptyBackground injustice) morallyGood rewarded 0

                Headline contrast. The traditional analysis predicts (60) and (61) both vacuously true; Kratzer's analysis predicts (60) true and (61) false. So the traditional analysis cannot distinguish the two conditionals at the morally-good actual world, while Kratzer's analysis does.