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

3

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$.

  • 0
    Thank you very much; i don't get in my head how to construct that stuff (proofs in general) any tipps?2012-02-06
  • 0
    @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.2012-02-06
  • 0
    @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.2012-02-07
0

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

  • 0
    $\LaTeX$ tip: `\vdash` produces the $\vdash$ symbol. `\models` produces $\models$2012-03-18
  • 0
    I know, but I **ALWAYS** use ASCII art. And damned, this stack exchange is too stupid to change it automatically into what they prefer.2012-03-18
  • 0
    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.2012-03-18
  • 0
    You're welcome. (Means: I would be pleased, english for "Bitteschön - Dank erwidernd").2012-03-18
  • 0
    Huh? ${}{}{}{}{}{}{}{}$2012-03-18
  • 0
    Mind you, it should read the step from ~~A to A. And my reference is wrong.2012-03-18
  • 0
    Then feel free to fix it...2012-03-18