Deducing material implication from inference rule

Question

Say I have a rule of inference $$ \vdash P\Rightarrow\;\vdash Q, $$ where $\Rightarrow$ denotes logical inference (as opposed to material implication) and $P$ and $Q$ are some forms. For example, $P$ may be of form $\varphi$ and $Q$ may be of form $\forall x\varphi$.

Then I propose an (arbitrary) instance of $$ \vdash P\rightarrow Q, $$ with $\rightarrow$ denoting material implication.

This seems to follow from a metalogical argument by cases. For a given instance of $P$ and corresponding instance of $Q$, if you have $P$, then you can deduce $Q$, and thus, both being true, $P\rightarrow Q$. If you have rather $\neg P$, $P\rightarrow Q$ is immediately vacuously true.

However, I've not been able to construct an argument to this effect in the system. This leads me to two questions:

1. Is the above argument sound, or have I missed some subtlety?
2. If it is sound, can it be shown in the system for a given rule and instantiation, or if not, what modification to the system must be made to assert such a conclusion?

"The system" being typical classical logic, say modus ponens and a typical axiomatization: $$ \vdash\varphi\;\&\vdash\varphi\rightarrow\psi\Rightarrow\enspace\vdash\psi\\\vdash\varphi\rightarrow(\psi\rightarrow\varphi)\\\vdash(\varphi\rightarrow(\psi\rightarrow\chi))\rightarrow((\varphi\rightarrow\psi)\rightarrow(\varphi\rightarrow\chi))\\\vdash(\neg\varphi\rightarrow\neg\psi)\rightarrow(\psi\rightarrow\varphi) $$

Answer 1

As far as I understand, your deductive system is the Hilbert calculus for classical propositional logic.

The property that you want to prove is the deduction theorem: roughly, it says that if we deduce a proposition $B$ on the assumption of a proposition $A$, then we conclude that the implication "If $A$ then $B$" holds (i.e. $A \to B$ is derivable). Deduction theorem explains why proofs of conditional sentences in mathematics are logically correct.

The proof of this property is by induction on the length of the derivation of $B$ from the assumption $A$. For details, see here (and here for a discussion).

Answer 2

For completeness, the answer to the second question:

The deduction theorem depends on the existence of a theorem to deduce the following form: $$ \vdash H \rightarrow P\\ \vdash H \rightarrow Q\\ ...\\ \vdash H \rightarrow R $$ where $$ \vdash P\;\&\vdash Q\;\&\;... \Rightarrow\;\vdash R\\ $$ for all inference rules in the system. For example, for modus ponens: $$ \vdash H \rightarrow \varphi\\ \vdash H \rightarrow (\varphi \rightarrow \psi)\\ \vdash(H \rightarrow (\varphi \rightarrow \psi))\rightarrow ((H\rightarrow \varphi) \rightarrow (H \rightarrow \psi)) $$ and then by modus ponens twice, $\vdash H\rightarrow \psi$.

For the example I used of $\vdash\varphi\Rightarrow\;\vdash\forall x\varphi$, the axiom typically providing for this prerequisite theorem is $\vdash\varphi\rightarrow\forall x\varphi,\ x\ \text{not free in}\ \varphi$. Obviously this is the desired implication, but from this axiom follows $\vdash(H\rightarrow\varphi)\rightarrow(H\rightarrow\forall x\varphi),\ x\ \text{not free in}\ \varphi$, which would be sufficient for the deduction theorem to hold.

(NB: The restriction on $x$ being not free in $\varphi$ is not a weakening as compared to the inference rule, as it too requires that $x$ not be free in $\varphi$. The non-freeness of $x$ is however implied by $\vdash\varphi$, as no variable is free in a theorem)