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!


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.

  • $\begingroup$ 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. $\endgroup$ – Doug Spoonwood Aug 29 '18 at 22:34
  • $\begingroup$ @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. $\endgroup$ – Henning Makholm Aug 29 '18 at 22:36
  • $\begingroup$ On second thought I think your answer is correct and my previous comment was in error. $\endgroup$ – Doug Spoonwood Aug 30 '18 at 0:53
  • $\begingroup$ This is exactly what I was looking for! Thank you so much! :D $\endgroup$ – StudentType Sep 13 '18 at 5:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.