reverse direction of modus ponens 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) $$
 A: 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$.
