Alternative-Sensitive Conditional Semantics #
@cite{santorio-2018}
Alternatives and truthmakers in conditional semantics. The Journal of Philosophy 115(10): 513--549.
Core Ideas #
- Conditional antecedents denote sets of propositions (alternatives), not single propositions
- Each alternative is evaluated separately against the closest worlds
- An optional DIST_π operator distributes the consequent over alternatives, carrying a homogeneity presupposition
- When DIST_π is present → SDA (Simplification of Disjunctive Antecedents)
- When DIST_π is absent → no SDA guarantee (the Spain/Axis reading)
Connection to Homogeneity #
DIST_π is structurally identical to DIST for plural individuals (@cite{kriz-2016}, @cite{tieu-kriz-chemla-2019}):
| Operator | Domain | TRUE | FALSE | GAP |
|---|---|---|---|---|
| DIST | atoms of a plurality | all satisfy P | none | mixed |
| DIST_π | alternatives of antecedent | all make C true | none | mixed |
Both are instances of the generic dist operator (Core/Logic/Truth3.lean).
Main Definitions #
altConditionalResults: per-alternative conditional evaluationhomogeneityEval: DIST_π applied to conditional alternatives (=dist)sdaEval/dcrEval: universal / existential resolutionslewisDAC: Lewis's Boolean-disjunction semantics (for contrast)IsTruthmaker: the truthmaker entailment relation (condition ii)satisfiable/isStable/isMinimalStable: the stability algorithm (§IV.2)conjunctiveClosure: conjunction of a subset of alternativesIsTruthmakerOf: full truthmaker definition (stability + entailment)
Key Theorems #
homogeneityEval_eq_dist: DIST_π = genericdistsda_is_universal_homogeneity: SDA ↔ homogeneity resolves to TRUEdcr_is_existential_homogeneity: DCR ↔ homogeneity does not resolve to FALSEspain_sda_fails/spain_lewis_true: SDA is optional without DIST_πantecedent_strengthening_fails: Constraint #1 (AS failure)hyperintensional/sle_fails: Constraint #3 (SLE failure)oa_otto_minimal/oa_anna_minimal: minimal stable subsets verifiedoa_otto_is_truthmaker/oa_anna_is_truthmaker: full truthmakers verified
Evaluate each alternative antecedent separately against closest worlds. Returns one Bool per alternative: true iff all closest worlds for that alternative satisfy the consequent.
Equations
- One or more equations did not get rendered due to their size.
Instances For
DIST_π (@cite{santorio-2018} §V): distribute the consequent over antecedent alternatives with a homogeneity presupposition.
⟦[if φ] DIST_π [would ψ]⟧ʷ = TRUE if ∀p ∈ Alt(φ) : min_w(p) ⊆ ⟦ψ⟧ FALSE if ∀p ∈ Alt(φ) : min_w(p) ⊆ ⟦¬ψ⟧ GAP otherwise (homogeneity failure)
This is dist applied to per-alternative conditional results,
making the structural parallel with plural DIST explicit.
Equations
- Semantics.Conditionals.AlternativeSensitive.homogeneityEval closer domain alts C w = Core.Duality.dist (Semantics.Conditionals.AlternativeSensitive.altConditionalResults closer domain alts C w)
Instances For
SDA reading: universal resolution of DIST_π (conjunction). "if A or B, C" is true iff BOTH (if A, C) and (if B, C).
Equations
- Semantics.Conditionals.AlternativeSensitive.sdaEval closer domain alts C w = (Semantics.Conditionals.AlternativeSensitive.altConditionalResults closer domain alts C w).all id
Instances For
DCR reading: existential resolution of DIST_π (disjunction). "if A or B, C" is true iff EITHER (if A, C) or (if B, C).
Equations
- Semantics.Conditionals.AlternativeSensitive.dcrEval closer domain alts C w = (Semantics.Conditionals.AlternativeSensitive.altConditionalResults closer domain alts C w).any id
Instances For
Lewis semantics: Boolean disjunction, not alternative-generating. "if A or B, C" evaluates min_w(A ∪ B) against C.
Equations
- One or more equations did not get rendered due to their size.
Instances For
DIST_π for conditionals = generic dist on per-alternative results.
SDA = homogeneity resolving to TRUE. The universal (SDA) reading is exactly the case where the truth-value gap does not arise.
DCR = homogeneity not resolving to FALSE. The existential (DCR) reading succeeds iff at least one alternative's conditional is true.
| Reading | Eval | Homogeneity condition |
|---|---|---|
| SDA | sdaEval | homogeneityEval == .true |
| DCR | dcrEval | homogeneityEval != .false |
Dual of sda_is_universal_homogeneity. Requires non-empty alternatives
(for [] : List Bool, any id = false but dist [] = .true).
SDA is optional — the Spain example #
Example (8) from @cite{santorio-2018} (p. 522; originally from @cite{mckay-vaninwagen-1977}): "If Spain had fought with the Axis or the Allies, she would have fought with the Axis." This conditional is acceptable WITHOUT implying (9): "If Spain had fought with the Allies, she would have fought with the Axis."
The non-SDA reading arises when DIST_π is absent (§V) — the modal takes the disjunctive closure of the antecedent alternatives directly.
This example also demonstrates Failure of Antecedent Strengthening (Constraint #1, p. 513): the Lewis reading of (8) is true, but strengthening to "If Allies, she'd fight Axis" makes it false.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Instances For
With DIST_π, SDA fails: the Allies simplification is false.
Homogeneity evaluation returns GAP (mixed results).
Without DIST_π, Lewis's disjunctive closure gives TRUE: the closest (Axis ∨ Allies)-world is the Axis-world, which satisfies C.
DCR reading gives TRUE: at least one alternative succeeds (the Axis simplification is true).
Failure of Antecedent Strengthening (Constraint #1, p. 513): the Lewis reading of (8) "if Axis or Allies, fought Axis" is true, but strengthening the antecedent to just "Allies" (which entails "Axis or Allies") reverses the truth value.
Hyperintensionality — Failure of SLE (@cite{santorio-2018} §VI) #
Logically equivalent antecedents can yield different conditional truth values because they generate different alternatives — and hence different truthmakers. This drops Substitution of Logical Equivalents (SLE) (Constraint #3, p. 514), making conditionals hyperintensional.
Together with Failure of Antecedent Strengthening (antecedent_strengthening_fails)
and optional SDA (spain_sda_fails / spain_lewis_true), this covers
all three constraints from the paper's introduction (pp. 513–514).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The antecedents are extensionally equivalent: annaCame ↔ annaCame ∨ ottoAndAnnaCame at every world.
Simple antecedent [annaCame]: TRUE. Closest annaCame-world is annaOnly; the party is fun there.
Disjunctive antecedent [annaCame, ottoAndAnnaCame]: FALSE. Closest ottoAndAnnaCame-world is both; the party is not fun there.
Hyperintensionality: logically equivalent antecedents with different alternatives yield different conditional truth values. This is Failure of SLE (Constraint #3, p. 514).
Substitution of Logical Equivalents fails: Constraint #3 from
@cite{santorio-2018} (p. 514). Alias for hyperintensional.
The Stability Algorithm (@cite{santorio-2018} §IV.2) #
The stability algorithm defines truthmakers from syntactic alternatives. Given ALT_S (the alternatives to sentence S):
- A subset σ ⊆ ALT_S is stable iff σ ∪ (ALT_S \ σ)⁻ is consistent (i.e., there exists a world satisfying all propositions in σ AND the negation of every alternative NOT in σ)
- σ is minimal stable iff stable, non-empty, and no non-empty proper subset is stable
- Truthmakers of S are ⋀σ for each minimal stable σ such that ⋀σ ⊨ S
The stability algorithm requires syntactic alternatives — generated by
@cite{katzir-2007} (formalized in
Theories/Semantics/Alternatives/Structural.lean) — to
compute ALT_S. The truthmakers then serve as the alternatives for
DIST_π evaluation (§V): each truthmaker is evaluated separately against
the closest worlds, and DIST_π distributes with a homogeneity
presupposition.
Duality with Fox's Innocent Exclusion #
Santorio's stability is the dual of @cite{fox-2007}'s innocent exclusion
(footnote 40, p. 540): minimal stable subsets correspond to maximal
consistent exclusions. This duality is computationally verified in
Section 9 below (stability_exclusion_duality, ie_from_stability).
Satisfiability: some world in the domain makes all propositions true.
Equations
- Semantics.Conditionals.AlternativeSensitive.satisfiable domain props = domain.any fun (w : W) => props.all fun (p : W → Bool) => p w
Instances For
Stability (p. 540): a subset σ (given by indices into alts) is stable
w.r.t. ALT_S iff σ together with the negation of every non-member
alternative is satisfiable.
σ ⊆ ALT_S is stable iff σ ∪ (ALT_S \ σ)⁻ ⊬ ⊥
Equations
- One or more equations did not get rendered due to their size.
Instances For
All sublists of a list (the power set). Used by both the stability algorithm (Santorio) and innocent exclusion (Fox).
Equations
Instances For
Minimal stability (p. 540): non-empty, stable, and no non-empty proper subset is stable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Conjunctive closure: the conjunction of all propositions at given indices. ⋀σ = λw. ∀i ∈ σ, altsi = true
Equations
- Semantics.Conditionals.AlternativeSensitive.conjunctiveClosure alts σ w = (List.filterMap (fun (i : ℕ) => alts[i]?) σ).all fun (p : W → Bool) => p w
Instances For
Entailment condition for truthmakers: p entails S. This is condition (ii) of the paper's definition (p. 540).
Equations
Instances For
Full truthmaker definition (p. 540): σ witnesses that its conjunctive closure is a truthmaker of S iff (i) σ is a minimal stable subset of ALT_S, and (ii) ⋀σ entails S.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Each disjunct is a truthmaker of the disjunction.
Conjunction of disjuncts is a truthmaker of the disjunction.
Worked Example: "Otto or Anna went to the party" #
Verifies the stability algorithm on the paper's central example (pp. 535–537).
- S = "Otto or Anna went to the party" = O ∨ A
- ALT_S = {O∨A, O, A, O∧A}
- Stable subsets: {O∨A, O}, {O∨A, A}, ALT_S
- Minimal stable: {O∨A, O} and {O∨A, A}
- Truthmakers: O (= ⋀{O∨A, O}) and A (= ⋀{O∨A, A})
The truthmakers are exactly the individual disjuncts — the "ways for
the disjunction to be true." These then feed into altConditionalResults
and homogeneityEval (DIST_π) for conditional evaluation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Instances For
{O∨A} alone is NOT stable (p. 536): no world satisfies O∨A ∧ ¬O ∧ ¬A ∧ ¬(O∧A).
{O∨A, O} IS stable (witness: ottoOnly satisfies O∨A ∧ O ∧ ¬A ∧ ¬(O∧A)).
{O∨A, A} IS stable (witness: annaOnly).
{O∨A, O∧A} is NOT stable: O∧A implies O∨A, but ¬O ∧ ¬A contradicts O∧A.
{O∨A, O} is MINIMAL stable: neither {O∨A} nor {O} alone is stable.
⋀{O∨A, O} = O (Otto went): the conjunctive closure reduces to the stronger conjunct.
⋀{O∨A, A} = A (Anna went).
O is a truthmaker of O∨A via the minimal stable subset {O∨A, O}: both conditions of the full definition (p. 540) are satisfied.
A is a truthmaker of O∨A via {O∨A, A}.
Fox–Santorio Duality #
@cite{santorio-2018} (footnote 40, p. 540) observes that his stability algorithm is the dual of @cite{fox-2007}'s innocent exclusion: where Fox finds maximal sets of alternatives that can consistently be excluded, Santorio finds minimal sets that can consistently be included (with the complement negated).
Concretely, for disjunction alternatives {p∨q, p, q, p∧q}:
| Santorio (minimal stable) | Fox (maximal consistent exclusion) |
|---|---|
| {p∨q, p} — include p, negate q,p∧q | {q, p∧q} — exclude q, p∧q |
| {p∨q, q} — include q, negate p,p∧q | {p, p∧q} — exclude p, p∧q |
The complement of each minimal stable subset (restricted to the non-weaker alternatives NW) equals a maximal consistent exclusion. This section verifies the duality computationally on both algorithms.
The two minimal stable subsets of the disjunction alternatives. Each includes the prejacent (index 0) plus one disjunct.
Fox's maximal consistent exclusions for p∨q.
Duality verified: the complement (in NW) of each minimal stable subset equals the corresponding maximal consistent exclusion.
- minStable {0,2}: NW \ {2} = {1,3} = MCE₂
- minStable {0,1}: NW \ {1} = {2,3} = MCE₁
The innocently excludable alternatives (Fox) are exactly those NOT in ANY minimal stable subset beyond the prejacent (Santorio).
Fox: I-E = {3} (= p∧q) Santorio: ⋃(minStable ∩ NW) = {1, 2} (= p, q) Complement: NW \ {1,2} = {3} = I-E