Neat. Okay, here’s my sketch of a counterexample (or more precisely, a way in which this may violate my imagined desiderata for counterfactuals). A statement ϕ that leads to a to a short proof of ⊥ does not seem like the counterfactual ancestor of every single statement ψ that does not lead to a short proof of ⊥.
E.g. “5263=3126” doesn’t seem like it counterfactually implies that there exists a division of the plane that requires at least 5 colors to fill in without having identical colors touch. It seem much more like it counterfactually implies “5163=3063″ (i.e. the converse of the trolljecture seems really false).
But I dunno, maybe that’s just my aesthetics about proofs that go through ⊥. Presumably “legitimate counterfactual consequence” could be cashed out as some sort of pragmatic statement about a decision-making algorithm?
Neat. Okay, here’s my sketch of a counterexample (or more precisely, a way in which this may violate my imagined desiderata for counterfactuals). A statement ϕ that leads to a to a short proof of ⊥ does not seem like the counterfactual ancestor of every single statement ψ that does not lead to a short proof of ⊥.
E.g. “5263=3126” doesn’t seem like it counterfactually implies that there exists a division of the plane that requires at least 5 colors to fill in without having identical colors touch. It seem much more like it counterfactually implies “5163=3063″ (i.e. the converse of the trolljecture seems really false).
But I dunno, maybe that’s just my aesthetics about proofs that go through ⊥. Presumably “legitimate counterfactual consequence” could be cashed out as some sort of pragmatic statement about a decision-making algorithm?