One immediate idea is to replace the conditional [(Prf(S) → U=u) and U<=u] → S with the rule of inference “from [(Prf(S) → U=u) and U<=u], deduce S”. That way you can’t get a contrapositive, and you probably need to get Loebian to hope to find a contradiction.
Yes, that was the intention, and the problem is that the implication can be tugged from the wrong side, but implication can’t be one-sided. I’d prefer to stay with standard inference rules though, if at all possible.
One immediate idea is to replace the conditional [(Prf(S) → U=u) and U<=u] → S with the rule of inference “from [(Prf(S) → U=u) and U<=u], deduce S”. That way you can’t get a contrapositive, and you probably need to get Loebian to hope to find a contradiction.
Not confident at all that would work, though.
Yes, that was the intention, and the problem is that the implication can be tugged from the wrong side, but implication can’t be one-sided. I’d prefer to stay with standard inference rules though, if at all possible.
Pulling on one side but not the other seems textbook of what relevance logics were designed for.