Deducing material implication from inference rule 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:


*

*Is the above argument sound, or have I missed some subtlety?

*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)
$$
 A: 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).
A: 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)
