The modal-horizon counterfactual

On von Fintel's dynamic strict analysis, a counterfactual quantifies over a modal horizon, a set of worlds accessible from each evaluation point that the context widens as needed. If p, would q presupposes that the horizon admits p and asserts that every p-world of the horizon is a q-world, the strict conditional Conditional.strictImp over the horizon. Strengthening the antecedent is then not classically valid, since the strengthened antecedent may fall outside the horizon, but it is valid wherever the conclusion's presupposition holds.

Main definitions

• Conditional.horizonCounterfactual: the counterfactual over a modal horizon, a trivalent proposition.

Main results

• Conditional.exists_mem_of_horizonCounterfactual_eq_one: a true counterfactual has a horizon-world where antecedent and consequent hold together.

Implementation notes

The admissibility of the horizon with respect to an ordering source, a condition on the context that does not mention the antecedent, is left to the caller. Von Fintel's page prints the consequent as evaluated at w; it is evaluated at the horizon-world w', as here.

References

• [vF99a]
• [vF00a]

noncomputable def Conditional.horizonCounterfactual {I : Type u_1} {W : Type u_2} (horizon : I → Set W) (p q : Set W) : I → SignType

If p, would q over a modal horizon presupposes that the horizon admits p and asserts the strict conditional over the horizon ([vF99a]'s (82) and (83)).

Equations

• Conditional.horizonCounterfactual horizon p q = {i : I | (horizon i ∩ p).Nonempty}.indicator fun (i : I) => SignType.ofProp (i ∈ Conditional.strictImp horizon p q)

@[simp]

theorem Conditional.horizonCounterfactual_eq_zero_iff {I : Type u_1} {W : Type u_2} {horizon : I → Set W} {p q : Set W} {i : I} : horizonCounterfactual horizon p q i = 0 ↔ ¬(horizon i ∩ p).Nonempty

@[simp]

theorem Conditional.horizonCounterfactual_eq_one_iff {I : Type u_1} {W : Type u_2} {horizon : I → Set W} {p q : Set W} {i : I} : horizonCounterfactual horizon p q i = 1 ↔ (horizon i ∩ p).Nonempty ∧ horizon i ∩ p ⊆ q

@[simp]

theorem Conditional.horizonCounterfactual_eq_neg_one_iff {I : Type u_1} {W : Type u_2} {horizon : I → Set W} {p q : Set W} {i : I} : horizonCounterfactual horizon p q i = -1 ↔ (horizon i ∩ p).Nonempty ∧ ¬horizon i ∩ p ⊆ q

theorem Conditional.exists_mem_of_horizonCounterfactual_eq_one {I : Type u_1} {W : Type u_2} {horizon : I → Set W} {p q : Set W} {i : I} (h : horizonCounterfactual horizon p q i = 1) : ∃ w ∈ horizon i, w ∈ p ∧ w ∈ q

A true counterfactual has a horizon-world where its antecedent and consequent hold together.