Santorio 2018 — Alternative-Sensitive Conditional Semantics #
@cite{santorio-2018}
Self-contained formalization of Alternatives and truthmakers in conditional semantics, The Journal of Philosophy 115(10): 513–549.
Substrate consumption #
Built on Conditionals.Counterfactual.universalCounterfactual (the
canonical @cite{lewis-1973}/Kratzer universal counterfactual operator)
and on Truthmaker.ExactEntails (= ≤ on TMProp,
Truthmaker/Inexact.lean). Predicates are typed Prop with
DecidablePred instances throughout — no Bool-vs-Prop adapters. The
per-alternative apparatus uses DecAlt W := Σ' A : W → Prop, DecidablePred A to bundle decidability with each alternative
predicate.
Sections #
- §1 Per-alternative evaluation (
altConditionalResults) - §2 DIST_π and its resolutions (
homogeneityEval,sdaEval,disjunctiveCounterfactual= "would" extracts ⋁S, p. 547) - §3 Structural theorems
- §4 Lewis bridge (alias to
universalCounterfactualon disjunctive closure) - §5 Truthmakers (
IsTruthmaker := ExactEntailsdirectly) - §6 Stability algorithm (§IV.2 p. 540):
isConsistent,isStable,isMinimalStable,conjunctiveClosure,IsTruthmakerOf - §7 Generic truthmaker lemmas
- §8 Hyperintensionality / SLE failure (§VI)
- §9 Otto/Anna stability worked example (pp. 535–537)
- §10 Spain analysis on top of @cite{mckay-vaninwagen-1977} data
- §11 Cross-framework: Santorio classical truthmaker ≠ @cite{jago-2026} Fine-style content parthood
Faithfulness notes #
DIST_π trivalent rendering. Santorio's own DIST_π is bivalent-with-presupposition (p. 547). Footnote 52 p. 545 explicitly declines the trivalent collapse: "To switch to a Križ-style framework, we would need to divorce homogeneity from the distributivity operator and move to a trivalent semantics." We render DIST_π via
Core.Duality.Truth3/distListbecause it is ergonomic and faithful on the all/none/mixed verdicts; the divergence is in how the homogeneity failure is typed (gap vs. presupposition failure).Two readings, not three. Santorio's binary architecture is SDA (with DIST_π) vs. asymmetric/Lewis (without DIST_π — modal extracts the disjunctive closure, p. 547). The "DCR" (Disjunctive Conditional Reading) is not Santorio's term; it is named in @cite{zani-ciardelli-sanfelici-2026} (p. 10) and lives in that file.
Stability non-emptiness. Santorio's definition (p. 540) does not include a non-empty clause; he discharges the empty-σ case via the entailment condition (ii) of the truthmaker definition (since
⋀∅ = ⊤does not entail typical S). Theσ.length > 0clause inisMinimalStablehere is a Lean-side convenience yielding the same truthmaker set.Fox–Santorio relationship (footnote 40 p. 540). Santorio observes that minimal stability is "something like the converse" of @cite{fox-2007}'s maximal exclusion (note: not innocent exclusion, which is the intersection of maximals). He does not say "dual" and hedges. The general theorem
santorio_minimal_stable_dual_to_fox_maximal_exclusionis not formalised; it requires either a witness-typedIsMaximalExclusionpredicate inTheories/Semantics/Exhaustification/Innocent.lean(which currently exposesIE/innocentlyExcludableoverFinset (Finset W)) or aFinset Nat ↔ List Natreflection.Stability terminology. Santorio writes
σ ∪ (ALT_S − σ)⁻ ⊭ ⊥("consistent with the negation of every alternative", p. 540); this file inlines the consistency check directly intoisStablerather than expose a separateisConsistentpredicate.disjunctiveCounterfactualandwould(p. 547). The DIST_π-absent reading is named for the modalwould, which "extracts the disjunctive closure"⋁Sof the alternative set. We name the operatordisjunctiveCounterfactualrather thanlewisDACbecause p. 547 places this move in the lexical entry ofwould, not in Lewis's metatheory.
Future work (load-bearing Santorio content not yet formalized) #
- §II.2 Raffle / probability-operator argument (pp. 525–527) —
Santorio's central anti-scalar argument. Requires a probability
operator scoping over a counterfactual;
Theories/Semantics/Conditionals/has no such operator at present. - §II.3 Otto/Anna/Waldo non-closest-worlds (pp. 527–530) —
refutes minimal-change. Requires a
WaldoWorldenum with a tied- closest-worlds similarity ordering. - §IV.3 Karenina/W&P 8-alternative example (p. 538) — shows Santorio's stability algorithm is global (not local), distinguishing it from Alonso-Ovalle 2009 (no bib entry yet).
- §V full lexical entries (p. 547) — typed entries for
if,would, DIST_π. Requires typed-LF infrastructure.
Citations engaged in the formalization #
@cite{lewis-1973} (universal counterfactual substrate),
@cite{kratzer-1981} / @cite{kratzer-1991} / @cite{kratzer-2012}
(premise/restrictor semantics, sibling no-SDA tradition),
@cite{katzir-2007} (structural alternative generation, source of ALT_S),
@cite{kriz-spector-2021} (homogeneity-style trivalent option declined
by fn 52 p. 545), @cite{chierchia-2013} (domain alternatives, fn 40
p. 540), @cite{cariani-goldstein-2020} (sibling homogeneity account,
see CarianiGoldstein2020.lean), @cite{mckay-vaninwagen-1977} (Spain
data, §10), @cite{jago-2026} (Fine-style truthmaker contrast, §11).
Santorio also engages Alonso-Ovalle 2009 (§III precursor, no bib
entry yet), Klinedinst (scalar account refuted in §II, no bib entry
yet), Schlenker 2004 ("Conditionals as Definite Descriptions" — the
fn 24/47 descriptions analogy), and van Fraassen 1969 (truthmaker
ancestor, fn 41) — adding these to references.bib is a bib-hygiene
follow-up.
Decidability-bundled alternatives #
A propositional alternative on W paired with its decidability
witness. Used as the element type of alternative lists (List (DecAlt W))
so that per-alternative decide calls compose without per-element
typeclass synthesis.
Equations
- Phenomena.Conditionals.Studies.Santorio2018.DecAlt W = ((A : W → Prop) ×' DecidablePred A)
Instances For
Equations
- a.instDecidablePredPred = a.snd
Evaluate each alternative antecedent separately against closest
worlds via universalCounterfactual. 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_π (§V): distribute the consequent over antecedent
alternatives with a homogeneity presupposition. Rendered as dist
over per-alternative conditional results (faithfulness note 1).
Equations
- One or more equations did not get rendered due to their size.
Instances For
SDA reading (Simplification of Disjunctive Antecedents): universal resolution of DIST_π. "If A or B, C" is true iff every alternative simplification (if A, C) holds.
Equations
- Phenomena.Conditionals.Studies.Santorio2018.sdaEval sim alts C w = ((Phenomena.Conditionals.Studies.Santorio2018.altConditionalResults sim alts C w).all id = true)
Instances For
Equations
sdaEval unfolds to universal quantification over per-alternative
conditionals — Santorio's intended Simplification reading.
Disjunctive closure of an alternative set: ⋁S = λw. ∃A ∈ S, A w.
Per §V p. 547, the lexical entry for would extracts this when
DIST_π is absent.
Equations
- Phenomena.Conditionals.Studies.Santorio2018.disjunctiveClosure alts w = ∃ a ∈ alts, a.pred w
Instances For
Equations
- Phenomena.Conditionals.Studies.Santorio2018.instDecidablePredDisjunctiveClosure alts x✝ = inferInstance
DIST_π-absent reading (§V p. 547): the modal would extracts
the disjunctive closure of the alternatives, evaluating min_w(⋁S)
against C. Reduces to @cite{lewis-1973}'s universal counterfactual
on the disjunctive closure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
SDA = homogeneity resolves to TRUE.
disjunctiveCounterfactual IS @cite{lewis-1973}'s universal
counterfactual on the disjunctive closure of the alternatives.
Definitionally true; named for explicit cross-framework consumption.
Entailment condition for truthmakers: p entails S.
Defined directly as Truthmaker.ExactEntails from
Truthmaker/Inexact.lean (= ≤ on TMProp). Santorio is explicit
(p. 515) that his truthmakers are "cognitive rather than
metaphysical" and determined by syntactic alternatives, so the
classical world-extensional formulation is faithful.
The Up clause that distinguishes Fine's IsContentPart from this
Down-only relation is not part of Santorio's notion; the
inequivalence with Fine is refuted in
santorio_truthmaker_neq_fine_content_part below.
Equations
Instances For
Stability (p. 540): a subset σ (given by indices into alts) is
stable iff some world satisfies every in-σ alternative AND falsifies
every out-of-σ alternative. (Santorio's σ ∪ (ALT_S − σ)⁻ ⊭ ⊥,
"consistent" in his prose p. 540.)
Equations
- Phenomena.Conditionals.Studies.Santorio2018.isStable alts σ = ∃ (w : W), (∀ (i : ℕ) (h : i < alts.length), i ∈ σ → alts[i].pred w) ∧ ∀ (i : ℕ) (h : i < alts.length), i ∉ σ → ¬alts[i].pred w
Instances For
Equations
- Phenomena.Conditionals.Studies.Santorio2018.instDecidableIsStable alts σ = id inferInstance
Minimal stability (p. 540): non-empty (Lean-side, faithfulness note 3), stable, and no non-empty proper subset is stable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Phenomena.Conditionals.Studies.Santorio2018.instDecidableIsMinimalStable alts σ = id inferInstance
Conjunctive closure: ⋀σ = λw. ∀i ∈ σ, altsi.
Equations
- Phenomena.Conditionals.Studies.Santorio2018.conjunctiveClosure alts σ w = ∀ (i : ℕ) (h : i < alts.length), i ∈ σ → alts[i].pred w
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.
- minimal_stable : isMinimalStable alts σ
Condition (i): σ is a minimal stable subset of ALT_S.
- closure_entails : IsTruthmaker (conjunctiveClosure alts σ) S
Condition (ii): ⋀σ entails S (the truthmaker entailment).
Instances For
Each disjunct is a truthmaker of the disjunction.
Conjunction of disjuncts is a truthmaker of the disjunction.
Logically equivalent antecedents can yield different conditional truth values because they generate different alternatives. This drops Substitution of Logical Equivalents (SLE) (Constraint #3 p. 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.
Hyperintensionality / SLE Failure (Constraint #3 p. 514).
S = "Otto or Anna went to the party" = O ∨ A. ALT_S = {O∨A, O, A, O∧A} (p. 536). Stable: {O∨A, O}, {O∨A, A}, ALT_S. Minimal stable: {O∨A, O}, {O∨A, A}. Truthmakers: O and A (p. 537).
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.
Per CLAUDE.md "chronological dependency": this 2018 study consumes @cite{mckay-vaninwagen-1977}'s 1977 data (worlds, similarity ordering, disjunct predicates).
@cite{santorio-2018}'s homogeneity verdict on the
@cite{mckay-vaninwagen-1977} Spain scenario: .indet (mixed
results across the two alternatives), demonstrating the Truth3
middle column.
@cite{santorio-2018}'s SDA verdict on the same scenario: FALSE (the Allies simplification fails).
@cite{santorio-2018}'s IsTruthmaker is ExactEntails from
Truthmaker/Inexact.lean (the Down clause only). Fine-style
IsContentPart adds the Up clause: every part of the truthmade
proposition extends to a part of the truthmaker. The two relations are
non-equivalent.
Santorio truthmaker ≠ Fine content parthood: there exist
propositions p, S such that Santorio's classical truthmaker
relation (= ExactEntails) holds but Fine's IsContentPart (Down
- Up) fails. Witness: over
Natwith the usual order, takep = (· = 5)andS = (· < 10).
@cite{santorio-2018}'s introduction (pp. 513–514) lists three constraints on classical counterfactual logic that the paper refutes:
- Constraint #1: Antecedent Strengthening —
(A □→ C) ⊨ (A ∧ B) □→ C - Constraint #2: Simplification of Disjunctive Antecedents (SDA) —
(A ∨ B) □→ C ⊨ A □→ C ∧ B □→ C - Constraint #3: Substitution of Logical Equivalents (SLE)
The Spain analysis (§10) refutes Constraint #1 via
@cite{mckay-vaninwagen-1977} data; sle_fails (§8) refutes
Constraint #3. Constraint #2 is engaged throughout (it IS the central
phenomenon under DIST_π) — the theorem below states it as a structural
witness anchored to the named constraint.
Constraint #2 = SDA: under DIST_π, the alternative-sensitive
semantics validates SDA. If the per-alternative SDA-evaluation
holds, then each individual simplification holds. Direct
consequence of sdaEval_iff_forall.
Per CLAUDE.md "no bridge files": cross-framework contrasts go inside the chronologically-later study. Santorio 2018 is the latest of {Lewis 1973, Stalnaker 1968, Kratzer 1981, McKay & Van Inwagen 1977} that this file engages, so the divergence theorems live here.
Santorio vs. Alonso-Ovalle on Karenina/W&P (§IV.3 pp. 537–539) #
For the prejacent (35) "Every student read War and Peace or Anna Karenina", @cite{santorio-2018}'s stability algorithm (running on Katzir-generated 8-alternative ALT_S, eqn (48) p. 538) identifies three minimal-stable subsets, each yielding one truthmaker:
- σ₁ = {∀(A), ∀(A∨W), ∃(A), ∃(A∨W)} → "every student read AK"
- σ₂ = {∀(W), ∀(A∨W), ∃(W), ∃(A∨W)} → "every student read W&P"
- σ₃ = {∀(A∨W), ∃(A), ∃(W), ∃(A∨W)} → "some students read AK and some students read W&P" (the mixed truthmaker)
@cite{alonso-ovalle-2009}'s pointwise computation (running only on
the disjunct alternatives {∀(A), ∀(W)} per his Or Rule (10) p. 212)
identifies only two truthmakers (the universals); the mixed
truthmaker is invisible to AO's local algorithm.
@cite{santorio-2018}'s example (39) p. 539: "If every student read AK or W&P, the world would be a better place. But if some students read AK and some read W&P, the world would not be a better place." is felicitous ONLY if the second clause's antecedent is a truthmaker of the first clause's antecedent — which it is on Santorio's algorithm but not on AO's. Hence Santorio: "a theory based on the stability algorithm has an empirical advantage over Hamblin-style semantics" (p. 539).
KareninaWorld enumerates the 5 worlds needed to evaluate the 8
alternatives. The mixed truthmaker is realized at .mixed.
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.
Alternative predicates per @cite{santorio-2018} (48) p. 538 #
The three minimal-stable subsets (p. 539) #
Truthmaker realizations #
The AK-truthmaker is realized at .everyAK (and at .everyBoth).
The W&P-truthmaker is realized at .everyWP (and at .everyBoth).
The mixed truthmaker is realized at .mixed — the load-bearing
fact distinguishing @cite{santorio-2018} from
@cite{alonso-ovalle-2009}. At .mixed, every student reads at
least one book, some students read AK, some students read W&P, and
no student reads both.
The cross-framework theorem #
Santorio finds the mixed truthmaker; Alonso-Ovalle 2009 cannot.
@cite{alonso-ovalle-2009}'s alternative set for the prejacent
"every student read AK or W&P" is just the two disjunct universals
{∀(A), ∀(W)} (from the Hamblin Or Rule (10) p. 212 plus the
universal force §2.2.3 p. 218). At the .mixed world neither AO
alternative holds. But @cite{santorio-2018}'s kareninaSigmaMixed
truthmaker IS realized at .mixed. AO's pointwise alternative
generation thus undergenerates the truthmaker set: the mixed-
reading way for the antecedent to be true is invisible to AO but
visible to Santorio. This is the empirical advantage Santorio
claims at p. 539.
Santorio vs. von Fintel/Križ on Spain. The two homogeneity moves differ on cross-alternative aggregation:
- Santorio per-alternative homogeneity over
[foughtAxis, foughtAllies]yields.indet(mixed verdicts: Axis simplification true, Allies simplification false). - Von Fintel/Križ-style
homogeneityCounterfactualon the disjunctive antecedent(foughtAxis ∨ foughtAllies)finds the closest such world (the Axis-world, byspainSim's priority), checks foughtAxis-homogeneity over closest worlds (trivially satisfied — single closest world), and returnspresupposition := .satisfied.
The two operators thus deliver different verdicts on the same scenario: Santorio's homogeneity gap is at the cross-alternative level, von Fintel/Križ's is at the within-closest-world level. Both are "homogeneity," but at different scopes.