{I : Type u_1} {W : Type u_2} {access : I → Set W} {ord : I → Preorder W} {i : I} {p q : Set W} :
i ∈ Conditional.variablyStrictImp access ord p q ↔ q ∈ OrderingSemantics.necessityFilter (ord i) (access i ∩ p)
Lewis analyses the counterfactual as a variably strict conditional over comparative similarity:
if p, q holds when, as the accessible p-worlds come closer, the consequent eventually holds at
all of them, and if p, might q when it holds at some of them however close one comes. This file
takes as primitive the theory layer's conditional over an accessibility assignment and a family
of similarity preorders (Conditional.variablyStrictImp), which is membership in the filter of
necessities over the accessible antecedent-worlds, and derives the book's apparatus from it.
Lewis's systems of spheres are the sets of accessible worlds each closer than every accessible
world outside, and his truth condition by spheres is the primitive on a total preorder. Comparative
possibility by spheres is Lewis's lifting of the similarity order to the accessible
propositions, and the counterfactual is
definable from it. No strict
conditional makes two adjacent stages of a Sobel sequence true, and a variably strict one does.
Under the Limit Assumption the conditional is truth at the closest accessible antecedent-worlds;
without it, as for a line longer than an inch, the closest-world conditional is vacuously true of
every consequent while the variably strict one is not, and conditional excluded middle fails
although the ordering has no ties. Stalnaker's theory is the special case of a linear,
well-founded ordering, and conditional excluded middle at an antecedent is the filter being an
ultrafilter, which ties between closest worlds rule out. Lewis's axiomatization of the V-logics
with the counterfactual primitive is sound, its axioms being the laws of the filter, and every
theorem of Stalnaker's C2 holds under centering and Stalnaker's Assumption, while conditional
excluded middle is not a theorem of VC.
Implementation notes
Propositions are all sets of worlds, so Lewis's assumptions for every antecedent of the language are assumptions for every set. The conditions of §2.3 placing inaccessible worlds above the accessible ones enter by restricting antecedents to the accessible worlds.
The V-logics are stated over Stalnaker's formulas (Stalnaker1968.Formula), the corner read as
the counterfactual. The other operators are Lean definitions, so the axiom schema of definitions
holds by definition, and Deduction within Conditionals takes the conjunction of its premises as a
List.foldr. Centering is Conditional.IsCentered, stated over all worlds.
TODO
- The completeness of the V-logics (§6.1), and that every theorem of VCS is a theorem of Stalnaker's C2.
- The representation of set-selection functions (§2.7).
- Stalnaker's Assumption as a well-ordering of the accessible worlds (§3.4).
References
- Lewis 1973b, Counterfactuals
- Stalnaker 1968, A Theory of Conditionals formalized
Eventual and frequent truth
{W : Type u_2} {p q : Set W} {access : W → Set W} {ord : W → Preorder W} {w : W} :
w ∈ Conditional.might (Conditional.variablyStrictImp access ord) p q ↔ ∃ᶠ (v : W) in OrderingSemantics.necessityFilter (ord w) (access w ∩ p), v ∈ q
Systems of spheres
The spheres around i (§1.3) that comparative similarity determines (§2.3): the sets of
accessible worlds each closer to i than every accessible world outside.
- spheres access ord i = {S : Set W | S ⊆ access i ∧ ∀ j ∈ S, ∀ k ∈ access i, k ∉ S → j < k}
Used by mem_of_mem_spheres, isChain_spheres, sUnion_mem_spheres, sInter_mem_spheres, singleton_mem_spheres, setOf_le_mem_spheres, mem_variablyStrictImp_iff_spheres, forall_spheres_iff_lewis
{W : Type u_2} {access : W → Set W} {ord : W → Preorder W} {w : W} (hR : w ∈ access w) (hc : Conditional.IsCentered ord) :
{w} ∈ spheres access ord w
Built from
On a total preorder the accessible worlds at least as close as a given world form a sphere.
{I : Type u_1} {W : Type u_2} {access : I → Set W} {ord : I → Preorder W} {i : I} (htot : Std.Total LE.le) (j : W) :
{x : W | x ∈ access i ∧ x ≤ j} ∈ spheres access ord i
Built from
On a total preorder, if p, q holds when no sphere contains a p-world, or some sphere
contains one and q holds at every p-world in it (§1.3).
{I : Type u_1} {W : Type u_2} {access : I → Set W} {ord : I → Preorder W} {i : I} {p q : Set W} (htot : Std.Total LE.le) :
i ∈ Conditional.variablyStrictImp access ord p q ↔ (∀ S ∈ spheres access ord i, Disjoint S p) ∨ ∃ S ∈ spheres access ord i, (S ∩ p).Nonempty ∧ S ∩ p ⊆ q
Built from
Comparative possibility (§2.5)
On a total preorder Lewis's truth condition for comparative possibility, that every sphere
containing a q-world contains a p-world, says that the accessible p-worlds are at least as
possible as the accessible q-worlds under the similarity order (§2.5, p. 53).
{I : Type u_1} {W : Type u_2} {access : I → Set W} {ord : I → Preorder W} {i : I} {p q : Set W} (htot : Std.Total LE.le) :
(∀ S ∈ spheres access ord i, (S ∩ q).Nonempty → (S ∩ p).Nonempty) ↔ ComparativePossibility.Lewis LE.le (access i ∩ p) (access i ∩ q)
Built from
On a total preorder if p, q holds when no accessible world is a p-world or the p ∧ q
worlds are more possible than the p ∧ ¬q worlds, Lewis's definition of the counterfactual from
comparative possibility (§2.5, p. 53).
{I : Type u_1} {W : Type u_2} {access : I → Set W} {ord : I → Preorder W} {i : I} {p q : Set W} (htot : Std.Total LE.le) :
i ∈ Conditional.variablyStrictImp access ord p q ↔ access i ∩ p = ∅ ∨ AsymmRel (ComparativePossibility.Lewis LE.le) (access i ∩ p ∩ q) ((access i ∩ p) \ q)
Sobel sequences
If Otto had come it would have been lively; but if both Otto and Anna had come it would have been dreary (§1.2).
A strict conditional true of p and of p ∩ r with opposite consequents is true of p ∩ r
for every consequent: the stronger antecedent has no accessible worlds.
{I : Type u_1} {W : Type u_2} {access : I → Set W} {i : I} {p q r t : Set W} (h₁ : i ∈ Conditional.strictImp access p q) (h₂ : i ∈ Conditional.strictImp access (p ∩ r) qᶜ) :
i ∈ Conditional.strictImp access (p ∩ r) t
At 0, with Otto coming at 1 and 2, Anna at 2, and the party lively only at 1, if Otto
had come it would have been lively and not dreary, and if Otto and Anna had come it would have
been dreary and not lively.
Built from
The Limit Assumption
Lengths of a line, the actual one at most an inch, similar to the actual one as their lengths are close to it (§1.4).
Similarity of lengths by distance.
(w : ℝ) :
Preorder ℝ
- lineSim w = Preorder.lift fun (x : ℝ) => |x - w|
Used by minimals_lineSim, closestImp_line, not_mem_variablyStrictImp_line_two, mem_variablyStrictImp_line, not_cem_line
{a : ℝ} (ha : a ≤ 1) {x : ℝ} (hx : 1 < x) :
|x - a| = x - a
The conditional of the closest worlds makes if the line were over an inch long, it would be
q true of every q.
Built from
The variably strict conditional does not make if the line were over an inch long, it would be two inches long true.
{a : ℝ} (ha : a ≤ 1) :
a ∉ Conditional.variablyStrictImp (fun (x : ℝ) => Set.univ) lineSim (Set.Ioi 1) {2}
Built from
{a : ℝ} (ha : a ≤ 1) :
a ∈ Conditional.variablyStrictImp (fun (x : ℝ) => Set.univ) lineSim (Set.Ioi 1) (Set.Iio (3 / 2))
Built from
Conditional excluded middle at an antecedent is the filter of necessities over its accessible worlds being trivial or an ultrafilter.
{I : Type u_1} {W : Type u_2} {access : I → Set W} {ord : I → Preorder W} {i : I} {p : Set W} :
(∀ (q : Set W), i ∈ Conditional.variablyStrictImp access ord p q ∨ i ∈ Conditional.variablyStrictImp access ord p qᶜ) ↔ OrderingSemantics.necessityFilter (ord i) (access i ∩ p) = ⊥ ∨ IsAtom (OrderingSemantics.necessityFilter (ord i) (access i ∩ p))
Conditional excluded middle fails for the line although lengths over an inch are never tied: whether the length would be rational is settled by no closeness to the actual length.
{a : ℝ} (ha : a ≤ 1) :
(∀ x ∈ Set.Ioi 1, ∀ y ∈ Set.Ioi 1, x ≤ y → y ≤ x → x = y) ∧ a ∉ Conditional.variablyStrictImp (fun (x : ℝ) => Set.univ) lineSim (Set.Ioi 1) (Set.range Rat.cast) ∧ a ∉ Conditional.variablyStrictImp (fun (x : ℝ) => Set.univ) lineSim (Set.Ioi 1) (Set.range Rat.cast)ᶜ
Built from
Stalnaker's theory
Stalnaker's selection is Lewis's similarity with two further assumptions: the Limit Assumption, and that closest antecedent-worlds are never tied (§3.4).
Stalnaker's theory is a special case: on a centered similarity ordering that is linear and well-founded, the closest accessible antecedent-world is a selection function satisfying Stalnaker's conditions, and the variably strict conditional is truth at the world it selects.
{W : Type u_2} {p q : Set W} {access : W → Set W} {ord : W → Preorder W} (hR : ∀ (w : W), w ∈ access w) (hc : Conditional.IsCentered ord) (htot : ∀ (w : W), Std.Total LE.le) (hanti : ∀ (w : W), Std.Antisymm LE.le) (hwf : ∀ (w : W), WellFounded LT.lt) :
(Stalnaker1968.IsSelectionFunction access fun (w : W) (A : Set W) => (ord w).minimals (access w ∩ A)) ∧ Conditional.variablyStrictImp access ord p q = Conditional.ofDomain (fun (w : W) (A : Set W) => (ord w).minimals (access w ∩ A)) p q
{I : Type u_1} {W : Type u_2} {access : I → Set W} {ord : I → Preorder W} {i : I} {p : Set W} {v v' : W} (hv : v ∈ (ord i).minimals (access i ∩ p)) (hv' : v' ∈ (ord i).minimals (access i ∩ p)) (hne : v ≠ v') :
i ∉ Conditional.variablyStrictImp access ord p {v} ∧ i ∉ Conditional.variablyStrictImp access ord p {v}ᶜ
The V-logics with the counterfactual primitive
Lewis axiomatizes VC with the counterfactual primitive by Modus Ponens, Deduction within Conditionals and Interchange of Logical Equivalents, the tautologies, the definitions of the other operators, and axioms (3)–(7). VW drops (7), and VCS adds conditional excluded middle as (8) (§6.1). Axioms (3)–(5) and the rules hold on every total preorder. (3) and Deduction within Conditionals hold because the necessities over the antecedent-worlds form a filter containing them, (4) because an antecedent whose negation would imply it holds at every accessible world, and (5) because restricting an antecedent to a proposition possible over it restricts its filter to that proposition. (6) holds under weak centering, (7) under centering and (8) under Stalnaker's Assumption.
The proposition a formula expresses when its corner is read as the variably strict
conditional over access and ord.
{W : Type u_2} {α : Type u_3} (access : W → Set W) (ord : W → Preorder W) (V : α → Set W) :
Stalnaker1968.Formula α → Set W
- eval access ord V (Stalnaker1968.Formula.atom a) = V a
- eval access ord V A.neg = (eval access ord V A)ᶜ
- eval access ord V (A.imp B) = Conditional.materialImp (eval access ord V A) (eval access ord V B)
- eval access ord V (A.corner B) = Conditional.variablyStrictImp access ord (eval access ord V A) (eval access ord V B)
Used by eval_neg, mem_eval_imp, mem_eval_corner, eval_and, mem_eval_iff, Interchange.eval_eq, eval_eq_formula_eval
{W : Type u_2} {α : Type u_3} {access : W → Set W} {ord : W → Preorder W} {V : α → Set W} {w : W} {A B : Stalnaker1968.Formula α} :
w ∈ eval access ord V (A.corner B) ↔ eval access ord V B ∈ OrderingSemantics.necessityFilter (ord w) (access w ∩ eval access ord V A)
Built from
C' is C with some occurrences of A interchanged with B.
- refl {α : Type u_3} {A B : Stalnaker1968.Formula α} (C : Stalnaker1968.Formula α) : Interchange A B C C
- here {α : Type u_3} {A B : Stalnaker1968.Formula α} : Interchange A B A B
- neg {α : Type u_3} {A B C C' : Stalnaker1968.Formula α} : Interchange A B C C' → Interchange A B C.neg C'.neg
- imp {α : Type u_3} {A B C C' D D' : Stalnaker1968.Formula α} : Interchange A B C C' → Interchange A B D D' → Interchange A B (C.imp D) (C'.imp D')
- corner {α : Type u_3} {A B C C' D D' : Stalnaker1968.Formula α} : Interchange A B C C' → Interchange A B D D' → Interchange A B (C.corner D) (C'.corner D')
Used by Interchange.eval_eq, Provable
{W : Type u_2} {α : Type u_3} {access : W → Set W} {ord : W → Preorder W} {V : α → Set W} {A B C C' : Stalnaker1968.Formula α} (hAB : eval access ord V A = eval access ord V B) (h : Interchange A B C C') :
Built from ,
Lewis's V-logics VW, VC and VCS.
Used by VLogic.Holds, VLogic.Holds.mem, VLogic.Holds.le, VLogic.Holds.isCentered, Provable, Valid, Provable.sound
The conditions under which a V-logic is sound: weak centering for VW, centering for VC, and for VCS centering with Stalnaker's Assumption, a single closest accessible antecedent-world whenever there is an accessible one.
The definition is too large to print here; read it in the source.
Built from
Used by VLogic.Holds.mem, VLogic.Holds.le, VLogic.Holds.isCentered
The theorems of Lewis's axiomatization of a V-logic with the counterfactual primitive: the tautologies and axioms (3)–(6), with (7) except in VW and (8) in VCS, closed under Modus Ponens, Deduction within Conditionals and Interchange of Logical Equivalents.
- taut {α : Type u_3} {L : VLogic} {A : Stalnaker1968.Formula α} : A.IsTautology → Provable L A
- a3 {α : Type u_3} {L : VLogic} (φ : Stalnaker1968.Formula α) : Provable L (φ.corner φ)
- a4 {α : Type u_3} {L : VLogic} (φ ψ : Stalnaker1968.Formula α) : Provable L ((φ.neg.corner φ).imp (ψ.corner φ))
- a5 {α : Type u_3} {L : VLogic} (φ ψ χ : Stalnaker1968.Formula α) : Provable L ((φ.corner ψ.neg).or (((φ.and ψ).corner χ).iff (φ.corner (ψ.imp χ))))
- a6 {α : Type u_3} {L : VLogic} (φ ψ : Stalnaker1968.Formula α) : Provable L ((φ.corner ψ).imp (φ.imp ψ))
- a7 {α : Type u_3} {L : VLogic} (φ ψ : Stalnaker1968.Formula α) : L ≠ VLogic.VW → Provable L ((φ.and ψ).imp (φ.corner ψ))
- a8 {α : Type u_3} {L : VLogic} (φ ψ : Stalnaker1968.Formula α) : L = VLogic.VCS → Provable L ((φ.corner ψ).or (φ.corner ψ.neg))
- mp {α : Type u_3} {L : VLogic} {A B : Stalnaker1968.Formula α} : Provable L (A.imp B) → Provable L A → Provable L B
- deduction {α : Type u_3} {L : VLogic} (φ ψ χ : Stalnaker1968.Formula α) (χs : List (Stalnaker1968.Formula α)) : Provable L ((List.foldr Stalnaker1968.Formula.and χ χs).imp ψ) → Provable L ((List.foldr Stalnaker1968.Formula.and (φ.corner χ) (List.map φ.corner χs)).imp (φ.corner ψ))
- interchange {α : Type u_3} {L : VLogic} {A B C C' : Stalnaker1968.Formula α} : Provable L (A.iff B) → Interchange A B C C' → Provable L C → Provable L C'
Built from ,
Used by Provable.sound, not_provable_vc_cem
A formula is valid in a V-logic when it holds at every world of every interpretation over a total preorder satisfying the logic's conditions.
The definition is too large to print here; read it in the source.
Built from
Used by Provable.sound, valid_vcs_of_c2
The V-logics are sound.
Built from , ,
{W : Type u_2} {α : Type u_3} {access : W → Set W} {ord : W → Preorder W} {V : α → Set W} (hlim : ∀ (w : W) (B : Set W), (access w ∩ B).Nonempty → ((ord w).minimals (access w ∩ B)).Nonempty) (A : Stalnaker1968.Formula α) :
eval access ord V A = Stalnaker1968.Formula.eval (fun (w : W) (B : Set W) => (ord w).minimals (access w ∩ B)) V A
Built from
{W : Type u_2} {access : W → Set W} {ord : W → Preorder W} (hR : ∀ (w : W), w ∈ access w) (hc : Conditional.IsCentered ord) (htot : ∀ (w : W), Std.Total LE.le) (hS : ∀ (w : W) (p : Set W), (access w ∩ p).Nonempty → ∃ (v : W), (ord w).minimals (access w ∩ p) = {v}) :
Stalnaker1968.IsSelectionFunction access fun (w : W) (A : Set W) => (ord w).minimals (access w ∩ A)
Every theorem of Stalnaker's C2 is valid under centering and Stalnaker's Assumption.
Built from
Comparative similarity from w under which every other world is equally far.
(w : Fin 3) :
Preorder (Fin 3)
- tieSim w = Preorder.lift fun (v : Fin 3) => if v = w then 0 else 1
Conditional excluded middle is not a theorem of VC: two worlds tied for closest falsify both of its disjuncts (§3.4).
Built from