Lewis (1981): Ordering semantics and premise semantics for counterfactuals

This file formalizes [Lew81]'s equivalence of two ways of letting factual background settle the truth of a counterfactual. An ordering frame assigns to each world a set of worlds, its field, and an ordering of them by how little they differ from it, and a counterfactual is true when its consequent holds at the closest antecedent-worlds (truth condition OF, the library's orderingImp). A premise frame assigns to each world a set of premises, and a counterfactual is true when every nonempty maximal set of premises consistent with the antecedent implies the consequent together with it (truth condition PF, the premise semantics of [Kra81a] up to the word nonempty). A premise frame induces an ordering frame on the worlds where some premise holds, one world closer than another when it satisfies every premise the other satisfies, and the two frames evaluate every counterfactual alike (premiseImp_eq_orderingImp, §4). Every ordering frame is induced in this way, by the premises that say a world is at least as close as some world of the field (orderingImp_eq_premiseImp), so the correspondence exhausts both classes of frames.

Section 6 replaces OF by a truth condition that needs neither the Limit Assumption nor comparability: every antecedent-world of the field has one at least as close, all of whose antecedent-worlds at least as close are consequent-worlds (neutralImp), the necessity of ordering semantics over the antecedent-worlds of the field. It entails OF (neutralImp_subset_orderingImp), follows from OF under the Limit Assumption (orderingImp_subset_neutralImp), and on a universal frame is [Lew73b]'s truth condition under comparability (neutralImp_univ_eq_variablyStrictImp).

Main definitions

• Lewis1981.premiseImp: truth condition PF of a premise frame.
• Lewis1981.premiseOrder: the ordering a premise frame induces.
• Lewis1981.ofOrdering: the premise frame an ordering frame induces.
• Lewis1981.neutralImp: the neutral truth condition O of §6.

Main results

• Lewis1981.premiseImp_eq_orderingImp: a premise frame and the ordering frame it induces evaluate every counterfactual alike.
• Lewis1981.orderingImp_eq_premiseImp: every ordering frame is induced by a premise frame.
• Lewis1981.neutralImp_subset_orderingImp, Lewis1981.orderingImp_subset_neutralImp, Lewis1981.neutralImp_univ_eq_variablyStrictImp: the neutral truth condition reduces to OF under the Limit Assumption and to [Lew73b]'s under comparability.

Implementation notes

• Lewis's orderings are strict partial orders of their fields; the library's are preorders on all worlds, the field entering as the accessibility argument of orderingImp. Preorders allow ties, which a strict ordering cannot tell from incomparabilities, and the proofs do not need antisymmetry.
• Neither Centering nor finiteness is assumed: §7 notes that the equivalence results do not depend on Centering, and §6 that they carry over to the infinite case.
• Section 5's reconciliation of partial with total orderings, truth on an ordering being truth on every refinement to a total one, is Conditional.mem_closestImp_iff_forall_compatible for the refinements [Sta81] calls completions.

TODO

• Section 6's neutral truth condition for premise frames and its equivalence with neutralImp.
• Section 6's example of a counterfactual true under the neutral condition on a frame and false on one of its refinements.

References

• D. Lewis, Ordering Semantics and Premise Semantics for Counterfactuals (1981)
• A. Kratzer, Partition and Revision: The Semantics of Counterfactuals (1981)
• A. Kratzer, Conditional Necessity and Possibility (1979)
• D. Lewis, Counterfactuals (1973)
• R. C. Stalnaker, A Defense of Conditional Excluded Middle (1981)

Premise frames (§3)

def Lewis1981.IsConsistentPremiseSet {W : Type u_1} (H : W → Set (Set W)) (A : Set W) (i : W) (J : Set (Set W)) : Prop

An A-consistent premise set for i: a set of premises for i consistent with A.

Equations

• Lewis1981.IsConsistentPremiseSet H A i J = (J ⊆ H i ∧ (A ∩ ⋂₀ J).Nonempty)

def Lewis1981.premiseImp {W : Type u_1} (H : W → Set (Set W)) (A C : Set W) : Set W

Truth condition PF holds when every nonempty maximal A-consistent premise set for i implies C together with A.

Equations

• Lewis1981.premiseImp H A C = {i : W | ∀ (J : Set (Set W)), Maximal (Lewis1981.IsConsistentPremiseSet H A i) J → J.Nonempty → A ∩ ⋂₀ J ⊆ C}

@[reducible, inline]

abbrev Lewis1981.premiseOrder {W : Type u_1} (H : W → Set (Set W)) (i : W) : Preorder W

In the ordering a premise frame induces at i, j is at least as close as k when every premise for i that holds at k holds at j.

Equations

• Lewis1981.premiseOrder H i = Preorder.ofCriteria (fun (x1 : W) (x2 : Set W) => x1 ∈ x2) (H i)

Equivalence of frames (§4)

theorem Lewis1981.premiseImp_eq_orderingImp {W : Type u_1} {H : W → Set (Set W)} {A C : Set W} : premiseImp H A C = Conditional.orderingImp (fun (i : W) => ⋃₀ H i) (premiseOrder H) A C

A premise frame and the ordering frame it induces, on the worlds where some premise holds, evaluate every counterfactual alike. For an antecedent-world j, the premises that hold at j form a nonempty maximal consistent premise set exactly when j is a closest antecedent-world.

def Lewis1981.ofOrdering {W : Type u_1} (S : W → Set W) (ord : W → Preorder W) (i : W) : Set (Set W)

In the premise frame an ordering frame induces, the premises for i say that a world of the field is at least as close as some given world of it.

Equations

• Lewis1981.ofOrdering S ord i = (fun (k : W) => {j : W | j ∈ S i ∧ j ≤ k}) '' S i

theorem Lewis1981.orderingImp_eq_premiseImp {W : Type u_1} {A C : Set W} (S : W → Set W) (ord : W → Preorder W) : Conditional.orderingImp S ord A C = premiseImp (ofOrdering S ord) A C

Every ordering frame is induced by a premise frame, so the correspondence of §4 exhausts both classes of frames.

Surplus information (§4)

Two premise frames can induce the same strict ordering, and so evaluate every counterfactual alike, while differing on whether two worlds are tied or incomparable. Of three worlds 0, 1, 2, premises {0} and {0, 1, 2} for 0 tie 1 and 2, and premises {0, 1} and {0, 2} make them incomparable.

def Lewis1981.tied : Fin 3 → Set (Set (Fin 3))

Premises {0} and {0, 1, 2}.

Equations

• Lewis1981.tied x✝ = {{0}, {0, 1, 2}}

def Lewis1981.split : Fin 3 → Set (Set (Fin 3))

Premises {0, 1} and {0, 2}.

Equations

• Lewis1981.split x✝ = {{0, 1}, {0, 2}}

theorem Lewis1981.premiseOrder_tied_ne_split : premiseOrder tied 0 ≠ premiseOrder split 0

The two frames order 1 and 2 differently from 0, as tied and as incomparable.

theorem Lewis1981.premiseImp_tied_iff_split (A C : Set (Fin 3)) : 0 ∈ premiseImp tied A C ↔ 0 ∈ premiseImp split A C

The two frames evaluate every counterfactual at 0 alike.

The neutral truth condition (§6)

def Lewis1981.neutralImp {W : Type u_1} (S : W → Set W) (ord : W → Preorder W) (A C : Set W) : Set W

Truth condition O holds when every antecedent-world h of the field has an antecedent-world j of the field at least as close, all of whose antecedent-worlds of the field at least as close are consequent-worlds. It is necessity in ordering semantics over the antecedent-worlds of the field.

Equations

• Lewis1981.neutralImp S ord A C = {i : W | OrderingSemantics.IsNecessity (ord i) (S i ∩ A) C}

theorem Lewis1981.neutralImp_subset_orderingImp {W : Type u_1} {A C : Set W} {S : W → Set W} {ord : W → Preorder W} : neutralImp S ord A C ⊆ Conditional.orderingImp S ord A C

The neutral truth condition entails OF.

theorem Lewis1981.orderingImp_subset_neutralImp {W : Type u_1} {A C : Set W} {S : W → Set W} {ord : W → Preorder W} {i : W} (hlim : ∀ (B : Set W), (S i ∩ B).Nonempty → ((ord i).minimals (S i ∩ B)).Nonempty) (hi : i ∈ Conditional.orderingImp S ord A C) : i ∈ neutralImp S ord A C

Under the Limit Assumption OF entails the neutral truth condition.

theorem Lewis1981.neutralImp_univ_subset_variablyStrictImp {W : Type u_1} {A C : Set W} {ord : W → Preorder W} : neutralImp (fun (x : W) => Set.univ) ord A C ⊆ Conditional.variablyStrictImp ord A C

On a universal frame the neutral truth condition entails [Lew73b]'s.

theorem Lewis1981.neutralImp_univ_eq_variablyStrictImp {W : Type u_1} {A C : Set W} {ord : W → Preorder W} (htot : ∀ (w : W), Std.Total LE.le) : neutralImp (fun (x : W) => Set.univ) ord A C = Conditional.variablyStrictImp ord A C

On a universal frame satisfying comparability the neutral truth condition is [Lew73b]'s.