Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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

share|improve this question
1  
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

2 Answers 2

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

share|improve this answer
    
Thank you very much; i don't get in my head how to construct that stuff (proofs in general) any tipps? –  tri Feb 6 '12 at 13:26
    
@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. –  Matt N. Feb 6 '12 at 14:46
    
@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. –  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.

Bye

share|improve this answer
    
$\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

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.