Counterfactuals over sets of antecedent propositions #
This file defines counterfactuals whose antecedent denotes a finite set of propositions, such as the disjuncts of a disjunctive antecedent or the antecedent's truthmakers. Such a counterfactual can be read collectively, quantifying over the closest worlds of the union of the propositions, which is Lewis's treatment of a disjunctive antecedent and does not validate the simplification of disjunctive antecedents, or distributively, requiring the counterfactual of each proposition, which does. The homogeneous reading is super-truth over the propositions: true when every proposition's counterfactual holds, false when none does, and indeterminate otherwise.
Main definitions #
Conditional.disjunctiveImp: the counterfactual over the union of the propositions.Conditional.distributiveImp: the counterfactual of each proposition.Conditional.homogeneousImp: the all-or-nothing verdict over the propositions.
References #
def
Conditional.distributiveImp
{W : Type u_1}
(ord : W → Preorder W)
(S : Finset (Finset W))
(C : Set W)
:
Set W
The distributive reading, on which the counterfactual holds of each proposition in S.
Equations
- Conditional.distributiveImp ord S C = ⋂ A ∈ S, Conditional.closestImp ord (↑A) C
Instances For
@[simp]
theorem
Conditional.mem_distributiveImp
{W : Type u_1}
{ord : W → Preorder W}
{S : Finset (Finset W)}
{C : Set W}
{w : W}
:
w ∈ distributiveImp ord S C ↔ ∀ A ∈ S, w ∈ closestImp ord (↑A) C
def
Conditional.disjunctiveImp
{W : Type u_1}
(ord : W → Preorder W)
(S : Finset (Finset W))
(C : Set W)
[DecidableEq W]
:
Set W
The counterfactual over S quantifies over the closest worlds of the union of its
propositions.
Equations
- Conditional.disjunctiveImp ord S C = Conditional.closestImp ord (↑(S.sup id)) C
Instances For
theorem
Conditional.coe_sup_id
{W : Type u_1}
{S : Finset (Finset W)}
[DecidableEq W]
:
↑(S.sup id) = ⋃ A ∈ S, ↑A
theorem
Conditional.disjunctiveImp_eq_closestImp_iUnion
{W : Type u_1}
{ord : W → Preorder W}
{S : Finset (Finset W)}
{C : Set W}
[DecidableEq W]
:
disjunctiveImp ord S C = closestImp ord (⋃ A ∈ S, ↑A) C
theorem
Conditional.disjunctiveImp_singleton
{W : Type u_1}
{ord : W → Preorder W}
{C : Set W}
[DecidableEq W]
(A : Finset W)
:
disjunctiveImp ord {A} C = closestImp ord (↑A) C
theorem
Conditional.disjunctiveImp_pair
{W : Type u_1}
{ord : W → Preorder W}
{C : Set W}
[DecidableEq W]
(A B : Finset W)
:
disjunctiveImp ord {A, B} C = closestImp ord (↑A ∪ ↑B) C
theorem
Conditional.mem_distributiveImp_pair
{W : Type u_1}
{ord : W → Preorder W}
{C : Set W}
{w : W}
[DecidableEq W]
{A B : Finset W}
:
w ∈ distributiveImp ord {A, B} C ↔ w ∈ closestImp ord (↑A) C ∧ w ∈ closestImp ord (↑B) C
theorem
Conditional.mem_disjunctiveImp_pair_of_mem_distributiveImp
{W : Type u_1}
{ord : W → Preorder W}
{C : Set W}
{w : W}
[DecidableEq W]
{A B : Finset W}
(h : w ∈ distributiveImp ord {A, B} C)
:
w ∈ disjunctiveImp ord {A, B} C
Each proposition's counterfactual entails the counterfactual over the union for a pair.
def
Conditional.homogeneousImp
{W : Type u_1}
(ord : W → Preorder W)
(S : Finset (Finset W))
(C : Set W)
[DecidableEq W]
[Fintype W]
[(w : W) → DecidableRel LE.le]
[DecidablePred fun (x : W) => x ∈ C]
(w : W)
:
SignType
The all-or-nothing verdict over S, super-truth over its propositions' counterfactuals.
Equations
- Conditional.homogeneousImp ord S C w = SignType.supervaluation S fun (A : Finset W) => w ∈ Conditional.closestImp ord (↑A) C
Instances For
@[instance_reducible]
instance
Conditional.instDecidableMemSetDisjunctiveImp
{W : Type u_1}
(ord : W → Preorder W)
(S : Finset (Finset W))
(C : Set W)
[DecidableEq W]
[Fintype W]
[(w : W) → DecidableRel LE.le]
[DecidablePred fun (x : W) => x ∈ C]
(w : W)
:
Decidable (w ∈ disjunctiveImp ord S C)
Equations
- Conditional.instDecidableMemSetDisjunctiveImp ord S C w = { decide := decide (∀ v ∈ {x : W | x ∈ ↑(S.sup id)}, (∀ u ∈ {x : W | x ∈ ↑(S.sup id)}, u ≤ v → v ≤ u) → v ∈ C), reflects_decide := ⋯ }
@[instance_reducible]
instance
Conditional.instDecidableMemSetDistributiveImp
{W : Type u_1}
(ord : W → Preorder W)
(S : Finset (Finset W))
(C : Set W)
[DecidableEq W]
[Fintype W]
[(w : W) → DecidableRel LE.le]
[DecidablePred fun (x : W) => x ∈ C]
(w : W)
:
Decidable (w ∈ distributiveImp ord S C)
Equations
- Conditional.instDecidableMemSetDistributiveImp ord S C w = decidable_of_iff (∀ A ∈ S, w ∈ Conditional.closestImp ord (↑A) C) ⋯
theorem
Conditional.homogeneousImp_eq_one_iff
{W : Type u_1}
{ord : W → Preorder W}
{S : Finset (Finset W)}
{C : Set W}
[DecidableEq W]
[Fintype W]
[(w : W) → DecidableRel LE.le]
[DecidablePred fun (x : W) => x ∈ C]
{w : W}
:
homogeneousImp ord S C w = 1 ↔ w ∈ distributiveImp ord S C
theorem
Conditional.homogeneousImp_eq_neg_one_iff
{W : Type u_1}
{ord : W → Preorder W}
{S : Finset (Finset W)}
{C : Set W}
[DecidableEq W]
[Fintype W]
[(w : W) → DecidableRel LE.le]
[DecidablePred fun (x : W) => x ∈ C]
{w : W}
:
homogeneousImp ord S C w = -1 ↔ S.Nonempty ∧ ∀ A ∈ S, w ∉ closestImp ord (↑A) C
theorem
Conditional.homogeneousImp_eq_zero_iff
{W : Type u_1}
{ord : W → Preorder W}
{S : Finset (Finset W)}
{C : Set W}
[DecidableEq W]
[Fintype W]
[(w : W) → DecidableRel LE.le]
[DecidablePred fun (x : W) => x ∈ C]
{w : W}
:
homogeneousImp ord S C w = 0 ↔ (∃ A ∈ S, w ∈ closestImp ord (↑A) C) ∧ ∃ A ∈ S, w ∉ closestImp ord (↑A) C