# Logical reasoning: What is the difference between NOT-elimination and False-introduction?

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

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