Kratzer (1989): An Investigation of the Lumps of Thought

This file formalizes [Kra89]'s premise semantics for counterfactuals over situations and its argument that counterfactual reasoning needs the lumping relation between propositions. Situations are the elements of a type with a parthood preorder, propositions are sets of situations, and the worlds are the maximal situations. A proposition lumps another in a world when it is true there and every part of the world in which it is true is one in which the other is true too (§2). This is neither logical nor material implication, and a possible-worlds semantics, whose worlds have no parts, cannot tell it from the latter.

The analysis of §4.2 adds true propositions to the antecedent of a counterfactual while preserving consistency. Taken at face value it predicts (§4.3) that if Paula weren't buying a pound of apples, the Atlantic Ocean might be drying up, since the true disjunction that Paula is buying apples or the Atlantic is drying up can be added consistently to the antecedent and, with it, yields the consequent. The repair of §4.4 is that a proposition brings along everything it lumps. In a world where the Atlantic is not drying up, every situation where the disjunction holds is one where Paula is buying apples, so the disjunction lumps the first disjunct, which contradicts the antecedent. The spurious might-counterfactual is blocked, and the proposition that the Atlantic is not drying up survives and settles the question. The formal definitions of §4.6 build this into the crucial set, the family of premise sets over which would and might quantify.

Main definitions

• Kratzer1989.Lumps: lumping in a situation.
• Kratzer1989.Follows, Kratzer1989.IsConsistent, Kratzer1989.IsCompatible: logical consequence, consistency, and compatibility, which quantify over worlds only.
• Kratzer1989.Would, Kratzer1989.Might: the counterfactuals over a family of premise sets.
• Kratzer1989.consistentPremiseSets: the premise sets of the analysis of §4.2.
• Kratzer1989.IsCrucial: membership in the crucial set of §4.6.

Main results

• Kratzer1989.Lumps.iff_of_isMin: at a situation without proper parts lumping is joint truth.
• Kratzer1989.closedUnderConsequence_iff: strong closure under logical consequence is closure of the whole set.
• Kratzer1989.might_iff_not_would_compl: might is the dual of would.
• Kratzer1989.might_consistentPremiseSets_atlantic: the analysis of §4.2 validates (10a).
• Kratzer1989.not_might_crucialSet_atlantic: the crucial set blocks it.

Implementation notes

The set F of propositions relevant at a world is a parameter. The paper requires its members to be true in the world and persistent, among further conditions left open, and says the two closure conditions must be relativized to it; ClosedUnderLumping and ClosedUnderConsequence are stated relative to F.

The model has three worlds, the actual one, one where only Paula's purchase differs, and one where the Atlantic dries, and two parts of the actual world, one supporting only the purchase and one supporting only the Atlantic's calm. The second is what keeps the calm from lumping the purchase. The relevant propositions are (9a), (9b), and (9d); the moon disjunction (9e) runs in parallel.

TODO

Closure under logical consequence is idle in the Paula example. The paper motivates it with the King Ludwig example of §5.2, which needs the non-accidental generalizations of §5.

References

• A. Kratzer, An investigation of the lumps of thought (1989)
• [Kra12b], Chapter 5, the revised version of the paper

structure Kratzer1989.Lumps {S : Type u_1} [Preorder S] (p q : Set S) (w : S) : Prop

p lumps q in w when p is true in w and q is true in every part of w in which p is true (§2).

• holds : w ∈ p

  p is true in w.

• localImpl ⦃s : S⦄ : s ≤ w → s ∈ p → s ∈ q

  q is true in every part of w in which p is true.

theorem Kratzer1989.Lumps.iff_of_isMin {S : Type u_2} [PartialOrder S] {p q : Set S} {w : S} (hw : IsMin w) : Lumps p q w ↔ w ∈ p ∧ w ∈ q

At a situation without proper parts lumping is joint truth. In a possible-worlds semantics every situation is such a world, so lumping cannot be told from material implication between true propositions, which §2 argues it is not.

def Kratzer1989.worlds (S : Type u_1) [Preorder S] : Set S

The worlds, the maximal situations.

Equations

• Kratzer1989.worlds S = {s : S | IsMax s}

@[simp]

theorem Kratzer1989.mem_worlds {S : Type u_1} [Preorder S] {s : S} : s ∈ worlds S ↔ IsMax s

def Kratzer1989.Follows {S : Type u_1} [Preorder S] (A : Set (Set S)) (q : Set S) : Prop

A logically implies q when q is true in every world in which all of A is (§3.3).

Equations

• Kratzer1989.Follows A q = (Kratzer1989.worlds S ∩ ⋂₀ A ⊆ q)

def Kratzer1989.IsConsistent {S : Type u_1} [Preorder S] (A : Set (Set S)) : Prop

A is consistent when all of it is true in some world (§3.3).

Equations

• Kratzer1989.IsConsistent A = (Kratzer1989.worlds S ∩ ⋂₀ A).Nonempty

def Kratzer1989.IsCompatible {S : Type u_1} [Preorder S] (p : Set S) (A : Set (Set S)) : Prop

p is compatible with A when adding it to A preserves consistency (§3.3).

Equations

• Kratzer1989.IsCompatible p A = Kratzer1989.IsConsistent (insert p A)

theorem Kratzer1989.Follows.mono {S : Type u_1} [Preorder S] {A B : Set (Set S)} {q : Set S} (h : Follows B q) (hBA : B ⊆ A) : Follows A q

theorem Kratzer1989.isCompatible_iff_not_follows_compl {S : Type u_1} [Preorder S] {A : Set (Set S)} {p : Set S} : IsCompatible p A ↔ ¬Follows A pᶜ

Counterfactuals over premise sets

Both analyses of the paper evaluate if p, would q and if p, might q against a family of premise sets, and differ only in the family.

def Kratzer1989.Would {S : Type u_1} [Preorder S] (𝒜 : Set (Set (Set S))) (q : Set S) : Prop

Would q over the premise sets 𝒜: every premise set has an extension in 𝒜 that logically implies q.

Equations

• Kratzer1989.Would 𝒜 q = ∀ A ∈ 𝒜, ∃ A' ∈ 𝒜, A ⊆ A' ∧ Kratzer1989.Follows A' q

def Kratzer1989.Might {S : Type u_1} [Preorder S] (𝒜 : Set (Set (Set S))) (q : Set S) : Prop

Might q over the premise sets 𝒜: some premise set has q compatible with all of its extensions in 𝒜.

Equations

• Kratzer1989.Might 𝒜 q = ∃ A ∈ 𝒜, ∀ A' ∈ 𝒜, A ⊆ A' → Kratzer1989.IsCompatible q A'

theorem Kratzer1989.might_iff_not_would_compl {S : Type u_1} [Preorder S] {q : Set S} {𝒜 : Set (Set (Set S))} : Might 𝒜 q ↔ ¬Would 𝒜 qᶜ

Might q is the negation of would not q (§4.2).

def Kratzer1989.consistentPremiseSets {S : Type u_1} [Preorder S] (F : Set (Set S)) (p : Set S) : Set (Set (Set S))

The premise sets of the analysis of §4.2: the ways of adding propositions of F to the antecedent p while preserving consistency.

Equations

• Kratzer1989.consistentPremiseSets F p = {A : Set (Set S) | A ⊆ insert p F ∧ p ∈ A ∧ Kratzer1989.IsConsistent A}

The crucial set (§4.6)

def Kratzer1989.ClosedUnderLumping {S : Type u_1} [Preorder S] (F A : Set (Set S)) (w : S) : Prop

A is (weakly) closed under lumping in w relative to F: whatever in F a member of A lumps in w is in A.

Equations

• Kratzer1989.ClosedUnderLumping F A w = ∀ p ∈ A, ∀ q ∈ F, Kratzer1989.Lumps p q w → q ∈ A

def Kratzer1989.ClosedUnderConsequence {S : Type u_1} [Preorder S] (F A : Set (Set S)) : Prop

A is (strongly) closed under logical consequence relative to F: whatever in F a subset of A logically implies is in A.

Equations

• Kratzer1989.ClosedUnderConsequence F A = ∀ B ⊆ A, ∀ q ∈ F, Kratzer1989.Follows B q → q ∈ A

theorem Kratzer1989.closedUnderConsequence_iff {S : Type u_1} [Preorder S] {F A : Set (Set S)} : ClosedUnderConsequence F A ↔ ∀ q ∈ F, Follows A q → q ∈ A

Since consequence is monotone in the premises, strong closure under logical consequence is closure under the consequences of the whole set.

structure Kratzer1989.IsCrucial {S : Type u_1} [Preorder S] (F : Set (Set S)) (w : S) (p : Set S) (A : Set (Set S)) : Prop

A belongs to the crucial set F_{w,p}: it is a consistent subset of F ∪ {p} containing p, closed under lumping in w, whose members other than p are closed under logical consequence.

• subset : A ⊆ insert p F
• consistent : IsConsistent A

  Condition (i).

• antecedent_mem : p ∈ A

  Condition (ii).

• closedUnderLumping : ClosedUnderLumping F A w

  Condition (iii).

• closedUnderConsequence : ClosedUnderConsequence F (A \ {p})

  Condition (iv).

def Kratzer1989.crucialSet {S : Type u_1} [Preorder S] (F : Set (Set S)) (w : S) (p : Set S) : Set (Set (Set S))

The crucial set F_{w,p}.

Equations

• Kratzer1989.crucialSet F w p = {A : Set (Set S) | Kratzer1989.IsCrucial F w p A}

@[simp]

theorem Kratzer1989.mem_crucialSet {S : Type u_1} [Preorder S] {F A : Set (Set S)} {p : Set S} {w : S} : A ∈ crucialSet F w p ↔ IsCrucial F w p A

theorem Kratzer1989.crucialSet_subset_consistentPremiseSets {S : Type u_1} [Preorder S] {F : Set (Set S)} {p : Set S} {w : S} : crucialSet F w p ⊆ consistentPremiseSets F p

The crucial set refines the premise sets of §4.2 by the two closure conditions.

Paula's apples

inductive Kratzer1989.Sit : Type

The situations: three worlds and two parts of the actual world.

• actual : Sit
• noApples : Sit
• atlantic : Sit
• purchase : Sit
• calm : Sit

@[instance_reducible]

instance Kratzer1989.instDecidableEqSit : DecidableEq Sit

Equations

• Kratzer1989.instDecidableEqSit x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Kratzer1989.instFintypeSit : Fintype Sit

Equations

• Kratzer1989.instFintypeSit = { elems := { val := ↑Kratzer1989.Sit.enumList, nodup := Kratzer1989.Sit.enumList_nodup }, complete := Kratzer1989.instFintypeSit._proof_1 }

def Kratzer1989.Sit.le (a b : Sit) : Prop

Parthood: the two partial situations are parts of the actual world.

Equations

• a.le b = (a = b ∨ (a = Kratzer1989.Sit.purchase ∨ a = Kratzer1989.Sit.calm) ∧ b = Kratzer1989.Sit.actual)

@[instance_reducible]

instance Kratzer1989.instDecidableRelSitLe : DecidableRel Sit.le

Equations

• Kratzer1989.instDecidableRelSitLe x✝¹ x✝ = id inferInstance

@[instance_reducible]

instance Kratzer1989.instPartialOrderSit : PartialOrder Sit

Equations

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

@[instance_reducible]

instance Kratzer1989.instDecidableRelSitLe_1 : DecidableRel fun (x1 x2 : Sit) => x1 ≤ x2

Equations

• Kratzer1989.instDecidableRelSitLe_1 a b = Kratzer1989.instDecidableRelSitLe a b

@[instance_reducible]

instance Kratzer1989.instDecidableIsMaxSit (s : Sit) : Decidable (IsMax s)

Equations

• Kratzer1989.instDecidableIsMaxSit s = { decide := decide (∀ a ∈ Finset.univ, (fun (b : Kratzer1989.Sit) => s ≤ b → b ≤ s) a), reflects_decide := ⋯ }

def Kratzer1989.pa : Set Sit

(9a): Paula is buying a pound of apples.

Equations

• Kratzer1989.pa = {Kratzer1989.Sit.purchase, Kratzer1989.Sit.actual}

def Kratzer1989.ad : Set Sit

The Atlantic Ocean is drying up.

Equations

• Kratzer1989.ad = {Kratzer1989.Sit.atlantic}

def Kratzer1989.notAd : Set Sit

(9b): the Atlantic Ocean is not drying up.

Equations

• Kratzer1989.notAd = {Kratzer1989.Sit.calm, Kratzer1989.Sit.actual, Kratzer1989.Sit.noApples}

def Kratzer1989.paOrAd : Set Sit

(9d): Paula is buying a pound of apples or the Atlantic Ocean is drying up.

Equations

• Kratzer1989.paOrAd = Kratzer1989.pa ∪ Kratzer1989.ad

def Kratzer1989.notPa : Set Sit

The antecedent of (10a): Paula is not buying a pound of apples.

Equations

• Kratzer1989.notPa = {Kratzer1989.Sit.noApples, Kratzer1989.Sit.atlantic}

def Kratzer1989.facts : Set (Set Sit)

The propositions relevant at the actual world: (9a), (9b), and (9d).

Equations

• Kratzer1989.facts = {Kratzer1989.pa, Kratzer1989.notAd, Kratzer1989.paOrAd}

def Kratzer1989.tacticDecide_sit : Lean.ParserDescr

Decide a claim about the situations and propositions.

Equations

• Kratzer1989.tacticDecide_sit = Lean.ParserDescr.node `Kratzer1989.tacticDecide_sit 1024 (Lean.ParserDescr.nonReservedSymbol "decide_sit" false)

theorem Kratzer1989.actual_mem_and_isUpperSet_of_mem_facts (q : Set Sit) : q ∈ facts → Sit.actual ∈ q ∧ IsUpperSet q

The facts are true in the actual world and persistent, as §4.6 requires.

theorem Kratzer1989.lumps_paOrAd_pa : Lumps paOrAd pa Sit.actual

The disjunction lumps its first disjunct in the actual world (§4.4): the Atlantic is not drying up in any part of it.

theorem Kratzer1989.not_follows_paOrAd_pa : ¬Follows {paOrAd} pa

Lumping is not logical implication (§2): the disjunction does not imply its first disjunct.

theorem Kratzer1989.not_lumps_notAd_pa : ¬Lumps notAd pa Sit.actual

Nor is it material implication (§2): the calm of the Atlantic and the purchase are both true in the actual world, but a part of it supports the first without the second.

theorem Kratzer1989.not_lumps_notAd_paOrAd : ¬Lumps notAd paOrAd Sit.actual

Nor does the calm lump the disjunction.

The analysis of §4.2 and its failure (§4.3)

theorem Kratzer1989.might_consistentPremiseSets_atlantic : Might (consistentPremiseSets facts notPa) ad

(10a) under the analysis of §4.2: adding the disjunction to the antecedent keeps the premises consistent and makes the Atlantic's drying compatible with every extension.

The repair (§4.4)

theorem Kratzer1989.isCrucial_notPa_notAd : IsCrucial facts Sit.actual notPa {notPa, notAd}

The antecedent together with the Atlantic's calm is in the crucial set.

theorem Kratzer1989.not_might_crucialSet_atlantic : ¬Might (crucialSet facts Sit.actual notPa) ad

(10a) under lumping: no crucial premise set keeps the Atlantic's drying compatible. The disjunction cannot be added, since it brings along the purchase, which contradicts the antecedent; and once the Atlantic's calm is added the consequent is out.

theorem Kratzer1989.would_crucialSet_compl_ad : Would (crucialSet facts Sit.actual notPa) adᶜ

The dual: under lumping, if Paula weren't buying apples the Atlantic would not be drying up.