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

-
Which axioms are you using? – Chris Eagle Feb 6 '12 at 13:01
Excuse me, I forgot them: $\varphi \rightarrow (\psi \rightarrow \varphi)$; $(\varphi \rightarrow (\psi \rightarrow \xi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \xi))$; $(\neg \varphi \rightarrow \neg \psi) \rightarrow (\psi \rightarrow \varphi)$ – tri Feb 6 '12 at 13:04

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$.
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.
 $\LaTeX$ tip: \vdash produces the $\vdash$ symbol. \models produces $\models$ – Arturo Magidin Mar 18 '12 at 20:16 I know, but I ALWAYS use ASCII art. And damned, this stack exchange is too stupid to change it automatically into what they prefer. – Cookie Monster Mar 18 '12 at 20:20 In that case, I hope you don't mind my doing it. I, too spend a lot of time using ASCII art, and I'm glad I don't have to do so here. – Arturo Magidin Mar 18 '12 at 20:23 You're welcome. (Means: I would be pleased, english for "Bitteschön - Dank erwidernd"). – Cookie Monster Mar 18 '12 at 20:24 Huh? ${}{}{}{}{}{}{}{}$ – Arturo Magidin Mar 18 '12 at 20:25