1
$\begingroup$

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
    Which axioms are you using?2012-02-06
  • 0
    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)$2012-02-06

2 Answers 2