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.Kratzer.Operators. 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: 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.

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.

References

• [kratzer-1981]
• [kratzer-2012] — Chapter 2, the revised version of the paper

@[reducible, inline]

abbrev Kratzer1981.World : Type

A world: does the speaker become mayor, and 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.Kratzer.ModalBase World

The relevant circumstances: 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.Kratzer.OrderingSource World

What 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) ≤[desires w₀] (false, false)) ∧ ¬(false, false) ≤[desires w₀] (true, true)

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 ≤[desires w₀] (false, true)) ∧ ¬(false, true) ≤[desires w₀] v

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 ∈ Modality.Kratzer.accessibleWorlds circumstances w₀, ∀ v ∈ Modality.Kratzer.accessibleWorlds circumstances w₀, w ≤[desires w₀] v

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

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

The best worlds are the two ideal-realizing ones.

theorem Kratzer1981.limitAssumption : Modality.Kratzer.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.Kratzer.humanNecessity circumstances desires (fun (x : World) => x.2 = true) w₀

Conclusion one fails: the speaker need not go to the pub.

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

Conclusion two fails: the speaker need not avoid the pub.

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

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

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

Conclusion four holds: the speaker could go to the pub.

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

Conclusion five holds: the speaker could avoid the pub.