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? Mar 20, 2014 at 1:25

1 Answer 1


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, 2014 at 19:32
  • What does the Negation-Elimination rule say according to your book? Mar 19, 2014 at 19:36
  • Okay, let me try something else. See if it's what you need. Mar 19, 2014 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, 2014 at 19:44
  • Check it out now. Mar 19, 2014 at 19:56

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .