Merin (1999): Information, Relevance, and Social Decisionmaking

This file formalizes the applications of Decision-Theoretic Semantics in [Mer99b] to or, but, even, and also. The framework (contexts, relevance, issue-conditional independence, Fact 5, Theorem 6a) is Pragmatics/DecisionTheoretic/Basic.lean.

Scalar implicature. Hypothesis 3 licenses X if not indeed Y in a context when Y is more relevant than X, and X positively so, to one side of the issue (IfNotIndeed). When A and B are independent on each side of the issue and finitely confirm it (IndepConfirmers, the antecedent of Theorem 6), Theorem 6a makes the conjunction more relevant than either disjunct and than the disjunction, so A (or B), if not indeed A and B is licensed (Prediction 2, IndepConfirmers.ifNotIndeed_inter). Theorem 6b's non-derivabilities are countermodels: the exclusive disjunction can be negatively relevant (exists_negRelevant_symmDiff) or not (exists_not_negRelevant_symmDiff), and the disjunction can be as relevant as a disjunct, which blocks A or B, if not indeed A (Prediction 1, exists_not_ifNotIndeed_union).

But and even. Hypothesis 4 (ButFelicitous) makes A an argument for the issue and B and A∧B arguments against it. Hypothesis 5 (EvenFelicitous) is the scalar presupposition of even (Focus.Particles.evenPresup) with relevance in place of likelihood; by Fact 2 the most relevant alternative is the one whose truth would be most surprising if ¬H rather than H were accepted, Merin's reconciliation of argumentative value with [Fra95]'s surprise and against [Kay90]'s informativeness. With one issue per reading, the two hypotheses clash on the sign of B (Prediction 3, not_butFelicitous_and_evenFelicitous). Under issue-conditional independence, A and B are H-contrary iff B is unexpected given A (Theorem 8, cond_lt_iff_hContrary). The default issue of A but B is ¬B, where independence holds automatically (Theorem 9) and the basic properties of but follow (Theorem 10). Non-negative instantial relevance then excludes Qa but Qb (Corollary 11), Harris's subject-predicate asymmetry.

Also. A proposition is presupposed when conditioning on it changes nothing (Definition 12), equivalently when it has probability one (isPresupposed_iff); it is then irrelevant to every issue and factors out of conjunctions (Fact 17). The antecedent of also must have spent its relevance in becoming presupposed (Definition 13, Hypothesis 8), so it cannot be the focus's own instance (Corollary 15), cannot be properly accommodated (Partial Definition 14), and lacks prima facie causal responsibility for its host (Corollary 16, Prediction 4).

Implementation notes

• Relevance statements are on bayesFactor in ℝ≥0∞: r > 0 is 1 < bayesFactor, finitude of relevance is bayesFactor ≠ ⊤, and Merin's sgn(r) is compare (bayesFactor ctx e) 1.
• The earlier context i − k of Definition 13 is a second Context over the same issue; that it is the last one before D became presupposed is not modelled.
• Theorem 6b's countermodels are counting priors on small world types.

TODO

• Theorem 6a's clause that the disjunction is more relevant than the exclusive disjunction is not formalized.
• Definition 7, Definition 8 with Hypothesis 1 (claims and implicatures as relevance cones), Fact 4, Theorem 7, and Theorems 12 and 13 with Corollary 14 are not formalized.

References

• [Mer99b]
• [AD77]
• [KP79]
• [Kay90]
• [Fra95]

Scalar implicature

structure Merin1999a.IndepConfirmers {W : Type u_1} [MeasurableSpace W] (ctx : DTS.Context W) (a b : Set W) : Prop

The antecedent of Theorem 6: A and B independent conditionally on each side of the issue (Definition 9) and each confirming H finitely, ∞ > r(A), r(B) > 0.

• indep : DTS.CondIndepIssue ctx a b
• one_lt_left : DTS.posRelevant ctx a
• one_lt_right : DTS.posRelevant ctx b
• ne_top_left : DTS.bayesFactor ctx a ≠ ⊤
• ne_top_right : DTS.bayesFactor ctx b ≠ ⊤

def Merin1999a.IfNotIndeed {W : Type u_1} [MeasurableSpace W] (ctx : DTS.Context W) (x y : Set W) : Prop

The condition Hypothesis 3 places on a context for X if not indeed Y: X is positively relevant, and Y more so, to H or to ¬H. The schema is acceptable iff every context in which X and Y satisfy the Conditional Independence Presumption with finite relevance meets it.

Equations

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

theorem Merin1999a.IndepConfirmers.ifNotIndeed_inter {W : Type u_1} [MeasurableSpace W] {ctx : DTS.Context W} [MeasureTheory.IsFiniteMeasure ctx.prior] [ctx.Nondegenerate] {a b : Set W} (hbm : MeasurableSet b) (h : IndepConfirmers ctx a b) : IfNotIndeed ctx (a ∪ b) (a ∩ b) ∧ IfNotIndeed ctx a (a ∩ b)

Prediction 2: A (or B), if not indeed A and B. When A and B are independent finite confirmers of H, the conjunction is more relevant than the disjunction and than A, both of which confirm H (Theorem 6a).

Theorem 6b

inductive Merin1999a.World₁ : Type

The worlds of the first countermodel: at issue, the only world where H holds, A and B both hold; at off a b, A holds iff a and B iff b.

• issue : World₁
• off (a b : Bool) : World₁

def Merin1999a.instDecidableEqWorld₁.decEq (x✝ x✝¹ : World₁) : Decidable (x✝ = x✝¹)

Equations

• Merin1999a.instDecidableEqWorld₁.decEq Merin1999a.World₁.issue Merin1999a.World₁.issue = isTrue ⋯
• Merin1999a.instDecidableEqWorld₁.decEq Merin1999a.World₁.issue (Merin1999a.World₁.off a b) = isFalse ⋯
• Merin1999a.instDecidableEqWorld₁.decEq (Merin1999a.World₁.off a b) Merin1999a.World₁.issue = isFalse ⋯
• Merin1999a.instDecidableEqWorld₁.decEq (Merin1999a.World₁.off a a_1) (Merin1999a.World₁.off b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Merin1999a.instDecidableEqWorld₁ : DecidableEq World₁

Equations

• Merin1999a.instDecidableEqWorld₁ = Merin1999a.instDecidableEqWorld₁.decEq

@[instance_reducible]

instance Merin1999a.instFintypeWorld₁ : Fintype World₁

Equations

• Merin1999a.instFintypeWorld₁ = Fintype.ofEquiv (Unit ⊕ (_ : Bool) × Bool) Merin1999a.World₁.proxyTypeEquiv

@[instance_reducible]

instance Merin1999a.instMeasurableSpaceWorld₁ : MeasurableSpace World₁

Equations

• Merin1999a.instMeasurableSpaceWorld₁ = ⊤

instance Merin1999a.instDiscreteMeasurableSpaceWorld₁ : DiscreteMeasurableSpace World₁

def Merin1999a.World₁.a : World₁ → Bool

Whether A holds at a world of the first countermodel.

Equations

• Merin1999a.World₁.issue.a = true
• (Merin1999a.World₁.off a a_1).a = a

def Merin1999a.World₁.b : World₁ → Bool

Whether B holds at a world of the first countermodel.

Equations

• Merin1999a.World₁.issue.b = true
• (Merin1999a.World₁.off a a_1).b = a_1

theorem Merin1999a.exists_negRelevant_symmDiff : ∃ (ctx : DTS.Context World₁) (a : Set World₁) (b : Set World₁), IndepConfirmers ctx a b ∧ DTS.negRelevant ctx (symmDiff a b)

Theorem 6b, first clause: that the exclusive disjunction of independent finite confirmers does not disconfirm H is not derivable. In the first countermodel it is false at the one world where H holds.

inductive Merin1999a.World₂ : Type

The worlds of the second countermodel: at issue a, where H holds, A holds iff a and B holds; at off i b, A holds iff i = 0 and B iff b.

• issue (a : Bool) : World₂
• off (i : Fin 3) (b : Bool) : World₂

def Merin1999a.instDecidableEqWorld₂.decEq (x✝ x✝¹ : World₂) : Decidable (x✝ = x✝¹)

Equations

• Merin1999a.instDecidableEqWorld₂.decEq (Merin1999a.World₂.issue a) (Merin1999a.World₂.issue b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Merin1999a.instDecidableEqWorld₂.decEq (Merin1999a.World₂.issue a) (Merin1999a.World₂.off i b) = isFalse ⋯
• Merin1999a.instDecidableEqWorld₂.decEq (Merin1999a.World₂.off i b) (Merin1999a.World₂.issue a) = isFalse ⋯
• Merin1999a.instDecidableEqWorld₂.decEq (Merin1999a.World₂.off a a_1) (Merin1999a.World₂.off b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Merin1999a.instDecidableEqWorld₂ : DecidableEq World₂

Equations

• Merin1999a.instDecidableEqWorld₂ = Merin1999a.instDecidableEqWorld₂.decEq

@[instance_reducible]

instance Merin1999a.instFintypeWorld₂ : Fintype World₂

Equations

• Merin1999a.instFintypeWorld₂ = Fintype.ofEquiv (Bool ⊕ (_ : Fin 3) × Bool) Merin1999a.World₂.proxyTypeEquiv

@[instance_reducible]

instance Merin1999a.instMeasurableSpaceWorld₂ : MeasurableSpace World₂

Equations

• Merin1999a.instMeasurableSpaceWorld₂ = ⊤

instance Merin1999a.instDiscreteMeasurableSpaceWorld₂ : DiscreteMeasurableSpace World₂

def Merin1999a.World₂.h : World₂ → Bool

Whether H holds at a world of the second countermodel.

Equations

• (Merin1999a.World₂.issue a).h = true
• (Merin1999a.World₂.off a a_1).h = false

def Merin1999a.World₂.a : World₂ → Bool

Whether A holds at a world of the second countermodel.

Equations

• (Merin1999a.World₂.issue a).a = a
• (Merin1999a.World₂.off a a_1).a = decide (a = 0)

def Merin1999a.World₂.b : World₂ → Bool

Whether B holds at a world of the second countermodel.

Equations

• (Merin1999a.World₂.issue a).b = true
• (Merin1999a.World₂.off a a_1).b = a_1

theorem Merin1999a.exists_not_negRelevant_symmDiff : ∃ (ctx : DTS.Context World₂) (a : Set World₂) (b : Set World₂), IndepConfirmers ctx a b ∧ ¬DTS.negRelevant ctx (symmDiff a b)

Theorem 6b, second clause: that the exclusive disjunction of independent finite confirmers disconfirms H is not derivable either. In the second countermodel it is irrelevant.

theorem Merin1999a.exists_not_ifNotIndeed_union : ∃ (ctx : DTS.Context World₂) (a : Set World₂) (b : Set World₂), IndepConfirmers ctx a b ∧ ¬IfNotIndeed ctx (a ∪ b) a

Prediction 1: A or B, if not indeed A. By Theorem 6b's third clause the disjunction need not be less relevant than a disjunct: in the second countermodel the disjunction and A confirm H equally, and the disjunction disconfirms ¬H, so neither condition of Hypothesis 3 holds.

But and even

def Merin1999a.ButFelicitous {W : Type u_1} [MeasurableSpace W] (ctx : DTS.Context W) (a b : Set W) : Prop

Hypothesis 4: A but B is felicitous only if, for the issue H, A confirms H while B and A∧B disconfirm it.

Equations

• Merin1999a.ButFelicitous ctx a b = (DTS.posRelevant ctx a ∧ DTS.negRelevant ctx b ∧ DTS.negRelevant ctx (a ∩ b))

def Merin1999a.EvenFelicitous {W : Type u_1} [MeasurableSpace W] (ctx : DTS.Context W) (a b : Set W) : Prop

Hypothesis 5: A CONJ even(B) with VP-focus is felicitous only if, for an issue H other than B, A confirms H and B is more relevant to H than A: the scalar presupposition of even with relevance for likelihood, over the one alternative A.

Equations

• Merin1999a.EvenFelicitous ctx a b = (ctx.topic ≠ b ∧ DTS.posRelevant ctx a ∧ Focus.Particles.evenPresup (fun (e : Set W) => OrderDual.toDual (DTS.bayesFactor ctx e)) b {a})

theorem Merin1999a.not_butFelicitous_and_evenFelicitous {W : Type u_1} [MeasurableSpace W] (ctx : DTS.Context W) (a b : Set W) : ¬(ButFelicitous ctx a b ∧ EvenFelicitous ctx a b)

Prediction 3: *Kim splurbs but Kim even glurbs. With one issue per reading, but needs B to disconfirm it and even needs B to confirm it more than A does.

theorem Merin1999a.cond_lt_iff_hContrary {W : Type u_1} [MeasurableSpace W] (ctx : DTS.Context W) [MeasureTheory.IsProbabilityMeasure ctx.prior] [ctx.Nondegenerate] {a b : Set W} (ham : MeasurableSet a) (hcip : DTS.CondIndepIssue ctx a b) (ha0 : ctx.prior a ≠ 0) (hb0 : ctx.prior b ≠ 0) : ctx.prior[b | a] < ctx.prior b ↔ DTS.hContrary ctx a b

Theorem 8: under issue-conditional independence, B is unexpected given A iff A and B are H-contrary. Both come to the sign of one factorized cross-product of the masses of A and B on either side of the issue.

@[reducible, inline]

abbrev Merin1999a.defaultButCtx {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) (b : Set W) (hb : MeasurableSet b) : DTS.Context W

The default context of A but B: the issue is ¬B, the special case of Hypothesis 4 that [Mer99b] compares with [AD77] and proposes as the default interpretation.

Equations

• Merin1999a.defaultButCtx μ b hb = { topic := bᶜ, topicMeasurable := ⋯, prior := μ }

theorem Merin1999a.condIndepIssue_defaultButCtx {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure μ] {a b : Set W} (ham : MeasurableSet a) (hbm : MeasurableSet b) : DTS.CondIndepIssue (defaultButCtx μ b hbm) a b

Theorem 9: when the issue is ¬B, A and B are issue-conditionally independent for every A. Given ¬B, B and A∧B are null; given B, B is certain.

theorem Merin1999a.negRelevant_defaultButCtx {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) {b : Set W} (hbm : MeasurableSet b) : DTS.negRelevant (defaultButCtx μ b hbm) b

Theorem 10(a): when the issue is ¬B, B disconfirms it.

theorem Merin1999a.bayesFactor_lt_swapIssue_defaultButCtx {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure μ] {a b : Set W} (hbm : MeasurableSet b) (hab : μ (a ∩ b) ≠ 0) : DTS.bayesFactor (defaultButCtx μ b hbm) a < DTS.bayesFactor (DTS.swapIssue (defaultButCtx μ b hbm)) b ∧ DTS.bayesFactor (defaultButCtx μ b hbm) a < DTS.bayesFactor (DTS.swapIssue (defaultButCtx μ b hbm)) (a ∩ b)

Theorem 10(b): when the issue is ¬B and A∧B is possible, B and A∧B confirm B infinitely, hence more than A confirms ¬B.

theorem Merin1999a.cond_lt_of_posRelevant_defaultButCtx {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure μ] {a b : Set W} (ham : MeasurableSet a) (hbm : MeasurableSet b) (hpos : DTS.posRelevant (defaultButCtx μ b hbm) a) (hab : μ (a ∩ b) ≠ 0) : μ[b | a] < μ b

Theorem 10(c): when the issue is ¬B, an A that confirms it makes B unexpected. The default issue makes A and B independent (Theorem 9) and H-contrary (Theorem 10(a)), so Theorem 8 applies.

theorem Merin1999a.bayesFactor_inter_defaultButCtx {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure μ] {a b : Set W} (ham : MeasurableSet a) (hbm : MeasurableSet b) (hb : μ b ≠ 0) : DTS.bayesFactor (defaultButCtx μ b hbm) (a ∩ b) = DTS.bayesFactor (defaultButCtx μ b hbm) a * DTS.bayesFactor (defaultButCtx μ b hbm) b

Theorem 10(d): when the issue is ¬B, relevance is additive over A∧B (Fact 5 by Theorem 9).

def Merin1999a.NonnegInstantialRelevance {W : Type u_1} [MeasurableSpace W] {E : Type u_2} (μ : MeasureTheory.Measure W) (Q : E → Set W) : Prop

Definition 10: the prior satisfies non-negative instantial relevance for a predicate Q when no instance Qa makes another instance Qb less probable.

Equations

• Merin1999a.NonnegInstantialRelevance μ Q = ∀ (i j : E), μ (Q j) ≤ μ[Q j | Q i]

theorem Merin1999a.not_butFelicitous_of_nonnegInstantialRelevance {W : Type u_1} [MeasurableSpace W] {E : Type u_2} (ctx : DTS.Context W) [MeasureTheory.IsProbabilityMeasure ctx.prior] [ctx.Nondegenerate] {Q : E → Set W} (hQ : NonnegInstantialRelevance ctx.prior Q) {i j : E} (hm : MeasurableSet (Q i)) (hcip : DTS.CondIndepIssue ctx (Q i) (Q j)) (hi : ctx.prior (Q i) ≠ 0) (hj : ctx.prior (Q j) ≠ 0) : ¬ButFelicitous ctx (Q i) (Q j)

Corollary 11: under non-negative instantial relevance, Qa but Qb is infelicitous in every context where the Conditional Independence Presumption holds of its conjuncts, since H-contrariness would make Qb unexpected given Qa (Theorem 8).

theorem Merin1999a.not_butFelicitous_defaultButCtx {W : Type u_1} [MeasurableSpace W] {E : Type u_2} (μ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure μ] {Q : E → Set W} (hQ : NonnegInstantialRelevance μ Q) {i j : E} (hmi : MeasurableSet (Q i)) (hmj : MeasurableSet (Q j)) (hi : μ (Q i) ≠ 0) (hj : μ (Q j) ≠ 0) (hjc : μ (Q j)ᶜ ≠ 0) : ¬ButFelicitous (defaultButCtx μ (Q j) hmj) (Q i) (Q j)

Corollary 11 at the default issue ¬Qb, where the presumption holds by Theorem 9.

Also

def Merin1999a.IsPresupposed {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) (a : Set W) : Prop

Definition 12: A is presupposed when conditioning on A changes no probability.

Equations

• Merin1999a.IsPresupposed μ a = (μ[|a] = μ)

theorem Merin1999a.isPresupposed_iff {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} [MeasureTheory.IsProbabilityMeasure μ] {a : Set W} (ha : MeasurableSet a) : IsPresupposed μ a ↔ μ a = 1

A presupposition is a proposition of probability one.

theorem Merin1999a.IsPresupposed.bayesFactor_inter {W : Type u_1} [MeasurableSpace W] {ctx : DTS.Context W} {a : Set W} [MeasureTheory.IsProbabilityMeasure ctx.prior] (h : IsPresupposed ctx.prior a) (ha : MeasurableSet a) (b : Set W) : DTS.bayesFactor ctx (a ∩ b) = DTS.bayesFactor ctx b

A presupposed proposition factors out of any conjunction: A∧B is exactly as relevant as B (the step of Fact 17's proof).

theorem Merin1999a.IsPresupposed.irrelevant {W : Type u_1} [MeasurableSpace W] {ctx : DTS.Context W} {a : Set W} [MeasureTheory.IsProbabilityMeasure ctx.prior] [ctx.Nondegenerate] (h : IsPresupposed ctx.prior a) (ha : MeasurableSet a) : DTS.irrelevant ctx a

A presupposed proposition is irrelevant to every live issue.

theorem Merin1999a.IsPresupposed.bayesFactor_inter_eq_mul {W : Type u_1} [MeasurableSpace W] {ctx : DTS.Context W} {a : Set W} [MeasureTheory.IsProbabilityMeasure ctx.prior] [ctx.Nondegenerate] (h : IsPresupposed ctx.prior a) (ha : MeasurableSet a) (b : Set W) : DTS.bayesFactor ctx (a ∩ b) = DTS.bayesFactor ctx a * DTS.bayesFactor ctx b

Fact 17: conditioning on A makes relevance additive over A∧B, with no independence assumption.

structure Merin1999a.TopicAnaphoricallySalient {W : Type u_1} [MeasurableSpace W] (ctx₀ ctx : DTS.Context W) (d e : Set W) : Prop

Definition 13: D is topic-anaphorically salient for E in context ctx when E is relevant to the issue, D is presupposed, and in an earlier context ctx₀ on the same issue, where D was not yet presupposed, D was relevant.

• topic_eq : ctx₀.topic = ctx.topic
• relevant : ¬DTS.irrelevant ctx e
• presupposed : IsPresupposed ctx.prior d
• lt_one : ctx₀.prior d < 1
• wasRelevant : ¬DTS.irrelevant ctx₀ d

def Merin1999a.AlsoFelicitous {W : Type u_1} [MeasurableSpace W] (ctx₀ ctx : DTS.Context W) (ba bb : Set W) : Prop

Hypothesis 8, (and) also: also(b, B) is felicitous only if Ba is topic-anaphorically salient for Bb and Ba had, when it was relevant, the relevance sign Bb has now.

Equations

• Merin1999a.AlsoFelicitous ctx₀ ctx ba bb = (Merin1999a.TopicAnaphoricallySalient ctx₀ ctx ba bb ∧ compare (DTS.bayesFactor ctx₀ ba) 1 = compare (DTS.bayesFactor ctx bb) 1)

def Merin1999a.ButAlsoFelicitous {W : Type u_1} [MeasurableSpace W] (ctx₀ ctx : DTS.Context W) (ba bb : Set W) : Prop

Hypothesis 8, but also: the signs are opposite.

Equations

• Merin1999a.ButAlsoFelicitous ctx₀ ctx ba bb = (Merin1999a.TopicAnaphoricallySalient ctx₀ ctx ba bb ∧ compare (DTS.bayesFactor ctx₀ ba) 1 = (compare (DTS.bayesFactor ctx bb) 1).swap)

theorem Merin1999a.TopicAnaphoricallySalient.ne {W : Type u_1} [MeasurableSpace W] {ctx : DTS.Context W} {E : Type u_2} {ctx₀ : DTS.Context W} [MeasureTheory.IsProbabilityMeasure ctx.prior] [ctx.Nondegenerate] {B : E → Set W} {i j : E} (h : TopicAnaphoricallySalient ctx₀ ctx (B i) (B j)) (hm : MeasurableSet (B i)) : i ≠ j

Corollary 15: the antecedent of also is not an instance of the focus itself. Were b = a, Bb would be presupposed and so irrelevant to the issue, while salience needs it relevant.

def Merin1999a.ProperlyAccommodable {W : Type u_1} [MeasurableSpace W] (ctx : DTS.Context W) (φ : Set W) : Prop

Partial Definition 14: φ is properly accommodable only if it is contingent and irrelevant to the issue.

Equations

• Merin1999a.ProperlyAccommodable ctx φ = (0 < ctx.prior φ ∧ ctx.prior φ < 1 ∧ DTS.irrelevant ctx φ)

theorem Merin1999a.TopicAnaphoricallySalient.not_properlyAccommodable {W : Type u_1} [MeasurableSpace W] {ctx ctx₀ : DTS.Context W} {d e : Set W} (h : TopicAnaphoricallySalient ctx₀ ctx d e) : ¬ProperlyAccommodable ctx₀ d

Also resists accommodation: its antecedent must have been relevant just before becoming presupposed, so it was not properly accommodable then.

def Merin1999a.PrimaFacieCause {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) (a b : Set W) : Prop

Partial Definition 15: A has prima facie causal responsibility for B only if A makes B more probable.

Equations

• Merin1999a.PrimaFacieCause μ a b = (μ b < μ[b | a])

theorem Merin1999a.IsPresupposed.not_primaFacieCause {W : Type u_1} [MeasurableSpace W] {a : Set W} {μ : MeasureTheory.Measure W} (h : IsPresupposed μ a) (b : Set W) : ¬PrimaFacieCause μ a b

Corollary 16: a presupposed proposition is prima facie causally responsible for nothing.

theorem Merin1999a.AlsoFelicitous.not_primaFacieCause {W : Type u_1} [MeasurableSpace W] {ctx ctx₀ : DTS.Context W} {ba bb : Set W} (h : AlsoFelicitous ctx₀ ctx ba bb) : ¬PrimaFacieCause ctx.prior ba bb

Prediction 4: in Kim fell and she also broke her arm, also removes the causal implicature, since its antecedent is presupposed.