Counterpossibles and contradictory consequences

In a previous post, I proposed formalizing counterpossible reasoning with respect to a deductive system. To counterpossibly assume statement S, we'd add S to the axioms of the proof system P, and modify the inference rules so that any inference yielding not-S yields S instead, giving a modified system PS. I've found a possible issue with this, which I think has implications for counterpossibles more generally, or maybe just torpedoes this specific proposal.

Let's suppose that S is not "really true" -- that we can actually prove not-S in P (which is the interesting case for counterpossibles anyway). S would have some counterpossible consequences -- statements S' that are provable in PS, where not-S' is provable in P. If the only way to prove not-S' is via not-S, then there's no problem, since PS will just prove S instead of not-S, and proceed to prove S' instead of not-S'.

However, if there's another way to prove not-S' in P, a way that doesn't go through S, we have a conflict. P will prove not-S' either via not-S, or via this second path; PS, on the other hand, will prove S' if it goes via S, and will prove not-S' if it goes via the second proof path. (Maybe this would be easier to understand with an example, but I don't have one right now.) So, PS will be able to prove both S' and not-S'. Whoops!

There seem to be at least two options, if we want to stick with the deductive-system view of counterpossibles:

1. A precedence rule: if PS can prove some statement via S or via some other path, then the S-path takes precedence, and the other path is ignored. This has the unfortunate effect of making PS's inference rules "non-local", since conclusions don't just depend on premises, but also on everything else the system can prove.
2. Paraconsistent logic: we can allow PS to prove some statements both true and false, and somehow limit the explosion to make sure that the result isn't a world where every statement besides S isn't both true and false.

Of these two, the second is somehow more appealing to me; it really does seem like counterpossibly assuming S is not "enough" to flip not-S' to S' if there is a way to prove not-S' independent of S. This makes these kind of contradictions seem more like a desirable feature of the deductive-system formalization of counterpossibles than a bug. I would be unsatisfied with this, however, if every counterpossible consequence S' of S became both true and false. I'm not sure, generally, whether most statements in deductive proof systems have many proof pathways (which would be bad news for this method), or whether some systems have some statements that can only be proved in one way.

There seem to be a bunch of paraconsistent logics that I could use, and I don't know anything about the pros and cons, thought I like the idea of rejecting disjunctive syllogism and reductio ad absurdum. Intuitively, I don't think I want to completely limit the explosion; it seems to me that statements "downstream" of S' and not-S' should also be both true and false, but statements "upstream" shouldn't be affected, but I can't say precisely what that means.

⁂

Incidentally, it feels to me like this kind of problem shouldn't affect decision-making programs that need to use counterpossible reasoning. My feeling is that a decision-making system shouldn't be able to figure out that some decision it could make would cause a contradiction, since it "should be in a position" to make any decision it would "like" to. This smells to me a little like free will -- the consequences of a decision-maker's actions irreducibly depend on the action itself, and there aren't proof pathways that circumvent the decision entirely. Maybe that provides a lead on how decision-making programs should use counterpossible reasoning, though I don't know how to cash it out formally.

However, the thoughts above certainly seem to me to be applicable to mathematical counterpossibles, like what "would be true" if 2 = 3 or if root 2 were rational -- in those cases, I think we need to use some paraconsistent logic.