The Hilbert-style system I am using consists of the following axioms:
- $\phi \to (\psi \to \phi)$
- $\phi \to (\psi \to \xi) \to ((\phi \to \psi) \to (\phi \to \xi))$
- $(\neg\phi \to \psi) \to (\neg\phi \to \neg\psi) \to \phi$
and modus ponens
- $\Gamma \vdash \phi \Rightarrow \Gamma \vdash \phi \to \psi \Rightarrow \psi$.
I would like to prove the following metatheorem (call it 'implication metatheorem'):
Implication metatheorem. $\qquad \Gamma \vdash A \Rightarrow \Gamma \vdash B \quad\Longleftrightarrow\quad \Gamma \vdash A \to B$
I already have a proof of the ($\Leftarrow$) direction (which is trivial), but I got stuck on the ($\Rightarrow$) step. My guess is that we need to use the deduction metatheorem and show that $\Gamma, A \vdash B$ holds if any derivation of $A$ from a set of assumptions $\Gamma$ gives a derivation of $B$ from $\Gamma$. This is very intuitive, but now I can't come up with a precise argument that shows that $\Gamma, A \vdash B$ must be the case!
My obvious first attempt was the following:
(i) assume the left-hand side of the equivalence: $\Gamma \vdash A \Rightarrow \Gamma \vdash B$,
(ii) assume $\Gamma$ and $A$ as hypothesis,
(iii) derive $A$,
(iv) derive $B$ using the left-hand side of the equivalence.
but on closer inspection I noticed that the strategy in (iv) has a fatal flaw: what we accomplish is just a derivation of $\Gamma,A \vdash A$, so we cannot use the left-hand side of the equivalence unless we know that $A \in \Gamma$, or a means of reducing it to a derivation of $\Gamma \vdash A$. In other words, that would be to assume the stronger lemma $$\Gamma \vdash A \Rightarrow \Gamma\vdash B \quad\Longrightarrow\quad \Gamma, C \vdash A \Rightarrow \Gamma, C\vdash B$$ but I don't know how to prove that either (is it even true?)