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

  • 1
    $\begingroup$ Which axioms are you using? $\endgroup$ – Chris Eagle Feb 6 '12 at 13:01
  • $\begingroup$ 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)$ $\endgroup$ – 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$.

  • $\begingroup$ Thank you very much; i don't get in my head how to construct that stuff (proofs in general) any tipps? $\endgroup$ – tri Feb 6 '12 at 13:26
  • $\begingroup$ @tri Mostly, the "easier" proofs are either by induction or by contradiction (or by contraposition, as in my answer above). So if you want to prove something first check if you can use any of these techniques. $\endgroup$ – Rudy the Reindeer Feb 6 '12 at 14:46
  • $\begingroup$ @tri Another common technique is to use tautologies in various ways, which requires a lot of practice to have a library of useful tautologies in your head. $\endgroup$ – Carl Mummert Feb 7 '12 at 12:58

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.


  • $\begingroup$ $\LaTeX$ tip: \vdash produces the $\vdash$ symbol. \models produces $\models$ $\endgroup$ – Arturo Magidin Mar 18 '12 at 20:16
  • $\begingroup$ I know, but I ALWAYS use ASCII art. And damned, this stack exchange is too stupid to change it automatically into what they prefer. $\endgroup$ – j4n bur53 Mar 18 '12 at 20:20
  • $\begingroup$ 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. $\endgroup$ – Arturo Magidin Mar 18 '12 at 20:23
  • $\begingroup$ You're welcome. (Means: I would be pleased, english for "Bitteschön - Dank erwidernd"). $\endgroup$ – j4n bur53 Mar 18 '12 at 20:24
  • $\begingroup$ Huh? ${}{}{}{}{}{}{}{}$ $\endgroup$ – Arturo Magidin Mar 18 '12 at 20:25

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.