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