Contradiction Theorem I'm a beginner in formal logic. Can anyone of you help me with the proof of the following lemma:
For any Theory $T$ and closed formula $\varphi$ it holds that $T \vdash \varphi$ if and only if $T,\neg \varphi$ is inconsistent. 
The left to right direction is easy, but I'm struggling with the right-to-left direction. I realize that (according to the deduction theorem), it holds that
$T \vdash \neg \varphi \rightarrow \varphi$
Obviously $T \vdash \varphi$ must hold. However, I'm not allowed to assume completeness of first order logic (but soundness though); so do I have to construct a proof of $\varphi$ assuming that I have a proof of $\neg \varphi \rightarrow \varphi$ (we are using a Hilbert-Type-Calculus with MP as the only rule)?
 A: We have that $T$ and $\neg \varphi$ are inconsistent, so $T, \neg \varphi \vdash \psi$ for any $\psi$. This will be most useful if we let $\psi$ be the negation of some easily proven tautology, say $\psi=\neg(\varphi \rightarrow (\varphi \rightarrow \varphi))$. Then by the deduction theorem, we have $T \vdash \neg \varphi \rightarrow \neg (\varphi \rightarrow (\varphi \rightarrow \varphi))$. Using the third axiom and modus ponens, we get $T \vdash (\varphi \rightarrow (\varphi \rightarrow \varphi)) \rightarrow \varphi$. Since we can easily prove $T \vdash \varphi \rightarrow (\varphi \rightarrow \varphi)$, modus ponens gives us $T \vdash \varphi$.
A: The easiest would be to say $S$ inconsistent $\iff S\vdash \text{f}$. 
We then have if $T, {\neg}A$ inconsistent, then 
$$T,{\neg}A\vdash\text{f}$$
By the deduction theorem we have:
$$T\vdash {\neg}{\neg}A$$
By double negation elimination we have:
$$T\vdash A$$
There is a twist, the deduction theorem is a derived rule in
most Hilbert Style systems. So the above is a real meta theorem,
it doesn't show a fixed number of steps to arrive from $T, {\neg}A \vdash \text{f}$
to $T \vdash {\neg}{\neg}A$. Also the step from ${\neg}{\neg}A$ to $A$ can be quite tedious.
Bye
