Kratzer (2012): Modals and Conditionals

This file formalizes the distinction the book's second chapter draws, in its typology of conversational backgrounds, between realistic backgrounds representing evidence of things and informational backgrounds representing the propositional content of a source of information. A rumor that Roger was elected chief can feed either. As evidence of things it determines the worlds that contain a counterpart of the rumor, produced the same way; whether Roger's counterpart was elected there depends on how reliable the source is, so given the rumor, Roger must have been elected chief is false when the rumor rests on shaky evidence and true only when the source is reliable. As a source of information it determines the worlds compatible with what it says, so the German reportative sollen in dem Gerücht nach soll Roger zum Häuptling gewählt worden sein is true whatever the rumor's provenance, even a lie. The informational background is therefore not realistic, since the actual world need not be among the worlds the rumor describes.

The chapter's revised comparative possibility (§2.4) compares two propositions only on the worlds where they differ. Along a ranking of worlds without ties, the probability measures that preserve it are exactly those in which each world outweighs all worse worlds together, and Kratzer's toy measure, giving the world wᵢ the probability 2ⁱ/15, is one of them. Once two worlds are unranked and a third is not above them, no measure giving that third world weight preserves it, as the chapter observes for ties. Under the Limit Assumption a ranking without ties has a single best world, so necessity and possibility collapse (§2.5). With a tie they come apart. The necessary propositions are then those necessary however the tie is resolved, a supervaluation that Stalnaker proposed for counterfactuals, and the merely possible ones are those holding at exactly one of the tied best worlds.

Implementation notes

The worlds record whether Roger was elected and whether the rumor exists, so every claim is decided over Bool × Bool. The evidence-of-things background at a world lists the status of the rumor there; the informational background lists the rumor's content. Reliability is stated generally, as a proposition of the background entailing the content wherever the rumor exists, rather than as an extra coordinate. Counterparts are identified with the rumor's status, since the model has no other individuals.

The toy examples' worlds are Fin 4, the index of wᵢ being i, and all of them are accessible, so comparative possibility is KratzerLift of the induced ordering with no modal base to restrict it. The chapter states the rankings O₁ and O₂ of §2.5 directly; here they are induced by nested ordering sources, and O₁ is the ranking of §2.4. The general results of §2.4–§2.5 are Kratzer's question and caveats answered for these operators rather than theorems the chapter proves.

References

• [Kra12b]
• [Kra81b] — the original typology of conversational backgrounds
• [Sta81] — the supervaluation over resolutions of an ordering, for counterfactuals
• [RMD08] — the St'át'imcets reportative the chapter contrasts with German sollen

@[reducible, inline]

abbrev Kratzer2012.World : Type

A world records whether Roger was elected chief and whether the rumor that he was exists.

Equations

• Kratzer2012.World = (Bool × Bool)

def Kratzer2012.chief : World → Prop

Roger was elected chief.

Equations

• Kratzer2012.chief x✝ = (x✝.1 = true)

def Kratzer2012.rumor : World → Prop

The rumor exists.

Equations

• Kratzer2012.rumor x✝ = (x✝.2 = true)

def Kratzer2012.evidence : Modality.Background World

As evidence of things, the rumor makes the background at w record its status in w, so the accessible worlds are those with a counterpart of the actual rumor, or with none if there is none.

Equations

• Kratzer2012.evidence w = {fun (v : Kratzer2012.World) => v.2 = w.2}

def Kratzer2012.content : Modality.Background World

As a source of information, the rumor makes the background list its content.

Equations

• Kratzer2012.content = Function.const Kratzer2012.World {Kratzer2012.chief}

def Kratzer2012.tacticDecide_worlds : Lean.ParserDescr

Decide a claim about the backgrounds over the four worlds.

Equations

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

theorem Kratzer2012.evidence_realistic : evidence.IsRealistic

The evidence-of-things background is realistic, since every world has the rumor's status it has.

theorem Kratzer2012.content_not_realistic : ¬content.IsRealistic

The informational background is not realistic, since at a world where the rumor is a lie the world itself is not among those compatible with the rumor's content.

theorem Kratzer2012.sollen_holds (w : World) : Modality.simpleNecessity content chief w

The reportative reading of (8b) holds at every world, a lie included, because it reports the rumor's content.

theorem Kratzer2012.not_must_chief (w : World) : ¬Modality.simpleNecessity evidence chief w

On shaky evidence (8a) fails, since where the rumor exists the worlds with a counterpart of it include one where Roger was not elected, so Roger need not have been elected chief.

theorem Kratzer2012.can_chief (w : World) (h : rumor w) : Modality.simplePossibility evidence chief w

Yet the rumor leaves Roger's election possible wherever it exists.

theorem Kratzer2012.must_of_reliable {W : Type u_1} (rumor chief reliable : W → Prop) (f : Modality.Background W) (hf : ∀ (w : W), rumor w → rumor ∈ f w ∧ reliable ∈ f w) (hrel : ∀ (v : W), reliable v → rumor v → chief v) (w : W) (hw : rumor w) : Modality.simpleNecessity f chief w

From a reliable source (8a) holds. If the background also records that the rumor is reliable, a proposition entailing its content wherever the rumor exists, then Roger must have been elected chief, for any worlds and backgrounds.

Grades of possibility (§2.4–§2.5)

Comparative possibility on a ranking of worlds is the revised lift KratzerLift, which compares two propositions only on the worlds where they differ. Along a ranking without ties, the probability measures that preserve it are those in which each world outweighs all worse worlds together, and once two worlds are unranked with a third not above them, no measure giving that third world weight preserves it. Under the Limit Assumption a ranking without ties has a single best world, so necessity and possibility coincide. The toy examples of §2.4 and §2.5 are instances on four worlds.

def Kratzer2012.Grades.Superincreasing {α : Type u_1} [MeasurableSpace α] [Preorder α] (μ : MeasureTheory.Measure α) : Prop

A measure is superincreasing along a ranking when each world outweighs all worse worlds together.

Equations

• Kratzer2012.Grades.Superincreasing μ = ∀ (a : α), μ (Set.Iio a) < μ {a}

theorem Kratzer2012.Grades.Superincreasing.measure_lt_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [LinearOrder α] [Finite α] (hμ : Superincreasing μ) {D E : Set α} (hDE : Disjoint D E) : μ D < μ E ↔ ∃ b ∈ E, ∀ a ∈ D, a < b

Under a superincreasing measure one proposition outweighs another disjoint from it exactly when some world of it is better than every world of the other.

theorem Kratzer2012.Grades.not_kratzerLift_iff_measure_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasurableSingletonClass α] [MeasureTheory.IsFiniteMeasure μ] {r : α → α → Prop} {a b c : α} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hab' : ¬(r a b ∧ ¬r b a)) (hba : ¬(r b a ∧ ¬r a b)) (hca : ¬(r c a ∧ ¬r a c)) (hc : μ {c} ≠ 0) : ¬∀ (A B : Set α), ComparativeProbability.KratzerLift r A B ↔ μ B ≤ μ A

No measure giving c weight preserves comparative possibility when neither of a and b is strictly better than the other and c is not strictly better than a. The propositions {a} and {b, c} are then equally good possibilities, which leaves c no weight (p. 41).

theorem Kratzer2012.Grades.kratzerLift_iff_measure_le_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasurableSingletonClass α] [MeasureTheory.IsFiniteMeasure μ] [Finite α] [LinearOrder α] : (∀ (A B : Set α), ComparativeProbability.KratzerLift (fun (x1 x2 : α) => x1 ≥ x2) A B ↔ μ B ≤ μ A) ↔ Superincreasing μ

The measures that preserve comparative possibility along a ranking without ties are the superincreasing ones.

theorem Kratzer2012.Grades.humanNecessity_iff_humanPossibility {W : Type u_1} {f g : Modality.Background W} {w : W} (p : W → Prop) (hlim : Modality.LimitAssumption f g w) (hne : (f.accessibleWorlds w).Nonempty) (htot : ∀ u ∈ f.accessibleWorlds w, ∀ v ∈ f.accessibleWorlds w, u ≤ v ∨ v ≤ u) (hanti : ∀ u ∈ f.accessibleWorlds w, ∀ v ∈ f.accessibleWorlds w, u ≤ v → v ≤ u → u = v) : Modality.humanNecessity f g p w ↔ Modality.humanPossibility f g p w

Under the Limit Assumption, necessity and possibility coincide when no two accessible worlds are tied or incomparable, since there is then a single best world (§2.5).

The toy example of §2.4

@[reducible, inline]

abbrev Kratzer2012.Grades.World : Type

The worlds w₀, w₁, w₂, w₃ of the toy examples.

Equations

• Kratzer2012.Grades.World = Fin 4

def Kratzer2012.Grades.ideal : Modality.Background World

The ordering source of §2.4, {w₃}, {w₂, w₃} and {w₁, w₂, w₃} at every world, which induces the ranking O₁ of §2.5.

Equations

• Kratzer2012.Grades.ideal x✝ = {fun (x : Kratzer2012.Grades.World) => 3 ≤ x, fun (x : Kratzer2012.Grades.World) => 2 ≤ x, fun (x : Kratzer2012.Grades.World) => 1 ≤ x}

theorem Kratzer2012.Grades.atLeastAsGoodAs_ideal_iff (v w z : World) : w ≤ z ↔ z ≤ w

The ranking w₃ < w₂ < w₁ < w₀ is connected and has no ties, one world being at least as good as another exactly when its index is at least the other's.

def Kratzer2012.Grades.BetterPossibility (p q : Set World) : Prop

p is a better possibility than q when it is at least as good a possibility, in the revised sense of §2.4, and not conversely.

Equations

• Kratzer2012.Grades.BetterPossibility p q = (ComparativeProbability.KratzerLift LE.le p q ∧ ¬ComparativeProbability.KratzerLift LE.le q p)

noncomputable def Kratzer2012.Grades.prob : MeasureTheory.Measure World

Kratzer's probability measure gives wᵢ the probability 2ⁱ/15.

Equations

• Kratzer2012.Grades.prob = ∑ i : Kratzer2012.Grades.World, (2 ^ ↑i / 15) • MeasureTheory.Measure.dirac i

theorem Kratzer2012.Grades.prob_coe (s : Finset World) : prob ↑s = ↑(∑ i ∈ s, 2 ^ ↑i) / 15

The probability of a proposition is the sum of 2ⁱ over its worlds wᵢ, divided by 15, which is the table of p. 42.

instance Kratzer2012.Grades.instIsProbabilityMeasureWorldProb : MeasureTheory.IsProbabilityMeasure prob

Kratzer's measure is a probability measure.

theorem Kratzer2012.Grades.superincreasing_prob : Superincreasing prob

Each world outweighs all worse worlds together under Kratzer's measure.

theorem Kratzer2012.Grades.betterPossibility_iff (p q : Set World) : BetterPossibility p q ↔ prob q < prob p

One proposition is a better possibility than another exactly when it is more probable, so the measure preserves comparative possibility (p. 43).

The rankings of §2.5

def Kratzer2012.Grades.swapped : Modality.Background World

The ordering source {w₂}, {w₂, w₃}, {w₁, w₂, w₃}, which induces the ranking O₂, w₂ < w₃ < w₁ < w₀.

Equations

• Kratzer2012.Grades.swapped x✝ = {fun (x : Kratzer2012.Grades.World) => x = 2, fun (x : Kratzer2012.Grades.World) => 2 ≤ x, fun (x : Kratzer2012.Grades.World) => 1 ≤ x}

def Kratzer2012.Grades.tied : Modality.Background World

The ordering source {w₂, w₃}, {w₁, w₂, w₃} of p. 46, which induces the ranking O₃, w₂, w₃ < w₁ < w₀, with a tie.

Equations

• Kratzer2012.Grades.tied x✝ = {fun (x : Kratzer2012.Grades.World) => 2 ≤ x, fun (x : Kratzer2012.Grades.World) => 1 ≤ x}

theorem Kratzer2012.Grades.bestWorlds_ideal : Modality.bestWorlds ⊥ ideal 0 = {3}

w₃ is the best world under O₁.

theorem Kratzer2012.Grades.bestWorlds_swapped : Modality.bestWorlds ⊥ swapped 0 = {2}

w₂ is the best world under O₂.

theorem Kratzer2012.Grades.bestWorlds_tied : Modality.bestWorlds ⊥ tied 0 = {2, 3}

w₂ and w₃ are the best worlds under O₃.

theorem Kratzer2012.Grades.humanNecessity_iff (p : World → Prop) : Modality.humanNecessity ⊥ ideal p 0 ↔ 8 / 15 ≤ prob {w : World | p w}

A proposition is necessary under O₁ exactly when its probability is at least 8/15 (§2.5).

theorem Kratzer2012.Grades.humanPossibility_iff (p : World → Prop) : Modality.humanPossibility ⊥ ideal p 0 ↔ 8 / 15 ≤ prob {w : World | p w}

A proposition is possible under O₁ exactly when it is necessary, so exactly when its probability is at least 8/15 (§2.5).

theorem Kratzer2012.Grades.humanNecessity_tied_iff (p : World → Prop) : Modality.humanNecessity ⊥ tied p 0 ↔ p 2 ∧ p 3

Under O₃ the necessary propositions are those containing w₂ and w₃ (p. 44).

theorem Kratzer2012.Grades.humanNecessity_tied_iff_and (p : World → Prop) : Modality.humanNecessity ⊥ tied p 0 ↔ Modality.humanNecessity ⊥ ideal p 0 ∧ Modality.humanNecessity ⊥ swapped p 0

The propositions necessary under O₃ are those necessary however the tie is resolved, under both O₁ and O₂ (p. 44).

theorem Kratzer2012.Grades.humanPossibility_and_iff (p : World → Prop) : Modality.humanPossibility ⊥ ideal p 0 ∧ Modality.humanPossibility ⊥ swapped p 0 ↔ Modality.humanNecessity ⊥ ideal p 0 ∧ Modality.humanNecessity ⊥ swapped p 0

Resolving the tie collapses possibility into necessity, so the propositions possible under both O₁ and O₂ are those necessary under both (p. 45).

theorem Kratzer2012.Grades.merelyPossible_tied_iff (p : World → Prop) : Modality.humanPossibility ⊥ tied p 0 ∧ ¬Modality.humanNecessity ⊥ tied p 0 ↔ Xor (p 2) (p 3)

Under O₃ the merely possible propositions, possible but not necessary, are those containing exactly one of w₂ and w₃ (p. 45).

noncomputable def Kratzer2012.Grades.probTied : MeasureTheory.Measure World

The probability measure of p. 46 gives w₀, w₁, w₂, w₃ the probabilities 1/11, 2/11, 4/11 and 4/11.

Equations

• Kratzer2012.Grades.probTied = ∑ i : Kratzer2012.Grades.World, (↑(![1, 2, 4, 4] i) / 11) • MeasureTheory.Measure.dirac i

theorem Kratzer2012.Grades.probTied_coe (s : Finset World) : probTied ↑s = ↑(∑ i ∈ s, ![1, 2, 4, 4] i) / 11

instance Kratzer2012.Grades.instIsProbabilityMeasureWorldProbTied : MeasureTheory.IsProbabilityMeasure probTied

The measure of p. 46 is a probability measure.

theorem Kratzer2012.Grades.humanNecessity_tied_iff_probTied (p : World → Prop) : Modality.humanNecessity ⊥ tied p 0 ↔ 8 / 11 ≤ probTied {w : World | p w}

Under O₃ a proposition is necessary exactly when its probability is at least 8/11 (p. 46).

theorem Kratzer2012.Grades.humanPossibility_tied_iff_probTied (p : World → Prop) : Modality.humanPossibility ⊥ tied p 0 ↔ 4 / 11 ≤ probTied {w : World | p w}

Under O₃ a proposition is possible exactly when its probability is at least 4/11 (p. 46).

theorem Kratzer2012.Grades.not_kratzerLift_tied_iff (μ : MeasureTheory.Measure World) [MeasureTheory.IsFiniteMeasure μ] (h : μ {1} ≠ 0) : ¬∀ (A B : Set World), ComparativeProbability.KratzerLift LE.le A B ↔ μ B ≤ μ A

No measure giving w₁ weight, the measure of p. 46 among them, preserves the comparative possibility of O₃, under which {w₂} and {w₁, w₃} are equally good possibilities.