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

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

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.

• Suppose that $\Gamma$ is ∅. Suppose that A is true, and B is true also. Then $\Gamma$, A $\vdash$ B abbreviates (∅ U {A}) $\vdash$ B or equivalently {A} $\vdash$ B. That holds true. But, if the empty set doesn't imply anything, then $\Gamma$ $\vdash$ (A $\rightarrow$ B) is false, since that's just ∅ $\vdash$ (A $\rightarrow$ B) in other notation. So, the same reasoning used here leads to the Deduction Meta-Theorem failing. Thus, I can't see this answer as correct. Commented Aug 29, 2018 at 22:34
• @DougSpoonwood: (1) We're talking about provability here -- propositional variables have no inherent notion of being true or false, and proofs are conducted without committing to any particular value assignment for them. So "suppose $A$ is true" is not a meaningful statement. (2) $A\vdash B$ is not true. (3) The empty set entails lots of things; for example $\varnothing\vdash A\to A$ holds. Commented Aug 29, 2018 at 22:36
• On second thought I think your answer is correct and my previous comment was in error. Commented Aug 30, 2018 at 0:53
• This is exactly what I was looking for! Thank you so much! :D Commented Sep 13, 2018 at 5:28