Does the deduction theorem hold in Q?

Question

The proof of the deduction theorem (for a system including Hilbert Calculus) that I am familiar with uses modus ponens to prove the result one way, and mathematical induction the other way.

Robinson's Arithmetic, $Q$, is defined as $PA$ without the induction scheme. Does this entail that the deduction theorem does not hold in $Q$? Or is there another proof?

Answer 1

Yes, deduction theorem holds in Robinson arithmetic $Q$. Let us prove it, relying on the fact that deduction theorem holds for the Hilbert calculus $H$.

Suppose that $\vdash_Q A \to B$, i.e. that $A \to B$ is provable in the system $Q$. System $Q$ is nothing but Hilbert calculus $H$ (its axioms and its inference rules) plus the axioms $Q_1, \dots, Q_7$ of Robinson arithmetic. Therefore, $\vdash_Q A \to B$, means that $Q_1, \dots, Q_7 \vdash_H A \to B$, i.e. $A \to B$ is provable in the system $H$ under the assumptions $Q_1, \dots, Q_7$. By the deduction theorem for the system $H$, we have that $Q_1, \dots, Q_7, A \vdash_H B$, i.e. $B$ is provable in the system $H$ under the assumptions $Q_1, \dots, Q_7, A$. But this exactly means that $A \vdash_Q B$, i.e. $B$ is provable in the system $Q$ under the assumption $A$.

Therefore, we proved that if $\vdash_Q A \to B$ then $A \vdash_Q B$, i.e. the deduction theorem holds for the system $Q$ (Robinson arithmetic).

Answer 2

It's really a bit of a weird question to ask if the deduction theorem holds for $Q$ ... $Q$ is a theory about numbers; its axioms express elementary arithmetical truths. Whereas the Deduction theorem is about logic, so that has really nothing to do with the axioms of $Q$.

Now, it does make sense to say that the Deduction Theorem holds for $H$, because $H$ is a theory for logic: using its axioms, together with Modus Ponens, you can derive logical truths.

But again, to ask whether the deduction theorem holds for $Q$ is misguided. Indeed, typically you are using a proof system in addition to the axioms of $Q$, in order to actually to do some inferencing, and prove further arithmetical truths. And you could then ask whether the Deduction Theorem holds for that proof system.... though typically in the context of discussing $Q$, it is implicitly assumed that we are using a sounds and complete proof system, meaning that the Deduction Theorem does hold for that proof system.