You’re right, this shows that the moral axioms as stated don’t work. Essentially [(Prf(C) → U=v) and U<=v] → C simplifies to (Prf(C) → U=v) → C, and if C is absurdity, then ~(Prf(C) → U=v), that is (~U=v and Prf(C)). Both Prf(C) and ~U=v shouldn’t hold. Thus, moral axioms in the present form shouldn’t be added for any easily-provably-false statements. Will try to figure out if the damage can be contained.
(Updated the post and its summary to mention the problem.)
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.
You’re right, this shows that the moral axioms as stated don’t work. Essentially [(Prf(C) → U=v) and U<=v] → C simplifies to (Prf(C) → U=v) → C, and if C is absurdity, then ~(Prf(C) → U=v), that is (~U=v and Prf(C)). Both Prf(C) and ~U=v shouldn’t hold. Thus, moral axioms in the present form shouldn’t be added for any easily-provably-false statements. Will try to figure out if the damage can be contained.
(Updated the post and its summary to mention the problem.)
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.