A Hilbert-style proof that $\Gamma \vdash A \Rightarrow \Gamma \vdash B \Longleftrightarrow \Gamma \vdash A \to B$

Question

The Hilbert-style system I am using consists of the following axioms:

1. $\phi \to (\psi \to \phi)$
2. $\phi \to (\psi \to \xi) \to ((\phi \to \psi) \to (\phi \to \xi))$
3. $(\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!

Edit:

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

Answer 1

The $\Rightarrow$ direction you want to prove does not hold.

As a counterexample, let $A$ and $B$ be different propositional variables, and let $\Gamma$ be empty.

Then $\varnothing\vdash A \Rightarrow \varnothing\vdash B$ is true (because $\varnothing\vdash A$ and $\varnothing\vdash B$ are both false), but $\varnothing\vdash A\to B$ is false.

---

The metatheorem that does hold is: $$ \Gamma, A \vdash B \iff \Gamma \vdash A \to B $$ whose $\Rightarrow$ direction is the (nontrivial) Deduction Theorem.