Kratzer (1981): The Notional Category of Modality

This file formalizes the paper's practical-inference example, on the modal base and ordering source semantics of Modality.Necessity. Someone wants two things, to become mayor and to avoid the pub, while the circumstances are such that they become mayor only if they go to the pub. The circumstances supply the modal base and the desires the ordering source, and the two ideals pull apart, since a world where the speaker goes to the pub and becomes mayor and one where they stay home and do not are incomparable, so the ordering is not connected. Of the five conclusions the paper considers, the three necessities and impossibilities (that the speaker should go to the pub, should avoid it, and could become mayor without it) fail, while the two possibilities (that they could go and could avoid going) hold, under the paper's limit-free necessity and its dual possibility.

The paper's section on conditionals treats an if-clause as restricting the modal base of the modal in its matrix clause, the substrate's Conditional.Restrictor.conditionalNecessity, and derives the kinds of conditional from the settings of the two backgrounds, material implication from a totally realistic base and an empty ordering source (material_implication), strict implication from an empty base and an empty ordering source (strict_implication), counterfactuals from an empty base and a totally realistic ordering source, the subject of the paper's companion on partition and revision, and deontic conditionals from an empty base and an ordering source of what is morally good. The deontic example is the argument against analyzing conditionals as modalized material implications. Given that justice must be done, that analysis makes if someone was treated unjustly, the injustice must be amended for and ... must be rewarded both vacuously true (traditional_collapses), while restricting an empty base by the antecedent and ordering by what is morally good makes the first true and the second false (injustice_must_be_amended, not_injustice_must_be_rewarded), a world where injustice is amended for being closer to the good than one where it is rewarded, the truth conditions of [Lew73b].

Implementation notes

The worlds are the four combinations of becoming mayor and going to the pub, so every claim is decided once the modal base, the ordering source, and the operators are unfolded. The example also fixes the reading of bestWorlds: the world that is at least as good as every accessible world does not exist here, so the minimality reading, on which the best worlds are the two ideal-realizing ones, is the one that agrees with the limit-free operators.

The deontic example's worlds are the situations with no injustice and those where an injustice was amended for, rewarded, or neither; the ordering source of what is morally good is left informal in the paper and is rendered by two ideals, that there is no injustice and that any injustice is amended for. The section on conditionals is read from the revised version of the paper in [Kra12b].

References

• [Kra81b]
• [Kra12b] — Chapter 2, the revised version of the paper
• [Lew73b]

@[reducible, inline]

abbrev Kratzer1981.World : Type

A world records whether the speaker becomes mayor and whether they go to the pub regularly.

Equations

• Kratzer1981.World = (Bool × Bool)

def Kratzer1981.w₀ : World

The evaluation world, arbitrary since the backgrounds are constant.

Equations

• Kratzer1981.w₀ = (false, false)

def Kratzer1981.circumstances : Modality.Background World

The relevant circumstances are that the speaker becomes mayor only by going to the pub.

Equations

• Kratzer1981.circumstances = Function.const Kratzer1981.World {fun (w : Kratzer1981.World) => w.1 = true → w.2 = true}

def Kratzer1981.desires : Modality.Background World

The speaker wants to become mayor and to avoid the pub.

Equations

• Kratzer1981.desires = Function.const Kratzer1981.World {fun (w : Kratzer1981.World) => w.1 = true, fun (w : Kratzer1981.World) => w.2 = false}

def Kratzer1981.tacticDecide_worlds : Lean.ParserDescr

Decide a claim about the backgrounds and the ordering over the four worlds.

Equations

• Kratzer1981.tacticDecide_worlds = Lean.ParserDescr.node `Kratzer1981.tacticDecide_worlds 1024 (Lean.ParserDescr.nonReservedSymbol "decide_worlds" false)

theorem Kratzer1981.mayor_pub_incomparable : ¬(true, true) ≤ (false, false) ∧ ¬(false, false) ≤ (true, true)

By the paper's clause (c), the world of going to the pub and becoming mayor and the world of staying home are incomparable, so the ordering is not connected.

theorem Kratzer1981.pub_no_mayor_worst (v : World) : v ∈ {(true, true), (false, false)} → v ≤ (false, true) ∧ ¬(false, true) ≤ v

By clause (f), the accessible world where the speaker goes to the pub and still fails to become mayor is strictly worse than either ideal-realizing world.

theorem Kratzer1981.no_dominant_world : ¬∃ w ∈ circumstances.accessibleWorlds w₀, ∀ v ∈ circumstances.accessibleWorlds w₀, w ≤ v

No accessible world is at least as good as every accessible world, so on the dominance reading of "best" the example would have no best world at all.

theorem Kratzer1981.mem_bestWorlds_iff (w : World) : w ∈ Modality.bestWorlds circumstances desires w₀ ↔ w = (true, true) ∨ w = (false, false)

The best worlds are the two ideal-realizing ones.

theorem Kratzer1981.limitAssumption : Modality.LimitAssumption circumstances desires w₀

The example satisfies the Limit Assumption, so the paper's limit-free operators are quantification over bestWorlds.

def Kratzer1981.tacticDecide_verdict : Lean.ParserDescr

Decide a verdict of the limit-free operators through the best worlds.

Equations

• Kratzer1981.tacticDecide_verdict = Lean.ParserDescr.node `Kratzer1981.tacticDecide_verdict 1024 (Lean.ParserDescr.nonReservedSymbol "decide_verdict" false)

theorem Kratzer1981.not_must_pub : ¬Modality.humanNecessity circumstances desires (fun (x : World) => x.2 = true) w₀

Conclusion one fails, as the speaker need not go to the pub.

theorem Kratzer1981.not_must_avoid : ¬Modality.humanNecessity circumstances desires (fun (x : World) => x.2 = false) w₀

Conclusion two fails, as the speaker need not avoid the pub.

theorem Kratzer1981.not_can_mayor_without_pub : ¬Modality.humanPossibility circumstances desires (fun (w : World) => w.1 = true ∧ w.2 = false) w₀

Conclusion three fails, since becoming mayor without the pub is not even accessible and wishes cannot override facts.

theorem Kratzer1981.can_pub : Modality.humanPossibility circumstances desires (fun (x : World) => x.2 = true) w₀

Conclusion four holds, as the speaker could go to the pub.

theorem Kratzer1981.can_avoid : Modality.humanPossibility circumstances desires (fun (x : World) => x.2 = false) w₀

Conclusion five holds, as the speaker could avoid the pub.

Conditionals

An if-clause restricts the modal base of the modal in its matrix clause, so (if α) (necessarily β) is the necessity of β at the base enlarged by α. The kinds of conditional differ in the settings of the two backgrounds.

theorem Kratzer1981.material_implication {W : Type u_1} {f : Modality.Background W} (hf : f.IsTotallyRealistic) (α β : W → Prop) (w : W) : Conditional.Restrictor.conditionalNecessity f ⊥ α β w ↔ α w → β w

A totally realistic modal base and an empty ordering source give material implication.

theorem Kratzer1981.strict_implication {W : Type u_1} (α β : W → Prop) (w : W) : Conditional.Restrictor.conditionalNecessity ⊥ ⊥ α β w ↔ ∀ (v : W), α v → β v

An empty modal base and an empty ordering source give strict implication, the conditional holding iff the antecedent logically implies the consequent.

theorem Kratzer1981.traditional_vacuous {W : Type u_1} (f : Modality.Background W) (α β : W → Prop) (w : W) (h : Modality.simpleNecessity f (fun (v : W) => ¬α v) w) : Modality.simpleNecessity f (fun (v : W) => α v → β v) w

Under an analysis of conditionals as modalized material implications, a necessity that the antecedent fail makes every conditional with that antecedent vacuously true.

The deontic example

inductive Kratzer1981.Redress : Type

An injustice was amended for, rewarded, or neither.

• amended : Redress
• rewarded : Redress
• neither : Redress

@[instance_reducible]

instance Kratzer1981.instDecidableEqRedress : DecidableEq Redress

Equations

• Kratzer1981.instDecidableEqRedress x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Kratzer1981.instReprRedress : Repr Redress

Equations

• Kratzer1981.instReprRedress = { reprPrec := Kratzer1981.instReprRedress.repr }

def Kratzer1981.instReprRedress.repr : Redress → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Kratzer1981.instFintypeRedress : Fintype Redress

Equations

• Kratzer1981.instFintypeRedress = { elems := { val := ↑Kratzer1981.Redress.enumList, nodup := Kratzer1981.Redress.enumList_nodup }, complete := Kratzer1981.instFintypeRedress._proof_1 }

@[reducible, inline]

abbrev Kratzer1981.Situation : Type

A situation has no injustice, or an injustice and what became of it.

Equations

• Kratzer1981.Situation = Option Kratzer1981.Redress

def Kratzer1981.injustice (s : Situation) : Prop

Someone was treated unjustly.

Equations

• Kratzer1981.injustice s = (Option.isSome s = true)

def Kratzer1981.amended (s : Situation) : Prop

The injustice was amended for.

Equations

• Kratzer1981.amended s = (s = some Kratzer1981.Redress.amended)

def Kratzer1981.rewarded (s : Situation) : Prop

The injustice was rewarded.

Equations

• Kratzer1981.rewarded s = (s = some Kratzer1981.Redress.rewarded)

@[instance_reducible]

instance Kratzer1981.instDecidablePredSituationInjustice : DecidablePred injustice

Equations

• Kratzer1981.instDecidablePredSituationInjustice s = Kratzer1981.instDecidablePredSituationInjustice._aux_1 s

@[instance_reducible]

instance Kratzer1981.instDecidablePredSituationAmended : DecidablePred amended

Equations

• Kratzer1981.instDecidablePredSituationAmended s = Kratzer1981.instDecidablePredSituationAmended._aux_1 s

@[instance_reducible]

instance Kratzer1981.instDecidablePredSituationRewarded : DecidablePred rewarded

Equations

• Kratzer1981.instDecidablePredSituationRewarded s = Kratzer1981.instDecidablePredSituationRewarded._aux_1 s

def Kratzer1981.morallyGood : Modality.Background Situation

What is morally good is that there be no injustice and that any injustice be amended for. A situation with amended injustice is not good, but it is closer to the good than one where the injustice is rewarded or unredressed.

Equations

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

def Kratzer1981.morallyAccessible : Modality.Background Situation

The morally accessible situations of the traditional analysis are those without injustice.

Equations

• Kratzer1981.morallyAccessible = Function.const Kratzer1981.Situation {fun (s : Kratzer1981.Situation) => ¬Kratzer1981.injustice s}

def Kratzer1981.tacticDecide_situations : Lean.ParserDescr

Decide a claim about the backgrounds and the ordering over the four situations.

Equations

• Kratzer1981.tacticDecide_situations = Lean.ParserDescr.node `Kratzer1981.tacticDecide_situations 1024 (Lean.ParserDescr.nonReservedSymbol "decide_situations" false)

theorem Kratzer1981.mem_bestWorlds_good_iff (s : Situation) : s ∈ Modality.bestWorlds ⊥ morallyGood none ↔ s = none

With an empty base, the situation closest to the good is the one without injustice.

theorem Kratzer1981.mem_bestWorlds_injustice_iff (s : Situation) : s ∈ Modality.bestWorlds (⊥.restrict injustice) morallyGood none ↔ s = some Redress.amended

Among the situations with injustice, the one closest to the good is the one where it is amended for.

theorem Kratzer1981.limitAssumption_injustice : Modality.LimitAssumption (⊥.restrict injustice) morallyGood none

The restricted base satisfies the Limit Assumption, so the verdicts below are those of the paper's human necessity as well.

theorem Kratzer1981.justice_must_be_done : Modality.necessity ⊥ morallyGood (fun (s : Situation) => ¬injustice s) none

Justice must be done (59), there being no injustice in the situations closest to the good.

theorem Kratzer1981.injustice_must_be_amended : Conditional.Restrictor.conditionalNecessity ⊥ morallyGood injustice amended none

If someone was treated unjustly, the injustice must be amended for (60).

theorem Kratzer1981.not_injustice_must_be_rewarded : ¬Conditional.Restrictor.conditionalNecessity ⊥ morallyGood injustice rewarded none

(61) is false, since the injustice need not be rewarded.

theorem Kratzer1981.traditional_collapses : Modality.simpleNecessity morallyAccessible (fun (s : Situation) => ¬injustice s) none ∧ Modality.simpleNecessity morallyAccessible (fun (s : Situation) => injustice s → amended s) none ∧ Modality.simpleNecessity morallyAccessible (fun (s : Situation) => injustice s → rewarded s) none

Under the traditional analysis over the morally accessible situations (59) holds, and then (60) and (61) are both vacuously true, since no accessible situation has injustice.