Kratzer (1977): What 'must' and 'can' must and can mean

Kratzer reads must and can in view of a premise set as consequence and compatibility (Definitions 5 and 6, the substrate's simpleNecessity and simplePossibility), and revises them for inconsistent premise sets by quantifying over the consistent subsets (Definitions 7 and 8, MustInView and CanInView). In a New Zealand whose whole common law is three judgments, that murder is a crime and that deer are, and are not, personally responsible for the damage they inflict on young trees, the revised definitions recover the verdicts the paper argues for: murder must be a crime, while deer can be responsible and can fail to be. The recommendations of the former principals of a Whare Wananga show that the verdicts depend on how premises are individuated.

Main statements

• must_p, can_q, can_neg_q: the revised verdicts on the New Zealand judgments.
• not_must_q, must_q: flying is required only when Te Miti's recommendation is two premises.
• canInView_iff_not_mustInView_not: the revised modals are dual.

Implementation notes

• Each example's worlds are the four combinations of the two issues it turns on, and its premise set is the same at every world.
• Every premise but one looks at a single issue, so a world of a consistent subset can be moved along the other issue without leaving it; the verdicts are proved that way rather than by enumerating subsets.
• The paper's sentence numbers are those of the original article; the 2012 revision renumbers them.

References

• [Kra77]
• [Kra12b] — Chapter 1, the revised version of the paper

Definitions 7 and 8: must and can over consistent subsets

def Kratzer1977.consistentSubsets {W : Type u_1} (A : Set (W → Prop)) : Set (Set (W → Prop))

The consistent subsets of a premise set, X_A = {B ⊆ A : ⋂B ≠ ∅}, over which the revised definitions quantify.

Equations

• Kratzer1977.consistentSubsets A = {B : Set (W → Prop) | B ⊆ A ∧ sInf B ≠ ⊥}

def Kratzer1977.MustInView {W : Type u_1} (f : Modality.Background W) (φ : W → Prop) (i : W) : Prop

Definition 7: must φ in view of f holds at i when every consistent subset of f i extends to a consistent subset from which φ follows, ν(φ, f) = {i : ∀B[B ∈ X_{f(i)} → ∃C[C ∈ X_{f(i)} ∧ B ⊆ C ∧ ⋂C ⊆ φ]]}.

Equations

• Kratzer1977.MustInView f φ i = ∀ B ∈ Kratzer1977.consistentSubsets (f i), ∃ C ∈ Kratzer1977.consistentSubsets (f i), B ⊆ C ∧ sInf C ≤ φ

def Kratzer1977.CanInView {W : Type u_1} (f : Modality.Background W) (φ : W → Prop) (i : W) : Prop

Definition 8: can φ in view of f holds at i when some consistent subset of f i has φ compatible with each of its consistent extensions, μ(φ, f) = {i : ∃B[B ∈ X_{f(i)} ∧ ∀C[(C ∈ X_{f(i)} ∧ B ⊆ C) → consistent(C ∪ {φ})]]}.

Equations

• Kratzer1977.CanInView f φ i = ∃ B ∈ Kratzer1977.consistentSubsets (f i), ∀ C ∈ Kratzer1977.consistentSubsets (f i), B ⊆ C → ¬Disjoint (sInf C) φ

theorem Kratzer1977.mustInView_iff_of_consistent {W : Type u_1} {f : Modality.Background W} {φ : W → Prop} {i : W} (h : sInf (f i) ≠ ⊥) : MustInView f φ i ↔ Modality.simpleNecessity f φ i

On a consistent premise set the revised necessity is Definition 5: the premise set is itself the consistent subset that dominates every other.

theorem Kratzer1977.canInView_iff_of_consistent {W : Type u_1} {f : Modality.Background W} {φ : W → Prop} {i : W} (h : sInf (f i) ≠ ⊥) : CanInView f φ i ↔ Modality.simplePossibility f φ i

On a consistent premise set the revised possibility is Definition 6.

theorem Kratzer1977.canInView_iff_not_mustInView_not {W : Type u_1} (f : Modality.Background W) (φ : W → Prop) (i : W) : CanInView f φ i ↔ ¬MustInView f (fun (j : W) => ¬φ j) i

Can is the negation of must not, since compatibility with a premise set is the failure of the negation to follow from it.

theorem Kratzer1977.mustInView_iff_not_canInView_not {W : Type u_1} (f : Modality.Background W) (φ : W → Prop) (i : W) : MustInView f φ i ↔ ¬CanInView f (fun (j : W) => ¬φ j) i

theorem Kratzer1977.canInView_of_mem {W : Type u_1} {f : Modality.Background W} {φ : W → Prop} {i : W} {B : Set (W → Prop)} (hB : B ∈ consistentSubsets (f i)) (hφ : φ ∈ B) : CanInView f φ i

A premise in a consistent subset is possible under Definition 8: every consistent extension still contains it.

theorem Kratzer1977.mustInView_of_forall_not_disjoint {W : Type u_1} {f : Modality.Background W} {φ : W → Prop} {i : W} (hφ : φ ∈ f i) (h : ∀ B ∈ consistentSubsets (f i), ¬Disjoint (sInf B) φ) : MustInView f φ i

A premise of f i is necessary under Definition 7 when it is compatible with every consistent subset: each extends by it to a consistent subset that entails it.

theorem Kratzer1977.sInf_ne_bot_iff {W : Type u_1} {B : Set (W → Prop)} : sInf B ≠ ⊥ ↔ ∃ (w : W), ∀ x ∈ B, x w

theorem Kratzer1977.not_disjoint_sInf_iff {W : Type u_1} {φ : W → Prop} {B : Set (W → Prop)} : ¬Disjoint (sInf B) φ ↔ ∃ (w : W), (∀ x ∈ B, x w) ∧ φ w

The worlds

@[reducible, inline]

abbrev Kratzer1977.World : Type

The four worlds: the truth values of the two issues an example turns on.

Equations

• Kratzer1977.World = (Bool × Bool)

def Kratzer1977.p : World → Prop

The first issue holds.

Equations

• Kratzer1977.p x✝ = (x✝.1 = true)

def Kratzer1977.q : World → Prop

The second issue holds.

Equations

• Kratzer1977.q x✝ = (x✝.2 = true)

The New Zealand judgments (§2.1–§2.2)

p is that murder is a crime, the judgment (10); q that deer are personally responsible for damage they inflict on young trees, the Auckland judgment (11); and qᶜ the Wellington judgment (12).

def Kratzer1977.judgments : Set (World → Prop)

What the New Zealand judgments provide.

Equations

• Kratzer1977.judgments = {Kratzer1977.p, Kratzer1977.q, Kratzer1977.qᶜ}

theorem Kratzer1977.judgments_inconsistent : sInf judgments = ⊥

theorem Kratzer1977.simpleNecessity_neg_p (w : World) : Modality.simpleNecessity (Function.const World judgments) pᶜ w

Under Definition 5 the inconsistent judgments make (7) true: it must be that murder is not a crime, by ex falso quodlibet.

theorem Kratzer1977.not_simplePossibility_q (w : World) : ¬Modality.simplePossibility (Function.const World judgments) q w

Under Definition 6 nothing is compatible with the judgments, so (8) is false: deer cannot be personally responsible.

theorem Kratzer1977.must_p (w : World) : MustInView (Function.const World judgments) p w

Definition 7 makes (6) true, murder must be a crime: p is compatible with every consistent subset of the judgments, since making murder a crime at a world of the subset keeps it there.

theorem Kratzer1977.not_must_neg_p (w : World) : ¬MustInView (Function.const World judgments) pᶜ w

Definition 7 makes (7) false: no consistent subset of the judgments entails that murder is not a crime, since any of its worlds can be moved to one where murder is a crime.

theorem Kratzer1977.can_q (w : World) : CanInView (Function.const World judgments) q w

Definition 8 makes (8) true: the judgment that deer are responsible is itself a consistent subset.

theorem Kratzer1977.can_neg_q (w : World) : CanInView (Function.const World judgments) qᶜ w

Definition 8 makes (9) true, symmetrically.

theorem Kratzer1977.not_can_neg_p (w : World) : ¬CanInView (Function.const World judgments) pᶜ w

Definition 8 makes (13) false, it cannot be that murder is not a crime: the dual of (6).

The Whare Wananga recommendations (§2.3)

p is that the pupils practise striding and q that they practise flying. Te Miti's recommendation is read once as the single proposition (14), that they do both, and once as two recommendations; Te Kini's is (15), that they do not stride.

def Kratzer1977.recommendations : Set (World → Prop)

Te Miti's recommendation as one proposition, with Te Kini's.

Equations

• Kratzer1977.recommendations = {fun (w : Kratzer1977.World) => Kratzer1977.p w ∧ Kratzer1977.q w, Kratzer1977.pᶜ}

def Kratzer1977.recommendations' : Set (World → Prop)

Te Miti's recommendation as two propositions, with Te Kini's.

Equations

• Kratzer1977.recommendations' = {Kratzer1977.q, Kratzer1977.p, Kratzer1977.pᶜ}

theorem Kratzer1977.not_must_q (w : World) : ¬MustInView (Function.const World recommendations) q w

On the first reading (16) is false: Te Kini's ban is a consistent subset whose only consistent extension is itself, and flying does not follow from it.

theorem Kratzer1977.must_q (w : World) : MustInView (Function.const World recommendations') q w

On the second reading (16) is true: flying is compatible with every consistent subset.