What is the difference between derivation rules: NOT-elimination and False-introduction?

My book says they are similar, but they differ in use. I think my book lacks the description of the difference and also when to use which one.

I hope someone can answer my question including a example!

  • Which book are you using? – Mozibur Ullah Mar 20 '14 at 1:25
up vote 1 down vote accepted

The ¬-Elim says that:

If you have:                       ¬P ⊢ ⊥

Then you can conclude:   ⊢ P

Example. Suppose that 3 is not odd(¬O). Derive a contradiction using some number-theoretic fact (⊥). Then by ¬-Elim you can conclude that the assumption (viz. ¬O) was false, so O is the case.


Remark 1. Treating negation in a special way we get the equivalent form:

If you have:                       (P → ⊥) ⊢ ⊥

Then you can conclude:   ⊢ P

Combining this with the deduction theorem, we get the equivalent:

If you have:                       ⊢ (P → ⊥) → ⊥

Then you can conclude:   ⊢ P

Which, once the negation is re-interpreted in classical terms, becomes:

If you have:                        ⊢ ¬¬ P

Then you can conclude:    ⊢ P

Conclusion. ¬-Elim and the rule of "double negation elimination" are the same thing.


The ⊥-Intro rule says this:

If you have:                        ⊢ P   and   ⊢ ¬P

Then you can conclude:    ⊢ ⊥

Example. (this one is more abstract). Suppose that you have been able to derive that some number k is prime (P). If you have also been able to derive that that k has, say three divisors (¬P), then you can appeal to ⊥-Intro to conclude that you have derived a contradiction (⊥). You can then appeal to the fact that you have proved ⊥ to conclude any sentence Q you want (by ⊥-Elim).


Remark 2. The ⊥-Intro rule can also be seen as an instance of modus ponens (→-Elim):

If you have:                        ⊢ P   and   ⊢ (P → ⊥)

Then you can conclude:    ⊢ ⊥

  • Thanks for your explanation. But I meant the negation elimination, not the double negation elimination. Could you change your answer? My book says that one could conclude False from !P and P by both rules. – Tim Mar 19 '14 at 19:32
  • What does the Negation-Elimination rule say according to your book? – Hunan Rostomyan Mar 19 '14 at 19:36
  • Okay, let me try something else. See if it's what you need. – Hunan Rostomyan Mar 19 '14 at 19:41
  • It says: || || \n (k) !P \n || || \n P \n || || \n { !-elim on (k) and (l): } \n (m) False. Sorry for the \n, you would have to format it yourself. Also the ! should be the negation symbol. Looking at the False-introduction however it is completely the same, except the lines with || || consist of three vertical dots. – Tim Mar 19 '14 at 19:44
  • Check it out now. – Hunan Rostomyan Mar 19 '14 at 19:56

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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