reverse direction of modus ponens

Question

Let $\mathit{pvbl}$ is a formalized provability predicate. If a sentence $X$ is decidable, then following is correct?

$$ \left(\mathit{pvbl}(X) \to \mathit{pvbl}(Y) \right) \implies \mathit{pvbl}(X \to Y) $$

Answer 1

I'm not clear how this is “the reverse direction of modus ponens.” The rule modus ponens says that from $P$ and $P \to Q$, infer $Q$. It would seem like the “reverse direction of modus ponens” would be something like “from $Q$ infer $P$ and $P \to Q$.” Inferring $P \to Q$ from $Q$ is sound, but inferring $P$ from $Q$ is not.

The question above provability is essentially the question of whether the deduction theorem holds for the proof system at hand. It only make sense to speak of a predicate $\mathit{provable}$ encoding provability in some particular proof system. The deduction theorem for some proof system, says that if proof takes some sentence $\phi$ as an assumption and can derive some conclusion $\psi$, then the proof system can also derive $\phi \to \psi$ (without assuming $\phi$). Having the deduction theorem for a proof system can make many proofs much easier to construct, and allows proofs of conditionals through techniques that are much more like natural deduction. The question of whether

$$ \left(\mathit{provable}(X) \to \mathit{provable}(Y)\right) \implies \mathit{provable}(X \to Y) \tag{1}$$

is precisely the question of whether the deduction theorem holds for the proof system at hand.

I don't think the decidability of $X$ comes into play here. The predicate $\mathit{provable}$ characterizes something about the proof system, and not about a particular sentence. Similarly $(1)$ is a claim about a proof system, not about particular sentences $X$ and $Y$.