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

  • $\begingroup$ I edited question. $\endgroup$ – HoCheol SHIN May 6 '13 at 19:30
  • $\begingroup$ @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). $\endgroup$ – Joshua Taylor May 6 '13 at 19:47
  • $\begingroup$ @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. $\endgroup$ – Joshua Taylor May 6 '13 at 19:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.