Santorio (2018): Alternatives and Truthmakers in Conditional Semantics

This file formalizes the paper's truthmaker semantics for conditionals. The paper 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. It 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 (Stable, MinimalStable, truthmakers). The conditional is a description of that set: with the optional distributivity operator it holds of each truthmaker, which is Simplification (distributiveConditional), and without it the modal would extracts the disjunctive closure, which is not (collectiveConditional); the operator 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 Alonso-Ovalle's disjunct alternatives cannot (karenina_truthmakers, karenina_mixed_not_alonsoOvalle), predicting the infelicity of (39). On McKay and van Inwagen's Spain case (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).

Implementation notes

The formalization is checked against the author's revised draft, whose example numbering the labels follow; the draft's definition of a truthmaker once says "maximal stable" where its text and its examples require minimal stability. The empty set of alternatives, stable whenever some world falsifies every alternative, is excluded from the minimal stable sets, as the paper's examples presuppose. Alternatives are given as propositions over a finite world type rather than generated from syntactic substitution sources.

References

• [San18b]
• [AO09]
• [McKVI77]

The stability algorithm (§5)

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

σ is stable with respect to the alternatives alts when 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 σ = { decide := decide (∃ a ∈ Finset.univ, (fun (w : W) => (∀ A ∈ σ, w ∈ A) ∧ ∀ A ∈ alts, A ∉ σ → w ∉ A) a), reflects_decide := ⋯ }

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

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

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 are 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.sup_truthmakers_subset {W : Type u_1} [DecidableEq W] [Fintype W] (alts : List (Finset W)) (S : Finset W) : (truthmakers alts S).toFinset.sup id ⊆ S

The union of the truthmakers is at most the antecedent.

Conditionals as descriptions (§6)

def Santorio2018.distributiveConditional {W : Type u_1} [DecidableEq W] [Fintype W] (ord : W → Preorder W) (alts : List (Finset W)) (S : Finset W) (C : Set W) (w : W) : Prop

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

Equations

• Santorio2018.distributiveConditional ord alts S C w = (w ∈ Conditional.distributiveImp ord (Santorio2018.truthmakers alts S).toFinset C)

def Santorio2018.homogeneityPresup {W : Type u_1} [DecidableEq W] [Fintype W] (ord : W → Preorder W) [(w : W) → DecidableRel LE.le] (alts : List (Finset W)) (S : Finset W) (C : Set W) [DecidablePred fun (x : W) => x ∈ C] (w : W) : SignType

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

Equations

• Santorio2018.homogeneityPresup ord alts S C w = Conditional.homogeneousImp ord (Santorio2018.truthmakers alts S).toFinset C w

def Santorio2018.collectiveConditional {W : Type u_1} [DecidableEq W] [Fintype W] (ord : W → Preorder W) (alts : List (Finset W)) (S : Finset W) (C : Set W) (w : W) : Prop

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

Equations

• Santorio2018.collectiveConditional ord alts S C w = (w ∈ Conditional.disjunctiveImp ord (Santorio2018.truthmakers alts S).toFinset C)

@[instance_reducible]

instance Santorio2018.instDecidableDistributiveConditional {W : Type u_1} [DecidableEq W] [Fintype W] (ord : W → Preorder W) [(w : W) → DecidableRel LE.le] (alts : List (Finset W)) (S : Finset W) (C : Set W) [DecidablePred fun (x : W) => x ∈ C] (w : W) : Decidable (distributiveConditional ord alts S C w)

Equations

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

@[instance_reducible]

instance Santorio2018.instDecidableCollectiveConditional {W : Type u_1} [DecidableEq W] [Fintype W] (ord : W → Preorder W) [(w : W) → DecidableRel LE.le] (alts : List (Finset W)) (S : Finset W) (C : Set W) [DecidablePred fun (x : W) => x ∈ C] (w : W) : Decidable (collectiveConditional ord alts S C w)

Equations

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

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)

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

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, since 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) are 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, so [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 = {x : McKayVanInwagen1977.SpainWorld | x ∈ McKayVanInwagen1977.foughtAxis}

@[reducible, inline]

abbrev Santorio2018.allies : Finset McKayVanInwagen1977.SpainWorld

Equations

• Santorio2018.allies = {x : McKayVanInwagen1977.SpainWorld | x ∈ McKayVanInwagen1977.foughtAllies}

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 ∧ McKayVanInwagen1977.SpainWorld.actual ∉ Conditional.closestImp McKayVanInwagen1977.spainSim (↑allies) McKayVanInwagen1977.foughtAxis

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

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

Distributively, (8) is false, since 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 = 0

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

Substitution of Logical Equivalents (57)–(58)

@[reducible, inline]

abbrev Santorio2018.partySim : Party → Preorder Party

Closeness for the party puts the Anna-only world 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.

@[instance_reducible]

instance Santorio2018.instDecidableRelPartyLe (w : Party) : DecidableRel LE.le

Equations

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

@[reducible, inline]

abbrev Santorio2018.partyFun : Finset Party

The party was fun holds only when Anna came alone.

Equations

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

theorem Santorio2018.substitution_fails : anna = anna ∪ otto ∩ anna ∧ Party.neither ∈ Conditional.distributiveImp partySim {anna} ↑partyFun ∧ Party.neither ∉ Conditional.distributiveImp partySim {anna, otto ∩ anna} ↑partyFun

(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.