# 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:

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

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

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)