Kratzer 1981: The Notional Category of Modality

[Kra81]'s practical-inference example (her §7): I want to become mayor; I will become mayor only if I go to the pub regularly. The circumstances contribute the modal base, the desires the ordering source, and the ordering source's two ideals — becoming mayor, not going to the pub — pull in opposite directions, so the induced ordering is non-connected by construction: her clause (c), "If v ∈ A and z ∈ B, then neither v ≤ z nor z ≤ v."

Her verdicts: conclusions one ("must go to the pub"), two ("must not go"), and three ("possible to become mayor without going") are faulty; four ("possible to go") and five ("possible not to go") are correct. The example also fixes the form of bestWorlds: under the dominance reading (at least as good as every accessible world) the best set here is empty and all five conclusions would come out trivially, so her verdicts require the minimality reading (dominance_best_empty, best_nonempty).

@[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; the backgrounds are constant).

Equations

• Kratzer1981.w₀ = (false, false)

def Kratzer1981.circumstances : Semantics.Modality.Kratzer.ModalBase World

Circumstances: I will become mayor only if I go to the pub regularly.

Equations

• Kratzer1981.circumstances x✝ = [fun (w : Kratzer1981.World) => w.1 = true → w.2 = true]

def Kratzer1981.desires : Semantics.Modality.Kratzer.OrderingSource World

Desires: to become mayor, and not to go to the pub.

Equations

• Kratzer1981.desires x✝ = [fun (w : Kratzer1981.World) => w.1 = true, fun (w : Kratzer1981.World) => w.2 = false]

theorem Kratzer1981.mayor_pub_incomparable : (¬(true, true) ≤[desires w₀] (false, false)) ∧ ¬(false, false) ≤[desires w₀] (true, true)

Her clause (c): the mayor-ideal world and the no-pub-ideal world are incomparable — the ordering is non-connected by construction.

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

The best worlds are exactly the two ideal-realizing ones: become mayor and go, or stay home and skip the pub.

theorem Kratzer1981.conclusion_one_faulty : ¬Semantics.Modality.Kratzer.necessity circumstances desires (fun (w : World) => w.2 = true) w₀

Conclusion one is faulty: it is not necessary to go to the pub.

theorem Kratzer1981.conclusion_two_faulty : ¬Semantics.Modality.Kratzer.necessity circumstances desires (fun (w : World) => w.2 = false) w₀

Conclusion two is faulty: it is not necessary to skip the pub.

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

Conclusion three is faulty: becoming mayor without the pub is not even accessible.

theorem Kratzer1981.conclusion_four_correct : Semantics.Modality.Kratzer.possibility circumstances desires (fun (w : World) => w.2 = true) w₀

Conclusion four is correct: going to the pub is possible.

theorem Kratzer1981.conclusion_five_correct : Semantics.Modality.Kratzer.possibility circumstances desires (fun (w : World) => w.2 = false) w₀

Conclusion five is correct: skipping the pub is possible.

The example fixes the form of bestWorlds

theorem Kratzer1981.dominance_best_empty : {w : World | w ∈ Semantics.Modality.Kratzer.accessibleWorlds circumstances w₀ ∧ ∀ v ∈ Semantics.Modality.Kratzer.accessibleWorlds circumstances w₀, w ≤[desires w₀] v} = ∅

Under the dominance reading of "best" — at least as good as every accessible world — the best set of her example is empty: the two ideal-realizing worlds disqualify each other.

theorem Kratzer1981.best_nonempty : (Semantics.Modality.Kratzer.bestWorlds circumstances desires w₀).Nonempty

The minimality reading leaves the best set nonempty, as her verdicts require.