This is an interesting way of thinking about logical counterfactuals. It all seems to come down to what desiderata you desiderate.
We might assign a DAG to WN by choosing a reference theorem-prover, which uses theorems/syntactic rules to generate more theorems. We then draw an edge to each sentence in WN from its direct antecedents in it first proof in the reference theorem-prover. One option is that C(ϕ) would only be allowed to disagree with sentences in WN for sentences that are descendants of ¬ϕ. But this doesn’t specify your G, because it doesn’t assign a place in the graph to sentences not in WN.
If we try a similar theorem-prover assignment to specify C(ϕ) with ϕ false under PA, we’ll get very silly things as soon as the theorem-prover proves ⊥ and explodes; our graph will no longer follow the route analogous to the one for WN. Is there some way to enforce that analogy?
Ideally what I think I desiderate is more complicated than only disagreeing on WN-descendants of ¬ϕ - for example if ϕ is a counterexample to a universal statement that is not a descendant of any individual cases, I’d like the universal statement to be counterfactually disproved.
This is an interesting way of thinking about logical counterfactuals. It all seems to come down to what desiderata you desiderate.
We might assign a DAG to WN by choosing a reference theorem-prover, which uses theorems/syntactic rules to generate more theorems. We then draw an edge to each sentence in WN from its direct antecedents in it first proof in the reference theorem-prover. One option is that C(ϕ) would only be allowed to disagree with sentences in WN for sentences that are descendants of ¬ϕ. But this doesn’t specify your G, because it doesn’t assign a place in the graph to sentences not in WN.
If we try a similar theorem-prover assignment to specify C(ϕ) with ϕ false under PA, we’ll get very silly things as soon as the theorem-prover proves ⊥ and explodes; our graph will no longer follow the route analogous to the one for WN. Is there some way to enforce that analogy?
Ideally what I think I desiderate is more complicated than only disagreeing on WN-descendants of ¬ϕ - for example if ϕ is a counterexample to a universal statement that is not a descendant of any individual cases, I’d like the universal statement to be counterfactually disproved.