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

  • 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
    @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
    Then feel free to fix it...2012-03-18