# 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)$$

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$.

• I edited question. – HoCheol SHIN May 6 '13 at 19:30
• @HoCheolSHIN I think it still comes down to two questions: 1) whether the deduction theorem hold for the proof system; and 2) what exactly do you mean by "$X$ is decidable."? However, re-reading my answer, I think perhaps the first $\mathit{provable}$ ought to be $\mathit{theorem}$, because if $X$ is neither a theorem nor is its negation, (e.g., $A \lor B$), then $\lnot\mathit{provable}(X)$, so the conditional on the left is vacuously true, but $\mathit{provable}(X \to Y)$ could be false (in the case that $Y$ is not a theorem). – Joshua Taylor May 6 '13 at 19:47
• @HoCheolSHIN Regarding my last comment: if by "$X$ is decidable" you mean that either $\mathit{provable}(X) \lor \mathit{provable}(\lnot X)$, then my comment about $\mathit{theorem}$ vs. $\mathit{provable}$ doesn't make a difference. – Joshua Taylor May 6 '13 at 19:53