Glass 2023: Anna Karenina Principle and cause

[Gla23b]

Using the Anna Karenina Principle to explain why cause favors negative-sentiment complements. Semantics and Pragmatics 16, Article 6.

Core contributions

1. Cross-cuts necessity/sufficiency into local (∃ background) vs global (∀ backgrounds) variants.

2. Shows that global sufficiency licenses inference under uncertainty while global necessity does not — the key asymmetry (Table 2).

3. Proposes that cause entails local sufficiency and only implicates local necessity — reversing [NL20]'s assignment where cause entails necessity.

4. Links the asymmetry to sentiment via the Anna Karenina Principle (Diamond 1997): desirable outcomes get conjunctive models (multiple necessary factors), undesirable outcomes get disjunctive models (single sufficient factors), so C causes E is true in more contexts when E is bad.

V2 substrate

This file uses V2 BoolSEM directly. The legacy CausalDynamics-based formalization (576 LOC including conjunctive/disjunctive helper lemmas and the Anna Karenina sentiment theorems) was deleted in Phase D-H; the core local/global concepts are re-stated here over BoolSEM. The sentiment-asymmetry theorems are recoverable from this scaffolding when needed.

Local vs Global Sufficiency / Necessity (defs 8–11)

Glass's quartet of distinctions over BoolSEM:

• GloballySufficient: setting cause = true develops effect = true in every background where cause and effect are undetermined.
• LocallySufficient: there exists some such background.
• GloballyNecessary: in every background where cause and effect are undetermined, effect does NOT develop.
• LocallyNecessary: there exists some such background.

The local/global distinction matters because Glass argues that cause asserts only local sufficiency but pragmatically implicates the stronger global form.

noncomputable def Glass2023.GloballySufficient {V : Type u_1} [Fintype V] [DecidableEq V] (M : Causation.BoolSEM V) [M.graph.IsDAG] [Causation.SEM.IsDeterministic M] (cause effect : V) : Prop

Globally sufficient ([Gla23b] def 11).

Equations

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

noncomputable def Glass2023.LocallySufficient {V : Type u_1} [Fintype V] [DecidableEq V] (M : Causation.BoolSEM V) [M.graph.IsDAG] [Causation.SEM.IsDeterministic M] (cause effect : V) : Prop

Locally sufficient ([Gla23b] def 10).

Equations

• Glass2023.LocallySufficient M cause effect = ∃ (bg : Causation.Valuation fun (x : V) => Bool), bg.get effect = none ∧ (Causation.SEM.developDet M (bg.extend cause true)).hasValue effect true

noncomputable def Glass2023.GloballyNecessary {V : Type u_1} [Fintype V] [DecidableEq V] (M : Causation.BoolSEM V) [M.graph.IsDAG] [Causation.SEM.IsDeterministic M] (cause effect : V) : Prop

Globally necessary ([Gla23b] def 9).

Equations

• Glass2023.GloballyNecessary M cause effect = ∀ (bg : Causation.Valuation fun (x : V) => Bool), bg.get cause = none → bg.get effect = none → ¬(Causation.SEM.developDet M bg).hasValue effect true

noncomputable def Glass2023.LocallyNecessary {V : Type u_1} [Fintype V] [DecidableEq V] (M : Causation.BoolSEM V) [M.graph.IsDAG] [Causation.SEM.IsDeterministic M] (cause effect : V) : Prop

Locally necessary ([Gla23b] def 8).

Equations

• Glass2023.LocallyNecessary M cause effect = ∃ (bg : Causation.Valuation fun (x : V) => Bool), bg.get cause = none ∧ bg.get effect = none ∧ ¬(Causation.SEM.developDet M bg).hasValue effect true

Entailment: Global → Local

Both global → local entailments are immediate: instantiate the universal with Valuation.empty, which trivially has cause and effect undetermined.

theorem Glass2023.global_sufficient_implies_local {V : Type u_1} [Fintype V] [DecidableEq V] {M : Causation.BoolSEM V} [M.graph.IsDAG] [Causation.SEM.IsDeterministic M] {cause effect : V} (h : GloballySufficient M cause effect) : LocallySufficient M cause effect

Global sufficiency entails local sufficiency ([Gla23b] (22a)).

theorem Glass2023.global_necessary_implies_local {V : Type u_1} [Fintype V] [DecidableEq V] {M : Causation.BoolSEM V} [M.graph.IsDAG] [Causation.SEM.IsDeterministic M] {cause effect : V} (h : GloballyNecessary M cause effect) : LocallyNecessary M cause effect

Global necessity entails local necessity ([Gla23b] (21a)).

Glass's cause (def 12)

Glass argues that cause truth-conditionally requires only LOCAL sufficiency — causeSemGlass collapses to BoolSEM.causallySufficient. This is truth-conditionally identical to [NL20]'s make; the difference is that Glass relegates necessity to pragmatic implicature.

@[reducible, inline]

abbrev Glass2023.causeSemGlass {V : Type u_1} [Fintype V] [DecidableEq V] (M : Causation.BoolSEM V) [M.graph.IsDAG] [Causation.SEM.IsDeterministic M] (bg : Causation.Valuation fun (x : V) => Bool) (cause effect : V) : Prop

Glass's proposed truth condition for "C causes E" ([Gla23b] def 12): C is causally sufficient for E in the actual background.

Equations

• Glass2023.causeSemGlass M bg cause effect = M.causallySufficient bg cause effect

theorem Glass2023.glass_cause_is_causallySufficient {V : Type u_1} [Fintype V] [DecidableEq V] (M : Causation.BoolSEM V) [M.graph.IsDAG] [Causation.SEM.IsDeterministic M] (bg : Causation.Valuation fun (x : V) => Bool) (cause effect : V) : causeSemGlass M bg cause effect ↔ M.causallySufficient bg cause effect

Glass's cause is truth-conditionally identical to N&L's make (causallySufficient). The difference is pragmatic.

theorem Glass2023.glass_nl_diverge_on_bus : causeSemGlass NadathurLauer2020.Bus.busSEM NadathurLauer2020.Bus.s_b NadathurLauer2020.Bus.V.Tr NadathurLauer2020.Bus.V.Bs ∧ ¬Causation.Necessity.causeSem NadathurLauer2020.Bus.busSEM NadathurLauer2020.Bus.s_b NadathurLauer2020.Bus.V.Tr true NadathurLauer2020.Bus.V.Bs true

Glass vs N&L diverge on the Bus scenario: "Ava's training caused Lia to take the bus" is true on Glass's sufficiency-based cause but false on [NL20]'s necessity-based cause — the same verb, the same scenario, opposite predictions. The two conjuncts are [NL20]'s own (33a)/(33b) verdicts, repackaged as the rival-accounts comparison this paper draws.