Santorio (2018): alternatives and truthmakers in conditional semantics

[San18b] starts from a trilemma: counterfactuals invalidate Antecedent Strengthening, validate Simplification of Disjunctive Antecedents, and validate Substitution of Logical Equivalents in the antecedent, yet with Boolean disjunction the last two entail the first. The paper keeps the first and gives up the other two by letting an if-clause denote the set of truthmakers of its antecedent: the conjunctive closures of the minimal stable subsets of the antecedent's alternatives that entail it, where a subset is stable when it is consistent with the negation of every alternative outside it (§5: Stable, MinimalStable, truthmakers). The conditional is a description of that set (§6): with the optional distributivity operator DIST_π it holds of each truthmaker, which is Simplification (distributiveConditional), and without it the modal would extracts the disjunctive closure, which is not (collectiveConditional); DIST_π carries the all-or-nothing homogeneity presupposition (homogeneityPresup). The readings are those of Semantics/Conditionals/Counterfactual/Alternatives.lean over the truthmakers.

On Otto or Anna went to the party (44) the truthmakers are Otto went and Anna went (party_truthmakers). On (35) every student read War and Peace or Anna Karenina the global algorithm finds the mixed truthmaker some read Anna Karenina and some read War and Peace that [AO09]'s disjunct alternatives cannot (karenina_truthmakers, karenina_mixed_not_alonsoOvalle), predicting the infelicity of (39). On [McKVI77]'s Spain case, the paper's (8), the collective parsing is true and the distributive one is not, so Antecedent Strengthening fails and Simplification is not validated (spain_collective, spain_not_distributive, spain_homogeneity); and on (57)–(58), logically equivalent antecedents whose if-clauses denote different sets receive different distributive verdicts (substitution_fails).

The stability algorithm (§5)

def Santorio2018.Stable {W : Type u_1} (alts σ : List (Finset W)) : Prop

σ is stable with respect to the alternatives alts: some world verifies every member of σ and falsifies every other alternative.

Equations

• Santorio2018.Stable alts σ = ∃ (w : W), (∀ A ∈ σ, w ∈ A) ∧ ∀ A ∈ alts, A ∉ σ → w ∉ A

@[instance_reducible]

instance Santorio2018.instDecidableStable {W : Type u_1} [DecidableEq W] [Fintype W] (alts σ : List (Finset W)) : Decidable (Stable alts σ)

Equations

• Santorio2018.instDecidableStable alts σ = Santorio2018.instDecidableStable._aux_1 alts σ

def Santorio2018.MinimalStable {W : Type u_1} (alts σ : List (Finset W)) : Prop

A nonempty stable sublist of alts none of whose nonempty proper sublists is stable. (The empty set, stable whenever some world falsifies every alternative, is excluded.)

Equations

• Santorio2018.MinimalStable alts σ = (σ ≠ [] ∧ σ.Sublist alts ∧ Santorio2018.Stable alts σ ∧ ∀ τ ∈ σ.sublists, τ ≠ [] → τ ≠ σ → ¬Santorio2018.Stable alts τ)

@[instance_reducible]

instance Santorio2018.instDecidableMinimalStable {W : Type u_1} [DecidableEq W] [Fintype W] (alts σ : List (Finset W)) : Decidable (MinimalStable alts σ)

Equations

• Santorio2018.instDecidableMinimalStable alts σ = Santorio2018.instDecidableMinimalStable._aux_1 alts σ

def Santorio2018.conjunctiveClosure {W : Type u_1} [DecidableEq W] [Fintype W] (σ : List (Finset W)) : Finset W

⋀σ.

Equations

• Santorio2018.conjunctiveClosure σ = List.foldr (fun (x1 x2 : Finset W) => x1 ∩ x2) Finset.univ σ

def Santorio2018.truthmakers {W : Type u_1} [DecidableEq W] [Fintype W] (alts : List (Finset W)) (S : Finset W) : List (Finset W)

The truthmakers of S relative to alts: the conjunctive closures of the minimal stable subsets of alts that entail S — the denotation of the if-clause.

Equations

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

theorem Santorio2018.subset_of_mem_truthmakers {W : Type u_1} [DecidableEq W] [Fintype W] {alts : List (Finset W)} {S p : Finset W} (h : p ∈ truthmakers alts S) : p ⊆ S

theorem Santorio2018.disjunctiveClosure_truthmakers_subset {W : Type u_1} [DecidableEq W] [Fintype W] (alts : List (Finset W)) (S : Finset W) : Semantics.Conditionals.Counterfactual.disjunctiveClosure (truthmakers alts S) ⊆ S

The disjunctive closure of the truthmakers is at most the antecedent.

Conditionals as descriptions (§6)

def Santorio2018.distributiveConditional {W : Type u_1} [DecidableEq W] [Fintype W] (sim : Semantics.Conditionals.SimilarityOrdering W) (alts : List (Finset W)) (S : Finset W) (C : W → Prop) [DecidablePred C] (w : W) : Prop

[if φ] DIST_π [would ψ]: the counterfactual holds of every truthmaker of φ.

Equations

• Santorio2018.distributiveConditional sim alts S C w = Semantics.Conditionals.Counterfactual.Distributive sim (Santorio2018.truthmakers alts S) C w

def Santorio2018.homogeneityPresup {W : Type u_1} [DecidableEq W] [Fintype W] (sim : Semantics.Conditionals.SimilarityOrdering W) (alts : List (Finset W)) (S : Finset W) (C : W → Prop) [DecidablePred C] (w : W) : Trivalent

The homogeneity presupposition of DIST_π: every truthmaker's counterfactual holds, or none does.

Equations

• Santorio2018.homogeneityPresup sim alts S C w = Semantics.Conditionals.Counterfactual.homogeneity sim (Santorio2018.truthmakers alts S) C w

def Santorio2018.collectiveConditional {W : Type u_1} [DecidableEq W] [Fintype W] (sim : Semantics.Conditionals.SimilarityOrdering W) (alts : List (Finset W)) (S : Finset W) (C : W → Prop) [DecidablePred C] (w : W) : Prop

[if φ] would ψ without DIST_π: the modal extracts the disjunctive closure of the truthmakers.

Equations

• Santorio2018.collectiveConditional sim alts S C w = Semantics.Conditionals.Counterfactual.would sim (Santorio2018.truthmakers alts S) C w

@[instance_reducible]

instance Santorio2018.instDecidableDistributiveConditional {W : Type u_1} [DecidableEq W] [Fintype W] (sim : Semantics.Conditionals.SimilarityOrdering W) (alts : List (Finset W)) (S : Finset W) (C : W → Prop) [DecidablePred C] (w : W) : Decidable (distributiveConditional sim alts S C w)

Equations

• Santorio2018.instDecidableDistributiveConditional sim alts S C w = Santorio2018.instDecidableDistributiveConditional._aux_1 sim alts S C w

@[instance_reducible]

instance Santorio2018.instDecidableCollectiveConditional {W : Type u_1} [DecidableEq W] [Fintype W] (sim : Semantics.Conditionals.SimilarityOrdering W) (alts : List (Finset W)) (S : Finset W) (C : W → Prop) [DecidablePred C] (w : W) : Decidable (collectiveConditional sim alts S C w)

Equations

• Santorio2018.instDecidableCollectiveConditional sim alts S C w = Santorio2018.instDecidableCollectiveConditional._aux_1 sim alts S C w

Otto and Anna (44)

inductive Santorio2018.Party : Type

Who went to the party.

• ottoOnly : Party
• annaOnly : Party
• both : Party
• neither : Party

@[instance_reducible]

instance Santorio2018.instDecidableEqParty : DecidableEq Party

Equations

• Santorio2018.instDecidableEqParty x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Santorio2018.instFintypeParty : Fintype Party

Equations

• Santorio2018.instFintypeParty = { elems := { val := ↑Santorio2018.Party.enumList, nodup := Santorio2018.Party.enumList_nodup }, complete := Santorio2018.instFintypeParty._proof_1 }

@[reducible, inline]

abbrev Santorio2018.otto : Finset Party

Equations

• Santorio2018.otto = {Santorio2018.Party.ottoOnly, Santorio2018.Party.both}

@[reducible, inline]

abbrev Santorio2018.anna : Finset Party

Equations

• Santorio2018.anna = {Santorio2018.Party.annaOnly, Santorio2018.Party.both}

def Santorio2018.partyAlts : List (Finset Party)

(45): the alternatives to Otto or Anna went to the party.

Equations

• Santorio2018.partyAlts = [Santorio2018.otto ∪ Santorio2018.anna, Santorio2018.otto, Santorio2018.anna, Santorio2018.otto ∩ Santorio2018.anna]

theorem Santorio2018.party_truthmakers : (truthmakers partyAlts (otto ∪ anna)).toFinset = {otto, anna}

The truthmakers of (44) are Otto went and Anna went: the minimal stable subsets are {O ∨ A, O} and {O ∨ A, A}.

Every student read War and Peace or Anna Karenina (35)

inductive Santorio2018.Reading : Type

Which of the two books the students read.

• none : Reading
• everyAK : Reading
• everyWP : Reading
• mixed : Reading
• everyBoth : Reading

@[instance_reducible]

instance Santorio2018.instDecidableEqReading : DecidableEq Reading

Equations

• Santorio2018.instDecidableEqReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Santorio2018.instFintypeReading : Fintype Reading

Equations

• Santorio2018.instFintypeReading = { elems := { val := ↑Santorio2018.Reading.enumList, nodup := Santorio2018.Reading.enumList_nodup }, complete := Santorio2018.instFintypeReading._proof_1 }

@[reducible, inline]

abbrev Santorio2018.everyA : Finset Reading

Equations

• Santorio2018.everyA = {Santorio2018.Reading.everyAK, Santorio2018.Reading.everyBoth}

@[reducible, inline]

abbrev Santorio2018.everyW : Finset Reading

Equations

• Santorio2018.everyW = {Santorio2018.Reading.everyWP, Santorio2018.Reading.everyBoth}

@[reducible, inline]

abbrev Santorio2018.everyAorW : Finset Reading

Equations

• Santorio2018.everyAorW = {Santorio2018.Reading.everyAK, Santorio2018.Reading.everyWP, Santorio2018.Reading.mixed, Santorio2018.Reading.everyBoth}

@[reducible, inline]

abbrev Santorio2018.someA : Finset Reading

Equations

• Santorio2018.someA = {Santorio2018.Reading.everyAK, Santorio2018.Reading.mixed, Santorio2018.Reading.everyBoth}

@[reducible, inline]

abbrev Santorio2018.someW : Finset Reading

Equations

• Santorio2018.someW = {Santorio2018.Reading.everyWP, Santorio2018.Reading.mixed, Santorio2018.Reading.everyBoth}

@[reducible, inline]

abbrev Santorio2018.someAorW : Finset Reading

∃(A ∨ W), which coincides with ∀(A ∨ W) on these five worlds.

Equations

• Santorio2018.someAorW = Santorio2018.everyAorW

def Santorio2018.readingAlts : List (Finset Reading)

The alternatives to (35): the universal and existential claims over A ∧ W, A, W, A ∨ W.

Equations

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

theorem Santorio2018.karenina_truthmakers : (truthmakers readingAlts everyAorW).toFinset = {everyA, everyW, someA ∩ someW}

(35) has three truthmakers: every student read AK, every student read W&P, and the mixed some read AK and some read W&P.

theorem Santorio2018.karenina_mixed_not_alonsoOvalle : Reading.mixed ∈ someA ∩ someW ∧ Reading.mixed ∉ everyA ∧ Reading.mixed ∉ everyW

The mixed truthmaker is realized where no universal alternative is: [AO09]'s disjunct alternatives {∀A, ∀W} miss the way for (35) to be true that makes (39) infelicitous.

Spain (8), on [McKVI77]

@[reducible, inline]

abbrev Santorio2018.axis : Finset McKayVanInwagen1977.SpainWorld

Equations

• Santorio2018.axis = Finset.filter McKayVanInwagen1977.foughtAxis Finset.univ

@[reducible, inline]

abbrev Santorio2018.allies : Finset McKayVanInwagen1977.SpainWorld

Equations

• Santorio2018.allies = Finset.filter McKayVanInwagen1977.foughtAllies Finset.univ

def Santorio2018.spainAlts : List (Finset McKayVanInwagen1977.SpainWorld)

The alternatives to Spain fought with the Axis or the Allies.

Equations

• Santorio2018.spainAlts = [Santorio2018.axis ∪ Santorio2018.allies, Santorio2018.axis, Santorio2018.allies, Santorio2018.axis ∩ Santorio2018.allies]

theorem Santorio2018.spain_collective : collectiveConditional McKayVanInwagen1977.spainSim spainAlts (axis ∪ allies) McKayVanInwagen1977.foughtAxis McKayVanInwagen1977.SpainWorld.actual ∧ ¬Semantics.Conditionals.Counterfactual.universalCounterfactual McKayVanInwagen1977.spainSim (fun (x : McKayVanInwagen1977.SpainWorld) => x ∈ allies) McKayVanInwagen1977.foughtAxis McKayVanInwagen1977.SpainWorld.actual

Collectively, (8) is true: the closest world where Spain fought with either is the Axis world. Strengthening the antecedent to the Allies makes it false — Antecedent Strengthening fails.

theorem Santorio2018.spain_not_distributive : ¬distributiveConditional McKayVanInwagen1977.spainSim spainAlts (axis ∪ allies) McKayVanInwagen1977.foughtAxis McKayVanInwagen1977.SpainWorld.actual

Distributively, (8) is false: the Allies truthmaker's counterfactual fails, so Simplification is not validated by the collective parsing.

theorem Santorio2018.spain_homogeneity : homogeneityPresup McKayVanInwagen1977.spainSim spainAlts (axis ∪ allies) McKayVanInwagen1977.foughtAxis McKayVanInwagen1977.SpainWorld.actual = Trivalent.indet

The homogeneity presupposition of the distributive parsing fails on (8).

Substitution of Logical Equivalents (57)–(58)

def Santorio2018.partySim : Semantics.Conditionals.SimilarityOrdering Party

Closeness for the party: the Anna-only world is closest to the actual world, then the world where both came, then Otto's.

Equations

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

@[reducible, inline]

abbrev Santorio2018.partyFun : Finset Party

The party was fun: only when Anna came alone.

Equations

• Santorio2018.partyFun = {Santorio2018.Party.annaOnly}

theorem Santorio2018.substitution_fails : anna = anna ∪ otto ∩ anna ∧ Semantics.Conditionals.Counterfactual.Distributive partySim [anna] (fun (x : Party) => x ∈ partyFun) Party.neither ∧ ¬Semantics.Conditionals.Counterfactual.Distributive partySim [anna, otto ∩ anna] (fun (x : Party) => x ∈ partyFun) Party.neither

(57) If Anna came, the party would be fun and (58) If Anna, or Otto and Anna, came, the party would be fun have logically equivalent antecedents, yet with the if-clauses denoting {Anna came} and {Anna came, Otto and Anna came} the distributive parsing makes (57) true and (58) false.