Restrictor Theory of Conditionals #
@cite{kratzer-1986} @cite{kratzer-2012}
Kratzer's restrictor analysis: if-clauses restrict the modal domain rather than functioning as binary connectives. "If α, (must) β" is analyzed as modal necessity/possibility over the modal base restricted by α.
This module bridges Conditionals/Basic.lean and Modality/Kratzer.lean,
deriving conditional truth conditions from modal restriction.
Core Thesis #
If-clauses are not propositional connectives. They are restrictors of the modal base. "If it rains, the streets are wet" does not express a binary relation between two propositions. Instead, "if it rains" restricts the modal base to rain-worlds, and the (possibly covert) necessity operator quantifies over the best of those worlds.
Key Result #
restrictor_eq_strict: with empty ordering source, Kratzer's conditional
necessity (∀w' ∈ Best(f+α, ∅, w). β(w')) equals the strict conditional
(∀w' ∈ ∩f(w). α(w') → β(w')) from Conditionals/Basic.lean. This is the
core bridge connecting the two currently-independent modules.
Helper #
Core definitions #
If α, must β under the restrictor analysis: necessity over the α-restricted modal base.
⟦if α, must β⟧(w) = ∀w' ∈ Best(f+α, g, w). β(w')
Equations
Instances For
If α, might β under the restrictor analysis: possibility over the α-restricted modal base.
⟦if α, might β⟧(w) = ∃w' ∈ Best(f+α, g, w). β(w')
Equations
Instances For
Structural lemma #
Restricted accessible worlds = α-worlds within the original accessible worlds.
This is the foundational decomposition: restricting the modal base by α and then computing accessibility is the same as computing accessibility first and then filtering by α.
Main bridge theorems #
Restrictor = Strict conditional (the core bridge theorem).
With empty ordering source, "if α, must β" (restrictor analysis from
Kratzer.lean) equals "□_f(α → β)" (strict conditional from
Conditionals/Basic.lean).
∀w' ∈ Best(f+α, ∅, w). β(w') ⟺ ∀w' ∈ ∩f(w). α(w') → β(w')
This connects Modality/Kratzer.lean to Conditionals/Basic.lean.
Kratzer's materialImplication equals materialImpB from
Conditionals/Basic.lean — the two modules defined the same operation
independently.
Properties #
Conditional duality: "if α, must β" ↔ ¬"if α, might ¬β".
Vacuous conditional: if no accessible worlds satisfy α, conditional necessity holds vacuously (for any β and any ordering source).
Material conditional as degenerate case: with totally realistic base and empty ordering, "if α, must β" reduces to material implication.
When ∩f(w) = {w} and g = ∅, the restrictor conditional collapses to the classical truth-functional conditional ¬α(w) ∨ β(w).
Restrictor monotonicity: if α₂ entails α₁, then the α₂-restricted base is contained in the α₁-restricted base. Stronger antecedents yield fewer accessible worlds.
Double restriction: restricting by α₁ then α₂ equals restricting by (α₁ ∧ α₂). Grounds iterated conditionals:
"if α₁, if α₂, must β" = "if (α₁ ∧ α₂), must β"
Restrictor strengthening: adding a restrictor α to a modal base can only shrink (or preserve) the set of accessible worlds.
Conditional K axiom: conditional necessity distributes over material implication.
If (if α, must (β → γ)) and (if α, must β), then (if α, must γ).